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

InstanceResultTime
rankfunc61_signed_64SAT0
stmt46_289_388UNSAT0
stmt22_6_414UNSAT0
stmt21_178_258UNSAT0
stmt21_181_369UNSAT0
usb-phy-fixpoint-2UNSAT0
stmt21_310_360UNSAT0
stmt41_160_235UNSAT0
cache-coherence-2-fixpoint-6UNSAT0
stmt46_111_238UNSAT0
stmt21_143_403UNSAT0
stmt19_83_412UNSAT0
rankfunc2_unsigned_64SAT0
rankfunc56_signed_64SAT0
rankfunc48_signed_64SAT0
rankfunc58_unsigned_64SAT0
stmt29_275_376UNSAT0
stmt32_329_378UNSAT0
stmt19_133_217UNSAT0
stmt21_84_364UNSAT0
stmt31_22_328UNSAT0
stmt41_336_385UNSAT0
sdlx-fixpoint-6UNSAT0
stmt21_71_413UNSAT0
sdlx-fixpoint-5UNSAT0
stmt39_285_335UNSAT0
stmt44_40_387UNSAT0
stmt19_66_214UNSAT0
stmt22_311_370UNSAT0
stmt41_286_385UNSAT0
stmt19_3_401UNSAT0
stmt27_149_224UNSAT0
stmt21_70_369UNSAT0
stmt31_276_328UNSAT0
stmt19_90_408UNSAT0
itc-b13-fixpoint-6SAT0
stmt19_137_408UNSAT0
stmt27_16_224UNSAT0
stmt21_71_354UNSAT0
cache-coherence-2-fixpoint-5UNSAT0
stmt19_313_412UNSAT0
stmt29_226_376UNSAT0
small-seq-fixpoint-3UNSAT0
usb-phy-fixpoint-3UNSAT0
small-synabs-fixpoint-10UNSAT0
itc-b13-fixpoint-3SAT0
small-pipeline-fixpoint-1UNSAT0
rankfunc31_signed_64SAT0
rankfunc35_signed_64SAT0
rankfunc53_unsigned_64SAT0
rankfunc52_signed_64SAT0
cache-coherence-3-fixpoint-3UNSAT0
usb-phy-fixpoint-4UNSAT0
itc-b13-fixpoint-5SAT0
usb-phy-fixpoint-1UNSAT0
small-seq-fixpoint-7UNSAT0
sdlx-fixpoint-4UNSAT0
small-seq-fixpoint-8UNSAT0
itc-b13-fixpoint-4SAT0
itc-b13-fixpoint-2UNSAT0
small-seq-fixpoint-4UNSAT0
cache-coherence-2-fixpoint-2UNSAT0
rankfunc51_unsigned_64SAT0
rankfunc41_signed_64SAT0
rankfunc49_unsigned_64SAT0
rankfunc51_signed_64SAT0
rankfunc59_unsigned_64SAT0
rankfunc49_signed_64SAT0
rankfunc54_unsigned_64SAT0
rankfunc48_unsigned_16SAT0
rankfunc31_unsigned_64SAT0
rankfunc48_unsigned_64SAT0
rankfunc54_signed_64SAT0
rankfunc58_signed_64SAT0
rankfunc61_unsigned_64SAT0
rankfunc56_unsigned_64SAT0
rankfunc55_unsigned_64SAT0
rankfunc57_unsigned_64SAT0
rankfunc59_signed_64SAT0
rankfunc53_signed_64SAT0
rankfunc60_unsigned_32SAT0
rankfunc35_unsigned_64SAT0
rankfunc52_unsigned_64SAT0
rankfunc41_unsigned_64SAT0
add20y.satSAT0
small-synabs-fixpoint-3UNSAT0
ethernet-fixpoint-4UNSAT0
itc-b13-fixpoint-8SAT0
ethernet-fixpoint-1UNSAT0
usb-phy-fixpoint-5UNSAT0
itc-b13-fixpoint-10SAT0
cache-coherence-2-fixpoint-4UNSAT0
cache-coherence-3-fixpoint-1UNSAT0
ethernet-fixpoint-2UNSAT0
itc-b13-fixpoint-9SAT0
ethernet-fixpoint-3UNSAT0
small-pipeline-fixpoint-2UNSAT0
small-pipeline-fixpoint-3UNSAT0
small-seq-fixpoint-5UNSAT0
small-seq-fixpoint-2UNSAT0
GuidanceService2UNSAT0
GuidanceServiceUNSAT0
kenflashp04SAT0
floor128SAT0
neclaftp4001UNSAT0
floor256SAT0
trivial_query42_1344nUNSAT0
query07_query42_1344nUNSAT0
ntrivil_query42_1344nUNSAT0
exquery_query42_1344nUNSAT0
Q_2-3_v-80-100_r-13.4UNSAT0
Q_2-3_v-80-100_r-13.0UNSAT0
small-seq-fixpoint-1UNSAT0
stmt44_554_604SAT0
stmt27_93_98SAT0
cache-coherence-3-fixpoint-2UNSAT0
itc-b13-fixpoint-1UNSAT0
pi-bus-fixpoint-1UNSAT0
stmt1_79_80SAT0
stmt9_445_446SAT0
stmt41_262_275SAT0
stmt5_731_730SAT0
stmt25_52_53SAT0
stmt16_818_819SAT0
stmt19_352_359UNSAT0
itc-b13-fixpoint-7SAT0
stmt47_290_340UNSAT0
stmt124_966_965SAT0
small-seq-fixpoint-6UNSAT0
stmt25_597_598SAT0
sdlx-fixpoint-3UNSAT0
stmt2_976_999SAT0.51
small-seq-fixpoint-9UNSAT0.58
stmt53_296_346UNSAT0.58
stmt47_340_389UNSAT0.59
stmt52_295_394UNSAT0.61
small-seq-fixpoint-10UNSAT0.61
pi-bus-fixpoint-2UNSAT0.79
pdtpmsmiimSAT0.85
pdtpmsrotate32SAT0.9
stmt50_343_392UNSAT1
kenflashp12SAT1.08
pi-bus-fixpoint-3UNSAT1.22
AR-fixpoint-1UNSAT1.33
sortnetsort7.AE.stepl.007UNSAT1.6
sortnetsort8.AE.stepl.004SAT1.86
sortnetsort7.AE.stepl.008UNSAT1.9
stmt23_66_67SAT2.1
sortnetsort7.AE.stepl.009UNSAT2.21
stmt21_181_218UNSAT2.28
stmt17_63_70SAT2.44
stmt23_66_76SAT2.5
stmt28_68_69SAT2.58
stmt28_68_73SAT2.8
stmt17_63_78SAT2.88
stmt23_72_76SAT3.01
stmt17_62_78SAT3.02
stmt17_63_82SAT3.18
stmt17_70_78SAT3.2
stmt28_68_81SAT3.3
sdlx-fixpoint-8SAT3.3
stmt19_65_87SAT3.33
stmt19_64_87SAT3.36
stmt17_74_78SAT3.37
stmt17_70_82SAT3.51
stmt19_75_83SAT3.72
stmt28_73_85SAT3.74
stmt19_64_91SAT3.77
mult9.satSAT3.8
stmt23_67_92SAT3.85
stmt19_79_83SAT3.88
ceiling128SAT3.89
sortnetsort9.AE.stepl.004SAT3.91
AR-fixpoint-2UNSAT3.93
sdlx-fixpoint-7SAT3.94
stmt17_70_86SAT3.95
stmt17_74_90SAT4.07
stmt19_65_95SAT4.1
stmt19_79_87SAT4.1
stmt23_66_96SAT4.14
stmt17_70_90SAT4.14
stmt19_64_99SAT4.16
stmt19_71_95SAT4.33
stmt19_75_95SAT4.45
stmt17_82_86SAT4.5
stmt17_78_90SAT4.5
stmt19_83_91SAT4.51
stmt17_62_98SAT4.55
stmt17_78_94SAT4.6
stmt28_73_97SAT4.7
stmt23_88_92SAT4.81
stmt17_78_98SAT4.88
stmt17_70_98SAT4.9
stmt17_82_94SAT5.11
stmt23_92_96SAT5.28
stmt17_86_98SAT5.35
stmt19_87_95SAT5.38
stmt17_82_98SAT5.44
nxquery_query42_1344nUNSAT5.63
sortnetsort10.AE.stepl.004SAT5.67
stmt28_89_97SAT5.77
stmt17_94_98SAT6.08
sdlx-fixpoint-9SAT6.6
bs128n.satSAT7.37
bs128y.satSAT7.73
query02_query44_1344nUNSAT8.89
sdlx-fixpoint-10SAT9.02
eijkbs3330SAT10.16
sortnetsort8.AE.stepl.009UNSAT10.25
AR-fixpoint-4UNSAT12.27
sortnetsort9.AE.stepl.011UNSAT13.84
query27_query42_1344nUNSAT14.08
sortnetsort7.AE.stepl.006UNSAT15.27
sortnetsort8.AE.stepl.008UNSAT15.72
sortnetsort10.AE.stepl.011UNSAT15.9
ltl2dba_C2-6_comp3_REAL.satSAT16.56
stmt31_190_227UNSAT18.01
sortnetsort9.AE.stepl.012UNSAT18.78
Q_2-3_v-80-100_r-13.1UNSAT18.81
AR-fixpoint-6UNSAT19.83
stmt53_208_245UNSAT20.05
ceiling256SAT20.36
sortnetsort7.AE.stepl.005SAT21.21
Q_2-3_v-80-100_r-13.3UNSAT27.61
mult_bool_matrix_10_9_11.satSAT29.92
AR-fixpoint-8UNSAT32.28
sortnetsort9.AE.stepl.010UNSAT34.78
AR-fixpoint-10UNSAT38.78
sortnetsort8.AE.stepl.005SAT39.8
query08_query42_1344nUNSAT47.69
Q_2-3_v-80-100_r-13.6UNSAT54.09
ltl2dba_C2-8_comp4_REAL.satSAT54.78
stay24n.satSAT55.14
small-swap1-fixpoint-4SAT59.08
Q_2-3_v-80-100_r-13.7UNSAT67.05
sortnetsort9.AE.stepl.005SAT69.88
sortnetsort9.AE.stepl.009UNSAT70.39
driver_c9y.satSAT78.54
mult_bool_matrix_12_13_11.satSAT90.41
sortnetsort8.AE.stepl.006UNSAT90.82
driver_d9y.satSAT116.79
axquery_query42_1344nUNSAT119.67
sortnetsort10.AE.stepl.005SAT152.89
stmt22_320_370SAT173.07
Q_2-3_v-80-100_r-13.9UNSAT183.52
stmt21_319_418SAT194.86
decomposition128SAT206.72
stmt19_368_417SAT222.78
sortnetsort10.AE.stepl.012UNSAT271.23
query03_query42_1344nUNSAT305.95
small-swap1-fixpoint-7SAT323.11
driver_c9n.satSAT330.48
Q_2-3_v-80-100_r-13.2UNSAT370.86
driver_a10y.satSAT502.77
stmt19_302_352SAT540.99
stmt85_300_399SAT546.65
small-swap1-fixpoint-8SAT560.1
small-swap1-fixpoint-6SAT631.07
driver_b8n.satSAT652.87
query02_query42_1344nUNSAT710.91
mult_bool_matrix_dyn_9_5.satSAT752.87
stmt21_354_403SAT793.7
small-swap1-fixpoint-9SAT860.11
oski3ub5i_c0to255.satFAIL900
Q_2-3_v-80-100_r-11.8FAIL900
ci.e#1.a#3.E#40.A#60.c#400.w#2.s#1.aspFAIL900
driver_a9n.satFAIL900
ctrl.e#1.a#3.E#118.A#48.c#.w#5.s#7.aspFAIL900
genbuf9b4n.satFAIL900
query51_query57_1344nFAIL900
beemskbn1f1_c0to7.satFAIL900.01
bobtuint31negFAIL900.01
sortnetsort10.AE.stepl.009FAIL900.01
ctrl.e#1.a#3.E#128.A#48.c#.w#5.s#60.aspFAIL900.01
query54_query42_1344nFAIL900.01
NotificationServiceImpl2FAIL900.01
ctrl.e#1.a#3.E#128.A#48.c#.w#7.s#60.aspFAIL900.01
intermediate128FAIL900.01
reachqu_query71_1344nFAIL900.01
reachqu_query42_1344nFAIL900.01
query31_query42_1344nFAIL900.01
query26_query42_1344nFAIL900.01
query09_query42_1344nFAIL900.01
sortnetsort9.AE.stepl.007FAIL900.01
query04_query42_1344nFAIL900.01
oski3ub5i_c0to63.satFAIL900.01
UserServiceImplFAIL900.01
query54_query58_1344nFAIL900.01
query31_query50_1344nFAIL900.01
ci.e#1.a#3.E#40.A#60.c#384.w#6.s#8.aspFAIL900.01
Q_2-3_v-80-100_r-11.7FAIL900.01
nxquery_query50_1344nFAIL900.01
small-swap1-fixpoint-5FAIL900.01
ci.e#1.a#3.E#40.A#60.c#408.w#2.s#2.aspFAIL900.01
query31_reachqu_1344nFAIL900.02
query60_query44_1344nFAIL900.02
query33_query42_1344nFAIL900.02
decomposition256FAIL900.02
cycle_sched_12_2_1.satFAIL900.02
ci.e#1.a#3.E#40.A#60.c#408.w#2.s#1.aspFAIL900.02
query51_query42_1344nFAIL900.02
query10_query45_1344nFAIL900.02
query05_query31_1344nFAIL900.02
mult_bool_matrix_17_17_17.satFAIL900.02
small-equiv-fixpoint-5FAIL900.02
ctrl.e#1.a#3.E#134.A#48.c#.w#9.s#40.aspFAIL900.02
ConcreteActivityServiceFAIL900.02
sortnetsort10.AE.stepl.008FAIL900.03
ctrl.e#1.a#3.E#124.A#48.c#.w#7.s#50.aspFAIL900.03
sortnetsort10.AE.stepl.010FAIL900.03
query42_query42_1344nFAIL900.03
query33_query45_1344nFAIL900.03
query64_query11_1344nFAIL900.03
IssueServiceImplFAIL900.03
query60_query45_1344nFAIL900.03
cycle_sched_4_7_1.satFAIL900.03
query05_query42_1344nFAIL900.03
sortnetsort9.AE.stepl.008FAIL900.03
query44_query26_1344nFAIL900.03
Q_2-3_v-80-100_r-13.8FAIL900.03
small-equiv-fixpoint-2FAIL900.03
Q_2-3_v-80-100_r-11.9FAIL900.03
Q_2-3_v-80-100_r-11.6FAIL900.03
oski3ub5i_c0to511.satFAIL900.03
query64_query01_1344nFAIL900.04
load_2c_comp_comp7_REAL.satFAIL900.04
cycle_sched_6_7_1.satFAIL900.04
query52_query25_1344nFAIL900.04
query50_query06_1344nFAIL900.04
Q_2-3_v-80-100_r-11.3FAIL900.04
Q_2-3_v-80-100_r-11.5FAIL900.04
neclaftp2002FAIL900.04
IterationServiceFAIL900.04
ctrl.e#1.a#3.E#128.A#48.c#.w#7.s#7.aspFAIL900.04
ctrl.e#1.a#3.E#112.A#48.c#.w#5.s#27.aspFAIL900.04
amba3b5y.satFAIL900.04
query71_query36_1344nFAIL900.04
ctrl.e#1.a#3.E#128.A#48.c#.w#3.s#26.aspFAIL900.05
amba2c7n.satFAIL900.05
query36_query25_1344nFAIL900.05
ctrl.e#1.a#3.E#120.A#48.c#.w#3.s#3.aspFAIL900.05
small-equiv-fixpoint-4FAIL900.05
beemldelec4b1_c0to127.satFAIL900.05
ci.e#1.a#3.E#40.A#60.c#416.w#2.s#3.aspFAIL900.05
Q_2-3_v-80-100_r-11.0FAIL900.05
eequery_query64_1344nFAIL900.05
cycle_sched_2_10_1.satFAIL900.06
cycle_sched_4_4_2.satFAIL900.06
nreachq_query11_1344nFAIL900.06
ctrl.e#1.a#3.E#128.A#48.c#.w#7.s#1.aspFAIL900.06
PhaseServiceFAIL900.06
eijkbs4863FAIL900.06
amba2f9n.satFAIL900.06
query06_query42_1344nFAIL900.06
Q_2-3_v-80-100_r-11.4FAIL900.06
Q_2-3_v-80-100_r-11.1FAIL900.06
ci.e#1.a#3.E#40.A#60.c#288.w#6.s#2.aspFAIL900.06
query50_query42_1344nFAIL900.06
Q_2-3_v-80-100_r-13.5FAIL900.06
query71_query31_1344nFAIL900.07
reachqu_query64_1344nFAIL900.07
query64_query42_1344nFAIL900.07
query58_query42_1344nFAIL900.07
query10_query42_1344nFAIL900.07
small-equiv-fixpoint-1FAIL900.07
ctrl.e#1.a#3.E#128.A#48.c#.w#9.s#60.aspFAIL900.07
small-equiv-fixpoint-3FAIL900.07
ctrl.e#1.a#3.E#128.A#48.c#.w#9.s#1.aspFAIL900.07
query01_query42_1344nFAIL900.07
query33_query57_1344nFAIL900.07
query34_query11_1344nFAIL900.07
query36_query42_1344nFAIL900.07
query48_exquery_1344nFAIL900.07
ActivityServiceFAIL900.07
query49_ntrivil_1344nFAIL900.07
query45_query42_1344nFAIL900.07
ctrl.e#1.a#3.E#110.A#48.c#.w#9.s#13.aspFAIL900.07
query25_query42_1344nFAIL900.08
query42_query06_1344nFAIL900.08
query21_query42_1344nFAIL900.08
small-equiv-fixpoint-8FAIL900.08
Q_2-3_v-80-100_r-11.2FAIL900.08
query34_query42_1344nFAIL900.08
ctrl.e#1.a#3.E#116.A#48.c#.w#7.s#56.aspFAIL900.08
nreachq_query54_1344nFAIL900.08
query52_query42_1344nFAIL900.08
query42_query45_1344nFAIL900.08
query48_query42_1344nFAIL900.08
ActivityService2FAIL900.08
mult_bool_matrix_18_18_18.satFAIL900.09
ltl2dpa_C26_comp2_REAL.satFAIL900.09
6s289rb05233_c0to63.satFAIL900.09
query11_query42_1344nFAIL900.09
query04_query25_1344nFAIL900.09
query55_query42_1344nFAIL900.09
small-swap1-fixpoint-10FAIL900.09
query21_query58_1344nFAIL900.09
cycle_sched_6_6_2.satFAIL900.09
query31_eequery_1344nFAIL900.09
eequery_query42_1344nFAIL900.1
intermediate256FAIL900.11
query33_query51_1344nFAIL900.17