Instances solved by GhostQ-PG_plain
QBFEVAL'18 - Prenex 2QBF Track

InstanceResultTime
small-synabs-fixpoint-3UNSAT0
itc-b13-fixpoint-1UNSAT0.28
nxquery_query42_1344nUNSAT0.35
axquery_query42_1344nUNSAT0.36
query02_query42_1344nUNSAT0.44
stmt27_16_224UNSAT0.52
exquery_query42_1344nUNSAT0.54
stmt19_66_214UNSAT0.58
small-pipeline-fixpoint-1UNSAT0.61
query02_query44_1344nUNSAT0.61
stmt19_133_217UNSAT0.64
usb-phy-fixpoint-1UNSAT0.67
stmt46_111_238UNSAT0.67
rankfunc60_unsigned_32SAT0.69
itc-b13-fixpoint-2UNSAT0.76
stmt31_22_328UNSAT0.77
stmt21_181_218UNSAT0.77
stmt27_149_224UNSAT0.8
rankfunc48_unsigned_16SAT0.9
stmt21_178_258UNSAT0.9
stmt41_160_235UNSAT0.9
small-seq-fixpoint-1UNSAT0.91
rankfunc56_unsigned_64SAT0.92
stmt21_71_354UNSAT0.93
query04_query42_1344nUNSAT0.95
stmt44_40_387UNSAT0.97
stmt22_6_414UNSAT0.99
cache-coherence-3-fixpoint-1UNSAT0.99
stmt21_70_369UNSAT1.01
stmt53_208_245UNSAT1.06
rankfunc56_signed_64SAT1.07
stmt21_84_364UNSAT1.07
stmt21_71_413UNSAT1.07
stmt19_3_401UNSAT1.08
query26_query42_1344nUNSAT1.14
stmt19_90_408UNSAT1.16
stmt31_190_227UNSAT1.17
stmt21_181_369UNSAT1.2
small-synabs-fixpoint-10UNSAT1.21
stmt19_83_412UNSAT1.21
stmt21_143_403UNSAT1.24
stmt19_137_408UNSAT1.25
stmt29_226_376UNSAT1.31
itc-b13-fixpoint-3SAT1.34
ntrivil_query42_1344nUNSAT1.36
ethernet-fixpoint-1UNSAT1.36
trivial_query42_1344nUNSAT1.37
sdlx-fixpoint-3UNSAT1.44
rankfunc2_unsigned_64SAT1.5
rankfunc55_unsigned_64SAT1.51
stmt22_311_370UNSAT1.57
stmt19_352_359UNSAT1.77
stmt19_313_412UNSAT1.79
small-pipeline-fixpoint-2UNSAT1.8
stmt47_290_340UNSAT1.82
cache-coherence-2-fixpoint-2UNSAT1.83
stmt41_336_385UNSAT1.86
stmt21_310_360UNSAT1.86
stmt53_296_346UNSAT1.9
itc-b13-fixpoint-4SAT1.91
rankfunc49_unsigned_64SAT2.09
sdlx-fixpoint-4UNSAT2.13
rankfunc53_signed_64SAT2.15
rankfunc49_signed_64SAT2.28
nxquery_query50_1344nSAT2.37
rankfunc53_unsigned_64SAT2.45
usb-phy-fixpoint-2UNSAT2.57
rankfunc61_unsigned_64SAT2.58
query07_query42_1344nUNSAT2.61
itc-b13-fixpoint-5SAT2.73
query27_query42_1344nUNSAT2.87
rankfunc51_signed_64SAT2.93
rankfunc51_unsigned_64SAT3
sdlx-fixpoint-5UNSAT3.01
itc-b13-fixpoint-6SAT3.03
rankfunc57_unsigned_64SAT3.09
rankfunc52_unsigned_64SAT3.18
small-pipeline-fixpoint-3UNSAT3.19
small-seq-fixpoint-2UNSAT3.29
rankfunc52_signed_64SAT3.3
rankfunc35_unsigned_64SAT3.4
cache-coherence-3-fixpoint-2UNSAT3.54
ethernet-fixpoint-2UNSAT3.68
itc-b13-fixpoint-7SAT3.85
rankfunc58_unsigned_64SAT3.91
sdlx-fixpoint-6UNSAT3.93
itc-b13-fixpoint-8SAT4.4
rankfunc61_signed_64SAT4.44
stmt46_289_388UNSAT4.52
stmt52_295_394UNSAT4.63
rankfunc58_signed_64SAT4.66
cache-coherence-2-fixpoint-4UNSAT4.91
cache-coherence-3-fixpoint-3UNSAT5.08
query03_query42_1344nUNSAT5.3
small-seq-fixpoint-3UNSAT5.42
rankfunc54_signed_64SAT5.44
itc-b13-fixpoint-9SAT5.81
rankfunc54_unsigned_64SAT6
usb-phy-fixpoint-3UNSAT6.02
sdlx-fixpoint-7SAT6.02
rankfunc35_signed_64SAT6.07
cache-coherence-2-fixpoint-5UNSAT6.21
stmt16_818_819SAT6.28
query21_query58_1344nUNSAT6.62
stmt29_275_376UNSAT6.76
sdlx-fixpoint-8SAT6.78
stmt47_340_389UNSAT6.85
itc-b13-fixpoint-10SAT6.98
rankfunc59_unsigned_64SAT6.99
stmt50_343_392UNSAT7.08
sortnetsort7.AE.stepl.009UNSAT7.09
sortnetsort7.AE.stepl.008UNSAT7.13
pi-bus-fixpoint-1UNSAT7.21
ethernet-fixpoint-3UNSAT7.38
cache-coherence-2-fixpoint-6UNSAT7.5
query21_query42_1344nUNSAT7.52
rankfunc31_unsigned_64SAT7.6
rankfunc31_signed_64SAT7.69
small-seq-fixpoint-4UNSAT7.71
sdlx-fixpoint-9SAT7.93
query33_query45_1344nSAT9.16
query31_query50_1344nSAT9.25
stmt39_285_335UNSAT9.47
sdlx-fixpoint-10SAT9.52
small-seq-fixpoint-5UNSAT10.31
rankfunc48_unsigned_64SAT10.58
rankfunc59_signed_64SAT11.06
usb-phy-fixpoint-4UNSAT11.81
stmt32_329_378UNSAT13.11
rankfunc48_signed_64SAT13.5
small-seq-fixpoint-6UNSAT14.43
ethernet-fixpoint-4UNSAT14.99
small-seq-fixpoint-7UNSAT15.41
sortnetsort8.AE.stepl.008UNSAT16.98
small-seq-fixpoint-8UNSAT17.95
rankfunc41_unsigned_64SAT18.5
query06_query42_1344nUNSAT18.79
rankfunc41_signed_64SAT19.54
usb-phy-fixpoint-5UNSAT20.12
small-seq-fixpoint-9UNSAT20.49
query08_query42_1344nUNSAT20.54
query09_query42_1344nUNSAT21.71
small-seq-fixpoint-10UNSAT22.62
stmt41_286_385UNSAT24.06
AR-fixpoint-1FAIL28.53
sortnetsort9.AE.stepl.012UNSAT48.49
query49_ntrivil_1344nSAT63.53
sortnetsort7.AE.stepl.007UNSAT64.07
stmt124_966_965SAT67.06
stmt5_731_730SAT70.48
sortnetsort9.AE.stepl.010UNSAT90.68
sortnetsort8.AE.stepl.009UNSAT93.73
stay24n.satSAT100.34
sortnetsort10.AE.stepl.011UNSAT100.47
AR-fixpoint-2FAIL102.19
query58_query42_1344nUNSAT109.74
stmt22_320_370SAT124.32
stmt21_319_418SAT125.99
sortnetsort7.AE.stepl.006UNSAT141.35
stmt19_368_417SAT162.04
query31_eequery_1344nSAT168.16
query36_query25_1344nSAT168.38
pi-bus-fixpoint-2UNSAT171.54
query50_query06_1344nSAT191.39
query52_query25_1344nSAT222.18
query04_query25_1344nSAT224.61
AR-fixpoint-4FAIL256.62
query60_query45_1344nSAT261.51
sortnetsort10.AE.stepl.012UNSAT263.73
stmt31_276_328UNSAT365.78
AR-fixpoint-6FAIL407.38
query25_query42_1344nSAT468.17
pi-bus-fixpoint-3UNSAT469.48
query45_query42_1344nSAT518.12
query05_query31_1344nSAT599.5
AR-fixpoint-8FAIL628.01
query31_reachqu_1344nSAT629.27
sortnetsort9.AE.stepl.011UNSAT702.19
AR-fixpoint-10FAIL730.52
query42_query42_1344nUNSAT764.97
query34_query11_1344nSAT838.82
eequery_query42_1344nSAT896.76
Q_2-3_v-80-100_r-11.3FAIL900
stmt17_78_98FAIL900
query54_query42_1344nFAIL900
ctrl.e#1.a#3.E#128.A#48.c#.w#3.s#26.aspFAIL900
sortnetsort9.AE.stepl.009FAIL900
Q_2-3_v-80-100_r-13.1FAIL900
query05_query42_1344nFAIL900
stmt19_65_87FAIL900
query71_query36_1344nFAIL900
ci.e#1.a#3.E#40.A#60.c#400.w#2.s#1.aspFAIL900
query42_query45_1344nFAIL900
ctrl.e#1.a#3.E#118.A#48.c#.w#5.s#7.aspFAIL900.01
query48_exquery_1344nFAIL900.01
query34_query42_1344nFAIL900.01
cycle_sched_2_10_1.satFAIL900.01
small-swap1-fixpoint-7FAIL900.01
driver_a10y.satFAIL900.01
driver_c9n.satFAIL900.01
GuidanceService2FAIL900.01
bobtuint31negFAIL900.01
mult_bool_matrix_10_9_11.satFAIL900.01
Q_2-3_v-80-100_r-13.7FAIL900.01
Q_2-3_v-80-100_r-13.6FAIL900.01
query48_query42_1344nFAIL900.01
query50_query42_1344nFAIL900.01
Q_2-3_v-80-100_r-11.6FAIL900.01
Q_2-3_v-80-100_r-11.0FAIL900.01
cycle_sched_6_7_1.satFAIL900.01
driver_d9y.satFAIL900.01
decomposition256FAIL900.01
stmt44_554_604FAIL900.01
stmt25_597_598FAIL900.01
sortnetsort10.AE.stepl.008FAIL900.01
stmt23_67_92FAIL900.01
stmt19_302_352FAIL900.01
stmt85_300_399FAIL900.01
stmt19_87_95FAIL900.01
stmt19_65_95FAIL900.01
stmt17_78_90FAIL900.01
stmt17_74_90FAIL900.01
small-equiv-fixpoint-1FAIL900.01
mult9.satFAIL900.02
Q_2-3_v-80-100_r-11.1FAIL900.02
ctrl.e#1.a#3.E#128.A#48.c#.w#9.s#60.aspFAIL900.02
ConcreteActivityServiceFAIL900.02
ci.e#1.a#3.E#40.A#60.c#408.w#2.s#1.aspFAIL900.02
query52_query42_1344nFAIL900.02
NotificationServiceImpl2FAIL900.02
sortnetsort10.AE.stepl.010FAIL900.02
stmt17_70_78FAIL900.02
ctrl.e#1.a#3.E#128.A#48.c#.w#5.s#60.aspFAIL900.02
Q_2-3_v-80-100_r-11.2FAIL900.02
Q_2-3_v-80-100_r-11.4FAIL900.02
stmt17_70_98FAIL900.02
sortnetsort9.AE.stepl.008FAIL900.02
stmt28_73_97FAIL900.02
stmt17_82_94FAIL900.02
query64_query42_1344nFAIL900.02
sortnetsort9.AE.stepl.005FAIL900.02
stmt28_68_73FAIL900.02
stmt17_62_78FAIL900.02
stmt23_66_96FAIL900.02
Q_2-3_v-80-100_r-13.4FAIL900.02
stmt17_82_98FAIL900.02
cycle_sched_12_2_1.satFAIL900.02
query71_query31_1344nFAIL900.02
small-equiv-fixpoint-5FAIL900.02
cycle_sched_4_4_2.satFAIL900.02
mult_bool_matrix_dyn_9_5.satFAIL900.02
small-swap1-fixpoint-4FAIL900.02
stmt19_79_83FAIL900.03
driver_b8n.satFAIL900.03
ceiling128FAIL900.03
small-swap1-fixpoint-6FAIL900.03
stmt25_52_53FAIL900.03
intermediate256FAIL900.03
Q_2-3_v-80-100_r-13.5FAIL900.03
small-swap1-fixpoint-9FAIL900.03
Q_2-3_v-80-100_r-13.3FAIL900.03
amba2f9n.satFAIL900.03
bs128y.satFAIL900.03
query01_query42_1344nFAIL900.03
beemskbn1f1_c0to7.satFAIL900.03
stmt19_71_95FAIL900.03
reachqu_query42_1344nFAIL900.03
query54_query58_1344nFAIL900.03
ctrl.e#1.a#3.E#134.A#48.c#.w#9.s#40.aspFAIL900.03
sortnetsort7.AE.stepl.005FAIL900.03
amba3b5y.satFAIL900.03
ctrl.e#1.a#3.E#116.A#48.c#.w#7.s#56.aspFAIL900.03
stmt23_92_96FAIL900.03
small-equiv-fixpoint-4FAIL900.03
stmt17_70_86FAIL900.03
driver_a9n.satFAIL900.04
stmt23_66_76FAIL900.04
stmt19_75_95FAIL900.04
stmt19_79_87FAIL900.04
ltl2dba_C2-8_comp4_REAL.satFAIL900.04
query55_query42_1344nFAIL900.04
mult_bool_matrix_18_18_18.satFAIL900.04
stmt28_89_97FAIL900.04
stmt23_88_92FAIL900.04
stmt19_64_91FAIL900.04
reachqu_query64_1344nFAIL900.04
query42_query06_1344nFAIL900.04
query44_query26_1344nFAIL900.04
sortnetsort10.AE.stepl.005FAIL900.04
Q_2-3_v-80-100_r-11.5FAIL900.04
query10_query45_1344nFAIL900.04
Q_2-3_v-80-100_r-11.9FAIL900.04
GuidanceServiceFAIL900.04
ctrl.e#1.a#3.E#110.A#48.c#.w#9.s#13.aspFAIL900.04
query51_query57_1344nFAIL900.04
Q_2-3_v-80-100_r-13.2FAIL900.04
cycle_sched_6_6_2.satFAIL900.04
genbuf9b4n.satFAIL900.04
ctrl.e#1.a#3.E#128.A#48.c#.w#9.s#1.aspFAIL900.04
ltl2dba_C2-6_comp3_REAL.satFAIL900.04
sortnetsort9.AE.stepl.004FAIL900.04
stmt1_79_80FAIL900.04
stmt23_66_67FAIL900.04
query64_query11_1344nFAIL900.04
ctrl.e#1.a#3.E#128.A#48.c#.w#7.s#60.aspFAIL900.05
oski3ub5i_c0to63.satFAIL900.05
ctrl.e#1.a#3.E#112.A#48.c#.w#5.s#27.aspFAIL900.05
sortnetsort8.AE.stepl.005FAIL900.05
floor128FAIL900.05
oski3ub5i_c0to255.satFAIL900.05
sortnetsort9.AE.stepl.007FAIL900.05
load_2c_comp_comp7_REAL.satFAIL900.05
driver_c9y.satFAIL900.05
mult_bool_matrix_12_13_11.satFAIL900.05
mult_bool_matrix_17_17_17.satFAIL900.05
sortnetsort8.AE.stepl.006FAIL900.05
eijkbs4863FAIL900.05
query51_query42_1344nFAIL900.05
stmt17_86_98FAIL900.05
stmt21_354_403FAIL900.05
query31_query42_1344nFAIL900.05
eequery_query64_1344nFAIL900.05
nreachq_query11_1344nFAIL900.05
ci.e#1.a#3.E#40.A#60.c#384.w#6.s#8.aspFAIL900.05
stmt17_63_70FAIL900.05
stmt9_445_446FAIL900.05
small-swap1-fixpoint-8FAIL900.05
stmt17_94_98FAIL900.05
stmt19_64_99FAIL900.05
stmt19_75_83FAIL900.05
neclaftp2002FAIL900.05
stmt17_63_78FAIL900.05
query33_query42_1344nFAIL900.05
query36_query42_1344nFAIL900.05
ci.e#1.a#3.E#40.A#60.c#288.w#6.s#2.aspFAIL900.06
Q_2-3_v-80-100_r-11.8FAIL900.06
nreachq_query54_1344nFAIL900.06
sortnetsort8.AE.stepl.004FAIL900.06
query11_query42_1344nFAIL900.06
kenflashp04FAIL900.06
query60_query44_1344nFAIL900.06
beemldelec4b1_c0to127.satFAIL900.06
Q_2-3_v-80-100_r-13.9FAIL900.06
Q_2-3_v-80-100_r-13.0FAIL900.06
intermediate128FAIL900.06
small-swap1-fixpoint-10FAIL900.06
stmt23_72_76FAIL900.06
bs128n.satFAIL900.06
stmt17_62_98FAIL900.06
sortnetsort10.AE.stepl.009FAIL900.07
ctrl.e#1.a#3.E#128.A#48.c#.w#7.s#7.aspFAIL900.07
ActivityServiceFAIL900.07
ctrl.e#1.a#3.E#124.A#48.c#.w#7.s#50.aspFAIL900.07
PhaseServiceFAIL900.07
stmt27_93_98FAIL900.07
stmt19_64_87FAIL900.07
ci.e#1.a#3.E#40.A#60.c#408.w#2.s#2.aspFAIL900.07
pdtpmsrotate32FAIL900.07
reachqu_query71_1344nFAIL900.07
oski3ub5i_c0to511.satFAIL900.07
query10_query42_1344nFAIL900.07
neclaftp4001FAIL900.07
small-swap1-fixpoint-5FAIL900.07
small-equiv-fixpoint-8FAIL900.07
stmt28_68_81FAIL900.07
6s289rb05233_c0to63.satFAIL900.07
stmt2_976_999FAIL900.07
ctrl.e#1.a#3.E#120.A#48.c#.w#3.s#3.aspFAIL900.07
Q_2-3_v-80-100_r-11.7FAIL900.07
stmt17_74_78FAIL900.07
ci.e#1.a#3.E#40.A#60.c#416.w#2.s#3.aspFAIL900.07
Q_2-3_v-80-100_r-13.8FAIL900.08
stmt41_262_275FAIL900.08
floor256FAIL900.08
query33_query51_1344nFAIL900.08
stmt28_68_69FAIL900.08
stmt17_70_90FAIL900.08
stmt17_78_94FAIL900.08
stmt17_82_86FAIL900.08
cycle_sched_4_7_1.satFAIL900.08
ActivityService2FAIL900.08
IterationServiceFAIL900.08
pdtpmsmiimFAIL900.08
kenflashp12FAIL900.08
query64_query01_1344nFAIL900.08
decomposition128FAIL900.08
stmt19_83_91FAIL900.08
add20y.satFAIL900.09
UserServiceImplFAIL900.09
small-equiv-fixpoint-2FAIL900.09
ctrl.e#1.a#3.E#128.A#48.c#.w#7.s#1.aspFAIL900.09
sortnetsort10.AE.stepl.004FAIL900.09
query33_query57_1344nFAIL900.09
IssueServiceImplFAIL900.09
eijkbs3330FAIL900.09
stmt17_63_82FAIL900.09
ceiling256FAIL900.09
stmt28_73_85FAIL900.09
small-equiv-fixpoint-3FAIL900.1
stmt17_70_82FAIL900.1
ltl2dpa_C26_comp2_REAL.satFAIL900.1
amba2c7n.satFAIL900.11