LIA (Single Query Track)

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

Page generated on 2020-07-04 11:46:58 +0000

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

Winners

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

Note: the division has disagreements

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
z3n	0	198	9.388	9.421	198	90	108	0		0	0
2019-Z3n	0	198	9.82	9.844	198	90	108	0		0	0
CVC4	0	198	28.427	28.379	198	90	108	0		0	0
UltimateEliminator+MathSAT	0	107	54687.279	54230.272	107	21	86	91		44	0
Vampire	0	100	117705.432	117649.543	100	1	99	98		98	0
SMTInterpol-fixedn	0	71	73496.382	72975.958	71	7	64	127		51	0
SMTInterpol	0	71	73519.75	72989.521	71	7	64	127		51	0
veriT	0	42	156754.891	156587.06	42	0	42	156		104	0
veriT+viten	0	42	184798.26	184811.878	42	0	42	156		153	1

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
z3n	0	198	9.388	9.421	198	90	108	0		0	0
2019-Z3n	0	198	9.82	9.844	198	90	108	0		0	0
CVC4	0	198	28.427	28.379	198	90	108	0		0	0
UltimateEliminator+MathSAT	0	107	54687.279	54230.272	107	21	86	91		44	0
Vampire	0	100	121305.582	117645.443	100	1	99	98		98	0
SMTInterpol-fixedn	0	71	73496.382	72975.958	71	7	64	127		51	0
SMTInterpol	0	71	73519.75	72989.521	71	7	64	127		51	0
veriT	0	42	156762.031	156584.04	42	0	42	156		104	0
veriT+viten	0	42	184807.49	184807.528	42	0	42	156		153	1

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
z3n	0	90	4.786	4.794	90	90	0	108	0	0
2019-Z3n	0	90	4.904	4.907	90	90	0	108	0	0
CVC4	0	90	22.638	22.62	90	90	0	108	0	0
UltimateEliminator+MathSAT	0	21	39923.813	39594.91	21	21	0	177	44	0
SMTInterpol-fixedn	0	7	57760.433	57415.946	7	7	0	191	51	0
SMTInterpol	0	7	57772.377	57421.458	7	7	0	191	51	0
Vampire	0	1	110400.273	106795.974	1	1	0	197	98	0
veriT	0	0	99996.24	99996.887	0	0	0	198	104	0
veriT+viten	0	0	106807.049	106807.048	0	0	0	198	153	1

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
z3n	0	108	4.602	4.627	108	0	108	90	0	0
2019-Z3n	0	108	4.916	4.937	108	0	108	90	0	0
CVC4	0	108	5.79	5.759	108	0	108	90	0	0
Vampire	0	99	10905.31	10849.468	99	0	99	99	98	0
UltimateEliminator+MathSAT	0	86	14763.466	14635.362	86	0	86	112	44	0
SMTInterpol-fixedn	0	64	15735.949	15560.013	64	0	64	134	51	0
SMTInterpol	0	64	15747.373	15568.062	64	0	64	134	51	0
veriT	0	42	56765.791	56587.153	42	0	42	156	104	0
veriT+viten	0	42	78000.441	78000.48	42	0	42	156	153	1

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
z3n	0	198	9.388	9.421	198	90	108	0		0	0
2019-Z3n	0	198	9.82	9.844	198	90	108	0		0	0
CVC4	0	198	28.427	28.379	198	90	108	0		0	0
UltimateEliminator+MathSAT	0	106	1934.805	1645.713	106	20	86	92		51	0
Vampire	0	100	2457.432	2401.543	100	1	99	98		98	0
SMTInterpol-fixedn	0	71	2249.73	2080.277	71	7	64	127		78	0
SMTInterpol	0	71	2266.344	2083.56	71	7	64	127		78	0
veriT+viten	0	42	3703.49	3703.528	42	0	42	156		153	1
veriT	0	42	3720.59	3720.584	42	0	42	156		155	0

n Non-competing.
Abstained: Total of benchmarks in logics in this division that solver chose to abstain from. For SAT/UNSAT scores, this column also includes benchmarks not known to be SAT/UNSAT.