Instances solved by Qute_hybrid
QBFEVAL'17 - Prenex non-CNF Track

InstanceResultTime
halfadder_match2.unsatUNSAT0
mvs16y.unsatUNSAT0.01
halfadder_match2.satSAT0.01
mutex-4-sSAT0.01
szymanski-5-sUNSAT0.04
mutex-32-sSAT0.07
mvs16y.satSAT0.09
CHAIN20v.21SAT0.09
szymanski-6-sUNSAT0.11
stay24n.unsatUNSAT0.12
CHAIN22v.23SAT0.12
assertion12_0_1UNSAT0.14
CHAIN23v.24SAT0.14
mutex-64-sSAT0.15
ci.e#1.a#3.E#40.A#60.c#208.w#6.s#8.aspSAT0.17
stay24n.satSAT0.36
k_ph_n-21SAT0.4
BLOCKS4iii.6UNSAT0.45
Core1108_tbm_02.tex.moduleQ3.2S.000015UNSAT0.47
szymanski-8-sUNSAT0.53
consistency_0_1SAT0.56
driver_d9y.unsatUNSAT0.74
possibility8_0_1SAT0.98
possibility10_0_1UNSAT1.12
beemldelec4b1_c0to127.unsatUNSAT1.37
oski3ub5i_c0to255.unsatUNSAT1.68
SR-unsat-03-01-07-1UNSAT1.99
driver_d9y.satSAT2.09
consistency_0_2SAT2.54
possibility5_0_1UNSAT3.5
assertion12_0_2SAT3.51
ci.e#1.a#3.E#40.A#60.c#424.w#2.s#1.aspUNSAT3.65
klieber2017q-104-26-t1UNSAT3.71
b20_PR_7_20SAT4.16
ci.e#1.a#3.E#40.A#60.c#432.w#2.s#8.aspUNSAT5.22
possibility6_0_3UNSAT6.34
consistency_0_3SAT6.42
fpu-10Xe-correct01-nonuniform-depth-24UNSAT6.69
fpu-10Xh-correct04-nonuniform-depth-27UNSAT7.83
assertion6_0_3UNSAT8.36
incrementer-enc07-uniform-depth-25UNSAT10.6
filesys_smbmrx_cvsndrcv.cUNSAT12
szymanski-14-sUNSAT13.62
DW-unsat-08-21-1UNSAT14.38
ci.e#1.a#3.E#40.A#60.c#400.w#2.s#1.aspUNSAT16.17
consistency_0_4SAT16.41
assertion1_0_4SAT16.59
ci.e#1.a#3.E#40.A#60.c#416.w#2.s#3.aspUNSAT20.27
vonNeumann-ripple-carry-12-cUNSAT22.83
klieber2017q-108-27-t1UNSAT23.42
klieber2017q-092-23-t1UNSAT27.91
klieber2017q-078-19-t1UNSAT30.9
b22_PR_8_20SAT31.78
possibility7_0_3SAT38.52
klieber2017q-084-21-t1UNSAT39.6
klieber2017q-076-19-t1UNSAT39.7
szymanski-16-sUNSAT50.61
consistency_0_5SAT51.08
DW-unsat-09-23-1UNSAT56.92
JP-unsat-02-07-2UNSAT61.4
uclid-pipe3aSAT67.08
consistency_0_6SAT69.33
assertion10_0_6SAT73.52
possibility6_0_7UNSAT79.72
ltl2dba_C2-6_comp3_REAL.unsatUNSAT80.13
uclid-pipe2SAT92.56
ev-pr-4x4-13-3-0-0-1-lgSAT92.65
consistency_0_7SAT105.12
consistency_0_8SAT139.6
assertion9_0_3SAT154.87
ev-pr-4x4-11-3-0-0-1-lgSAT192.51
C6288.blif_0.10_0.20_0_1_out_exactSAT196.18
klieber2017q-088-22-t1UNSAT196.54
assertion1_0_9SAT264.22
consistency_0_9SAT303.89
consistency_0_10SAT359.71
possibility6_0_10UNSAT363.1
amba2f9n.unsatUNSAT443.42
DW-unsat-09-22-1UNSAT456.7
SR-unsat-04-01-08-1UNSAT460.68
assertion7_0_3UNSAT472.58
klieber2017q-080-20-t1UNSAT485.04
assertion10_0_9SAT522.57
dungeon_i15-m7-u4-v0.pddl_planlen=81UNSAT529.27
k_branch_p-11UNSAT541.68
s15850_PR_8_50SAT545.77
klieber2017q-112-28-t1UNSAT565.88
CM-sat-07-01-07-3SAT569.33
stmt41_160_235UNSAT597.79
cnt14SAT614.9
ci.e#1.a#3.E#40.A#60.c#200.w#6.s#6.aspSAT653.45
rankfunc17_unsigned_16FAIL754.22
test3_quant_squaring2UNSAT793.36
k_branch_p-10UNSAT796.45
possibility1_0_3SAT813.34
SR-sat-03-01-08-2FAIL852.84
klieber2017q-116-29-t1FAIL854.9
f600-50FAIL855.62
klieber2017q-086-21-t1FAIL856.31
DW-sat-08-22-1SAT862.42
c1_Debug_s5_f1_e1_v2FAIL875.55
DW-sat-08-23-1FAIL875.61
possibility4_0_7FAIL875.72
ev-pr-6x6-9-5-0-1-2-sFAIL875.81
ev-pr-6x6-17-5-0-1-2-sFAIL875.81
ev-pr-4x4-13-3-0-0-1-sFAIL875.92
CM-unsat-07-01-05-3FAIL875.93
SR-sat-04-01-08-2FAIL875.95
DW-unsat-19-43-1FAIL875.95
c4_Debug_s3_f2_e2_v2FAIL876.07
connect_9x8_6_RFAIL876.16
assertion2_0_8FAIL876.23
k12_4_2FAIL876.31
CM-unsat-08-01-05-3FAIL876.31
CM-sat-17-01-07-3FAIL876.32
ev-pr-6x6-9-5-0-1-2-lgFAIL876.32
b20_C_3_2FAIL876.33
query42_query06_1344nFAIL876.33
dungeon_i25-m12-u3-v0.pddl_planlen=190FAIL876.34
DWs-unsat-12-25-1FAIL876.34
c3_Debug_s3_f2_e2_v2FAIL876.36
CM-unsat-18-01-05-3FAIL876.41
ev-pr-6x6-11-5-0-1-2-sFAIL876.41
ev-pr-8x8-7-7-0-1-2-lgFAIL876.41
ev-pr-8x8-13-7-0-1-2-lgFAIL876.41
ev-pr-6x6-19-5-0-1-2-lgFAIL876.42
pipesnotankage14_10FAIL876.42
JP-sat-03-09-5FAIL876.49
ev-pr-6x6-17-5-0-1-2-lgFAIL876.51
cnt16rFAIL876.52
DWs-unsat-11-24-1FAIL876.52
cycle_sched_4_7_1.unsatFAIL876.53
connect_8x7_6_RFAIL876.53
ev-pr-6x6-11-5-0-1-2-lgFAIL876.59
network_ndis_rtlnwifi_hw_hw_ccmp.cFAIL876.61
JP-unsat-03-07-4FAIL876.61
pipesnotankage18_8FAIL876.63
assertion1_0_10FAIL876.63
CM-sat-17-01-06-4FAIL876.64
p20-20.pddl_planlen=23FAIL876.67
ltl2dba_C2-6_comp3_REAL.satFAIL876.71
load_full_4_comp3_REAL.unsatFAIL876.73
mult_bool_matrix_17_17_17.unsatFAIL876.73
ev-pr-4x4-17-3-0-0-1-sFAIL876.74
s1269_d15_uFAIL876.81
ev-pr-4x4-7-3-0-0-1-sFAIL876.82
s3330_d12_uFAIL876.82
CM-unsat-17-01-06-2FAIL876.82
s3330_d9_sFAIL876.82
load_3c_comp_comp7_REAL.satFAIL876.82
dungeon_i25-m12-u3-v0.pddl_planlen=165FAIL876.84
p20-5.pddl_planlen=32FAIL876.89
SR-sat-03-01-07-3FAIL876.89
SR-unsat-04-01-07-2FAIL876.91
ltl2dpa_C26_comp2_REAL.satFAIL876.92
possibility5_0_9FAIL876.93
DW-sat-08-24-1FAIL876.93
p20-1.pddl_planlen=24FAIL876.94
c4_Debug_s5_f2_e2_v1FAIL876.95
c2_BMC_p1_k2048FAIL876.97
cycle_sched_4_7_1.satFAIL877
possibility3_0_6FAIL877.01
sortnetsort9.AE.stepl.012FAIL877.01
CM-sat-07-01-06-3FAIL877.01
amba2f9n.satFAIL877.01
oski3ub5i_c0to255.satFAIL877.02
possibility10_0_7FAIL877.02
c2_Debug_s3_f1_e1_v2FAIL877.05
ev-pr-6x6-13-5-0-1-2-sFAIL877.08
load_full_4_comp3_REAL.satFAIL877.09
CM-unsat-17-01-05-3FAIL877.1
ci.e#1.a#3.E#40.A#60.c#312.w#2.s#3.aspFAIL877.11
k_branch_n-10FAIL877.11
adder-14-satFAIL877.11
c5_BMC_p2_k128FAIL877.11
cycle_sched_6_7_1.satFAIL877.11
possibility3_0_3FAIL877.12
b21_C_3_206FAIL877.12
qshifter_8FAIL877.12
load_3c_comp_comp7_REAL.unsatFAIL877.15
stmt19_64_99FAIL877.2
beemldelec4b1_c0to127.satFAIL877.21
amba4b9y.satFAIL877.21
ci.e#1.a#3.E#40.A#60.c#280.w#6.s#7.aspFAIL877.21
assertion11_0_7FAIL877.21
stmt16_950_951FAIL877.21
s1269_d13_uFAIL877.21
possibility1_0_8FAIL877.21
CM-sat-07-01-06-4FAIL877.21
DW-unsat-20-44-1FAIL877.22
stmt17_63_82FAIL877.22
amba4b9y.unsatFAIL877.22
DWs-unsat-11-23-1FAIL877.22
ev-pr-8x8-15-7-0-1-2-lgFAIL877.23
DW-sat-19-45-1FAIL877.25
assertion4_0_10FAIL877.26
possibility11_0_7FAIL877.3
s1269_d12_uFAIL877.31
JP-sat-03-09-4FAIL877.31
possibility5_0_4FAIL877.31
stmt28_68_81FAIL877.31
arbiter-08-comp-error02-qbf-hardness-depth-9FAIL877.31
Adder2-16-sFAIL877.32
stmt17_86_98FAIL877.32
ci.e#1.a#3.E#40.A#60.c#264.w#4.s#2.aspFAIL877.32
ci.e#1.a#3.E#40.A#60.c#296.w#6.s#7.aspFAIL877.38
possibility10_0_2FAIL877.41
CM-sat-17-01-06-3FAIL877.41
k14_2_3FAIL877.42
ci.e#1.a#3.E#40.A#60.c#288.w#4.s#8.aspFAIL877.42
k_branch_p-16FAIL877.5
DWs-sat-10-24-1FAIL877.51
ci.e#1.a#3.E#40.A#60.c#304.w#4.s#7.aspFAIL877.51
query44_query26_1344nFAIL877.52
k_ph_p-19FAIL877.52
DWs-sat-10-23-1FAIL877.6
genbuf10b4n.satFAIL877.61
input_pnpi8042_moudep.cFAIL877.62
incrementer-enc02-uniform-depth-58FAIL877.62
DW-unsat-19-42-1FAIL877.62
arbiter-10-comp-error01-qbf-hardness-depth-22FAIL877.62
DW-sat-19-46-1FAIL877.68
network_irda_miniport_nscirda_comm.cFAIL877.7
qshifter_7FAIL877.71
mult_bool_matrix_17_17_17.satFAIL877.72
sortnetsort9.v.stepl.005FAIL877.72
k_branch_n-12FAIL877.72
assertion9_0_7FAIL877.72
possibility8_0_7FAIL877.72
stmt41_738_749FAIL877.81
ci.e#1.a#3.E#40.A#60.c#376.w#2.s#4.aspFAIL877.81
ci.e#1.a#3.E#40.A#60.c#320.w#4.s#8.aspFAIL877.81
adder-10-satFAIL877.81
ken.flash^08.C-d4FAIL877.81
stmt17_70_90FAIL877.81
mult_bool_matrix_10_9_11.satFAIL877.82
possibility7_0_6FAIL877.82
assertion2_0_6FAIL877.82
ci.e#1.a#3.E#40.A#60.c#344.w#4.s#5.aspFAIL877.87
test2_quant_squaring2FAIL877.91
CM-unsat-07-01-06-2FAIL877.91
adder-12-unsatFAIL877.91
genbuf9b4n.satFAIL877.92
small-swap2-fixpoint-4FAIL877.99
C6288.blif_0.10_0.20_0_0_inp_exactFAIL878
JP-unsat-02-06-3FAIL878.01
possibility4_0_5FAIL878.01
ci.e#1.a#3.E#40.A#60.c#304.w#6.s#8.aspFAIL878.01
test3_quant_squaring4FAIL878.01
ring_r6_ser--opt-17_FAIL878.08
c5_BMC_p2_k64FAIL878.11
audio_ddksynth_csynth2.cppFAIL878.11
ci.e#1.a#3.E#40.A#60.c#336.w#4.s#5.aspFAIL878.12
driver_a9n.unsatFAIL878.21
small-synabs-fixpoint-9FAIL878.22
rankfunc5_unsigned_64FAIL878.22
test1_quant_squaring3FAIL878.22
rankfunc33_signed_32FAIL878.3
cycle_sched_6_7_1.unsatFAIL878.31
small-swap1-fixpoint-3FAIL878.31
k8_2_3FAIL878.32
ltl2dpa_C26_comp2_REAL.unsatFAIL878.41
rankfunc14_signed_64FAIL878.41
Umbrella_tbm_05.tex.module.000039FAIL878.42
incrementer-enc08-uniform-depth-33FAIL878.42
sdlx-fixpoint-3FAIL878.42
driver_a9n.satFAIL878.5
ci.e#1.a#3.E#40.A#60.c#384.w#6.s#8.aspFAIL878.5
cache-coherence-2-fixpoint-6FAIL878.6
C5315.blif_0.10_0.20_0_0_out_exactFAIL878.61
assertion2_0_3FAIL878.62
JP-sat-03-08-5FAIL878.69
ken.oop^2.C-d4FAIL878.7
k_ph_p-12FAIL878.71
ci.e#1.a#3.E#40.A#60.c#392.w#6.s#4.aspFAIL878.71
ev-pr-8x8-19-7-0-1-2-lgFAIL878.71
rankfunc13_unsigned_64FAIL878.71
C880.blif_0.10_0.20_0_1_inp_exactFAIL878.72
ev-pr-4x4-15-3-0-0-1-sFAIL878.72
test2_quant_squaring3FAIL878.81
sortnetsort9.v.stepl.007FAIL878.91
genbuf9b4n.unsatFAIL878.92
genbuf10b4n.unsatFAIL878.92
assertion5_0_9FAIL878.92
k5_2_3FAIL878.92
DWs-sat-10-25-1FAIL879
mult_bool_matrix_10_9_11.unsatFAIL879.02
ci.e#1.a#3.E#40.A#60.c#408.w#4.s#3.aspFAIL879.06
C880.blif_0.10_1.00_0_0_inp_exactFAIL879.1
klieber2017q-100-25-eqFAIL879.11
C499.blif_0.10_0.20_0_0_out_exactFAIL879.21
klieber2017q-092-23-eqFAIL879.21
klieber2017q-084-21-eqFAIL879.22
klieber2017q-078-19-eqFAIL879.31
cube_c7_ser--opt-24_FAIL879.32
C6288.blif_0.10_1.00_0_0_out_exactFAIL879.32
DW-sat-19-44-1FAIL879.48
klieber2017q-096-24-t1FAIL879.51
klieber2017q-088-22-eqFAIL879.51
assertion2_0_5FAIL879.52
C6288.blif_0.10_0.20_0_0_out_exactFAIL879.61
C499.blif_0.10_0.20_0_1_out_exactFAIL879.62
emptyroom_e4_ser--opt-44_FAIL879.62
klieber2017q-096-24-eqFAIL879.67
klieber2017q-076-19-eqFAIL879.7
klieber2017q-108-27-eqFAIL879.71
klieber2017q-074-18-eqFAIL879.72
klieber2017q-082-20-eqFAIL879.8
klieber2017q-082-20-t1FAIL879.8
klieber2017q-086-21-eqFAIL879.81
sortnetsort10.v.stepl.005FAIL879.81
klieber2017q-104-26-eqFAIL879.84
klieber2017q-112-28-eqFAIL879.92
klieber2017q-080-20-eqFAIL879.98
C499.blif_0.10_1.00_0_0_out_exactFAIL879.99
assertion3_0_6FAIL880.01
klieber2017q-116-29-eqFAIL880.04
klieber2017q-074-18-t1FAIL880.2
klieber2017q-100-25-t1FAIL881.62
assertion7_0_4FAIL883.84