Arith (Single Query Track)

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

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

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

Logics:

• LIA : 300 benchmarks
• LRA : 1013 benchmarks
• NIA : 248 benchmarks
• NRA : 99 benchmarks

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24s Performance (parallel)
cvc5	cvc5	YicesQS	cvc5	YicesQS

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
cvc5	0	1441	28855.859	28902.359	1441	549	892	219	0	219	0
2021-z3n	0	1417	39094.828	39065.151	1417	570	847	243	0	153	0
YicesQS	0	1386	3691.088	3691.524	1386	566	820	274	0	274	0
UltimateEliminator+MathSAT	0	1244	29809.362	23518.786	1244	457	787	416	0	287	0
iProver Fixedn	0	404	32637.338	8493.967	404	0	404	1256	0	1245	0
SMTInterpol	0	254	2763.93	1916.867	254	10	244	1059	347	135	0
iProver	22	418	37443.766	9648.036	418	0	418	1242	0	1209	0
Vampire	130	823	64893.67	16450.172	823	0	823	837	0	707	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	1441	28855.859	28902.359	1441	549	892	219	0	219	0
2021-z3n	0	1417	39094.828	39065.151	1417	570	847	243	0	153	0
YicesQS	0	1386	3691.088	3691.524	1386	566	820	274	0	274	0
UltimateEliminator+MathSAT	0	1246	32321.032	25856.516	1246	459	787	414	0	285	0
iProver Fixedn	0	428	79167.808	20264.847	428	0	428	1232	0	1221	0
SMTInterpol	0	254	2763.93	1916.867	254	10	244	1059	347	133	0
iProver	22	447	99991.716	25483.901	447	0	447	1213	0	1180	0
Vampire	130	831	80345.38	20342.616	831	0	831	829	0	699	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
2021-z3n	0	570	5490.037	5471.962	570	570	0	54	1036	153	0
YicesQS	0	566	2207.846	2208.06	566	566	0	58	1036	274	0
cvc5	0	549	9758.465	9774.748	549	549	0	75	1036	219	0
UltimateEliminator+MathSAT	0	459	16498.446	13399.227	459	459	0	165	1036	285	0
SMTInterpol	0	10	5.556	3.869	10	10	0	528	1122	133	0
Vampire	0	0	0.0	0.0	0	0	0	624	1036	699	0
iProver	0	0	0.0	0.0	0	0	0	624	1036	1180	0
iProver Fixedn	0	0	0.0	0.0	0	0	0	624	1036	1221	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
cvc5	0	892	19097.394	19127.611	892	0	892	139	629	219	0
2021-z3n	0	847	33604.792	33593.189	847	0	847	184	629	153	0
YicesQS	0	820	1483.241	1483.464	820	0	820	211	629	274	0
UltimateEliminator+MathSAT	0	787	15822.586	12457.289	787	0	787	244	629	285	0
iProver Fixedn	0	428	79167.808	20264.847	428	0	428	603	629	1221	0
SMTInterpol	0	244	2758.373	1912.997	244	0	244	531	885	133	0
iProver	22	447	99991.716	25483.901	447	0	447	584	629	1180	0
Vampire	130	831	80345.38	20342.616	831	0	831	200	629	699	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
YicesQS	0	1365	289.166	289.377	1365	551	814	295	0	295	0
cvc5	0	1308	480.656	466.174	1308	480	828	352	0	352	0
2021-z3n	0	1284	1389.477	1357.311	1284	542	742	376	0	295	0
UltimateEliminator+MathSAT	0	1155	9753.841	4846.032	1155	418	737	505	0	377	0
iProver Fixedn	0	342	4190.972	1189.951	342	0	342	1318	0	1307	0
SMTInterpol	0	247	992.385	406.564	247	10	237	1066	347	200	0
iProver	16	354	4435.513	1256.546	354	0	354	1306	0	1279	0
Vampire	127	519	2981.029	818.761	519	0	519	1141	0	1014	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.