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_opt993
QBFEVAL'18 - Prenex non-CNF Track
Instance
Result
Time
query21_reachqu_1133
SAT
0
ntrivil_query54_1133
SAT
0
query04_query03_1133
UNSAT
0
k_ph_n-21
SAT
0
query30_eequery_1133
SAT
0
query44_query57_1133
UNSAT
0
query50_query49_1133
UNSAT
0
query51_query48_1133
UNSAT
0
query64_query31_1133
UNSAT
0
pg-hkb-2
UNSAT
0
stay22n.unsat
UNSAT
0
bs128n.unsat
UNSAT
0
CM-sat-02-01-07-3
SAT
0
pg-hkb-3
UNSAT
0
query09_trivial_1344
SAT
0
query08_query26_1344
SAT
0
query03_query57_1344
SAT
0
SR-unsat-02-01-06-1
UNSAT
0
driver_d9n.unsat
UNSAT
0
query71_query15_1133
UNSAT
0
6s318r_c0to15.unsat
UNSAT
0.17
pg-hkb-4
UNSAT
0.82
stay24n.sat
SAT
0.84
jctc13-fail
UNSAT
1.14
klieber2017q-092-23-t1
UNSAT
1.21
beemldelec4b1_c0to15.unsat
UNSAT
1.37
dungeon_i15-m7-u4-v0.pddl_planlen=81
UNSAT
1.52
JP-sat-02-08-3
SAT
1.83
query49_query64_1133
UNSAT
1.92
JP-sat-02-07-3
SAT
2.46
ci.e#1.a#3.E#40.A#60.c#432.w#2.s#8.asp
UNSAT
2.59
jctc6-pass
SAT
2.93
oski3ub1i_c0to63.unsat
UNSAT
3.13
ci.e#1.a#3.E#40.A#60.c#424.w#2.s#1.asp
UNSAT
3.58
ev-pr-4x4-13-3-0-0-1-lg
SAT
3.59
ev-pr-4x4-11-3-0-0-1-lg
SAT
3.6
jctc4-fail
UNSAT
3.7
CM-sat-03-01-07-3
SAT
4
ci.e#1.a#3.E#40.A#60.c#400.w#2.s#1.asp
UNSAT
6
bs128n.sat
SAT
7.11
SR-unsat-02-01-05-2
UNSAT
8.81
SR-sat-02-01-07-2
SAT
11.37
k0201058.c.oe
SAT
12.35
pg-hkb-5
UNSAT
12.6
CM-sat-04-01-07-3
SAT
12.94
random-qcir-1000-50-940
UNSAT
12.96
chess_solving_mate_in_2_1983_FIN-CH-4_01
SAT
13.41
k_branch_p-11
UNSAT
14.41
chess_solving_mate_in_2_2012_GER-CH-36-19_03
SAT
15.79
random-qcir-1000-50-545
UNSAT
16.59
jctc9-pass
SAT
17.31
driver_a9y.unsat
UNSAT
18.32
chess_solving_mate_in_2_1996_FIN-CH-17_03
SAT
19.49
random-qcir-1000-50-393
UNSAT
20.28
random-qcir-1000-50-898
UNSAT
24.46
random-qcir-1000-50-98
UNSAT
25.19
jctc8-pass
SAT
26.57
random-qcir-1000-50-983
UNSAT
27.89
random-qcir-1000-50-930
UNSAT
28.15
DWs-unsat-07-16-1
UNSAT
28.27
random-qcir-1000-50-267
UNSAT
29.32
random-qcir-1000-50-275
UNSAT
29.59
klieber2017q-084-21-t1
UNSAT
30.68
random-qcir-1000-50-857
UNSAT
32.28
random-qcir-1000-50-793
UNSAT
33.64
random-qcir-1000-50-970
UNSAT
34.4
chess_solving_mate_in_2_2005_POLTAVA-OPEN_01
SAT
35.31
DW-sat-06-20-1
SAT
35.53
random-qcir-1000-50-68
UNSAT
36.99
random-qcir-1000-50-255
UNSAT
38.11
random-qcir-1000-50-441
UNSAT
38.19
random-qcir-1000-50-743
UNSAT
38.27
klieber2017q-112-28-t1
UNSAT
39
random-qcir-1000-50-295
UNSAT
42.09
CM-sat-07-01-07-3
SAT
42.28
JP-sat-02-07-4
SAT
49.8
random-qcir-1000-50-846
UNSAT
52.19
SR-sat-02-01-06-2
SAT
56.8
random-qcir-1000-50-658
UNSAT
58.4
random-qcir-1000-50-473
UNSAT
58.99
filesys_smbmrx_cvsndrcv.c
UNSAT
59.64
pg-hkb-6
UNSAT
61.18
random-qcir-1000-50-428
UNSAT
62.76
random-qcir-1000-50-754
UNSAT
68.58
DW-unsat-09-22-1
UNSAT
75.4
chess_solving_mate_in_2_2011_ISC-7B_01
SAT
84.78
cnt14
SAT
90.79
k0206272.s.oe
SAT
96.2
random-qcir-1000-50-134
UNSAT
99.9
ci.e#1.a#3.E#40.A#60.c#200.w#6.s#6.asp
SAT
127.14
random-qcir-1000-50-361
UNSAT
141.8
DWs-unsat-09-19-1
UNSAT
189.36
CM-sat-04-01-06-4
SAT
196.74
DWs-unsat-08-17-1
UNSAT
218.18
DW-unsat-11-27-1
UNSAT
249.2
k0026150.h.oe
SAT
249.47
amba2f9n.unsat
UNSAT
262.67
test3_quant_squaring2
UNSAT
268.88
k_branch_p-10
UNSAT
270.79
pg-hkb-7
UNSAT
273.57
DW-unsat-11-26-1
UNSAT
329.56
DW-unsat-10-25-1
UNSAT
330.35
DW-sat-08-22-1
SAT
358.66
ev-pr-8x8-7-7-0-1-2-lg
UNSAT
427.66
DWs-unsat-08-18-1
UNSAT
442.47
CM-sat-04-01-06-3
SAT
450.8
DW-sat-08-23-1
SAT
497.55
jctc2-pass
SAT
505.89
DW-sat-08-24-1
SAT
601.67
amba2f9n.sat
SAT
627.46
jctc1-pass
SAT
630.13
klieber2017q-080-20-t1
UNSAT
665.49
k0206272.h.oe
SAT
799.08
pg-hkb-8
UNSAT
864.32
nreachq_reachqu_2133
FAIL
900
ci.e#1.a#3.E#40.A#60.c#208.w#6.s#8.asp
FAIL
900
klieber2017q-086-21-t1
FAIL
900
jctc18-vals-0,2-pass
FAIL
900
pg-hkb-26
FAIL
900
k0225682.c.oe
FAIL
900
ci.e#1.a#3.E#40.A#60.c#376.w#4.s#6.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#360.w#2.s#8.asp
FAIL
900
pg-hkb-22
FAIL
900
JP-unsat-03-07-4
FAIL
900.01
pg-hkb-13
FAIL
900.01
chess_composing_8_template_02
FAIL
900.01
chess_composing_8_template_38
FAIL
900.01
chess_composing_8_template_42
FAIL
900.01
pg-hkb-15
FAIL
900.01
klieber2017q-076-19-eq
FAIL
900.01
klieber2017q-074-18-t1
FAIL
900.01
pg-hkb-21
FAIL
900.01
jctc5-fail
FAIL
900.01
pg-hkb-14
FAIL
900.01
DWs-unsat-13-28-1
FAIL
900.01
6s318r_c0to31.sat
FAIL
900.01
JP-unsat-03-08-5
FAIL
900.01
ci.e#1.a#3.E#40.A#60.c#368.w#2.s#7.asp
FAIL
900.01
load_3c_comp_comp7_REAL.unsat
FAIL
900.01
query42_query57_1344
FAIL
900.01
CM-unsat-07-01-06-2
FAIL
900.01
mult_bool_matrix_2_3_30.sat
FAIL
900.01
ci.e#1.a#3.E#40.A#60.c#280.w#6.s#7.asp
FAIL
900.01
query64_query55_1344
FAIL
900.01
DWs-sat-10-25-1
FAIL
900.01
ci.e#1.a#3.E#40.A#60.c#400.w#6.s#4.asp
FAIL
900.01
DWs-sat-10-23-1
FAIL
900.01
ci.e#1.a#3.E#40.A#60.c#312.w#4.s#3.asp
FAIL
900.01
mult_bool_matrix_2_3_30.unsat
FAIL
900.02
SR-unsat-03-01-06-2
FAIL
900.02
SR-sat-02-01-06-3
FAIL
900.02
pg-hkb-18
FAIL
900.02
pg-hkb-16
FAIL
900.02
DWs-sat-12-28-1
FAIL
900.02
DW-sat-09-26-1
FAIL
900.02
oski3ub1i_c0to63.sat
FAIL
900.02
jctc11-pass
FAIL
900.02
chess_solving_mate_in_5_1984_FIN-CH-5_09
FAIL
900.02
DWs-unsat-11-24-1
FAIL
900.02
CM-sat-07-01-06-3
FAIL
900.02
chess_composing_8_template_13
FAIL
900.02
klieber2017q-078-19-t1
FAIL
900.02
k_ph_p-12
FAIL
900.02
sdlx-fixpoint-3
FAIL
900.02
k_ph_p-19
FAIL
900.02
random-qcir-1000-50-456
FAIL
900.02
small-swap1-fixpoint-3
FAIL
900.02
DWs-sat-10-24-1
FAIL
900.02
pg-hkb-9
FAIL
900.02
cnt16r
FAIL
900.03
ev-pr-6x6-9-5-0-1-2-lg
FAIL
900.03
klieber2017q-082-20-eq
FAIL
900.03
klieber2017q-112-28-eq
FAIL
900.03
query48_query42_1344
FAIL
900.03
query08_query64_1344
FAIL
900.03
nreachq_query02_1344
FAIL
900.03
ev-pr-6x6-11-5-0-1-2-lg
FAIL
900.03
JP-unsat-03-08-3
FAIL
900.03
k_branch_p-16
FAIL
900.03
ci.e#1.a#3.E#40.A#60.c#304.w#6.s#8.asp
FAIL
900.03
klieber2017q-104-26-t1
FAIL
900.03
ci.e#1.a#3.E#40.A#60.c#312.w#2.s#3.asp
FAIL
900.03
genbuf10b4y.unsat
FAIL
900.03
klieber2017q-108-27-eq
FAIL
900.03
klieber2017q-092-23-eq
FAIL
900.03
JP-unsat-03-09-4
FAIL
900.03
mv16y.sat
FAIL
900.03
k0225418.h.oe
FAIL
900.03
klieber2017q-078-19-eq
FAIL
900.03
k0225418.connected.oe
FAIL
900.03
k0206272.connected.oe
FAIL
900.03
k0225418.s.oe
FAIL
900.03
chess_solving_mate_in_6_1998_OST-CH-1_15
FAIL
900.03
pg-hkb-25
FAIL
900.03
chess_composing_6_template_01
FAIL
900.03
chess_solving_mate_in_7_2005_GER-CH-29-12_15
FAIL
900.03
audio_ddksynth_csynth2.cpp
FAIL
900.03
pipesnotankage14_10
FAIL
900.03
k0206272.v.oe
FAIL
900.03
p20-20.pddl_planlen=23
FAIL
900.03
k0300663.h.oe
FAIL
900.03
SR-sat-03-01-08-2
FAIL
900.03
k_branch_n-12
FAIL
900.04
incrementer-enc08-uniform-depth-33
FAIL
900.04
chess_solving_mate_in_6_2013_WCCC-OPEN-56_10
FAIL
900.04
network_ndis_rtlnwifi_hw_hw_ccmp.c
FAIL
900.04
pg-hkb-20
FAIL
900.04
ken.oop^2.C-d4
FAIL
900.04
pg-hkb-10
FAIL
900.04
nreachq_reachqu_2233
FAIL
900.04
p20-1.pddl_planlen=24
FAIL
900.04
gb_s2_r2_comp3_REAL.unsat
FAIL
900.04
k0225744.h.oe
FAIL
900.04
sortnetsort9.AE.stepl.012
FAIL
900.04
test2_quant_squaring3
FAIL
900.04
klieber2017q-108-27-t1
FAIL
900.04
query44_query58_1344
FAIL
900.04
DWs-unsat-12-25-1
FAIL
900.04
DWs-unsat-11-23-1
FAIL
900.04
chess_solving_mate_in_5_2012_NED-CH-18A_11
FAIL
900.04
ltl2dpa_C26_comp2_REAL.unsat
FAIL
900.04
chess_solving_mate_in_4_1999_GER-CH-23-6_14
FAIL
900.04
jctc7-pass
FAIL
900.04
chess_composing_8_template_43
FAIL
900.04
jctc3-vals-0,2-pass
FAIL
900.04
jctc15-unrolled-fail
FAIL
900.04
JP-sat-03-09-4
FAIL
900.04
chess_solving_mate_in_3_2009_FIN-CH-30_04
FAIL
900.04
chess_solving_mate_in_7_2009_POL-CH-33_15
FAIL
900.04
query42_query64_1344
FAIL
900.05
k0225744.v.oe
FAIL
900.05
chess_solving_mate_in_9_2003_RUS-CH_15
FAIL
900.05
chess_solving_mate_in_7_2011_SVK-CH-19_15
FAIL
900.05
klieber2017q-080-20-eq
FAIL
900.05
pipesnotankage18_8
FAIL
900.05
JP-unsat-02-06-3
FAIL
900.05
klieber2017q-096-24-eq
FAIL
900.05
pg-hkb-24
FAIL
900.05
ci.e#1.a#3.E#40.A#60.c#320.w#4.s#8.asp
FAIL
900.05
ev-pr-4x4-15-3-0-0-1-s
FAIL
900.05
chess_solving_mate_in_4_1984_GBR-CH-5_04
FAIL
900.05
chess_solving_mate_in_3_2009_POLTAVA-OPEN_03
FAIL
900.05
klieber2017q-100-25-t1
FAIL
900.05
ci.e#1.a#3.E#40.A#60.c#384.w#6.s#3.asp
FAIL
900.05
SR-sat-03-01-07-2
FAIL
900.05
load_full_3_comp3_REAL.unsat
FAIL
900.05
klieber2017q-116-29-t1
FAIL
900.05
k_branch_n-10
FAIL
900.05
pg-hkb-19
FAIL
900.06
pg-hkb-17
FAIL
900.06
chess_solving_mate_in_5_1996_UKR-CH-10_15
FAIL
900.06
incrementer-enc07-uniform-depth-25
FAIL
900.06
k0026150.s.oe
FAIL
900.06
chess_composing_6_template_06
FAIL
900.06
k0225418.c.oe
FAIL
900.06
chess_composing_6_template_04
FAIL
900.06
chess_solving_mate_in_7_2016_BEL-CH-23A_03
FAIL
900.06
JP-sat-03-08-4
FAIL
900.06
test1_quant_squaring3
FAIL
900.06
gb_s2_r2_comp3_REAL.sat
FAIL
900.06
load_full_3_comp3_REAL.sat
FAIL
900.06
ltl2dpa_C26_comp3_REAL.sat
FAIL
900.06
sortnetsort9.v.stepl.005
FAIL
900.06
rankfunc17_unsigned_16
FAIL
900.06
k0300663.v.oe
FAIL
900.06
CM-sat-07-01-06-4
FAIL
900.06
ci.e#1.a#3.E#40.A#60.c#288.w#4.s#8.asp
FAIL
900.06
jctc16-vals-0,2-pass
FAIL
900.06
k0225744.s.oe
FAIL
900.06
p20-5.pddl_planlen=32
FAIL
900.06
jctc17-vals-0,2-pass
FAIL
900.06
k0300663.s.oe
FAIL
900.07
klieber2017q-100-25-eq
FAIL
900.07
k0026150.connected.oe
FAIL
900.07
rankfunc13_unsigned_64
FAIL
900.07
sortnetsort10.v.stepl.005
FAIL
900.07
k0026150.v.oe
FAIL
900.07
incrementer-enc02-uniform-depth-58
FAIL
900.07
k0300663.connected.oe
FAIL
900.07
k0225418.v.oe
FAIL
900.07
input_pnpi8042_moudep.c
FAIL
900.07
genbuf9b4n.unsat
FAIL
900.07
mult_bool_matrix_4_5_5.unsat
FAIL
900.07
dungeon_i25-m12-u3-v0.pddl_planlen=190
FAIL
900.07
dungeon_i25-m12-u3-v0.pddl_planlen=165
FAIL
900.07
ci.e#1.a#3.E#40.A#60.c#296.w#6.s#7.asp
FAIL
900.07
jctc10-fail
FAIL
900.07
chess_solving_mate_in_8_2011_BEL-CH-19A_03
FAIL
900.07
query64_query58_1344
FAIL
900.07
network_irda_miniport_nscirda_comm.c
FAIL
900.07
ci.e#1.a#3.E#40.A#60.c#368.w#6.s#7.asp
FAIL
900.07
chess_solving_mate_in_6_2011_SRB-CH_15
FAIL
900.07
ev-pr-6x6-17-5-0-1-2-lg
FAIL
900.07
beemldelec4b1_c0to15.sat
FAIL
900.08
ci.e#1.a#3.E#40.A#60.c#296.w#4.s#7.asp
FAIL
900.08
ci.e#1.a#3.E#40.A#60.c#416.w#2.s#3.asp
FAIL
900.08
ci.e#1.a#3.E#40.A#60.c#376.w#6.s#6.asp
FAIL
900.08
klieber2017q-096-24-t1
FAIL
900.08
qshifter_7
FAIL
900.08
DWs-sat-15-35-1
FAIL
900.08
klieber2017q-086-21-eq
FAIL
900.08
query33_query71_1344
FAIL
900.08
k0226271.c.oe
FAIL
900.08
ci.e#1.a#3.E#40.A#60.c#264.w#4.s#2.asp
FAIL
900.08
small-swap2-fixpoint-4
FAIL
900.08
chess_solving_mate_in_3_2016_BEL-CH-23A_02
FAIL
900.08
k0225744.connected.oe
FAIL
900.08
pg-hkb-12
FAIL
900.09
genbuf5b4n.unsat
FAIL
900.09
klieber2017q-116-29-eq
FAIL
900.09
genbuf5b4n.sat
FAIL
900.09
test2_quant_squaring2
FAIL
900.09
mult_bool_matrix_4_5_5.sat
FAIL
900.09
ci.e#1.a#3.E#40.A#60.c#400.w#4.s#5.asp
FAIL
900.09
ci.e#1.a#3.E#40.A#60.c#376.w#6.s#7.asp
FAIL
900.09
cycle_sched_6_2_1.sat
FAIL
900.09
chess_solving_mate_in_4_2009_SEROCK-OPEN_09
FAIL
900.09
jctc14-unrolled-fail
FAIL
900.09
klieber2017q-074-18-eq
FAIL
900.09
rankfunc33_signed_32
FAIL
900.09
query49_query58_1344
FAIL
900.09
CM-sat-03-01-06-4
FAIL
900.09
sortnetsort9.v.stepl.007
FAIL
900.09
ltl2dpa_C26_comp3_REAL.unsat
FAIL
900.09
pg-hkb-11
FAIL
900.09
ken.flash^08.C-d4
FAIL
900.09
klieber2017q-104-26-eq
FAIL
900.1
chess_solving_mate_in_6_2016_RUS-CH_15
FAIL
900.1
ci.e#1.a#3.E#40.A#60.c#304.w#4.s#7.asp
FAIL
900.1
pg-hkb-23
FAIL
900.1
cycle_sched_6_2_1.unsat
FAIL
900.1
k0302060.c.oe
FAIL
900.1
chess_solving_mate_in_3_1999_WCSC-23_05
FAIL
900.1
Contact
|
Organization
|
Links
|
Citing QBFLIB