QBF Solver Evaluation Portal
Home
QBFLIB
QBFGALLERY'23
QBFEVALs
2022
2020
2019
2018
2017
2016
2010
2008
2007
2006
2005
2004
QBF GALLERIES
QBF Gallery 2014
QBF Gallery 2013
DOWNLOADS
Download the QBFEVAL'22 dataset
Download the QBFEVAL'20 dataset
Download the QBFEVAL'19 dataset and raw results
Download the QBFEVAL'18 dataset and raw results
Download the QBFEVAL'17 dataset and raw results
Download the QBFEVAL'16 dataset
Download the QBFEVAL'10 dataset
Download the QBFEVAL'08 dataset
Download the non-prenex non-cnf track dataset
Download the QBFEVAL'07 dataset
Download the QBFEVAL'06 dataset
Download the QDIMACS to QPRO converter
Download the QDIMACS to QBF1.0 converter
qbflib.org
Instances solved by
Qute_default
Prenex non-CNF Track
Instance
Result
Time
trivial_query71_1344
SAT
0
k0325715.c.oe
FAIL
0
k0325624.v.oe
FAIL
0
k0325624.s.oe
FAIL
0
k0325624.connected.oe
FAIL
0
k0325261.s.oe
FAIL
0
k0325261.h.oe
FAIL
0
k0325261.connected.oe
FAIL
0
k0302060.s.oe
FAIL
0
k0302060.h.oe
FAIL
0
k0325715.connected.oe
FAIL
0
k0325715.s.oe
FAIL
0
trueque_query64_1344
SAT
0
trueque_query71_1344
SAT
0
axquery_query42_1133
SAT
0
k0327694.v.oe
FAIL
0
k0327620.h.oe
FAIL
0
k0327178.connected.oe
FAIL
0
k0327178.c.oe
FAIL
0
k0326578.connected.oe
FAIL
0
k0326191.connected.oe
FAIL
0
k0302060.connected.oe
FAIL
0
k0300663.v.oe
FAIL
0
k0300663.s.oe
FAIL
0
k0206272.s.oe
FAIL
0
k0206272.h.oe
FAIL
0
k0206272.c.oe
FAIL
0
k0201058.v.oe
FAIL
0
k0201058.h.oe
FAIL
0
k0201058.connected.oe
FAIL
0
k0026150.h.oe
FAIL
0
k0026150.c.oe
FAIL
0
SR-unsat-02-01-06-1
UNSAT
0
k0206272.v.oe
FAIL
0
k0225418.connected.oe
FAIL
0
k0300663.c.oe
FAIL
0
k0248814.v.oe
FAIL
0
k0248814.h.oe
FAIL
0
k0248814.c.oe
FAIL
0
k0226271.s.oe
FAIL
0
k0226271.connected.oe
FAIL
0
k0225744.s.oe
FAIL
0
k0225682.v.oe
FAIL
0
k0225418.v.oe
FAIL
0
klieber2017q-104-26-t1
UNSAT
0
trivial_query64_1344
SAT
0
ci.e#1.a#3.E#40.A#60.c#200.w#6.s#6.asp
SAT
0
query64_query11_1133
UNSAT
0
nxquery_query71_1133
UNSAT
0
nxquery_query64_1133
SAT
0
nxquery_query50_1133
UNSAT
0
nxquery_query42_1133
SAT
0
ntrivil_query71_1133
SAT
0
ntrivil_query64_1133
SAT
0
ntrivil_query42_1133
SAT
0
nreachq_query71_1133
UNSAT
0
query64_query42_1133
UNSAT
0
query71_query31_1133
UNSAT
0
ci.e#1.a#3.E#40.A#60.c#208.w#6.s#8.asp
SAT
0
trueque_query71_1133
SAT
0
trueque_query64_1133
SAT
0
trueque_query60_1133
SAT
0
trivial_query71_1133
SAT
0
trivial_query64_1133
SAT
0
trivial_query60_1133
SAT
0
query71_query36_1133
UNSAT
0
query71_query34_1133
UNSAT
0
nreachq_query54_1133
UNSAT
0
nreachq_query11_1133
UNSAT
0
falsequ_query64_1344
SAT
0
falsequ_query71_1344
SAT
0
eequery_query42_1133
UNSAT
0
ntrivil_query64_1344
SAT
0
ntrivil_query71_1344
SAT
0
nxquery_query71_1344
SAT
0
falsequ_query64_1133
SAT
0
axquery_query71_1133
UNSAT
0
axquery_query64_1133
SAT
0
eequery_query64_1133
UNSAT
0
eequery_query71_1133
SAT
0
falsequ_query71_1133
SAT
0
exquery_query42_1133
UNSAT
0
axquery_query71_1344
SAT
0
falsequ_query60_1133
SAT
0
exquery_query64_1133
SAT
0
exquery_query71_1133
SAT
0
k0201058.c.oe
FAIL
0.01
klieber2017q-048-12-t1
UNSAT
0.64
SR-sat-02-01-07-2
SAT
0.91
jctc13-fail
UNSAT
0.91
axquery_query64_1344
SAT
0.92
ci.e#1.a#3.E#40.A#60.c#424.w#2.s#1.asp
UNSAT
1.38
ci.e#1.a#3.E#40.A#60.c#416.w#2.s#3.asp
UNSAT
1.97
jctc8-pass
SAT
2.18
jctc4-fail
UNSAT
2.9
JP-sat-02-08-3
SAT
3.78
DW-sat-04-16-1
SAT
4.58
exquery_query71_1344
SAT
5.07
bs128n.sat
SAT
5.29
bs128y.sat
SAT
5.63
reachqu_query64_1133
SAT
5.69
SR-unsat-03-01-07-1
UNSAT
5.74
jctc9-pass
SAT
6.19
ci.e#1.a#3.E#40.A#60.c#432.w#2.s#8.asp
UNSAT
7.68
CM-sat-04-01-07-3
SAT
8.82
CM-sat-04-01-06-4
SAT
10.13
reachqu_query60_1133
SAT
11.87
JP-sat-02-07-4
SAT
17.36
klieber2017q-048-12-eq
SAT
19.61
SR-sat-02-01-06-3
SAT
20.45
SR-sat-02-01-06-2
SAT
26.29
klieber2017q-060-15-t1
UNSAT
26.87
jctc2-pass
SAT
27.5
klieber2017q-086-21-t1
UNSAT
28.56
ci.e#1.a#3.E#40.A#60.c#400.w#2.s#1.asp
UNSAT
29.93
klieber2017q-062-15-t1
UNSAT
30.21
SR-unsat-02-01-05-2
UNSAT
31.71
JP-unsat-02-07-2
UNSAT
41.52
stay24n.sat
SAT
42.96
chess_solving_mate_in_2_2009_BEL-CH-17B_01
SAT
56.8
chess_solving_mate_in_2_1983_FIN-CH-4_01
SAT
62.14
exquery_query64_1344
SAT
74.42
klieber2017q-052-13-eq
SAT
84.05
klieber2017q-072-18-t1
UNSAT
89.36
ci.e#1.a#3.E#40.A#60.c#400.w#2.s#4.asp
UNSAT
92.92
klieber2017q-066-16-t1
UNSAT
155.69
chess_solving_mate_in_2_2009_POL-CH-33_01
SAT
189.35
chess_solving_mate_in_2_2002_WCCC-OPEN-45_01
SAT
221.34
klieber2017q-056-14-eq
SAT
306.04
klieber2017q-082-20-t1
UNSAT
371.28
chess_solving_mate_in_2_2014_NED-CH-20B_09
SAT
389.26
chess_solving_mate_in_2_2015_GBR-CH-36_02
SAT
391.93
klieber2017q-084-21-t1
UNSAT
438.97
chess_solving_mate_in_2_2011_ISC-7B_01
SAT
461.18
klieber2017q-088-22-t1
UNSAT
488.25
chess_solving_mate_in_2_2005_POLTAVA-OPEN_01
SAT
507.94
chess_solving_mate_in_2_2002_MAC-CH-6_03
SAT
536.02
chess_solving_mate_in_2_1998_GBR-CH-19_01
SAT
567.09
chess_solving_mate_in_2_2008_BEL-CH-16B_08
SAT
584.81
add20y.sat
SAT
636.38
chess_solving_mate_in_2_2011_GBR-CH-32_03
SAT
656.01
ci.e#1.a#3.E#40.A#60.c#264.w#4.s#2.asp
SAT
735.73
klieber2017q-066-16-eq
SAT
768.88
chess_solving_mate_in_2_2011_WCCC-OPEN-54_01
SAT
770.21
klieber2017q-062-15-eq
SAT
776.47
chess_solving_mate_in_2_1987_FIN-CH-8_01
SAT
781.1
klieber2017q-076-19-t1
UNSAT
807.68
cycle_sched_2_10_1.sat
FAIL
900
cycle_sched_4_4_2.sat
FAIL
900
cycle_sched_6_6_2.sat
FAIL
900
cycle_sched_12_2_1.sat
FAIL
900
JP-sat-03-09-6
FAIL
900
ltl2dba_C2-6_comp3_REAL.sat
FAIL
900
ltl2dpa_C26_comp2_REAL.sat
FAIL
900
mult_bool_matrix_10_9_11.sat
FAIL
900
mult_bool_matrix_10_9_11.unsat
FAIL
900
mult_bool_matrix_17_17_17.sat
FAIL
900
JP-sat-03-10-5
FAIL
900
amba2c7n.sat
FAIL
900
amba3b5y.sat
FAIL
900
JP-unsat-03-08-3
FAIL
900
driver_a10y.sat
FAIL
900
mult_bool_matrix_18_18_18.sat
FAIL
900
mult_bool_matrix_dyn_9_5.sat
FAIL
900
reachqu_query60_1344
FAIL
900
klieber2017q-078-19-eq
FAIL
900
klieber2017q-074-18-eq
FAIL
900
klieber2017q-076-19-eq
FAIL
900
SR-sat-03-01-07-2
FAIL
900
SR-sat-04-01-08-3
FAIL
900
SR-unsat-03-01-06-2
FAIL
900
mult_bool_matrix_12_13_11.sat
FAIL
900
ltl2dba_C2-8_comp4_REAL.sat
FAIL
900
JP-unsat-03-08-5
FAIL
900
driver_b8n.sat
FAIL
900
klieber2017q-074-18-t1
FAIL
900
mult9.sat
FAIL
900
driver_c9n.sat
FAIL
900
driver_c9y.sat
FAIL
900
JP-unsat-03-09-4
FAIL
900
beemskbn1f1_c0to7.sat
FAIL
900
load_2c_comp_comp7_REAL.sat
FAIL
900
SR-sat-04-01-09-2
FAIL
900
genbuf9b4n.unsat
FAIL
900
ci.e#1.a#3.E#40.A#60.c#304.w#4.s#7.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#304.w#6.s#8.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#312.w#2.s#3.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#312.w#4.s#3.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#320.w#4.s#8.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#336.w#4.s#5.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#344.w#4.s#5.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#360.w#2.s#8.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#368.w#2.s#7.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#368.w#6.s#7.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#296.w#6.s#7.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#296.w#4.s#7.asp
FAIL
900
klieber2017q-068-17-eq
FAIL
900
klieber2017q-072-18-eq
FAIL
900
klieber2017q-064-16-t1
FAIL
900
klieber2017q-064-16-eq
FAIL
900
klieber2017q-070-17-t1
FAIL
900
klieber2017q-060-15-eq
FAIL
900
klieber2017q-070-17-eq
FAIL
900
klieber2017q-068-17-t1
FAIL
900
ci.e#1.a#3.E#40.A#60.c#280.w#6.s#7.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#288.w#4.s#8.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#376.w#2.s#4.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#376.w#4.s#6.asp
FAIL
900
amba2f9n.sat
FAIL
900
amba4b9y.unsat
FAIL
900
cycle_sched_4_7_1.sat
FAIL
900
cycle_sched_4_7_1.unsat
FAIL
900
cycle_sched_6_7_1.sat
FAIL
900
driver_a9n.sat
FAIL
900
driver_d9y.sat
FAIL
900
genbuf10b4n.unsat
FAIL
900
beemldelec4b1_c0to127.sat
FAIL
900
load_3c_comp_comp7_REAL.unsat
FAIL
900
reachqu_query71_1344
FAIL
900
reachqu_query64_1344
FAIL
900
ci.e#1.a#3.E#40.A#60.c#376.w#6.s#6.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#376.w#6.s#7.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#384.w#6.s#3.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#384.w#6.s#8.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#392.w#6.s#4.asp
FAIL
900
chess_solving_mate_in_3_2012_NED-CH-18B_04
FAIL
900
ci.e#1.a#3.E#40.A#60.c#400.w#4.s#5.asp
FAIL
900
eequery_query42_1344
FAIL
900
eequery_query64_1344
FAIL
900
nreachq_query71_1344
FAIL
900
load_full_4_comp3_REAL.unsat
FAIL
900
JP-sat-03-08-4
FAIL
900
chess_solving_mate_in_3_2012_GRE-CH-11_02
FAIL
900
chess_solving_mate_in_2_1982_WCSC-6_02
FAIL
900
chess_composing_8_template_43
FAIL
900
chess_composing_8_template_42
FAIL
900
chess_composing_8_template_38
FAIL
900
chess_composing_8_template_13
FAIL
900
chess_composing_8_template_02
FAIL
900
chess_composing_6_template_06
FAIL
900
chess_composing_6_template_04
FAIL
900
chess_composing_6_template_01
FAIL
900
SR-unsat-04-01-08-1
FAIL
900
SR-unsat-04-01-07-2
FAIL
900
chess_solving_mate_in_2_1991_GER-CH-15_01
FAIL
900
chess_solving_mate_in_2_1996_FIN-CH-17_03
FAIL
900
chess_solving_mate_in_3_2011_UKR-OPEN-25_04
FAIL
900
chess_solving_mate_in_3_2010_UKR-CH_04
FAIL
900
chess_solving_mate_in_3_2008_ISC-4B_07
FAIL
900
chess_solving_mate_in_3_2003_UKR-CH_04
FAIL
900
chess_solving_mate_in_3_2001_UKR-CH_06
FAIL
900
chess_solving_mate_in_3_2000_CZE-CH_04
FAIL
900
chess_solving_mate_in_3_1991_WCSC-15_05
FAIL
900
chess_solving_mate_in_3_1978_WCSC-2_05
FAIL
900
chess_solving_mate_in_2_2012_GER-CH-36-19_03
FAIL
900
chess_solving_mate_in_2_2011_ROM-CH-W_02
FAIL
900
chess_solving_mate_in_2_1997_WCCC-OPEN-40_03
FAIL
900
SR-sat-04-01-08-2
FAIL
900
SR-sat-03-01-08-2
FAIL
900
SR-sat-03-01-07-3
FAIL
900
DW-sat-08-23-1
FAIL
900
DW-sat-08-22-1
FAIL
900
CM-unsat-18-01-05-3
FAIL
900
CM-unsat-17-01-05-3
FAIL
900
CM-unsat-07-01-06-2
FAIL
900
CM-sat-07-01-07-3
FAIL
900
CM-sat-07-01-06-4
FAIL
900
CM-sat-07-01-06-3
FAIL
900
klieber2017q-112-28-t1
FAIL
900
klieber2017q-108-27-t1
FAIL
900
klieber2017q-088-22-eq
FAIL
900
DW-sat-19-44-1
FAIL
900
DWs-sat-10-23-1
FAIL
900
JP-unsat-03-07-4
FAIL
900
JP-unsat-02-06-3
FAIL
900
JP-sat-03-09-5
FAIL
900
JP-sat-03-09-4
FAIL
900
JP-sat-03-08-5
FAIL
900
DW-unsat-20-44-1
FAIL
900
DW-unsat-09-23-1
FAIL
900
DW-unsat-09-22-1
FAIL
900
DWs-unsat-11-24-1
FAIL
900
DWs-unsat-11-23-1
FAIL
900
DWs-sat-10-25-1
FAIL
900
klieber2017q-100-25-t1
FAIL
900
chess_solving_mate_in_3_2014_FRA-CH_03
FAIL
900
klieber2017q-078-19-t1
FAIL
900
DWs-unsat-08-18-1
FAIL
900
DWs-unsat-08-17-1
FAIL
900
DWs-sat-25-53-1
FAIL
900
DWs-sat-24-51-1
FAIL
900
DWs-sat-23-49-1
FAIL
900
DWs-sat-22-47-1
FAIL
900
DWs-sat-21-45-1
FAIL
900
DWs-sat-20-43-1
FAIL
900
DWs-sat-19-41-1
FAIL
900
DWs-sat-12-28-1
FAIL
900
DW-sat-22-50-1
FAIL
900
DWs-unsat-09-19-1
FAIL
900
DWs-unsat-10-22-1
FAIL
900
DW-unsat-25-54-1
FAIL
900
DW-unsat-24-52-1
FAIL
900
DW-unsat-23-50-1
FAIL
900
DW-unsat-22-48-1
FAIL
900
DW-unsat-21-46-1
FAIL
900
DW-unsat-11-26-1
FAIL
900
DW-unsat-10-25-1
FAIL
900
DWs-unsat-25-51-1
FAIL
900
DWs-unsat-24-49-1
FAIL
900
DWs-unsat-23-47-1
FAIL
900
DWs-unsat-22-45-1
FAIL
900
DW-sat-21-48-1
FAIL
900
DW-sat-20-46-1
FAIL
900
DW-sat-18-42-1
FAIL
900
CM-sat-18-01-07-3
FAIL
900
CM-sat-04-01-06-3
FAIL
900
jctc6-pass
FAIL
900
jctc5-fail
FAIL
900
klieber2017q-084-21-eq
FAIL
900
jctc18-vals-0,2-pass
FAIL
900
jctc17-vals-0,2-pass
FAIL
900
jctc16-vals-0,2-pass
FAIL
900
jctc14-unrolled-fail
FAIL
900
jctc10-fail
FAIL
900
jctc1-pass
FAIL
900
CM-sat-19-01-06-3
FAIL
900
CM-sat-20-01-06-3
FAIL
900
DW-sat-17-40-1
FAIL
900
DW-sat-09-26-1
FAIL
900
klieber2017q-080-20-t1
FAIL
900
CM-unsat-21-01-05-3
FAIL
900
CM-unsat-20-01-05-3
FAIL
900
CM-unsat-19-01-05-3
FAIL
900
CM-unsat-16-01-05-3
FAIL
900
CM-unsat-15-01-05-3
FAIL
900
CM-unsat-14-01-05-3
FAIL
900
CM-unsat-13-01-05-3
FAIL
900
CM-sat-21-01-06-3
FAIL
900
chess_solving_mate_in_4_2001_UKR-CH_13
FAIL
900
Contact
|
Organization
|
Links
|
Citing QBFLIB