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
qbfrelay-limited-depqbf
QBFEVAL'17 - Prenex 2QBF Track
Instance
Result
Time
small-bug1-fixpoint-8
SAT
0.11
small-bug1-fixpoint-5
SAT
0.11
small-bug1-fixpoint-6
SAT
0.11
small-bug1-fixpoint-3
SAT
0.11
falsequ_query42_1344n
UNSAT
0.12
small-dyn-partition-fixpoint-1
UNSAT
0.13
floor128
SAT
0.14
small-bug1-fixpoint-10
SAT
0.15
small-bug1-fixpoint-4
SAT
0.16
trueque_query42_1344n
UNSAT
0.16
query24_query42_1344n
UNSAT
0.16
rankfunc55_unsigned_32
SAT
0.17
rankfunc48_unsigned_16
SAT
0.18
query23_query42_1344n
UNSAT
0.18
kenflashp04
SAT
0.18
stmt27_16_224
UNSAT
0.2
small-bug1-fixpoint-9
SAT
0.2
equalization128
SAT
0.2
axquery_query42_1344n
UNSAT
0.23
nxquery_query42_1344n
UNSAT
0.23
query30_query42_1344n
UNSAT
0.24
decomposition128
SAT
0.24
ntrivil_query42_1344n
UNSAT
0.25
bobtuint31neg
SAT
0.25
rankfunc60_unsigned_32
SAT
0.26
sdlx-fixpoint-1
UNSAT
0.26
stmt21_178_258
UNSAT
0.27
small-pipeline-fixpoint-1
UNSAT
0.29
query15_query42_1344n
UNSAT
0.3
trivial_query42_1344n
UNSAT
0.3
query02_query42_1344n
UNSAT
0.3
small-dyn-partition-fixpoint-2
UNSAT
0.34
stmt22_311_370
UNSAT
0.35
query07_query42_1344n
UNSAT
0.36
stmt19_352_359
UNSAT
0.38
stmt21_70_369
UNSAT
0.43
stmt21_84_364
UNSAT
0.45
stmt21_71_354
UNSAT
0.59
itc-b13-fixpoint-1
UNSAT
0.62
stmt19_180_352
UNSAT
0.63
stmt31_22_328
UNSAT
0.81
exquery_query42_1344n
UNSAT
1.22
small-dyn-partition-fixpoint-3
UNSAT
1.31
query21_query42_1344n
UNSAT
2.51
stmt44_40_387
UNSAT
3.45
small-dyn-partition-fixpoint-4
UNSAT
10.76
stmt52_295_394
UNSAT
21.64
stmt53_296_346
UNSAT
26.97
query26_query42_1344n
UNSAT
27.03
stmt21_84_215
UNSAT
28.05
stmt19_66_214
UNSAT
28.15
small-dyn-partition-fixpoint-5
UNSAT
42.31
small-dyn-partition-fixpoint-6
UNSAT
45.82
stmt46_111_238
UNSAT
66.63
pdtpmsrotate32
SAT
72.39
rankfunc38_signed_64
SAT
72.44
rankfunc38_unsigned_64
SAT
72.45
add20y.sat
SAT
72.47
small-dyn-partition-fixpoint-7
UNSAT
72.51
small-dyn-partition-fixpoint-9
UNSAT
72.54
stmt41_262_275
SAT
72.59
stmt5_731_730
SAT
72.61
stmt25_597_598
SAT
72.66
small-dyn-partition-fixpoint-10
UNSAT
72.7
usb-phy-fixpoint-1
UNSAT
72.79
itc-b13-fixpoint-2
UNSAT
72.92
small-swap1-fixpoint-5
SAT
72.95
eijkbs3330
SAT
72.97
small-swap2-fixpoint-5
SAT
73
small-swap1-fixpoint-4
SAT
73.02
driver_c9y.sat
SAT
73.05
rankfunc56_unsigned_64
SAT
73.11
small-synabs-fixpoint-10
UNSAT
73.12
driver_c9n.sat
SAT
73.23
rankfunc56_signed_64
SAT
73.24
small-swap2-fixpoint-6
SAT
73.31
small-seq-fixpoint-1
UNSAT
73.33
stmt27_93_98
SAT
73.34
small-swap1-fixpoint-6
SAT
73.34
small-swap1-fixpoint-7
SAT
73.43
small-swap2-fixpoint-7
SAT
73.49
rankfunc55_signed_64
SAT
73.55
rankfunc34_unsigned_64
SAT
73.56
itc-b13-fixpoint-3
SAT
73.61
rankfunc34_signed_64
SAT
73.67
rankfunc53_signed_64
SAT
73.73
rankfunc55_unsigned_64
SAT
73.76
small-swap1-fixpoint-8
SAT
73.8
rankfunc53_unsigned_64
SAT
73.86
rankfunc49_unsigned_64
SAT
73.89
small-swap2-fixpoint-8
SAT
73.89
ceiling256
SAT
73.89
small-swap1-fixpoint-9
SAT
74
cycle_sched_12_2_1.sat
SAT
74.03
rankfunc61_unsigned_64
SAT
74.17
rankfunc51_signed_64
SAT
74.19
rankfunc51_unsigned_64
SAT
74.24
rankfunc52_signed_64
SAT
74.3
small-swap2-fixpoint-9
SAT
74.34
rankfunc52_unsigned_64
SAT
74.4
small-swap2-fixpoint-10
SAT
74.44
mult_bool_matrix_dyn_9_5.sat
SAT
74.46
rankfunc61_signed_64
SAT
74.52
itc-b13-fixpoint-4
SAT
74.54
rankfunc58_signed_64
SAT
74.58
rankfunc58_unsigned_64
SAT
74.61
stmt21_181_218
UNSAT
74.63
rankfunc49_signed_64
SAT
74.77
cache-coherence-3-fixpoint-1
UNSAT
74.77
rankfunc2_unsigned_64
SAT
74.8
usb-phy-fixpoint-2
UNSAT
74.94
rankfunc54_unsigned_64
SAT
75.06
rankfunc54_signed_64
SAT
75.07
rankfunc57_unsigned_64
SAT
75.11
rankfunc59_signed_64
SAT
75.59
rankfunc59_unsigned_64
SAT
75.6
rankfunc35_unsigned_64
SAT
75.64
cache-coherence-2-fixpoint-2
UNSAT
75.68
ethernet-fixpoint-1
UNSAT
75.69
bs128n.sat
SAT
75.9
driver_a10y.sat
SAT
76.02
bs128y.sat
SAT
76.04
driver_b8n.sat
SAT
76.26
sdlx-fixpoint-2
UNSAT
76.39
ltl2dba_C2-8_comp4_REAL.sat
SAT
76.75
small-seq-fixpoint-2
UNSAT
76.97
rankfunc35_signed_64
SAT
76.99
rankfunc31_unsigned_64
SAT
77.1
itc-b13-fixpoint-6
SAT
77.16
rankfunc41_signed_64
SAT
77.43
stmt19_3_401
UNSAT
77.43
rankfunc41_unsigned_64
SAT
77.65
rankfunc48_signed_64
SAT
77.68
rankfunc31_signed_64
SAT
77.83
rankfunc48_unsigned_64
SAT
77.9
stmt22_320_370
SAT
78.22
stmt23_66_67
SAT
78.48
cache-coherence-3-fixpoint-2
UNSAT
78.76
itc-b13-fixpoint-7
SAT
78.92
stmt17_63_70
SAT
79.07
stmt53_208_245
UNSAT
79.14
stmt19_133_217
UNSAT
79.16
stmt21_354_403
SAT
79.2
stmt85_300_399
SAT
79.68
ctrl.e#1.a#3.E#128.A#48.c#.w#7.s#1.asp
SAT
79.75
stmt19_302_352
SAT
79.83
stmt19_368_417
SAT
79.92
stmt23_66_76
SAT
79.98
stmt19_90_408
UNSAT
80.01
stmt21_143_403
UNSAT
80.07
itc-b13-fixpoint-8
SAT
80.34
small-swap1-fixpoint-10
SAT
80.89
stmt27_149_224
UNSAT
81.01
itc-b13-fixpoint-9
SAT
81.55
ctrl.e#1.a#3.E#110.A#48.c#.w#9.s#13.asp
SAT
81.56
stmt22_6_414
UNSAT
82.01
stmt28_68_73
SAT
82.03
stmt19_137_408
UNSAT
82.5
stmt29_275_376
UNSAT
83.18
cycle_sched_4_4_2.sat
SAT
83.57
itc-b13-fixpoint-10
SAT
83.58
stmt21_71_413
UNSAT
84.81
ethernet-fixpoint-2
UNSAT
84.93
stmt31_190_227
UNSAT
85
stmt28_68_69
SAT
85.81
stmt17_63_78
SAT
86.88
cache-coherence-2-fixpoint-5
UNSAT
88.5
usb-phy-fixpoint-4
UNSAT
90.03
amba2c7n.sat
SAT
94.96
load_2c_comp_comp7_REAL.sat
SAT
97.62
small-seq-fixpoint-4
UNSAT
98.01
ethernet-fixpoint-3
UNSAT
100.42
mult_bool_matrix_12_13_11.sat
SAT
100.95
sortnetsort9.AE.stepl.004
SAT
103.39
sortnetsort8.AE.stepl.004
SAT
104.01
usb-phy-fixpoint-5
UNSAT
106.29
sortnetsort8.AE.stepl.006
UNSAT
137.93
beemskbn1f1_c0to7.sat
SAT
139.11
sortnetsort10.AE.stepl.004
SAT
143.13
mult9.sat
SAT
144.57
small-seq-fixpoint-6
UNSAT
152.19
mult_bool_matrix_18_18_18.sat
SAT
152.25
query03_query42_1344n
UNSAT
156.19
oski3ub5i_c0to63.sat
SAT
157.51
oski3ub5i_c0to511.sat
SAT
159.62
cycle_sched_2_10_1.sat
SAT
165.47
ctrl.e#1.a#3.E#116.A#48.c#.w#7.s#56.asp
SAT
177.27
sortnetsort7.AE.stepl.006
UNSAT
181.05
6s289rb05233_c0to63.sat
SAT
182.45
query31_query50_1344n
SAT
185.14
sortnetsort7.AE.stepl.005
SAT
207.06
sortnetsort9.AE.stepl.008
UNSAT
210.52
sortnetsort8.AE.stepl.009
UNSAT
229.88
sortnetsort8.AE.stepl.008
UNSAT
249
sortnetsort10.AE.stepl.009
UNSAT
249.09
nxquery_query50_1344n
SAT
263.45
sortnetsort9.AE.stepl.011
UNSAT
266.63
sortnetsort9.AE.stepl.005
SAT
302.22
amba3b5y.sat
SAT
387.61
query08_query42_1344n
UNSAT
393.74
query27_query42_1344n
UNSAT
396.62
sortnetsort10.AE.stepl.010
UNSAT
432.02
sortnetsort8.AE.stepl.005
SAT
438.05
sortnetsort10.AE.stepl.005
SAT
495.11
sortnetsort10.AE.stepl.011
UNSAT
550.41
sortnetsort10.AE.stepl.012
UNSAT
641.28
query52_query25_1344n
SAT
679.66
reachqu_query42_1344n
FAIL
885.41
query42_query60_1344n
FAIL
885.71
small-equiv-fixpoint-8
FAIL
885.85
small-equiv-fixpoint-4
FAIL
885.94
query48_query42_1344n
FAIL
886.1
load_3c_comp_comp6_REAL.sat
FAIL
886.12
small-equiv-fixpoint-3
FAIL
886.44
query42_query45_1344n
FAIL
886.61
query33_query57_1344n
FAIL
886.93
query60_query10_1344n
FAIL
887
ctrl.e#1.a#3.E#128.A#48.c#.w#9.s#60.asp
FAIL
887.07
ctrl.e#1.a#3.E#128.A#48.c#.w#9.s#1.asp
FAIL
887.13
nreachq_query42_1344n
FAIL
887.17
nreachq_query11_1344n
FAIL
887.17
ActivityService
FAIL
887.2
PhaseService
FAIL
887.24
small-pipeline-fixpoint-10
FAIL
887.33
ConcreteActivityService
FAIL
887.43
eequery_query42_1344n
FAIL
887.51
query10_query45_1344n
FAIL
887.58
ctrl.e#1.a#3.E#112.A#48.c#.w#5.s#27.asp
FAIL
887.6
NotificationServiceImpl2
FAIL
887.63
query64_query42_1344n
FAIL
887.75
query48_exquery_1344n
FAIL
887.8
small-equiv-fixpoint-2
FAIL
887.83
query55_query42_1344n
FAIL
887.87
IterationService
FAIL
887.9
GuidanceService2
FAIL
887.92
ctrl.e#1.a#3.E#128.A#48.c#.w#3.s#60.asp
FAIL
887.92
query54_query42_1344n
FAIL
887.92
query06_query42_1344n
FAIL
887.93
sortnetsort7.AE.stepl.007
FAIL
887.96
query54_query58_1344n
FAIL
887.96
sdlx-fixpoint-6
FAIL
887.99
query05_query31_1344n
FAIL
888.01
ctrl.e#1.a#3.E#128.A#48.c#.w#3.s#1.asp
FAIL
888.03
query64_query11_1344n
FAIL
888.09
ctrl.e#1.a#3.E#122.A#48.c#.w#3.s#51.asp
FAIL
888.12
query71_query31_1344n
FAIL
888.13
stmt17_70_86
FAIL
888.19
query51_query42_1344n
FAIL
888.2
query60_query45_1344n
FAIL
888.22
ctrl.e#1.a#3.E#120.A#48.c#.w#3.s#3.asp
FAIL
888.24
query31_eequery_1344n
FAIL
888.25
query33_query45_1344n
FAIL
888.27
query04_query25_1344n
FAIL
888.29
ctrl.e#1.a#3.E#124.A#48.c#.w#7.s#50.asp
FAIL
888.3
stmt23_92_96
FAIL
888.32
LoginService
FAIL
888.35
stmt17_78_98
FAIL
888.37
ctrl.e#1.a#3.E#128.A#48.c#.w#3.s#26.asp
FAIL
888.38
stmt41_336_385
FAIL
888.41
stmt19_79_83
FAIL
888.46
query71_query34_1344n
FAIL
888.48
stmt17_82_86
FAIL
888.48
query25_query42_1344n
FAIL
888.53
stmt19_83_91
FAIL
888.56
ethernet-fixpoint-4
FAIL
888.61
small-pipeline-fixpoint-2
FAIL
888.63
stmt17_94_98
FAIL
888.63
small-equiv-fixpoint-7
FAIL
888.66
eequery_query64_1344n
FAIL
888.66
stmt17_74_90
FAIL
888.66
small-equiv-fixpoint-1
FAIL
888.7
ctrl.e#1.a#3.E#118.A#48.c#.w#5.s#7.asp
FAIL
888.75
query05_query42_1344n
FAIL
888.77
sortnetsort7.AE.stepl.009
FAIL
888.78
stmt17_78_90
FAIL
888.79
sortnetsort7.AE.stepl.008
FAIL
888.81
sdlx-fixpoint-5
FAIL
888.84
intermediate256
FAIL
888.88
query42_query42_1344n
FAIL
888.89
small-pipeline-fixpoint-8
FAIL
888.92
small-pipeline-fixpoint-9
FAIL
888.98
cycle_sched_6_6_2.sat
FAIL
889.04
stmt17_82_94
FAIL
889.06
stmt17_74_78
FAIL
889.06
stmt19_75_95
FAIL
889.06
query01_query42_1344n
FAIL
889.08
small-equiv-fixpoint-5
FAIL
889.13
stmt46_289_388
FAIL
889.13
query34_query11_1344n
FAIL
889.14
stmt23_67_92
FAIL
889.15
stmt19_71_95
FAIL
889.23
stmt28_89_97
FAIL
889.25
query11_query42_1344n
FAIL
889.25
query34_query42_1344n
FAIL
889.33
query60_query42_1344n
FAIL
889.35
ctrl.e#1.a#3.E#128.A#48.c#.w#7.s#60.asp
FAIL
889.36
query09_query42_1344n
FAIL
889.43
query64_query01_1344n
FAIL
889.43
ctrl.e#1.a#3.E#128.A#48.c#.w#3.s#17.asp
FAIL
889.46
ctrl.e#1.a#3.E#130.A#48.c#.w#7.s#11.asp
FAIL
889.46
ctrl.e#1.a#3.E#128.A#48.c#.w#7.s#7.asp
FAIL
889.52
query58_query42_1344n
FAIL
889.52
query50_query42_1344n
FAIL
889.58
mult_bool_matrix_dyn_7_7.sat
FAIL
889.59
ctrl.e#1.a#3.E#128.A#48.c#.w#5.s#1.asp
FAIL
889.59
genbuf14b4y.sat
FAIL
889.66
amba4c7n.sat
FAIL
889.67
query45_query42_1344n
FAIL
889.68
stmt41_286_385
FAIL
889.7
stmt19_65_87
FAIL
889.74
stmt17_62_78
FAIL
889.76
query04_query42_1344n
FAIL
889.77
stmt23_88_92
FAIL
889.81
query31_query42_1344n
FAIL
889.82
query60_query44_1344n
FAIL
889.83
genbuf8b4n.sat
FAIL
889.85
stmt19_75_83
FAIL
889.88
IssueServiceImpl
FAIL
889.89
genbuf7b4n.sat
FAIL
889.95
query10_query42_1344n
FAIL
889.97
stmt28_73_97
FAIL
889.99
query33_query42_1344n
FAIL
890.01
query49_ntrivil_1344n
FAIL
890.02
stmt50_343_392
FAIL
890.03
query71_query42_1344n
FAIL
890.04
query44_query42_1344n
FAIL
890.1
query49_query42_1344n
FAIL
890.13
query60_query33_1344n
FAIL
890.13
sortnetsort10.AE.stepl.006
FAIL
890.13
stmt47_290_340
FAIL
890.22
stmt19_64_87
FAIL
890.23
stmt17_78_94
FAIL
890.24
stmt17_70_78
FAIL
890.27
query71_query36_1344n
FAIL
890.38
query57_query42_1344n
FAIL
890.41
GuidanceService
FAIL
890.42
query33_query51_1344n
FAIL
890.42
small-pipeline-fixpoint-3
FAIL
890.43
query52_query42_1344n
FAIL
890.44
stmt28_73_85
FAIL
890.49
ctrl.e#1.a#3.E#128.A#48.c#.w#5.s#60.asp
FAIL
890.51
stmt47_340_389
FAIL
890.52
query50_query06_1344n
FAIL
890.52
nreachq_query54_1344n
FAIL
890.54
sortnetsort9.AE.stepl.007
FAIL
890.6
amba5b5n.sat
FAIL
890.65
stmt19_65_95
FAIL
890.68
stmt31_276_328
FAIL
890.71
ctrl.e#1.a#3.E#134.A#48.c#.w#9.s#40.asp
FAIL
890.72
query02_query44_1344n
FAIL
890.78
stmt19_79_87
FAIL
890.83
query10_query34_1344n
FAIL
890.84
stmt19_64_91
FAIL
890.91
query36_query42_1344n
FAIL
890.93
stmt17_70_82
FAIL
890.96
query51_query57_1344n
FAIL
891.02
pi-bus-fixpoint-2
FAIL
891.07
query36_query25_1344n
FAIL
891.22
sortnetsort9.AE.stepl.006
FAIL
891.23
query10_query06_1344n
FAIL
891.26
sortnetsort10.AE.stepl.007
FAIL
891.62
sdlx-fixpoint-10
FAIL
891.62
load_full_3_comp5_REAL.sat
FAIL
892.21
ltl2dba_U1-4_comp4_REAL.sat
FAIL
892.22
sdlx-fixpoint-7
FAIL
892.41
sdlx-fixpoint-4
FAIL
892.43
ltl2dba_E6_comp2_REAL.sat
FAIL
892.76
sortnetsort9.AE.stepl.010
FAIL
892.84
sdlx-fixpoint-8
FAIL
893.12
sdlx-fixpoint-9
FAIL
893.31
genbuf12b4y.sat
FAIL
893.49
small-pipeline-fixpoint-4
FAIL
893.6
ltl2dba_Q4_comp4_REAL.sat
FAIL
893.82
stmt19_87_95
FAIL
893.84
small-pipeline-fixpoint-5
FAIL
894.1
neclaftp2002
FAIL
894.75
sortnetsort10.AE.stepl.008
FAIL
895.13
AR-fixpoint-4
FAIL
900
AR-fixpoint-2
FAIL
900
small-seq-fixpoint-10
FAIL
900
AR-fixpoint-10
FAIL
900
load_4c_comp_comp4_REAL.sat
FAIL
900
AR-fixpoint-8
FAIL
900
AR-fixpoint-6
FAIL
900
Contact
|
Organization
|
Links
|
Citing QBFLIB