Largest Contribution Ranking - Single Query Track

Page generated on 2021-07-18 17:29:47 +0000

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24 seconds Performance (parallel)
Vampire	iProver	cvc5	cvc5	Vampire

Sequential Performance

Solver	Correct Score	Time Score	Division
Vampire	0.0489982	0.02375393	Equality+NonLinearArith
Vampire	0.01788343	0.01136702	Equality
cvc5	0.01710729	0.07812895	Equality+LinearArith
Yices2	0.00869686	0.02991173	QF_NonLinearIntArith
Yices2-QS	0.00278091	0.01654654	Arith
cvc5	0.00250854	0.01324292	QF_NonLinearRealArith
cvc5	0.00232601	0.0135751	QF_Equality
cvc5	0.00132654	0.00434066	Bitvec
cvc5	0.00098018	0.00052172	QF_Equality+NonLinearArith
cvc5	0.00086324	0.01424898	QF_LinearIntArith
Bitwuzla	0.00057358	0.02655054	QF_Bitvec
cvc5	0.00027728	0.00834592	QF_Equality+LinearArith
Yices2	0.0001749	0.00664358	QF_Equality+Bitvec
OpenSMT	0.00011	0.00217001	QF_LinearRealArith

Parallel Performance

Solver	Correct Score	Time Score	Division
iProver	0.08486995	0.01356117	Equality+NonLinearArith
Vampire	0.01847402	0.01229507	Equality
cvc5	0.01258234	0.05619468	Equality+LinearArith
Yices2	0.00868235	0.029859	QF_NonLinearIntArith
Yices2-QS	0.00269209	0.01649311	Arith
cvc5	0.00250854	0.01323976	QF_NonLinearRealArith
cvc5	0.0022348	0.01339827	QF_Equality
cvc5	0.00132654	0.00433845	Bitvec
cvc5	0.00098018	0.00052301	QF_Equality+NonLinearArith
cvc5	0.00086324	0.01406458	QF_LinearIntArith
Bitwuzla	0.00043296	0.02177732	QF_Bitvec
cvc5	0.00027713	0.00840443	QF_Equality+LinearArith
Yices2	0.0001749	0.00663162	QF_Equality+Bitvec
OpenSMT	0.00011	0.00218101	QF_LinearRealArith

SAT Performance

Solver	Correct Score	Time Score	Division
cvc5	0.10587024	0.00161216	Equality+LinearArith
UltimateEliminator+MathSAT	0.08416589	0.00358447	Equality+NonLinearArith
Vampire	0.02936727	0.00424783	Equality
cvc5	0.00616228	0.00599641	QF_NonLinearIntArith
Yices2-QS	0.00553133	0.00393864	Arith
cvc5	0.00262204	0.00188031	QF_NonLinearRealArith
cvc5	0.00157784	0.00059486	QF_Equality
cvc5	0.00145186	0.0022273	QF_LinearIntArith
cvc5	0.00125507	0.00027314	Bitvec
Bitwuzla	0.00093358	0.00069896	QF_Bitvec
cvc5	0.00093134	-0.00090887	QF_Equality+NonLinearArith
cvc5	0.00055932	-0.00228172	QF_FPArith
cvc5	0.00013178	0.00015434	QF_Equality+LinearArith
Yices2	0.00010454	0.00020464	QF_Equality+Bitvec
Yices2	9.601e-05	0.00035558	QF_LinearRealArith

UNSAT Performance

Solver	Correct Score	Time Score	Division
cvc5	0.05633672	0.03589274	Equality+NonLinearArith
Yices2	0.02120632	0.0072311	QF_NonLinearIntArith
cvc5	0.01061534	0.04760987	Equality+LinearArith
Vampire	0.00682471	0.00269049	Equality
cvc5	0.00270744	0.00174959	QF_Equality
cvc5	0.00236879	0.00189844	QF_NonLinearRealArith
cvc5	0.0013437	0.00203283	Bitvec
cvc5	0.00110459	-0.00108139	QF_Equality+NonLinearArith
Vampire	0.00102021	0.00113177	Arith
Yices2	0.00050192	0.00101881	QF_Bitvec
cvc5	0.00044916	0.00028312	QF_Equality+LinearArith
SMTInterpol	0.00034388	0.00027464	QF_LinearIntArith
Bitwuzla	0.00033382	0.00019843	QF_Equality+Bitvec
OpenSMT	0.00016838	0.00019975	QF_LinearRealArith

24s Performance

Solver	Correct Score	Time Score	Division
Vampire	0.03693418	0.01182153	Equality+NonLinearArith
cvc5	0.03523494	0.09052442	Equality+LinearArith
Vampire	0.02659309	0.01222879	Equality
Yices2	0.01948202	0.0497127	QF_LinearIntArith
Yices2	0.01905708	0.03544587	QF_NonLinearIntArith
Yices2-QS	0.00391344	0.01661497	Arith
cvc5	0.00244993	0.00977862	QF_NonLinearRealArith
Yices2	0.00213838	0.02694615	QF_Bitvec
cvc5	0.00116871	0.00349565	Bitvec
cvc5	0.00094534	-0.00054065	QF_Equality+NonLinearArith
Yices2	0.0009399	0.00313739	QF_LinearRealArith
Bitwuzla	0.00046524	0.0066385	QF_Equality+Bitvec
Yices2	0.0004051	0.0075656	QF_Equality+LinearArith
veriT	6.377e-05	0.000601	QF_Equality

n Non-competing.
e Experimental.