LIA (Single Query Track)

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

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

Benchmarks: 300
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
cvc5	0	300	78.701	78.663	300	137	163	0	0	0
2021-z3n	0	292	9.539	9.561	292	137	155	8	8	0
UltimateEliminator+MathSAT	0	243	10584.247	8693.446	243	83	160	57	57	0
YicesQS	0	179	1034.75	1034.924	179	97	82	121	121	0
iProver Fixedn	0	116	1217.929	360.401	116	0	116	184	173	0
SMTInterpol	0	98	135.088	91.251	98	8	90	202	98	0
iProver	21	128	2431.876	663.696	128	0	128	172	140	0
Vampire	127	162	863.351	233.043	162	0	162	138	11	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
cvc5	0	300	78.701	78.663	300	137	163	0	0	0
2021-z3n	0	292	9.539	9.561	292	137	155	8	8	0
UltimateEliminator+MathSAT	0	245	13095.917	11031.176	245	85	160	55	55	0
YicesQS	0	179	1034.75	1034.924	179	97	82	121	121	0
iProver Fixedn	0	116	1217.929	360.401	116	0	116	184	173	0
SMTInterpol	0	98	135.088	91.251	98	8	90	202	98	0
iProver	21	129	5767.756	1508.376	129	0	129	171	139	0
Vampire	127	162	863.351	233.043	162	0	162	138	11	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
2021-z3n	0	137	5.427	5.436	137	137	0	0	163	8	0
cvc5	0	137	60.141	60.171	137	137	0	0	163	0	0
YicesQS	0	97	1028.942	1029.075	97	97	0	40	163	121	0
UltimateEliminator+MathSAT	0	85	10638.683	9230.434	85	85	0	52	163	55	0
SMTInterpol	0	8	4.375	3.063	8	8	0	129	163	98	0
Vampire	0	0	0.0	0.0	0	0	0	137	163	11	0
iProver	0	0	0.0	0.0	0	0	0	137	163	139	0
iProver Fixedn	0	0	0.0	0.0	0	0	0	137	163	173	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	163	18.56	18.492	163	0	163	0	137	0	0
UltimateEliminator+MathSAT	0	160	2457.234	1800.742	160	0	160	3	137	55	0
2021-z3n	0	155	4.112	4.124	155	0	155	8	137	8	0
iProver Fixedn	0	116	1217.929	360.401	116	0	116	47	137	173	0
SMTInterpol	0	90	130.713	88.189	90	0	90	73	137	98	0
YicesQS	0	82	5.808	5.849	82	0	82	81	137	121	0
iProver	21	129	5767.756	1508.376	129	0	129	34	137	139	0
Vampire	127	162	863.351	233.043	162	0	162	1	137	11	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
cvc5	0	300	78.701	78.663	300	137	163	0	0	0
2021-z3n	0	292	9.539	9.561	292	137	155	8	8	0
UltimateEliminator+MathSAT	0	212	2310.811	1120.735	212	61	151	88	88	0
YicesQS	0	170	55.381	55.538	170	88	82	130	130	0
iProver Fixedn	0	114	855.088	266.991	114	0	114	186	175	0
SMTInterpol	0	98	135.088	91.251	98	8	90	202	132	0
iProver	16	126	1190.466	347.603	126	0	126	174	147	0
Vampire	126	161	175.941	59.722	161	0	161	139	13	0

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