AUFLIA (Single Query Track)

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

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

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

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
cvc5	0	1359	321641.1	328740.383	1359	122	1237	279	252	0
2020-CVC4n	0	1356	319231.277	327895.132	1356	119	1237	282	251	0
Vampire	0	1347	352077.099	344672.045	1347	96	1251	291	285	0
z3-4.8.17n	0	1282	388652.457	389699.833	1282	151	1131	356	288	4
veriT	0	1233	310066.615	310094.486	1233	0	1233	405	251	0
smtinterpol-fixedn	0	1107	567925.677	563701.026	1107	79	1028	531	454	0
smtinterpol	0	1107	567964.851	563761.217	1107	79	1028	531	454	0
UltimateEliminator+MathSAT	0	52	10948.633	6356.314	52	8	44	1586	0	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
cvc5	0	1359	328253.89	328724.813	1359	122	1237	279	252	0
2020-CVC4n	0	1356	327413.857	327883.532	1356	119	1237	282	251	0
Vampire	0	1356	400917.949	337963.323	1356	96	1260	282	276	0
z3-4.8.17n	0	1282	388717.867	389686.213	1282	151	1131	356	288	4
veriT	0	1233	310106.165	310083.856	1233	0	1233	405	251	0
smtinterpol-fixedn	0	1108	581899.587	553134.292	1108	79	1029	530	434	0
smtinterpol	0	1108	580781.411	554330.251	1108	79	1029	530	436	0
UltimateEliminator+MathSAT	0	52	10948.633	6356.314	52	8	44	1586	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	151	5266.917	5267.271	151	151	0	6	1481	288	4
cvc5	0	122	22922.884	23055.054	122	122	0	35	1481	252	0
2020-CVC4n	0	119	22584.217	22618.682	119	119	0	38	1481	251	0
Vampire	0	96	76814.55	73206.062	96	96	0	61	1481	276	0
smtinterpol-fixedn	0	79	30195.877	29965.169	79	79	0	78	1481	434	0
smtinterpol	0	79	30197.741	29973.196	79	79	0	78	1481	436	0
UltimateEliminator+MathSAT	0	8	812.947	465.132	8	8	0	149	1481	0	0
veriT	0	0	35274.009	35273.969	0	0	0	157	1481	251	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
Vampire	0	1260	56502.149	33203.222	1260	0	1260	28	350	276	0
cvc5	0	1237	74449.3	74787.624	1237	0	1237	51	350	252	0
2020-CVC4n	0	1237	74755.24	75189.809	1237	0	1237	51	350	251	0
veriT	0	1233	71147.539	71125.023	1233	0	1233	55	350	251	0
z3-4.8.17n	0	1131	163485.452	164451.16	1131	0	1131	157	350	288	4
smtinterpol	0	1029	335867.553	314217.49	1029	0	1029	259	350	436	0
smtinterpol-fixedn	0	1029	334652.418	314556.052	1029	0	1029	259	350	434	0
UltimateEliminator+MathSAT	0	44	7909.906	4572.575	44	0	44	1244	350	0	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Vampire	0	1327	8456.685	7738.904	1327	96	1231	311	305	0
z3-4.8.17n	0	1262	9428.65	9426.56	1262	150	1112	376	372	4
cvc5	0	1225	9700.553	9705.669	1225	82	1143	413	392	0
veriT	0	1221	7587.657	7573.883	1221	0	1221	417	276	0
2020-CVC4n	0	1217	9870.883	9874.724	1217	81	1136	421	401	0
smtinterpol	0	1030	17021.699	14848.873	1030	79	951	608	542	0
smtinterpol-fixedn	0	1029	17027.768	14838.441	1029	79	950	609	543	0
UltimateEliminator+MathSAT	0	52	9782.486	5619.768	52	8	44	1586	13	0

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