UFLIA (Single Query Track)

Competition results for the UFLIA logic in the Single Query Track.

Page generated on 2023-07-06 16:04:54 +0000

Benchmarks: 2849
Time Limit: 1200 seconds
Memory Limit: 60 GB

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24s Performance (parallel)
cvc5	cvc5	SMTInterpol	cvc5	cvc5

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
cvc5	0	1606	36898.006	37550.989	1606	2	1604	1243	1226	0
2022-cvc5n	0	1605	38431.333	38768.584	1605	2	1603	1244	1225	0
Vampire	0	1328	74007.452	18814.096	1328	0	1328	1521	1521	0
iProver	0	662	78604.843	20210.114	662	0	662	2187	2187	0
iProver Fixedn	0	647	76105.134	19635.863	647	0	647	2202	2201	0
SMTInterpol	0	406	30895.522	25020.676	406	5	401	2443	2380	0
UltimateEliminator+MathSAT	0	0	0.0	0.0	0	0	0	2849	7	2

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
cvc5	0	1606	36898.006	37550.989	1606	2	1604	1243	1226	0
2022-cvc5n	0	1605	38431.333	38768.584	1605	2	1603	1244	1225	0
Vampire	0	1380	202465.072	51118.363	1380	0	1380	1469	1469	0
iProver	0	691	144276.493	36808.466	691	0	691	2158	2158	0
iProver Fixedn	0	682	153167.114	39174.851	682	0	682	2167	2165	0
SMTInterpol	0	407	32213.002	26213.586	407	5	402	2442	2336	0
UltimateEliminator+MathSAT	0	0	0.0	0.0	0	0	0	2849	7	2

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
SMTInterpol	0	5	4.209	2.495	5	5	0	5	2839	2336	0
2022-cvc5n	0	2	513.229	516.977	2	2	0	8	2839	1225	0
cvc5	0	2	514.824	539.181	2	2	0	8	2839	1226	0
Vampire	0	0	0.0	0.0	0	0	0	10	2839	1469	0
UltimateEliminator+MathSAT	0	0	0.0	0.0	0	0	0	10	2839	7	2
iProver	0	0	0.0	0.0	0	0	0	10	2839	2158	0
iProver Fixedn	0	0	0.0	0.0	0	0	0	10	2839	2165	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
cvc5	0	1604	36383.183	37011.808	1604	0	1604	80	1165	1226	0
2022-cvc5n	0	1603	37918.104	38251.606	1603	0	1603	81	1165	1225	0
Vampire	0	1380	202465.072	51118.363	1380	0	1380	304	1165	1469	0
iProver	0	691	144276.493	36808.466	691	0	691	993	1165	2158	0
iProver Fixedn	0	682	153167.114	39174.851	682	0	682	1002	1165	2165	0
SMTInterpol	0	402	32208.793	26211.091	402	0	402	1282	1165	2336	0
UltimateEliminator+MathSAT	0	0	0.0	0.0	0	0	0	1684	1165	7	2

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
cvc5	0	1428	2398.563	2387.4	1428	1	1427	1421	1415	0
2022-cvc5n	0	1413	2723.519	2679.769	1413	1	1412	1436	1430	0
Vampire	0	1147	9539.661	2576.099	1147	0	1147	1702	1702	0
iProver	0	475	7855.906	2163.704	475	0	475	2374	2374	0
iProver Fixedn	0	469	7601.776	2112.888	469	0	469	2380	2380	0
SMTInterpol	0	323	2942.872	1239.514	323	5	318	2526	2465	0
UltimateEliminator+MathSAT	0	0	0.0	0.0	0	0	0	2849	122	2

n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.