AUFLIRA (Single Query Track)

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

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

Benchmarks: 1683
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	Vampire

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
z3-4.8.17n	0	1567	102642.546	102655.473	1567	11	1556	116	67	2
cvc5	0	1563	146923.889	147757.993	1563	0	1563	120	118	0
2020-CVC4n	0	1561	148589.87	149630.309	1561	0	1561	122	121	0
Vampire	0	1517	186791.544	184566.742	1517	0	1517	166	153	0
veriT	0	1342	406878.579	406913.672	1342	0	1342	341	267	72
smtinterpol	0	1335	277031.036	275146.923	1335	0	1335	348	225	0
smtinterpol-fixedn	0	1305	453144.193	450619.567	1305	0	1305	378	357	0
UltimateEliminator+MathSAT	0	9	8589.804	5036.991	9	0	9	1674	0	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
z3-4.8.17n	0	1567	102652.816	102652.733	1567	11	1556	116	67	2
cvc5	0	1563	147701.789	147752.763	1563	0	1563	120	118	0
2020-CVC4n	0	1561	149565.81	149624.589	1561	0	1561	122	121	0
Vampire	0	1537	223497.814	170386.81	1537	0	1537	146	133	0
veriT	0	1342	406905.239	406903.602	1342	0	1342	341	267	72
smtinterpol	0	1335	288132.986	272213.941	1335	0	1335	348	217	0
smtinterpol-fixedn	0	1306	467152.463	447580.119	1306	0	1306	377	347	0
UltimateEliminator+MathSAT	0	9	8589.804	5036.991	9	0	9	1674	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
z3-4.8.17n	0	11	46926.269	46924.67	11	11	0	39	1633	67	2
UltimateEliminator+MathSAT	0	0	302.753	171.522	0	0	0	50	1633	0	0
smtinterpol	0	0	2960.041	2596.673	0	0	0	50	1633	217	0
smtinterpol-fixedn	0	0	54051.921	53809.694	0	0	0	50	1633	347	0
veriT	0	0	57621.004	57621.006	0	0	0	50	1633	267	72
cvc5	0	0	57728.046	57729.035	0	0	0	50	1633	118	0
2020-CVC4n	0	0	58929.012	58930.275	0	0	0	50	1633	121	0
Vampire	0	0	63600.24	59998.02	0	0	0	50	1633	133	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
cvc5	0	1563	8373.743	8423.728	1563	0	1563	2	118	118	0
2020-CVC4n	0	1561	9036.798	9094.314	1561	0	1561	4	118	121	0
z3-4.8.17n	0	1556	8783.035	8780.916	1556	0	1556	9	118	67	2
Vampire	0	1537	60296.684	28804.7	1537	0	1537	28	118	133	0
veriT	0	1342	267684.235	267682.596	1342	0	1342	223	118	267	72
smtinterpol	0	1335	214744.109	211271.732	1335	0	1335	230	118	217	0
smtinterpol-fixedn	0	1306	333985.947	329478.593	1306	0	1306	259	118	347	0
UltimateEliminator+MathSAT	0	9	7942.745	4665.014	9	0	9	1556	118	0	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
z3-4.8.17n	0	1565	2756.415	2752.05	1565	9	1556	118	108	2
Vampire	0	1505	5143.544	4419.189	1505	0	1505	178	165	0
2020-CVC4n	0	1505	4423.217	4422.846	1505	0	1505	178	178	0
cvc5	0	1504	4464.76	4464.1	1504	0	1504	179	179	0
veriT	0	1342	8241.239	8239.602	1342	0	1342	341	267	72
smtinterpol	0	1324	8606.104	6954.396	1324	0	1324	359	236	0
smtinterpol-fixedn	0	1248	12025.55	11154.819	1248	0	1248	435	429	0
UltimateEliminator+MathSAT	0	9	8589.804	5036.991	9	0	9	1674	0	0

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