LIA (Single Query Track)

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

Page generated on 2021-07-18 17:29:05 +0000

Benchmarks: 191
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-z3n	0	191	8.828	8.848	191	83	108	0	0	0
2020-CVC4n	0	191	22.722	22.669	191	83	108	0	0	0
cvc5 - fixedn	0	191	65.533	65.5	191	83	108	0	0	0
cvc5	0	191	67.176	64.52	191	83	108	0	0	0
z3n	0	187	4806.065	4806.224	187	83	104	4	4	0
UltimateEliminator+MathSAT	0	147	61011.451	59483.947	147	43	104	44	44	0
Vampire	0	108	100933.93	100021.874	108	4	104	83	83	0
Vampire - fixedn	0	106	101818.537	100258.481	106	2	104	85	83	0
SMTInterpol	0	62	63791.374	63238.223	62	4	58	129	45	0
veriT	0	49	16176.927	16172.143	49	0	49	142	13	0
iProver	0	49	162611.653	162186.142	49	0	49	142	135	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
2020-z3n	0	191	8.828	8.848	191	83	108	0	0	0
2020-CVC4n	0	191	22.722	22.669	191	83	108	0	0	0
cvc5	0	191	67.176	64.52	191	83	108	0	0	0
cvc5 - fixedn	0	191	65.533	65.5	191	83	108	0	0	0
z3n	0	187	4806.165	4806.204	187	83	104	4	4	0
UltimateEliminator+MathSAT	0	147	61011.451	59483.947	147	43	104	44	44	0
Vampire	0	108	100933.93	100021.874	108	4	104	83	83	0
Vampire - fixedn	0	106	105418.727	100250.421	106	2	104	85	83	0
SMTInterpol	0	62	63791.374	63238.223	62	4	58	129	45	0
veriT	0	49	16178.357	16171.673	49	0	49	142	13	0
iProver	0	49	162611.653	162186.142	49	0	49	142	135	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
z3n	0	83	3.281	3.309	83	83	0	0	108	4	0
2020-z3n	0	83	4.404	4.419	83	83	0	0	108	0	0
2020-CVC4n	0	83	18.14	18.114	83	83	0	0	108	0	0
cvc5	0	83	58.786	56.18	83	83	0	0	108	0	0
cvc5 - fixedn	0	83	56.999	57.014	83	83	0	0	108	0	0
UltimateEliminator+MathSAT	0	43	53730.538	52844.234	43	43	0	40	108	44	0
SMTInterpol	0	4	51235.577	50901.074	4	4	0	79	108	45	0
Vampire	0	4	94807.891	94802.661	4	4	0	79	108	83	0
Vampire - fixedn	0	2	100800.54	97192.141	2	2	0	81	108	83	0
veriT	0	0	101.196	94.377	0	0	0	83	108	13	0
iProver	0	0	97200.974	97201.54	0	0	0	83	108	135	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-z3n	0	108	4.424	4.429	108	0	108	0	83	0	0
2020-CVC4n	0	108	4.581	4.555	108	0	108	0	83	0	0
cvc5	0	108	8.39	8.34	108	0	108	0	83	0	0
cvc5 - fixedn	0	108	8.534	8.486	108	0	108	0	83	0	0
Vampire - fixedn	0	104	4618.187	3058.28	104	0	104	4	83	83	0
z3n	0	104	4802.883	4802.894	104	0	104	4	83	4	0
Vampire	0	104	6126.039	5219.213	104	0	104	4	83	83	0
UltimateEliminator+MathSAT	0	104	7280.913	6639.713	104	0	104	4	83	44	0
SMTInterpol	0	58	12555.797	12337.15	58	0	58	50	83	45	0
veriT	0	49	16077.161	16077.296	49	0	49	59	83	13	0
iProver	0	49	65410.679	64984.602	49	0	49	59	83	135	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
2020-z3n	0	191	8.828	8.848	191	83	108	0	0	0
2020-CVC4n	0	191	22.722	22.669	191	83	108	0	0	0
cvc5	0	191	67.176	64.52	191	83	108	0	0	0
cvc5 - fixedn	0	191	65.533	65.5	191	83	108	0	0	0
z3n	0	187	102.165	102.204	187	83	104	4	4	0
UltimateEliminator+MathSAT	0	113	2788.303	2357.206	113	21	92	78	78	0
Vampire	0	104	2283.52	2177.606	104	4	100	87	87	0
Vampire - fixedn	0	100	2311.277	2225.157	100	2	98	91	90	0
SMTInterpol	0	62	2032.222	1885.713	62	4	58	129	73	0
veriT	0	49	479.917	473.186	49	0	49	142	15	0
iProver	0	48	3728.855	3412.834	48	0	48	143	136	0

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