AUFDTLIRA (Single Query Track)

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

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

Benchmarks: 4185
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	cvc5

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
cvc5	0	3655	639513.22	642667.447	3655	0	3655	530	530	0
2020-CVC4n	0	3628	59072.103	59079.976	3628	0	3628	557	48	0
z3-4.8.17n	0	3622	23264.489	23818.457	3622	0	3622	563	17	0
Vampire	0	3271	1672616.726	1233472.764	3271	0	3271	914	904	0
smtinterpol	0	3263	527305.63	509381.001	3263	0	3263	922	388	0
smtinterpol-fixedn	0	3095	1125809.691	1114498.309	3095	0	3095	1090	906	0
UltimateEliminator+MathSAT	0	0	19378.843	11502.331	0	0	0	4185	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	3655	642594.26	642643.147	3655	0	3655	530	530	0
2020-CVC4n	0	3628	59080.753	59078.046	3628	0	3628	557	48	0
z3-4.8.17n	0	3622	23268.459	23817.747	3622	0	3622	563	17	0
Vampire	0	3421	1947479.816	1137080.171	3421	0	3421	764	754	0
smtinterpol	0	3264	534074.17	507724.095	3264	0	3264	921	383	0
smtinterpol-fixedn	0	3096	1132954.481	1113767.06	3096	0	3096	1089	902	0
UltimateEliminator+MathSAT	0	0	19378.843	11502.331	0	0	0	4185	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
2020-CVC4n	0	0	0.0	0.0	0	0	0	0	4185	48	0
cvc5	0	0	0.0	0.0	0	0	0	0	4185	530	0
smtinterpol	0	0	0.0	0.0	0	0	0	0	4185	383	0
Vampire	0	0	0.0	0.0	0	0	0	0	4185	754	0
UltimateEliminator+MathSAT	0	0	0.0	0.0	0	0	0	0	4185	0	0
z3-4.8.17n	0	0	0.0	0.0	0	0	0	0	4185	17	0
smtinterpol-fixedn	0	0	0.0	0.0	0	0	0	0	4185	902	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	3655	17394.26	17443.147	3655	0	3655	9	521	530	0
2020-CVC4n	0	3628	16907.521	16905.924	3628	0	3628	36	521	48	0
z3-4.8.17n	0	3622	4452.856	4446.761	3622	0	3622	42	521	17	0
Vampire	0	3421	1246663.106	511974.391	3421	0	3421	243	521	754	0
smtinterpol	0	3264	417012.245	396237.509	3264	0	3264	400	521	383	0
smtinterpol-fixedn	0	3096	691979.59	673880.632	3096	0	3096	568	521	902	0
UltimateEliminator+MathSAT	0	0	16981.033	10067.356	0	0	0	3664	521	0	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
2020-CVC4n	0	3626	1629.124	1626.228	3626	0	3626	559	51	0
cvc5	0	3626	14134.749	14133.372	3626	0	3626	559	559	0
z3-4.8.17n	0	3617	1078.031	1074.972	3617	0	3617	568	29	0
smtinterpol	0	3157	33759.422	22037.224	3157	0	3157	1028	594	0
smtinterpol-fixedn	0	3005	38752.494	30370.047	3005	0	3005	1180	1022	0
Vampire	0	2424	54520.859	45467.271	2424	0	2424	1761	1753	0
UltimateEliminator+MathSAT	0	0	19378.843	11502.331	0	0	0	4185	0	0

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