Instances solved by depqbf-v1
QBFEVAL'16 - Prenex CNF Track.

InstanceResultTime
k_ph_n-3SAT0.02
k_d4_n-1SAT0.02
tree-exa2-10UNSAT0.02
rankfunc5_signed_32SAT0.02
rankfunc17_unsigned_16SAT0.02
toilet_g_02_01.2SAT0.02
toilet_g_10_01.2SAT0.02
toilet_g_08_01.2SAT0.02
toilet_g_04_01.2SAT0.02
toilet_g_15_01.2SAT0.02
toilet_c_06_01.8UNSAT0.02
tree-exa2-20UNSAT0.02
toilet_c_04_01.4UNSAT0.02
toilet_c_08_01.7UNSAT0.02
toilet_c_08_01.6UNSAT0.02
toilet_c_06_01.4UNSAT0.02
k_d4_p-1UNSAT0.02
toilet_g_20_01.2SAT0.02
k_dum_n-1SAT0.02
k_ph_n-1SAT0.02
k_ph_n-6SAT0.02
qshifter_3SAT0.02
mutex-4-sSAT0.02
k_path_p-2UNSAT0.02
tree-exa2-25UNSAT0.02
impl08SAT0.02
k_lin_p-3UNSAT0.02
k_lin_p-2UNSAT0.02
z4ml.blif_0.10_1.00_0_0_inp_exactUNSAT0.02
impl18SAT0.02
toilet_a_08_05.2UNSAT0.02
k_dum_p-3UNSAT0.02
impl04SAT0.02
k_dum_p-2UNSAT0.02
toilet_a_04_01.4UNSAT0.02
toilet_a_06_01.6UNSAT0.02
qshifter_4SAT0.02
mutex-8-sSAT0.02
qshifter_5SAT0.02
flipflop-4-cUNSAT0.02
impl06SAT0.02
Adder2-2-cUNSAT0.02
z4ml.blif_0.10_0.20_0_0_inp_exactUNSAT0.02
s27_d3_uUNSAT0.02
z4ml.blif_0.10_0.20_0_0_out_exactUNSAT0.02
impl02SAT0.02
k_lin_p-4UNSAT0.02
z4ml.blif_0.10_0.20_0_1_inp_exactSAT0.02
tree-exa2-30UNSAT0.02
k_branch_n-2SAT0.02
C432.blif_0.10_1.00_0_1_inp_exactSAT0.02
k_poly_p-8UNSAT0.02
tree-exa2-35UNSAT0.02
z4ml.blif_0.10_1.00_0_1_inp_exactSAT0.02
toilet_a_04_01.6UNSAT0.02
toilet_a_02_10.2SAT0.02
mutex-2-sSAT0.02
tree-exa10-10SAT0.02
toilet_a_04_05.2SAT0.02
k_poly_p-4UNSAT0.02
z4ml.blif_0.10_0.20_0_1_out_exactSAT0.02
k_dum_p-4UNSAT0.02
impl14SAT0.02
tree-exa2-50UNSAT0.02
k_d4_p-4UNSAT0.02
tree-exa2-40UNSAT0.02
toilet_c_08_01.2UNSAT0.02
z4ml.blif_0.10_1.00_0_0_out_exactUNSAT0.02
C432.blif_0.10_1.00_0_1_out_exactSAT0.02
toilet_c_08_05.4SAT0.02
stmt44_107_108SAT0.02
counter_e_2SAT0.02
flipflop-3-cUNSAT0.02
tree-exa2-45UNSAT0.02
irst.dme6.B-d2SAT0.02
cube_c3_ser--opt-6_SAT0.02
adder-2-unsatUNSAT0.02
k_ph_n-4SAT0.02
k_poly_p-9UNSAT0.02
impl10SAT0.02
tree-exa10-30SAT0.02
eijk.S382.S-d4SAT0.02
aim-100-1_6-yes1-2-00SAT0.02
lognBWLARGEB0UNSAT0.02
impl16SAT0.02
k_poly_p-11UNSAT0.02
cnt02eSAT0.02
stmt1_30_31SAT0.02
stmt44_107_113SAT0.02
k_poly_p-2UNSAT0.02
k_ph_p-1UNSAT0.02
impl20SAT0.02
lognBWLARGEA0UNSAT0.02
z4ml.blif_0.10_1.00_0_1_out_exactSAT0.02
k_ph_p-3UNSAT0.02
toilet_g_06_01.2SAT0.03
k_poly_p-7UNSAT0.03
cnt01SAT0.03
query48_query15_1344UNSAT0.03
impl12SAT0.03
s27_d2_sSAT0.03
biu.mv.xl_ao.bb-b003-p020-MIF04-c05.blif-biu.inv.prop.bb-bmc.conf01.01X-QBF.BB1-Zi.BB2-01X.BB3-01X.with-IOC.unfold-001UNSAT0.03
query26_query34_1344SAT0.04
k_d4_p-7UNSAT0.04
flipflop-5-cUNSAT0.04
k_lin_n-3SAT0.04
k_d4_p-10UNSAT0.05
arbiter-07-comp-error01-qbf-hardness-depth-4UNSAT0.05
texas.parsesys^1.E-d4SAT0.05
C880.blif_0.10_1.00_0_1_inp_exactSAT0.05
lights3_035_0_002UNSAT0.05
term1.blif_0.10_0.20_0_1_out_exactSAT0.05
p5-5.pddl_planlen=6SAT0.06
biu.mv.xl_ao.bb-b003-p020-IPF03-c03.blif-biu.inv.prop.bb-bmc.conf00.01X-QBF.BB1-01X.BB2-01X.BB3-01X.with-IOC.unfold-003UNSAT0.06
lights3_035_0_027UNSAT0.06
lut4_2_fXORSAT0.07
C432.blif_0.10_0.20_0_1_inp_exactSAT0.07
vis.prodcell^01.E-d2SAT0.07
lut4_3_fANDSAT0.07
toilet_a_06_01.10UNSAT0.07
term1.blif_0.10_1.00_0_1_inp_exactSAT0.07
s298_d2_sSAT0.07
k_ph_p-5UNSAT0.07
gttt_2_2_0010_3x3_torus_wUNSAT0.07
term1.blif_0.10_0.20_0_1_inp_exactSAT0.07
s01238_PR_8_2SAT0.07
k_d4_p-17UNSAT0.07
C499.blif_0.10_1.00_0_1_out_exactSAT0.07
k_path_n-3SAT0.07
cnt05SAT0.08
k_poly_p-16UNSAT0.08
stmt21_79_304UNSAT0.08
b12_PR_9_2SAT0.08
arbiter-07-comp-error02-qbf-hardness-depth-6UNSAT0.08
biu.mv.xl_ao.bb-b001-p010-MIF01-c01.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004SAT0.08
k_d4_p-8UNSAT0.09
BLOCKS3iii.4UNSAT0.09
C880.blif_0.10_1.00_0_1_out_exactSAT0.09
par8-1-c-50UNSAT0.09
lights3_021_0_009SAT0.09
lights3_021_0_027UNSAT0.09
lights3_035_0_051UNSAT0.09
k_d4_p-11UNSAT0.09
k_dum_p-6UNSAT0.09
k_d4_n-2SAT0.1
rankfunc13_signed_32SAT0.1
aim-50-6_0-yes1-3-50UNSAT0.1
biu.mv.xl_ao.bb-b001-p005-OPF05-c02.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004SAT0.1
k_poly_p-19UNSAT0.1
s27_d4_uUNSAT0.1
biu.mv.xl_ao.bb-b001-p005-OPF05-c03.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004SAT0.1
rankfunc33_signed_32SAT0.1
p5-5.pddl_planlen=5SAT0.1
stmt19_90_266UNSAT0.1
k_dum_n-2SAT0.1
k_poly_p-14UNSAT0.1
biu.mv.xl_ao.bb-b001-p010-OPF02-c08.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003SAT0.11
ev-pr-4x4-5-3-0-0-1-lgSAT0.11
mutex-32-sSAT0.11
query01_ntrivil_1344UNSAT0.11
stmt19_217_309UNSAT0.11
k_ph_n-8SAT0.11
biu.mv.xl_ao.bb-b001-p010-MIF05-c07.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004SAT0.11
k_lin_n-5SAT0.11
BLOCKS3ii.4.3UNSAT0.11
rankfunc51_signed_32SAT0.11
incrementer-enc05-uniform-depth-2UNSAT0.11
tlc03-uniform-depth-9UNSAT0.11
C6288.blif_0.10_1.00_0_1_out_exactSAT0.11
stmt27_16_97UNSAT0.11
k_grz_n-2SAT0.11
biu.mv.xl_ao.bb-b001-p010-IPF02-c08.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003SAT0.11
tlc03-nonuniform-depth-17UNSAT0.11
Core1108_tbm_02.tex.moduleQ3.2S.000015UNSAT0.11
ev-pr-4x4-7-3-0-0-1-lgSAT0.11
aim-100-6_0-yes1-3-50SAT0.11
lut4_XOR_f1SAT0.11
flipflop-6-cUNSAT0.11
term1.blif_0.10_1.00_0_1_out_exactSAT0.11
mutex-64-sSAT0.11
k_ph_n-9SAT0.11
s05378_PR_9_2SAT0.11
lut4_XOR_fORUNSAT0.11
toilet_a_10_05.3UNSAT0.11
gttt_2_2_00101121_3x3_bUNSAT0.11
gttt_1_1_000111_3x3_torus_wUNSAT0.11
aim-200-1_6-yes1-4-90SAT0.11
k_d4_p-16UNSAT0.11
k_dum_n-3SAT0.11
k_d4_p-13UNSAT0.11
arbiter-06-comp-error02-qbf-hardness-depth-5UNSAT0.11
k_poly_n-2SAT0.11
Core1108_tbm_21.tex.module.000026UNSAT0.11
k3_1_1SAT0.12
ring_r4_ser--opt-11_UNSAT0.12
C499.blif_0.10_1.00_0_1_inp_exactSAT0.12
rewriting_k_10UNSAT0.12
k_poly_p-15UNSAT0.12
Core1108_tbm_21.tex.module.000027UNSAT0.12
toilet_c_08_01.11UNSAT0.12
biu.mv.xl_ao.bb-b003-p020-MIF04-c05.blif-biu.inv.prop.bb-bmc.conf05.01X-QBF.BB1-Zi.BB2-01X.BB3-Zi.with-IOC.unfold-003UNSAT0.12
mutex-16-sSAT0.13
k_path_p-5UNSAT0.21
connect_5x4_3_DUNSAT0.21
k_lin_p-9UNSAT0.21
biu.mv.xl_ao.bb-b001-p010-MIF04-c06.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-005SAT0.21
incrementer-enc03-nonuniform-depth-13UNSAT0.21
connect_6x5_5_DUNSAT0.21
ken.flash^10.C-f2UNSAT0.21
stmt19_3_214UNSAT0.21
jnh212-50UNSAT0.21
BLOCKS3iii.5SAT0.21
toilet_a_08_05.9SAT0.21
k_branch_n-3SAT0.21
gttt_2_1_000111_3x3_torus_bSAT0.21
rewriting_k_30UNSAT0.21
gttt_2_1_0010_4x4_torus_bUNSAT0.21
vonNeumann-ripple-carry-5-cUNSAT0.21
s09234_PR_8_2SAT0.21
k_d4_p-20UNSAT0.21
s09234_PR_8_5SAT0.21
k_lin_p-8UNSAT0.21
k_grz_n-4SAT0.21
tlc03-uniform-depth-21UNSAT0.21
ev-pr-4x4-9-3-0-0-1-lgSAT0.21
flipflop-7-cUNSAT0.21
ev-pr-4x4-11-3-0-0-1-lgSAT0.21
C432.blif_0.10_1.00_0_0_inp_exactUNSAT0.31
ii32b1-00SAT0.31
ev-pr-4x4-13-3-0-0-1-lgSAT0.31
k_path_n-4SAT0.31
ev-pr-4x4-15-3-0-0-1-lgSAT0.31
mutex-128-sSAT0.31
p10-10.pddl_planlen=6UNSAT0.31
k_grz_n-5SAT0.31
ev-pr-8x8-5-7-0-1-2-lgUNSAT0.31
k_lin_p-10UNSAT0.31
ken.flash^03.C-f3UNSAT0.31
b20_PR_7_90UNSAT0.31
k_d4_n-3SAT0.31
query21_ntrivil_1344UNSAT0.31
c4_BMC_p1_k32SAT0.31
stmt29_226_376UNSAT0.41
rewriting_k_17UNSAT0.41
ev-pr-4x4-17-3-0-0-1-lgSAT0.41
connect_7x6_4_WUNSAT0.41
ken.flash^10.C-f3UNSAT0.41
gttt_1_1_001020_3x3_wUNSAT0.41
vonNeumann-ripple-carry-6-cUNSAT0.41
s15850_PR_2_2SAT0.41
b20_PR_7_20SAT0.41
k_dum_p-12UNSAT0.41
driverlog01_7SAT0.41
flipflop-8-cUNSAT0.41
s15850_PR_8_50SAT0.51
k_lin_p-11UNSAT0.51
Umbrella_tbm_25.tex.moduleQ3.2S.000075UNSAT0.51
tlc03-uniform-depth-52UNSAT0.51
k_ph_n-11SAT0.51
ev-pr-6x6-5-5-0-1-2-lgUNSAT0.51
rewriting_k_19UNSAT0.51
toilet_c_10_01.12UNSAT0.51
k_grz_p-4UNSAT0.61
k_lin_p-12UNSAT0.61
CHAIN12v.13SAT0.61
BLOCKS3ii.5.2UNSAT0.61
rewriting_k_21UNSAT0.61
connect_8x7_7_WUNSAT0.61
k_grz_n-6SAT0.61
incrementer-enc07-nonuniform-depth-17UNSAT0.61
k_lin_p-14UNSAT0.71
tlc01-uniform-depth-73UNSAT0.71
sortnetsort5.v.stepl.004UNSAT0.71
vonNeumann-ripple-carry-7-cUNSAT0.71
k_grz_p-5UNSAT0.71
k_grz_n-7SAT0.71
flipflop-9-cUNSAT0.71
rewriting_k_25UNSAT0.81
k_grz_n-8SAT0.81
k_lin_n-6SAT0.81
rewriting_k_23UNSAT0.81
incrementer-enc07-nonuniform-depth-21UNSAT0.81
term1.blif_0.10_1.00_0_0_inp_exactUNSAT0.81
s05378_PR_1_75UNSAT0.91
lut4_AND_f1SAT0.91
szymanski-5-sUNSAT1.02
C5315.blif_0.10_1.00_0_1_out_exactSAT1.02
vis.4-arbit^2.E-f2SAT1.02
s27_d5_uUNSAT1.12
par8-4-50UNSAT1.12
vonNeumann-ripple-carry-8-cUNSAT1.12
ring_r3_ser--opt-8_SAT1.21
toilet_a_08_01.13UNSAT1.22
k_dum_p-14UNSAT1.31
ev-pr-4x4-5-3-0-0-1-sSAT1.31
C499.blif_0.10_0.20_0_1_inp_exactSAT1.31
flipflop-10-cUNSAT1.41
k_dum_n-5SAT1.41
k_lin_p-19UNSAT1.51
tlc04-nonuniform-depth-56UNSAT1.51
k_lin_n-7SAT1.51
term1.blif_0.10_1.00_0_0_out_exactUNSAT1.71
rewriting_k_50UNSAT1.71
vonNeumann-ripple-carry-9-cUNSAT1.71
sortnetsort7.v.stepl.007SAT1.81
driverlog03_7SAT1.81
texas.two_proc^4.E-f2SAT2.01
lognBWLARGEA1UNSAT2.22
BLOCKS3ii.5.3SAT2.22
k_ph_n-14SAT2.31
vonNeumann-ripple-carry-10-cUNSAT2.41
term1.blif_0.10_0.20_0_0_out_exactUNSAT2.51
fpu-10Xh-error01-uniform-depth-5UNSAT2.61
CHAIN14v.15SAT2.71
ev-pr-8x8-7-7-0-1-2-lgUNSAT2.71
ev-pr-6x6-7-5-0-1-2-lgUNSAT2.71
k_path_n-5SAT2.81
flipflop-11-cUNSAT2.81
C5315.blif_0.10_1.00_0_1_inp_exactSAT2.81
fpu-10Xe-correct01-nonuniform-depth-6UNSAT2.91
p10-10.pddl_planlen=10SAT2.91
k_lin_n-8SAT2.91
biu.mv.xl_ao.bb-b003-p020-MIF04-c05.blif-biu.inv.prop.bb-bmc.conf03.01X-QBF.BB1-Zi.BB2-Zi.BB3-01X.with-IOC.unfold-005UNSAT3.01
cnt10SAT3.11
incrementer-enc02-nonuniform-depth-31UNSAT3.11
vonNeumann-ripple-carry-11-cUNSAT3.22
biu.mv.xl_ao.bb-b003-p020-IPF02-c05.blif-biu.inv.prop.bb-bmc.conf01.01X-QBF.BB1-Zi.BB2-01X.BB3-01X.with-IOC.unfold-005UNSAT3.22
C499.blif_0.10_1.00_0_0_inp_exactUNSAT3.32
dungeon_i10-m5-u10-v0.pddl_planlen=23UNSAT3.51
fpu-10Xh-correct04-uniform-depth-8UNSAT3.61
rewriting_k_75UNSAT3.71
k_t4p_n-2SAT3.71
gttt_2_2_001020_4x4_wUNSAT3.81
nusmv.tcas^6.B-f4SAT4.01
k_lin_n-9SAT4.01
c4_BMC_p2_k128UNSAT4.01
stmt52_244_394UNSAT4.21
vonNeumann-ripple-carry-12-cUNSAT4.52
k_dum_p-16UNSAT4.91
k_lin_n-11SAT5.52
sortnetsort8.v.stepl.009SAT6.11
vonNeumann-ripple-carry-13-cUNSAT6.11
CHAIN16v.17SAT6.12
query11_query21_1344UNSAT6.21
fpu-10Xh-correct04-uniform-depth-14UNSAT6.21
k_ph_n-16SAT6.31
arbiter-10-comp-error01-qbf-hardness-depth-10UNSAT6.41
k_grz_n-10SAT6.41
k_branch_n-4SAT6.52
rewriting_k_100UNSAT6.62
fpu-10Xh-correct04-uniform-depth-15UNSAT6.62
flipflop-12-cUNSAT6.71
stmt17_18_19SAT7.01
fpu-10Xh-correct04-uniform-depth-16UNSAT7.11
C5315.blif_0.10_1.00_0_0_inp_exactUNSAT7.31
query51_query50_1344UNSAT7.31
k_lin_n-15SAT7.41
c1_BMC_p2_k512UNSAT7.72
fpu-10Xh-correct04-nonuniform-depth-18UNSAT7.72
lognBWLARGEB1UNSAT7.72
tlc02-uniform-depth-114UNSAT8.01
arbiter-07-comp-error01-qbf-hardness-depth-11UNSAT8.21
incrementer-enc03-nonuniform-depth-24UNSAT8.31
k_grz_p-12UNSAT8.41
k_grz_p-10UNSAT8.51
k_grz_p-11UNSAT8.51
k_grz_p-13UNSAT9.11
fpu-10Xe-correct01-uniform-depth-22UNSAT9.61
connect_5x4_4_RUNSAT9.71
arbiter-06-comp-error01-qbf-hardness-depth-12UNSAT9.82
fpu-10Xe-correct01-nonuniform-depth-24UNSAT9.92
p20-20.pddl_planlen=23SAT10.11
ev-pr-4x4-7-3-0-0-1-sSAT10.31
BLOCKS4iii.6UNSAT10.41
vonNeumann-ripple-carry-15-cUNSAT10.51
term1.blif_0.10_0.20_0_0_inp_exactUNSAT10.71
fpu-10Xh-correct04-nonuniform-depth-27UNSAT11.41
k_lin_n-14SAT11.41
dungeon_i10-m10-u10-v0.pddl_planlen=187UNSAT11.61
dungeon_i10-m5-u10-v0.pddl_planlen=134UNSAT12.12
BLOCKS3i.5.4SAT12.41
k_dum_p-17UNSAT13.51
szymanski-6-sUNSAT14.01
k_path_n-6SAT14.22
cube_c7_ser--opt-24_SAT14.61
ev-pr-6x6-9-5-0-1-2-lgUNSAT14.71
c1_BMC_p2_k1024UNSAT15.32
test5_quant_squaring4SAT15.42
CHAIN17v.18SAT15.81
emptyroom_e3_ser--opt-20_SAT16.42
ev-pr-8x8-9-7-0-1-2-lgUNSAT16.81
CHAIN18v.19SAT17.72
k_t4p_p-4UNSAT17.81
incrementer-enc08-uniform-depth-33SAT18.21
lut4_2_f1SAT18.51
Umbrella_tbm_24.tex.module.000131SAT18.82
tlc04-nonuniform-depth-98UNSAT20.41
test5_quant_squaring5SAT23.02
biu.mv.xl_ao.bb-b003-p020-IPF01-c05.blif-biu.inv.prop.bb-bmc.conf04.01X-QBF.BB1-01X.BB2-01X.BB3-Zi.with-IOC.unfold-008UNSAT23.41
k_lin_n-17SAT24.12
Umbrella_tbm_24.tex.module.000066SAT26.21
sortnetsort8.AE.stepl.003SAT28.11
ev-pr-6x6-19-5-0-1-2-sFAIL28.55
tlc02-uniform-depth-241UNSAT29.11
ev-pr-6x6-17-5-0-1-2-sFAIL29.47
ev-pr-6x6-11-5-0-1-2-sFAIL30.14
ev-pr-6x6-15-5-0-1-2-sFAIL30.15
ev-pr-6x6-13-5-0-1-2-sFAIL30.25
k_ph_n-21SAT30.72
s510_d31_sFAIL31.35
s510_d32_sFAIL31.55
s510_d28_sFAIL32.55
connect_5x4_3_RUNSAT33.11
BLOCKS3i.5.3UNSAT33.91
s1269_d13_uFAIL34.25
s1269_d12_uFAIL36.16
s1269_d14_uFAIL36.45
s510_d35_sFAIL36.65
s3330_d5_sFAIL36.76
c2_BMC_p1_k2048SAT37.42
cube_c9_par--opt-11_SAT37.61
gttt_2_1_00102030_4x4_torus_bUNSAT37.91
s510_d36_sFAIL38.27
ev-pr-4x4-9-3-0-0-1-sSAT38.31
cnt11SAT39.62
s1269_d15_uFAIL40.65
s3330_d9_sFAIL41.05
s3330_d10_uFAIL41.95
ev-pr-6x6-5-5-0-1-2-sUNSAT44.81
par16-1-50UNSAT45.81
k_dum_p-20UNSAT46.71
CHAIN19v.20SAT46.71
k_grz_p-17UNSAT46.81
biu.mv.xl_ao.bb-b003-p020-MIF04-c05.blif-biu.inv.prop.bb-bmc.conf07.01X-QBF.BB1-Zi.BB2-Zi.BB3-Zi.with-IOC.unfold-007UNSAT48.71
k_grz_p-16UNSAT49.42
s3330_d12_uFAIL50.25
s3330_d7_sFAIL50.85
test3_quant_squaring2UNSAT51.31
CHAIN20v.21SAT51.82
Core1108_tbm_03.tex.moduleQ3.2S.000002UNSAT52.91
ev-pr-6x6-11-5-0-1-2-lgUNSAT53.21
C432.blif_0.10_1.00_0_0_out_exactUNSAT55.51
s3330_d14_uFAIL58.95
s3330_d8_sFAIL61.15
ev-pr-8x8-11-7-0-1-2-lgUNSAT62.21
c1_BMC_p1_k4SAT62.72
C432.blif_0.10_0.20_0_0_inp_exactUNSAT77.02
k_branch_p-5UNSAT85.11
sortnetsort8.v.stepl.007SAT86.31
k_grz_p-18UNSAT120.81
k_grz_p-19UNSAT122.41
CHAIN21v.22SAT148.31
gttt_2_1_00011020_4x4_bUNSAT148.81
k_dum_p-21UNSAT154.71
ev-pr-6x6-7-5-0-1-2-sUNSAT154.81
lut4_2_f2UNSAT161.72
CHAIN22v.23SAT162.91
ev-pr-4x4-11-3-0-0-1-sSAT168.01
BLOCKS4ii.7.2UNSAT177.91
k_grz_n-18SAT189.41
k_grz_n-21SAT205.01
k_grz_n-20SAT207.83
dungeon_i25-m12-u5-v0.pddl_planlen=65UNSAT227.91
lut4_AND_fXORUNSAT230.11
biu.mv.xl_ao.bb-b003-p020-IPF03-c03.blif-biu.inv.prop.bb-bmc.with-IOC.unfold-009UNSAT239.61
stmt41_160_235UNSAT298.31
ev-pr-6x6-13-5-0-1-2-lgUNSAT300.01
toilet_c_10_01.17UNSAT310.41
stmt19_83_412UNSAT351.41
ev-pr-8x8-13-7-0-1-2-lgUNSAT352.02
c1_Debug_s3_f1_e1_v1FAIL367.45
arbiter-06-comp-error01-qbf-hardness-depth-15UNSAT382.11
Core1108_tbm_21.tex.module.000030SAT402.11
b22_PR_8_20SAT416.21
CHAIN23v.24SAT485.31
biu.mv.xl_ao.bb-b001-p010-IPF02-c07.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003SAT503.91
Core1108_tbm_21.tex.module.000008SAT587.42
C499.blif_0.10_0.20_0_0_inp_exactUNSAT587.61
qshifter_8FAIL591.32
s713_d9_uFAIL591.32
c4_Debug_s3_f1_e1_v2FAIL591.42
szymanski-18-sFAIL591.52
stmt17_62_98FAIL591.62
AR-fixpoint-5FAIL591.62
input_pnpi8042_moudep.cFAIL591.62
s713_d7_uFAIL591.62
hid_hclient_ecdisp.cFAIL591.74
k_ph_p-18FAIL591.75
k_ph_p-19FAIL591.75
s641_d8_uFAIL591.75
s499_d12_sFAIL591.75
s298_d14_sFAIL591.75
c4_Debug_s3_f1_e2_v3FAIL591.75
k_branch_n-20FAIL591.75
stmt17_86_98FAIL591.84
s510_d11_sFAIL591.84
qshifter_7FAIL591.84
s298_d22_uFAIL591.84
s499_d15_sFAIL591.84
kernel_agplib_intrface.cFAIL591.85
c4_Debug_s3_f1_e2_v2FAIL591.85
szymanski-14-sFAIL591.85
s1196_d5_uFAIL591.85
c5_BMC_p1_k32FAIL591.85
s499_d25_uFAIL591.92
k_branch_p-18FAIL591.92
s713_d6_sFAIL591.92
ev-pr-4x4-17-3-0-0-1-sFAIL591.92
s386_d12_uFAIL591.92
sdlx-fixpoint-3FAIL591.92
szymanski-16-sFAIL591.93
c5_BMC_p2_k128FAIL591.93
biu.mv.xl_ao.bb-b003-p020-IPF03-c03.blif-biu.inv.prop.bb-bmc.conf07.01X-QBF.BB1-Zi.BB2-Zi.BB3-Zi.with-IOC.unfold-008FAIL592.02
biu.mv.xl_ao.bb-b003-p020-MIF04-c05.blif-biu.inv.prop.bb-bmc.conf07.01X-QBF.BB1-Zi.BB2-Zi.BB3-Zi.with-IOC.unfold-010FAIL592.02
c5_BMC_p2_k64FAIL592.02
c4_Debug_s5_f2_e2_v1FAIL592.02
s820_d14_uFAIL592.02
s1269_d9_sFAIL592.02
connect_9x8_6_RFAIL592.02
s499_d22_uFAIL592.02
s298_d19_uFAIL592.03
s713_d5_sFAIL592.03
k8_2_3FAIL592.12
k8_4_3FAIL592.12
k8_3_4FAIL592.12
s1269_d10_sFAIL592.12
c4_Debug_s3_f2_e2_v2FAIL592.12
ev-pr-8x8-19-7-0-1-2-lgFAIL592.12
s1269_d8_sFAIL592.12
s820_d7_sFAIL592.12
s499_d17_sFAIL592.12
connect_8x7_4_RFAIL592.12
incrementer-enc07-uniform-depth-25FAIL592.12
s713_d8_uFAIL592.12
k_branch_p-16FAIL592.12
s820_d12_uFAIL592.12
s1196_d4_uFAIL592.12
s298_d17_sFAIL592.12
c2_Debug_s3_f2_e1_v3FAIL592.12
eijk.bs4863.S-d4FAIL592.13
s1269_d5_sFAIL592.13
s713_d11_uFAIL592.22
cache-coherence-2-fixpoint-6FAIL592.22
network_irda_miniport_nscirda_settings.cFAIL592.22
cache-coherence-3-fixpoint-3FAIL592.22
ev-pr-6x6-17-5-0-1-2-lgFAIL592.22
query42_query06_1344nFAIL592.22
s298_d25_uFAIL592.22
c2_Debug_s3_f1_e1_v2FAIL592.22
stmt19_64_99FAIL592.22
stmt23_72_76FAIL592.22
stmt28_68_81FAIL592.22
texas.PI_main^05.E-f3FAIL592.22
s820_d9_sFAIL592.22
connect_8x7_5_RFAIL592.22
s820_d11_uFAIL592.22
s641_d7_uFAIL592.22
s499_d19_sFAIL592.22
szymanski-20-sFAIL592.22
s820_d10_sFAIL592.22
ev-pr-6x6-19-5-0-1-2-lgFAIL592.22
szymanski-12-sFAIL592.22
nusmv.reactor^3.C-d4FAIL592.22
filesys_smbmrx_cvsndrcv.cFAIL592.23
k_branch_p-14FAIL592.23
s298_d12_sFAIL592.32
k_branch_p-21FAIL592.32
stmt17_63_82FAIL592.32
szymanski-24-sFAIL592.32
stmt17_70_90FAIL592.32
s641_d10_uFAIL592.32
s510_d23_sFAIL592.32
s510_d24_sFAIL592.32
s386_d9_uFAIL592.32
ken.oop^2.C-d3FAIL592.32
ev-pr-4x4-13-3-0-0-1-sFAIL592.32
k_branch_n-16FAIL592.32
texas.PI_main^08.E-f3FAIL592.32
ev-pr-8x8-17-7-0-1-2-lgFAIL592.32
c1_Debug_s5_f1_e1_v2FAIL592.32
ev-pr-8x8-15-7-0-1-2-lgFAIL592.32
s3330_d2_sFAIL592.32
ken.oop^2.C-d4FAIL592.32
c3_BMC_p1_k256FAIL592.33
szymanski-10-sFAIL592.33
p20-5.pddl_planlen=17FAIL592.34
s499_d24_uFAIL592.42
k12_4_2FAIL592.42
stmt21_319_418FAIL592.42
s499_d9_sFAIL592.42
Adder2-16-sFAIL592.42
k_ph_p-13FAIL592.42
stmt23_66_96FAIL592.42
C6288.blif_0.10_1.00_0_1_inp_exactFAIL592.42
arbiter-10-comp-error01-qbf-hardness-depth-22FAIL592.42
stmt17_70_98FAIL592.42
s641_d6_sFAIL592.42
s3330_d4_sFAIL592.42
s713_d10_uFAIL592.42
C6288.blif_0.10_1.00_0_0_inp_exactFAIL592.42
ken.flash^08.C-d4FAIL592.42
rankfunc3_signed_64FAIL592.42
incrementer-enc06-uniform-depth-24FAIL592.42
sortnetsort9.AE.stepl.012FAIL592.42
input_mouser_cseries.cFAIL592.42
s298_d18_sFAIL592.42
s641_d5_sFAIL592.42
s641_d11_uFAIL592.42
s820_d15_uFAIL592.42
s3330_d3_sFAIL592.42
s386_d11_uFAIL592.42
s386_d10_uFAIL592.42
Adder2-8-cFAIL592.42
s1196_d6_uFAIL592.42
k_branch_p-11FAIL592.43
ev-pr-6x6-15-5-0-1-2-lgFAIL592.43
network_irda_miniport_nscirda_comm.cFAIL592.52
k_path_p-19FAIL592.52
k_ph_p-10FAIL592.52
k8_3_2FAIL592.52
k14_2_3FAIL592.52
tlc04-uniform-depth-36FAIL592.52
C6288.blif_0.10_0.20_0_1_inp_exactFAIL592.52
connect_8x7_6_RFAIL592.52
test2_quant_squaring2FAIL592.52
c3_Debug_s3_f2_e2_v2FAIL592.52
depots03_9FAIL592.52
nusmv.tcas^3.B-f2FAIL592.52
sortnetsort9.AE.stepl.009FAIL592.52
incrementer-enc02-uniform-depth-58FAIL592.53
k_path_p-21FAIL592.62
rankfunc14_signed_64FAIL592.62
rankfunc5_unsigned_64FAIL592.62
s298_d10_sFAIL592.62
cnt07eFAIL592.62
s386_d7_sFAIL592.62
s1196_d7_uFAIL592.62
s1269_d3_sFAIL592.62
k_t4p_p-12FAIL592.62
stmt17_82_98FAIL592.62
k_path_p-13FAIL592.62
network_trans_sys_notify.cFAIL592.62
s386_d2_sFAIL592.62
s386_d8_uFAIL592.62
C5315.blif_0.10_0.20_0_0_inp_exactFAIL592.62
s820_d8_sFAIL592.62
dungeon_i25-m12-u3-v0.pddl_planlen=190FAIL592.62
small-seq-fixpoint-5FAIL592.62
k_dum_n-12FAIL592.63
test2_quant_squaring3FAIL592.63
k_t4p_p-16FAIL592.63
k_ph_p-20FAIL592.72
adder-12-unsatFAIL592.72
k_d4_n-7FAIL592.72
k_d4_n-20FAIL592.72
rankfunc22_signed_64FAIL592.72
Umbrella_tbm_05.tex.module.000039FAIL592.72
C5315.blif_0.10_0.20_0_1_inp_exactFAIL592.72
query03_query25_1344FAIL592.72
s713_d4_sFAIL592.72
dungeon_i25-m12-u3-v0.pddl_planlen=72FAIL592.72
gttt_1_1_00101121_4x4_torus_wFAIL592.72
test3_quant_squaring4FAIL592.73
audio_ddksynth_csynth2.cppFAIL592.73
k_t4p_p-18FAIL592.73
s1269_d4_sFAIL592.83
s510_d3_sFAIL592.83
sortnetsort10.v.stepl.005FAIL592.83
small-synabs-fixpoint-9FAIL592.83
k_branch_n-9FAIL592.83
C880.blif_0.10_0.20_0_0_out_exactFAIL592.83
arbiter-07-comp-error01-qbf-hardness-depth-20FAIL592.84
ev-pr-4x4-15-3-0-0-1-sFAIL592.84
k_path_n-19FAIL592.84
k_branch_p-12FAIL592.84
C6288.blif_0.10_0.20_0_0_inp_exactFAIL592.84
s499_d18_sFAIL592.84
dungeon_i15-m7-u4-v0.pddl_planlen=81FAIL592.84
dungeon_i25-m12-u3-v0.pddl_planlen=130FAIL592.84
k_ph_p-15FAIL592.84
s1196_d3_uFAIL592.84
driverlog10_6FAIL592.85
s641_d4_sFAIL592.85
s510_d6_sFAIL592.85
s386_d6_sFAIL592.93
k_poly_n-5FAIL592.93
adder-10-satFAIL592.93
C880.blif_0.10_1.00_0_0_out_exactFAIL592.94
BLOCKS4i.6.4FAIL592.94
k_path_n-9FAIL592.94
nusmv.tcas-t^1.B-d2FAIL592.94
Adder2-10-sFAIL592.94
k_dum_n-11FAIL592.94
ev-pr-6x6-9-5-0-1-2-sFAIL592.94
emptyroom_e4_par---21_FAIL592.94
uclid-pipe3bFAIL592.94
s386_d4_sFAIL592.94
k_t4p_n-4FAIL592.94
C5315.blif_0.10_1.00_0_0_out_exactFAIL592.95
k_branch_p-8FAIL592.95
k_branch_p-10FAIL592.95
sortnetsort9.v.stepl.005FAIL592.95
k_ph_p-12FAIL593.02
dungeon_i25-m12-u5-v0.pddl_planlen=170FAIL593.02
k_branch_n-12FAIL593.02
network_ndis_rtlnwifi_hw_hw_ccmp.cFAIL593.02
k_poly_n-14FAIL593.02
k_poly_n-6FAIL593.02
k_dum_n-17FAIL593.02
test1_quant_squaring2FAIL593.03
small-swap1-fixpoint-3FAIL593.03
k_dum_n-9FAIL593.12
pipesnotankage14_10FAIL593.12
k_t4p_p-6FAIL593.12
small-seq-fixpoint-3FAIL593.12
k_t4p_p-15FAIL593.12
k_path_n-14FAIL593.12
k5_3_2FAIL593.12
k_d4_n-10FAIL593.12
f600-50FAIL593.12
p20-1.pddl_planlen=26FAIL593.12
p20-5.pddl_planlen=32FAIL593.12
k_t4p_p-10FAIL593.12
C432.blif_0.10_0.20_0_0_out_exactFAIL593.12
test4_quant_squaring4FAIL593.12
emptyroom_e4_ser--opt-44_FAIL593.22
cnt08eFAIL593.22
k_path_p-15FAIL593.22
s641_d3_sFAIL593.22
C5315.blif_0.10_0.20_0_1_out_exactFAIL593.22
k_d4_n-16FAIL593.22
k_branch_n-8FAIL593.22
C499.blif_0.10_0.20_0_1_out_exactFAIL593.22
qshifter_6FAIL593.22
k_t4p_n-15FAIL593.23
k_t4p_n-12FAIL593.23
small-swap2-fixpoint-4FAIL593.23
s713_d3_sFAIL593.23
k_poly_n-16FAIL593.32
s499_d7_sFAIL593.32
b20_C_3_2FAIL593.32
C6288.blif_0.10_0.20_0_1_out_exactFAIL593.32
pipesnotankage18_7FAIL593.32
k_branch_n-10FAIL593.32
rankfunc13_unsigned_64FAIL593.32
adder-12-satFAIL593.32
k_dum_n-21FAIL593.32
biu.mv.xl_ao.bb-b001-p010-IPF05-c07.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003FAIL593.32
k_t4p_p-20FAIL593.32
k_path_n-12FAIL593.32
s1196_d2_sFAIL593.32
k_branch_p-6FAIL593.32
C432.blif_0.10_0.20_0_1_out_exactFAIL593.33
cnt16rFAIL593.42
dungeon_i25-m12-u3-v0.pddl_planlen=165FAIL593.42
s641_d2_sFAIL593.42
k_t4p_p-9FAIL593.42
k_poly_n-20FAIL593.42
k_t4p_n-8FAIL593.42
C6288.blif_0.10_0.20_0_0_out_exactFAIL593.42
stmt41_738_749FAIL593.42
k_path_p-14FAIL593.42
k_t4p_n-6FAIL593.42
C880.blif_0.10_0.20_0_0_inp_exactFAIL593.42
b21_C_3_206FAIL593.42
C880.blif_0.10_0.20_0_1_inp_exactFAIL593.42
k_path_n-16FAIL593.42
s713_d2_sFAIL593.42
query44_query26_1344nFAIL593.42
p20-1.pddl_planlen=32FAIL593.42
s820_d3_sFAIL593.42
k_dum_n-18FAIL593.42
Adder2-8-sFAIL593.42
C499.blif_0.10_0.20_0_0_out_exactFAIL593.43
k_path_n-13FAIL593.43
pipesnotankage18_8FAIL593.52
texas.PI_main^16.E-f2FAIL593.52
k_t4p_p-17FAIL593.52
C880.blif_0.10_0.20_0_1_out_exactFAIL593.52
C6288.blif_0.10_1.00_0_0_out_exactFAIL593.52
adder-14-satFAIL593.52
cache-coherence-2-fixpoint-1FAIL593.52
k_t4p_n-14FAIL593.52
k_d4_n-14FAIL593.52
k_t4p_n-5FAIL593.52
k_poly_n-17FAIL593.52
k_poly_n-7FAIL593.52
k_d4_n-15FAIL593.52
C880.blif_0.10_1.00_0_0_inp_exactFAIL593.52
b22_C_2_12FAIL593.52
k_t4p_n-13FAIL593.52
s298_d4_sFAIL593.52
uclid-pipe3aFAIL593.52
stmt25_52_53FAIL593.52
s820_d2_sFAIL593.52
C5315.blif_0.10_0.20_0_0_out_exactFAIL593.52
test4_quant_squaring2FAIL593.52
k_branch_n-11FAIL593.52
s1196_1_5FAIL593.53
test1_quant_squaring3FAIL593.53
k_path_p-16FAIL593.62
szymanski-8-sFAIL593.62
k_path_p-18FAIL593.62
arbiter-08-comp-error02-qbf-hardness-depth-9FAIL593.62
cube_c11_par---13_FAIL593.62
k6_2_3FAIL593.62
s386_d3_sFAIL593.62
k_d4_n-8FAIL593.62
stmt44_916_917FAIL593.62
k_t4p_n-9FAIL593.62
uclid-pipe2FAIL593.62
stmt27_296_297FAIL593.62
k_poly_n-21FAIL593.63
biu.mv.xl_ao.bb-b001-p005-OPF03-c09.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003FAIL593.72
sortnetsort9.v.stepl.007FAIL593.72
C499.blif_0.10_1.00_0_0_out_exactFAIL593.72
k_poly_n-18FAIL593.72
k_path_p-10FAIL593.72
stmt24_765_766FAIL593.72
query31_reachqu_1344nFAIL593.72
p20-1.pddl_planlen=24FAIL593.73
stmt16_950_951FAIL593.82
k5_2_3FAIL593.82
cnt14FAIL593.82
emptyroom_e3_ser---19_FAIL593.82