UF (Single Query Track)

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

Page generated on 2022-08-10 11:17:45 +0000

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

Winners

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

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Vampire	0	1174	2087649.023	2026086.574	1174	470	704	1683	1671	0
cvc5	0	1162	2237927.348	2259838.879	1162	392	770	1695	1695	0
2020-CVC4n	0	1151	2252563.612	2270202.525	1151	397	754	1706	1706	0
veriT	0	669	2599147.673	2599272.115	669	0	669	2188	2050	75
z3-4.8.17n	0	478	2188074.757	2188369.349	478	61	417	2379	1409	39
Yices2	0	345	3028209.76	3028546.539	345	39	306	2512	2512	0
smtinterpol	0	200	3191138.475	3186265.681	200	6	194	2657	2638	0
UltimateEliminator+MathSAT	0	0	15457.022	9606.887	0	0	0	2857	0	1

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Vampire	0	1219	2509811.593	2001426.676	1219	473	746	1638	1626	0
cvc5	0	1162	2256199.028	2259756.349	1162	392	770	1695	1695	0
2020-CVC4n	0	1151	2266893.382	2270123.615	1151	397	754	1706	1706	0
veriT	0	669	2599411.743	2599189.215	669	0	669	2188	2050	75
z3-4.8.17n	0	478	2188307.857	2188305.189	478	61	417	2379	1409	39
Yices2	0	345	3028480.45	3028452.179	345	39	306	2512	2512	0
smtinterpol	0	203	3332603.025	3154938.852	203	7	196	2654	2545	0
UltimateEliminator+MathSAT	0	0	15457.022	9606.887	0	0	0	2857	0	1

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
Vampire	0	473	51093.538	19206.409	473	473	0	15	2369	1626	0
2020-CVC4n	0	397	297721.317	300654.002	397	397	0	91	2369	1706	0
cvc5	0	392	309418.903	312799.909	392	392	0	96	2369	1695	0
z3-4.8.17n	0	61	383672.829	383684.37	61	61	0	427	2369	1409	39
Yices2	0	39	539261.894	539262.061	39	39	0	449	2369	2512	0
smtinterpol	0	7	578684.38	552752.462	7	7	0	481	2369	2545	0
UltimateEliminator+MathSAT	0	0	2412.898	1420.145	0	0	0	488	2369	0	1
veriT	0	0	547095.18	546988.798	0	0	0	488	2369	2050	75

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	770	105980.125	106156.439	770	0	770	65	2022	1695	0
2020-CVC4n	0	754	128372.065	128669.612	754	0	754	81	2022	1706	0
Vampire	0	746	279501.035	142215.367	746	0	746	89	2022	1626	0
veriT	0	669	215249.502	215133.268	669	0	669	166	2022	2050	75
z3-4.8.17n	0	417	405853.876	405793.241	417	0	417	418	2022	1409	39
Yices2	0	306	648418.555	648390.119	306	0	306	529	2022	2512	0
smtinterpol	0	196	814790.415	781334.398	196	0	196	639	2022	2545	0
UltimateEliminator+MathSAT	0	0	5391.534	3652.618	0	0	0	835	2022	0	1

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Vampire	0	931	53132.228	47874.613	931	371	560	1926	1915	0
veriT	0	622	54013.387	54002.354	622	0	622	2235	2142	75
cvc5	0	621	54274.654	54274.774	621	11	610	2236	2236	0
2020-CVC4n	0	592	55038.886	55036.268	592	9	583	2265	2265	0
z3-4.8.17n	0	423	58807.058	58806.351	423	56	367	2434	2395	39
Yices2	0	283	62265.264	62265.541	283	36	247	2574	2574	0
smtinterpol	0	123	66549.422	65835.163	123	5	118	2734	2719	0
UltimateEliminator+MathSAT	0	0	14281.022	8430.887	0	0	0	2857	0	1

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