Instances solved by xb-bid-qsts
QBFEVAL'16 - Prenex CNF Track.

InstanceResultTime
tree-exa2-20UNSAT0
tree-exa2-30UNSAT0
tree-exa2-10UNSAT0
toilet_g_06_01.2SAT0.01
rewriting_k_10UNSAT0.01
ring_r4_ser--opt-11_UNSAT0.01
toilet_a_02_10.2SAT0.01
toilet_a_04_05.2SAT0.01
rewriting_k_17UNSAT0.01
stmt44_107_113SAT0.01
rewriting_k_19UNSAT0.01
impl14SAT0.01
impl16SAT0.01
k_ph_n-1SAT0.01
rewriting_k_21UNSAT0.01
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.01
cnt01SAT0.01
lognBWLARGEB0UNSAT0.01
impl04SAT0.01
impl12SAT0.01
qshifter_3SAT0.01
tree-exa2-25UNSAT0.01
lognBWLARGEA0UNSAT0.01
impl08SAT0.01
stmt44_107_108SAT0.01
toilet_c_04_01.4UNSAT0.01
toilet_g_15_01.2SAT0.01
toilet_g_20_01.2SAT0.01
toilet_g_04_01.2SAT0.01
impl18SAT0.01
toilet_g_08_01.2SAT0.01
toilet_g_10_01.2SAT0.01
toilet_g_02_01.2SAT0.01
toilet_c_08_01.2UNSAT0.01
cnt02eSAT0.01
s27_d2_sSAT0.01
impl10SAT0.01
k_ph_n-3SAT0.01
qshifter_4SAT0.01
stmt1_30_31SAT0.01
tree-exa10-30SAT0.01
tree-exa2-35UNSAT0.01
toilet_a_04_01.4UNSAT0.01
impl20SAT0.01
impl02SAT0.01
flipflop-3-cUNSAT0.01
k_d4_p-1UNSAT0.01
impl06SAT0.01
k_ph_p-1UNSAT0.01
tree-exa2-45UNSAT0.01
mutex-2-sSAT0.01
rewriting_k_23UNSAT0.01
k_ph_p-3UNSAT0.01
tree-exa2-50UNSAT0.01
k_d4_n-1SAT0.01
rewriting_k_25UNSAT0.01
tree-exa10-10SAT0.01
tree-exa2-40UNSAT0.01
k_path_p-2UNSAT0.02
k_poly_n-2SAT0.02
counter_e_2SAT0.02
toilet_c_06_01.4UNSAT0.02
adder-2-unsatUNSAT0.02
k_poly_p-2UNSAT0.02
rewriting_k_50UNSAT0.02
toilet_a_04_01.6UNSAT0.02
k_dum_n-1SAT0.02
k_ph_n-4SAT0.02
z4ml.blif_0.10_1.00_0_1_inp_exactSAT0.02
rewriting_k_30UNSAT0.02
z4ml.blif_0.10_1.00_0_0_inp_exactUNSAT0.02
k_dum_p-3UNSAT0.03
k_dum_n-3SAT0.03
k_lin_p-2UNSAT0.03
k_ph_p-5UNSAT0.03
toilet_a_06_01.6UNSAT0.03
k_dum_p-2UNSAT0.03
z4ml.blif_0.10_0.20_0_1_inp_exactSAT0.03
aim-100-1_6-yes1-2-00SAT0.03
rewriting_k_75UNSAT0.03
mutex-4-sSAT0.03
k_dum_n-2SAT0.03
z4ml.blif_0.10_1.00_0_1_out_exactSAT0.03
k_branch_n-2SAT0.04
stmt17_18_19SAT0.04
k_poly_n-6SAT0.04
k_dum_n-5SAT0.04
k3_1_1SAT0.04
k_poly_p-4UNSAT0.04
s27_d3_uUNSAT0.04
incrementer-enc05-uniform-depth-2UNSAT0.04
z4ml.blif_0.10_0.20_0_1_out_exactSAT0.04
k_poly_n-5SAT0.04
qshifter_5SAT0.04
toilet_c_06_01.8UNSAT0.04
k_dum_p-4UNSAT0.04
toilet_c_08_01.6UNSAT0.04
Adder2-2-cUNSAT0.04
z4ml.blif_0.10_0.20_0_0_out_exactUNSAT0.04
z4ml.blif_0.10_0.20_0_0_inp_exactUNSAT0.04
z4ml.blif_0.10_1.00_0_0_out_exactUNSAT0.04
k_path_n-3SAT0.05
s298_d2_sSAT0.05
k_ph_n-6SAT0.05
rewriting_k_100UNSAT0.05
k_d4_n-2SAT0.05
k_grz_n-2SAT0.05
k_lin_p-3UNSAT0.05
k_dum_p-6UNSAT0.05
k_poly_p-7UNSAT0.06
k_path_p-5UNSAT0.06
k_poly_n-7SAT0.06
k_lin_p-4UNSAT0.06
flipflop-4-cUNSAT0.06
toilet_c_08_01.7UNSAT0.06
k_poly_p-8UNSAT0.06
k_path_n-4SAT0.06
k_d4_p-4UNSAT0.06
cnt05SAT0.06
CHAIN12v.13SAT0.07
k_grz_n-4SAT0.07
k_poly_p-9UNSAT0.07
k_path_n-5SAT0.07
toilet_a_06_01.10UNSAT0.07
BLOCKS3iii.4UNSAT0.07
k_grz_n-5SAT0.08
k_grz_p-5UNSAT0.08
k_dum_n-9SAT0.08
k_grz_p-4UNSAT0.08
k_path_n-6SAT0.08
k_poly_p-11UNSAT0.08
k_t4p_n-2SAT0.08
k_dum_n-11SAT0.09
mutex-8-sSAT0.09
k_d4_n-3SAT0.09
k_dum_p-12UNSAT0.09
CHAIN14v.15SAT0.09
k_poly_n-14SAT0.1
k_ph_n-8SAT0.1
k_t4p_p-4UNSAT0.1
k_dum_n-12SAT0.1
toilet_a_08_05.2UNSAT0.1
stmt27_296_297SAT0.11
k_grz_n-6SAT0.11
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.11
k_poly_p-14UNSAT0.11
k_lin_n-3SAT0.11
k_dum_p-14UNSAT0.11
CHAIN17v.18SAT0.11
CHAIN16v.17SAT0.11
k_poly_p-16UNSAT0.12
k_poly_p-15UNSAT0.12
k_d4_p-7UNSAT0.12
k_poly_n-16SAT0.12
k_dum_p-16UNSAT0.12
k_dum_p-17UNSAT0.12
k_grz_n-7SAT0.13
k_path_n-9SAT0.13
texas.parsesys^1.E-d4SAT0.13
k_poly_n-17SAT0.13
BLOCKS3ii.4.3UNSAT0.13
rankfunc17_unsigned_16SAT0.13
k_d4_p-8UNSAT0.13
k_path_p-10UNSAT0.13
toilet_c_08_01.11UNSAT0.14
toilet_c_08_05.4SAT0.14
rankfunc5_signed_32SAT0.14
k_poly_n-18SAT0.14
lut4_XOR_fORUNSAT0.14
k_lin_p-8UNSAT0.14
k_dum_p-21UNSAT0.15
qshifter_6SAT0.15
k_grz_n-8SAT0.15
gttt_2_2_0010_3x3_torus_wUNSAT0.15
k_poly_p-19UNSAT0.15
k_branch_n-3SAT0.15
stmt44_916_917SAT0.15
lut4_XOR_f1SAT0.15
CHAIN19v.20SAT0.15
k_t4p_p-6UNSAT0.15
k_poly_n-20SAT0.15
k_dum_p-20UNSAT0.15
k_dum_n-17SAT0.15
vonNeumann-ripple-carry-5-cUNSAT0.16
k_t4p_n-4SAT0.16
stmt24_765_766SAT0.16
k_dum_n-18SAT0.16
k_poly_n-21SAT0.16
CHAIN20v.21SAT0.17
k_ph_n-9SAT0.17
k_d4_p-10UNSAT0.17
rankfunc13_signed_32SAT0.17
k_path_n-12SAT0.17
k_lin_p-11UNSAT0.17
k_path_p-13UNSAT0.17
connect_5x4_3_DUNSAT0.18
k_grz_p-10UNSAT0.18
BLOCKS3iii.5SAT0.18
k_dum_n-21SAT0.19
k_lin_p-9UNSAT0.19
k_grz_p-12UNSAT0.19
k_grz_p-13UNSAT0.19
k_path_p-14UNSAT0.19
k_path_n-13SAT0.19
CHAIN22v.23SAT0.19
ken.flash^10.C-f2UNSAT0.19
CHAIN21v.22SAT0.19
s27_d4_uUNSAT0.19
C432.blif_0.10_1.00_0_0_inp_exactUNSAT0.2
k_grz_p-11UNSAT0.2
k_d4_p-11UNSAT0.2
k_path_p-15UNSAT0.2
C432.blif_0.10_1.00_0_0_out_exactUNSAT0.2
k_path_n-14SAT0.2
k_lin_p-12UNSAT0.2
CHAIN23v.24SAT0.2
CHAIN18v.19SAT0.21
stmt16_950_951SAT0.21
k_t4p_n-5SAT0.21
k_grz_n-10SAT0.21
k_t4p_p-9UNSAT0.21
k_path_n-16SAT0.22
k_lin_p-10UNSAT0.22
rankfunc51_signed_32SAT0.22
k_branch_n-4SAT0.22
k_path_p-16UNSAT0.22
mutex-16-sSAT0.22
flipflop-5-cUNSAT0.22
k_lin_p-19UNSAT0.23
C432.blif_0.10_1.00_0_1_inp_exactSAT0.23
vis.4-arbit^2.E-f2SAT0.24
C432.blif_0.10_1.00_0_1_out_exactSAT0.24
toilet_c_10_01.12UNSAT0.24
cube_c3_ser--opt-6_SAT0.24
k_grz_p-17UNSAT0.24
k_t4p_p-10UNSAT0.24
term1.blif_0.10_0.20_0_1_out_exactSAT0.24
k_d4_p-13UNSAT0.24
k_grz_p-16UNSAT0.24
k_path_p-18UNSAT0.25
lut4_AND_f1SAT0.25
k_lin_p-14UNSAT0.25
k_t4p_n-6SAT0.26
connect_6x5_5_DUNSAT0.27
query01_ntrivil_1344UNSAT0.27
k_path_p-19UNSAT0.27
vis.prodcell^01.E-d2SAT0.28
sortnetsort5.v.stepl.004UNSAT0.28
k_lin_n-6SAT0.29
cnt11SAT0.29
k_path_p-21UNSAT0.29
k_path_n-19SAT0.29
k_t4p_p-12UNSAT0.29
vonNeumann-ripple-carry-6-cUNSAT0.29
cnt10SAT0.3
k_d4_p-16UNSAT0.3
k_d4_n-7SAT0.31
rankfunc5_unsigned_64SAT0.31
k_d4_p-17UNSAT0.32
k_grz_p-18UNSAT0.32
k_grz_p-19UNSAT0.32
k_lin_n-5SAT0.32
BLOCKS3i.5.4SAT0.32
ken.flash^10.C-f3UNSAT0.34
rankfunc33_signed_32SAT0.34
szymanski-5-sUNSAT0.34
BLOCKS4iii.6UNSAT0.35
stmt41_738_749SAT0.36
k_t4p_p-15UNSAT0.36
k_d4_n-8SAT0.36
k_t4p_n-8SAT0.36
small-swap1-fixpoint-3SAT0.36
term1.blif_0.10_1.00_0_0_inp_exactUNSAT0.36
p5-5.pddl_planlen=6SAT0.37
connect_7x6_4_WUNSAT0.39
k_t4p_p-16UNSAT0.39
k_d4_p-20UNSAT0.39
s27_d5_uUNSAT0.39
term1.blif_0.10_1.00_0_1_out_exactSAT0.4
k_branch_p-5UNSAT0.4
k_t4p_n-9SAT0.41
term1.blif_0.10_1.00_0_1_inp_exactSAT0.41
k_t4p_p-17UNSAT0.42
b12_PR_9_2SAT0.42
term1.blif_0.10_1.00_0_0_out_exactUNSAT0.42
rankfunc14_signed_64SAT0.42
k_lin_n-7SAT0.43
toilet_a_08_01.13UNSAT0.44
eijk.S382.S-d4SAT0.44
k_t4p_p-18UNSAT0.44
C499.blif_0.10_1.00_0_0_inp_exactUNSAT0.44
C880.blif_0.10_1.00_0_1_inp_exactSAT0.45
rankfunc13_unsigned_64SAT0.46
query48_query15_1344UNSAT0.46
lut4_3_fANDSAT0.47
k_ph_n-11SAT0.47
driverlog01_7SAT0.48
C880.blif_0.10_1.00_0_1_out_exactSAT0.48
k_t4p_p-20UNSAT0.49
k_grz_n-18SAT0.49
connect_8x7_7_WUNSAT0.49
BLOCKS3ii.5.3SAT0.5
query21_ntrivil_1344UNSAT0.5
aim-50-6_0-yes1-3-50UNSAT0.5
cnt14SAT0.5
BLOCKS3ii.5.2UNSAT0.5
k_d4_n-10SAT0.5
BLOCKS3i.5.3UNSAT0.51
arbiter-07-comp-error01-qbf-hardness-depth-4UNSAT0.51
vonNeumann-ripple-carry-7-cUNSAT0.52
C432.blif_0.10_0.20_0_1_inp_exactSAT0.52
k_grz_n-20SAT0.54
c4_BMC_p1_k32SAT0.56
stmt25_52_53SAT0.56
k_grz_n-21SAT0.57
par8-1-c-50UNSAT0.57
term1.blif_0.10_0.20_0_1_inp_exactSAT0.57
k_t4p_n-12SAT0.58
tlc03-uniform-depth-9UNSAT0.59
k_lin_n-8SAT0.63
k_t4p_n-13SAT0.65
biu.mv.xl_ao.bb-b001-p010-IPF02-c07.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003SAT0.67
k_branch_p-6UNSAT0.67
flipflop-6-cUNSAT0.68
gttt_2_2_00101121_3x3_bUNSAT0.68
arbiter-06-comp-error02-qbf-hardness-depth-5UNSAT0.68
rankfunc22_signed_64SAT0.69
biu.mv.xl_ao.bb-b001-p010-OPF02-c08.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003SAT0.69
C499.blif_0.10_1.00_0_0_out_exactUNSAT0.69
ev-pr-4x4-5-3-0-0-1-lgSAT0.7
toilet_a_08_05.9SAT0.7
k_t4p_n-14SAT0.71
biu.mv.xl_ao.bb-b001-p010-IPF02-c08.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003SAT0.72
small-synabs-fixpoint-9UNSAT0.73
stmt27_16_97UNSAT0.74
k_lin_n-9SAT0.74
biu.mv.xl_ao.bb-b001-p010-IPF05-c07.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003SAT0.75
driverlog03_7SAT0.75
k_t4p_n-15SAT0.77
biu.mv.xl_ao.bb-b001-p005-OPF03-c09.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003SAT0.78
mutex-32-sSAT0.78
szymanski-6-sUNSAT0.81
k_d4_n-14SAT0.83
vonNeumann-ripple-carry-8-cUNSAT0.84
k_d4_n-15SAT0.85
qshifter_7SAT0.87
p5-5.pddl_planlen=5SAT0.91
cnt07eSAT0.91
arbiter-07-comp-error02-qbf-hardness-depth-6UNSAT0.92
lights3_021_0_027UNSAT0.95
irst.dme6.B-d2SAT0.96
gttt_2_1_000111_3x3_torus_bSAT0.96
texas.PI_main^16.E-f2SAT0.99
k_d4_n-16SAT1
s386_d2_sSAT1.01
term1.blif_0.10_0.20_0_0_inp_exactUNSAT1.04
cache-coherence-2-fixpoint-1UNSAT1.04
C499.blif_0.10_0.20_0_1_inp_exactSAT1.06
lut4_2_f1SAT1.18
vonNeumann-ripple-carry-9-cUNSAT1.21
aim-100-6_0-yes1-3-50SAT1.25
lights3_021_0_009SAT1.28
k_lin_n-11SAT1.36
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-003UNSAT1.37
c4_BMC_p2_k128UNSAT1.43
k_branch_p-8UNSAT1.44
k_d4_n-20SAT1.48
k_branch_n-8SAT1.49
k_ph_n-14SAT1.81
dungeon_i10-m5-u10-v0.pddl_planlen=23UNSAT1.83
k_branch_n-9SAT1.84
flipflop-7-cUNSAT1.91
vonNeumann-ripple-carry-10-cUNSAT1.92
Core1108_tbm_21.tex.module.000026UNSAT1.93
arbiter-06-comp-error01-qbf-hardness-depth-12UNSAT1.94
tlc03-nonuniform-depth-17UNSAT1.97
s510_d3_sSAT1.97
arbiter-07-comp-error01-qbf-hardness-depth-11UNSAT1.98
ev-pr-4x4-7-3-0-0-1-lgSAT2
mutex-64-sSAT2.02
fpu-10Xh-error01-uniform-depth-5UNSAT2.03
ev-pr-6x6-5-5-0-1-2-lgUNSAT2.05
k_branch_n-10SAT2.39
term1.blif_0.10_0.20_0_0_out_exactUNSAT2.41
k_branch_p-10UNSAT2.42
fpu-10Xe-correct01-nonuniform-depth-6UNSAT2.49
arbiter-08-comp-error02-qbf-hardness-depth-9SAT2.55
biu.mv.xl_ao.bb-b001-p010-MIF01-c01.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004SAT2.57
arbiter-10-comp-error01-qbf-hardness-depth-10UNSAT2.64
vonNeumann-ripple-carry-11-cUNSAT2.69
rankfunc3_signed_64SAT2.69
biu.mv.xl_ao.bb-b001-p010-MIF05-c07.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004SAT2.73
toilet_a_10_05.3UNSAT2.74
tlc03-uniform-depth-21UNSAT2.83
szymanski-8-sUNSAT2.96
C5315.blif_0.10_1.00_0_0_inp_exactUNSAT2.98
lognBWLARGEA1UNSAT3.01
k_lin_n-14SAT3.2
C5315.blif_0.10_1.00_0_1_inp_exactSAT3.21
s05378_PR_1_75UNSAT3.22
s1196_d2_sSAT3.24
k_branch_n-11SAT3.3
fpu-10Xh-correct04-uniform-depth-8UNSAT3.34
k_branch_p-11UNSAT3.37
stmt19_3_214UNSAT3.44
arbiter-06-comp-error01-qbf-hardness-depth-15UNSAT3.55
lut4_2_f2UNSAT3.62
small-swap2-fixpoint-4SAT3.64
query51_query50_1344UNSAT3.68
stmt19_217_309UNSAT3.86
vonNeumann-ripple-carry-12-cUNSAT3.86
s386_d4_sSAT3.89
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.95
k_ph_n-16SAT4.04
k_lin_n-15SAT4.11
k_branch_p-12UNSAT4.38
k_branch_n-12SAT4.38
stmt19_90_266UNSAT4.46
texas.PI_main^08.E-f3SAT4.64
s820_d3_sSAT4.67
s09234_PR_8_5SAT4.89
vonNeumann-ripple-carry-13-cUNSAT5.02
lights3_035_0_002UNSAT5.08
flipflop-8-cUNSAT5.21
s05378_PR_9_2SAT5.22
mutex-128-sSAT5.22
lights3_035_0_027UNSAT5.24
incrementer-enc03-nonuniform-depth-13UNSAT5.36
s298_d4_sSAT5.43
k_branch_p-14UNSAT5.59
k_ph_p-10UNSAT5.75
fpu-10Xh-correct04-uniform-depth-14UNSAT5.8
s641_d3_sSAT5.82
fpu-10Xh-correct04-uniform-depth-15UNSAT6.12
k_branch_p-16UNSAT6.13
lut4_AND_fXORUNSAT6.13
fpu-10Xh-correct04-uniform-depth-16UNSAT6.24
test3_quant_squaring2UNSAT6.27
ev-pr-6x6-7-5-0-1-2-lgUNSAT6.29
gttt_2_2_001020_4x4_wUNSAT6.32
k_branch_n-16SAT6.41
ev-pr-8x8-5-7-0-1-2-lgUNSAT6.6
fpu-10Xh-correct04-nonuniform-depth-18UNSAT6.89
lights3_035_0_051UNSAT6.91
s713_d3_sSAT7.04
ev-pr-4x4-9-3-0-0-1-lgSAT7.17
k_lin_n-17SAT7.5
s3330_d2_sSAT7.69
query11_query21_1344UNSAT7.92
szymanski-10-sUNSAT8.21
fpu-10Xe-correct01-uniform-depth-22UNSAT8.21
vonNeumann-ripple-carry-15-cUNSAT8.66
cube_c9_par--opt-11_SAT8.87
fpu-10Xe-correct01-nonuniform-depth-24UNSAT8.98
b20_PR_7_90UNSAT9.17
cache-coherence-3-fixpoint-3UNSAT9.31
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-005UNSAT9.37
tlc04-uniform-depth-36UNSAT9.49
k_branch_p-18UNSAT9.7
fpu-10Xh-correct04-nonuniform-depth-27UNSAT9.87
Core1108_tbm_21.tex.module.000027UNSAT9.94
s820_d2_sSAT9.95
qshifter_8SAT10.91
arbiter-07-comp-error01-qbf-hardness-depth-20UNSAT11.25
tlc03-uniform-depth-52UNSAT11.66
tlc01-uniform-depth-73UNSAT12.15
incrementer-enc07-nonuniform-depth-17UNSAT12.73
gttt_2_1_00102030_4x4_torus_bUNSAT12.85
ken.flash^03.C-f3UNSAT13.22
aim-200-1_6-yes1-4-90SAT14.05
s713_d2_sSAT14.25
s386_d6_sSAT14.63
Core1108_tbm_21.tex.module.000030SAT14.77
Adder2-8-sUNSAT14.88
toilet_c_10_01.17UNSAT14.89
cube_c11_par---13_UNSAT15.53
p20-1.pddl_planlen=24UNSAT15.67
Core1108_tbm_21.tex.module.000008SAT15.8
s641_d2_sSAT15.82
lognBWLARGEB1UNSAT16.46
Core1108_tbm_02.tex.moduleQ3.2S.000015UNSAT16.53
incrementer-enc03-nonuniform-depth-24UNSAT16.68
incrementer-enc07-nonuniform-depth-21UNSAT17.13
p20-1.pddl_planlen=26UNSAT17.35
flipflop-9-cUNSAT17.67
ev-pr-8x8-7-7-0-1-2-lgUNSAT18.58
s1269_d3_sSAT19.44
s386_d7_sSAT19.75
Core1108_tbm_03.tex.moduleQ3.2S.000002UNSAT20.05
s641_d4_sSAT20.17
arbiter-10-comp-error01-qbf-hardness-depth-22UNSAT20.24
szymanski-12-sUNSAT20.45
dungeon_i10-m5-u10-v0.pddl_planlen=134UNSAT20.78
incrementer-enc02-nonuniform-depth-31UNSAT21.71
c1_BMC_p1_k4SAT22.23
tlc04-nonuniform-depth-56UNSAT22.98
ev-pr-6x6-9-5-0-1-2-lgUNSAT23.21
s641_d5_sSAT23.42
s510_d6_sSAT23.75
cnt08eSAT24.83
sortnetsort9.v.stepl.007SAT25.3
s298_d10_sSAT26.15
sortnetsort9.v.stepl.005SAT26.15
Umbrella_tbm_24.tex.module.000066SAT26.37
sortnetsort8.AE.stepl.003SAT26.81
sortnetsort8.v.stepl.007SAT26.83
lut4_2_fXORSAT27.05
s499_d9_sSAT27.11
jnh212-50UNSAT27.12
sortnetsort7.v.stepl.007SAT27.45
sortnetsort10.v.stepl.005SAT27.46
par8-4-50UNSAT27.74
gttt_1_1_001020_3x3_wSAT27.8
biu.mv.xl_ao.bb-b001-p005-OPF05-c02.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004SAT27.88
p20-1.pddl_planlen=32UNSAT28.88
s01238_PR_8_2SAT28.91
query26_query34_1344SAT29.09
s386_d8_uUNSAT29.54
test5_quant_squaring4SAT29.54
C432.blif_0.10_0.20_0_0_inp_exactSAT29.6
C5315.blif_0.10_1.00_0_1_out_exactSAT30.32
BLOCKS4i.6.4SAT30.67
tlc02-uniform-depth-114UNSAT30.73
stmt23_72_76SAT30.78
ring_r3_ser--opt-8_SAT30.79
s09234_PR_8_2SAT30.91
s15850_PR_2_2SAT31.03
s15850_PR_8_50SAT31.03
Umbrella_tbm_25.tex.moduleQ3.2S.000075UNSAT31.12
C499.blif_0.10_1.00_0_1_out_exactSAT31.29
C499.blif_0.10_1.00_0_1_inp_exactSAT31.32
k8_3_2SAT31.88
cnt16rSAT31.91
biu.mv.xl_ao.bb-b001-p010-MIF04-c06.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-005SAT32.06
Adder2-10-sUNSAT32.15
stmt17_63_82SAT32.63
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-008UNSAT33.15
s713_d4_sSAT33.97
C432.blif_0.10_0.20_0_1_out_exactSAT34.21
ev-pr-4x4-11-3-0-0-1-lgSAT34.49
dungeon_i10-m10-u10-v0.pddl_planlen=187UNSAT34.49
biu.mv.xl_ao.bb-b001-p005-OPF05-c03.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004SAT34.55
texas.two_proc^4.E-f2SAT34.55
gttt_1_1_000111_3x3_torus_wSAT35.05
sortnetsort9.AE.stepl.009UNSAT35.39
stmt17_62_98SAT35.75
k8_2_3SAT36.04
C5315.blif_0.10_0.20_0_1_inp_exactSAT36.21
stmt17_70_90SAT37.28
s641_d6_sSAT38.46
stmt17_70_98SAT39.31
s298_d12_sSAT39.57
Umbrella_tbm_24.tex.module.000131SAT39.92
s713_d5_sSAT40.04
stmt17_82_98SAT40.36
p20-5.pddl_planlen=32UNSAT40.59
stmt28_68_81SAT40.69
test5_quant_squaring5SAT41.63
k8_3_4SAT41.65
gttt_2_1_00011020_4x4_bSAT41.67
stmt17_86_98SAT41.74
BLOCKS4ii.7.2SAT42.23
gttt_2_1_0010_4x4_torus_bSAT44.63
ev-pr-6x6-11-5-0-1-2-lgUNSAT45.05
s499_d7_sSAT46
p20-5.pddl_planlen=17UNSAT46.44
szymanski-14-sUNSAT46.84
incrementer-enc07-uniform-depth-25SAT49.9
kernel_agplib_intrface.cSAT50.02
hid_hclient_ecdisp.cSAT52.04
C6288.blif_0.10_1.00_0_0_out_exactSAT53.21
p10-10.pddl_planlen=10SAT54.1
biu.mv.xl_ao.bb-b003-p020-IPF03-c03.blif-biu.inv.prop.bb-bmc.with-IOC.unfold-009UNSAT58.8
b22_PR_8_20SAT59.35
s499_d12_sSAT59.76
s641_d7_uUNSAT60.46
par16-1-50UNSAT61.07
input_mouser_cseries.cSAT61.8
network_irda_miniport_nscirda_settings.cSAT64.2
filesys_smbmrx_cvsndrcv.cSAT64.54
s1269_d4_sSAT66.51
ev-pr-8x8-9-7-0-1-2-lgUNSAT67.42
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-007UNSAT67.75
k_ph_n-21SAT68.13
tlc04-nonuniform-depth-98UNSAT69.06
s510_d11_sSAT76
s499_d15_sSAT78.6
k_ph_p-12UNSAT80.82
dungeon_i15-m7-u4-v0.pddl_planlen=81SAT84.31
s298_d14_sSAT86.48
s713_d6_sSAT87.33
s1196_d7_uUNSAT91.57
flipflop-10-cUNSAT93.01
s641_d10_uUNSAT93.09
connect_5x4_4_RSAT93.16
s1196_d4_uUNSAT93.45
s386_d9_uUNSAT93.97
cube_c7_ser--opt-24_SAT98.93
s499_d18_sSAT100.77
s820_d8_sSAT101.5
sortnetsort9.AE.stepl.012UNSAT102.22
s386_d3_sSAT104.25
ev-pr-4x4-13-3-0-0-1-lgSAT104.37
s298_d17_sSAT104.77
s713_d10_uUNSAT105.08
test4_quant_squaring2UNSAT105.88
Umbrella_tbm_05.tex.module.000039SAT111.07
s713_d7_uUNSAT112.97
s386_d12_uUNSAT116.35
connect_5x4_3_RSAT117.84
ii32b1-00SAT120.18
tlc02-uniform-depth-241UNSAT121
stmt41_160_235UNSAT121.8
s820_d10_sSAT123.01
C6288.blif_0.10_1.00_0_1_out_exactSAT125.87
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-008UNSAT127.66
Adder2-16-sSAT129.58
s499_d17_sSAT130.83
s641_d8_uUNSAT131.6
C6288.blif_0.10_1.00_0_1_inp_exactSAT131.77
s1196_d3_uUNSAT133.69
s1196_1_5SAT135.59
s1196_d5_uUNSAT145.16
b20_C_3_2FAIL147.14
b21_C_3_206FAIL157.43
k_ph_p-13UNSAT158.16
s499_d19_sSAT158.54
s3330_d4_sSAT160.78
c5_BMC_p2_k64SAT160.84
ev-pr-4x4-5-3-0-0-1-sFAIL164.03
c3_BMC_p1_k256SAT164.9
s499_d22_uUNSAT174.34
szymanski-16-sUNSAT177.47
ev-pr-4x4-7-3-0-0-1-sFAIL178.73
s713_d11_uUNSAT179.54
s641_d11_uUNSAT182.67
s820_d7_sSAT183.65
s386_d10_uUNSAT203.8
small-seq-fixpoint-5FAIL206.23
ev-pr-8x8-11-7-0-1-2-lgUNSAT206.25
s298_d18_sSAT207.02
sortnetsort8.v.stepl.009SAT216.94
s298_d22_uUNSAT217.66
s820_d12_uUNSAT226.41
ev-pr-6x6-5-5-0-1-2-sFAIL233.43
s386_d11_uUNSAT234.22
gttt_1_1_00101121_4x4_torus_wUNSAT244.02
ev-pr-4x4-9-3-0-0-1-sFAIL251.74
emptyroom_e3_ser--opt-20_SAT255.87
flipflop-11-cUNSAT262.99
connect_8x7_6_RSAT267.6
connect_8x7_5_RSAT285.01
s298_d25_uUNSAT292.89
ev-pr-4x4-15-3-0-0-1-lgSAT326.84
ev-pr-6x6-13-5-0-1-2-lgUNSAT356.18
ev-pr-4x4-11-3-0-0-1-sFAIL366.23
ev-pr-6x6-7-5-0-1-2-sFAIL367.43
C880.blif_0.10_1.00_0_0_inp_exactUNSAT369.05
ev-pr-8x8-19-7-0-1-2-lgFAIL400.47
ev-pr-4x4-17-3-0-0-1-sFAIL406.93
k_branch_p-21FAIL407.23
k_branch_n-20FAIL411.64
connect_9x8_6_RSAT434.36
ev-pr-4x4-15-3-0-0-1-sFAIL441.33
k12_4_2SAT441.88
s820_d14_uUNSAT453.52
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-010UNSAT459.15
s713_d9_uUNSAT486.75
szymanski-18-sUNSAT512.2
small-seq-fixpoint-3FAIL515.55
b20_PR_7_20FAIL545.34
p10-10.pddl_planlen=6UNSAT555.11
ev-pr-6x6-9-5-0-1-2-sFAIL559.54
s1196_d6_uUNSAT561.04
C432.blif_0.10_0.20_0_0_out_exactUNSAT577.01
p20-20.pddl_planlen=23FAIL596.61
pipesnotankage14_10FAIL597.71
c4_Debug_s3_f1_e2_v3FAIL598.02
ev-pr-6x6-19-5-0-1-2-sFAIL598.21
ev-pr-6x6-17-5-0-1-2-sFAIL598.51
ev-pr-6x6-15-5-0-1-2-sFAIL598.71
ev-pr-6x6-13-5-0-1-2-sFAIL598.81
ev-pr-6x6-11-5-0-1-2-sFAIL599.01
dungeon_i25-m12-u3-v0.pddl_planlen=72FAIL599.01
dungeon_i25-m12-u5-v0.pddl_planlen=65FAIL599.11
c4_Debug_s5_f2_e2_v1FAIL599.21
ev-pr-8x8-15-7-0-1-2-lgFAIL599.41
c4_Debug_s3_f1_e1_v2FAIL599.43
s1269_d13_uFAIL599.52
c5_BMC_p1_k32FAIL599.52
ev-pr-8x8-17-7-0-1-2-lgFAIL599.52
s3330_d9_sFAIL599.53
s3330_d5_sFAIL599.53
s1269_d12_uFAIL599.53
s3330_d8_sFAIL599.53
depots03_9FAIL599.53
c4_Debug_s3_f1_e2_v2FAIL599.53
input_pnpi8042_moudep.cFAIL599.61
s820_d9_sFAIL599.61
C6288.blif_0.10_0.20_0_0_inp_exactFAIL599.61
s510_d24_sFAIL599.61
ev-pr-6x6-17-5-0-1-2-lgFAIL599.61
s1269_d9_sFAIL599.61
network_irda_miniport_nscirda_comm.cFAIL599.61
network_trans_sys_notify.cFAIL599.61
s499_d25_uFAIL599.61
s510_d23_sFAIL599.61
adder-10-satFAIL599.61
s1269_d8_sFAIL599.61
s3330_d7_sFAIL599.61
s1269_d14_uFAIL599.61
ev-pr-8x8-13-7-0-1-2-lgFAIL599.61
adder-12-satFAIL599.61
adder-14-satFAIL599.61
s499_d24_uFAIL599.61
s820_d11_uFAIL599.61
network_ndis_rtlnwifi_hw_hw_ccmp.cFAIL599.61
s1269_d10_sFAIL599.62
ev-pr-4x4-13-3-0-0-1-sFAIL599.62
ev-pr-6x6-19-5-0-1-2-lgFAIL599.62
driverlog10_6FAIL599.62
s1269_d15_uFAIL599.71
C6288.blif_0.10_0.20_0_0_out_exactFAIL599.71
b22_C_2_12FAIL599.71
emptyroom_e4_ser--opt-44_FAIL599.71
nusmv.tcas^6.B-f4FAIL599.71
dungeon_i25-m12-u3-v0.pddl_planlen=165FAIL599.71
texas.PI_main^05.E-f3FAIL599.71
nusmv.tcas^3.B-f2FAIL599.71
s3330_d3_sFAIL599.71
ev-pr-6x6-15-5-0-1-2-lgFAIL599.71
emptyroom_e3_ser---19_FAIL599.71
uclid-pipe3aFAIL599.71
connect_8x7_4_RFAIL599.71
query03_query25_1344FAIL599.71
query44_query26_1344nFAIL599.71
s713_d8_uFAIL599.71
s510_d31_sFAIL599.71
C880.blif_0.10_1.00_0_0_out_exactFAIL599.71
eijk.bs4863.S-d4FAIL599.71
ken.flash^08.C-d4FAIL599.71
ken.oop^2.C-d3FAIL599.71
c2_Debug_s3_f2_e1_v3FAIL599.71
c4_Debug_s3_f2_e2_v2FAIL599.71
C6288.blif_0.10_0.20_0_1_out_exactFAIL599.71
uclid-pipe2FAIL599.71
s510_d32_sFAIL599.71
C880.blif_0.10_0.20_0_1_out_exactFAIL599.71
test2_quant_squaring2FAIL599.71
f600-50FAIL599.71
test1_quant_squaring2FAIL599.71
k8_4_3FAIL599.71
C5315.blif_0.10_1.00_0_0_out_exactFAIL599.71
incrementer-enc06-uniform-depth-24FAIL599.71
incrementer-enc08-uniform-depth-33FAIL599.71
test3_quant_squaring4FAIL599.71
k5_3_2FAIL599.71
ev-pr-4x4-17-3-0-0-1-lgFAIL599.71
C880.blif_0.10_0.20_0_0_inp_exactFAIL599.71
stmt19_83_412FAIL599.71
uclid-pipe3bFAIL599.71
C6288.blif_0.10_1.00_0_0_inp_exactFAIL599.71
incrementer-enc02-uniform-depth-58FAIL599.71
k6_2_3FAIL599.71
adder-12-unsatFAIL599.71
C5315.blif_0.10_0.20_0_0_inp_exactFAIL599.71
s510_d28_sFAIL599.71
test4_quant_squaring4FAIL599.71
s3330_d14_uFAIL599.71
cache-coherence-2-fixpoint-6FAIL599.71
sdlx-fixpoint-3FAIL599.71
s820_d15_uFAIL599.71
s510_d35_sFAIL599.71
k5_2_3FAIL599.71
stmt21_79_304FAIL599.71
C5315.blif_0.10_0.20_0_0_out_exactFAIL599.71
s1269_d5_sFAIL599.71
test1_quant_squaring3FAIL599.71
k_ph_p-15FAIL599.71
stmt19_64_99FAIL599.71
k_ph_p-19FAIL599.71
k_ph_p-20FAIL599.71
stmt29_226_376FAIL599.71
C499.blif_0.10_0.20_0_0_inp_exactFAIL599.71
k_ph_p-18FAIL599.71
test2_quant_squaring3FAIL599.71
s510_d36_sFAIL599.72
c2_BMC_p1_k2048FAIL599.72
szymanski-20-sFAIL599.72
query42_query06_1344nFAIL599.72
audio_ddksynth_csynth2.cppFAIL599.72
AR-fixpoint-5FAIL599.72
c1_Debug_s5_f1_e1_v2FAIL599.72
c5_BMC_p2_k128FAIL599.72
szymanski-24-sFAIL599.72
s3330_d10_uFAIL599.72
nusmv.reactor^3.C-d4FAIL599.72
s3330_d12_uFAIL599.72
flipflop-12-cFAIL599.72
s298_d19_uFAIL599.72
k14_2_3FAIL599.72
c1_BMC_p2_k1024FAIL599.72
Adder2-8-cFAIL599.72
c2_Debug_s3_f1_e1_v2FAIL599.72
c3_Debug_s3_f2_e2_v2FAIL599.72
emptyroom_e4_par---21_FAIL599.72
stmt23_66_96FAIL599.72
dungeon_i25-m12-u3-v0.pddl_planlen=190FAIL599.72
stmt52_244_394FAIL599.72
dungeon_i25-m12-u5-v0.pddl_planlen=170FAIL599.72
c1_BMC_p2_k512FAIL599.72
nusmv.tcas-t^1.B-d2FAIL599.81
C880.blif_0.10_0.20_0_1_inp_exactFAIL599.81
ken.oop^2.C-d4FAIL599.81
stmt21_319_418FAIL599.81
query31_reachqu_1344nFAIL599.81
pipesnotankage18_8FAIL599.81
C880.blif_0.10_0.20_0_0_out_exactFAIL599.81
C499.blif_0.10_0.20_0_1_out_exactFAIL599.81
C5315.blif_0.10_0.20_0_1_out_exactFAIL599.81
C6288.blif_0.10_0.20_0_1_inp_exactFAIL599.82
c1_Debug_s3_f1_e1_v1FAIL599.82
dungeon_i25-m12-u3-v0.pddl_planlen=130FAIL599.82
pipesnotankage18_7FAIL599.91
C499.blif_0.10_0.20_0_0_out_exactFAIL599.91