UFLRA (Single Query Track)

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

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

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

Winners

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

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
z3n	0	6	1431.115	1431.338	6	4	2	1	1	0
2020-z3n	0	6	1801.717	1802.012	6	4	2	1	1	0
2018-Z3n	0	5	3654.854	3655.492	5	3	2	2	2	0
cvc5 - fixedn	0	2	1242.105	6000.308	2	0	2	5	5	0
cvc5	0	2	2470.116	6000.328	2	0	2	5	5	0
veriT	0	2	4799.824	4800.493	2	0	2	5	4	0
SMTInterpol	0	2	4801.792	4801.199	2	0	2	5	4	0
iProver	0	2	4883.147	4822.324	2	0	2	5	4	0
2020-CVC4n	0	2	5993.214	6000.303	2	0	2	5	5	0
2020-Vampiren	0	2	6006.15	6002.508	2	0	2	5	5	0
UltimateEliminator+MathSAT	0	0	34.306	21.166	0	0	0	7	0	0
Vampire	0	0	8400.0	8400.0	0	0	0	7	7	0
Vampire - fixedn	0	0	8400.0	8400.0	0	0	0	7	7	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
z3n	0	6	1431.275	1431.308	6	4	2	1	1	0
2020-z3n	0	6	1801.797	1801.992	6	4	2	1	1	0
2018-Z3n	0	5	3655.234	3655.452	5	3	2	2	2	0
veriT	0	2	4800.344	4800.343	2	0	2	5	4	0
SMTInterpol	0	2	4801.792	4801.199	2	0	2	5	4	0
iProver	0	2	4883.147	4822.324	2	0	2	5	4	0
2020-CVC4n	0	2	6000.034	6000.033	2	0	2	5	5	0
cvc5 - fixedn	0	2	6000.039	6000.038	2	0	2	5	5	0
cvc5	0	2	6000.039	6000.038	2	0	2	5	5	0
2020-Vampiren	0	2	6006.15	6002.508	2	0	2	5	5	0
Vampire - fixedn	0	2	9627.64	6916.263	2	0	2	5	5	0
Vampire	0	2	13247.46	6917.907	2	0	2	5	5	0
UltimateEliminator+MathSAT	0	0	34.306	21.166	0	0	0	7	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
z3n	0	4	1431.242	1431.274	4	4	0	1	2	1	0
2020-z3n	0	4	1801.732	1801.927	4	4	0	1	2	1	0
2018-Z3n	0	3	3655.161	3655.379	3	3	0	2	2	2	0
UltimateEliminator+MathSAT	0	0	24.232	15.307	0	0	0	5	2	0	0
veriT	0	0	4800.32	4800.319	0	0	0	5	2	4	0
SMTInterpol	0	0	4800.602	4800.402	0	0	0	5	2	4	0
iProver	0	0	4800.517	4800.765	0	0	0	5	2	4	0
Vampire	0	0	9600.13	5998.2	0	0	0	5	2	5	0
2020-Vampiren	0	0	6000.0	6000.0	0	0	0	5	2	5	0
2020-CVC4n	0	0	6000.0	6000.0	0	0	0	5	2	5	0
cvc5	0	0	6000.0	6000.0	0	0	0	5	2	5	0
Vampire - fixedn	0	0	6000.0	6000.0	0	0	0	5	2	5	0
cvc5 - fixedn	0	0	6000.0	6000.0	0	0	0	5	2	5	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
veriT	0	2	0.024	0.023	2	0	2	0	5	4	0
2020-CVC4n	0	2	0.034	0.033	2	0	2	0	5	5	0
z3n	0	2	0.033	0.033	2	0	2	0	5	1	0
cvc5 - fixedn	0	2	0.039	0.038	2	0	2	0	5	5	0
cvc5	0	2	0.039	0.038	2	0	2	0	5	5	0
2020-z3n	0	2	0.065	0.065	2	0	2	0	5	1	0
2018-Z3n	0	2	0.073	0.073	2	0	2	0	5	2	0
SMTInterpol	0	2	1.191	0.797	2	0	2	0	5	4	0
2020-Vampiren	0	2	6.15	2.508	2	0	2	0	5	5	0
iProver	0	2	82.63	21.559	2	0	2	0	5	4	0
Vampire - fixedn	0	2	3627.64	916.263	2	0	2	0	5	5	0
Vampire	0	2	3647.33	919.707	2	0	2	0	5	5	0
UltimateEliminator+MathSAT	0	0	10.074	5.859	0	0	0	2	5	0	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
z3n	0	3	106.875	106.876	3	1	2	4	4	0
2020-z3n	0	3	112.035	112.036	3	1	2	4	4	0
2018-Z3n	0	3	112.75	112.752	3	1	2	4	4	0
veriT	0	2	96.344	96.343	2	0	2	5	4	0
SMTInterpol	0	2	97.792	97.199	2	0	2	5	4	0
iProver	0	2	179.147	118.324	2	0	2	5	4	0
2020-CVC4n	0	2	120.034	120.033	2	0	2	5	5	0
cvc5 - fixedn	0	2	120.039	120.038	2	0	2	5	5	0
cvc5	0	2	120.039	120.038	2	0	2	5	5	0
2020-Vampiren	0	2	126.15	122.508	2	0	2	5	5	0
UltimateEliminator+MathSAT	0	0	34.306	21.166	0	0	0	7	0	0
Vampire	0	0	168.0	168.0	0	0	0	7	7	0
Vampire - fixedn	0	0	168.0	168.0	0	0	0	7	7	0

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