LRA (Single Query Track)

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

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

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

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24s Performance (parallel)
YicesQS	YicesQS	YicesQS	YicesQS	YicesQS

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
YicesQS	0	1003	578.813	578.947	1003	397	606	10	10	0
2021-z3n	0	940	38384.3	38354.581	940	369	571	73	73	0
UltimateEliminator+MathSAT	0	848	17996.592	13874.916	848	325	523	165	165	0
cvc5	0	831	22819.9	22842.751	831	332	499	182	182	0
Vampire	0	496	52306.649	13246.63	496	0	496	517	517	0
iProver Fixedn	0	180	29224.947	7492.786	180	0	180	833	833	0
iProver	0	177	28871.506	7397.68	177	0	177	836	836	0
SMTInterpol	0	156	2628.842	1825.615	156	2	154	857	37	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
YicesQS	0	1003	578.813	578.947	1003	397	606	10	10	0
2021-z3n	0	940	38384.3	38354.581	940	369	571	73	73	0
UltimateEliminator+MathSAT	0	848	17996.592	13874.916	848	325	523	165	165	0
cvc5	0	831	22819.9	22842.751	831	332	499	182	182	0
Vampire	0	497	53516.369	13551.383	497	0	497	516	516	0
iProver	0	204	84401.356	21459.131	204	0	204	809	809	0
iProver Fixedn	0	201	68856.737	17515.819	201	0	201	812	812	0
SMTInterpol	0	156	2628.842	1825.615	156	2	154	857	35	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
YicesQS	0	397	435.982	436.059	397	397	0	4	612	10	0
2021-z3n	0	369	5477.915	5459.825	369	369	0	32	612	73	0
cvc5	0	332	6082.338	6085.623	332	332	0	69	612	182	0
UltimateEliminator+MathSAT	0	325	5213.28	3600.532	325	325	0	76	612	165	0
SMTInterpol	0	2	1.181	0.807	2	2	0	399	612	35	0
Vampire	0	0	0.0	0.0	0	0	0	401	612	516	0
iProver	0	0	0.0	0.0	0	0	0	401	612	809	0
iProver Fixedn	0	0	0.0	0.0	0	0	0	401	612	812	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
YicesQS	0	606	142.831	142.888	606	0	606	6	401	10	0
2021-z3n	0	571	32906.385	32894.756	571	0	571	41	401	73	0
UltimateEliminator+MathSAT	0	523	12783.311	10274.383	523	0	523	89	401	165	0
cvc5	0	499	16737.561	16757.128	499	0	499	113	401	182	0
Vampire	0	497	53516.369	13551.383	497	0	497	115	401	516	0
iProver	0	204	84401.356	21459.131	204	0	204	408	401	809	0
iProver Fixedn	0	201	68856.737	17515.819	201	0	201	411	401	812	0
SMTInterpol	0	154	2627.66	1824.809	154	0	154	458	401	35	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
YicesQS	0	999	125.678	125.725	999	394	605	14	14	0
2021-z3n	0	810	1336.612	1304.407	810	341	469	203	203	0
UltimateEliminator+MathSAT	0	793	6590.134	3243.073	793	310	483	220	220	0
cvc5	0	719	355.613	341.296	719	277	442	294	294	0
Vampire	0	234	2164.808	584.365	234	0	234	779	779	0
SMTInterpol	0	149	857.297	315.313	149	2	147	864	68	0
iProver	0	125	2894.169	786.698	125	0	125	888	888	0
iProver Fixedn	0	125	2982.45	800.154	125	0	125	888	888	0

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