ALIA (Single Query Track)

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

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

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

Winners

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

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	19	0.939	0.904	19	1	18	0	0	0
smtinterpol-fixedn	0	19	111.336	39.934	19	1	18	0	0	0
smtinterpol	0	19	112.217	41.286	19	1	18	0	0	0
2020-CVC4n	0	18	2.901	2.893	18	0	18	1	0	0
cvc5	0	18	5.875	5.868	18	0	18	1	0	0
Vampire	0	12	10224.911	8858.243	12	0	12	7	7	0
veriT	0	4	17998.731	18000.581	4	0	4	15	15	0
UltimateEliminator+MathSAT	0	1	125.655	64.009	1	1	0	18	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	19	0.939	0.904	19	1	18	0	0	0
smtinterpol-fixedn	0	19	111.336	39.934	19	1	18	0	0	0
smtinterpol	0	19	112.217	41.286	19	1	18	0	0	0
2020-CVC4n	0	18	2.901	2.893	18	0	18	1	0	0
cvc5	0	18	5.875	5.868	18	0	18	1	0	0
Vampire	0	13	10948.671	8142.849	13	0	13	6	6	0
veriT	0	4	18000.061	18000.061	4	0	4	15	15	0
UltimateEliminator+MathSAT	0	1	125.655	64.009	1	1	0	18	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	1	0.041	0.039	1	1	0	0	18	0	0
smtinterpol	0	1	0.704	0.439	1	1	0	0	18	0	0
smtinterpol-fixedn	0	1	0.705	0.443	1	1	0	0	18	0	0
UltimateEliminator+MathSAT	0	1	4.914	3.028	1	1	0	0	18	0	0
2020-CVC4n	0	0	0.304	0.3	0	0	0	1	18	0	0
cvc5	0	0	0.92	0.919	0	0	0	1	18	0	0
Vampire	0	0	1200.0	1200.0	0	0	0	1	18	6	0
veriT	0	0	1200.0	1200.0	0	0	0	1	18	15	0

UNSAT 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	18	0.899	0.866	18	0	18	0	1	0	0
2020-CVC4n	0	18	2.597	2.592	18	0	18	0	1	0	0
cvc5	0	18	4.955	4.949	18	0	18	0	1	0	0
smtinterpol-fixedn	0	18	110.631	39.491	18	0	18	0	1	0	0
smtinterpol	0	18	111.513	40.847	18	0	18	0	1	0	0
Vampire	0	13	9748.671	6942.849	13	0	13	5	1	6	0
veriT	0	4	16800.061	16800.061	4	0	4	14	1	15	0
UltimateEliminator+MathSAT	0	0	120.74	60.981	0	0	0	18	1	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	19	0.939	0.904	19	1	18	0	0	0
smtinterpol-fixedn	0	19	111.336	39.934	19	1	18	0	0	0
smtinterpol	0	19	112.217	41.286	19	1	18	0	0	0
2020-CVC4n	0	18	2.901	2.893	18	0	18	1	0	0
cvc5	0	18	5.875	5.868	18	0	18	1	0	0
Vampire	0	9	360.251	271.323	9	0	9	10	10	0
veriT	0	4	360.061	360.061	4	0	4	15	15	0
UltimateEliminator+MathSAT	0	1	125.655	64.009	1	1	0	18	0	0

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