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
PortfolioGhostQQfunQuAbSQute___pf2
QBFEVAL'18 - Prenex non-CNF Track
Instance
Result
Time
query04_query03_1133
UNSAT
4.53
query30_eequery_1133
SAT
4.56
random-qcir-1000-50-134
UNSAT
4.57
query51_query48_1133
UNSAT
4.58
random-qcir-1000-50-267
UNSAT
4.59
random-qcir-1000-50-743
UNSAT
4.6
k0206272.s.oe
SAT
4.62
query50_query49_1133
UNSAT
4.62
random-qcir-1000-50-898
UNSAT
4.62
random-qcir-1000-50-98
UNSAT
4.62
random-qcir-1000-50-983
UNSAT
4.62
ntrivil_query54_1133
SAT
4.63
random-qcir-1000-50-68
UNSAT
4.63
random-qcir-1000-50-255
UNSAT
4.64
random-qcir-1000-50-441
UNSAT
4.64
random-qcir-1000-50-393
UNSAT
4.64
random-qcir-1000-50-361
UNSAT
4.64
random-qcir-1000-50-428
UNSAT
4.64
random-qcir-1000-50-930
UNSAT
4.64
JP-sat-02-08-3
SAT
4.64
random-qcir-1000-50-970
UNSAT
4.64
6s318r_c0to15.unsat
UNSAT
4.65
pg-hkb-2
UNSAT
4.65
bs128n.unsat
UNSAT
4.65
query71_query15_1133
UNSAT
4.66
random-qcir-1000-50-275
UNSAT
4.67
random-qcir-1000-50-658
UNSAT
4.67
random-qcir-1000-50-295
UNSAT
4.68
query21_reachqu_1133
SAT
4.68
random-qcir-1000-50-456
UNSAT
4.68
random-qcir-1000-50-846
UNSAT
4.69
random-qcir-1000-50-754
UNSAT
4.69
random-qcir-1000-50-940
UNSAT
4.69
SR-unsat-02-01-06-1
UNSAT
4.7
random-qcir-1000-50-793
UNSAT
4.7
ci.e#1.a#3.E#40.A#60.c#200.w#6.s#6.asp
SAT
4.7
random-qcir-1000-50-473
UNSAT
4.72
random-qcir-1000-50-857
UNSAT
4.73
random-qcir-1000-50-545
UNSAT
4.73
query64_query31_1133
UNSAT
4.8
stay22n.unsat
UNSAT
4.81
ci.e#1.a#3.E#40.A#60.c#432.w#2.s#8.asp
UNSAT
4.85
CM-sat-02-01-07-3
SAT
4.98
ci.e#1.a#3.E#40.A#60.c#424.w#2.s#1.asp
UNSAT
5.02
driver_a9y.unsat
UNSAT
5.1
query08_query26_1344
SAT
5.12
query44_query57_1133
UNSAT
5.15
pg-hkb-3
UNSAT
5.23
jctc6-pass
SAT
5.4
k0201058.c.oe
SAT
5.46
CM-sat-03-01-06-4
SAT
5.47
SR-sat-02-01-07-2
SAT
5.73
k_ph_n-21
SAT
5.77
SR-sat-02-01-06-2
SAT
5.84
ci.e#1.a#3.E#40.A#60.c#208.w#6.s#8.asp
SAT
5.9
klieber2017q-112-28-t1
UNSAT
5.92
klieber2017q-078-19-t1
UNSAT
5.95
ci.e#1.a#3.E#40.A#60.c#264.w#4.s#2.asp
SAT
6
driver_d9n.unsat
UNSAT
6.32
ev-pr-4x4-11-3-0-0-1-lg
SAT
6.38
CM-sat-03-01-07-3
SAT
6.43
ev-pr-4x4-13-3-0-0-1-lg
SAT
6.72
JP-sat-02-07-3
SAT
6.73
sortnetsort9.v.stepl.005
FAIL
6.84
klieber2017q-082-20-eq
FAIL
6.84
ltl2dpa_C26_comp2_REAL.unsat
FAIL
6.85
klieber2017q-104-26-t1
FAIL
6.86
k0026150.s.oe
FAIL
6.86
rankfunc33_signed_32
FAIL
6.87
klieber2017q-108-27-t1
FAIL
6.87
klieber2017q-116-29-eq
FAIL
6.87
genbuf5b4n.sat
FAIL
6.87
klieber2017q-100-25-t1
FAIL
6.87
ltl2dpa_C26_comp3_REAL.sat
FAIL
6.88
ken.oop^2.C-d4
FAIL
6.88
klieber2017q-078-19-eq
FAIL
6.88
klieber2017q-108-27-eq
FAIL
6.88
chess_solving_mate_in_2_2005_POLTAVA-OPEN_01
FAIL
6.89
rankfunc17_unsigned_16
FAIL
6.89
genbuf10b4y.unsat
FAIL
6.89
query49_query58_1344
FAIL
6.9
query64_query55_1344
FAIL
6.9
klieber2017q-104-26-eq
FAIL
6.9
query33_query71_1344
FAIL
6.9
k0300663.s.oe
FAIL
6.9
k0225418.v.oe
FAIL
6.9
klieber2017q-074-18-t1
FAIL
6.9
small-swap1-fixpoint-3
FAIL
6.9
genbuf5b4n.unsat
FAIL
6.9
gb_s2_r2_comp3_REAL.unsat
FAIL
6.91
incrementer-enc07-uniform-depth-25
FAIL
6.91
mult_bool_matrix_2_3_30.unsat
FAIL
6.91
k0026150.h.oe
FAIL
6.91
klieber2017q-084-21-t1
FAIL
6.91
jctc2-pass
FAIL
6.92
mult_bool_matrix_4_5_5.unsat
FAIL
6.92
incrementer-enc08-uniform-depth-33
FAIL
6.92
k0206272.connected.oe
FAIL
6.92
audio_ddksynth_csynth2.cpp
FAIL
6.93
k0206272.h.oe
FAIL
6.93
query03_query57_1344
FAIL
6.93
k_ph_p-12
FAIL
6.93
k0225418.connected.oe
FAIL
6.93
k0026150.connected.oe
FAIL
6.93
klieber2017q-076-19-eq
FAIL
6.93
stay24n.sat
FAIL
6.93
k0302060.c.oe
FAIL
6.94
klieber2017q-096-24-t1
FAIL
6.94
test2_quant_squaring3
FAIL
6.94
jctc9-pass
FAIL
6.94
klieber2017q-074-18-eq
FAIL
6.94
sdlx-fixpoint-3
FAIL
6.94
small-swap2-fixpoint-4
FAIL
6.94
chess_solving_mate_in_2_1983_FIN-CH-4_01
FAIL
6.94
sortnetsort10.v.stepl.005
FAIL
6.94
klieber2017q-080-20-t1
FAIL
6.94
amba2f9n.unsat
FAIL
6.94
klieber2017q-086-21-eq
FAIL
6.94
klieber2017q-092-23-t1
FAIL
6.94
genbuf9b4n.unsat
FAIL
6.94
jctc10-fail
FAIL
6.95
k0206272.v.oe
FAIL
6.95
klieber2017q-100-25-eq
FAIL
6.95
k0225744.connected.oe
FAIL
6.95
load_full_3_comp3_REAL.sat
FAIL
6.95
amba2f9n.sat
FAIL
6.95
klieber2017q-092-23-eq
FAIL
6.95
klieber2017q-086-21-t1
FAIL
6.96
gb_s2_r2_comp3_REAL.sat
FAIL
6.96
k0300663.v.oe
FAIL
6.96
ltl2dpa_C26_comp3_REAL.unsat
FAIL
6.96
mult_bool_matrix_4_5_5.sat
FAIL
6.96
p20-1.pddl_planlen=24
FAIL
6.96
query44_query58_1344
FAIL
6.96
k0225744.h.oe
FAIL
6.96
load_3c_comp_comp7_REAL.unsat
FAIL
6.96
test1_quant_squaring3
FAIL
6.96
klieber2017q-112-28-eq
FAIL
6.96
query48_query42_1344
FAIL
6.96
k0026150.v.oe
FAIL
6.96
chess_solving_mate_in_3_2016_BEL-CH-23A_02
FAIL
6.97
klieber2017q-096-24-eq
FAIL
6.97
jctc4-fail
FAIL
6.97
jctc5-fail
FAIL
6.97
ev-pr-8x8-7-7-0-1-2-lg
FAIL
6.98
chess_solving_mate_in_2_1996_FIN-CH-17_03
FAIL
6.98
beemldelec4b1_c0to15.sat
FAIL
6.98
k0225744.v.oe
FAIL
6.98
bs128n.sat
FAIL
6.98
k0300663.connected.oe
FAIL
6.98
k0225418.h.oe
FAIL
6.98
nreachq_query02_1344
FAIL
6.98
chess_composing_6_template_04
FAIL
6.99
mult_bool_matrix_2_3_30.sat
FAIL
6.99
oski3ub1i_c0to63.sat
FAIL
6.99
sortnetsort9.v.stepl.007
FAIL
6.99
cycle_sched_6_2_1.sat
FAIL
6.99
chess_solving_mate_in_3_2009_POLTAVA-OPEN_03
FAIL
6.99
chess_solving_mate_in_3_2009_FIN-CH-30_04
FAIL
6.99
klieber2017q-116-29-t1
FAIL
6.99
load_full_3_comp3_REAL.unsat
FAIL
6.99
network_ndis_rtlnwifi_hw_hw_ccmp.c
FAIL
7
ken.flash^08.C-d4
FAIL
7
jctc1-pass
FAIL
7
chess_solving_mate_in_5_1996_UKR-CH-10_15
FAIL
7
chess_solving_mate_in_2_2011_ISC-7B_01
FAIL
7
chess_solving_mate_in_2_2012_GER-CH-36-19_03
FAIL
7
chess_composing_6_template_06
FAIL
7.01
dungeon_i15-m7-u4-v0.pddl_planlen=81
FAIL
7.01
incrementer-enc02-uniform-depth-58
FAIL
7.01
query08_query64_1344
FAIL
7.02
query42_query57_1344
FAIL
7.02
k0225418.c.oe
FAIL
7.02
input_pnpi8042_moudep.c
FAIL
7.02
oski3ub1i_c0to63.unsat
FAIL
7.02
jctc13-fail
FAIL
7.03
filesys_smbmrx_cvsndrcv.c
FAIL
7.03
chess_solving_mate_in_3_1999_WCSC-23_05
FAIL
7.03
rankfunc13_unsigned_64
FAIL
7.03
chess_solving_mate_in_4_1984_GBR-CH-5_04
FAIL
7.03
chess_composing_8_template_43
FAIL
7.04
query64_query58_1344
FAIL
7.04
k_ph_p-19
FAIL
7.05
chess_solving_mate_in_4_1999_GER-CH-23-6_14
FAIL
7.06
nreachq_reachqu_2233
FAIL
7.06
k0225744.s.oe
FAIL
7.06
chess_solving_mate_in_5_1984_FIN-CH-5_09
FAIL
7.07
ev-pr-4x4-15-3-0-0-1-s
FAIL
7.07
k0225682.c.oe
FAIL
7.07
chess_composing_8_template_02
FAIL
7.07
chess_composing_6_template_01
FAIL
7.07
mv16y.sat
FAIL
7.08
chess_composing_8_template_13
FAIL
7.08
beemldelec4b1_c0to15.unsat
FAIL
7.08
jctc8-pass
FAIL
7.08
chess_composing_8_template_42
FAIL
7.08
jctc14-unrolled-fail
FAIL
7.09
jctc7-pass
FAIL
7.09
query42_query64_1344
FAIL
7.09
network_irda_miniport_nscirda_comm.c
FAIL
7.09
jctc16-vals-0,2-pass
FAIL
7.1
jctc15-unrolled-fail
FAIL
7.1
chess_solving_mate_in_6_2013_WCCC-OPEN-56_10
FAIL
7.11
klieber2017q-080-20-eq
FAIL
7.12
6s318r_c0to31.sat
FAIL
7.12
chess_solving_mate_in_4_2009_SEROCK-OPEN_09
FAIL
7.12
chess_solving_mate_in_6_2016_RUS-CH_15
FAIL
7.13
k0226271.c.oe
FAIL
7.13
test2_quant_squaring2
FAIL
7.13
chess_solving_mate_in_5_2012_NED-CH-18A_11
FAIL
7.14
test3_quant_squaring2
FAIL
7.14
k0225418.s.oe
FAIL
7.14
cycle_sched_6_2_1.unsat
FAIL
7.18
chess_composing_8_template_38
FAIL
7.21
chess_solving_mate_in_6_2011_SRB-CH_15
FAIL
7.33
jctc3-vals-0,2-pass
FAIL
7.37
p20-5.pddl_planlen=32
FAIL
7.39
jctc11-pass
FAIL
7.63
jctc18-vals-0,2-pass
FAIL
7.86
query09_trivial_1344
FAIL
7.96
k0300663.h.oe
FAIL
7.97
pg-hkb-4
UNSAT
8.11
nreachq_reachqu_2133
FAIL
8.19
chess_solving_mate_in_6_1998_OST-CH-1_15
FAIL
8.2
jctc17-vals-0,2-pass
FAIL
8.23
DW-sat-06-20-1
SAT
8.52
CM-sat-04-01-06-3
SAT
8.59
dungeon_i25-m12-u3-v0.pddl_planlen=190
FAIL
8.95
JP-unsat-02-06-3
UNSAT
9.19
dungeon_i25-m12-u3-v0.pddl_planlen=165
FAIL
9.3
k_branch_p-10
UNSAT
9.68
JP-sat-02-07-4
SAT
9.84
SR-unsat-02-01-05-2
UNSAT
10.08
DW-sat-08-22-1
SAT
10.39
DW-sat-08-23-1
SAT
10.46
p20-20.pddl_planlen=23
FAIL
10.82
CM-sat-04-01-06-4
SAT
11.27
DWs-sat-10-23-1
SAT
13.85
CM-sat-04-01-07-3
SAT
14.53
DWs-unsat-07-16-1
UNSAT
14.74
DWs-sat-10-25-1
SAT
14.8
pg-hkb-5
UNSAT
15.35
DWs-sat-12-28-1
SAT
20.6
DWs-unsat-08-17-1
UNSAT
20.7
DWs-unsat-08-18-1
UNSAT
23.33
DW-sat-08-24-1
SAT
24.05
query49_query64_1133
UNSAT
26.14
ci.e#1.a#3.E#40.A#60.c#288.w#4.s#8.asp
SAT
33.75
k_branch_p-11
UNSAT
35.14
DWs-sat-15-35-1
SAT
39.77
ci.e#1.a#3.E#40.A#60.c#400.w#2.s#1.asp
UNSAT
42.45
SR-sat-02-01-06-3
SAT
42.73
ci.e#1.a#3.E#40.A#60.c#296.w#6.s#7.asp
SAT
47.97
DWs-unsat-09-19-1
UNSAT
52.02
pg-hkb-6
UNSAT
58.44
ci.e#1.a#3.E#40.A#60.c#320.w#4.s#8.asp
SAT
63.85
CM-sat-07-01-07-3
SAT
67.61
cnt14
SAT
70.59
DW-sat-09-26-1
SAT
82.7
CM-sat-07-01-06-4
SAT
87.66
ci.e#1.a#3.E#40.A#60.c#304.w#6.s#8.asp
SAT
95.76
DW-unsat-09-22-1
UNSAT
118.69
ci.e#1.a#3.E#40.A#60.c#312.w#2.s#3.asp
SAT
119.32
ci.e#1.a#3.E#40.A#60.c#304.w#4.s#7.asp
SAT
133.23
SR-sat-03-01-07-2
SAT
139.88
SR-sat-03-01-08-2
SAT
144.83
k_branch_n-10
SAT
153.18
ci.e#1.a#3.E#40.A#60.c#280.w#6.s#7.asp
SAT
158.02
DWs-sat-10-24-1
SAT
158.51
ci.e#1.a#3.E#40.A#60.c#296.w#4.s#7.asp
SAT
171.31
DWs-unsat-11-23-1
UNSAT
176.01
JP-unsat-03-08-3
UNSAT
178.69
JP-unsat-03-07-4
UNSAT
211.07
CM-sat-07-01-06-3
SAT
213.87
sortnetsort9.AE.stepl.012
UNSAT
251.73
DW-unsat-10-25-1
UNSAT
261.98
CM-unsat-07-01-06-2
UNSAT
287.34
pg-hkb-7
UNSAT
298.92
DWs-unsat-11-24-1
UNSAT
313.47
k_branch_p-16
UNSAT
347.76
ci.e#1.a#3.E#40.A#60.c#416.w#2.s#3.asp
UNSAT
357.55
ev-pr-6x6-9-5-0-1-2-lg
UNSAT
390.59
DWs-unsat-12-25-1
UNSAT
392.45
ci.e#1.a#3.E#40.A#60.c#312.w#4.s#3.asp
SAT
542.28
DW-unsat-11-26-1
UNSAT
668.78
DW-unsat-11-27-1
UNSAT
807.24
SR-unsat-03-01-06-2
UNSAT
888.41
pipesnotankage18_8
FAIL
900
pg-hkb-20
FAIL
900
pg-hkb-15
FAIL
900
pg-hkb-14
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#400.w#6.s#4.asp
FAIL
900
chess_solving_mate_in_7_2005_GER-CH-29-12_15
FAIL
900
pg-hkb-16
FAIL
900
pg-hkb-21
FAIL
900.01
cnt16r
FAIL
900.01
ev-pr-6x6-11-5-0-1-2-lg
FAIL
900.01
pg-hkb-22
FAIL
900.02
pg-hkb-17
FAIL
900.02
k_branch_n-12
FAIL
900.02
ci.e#1.a#3.E#40.A#60.c#384.w#6.s#3.asp
FAIL
900.02
JP-unsat-03-09-4
FAIL
900.02
pg-hkb-12
FAIL
900.02
chess_solving_mate_in_7_2009_POL-CH-33_15
FAIL
900.02
ci.e#1.a#3.E#40.A#60.c#360.w#2.s#8.asp
FAIL
900.03
ci.e#1.a#3.E#40.A#60.c#368.w#2.s#7.asp
FAIL
900.03
pg-hkb-23
FAIL
900.03
ev-pr-6x6-17-5-0-1-2-lg
FAIL
900.04
chess_solving_mate_in_7_2016_BEL-CH-23A_03
FAIL
900.05
JP-sat-03-09-4
FAIL
900.05
pg-hkb-26
FAIL
900.05
chess_solving_mate_in_7_2011_SVK-CH-19_15
FAIL
900.05
pg-hkb-8
FAIL
900.06
JP-unsat-03-08-5
FAIL
900.06
pg-hkb-13
FAIL
900.07
pg-hkb-24
FAIL
900.07
pg-hkb-11
FAIL
900.07
ci.e#1.a#3.E#40.A#60.c#376.w#6.s#6.asp
FAIL
900.07
pg-hkb-10
FAIL
900.08
qshifter_7
FAIL
900.08
pg-hkb-25
FAIL
900.08
chess_solving_mate_in_9_2003_RUS-CH_15
FAIL
900.08
ci.e#1.a#3.E#40.A#60.c#400.w#4.s#5.asp
FAIL
900.08
ci.e#1.a#3.E#40.A#60.c#376.w#4.s#6.asp
FAIL
900.08
ci.e#1.a#3.E#40.A#60.c#376.w#6.s#7.asp
FAIL
900.08
pipesnotankage14_10
FAIL
900.08
JP-sat-03-08-4
FAIL
900.09
pg-hkb-18
FAIL
900.09
pg-hkb-19
FAIL
900.09
DWs-unsat-13-28-1
FAIL
900.09
pg-hkb-9
FAIL
900.11
chess_solving_mate_in_8_2011_BEL-CH-19A_03
FAIL
900.12
Contact
|
Organization
|
Links
|
Citing QBFLIB