Equality+NonLinearArith (Single Query Track)

Competition results for the Equality+NonLinearArith division in the Single Query Track.

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

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

Logics:

• AUFDTNIRA : 762 benchmarks
• AUFNIA : 3 benchmarks
• AUFNIRA : 300 benchmarks
• UFDTNIA : 1 benchmarks
• UFDTNIRA : 2149 benchmarks
• UFNIA : 6278 benchmarks

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	Abstained	Timeout	Memout
cvc5	0	6135	3919824.849	4011759.133	6135	694	5441	3358	0	3227	0
2020-CVC4n	0	6055	3723112.023	3833254.7	6055	692	5363	3438	0	3064	0
z3-4.8.17n	0	5327	3477095.862	3482229.099	5327	627	4700	4166	0	2486	15
Vampire	0	4804	6146543.518	5711815.808	4804	0	4804	4689	0	4635	2
UltimateEliminator+MathSAT	0	568	649256.294	630232.179	568	397	171	8925	0	483	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
cvc5	0	6136	4009250.846	4011556.093	6136	694	5442	3357	0	3226	0
2020-CVC4n	0	6055	3827621.759	3833071.71	6055	692	5363	3438	0	3064	0
z3-4.8.17n	0	5327	3478506.492	3482130.419	5327	627	4700	4166	0	2486	15
Vampire	0	5124	7107011.638	5492638.325	5124	0	5124	4369	0	4310	2
UltimateEliminator+MathSAT	0	568	649288.534	630177.039	568	397	171	8925	0	480	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
cvc5	0	694	59103.696	59205.118	694	694	0	46	8753	3226	0
2020-CVC4n	0	692	47700.64	48095.224	692	692	0	48	8753	3064	0
z3-4.8.17n	0	627	102098.653	102088.04	627	627	0	113	8753	2486	15
UltimateEliminator+MathSAT	0	397	328504.159	327522.334	397	397	0	343	8753	480	0
Vampire	0	0	992404.87	887899.43	0	0	0	740	8753	4310	2

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
cvc5	0	5442	586128.77	588333.528	5442	0	5442	418	3633	3226	0
2020-CVC4n	0	5363	688713.053	693696.329	5363	0	5363	497	3633	3064	0
Vampire	0	5124	2224514.168	1134378.357	5124	0	5124	736	3633	4310	2
z3-4.8.17n	0	4700	874481.81	874462.811	4700	0	4700	1160	3633	2486	15
UltimateEliminator+MathSAT	0	171	194602.027	181883.204	171	0	171	5689	3633	480	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
cvc5	0	5396	99417.414	99378.229	5396	625	4771	4097	0	3973	0
2020-CVC4n	0	5368	95000.557	94980.117	5368	601	4767	4125	0	3827	0
z3-4.8.17n	0	5162	99359.605	99251.1	5162	605	4557	4331	0	3878	15
Vampire	0	3429	160477.643	149260.373	3429	0	3429	6064	0	6034	2
UltimateEliminator+MathSAT	0	534	58824.463	40920.702	534	364	170	8959	0	576	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.