UFDT (Single Query Track)

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

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

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

Winners

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

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
2020-CVC4n	0	534	1282014.526	1296328.106	534	124	410	1016	1016	0
cvc5	0	527	1289317.498	1306194.932	527	122	405	1023	1023	0
Vampire	0	357	1464303.357	1437187.024	357	1	356	1193	1190	0
z3-4.8.17n	0	241	1235491.046	1243372.458	241	12	229	1309	816	26
smtinterpol	0	96	1699084.984	1696070.05	96	1	95	1454	1405	0
UltimateEliminator+MathSAT	0	0	7422.385	4363.401	0	0	0	1550	0	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
2020-CVC4n	0	534	1293697.246	1296277.646	534	124	410	1016	1016	0
cvc5	0	527	1304124.398	1306144.422	527	122	405	1023	1023	0
Vampire	0	402	1784998.007	1418315.983	402	14	388	1148	1144	0
z3-4.8.17n	0	241	1236579.136	1243333.648	241	12	229	1309	816	26
smtinterpol	0	96	1727325.884	1688281.137	96	1	95	1454	1384	0
UltimateEliminator+MathSAT	0	0	7422.385	4363.401	0	0	0	1550	0	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
2020-CVC4n	0	124	61129.316	63397.411	124	124	0	4	1422	1016	0
cvc5	0	122	65221.819	66956.303	122	122	0	6	1422	1023	0
Vampire	0	14	229527.85	151954.308	14	14	0	114	1422	1144	0
z3-4.8.17n	0	12	111966.945	114491.068	12	12	0	116	1422	816	26
smtinterpol	0	1	137562.192	133857.24	1	1	0	127	1422	1384	0
UltimateEliminator+MathSAT	0	0	620.191	358.333	0	0	0	128	1422	0	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
2020-CVC4n	0	410	73367.929	73680.235	410	0	410	46	1094	1016	0
cvc5	0	405	79702.58	79988.118	405	0	405	51	1094	1023	0
Vampire	0	388	209061.617	107425.955	388	0	388	68	1094	1144	0
z3-4.8.17n	0	229	204036.76	204603.699	229	0	229	227	1094	816	26
smtinterpol	0	95	448721.597	433572.95	95	0	95	361	1094	1384	0
UltimateEliminator+MathSAT	0	0	2160.638	1291.777	0	0	0	456	1094	0	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
2020-CVC4n	0	329	29730.762	29730.746	329	2	327	1221	1221	0
cvc5	0	323	29802.12	29802.055	323	2	321	1227	1227	0
Vampire	0	281	34073.555	31347.994	281	0	281	1269	1266	0
z3-4.8.17n	0	225	31887.265	31886.849	225	12	213	1325	1295	26
smtinterpol	0	53	35418.891	35059.732	53	1	52	1497	1448	0
UltimateEliminator+MathSAT	0	0	7422.385	4363.401	0	0	0	1550	0	0

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