Instances solved by PortfolioDepQBFGhostQRaReQSQute___pf
QBFEVAL'18 - Prenex 2QBF Track

InstanceResultTime
small-synabs-fixpoint-3UNSAT5.27
pdtpmsrotate32SAT5.29
Q_2-3_v-80-100_r-13.4UNSAT5.3
small-pipeline-fixpoint-1UNSAT5.33
rankfunc60_unsigned_32SAT5.38
small-seq-fixpoint-1UNSAT5.38
floor128SAT5.38
rankfunc56_unsigned_64SAT5.39
floor256SAT5.39
rankfunc56_signed_64SAT5.4
rankfunc48_unsigned_16SAT5.41
itc-b13-fixpoint-1UNSAT5.42
stmt27_16_224UNSAT5.45
decomposition128SAT5.46
rankfunc53_unsigned_64SAT5.46
decomposition256SAT5.49
rankfunc51_signed_64SAT5.53
rankfunc58_signed_64SAT5.54
rankfunc53_signed_64SAT5.55
stmt22_6_414UNSAT5.56
rankfunc61_unsigned_64SAT5.62
stmt19_90_408UNSAT5.62
stmt21_71_413UNSAT5.63
rankfunc54_signed_64SAT5.64
stmt19_137_408UNSAT5.64
rankfunc49_signed_64SAT5.65
rankfunc61_signed_64SAT5.66
stmt21_178_258UNSAT5.7
stmt46_111_238UNSAT5.7
rankfunc59_unsigned_64SAT5.71
rankfunc51_unsigned_64SAT5.71
rankfunc52_signed_64SAT5.72
rankfunc54_unsigned_64SAT5.73
rankfunc52_unsigned_64SAT5.73
rankfunc58_unsigned_64SAT5.73
rankfunc35_unsigned_64SAT5.76
rankfunc31_unsigned_64SAT5.8
stmt31_22_328UNSAT5.8
itc-b13-fixpoint-2UNSAT5.8
stmt41_160_235UNSAT5.81
stmt19_66_214UNSAT5.85
rankfunc49_unsigned_64SAT5.85
stmt44_40_387UNSAT5.87
stmt21_84_364UNSAT5.88
stmt19_133_217UNSAT5.88
stmt21_70_369UNSAT5.89
rankfunc31_signed_64SAT5.89
rankfunc41_unsigned_64SAT5.89
rankfunc59_signed_64SAT5.9
rankfunc48_signed_64SAT5.9
exquery_query42_1344nUNSAT5.91
stmt21_71_354UNSAT5.93
stmt19_3_401UNSAT5.94
stmt21_181_369UNSAT5.97
stmt19_83_412UNSAT5.99
small-swap1-fixpoint-4SAT5.99
stmt21_143_403UNSAT6
Q_2-3_v-80-100_r-13.6UNSAT6.03
usb-phy-fixpoint-1UNSAT6.07
rankfunc41_signed_64SAT6.23
stmt29_226_376UNSAT6.23
itc-b13-fixpoint-3SAT6.24
small-swap1-fixpoint-6SAT6.3
rankfunc55_unsigned_64SAT6.45
rankfunc2_unsigned_64SAT6.46
Q_2-3_v-80-100_r-13.5UNSAT6.63
Q_2-3_v-80-100_r-13.2UNSAT6.76
stmt27_149_224UNSAT6.87
small-swap1-fixpoint-5SAT6.91
rankfunc35_signed_64SAT7
small-swap1-fixpoint-7SAT7.01
small-swap1-fixpoint-8SAT7.02
itc-b13-fixpoint-4SAT7.04
ntrivil_query42_1344nUNSAT7.04
Q_2-3_v-80-100_r-13.1UNSAT7.08
Q_2-3_v-80-100_r-13.0UNSAT7.15
stmt19_352_359UNSAT7.16
ctrl.e#1.a#3.E#128.A#48.c#.w#7.s#1.aspSAT7.24
rankfunc57_unsigned_64SAT7.31
stmt50_343_392UNSAT7.33
stmt21_310_360UNSAT7.41
ctrl.e#1.a#3.E#110.A#48.c#.w#9.s#13.aspSAT7.46
stmt21_181_218UNSAT7.48
stmt22_311_370UNSAT7.64
stmt9_445_446SAT7.75
stmt41_286_385UNSAT7.82
stmt52_295_394UNSAT7.86
small-swap1-fixpoint-10SAT7.87
itc-b13-fixpoint-5SAT7.87
Q_2-3_v-80-100_r-13.7UNSAT7.97
Q_2-3_v-80-100_r-11.3UNSAT8.21
cache-coherence-3-fixpoint-1UNSAT8.68
rankfunc48_unsigned_64SAT8.87
small-swap1-fixpoint-9SAT8.9
Q_2-3_v-80-100_r-13.3UNSAT8.9
bs128n.satSAT8.94
stmt29_275_376UNSAT8.95
bs128y.satSAT9.17
trivial_query42_1344nUNSAT9.28
itc-b13-fixpoint-6SAT9.29
driver_c9n.satSAT9.31
Q_2-3_v-80-100_r-13.8UNSAT9.32
stmt25_597_598SAT9.41
stmt46_289_388UNSAT9.45
kenflashp04SAT9.48
stmt124_966_965SAT9.58
stmt5_731_730SAT9.58
stmt41_262_275SAT9.6
stmt16_818_819SAT9.6
stmt44_554_604SAT9.71
ltl2dba_C2-6_comp3_REAL.satSAT9.76
driver_c9y.satSAT9.8
small-seq-fixpoint-2UNSAT9.83
driver_d9y.satSAT9.85
ci.e#1.a#3.E#40.A#60.c#416.w#2.s#3.aspUNSAT10
ethernet-fixpoint-1UNSAT10.02
query02_query44_1344nUNSAT10.06
query27_query42_1344nUNSAT10.11
axquery_query42_1344nUNSAT10.26
stmt31_190_227UNSAT10.54
query02_query42_1344nUNSAT10.66
cache-coherence-2-fixpoint-2UNSAT10.74
ltl2dba_C2-8_comp4_REAL.satSAT10.83
nxquery_query42_1344nUNSAT10.87
ci.e#1.a#3.E#40.A#60.c#408.w#2.s#1.aspUNSAT10.9
cycle_sched_12_2_1.satSAT11.02
driver_a10y.satSAT11.07
ci.e#1.a#3.E#40.A#60.c#400.w#2.s#1.aspUNSAT11.17
stmt53_208_245UNSAT11.31
small-pipeline-fixpoint-2UNSAT11.4
usb-phy-fixpoint-2UNSAT11.46
itc-b13-fixpoint-7SAT11.56
small-synabs-fixpoint-10UNSAT11.67
itc-b13-fixpoint-8SAT12.23
cache-coherence-3-fixpoint-2UNSAT12.27
usb-phy-fixpoint-3UNSAT12.37
ci.e#1.a#3.E#40.A#60.c#288.w#6.s#2.aspSAT12.5
Q_2-3_v-80-100_r-11.2UNSAT12.55
itc-b13-fixpoint-9SAT12.65
query26_query42_1344nUNSAT12.7
beemskbn1f1_c0to7.satSAT12.81
itc-b13-fixpoint-10SAT12.84
ctrl.e#1.a#3.E#124.A#48.c#.w#7.s#50.aspSAT13.01
nxquery_query50_1344nSAT13.32
stmt39_285_335UNSAT13.86
stmt47_340_389UNSAT14.13
stmt47_290_340UNSAT14.6
ethernet-fixpoint-2UNSAT14.95
Q_2-3_v-80-100_r-11.6UNSAT15.03
ci.e#1.a#3.E#40.A#60.c#408.w#2.s#2.aspUNSAT15.24
sortnetsort8.AE.stepl.004SAT15.52
usb-phy-fixpoint-4UNSAT15.73
cache-coherence-3-fixpoint-3UNSAT16.54
cache-coherence-2-fixpoint-4UNSAT17.49
sortnetsort9.AE.stepl.004SAT18.2
ethernet-fixpoint-3UNSAT18.77
query07_query42_1344nUNSAT19.45
small-seq-fixpoint-3UNSAT20.01
query03_query42_1344nUNSAT20.38
ctrl.e#1.a#3.E#112.A#48.c#.w#5.s#27.aspSAT20.88
cache-coherence-2-fixpoint-5UNSAT21.03
ctrl.e#1.a#3.E#116.A#48.c#.w#7.s#56.aspSAT21.78
pi-bus-fixpoint-1UNSAT22.52
usb-phy-fixpoint-5UNSAT24.16
ethernet-fixpoint-4UNSAT24.39
query52_query25_1344nSAT24.77
query04_query25_1344nSAT24.77
query31_eequery_1344nSAT26.16
query36_query25_1344nSAT26.18
query04_query42_1344nUNSAT26.85
query33_query45_1344nSAT28.01
query31_query50_1344nSAT29.84
eequery_query64_1344nSAT30.02
query64_query01_1344nSAT30.86
Q_2-3_v-80-100_r-13.9UNSAT34.15
amba2c7n.satSAT35.06
stay24n.satSAT35.58
mult_bool_matrix_dyn_9_5.satSAT35.73
cycle_sched_2_10_1.satSAT36.81
driver_b8n.satSAT36.86
mult9.satSAT42.42
stmt27_93_98SAT43.08
stmt25_52_53SAT43.11
stmt1_79_80SAT43.32
mult_bool_matrix_10_9_11.satSAT44.3
mult_bool_matrix_12_13_11.satSAT46.02
stmt2_976_999SAT57.95
mult_bool_matrix_17_17_17.satSAT58.13
mult_bool_matrix_18_18_18.satSAT59.33
stmt23_66_67SAT74.8
stmt17_63_70SAT79.9
stmt28_68_69SAT84.24
stmt17_63_78SAT87.01
stmt17_63_82SAT87.34
stmt23_66_76SAT89.36
stmt17_62_78SAT89.75
stmt23_72_76SAT91.76
stmt28_68_73SAT92.71
stmt17_70_78SAT97.71
stmt17_74_78SAT100.16
stmt19_64_87SAT101.41
stmt28_68_81SAT103.43
stmt23_67_92SAT107.2
stmt19_79_87SAT113.69
GuidanceService2UNSAT114.35
GuidanceServiceUNSAT114.44
stmt19_64_91SAT114.72
stmt19_75_83SAT115.86
stmt17_70_82SAT117.67
stmt17_70_90SAT120.51
stmt17_82_86SAT121.99
stmt19_79_83SAT123.71
stmt17_82_94SAT124.69
stmt23_88_92SAT127.19
stmt17_70_86SAT127.87
stmt19_65_87SAT129.09
stmt17_78_94SAT130.79
stmt28_73_85SAT131.35
stmt23_66_96SAT132.61
stmt17_74_90SAT134.98
stmt19_87_95SAT139.79
Q_2-3_v-80-100_r-11.8UNSAT144.71
stmt19_313_412UNSAT149.48
sdlx-fixpoint-3UNSAT150.03
neclaftp4001UNSAT150.49
Q_2-3_v-80-100_r-11.7UNSAT160.32
stmt31_276_328UNSAT160.58
stmt53_296_346UNSAT163.45
stmt32_329_378UNSAT175.81
Q_2-3_v-80-100_r-11.1UNSAT177.75
small-seq-fixpoint-4UNSAT178.68
Q_2-3_v-80-100_r-11.0UNSAT181.85
Q_2-3_v-80-100_r-11.4UNSAT188.26
cache-coherence-2-fixpoint-6UNSAT196.39
small-seq-fixpoint-5UNSAT214.44
beemldelec4b1_c0to127.satSAT243.68
small-seq-fixpoint-6UNSAT261.07
stmt41_336_385UNSAT317.92
AR-fixpoint-8FAIL603.31
small-seq-fixpoint-8UNSAT783.36
query21_query42_1344nUNSAT869.87
stmt23_92_96FAIL900
ctrl.e#1.a#3.E#128.A#48.c#.w#3.s#26.aspFAIL900
ctrl.e#1.a#3.E#128.A#48.c#.w#5.s#60.aspFAIL900
sortnetsort10.AE.stepl.009FAIL900
query52_query42_1344nFAIL900.01
query25_query42_1344nFAIL900.01
sortnetsort9.AE.stepl.007FAIL900.01
query06_query42_1344nFAIL900.01
ctrl.e#1.a#3.E#128.A#48.c#.w#7.s#60.aspFAIL900.01
stmt21_354_403FAIL900.01
query36_query42_1344nFAIL900.01
query01_query42_1344nFAIL900.01
stmt21_319_418FAIL900.01
sortnetsort7.AE.stepl.005FAIL900.01
small-seq-fixpoint-10FAIL900.01
ceiling128FAIL900.01
cycle_sched_6_7_1.satFAIL900.01
eijkbs4863FAIL900.01
ConcreteActivityServiceFAIL900.01
UserServiceImplFAIL900.01
oski3ub5i_c0to63.satFAIL900.01
query44_query26_1344nFAIL900.01
ceiling256FAIL900.01
ltl2dpa_C26_comp2_REAL.satFAIL900.01
query48_exquery_1344nFAIL900.01
sdlx-fixpoint-6FAIL900.01
reachqu_query64_1344nFAIL900.01
eijkbs3330FAIL900.02
sortnetsort8.AE.stepl.005FAIL900.02
stmt17_78_98FAIL900.02
query31_query42_1344nFAIL900.02
query54_query58_1344nFAIL900.02
oski3ub5i_c0to511.satFAIL900.02
query49_ntrivil_1344nFAIL900.02
sortnetsort10.AE.stepl.005FAIL900.02
query33_query42_1344nFAIL900.02
small-equiv-fixpoint-3FAIL900.02
sdlx-fixpoint-9FAIL900.02
query64_query42_1344nFAIL900.02
cycle_sched_6_6_2.satFAIL900.02
small-seq-fixpoint-7FAIL900.02
small-equiv-fixpoint-4FAIL900.02
sortnetsort10.AE.stepl.012FAIL900.02
query34_query11_1344nFAIL900.02
query51_query42_1344nFAIL900.02
neclaftp2002FAIL900.03
query09_query42_1344nFAIL900.03
query55_query42_1344nFAIL900.03
query21_query58_1344nFAIL900.03
NotificationServiceImpl2FAIL900.03
ctrl.e#1.a#3.E#120.A#48.c#.w#3.s#3.aspFAIL900.03
reachqu_query42_1344nFAIL900.03
genbuf9b4n.satFAIL900.03
query42_query42_1344nFAIL900.03
query34_query42_1344nFAIL900.03
stmt19_65_95FAIL900.03
stmt17_94_98FAIL900.03
eequery_query42_1344nFAIL900.03
AR-fixpoint-6FAIL900.03
AR-fixpoint-4FAIL900.03
cycle_sched_4_4_2.satFAIL900.03
sdlx-fixpoint-4FAIL900.03
sortnetsort10.AE.stepl.004FAIL900.03
sortnetsort10.AE.stepl.011FAIL900.03
sortnetsort10.AE.stepl.010FAIL900.03
stmt85_300_399FAIL900.03
query10_query42_1344nFAIL900.03
query31_reachqu_1344nFAIL900.03
query05_query42_1344nFAIL900.03
nreachq_query11_1344nFAIL900.03
sortnetsort10.AE.stepl.008FAIL900.03
reachqu_query71_1344nFAIL900.04
sortnetsort9.AE.stepl.009FAIL900.04
bobtuint31negFAIL900.04
sdlx-fixpoint-10FAIL900.04
query33_query51_1344nFAIL900.04
sdlx-fixpoint-8FAIL900.04
driver_a9n.satFAIL900.04
query50_query06_1344nFAIL900.04
query60_query45_1344nFAIL900.04
AR-fixpoint-2FAIL900.04
pi-bus-fixpoint-3FAIL900.04
query48_query42_1344nFAIL900.04
stmt17_86_98FAIL900.04
query08_query42_1344nFAIL900.04
small-equiv-fixpoint-8FAIL900.04
stmt19_368_417FAIL900.05
stmt22_320_370FAIL900.05
oski3ub5i_c0to255.satFAIL900.05
stmt19_75_95FAIL900.05
small-pipeline-fixpoint-3FAIL900.05
stmt17_78_90FAIL900.05
AR-fixpoint-1FAIL900.05
AR-fixpoint-10FAIL900.05
query71_query31_1344nFAIL900.05
sortnetsort7.AE.stepl.008FAIL900.05
pdtpmsmiimFAIL900.05
query42_query45_1344nFAIL900.05
sortnetsort8.AE.stepl.006FAIL900.05
stmt28_73_97FAIL900.05
query11_query42_1344nFAIL900.06
sortnetsort9.AE.stepl.011FAIL900.06
ActivityServiceFAIL900.06
sortnetsort8.AE.stepl.008FAIL900.06
sortnetsort8.AE.stepl.009FAIL900.06
add20y.satFAIL900.06
ctrl.e#1.a#3.E#134.A#48.c#.w#9.s#40.aspFAIL900.06
ctrl.e#1.a#3.E#128.A#48.c#.w#9.s#60.aspFAIL900.06
stmt19_64_99FAIL900.06
pi-bus-fixpoint-2FAIL900.06
small-equiv-fixpoint-5FAIL900.06
query50_query42_1344nFAIL900.06
query54_query42_1344nFAIL900.06
Q_2-3_v-80-100_r-11.9FAIL900.06
stmt17_82_98FAIL900.06
ci.e#1.a#3.E#40.A#60.c#384.w#6.s#8.aspFAIL900.06
sdlx-fixpoint-7FAIL900.06
query60_query44_1344nFAIL900.06
query51_query57_1344nFAIL900.06
amba2f9n.satFAIL900.06
query33_query57_1344nFAIL900.06
query64_query11_1344nFAIL900.07
stmt19_71_95FAIL900.07
stmt19_83_91FAIL900.07
stmt19_302_352FAIL900.07
load_2c_comp_comp7_REAL.satFAIL900.07
sortnetsort9.AE.stepl.005FAIL900.07
ctrl.e#1.a#3.E#128.A#48.c#.w#9.s#1.aspFAIL900.07
sortnetsort7.AE.stepl.006FAIL900.07
6s289rb05233_c0to63.satFAIL900.07
intermediate256FAIL900.07
sortnetsort9.AE.stepl.012FAIL900.07
IterationServiceFAIL900.07
IssueServiceImplFAIL900.07
query10_query45_1344nFAIL900.07
query58_query42_1344nFAIL900.07
stmt17_70_98FAIL900.07
cycle_sched_4_7_1.satFAIL900.08
kenflashp12FAIL900.08
sortnetsort9.AE.stepl.010FAIL900.08
query42_query06_1344nFAIL900.08
sortnetsort7.AE.stepl.007FAIL900.08
query71_query36_1344nFAIL900.08
intermediate128FAIL900.08
ctrl.e#1.a#3.E#128.A#48.c#.w#7.s#7.aspFAIL900.08
ctrl.e#1.a#3.E#118.A#48.c#.w#5.s#7.aspFAIL900.08
PhaseServiceFAIL900.08
small-equiv-fixpoint-2FAIL900.08
amba3b5y.satFAIL900.08
Q_2-3_v-80-100_r-11.5FAIL900.08
stmt28_89_97FAIL900.09
stmt17_62_98FAIL900.09
query45_query42_1344nFAIL900.09
nreachq_query54_1344nFAIL900.09
small-equiv-fixpoint-1FAIL900.09
query05_query31_1344nFAIL900.09
sortnetsort9.AE.stepl.008FAIL900.09
ActivityService2FAIL900.09
small-seq-fixpoint-9FAIL900.09
sortnetsort7.AE.stepl.009FAIL900.1
sdlx-fixpoint-5FAIL900.15