Equality+LinearArith (Single Query Track)

Competition results for the Equality+LinearArith division in the Single Query Track.

Page generated on 2023-07-06 16:04:54 +0000

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

Logics:

• ALIA : 1537 benchmarks
• AUFDTLIA : 188 benchmarks
• AUFDTLIRA : 4185 benchmarks
• AUFLIA : 1663 benchmarks
• AUFLIRA : 1683 benchmarks
• UFDTLIA : 278 benchmarks
• UFDTLIRA : 3129 benchmarks
• UFIDL : 20 benchmarks
• UFLIA : 2849 benchmarks
• UFLRA : 7 benchmarks

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	Abstained	Timeout	Memout
2022-cvc5n	0	11592	167275.16	170197.632	11592	795	10797	3947	0	3025	0
cvc5	0	11591	166052.984	170390.391	11591	793	10798	3948	0	3026	0
Vampire	0	10353	767702.669	194346.927	10353	123	10230	5186	0	5186	0
SMTInterpol	0	8719	124231.358	95508.387	8719	600	8119	6820	0	5136	0
iProver	0	8402	364539.02	95904.883	8402	0	8402	7137	0	7018	0
iProver Fixedn	0	8374	355467.17	93920.666	8374	0	8374	7165	0	7045	0
UltimateEliminator+MathSAT	0	73	430.425	237.193	73	19	54	7686	7780	7	2

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
2022-cvc5n	0	11592	167275.16	170197.632	11592	795	10797	3947	0	3025	0
cvc5	0	11591	166052.984	170390.391	11591	793	10798	3948	0	3026	0
SMTInterpol	0	8721	126767.758	97796.257	8721	600	8121	6818	0	5062	0
iProver	0	8646	876088.28	225284.521	8646	0	8646	6893	0	6740	0
iProver Fixedn	0	8630	887946.78	229038.648	8630	0	8630	6909	0	6753	0
UltimateEliminator+MathSAT	0	73	430.425	237.193	73	19	54	7686	7780	7	2
Vampire	17	10544	1227224.389	308826.58	10544	123	10421	4995	0	4978	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
2022-cvc5n	0	795	36797.002	37340.567	795	795	0	96	14648	3025	0
cvc5	0	793	36691.07	38032.019	793	793	0	98	14648	3026	0
SMTInterpol	0	600	511.051	353.514	600	600	0	291	14648	5062	0
Vampire	0	123	2046.715	523.955	123	123	0	768	14648	4978	0
UltimateEliminator+MathSAT	0	19	131.265	70.703	19	19	0	236	15284	7	2
iProver	0	0	0.0	0.0	0	0	0	891	14648	6740	0
iProver Fixedn	0	0	0.0	0.0	0	0	0	891	14648	6753	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
cvc5	0	10798	129361.914	132358.372	10798	0	10798	303	4438	3026	0
2022-cvc5n	0	10797	130478.159	132857.066	10797	0	10797	304	4438	3025	0
iProver	0	8646	876088.28	225284.521	8646	0	8646	2455	4438	6740	0
iProver Fixedn	0	8630	887946.78	229038.648	8630	0	8630	2471	4438	6753	0
SMTInterpol	0	8121	126256.708	97442.743	8121	0	8121	2980	4438	5062	0
UltimateEliminator+MathSAT	0	54	299.161	166.49	54	0	54	4927	10558	7	2
Vampire	17	10421	1225177.674	308302.625	10421	0	10421	680	4438	4978	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
cvc5	0	10886	3787.747	3798.255	10886	687	10199	4653	0	4064	0
2022-cvc5n	0	10880	4859.012	4837.45	10880	693	10187	4659	0	4074	0
Vampire	0	8588	32572.641	9114.687	8588	111	8477	6951	0	6951	0
SMTInterpol	0	8332	29780.355	13367.857	8332	600	7732	7207	0	5616	0
iProver	0	7465	45480.808	14469.932	7465	0	7465	8074	0	7966	0
iProver Fixedn	0	7455	45011.59	14426.127	7455	0	7455	8084	0	7975	0
UltimateEliminator+MathSAT	0	73	430.425	237.193	73	19	54	7686	7780	179	2

n Non-competing.
Abstained: Total of benchmarks in logics in this division that solver chose to abstain from. For SAT/UNSAT scores, this column also includes benchmarks not known to be SAT/UNSAT.