UFDTLIRA (Single Query Track)

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

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

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

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	2753	448351.999	448417.595	2753	582	2171	376	370	1
cvc5	0	2713	220709.299	222142.61	2713	540	2173	416	177	0
smtinterpol	0	2600	171815.893	167021.709	2600	498	2102	529	130	0
2020-CVC4n	0	2234	8567.048	8569.313	2234	64	2170	895	7	0
Vampire	0	2113	1283066.913	1219355.653	2113	12	2101	1016	998	0
UltimateEliminator+MathSAT	0	0	14606.022	8720.16	0	0	0	3129	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	2753	448406.639	448401.775	2753	582	2171	376	370	1
cvc5	0	2713	222048.999	222134.13	2713	540	2173	416	177	0
smtinterpol	0	2600	174647.043	163961.084	2600	498	2102	529	125	0
2020-CVC4n	0	2234	8569.458	8569.093	2234	64	2170	895	7	0
Vampire	0	2129	1497464.303	1209820.175	2129	12	2117	1000	982	0
UltimateEliminator+MathSAT	0	0	14606.022	8720.16	0	0	0	3129	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	582	490.51	489.499	582	582	0	0	2547	370	1
cvc5	0	540	10268.99	10278.09	540	540	0	42	2547	177	0
smtinterpol	0	498	595.591	326.258	498	498	0	84	2547	125	0
2020-CVC4n	0	64	12.907	12.865	64	64	0	518	2547	7	0
Vampire	0	12	783874.2	684563.097	12	12	0	570	2547	982	0
UltimateEliminator+MathSAT	0	0	2713.697	1623.662	0	0	0	582	2547	0	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	2173	2926.014	2981.089	2173	0	2173	1	955	177	0
z3-4.8.17n	0	2171	3741.143	3737.045	2171	0	2171	3	955	370	1
2020-CVC4n	0	2170	4933.375	4933.08	2170	0	2170	4	955	7	0
Vampire	0	2117	183185.453	77734.518	2117	0	2117	57	955	982	0
smtinterpol	0	2102	100590.81	90712.152	2102	0	2102	72	955	125	0
UltimateEliminator+MathSAT	0	0	10146.411	6057.741	0	0	0	2174	955	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	2748	9300.445	9295.256	2748	577	2171	381	379	1
cvc5	0	2701	6702.639	6706.841	2701	534	2167	428	242	0
smtinterpol	0	2563	10524.805	6916.821	2563	498	2065	566	170	0
2020-CVC4n	0	2234	337.458	337.093	2234	64	2170	895	7	0
Vampire	0	1884	35367.806	31137.885	1884	0	1884	1245	1228	0
UltimateEliminator+MathSAT	0	0	14606.022	8720.16	0	0	0	3129	0	0

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