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

InstanceResultTime
s27_d4_uUNSAT0
mutex-2-sSAT0
toilet_c_06_01.4UNSAT0
s27_d3_uUNSAT0
tree-exa10-10SAT0
stmt1_30_31SAT0
toilet_c_04_01.4UNSAT0
stmt44_107_108SAT0
impl02SAT0
z4ml.blif_0.10_0.20_0_1_out_exactSAT0
toilet_a_04_01.4UNSAT0
stmt44_107_113SAT0
s27_d5_uUNSAT0
toilet_c_08_01.2UNSAT0
lognBWLARGEB0UNSAT0
toilet_a_04_05.2SAT0
lognBWLARGEA0UNSAT0
toilet_a_02_10.2SAT0
z4ml.blif_0.10_1.00_0_1_out_exactSAT0
z4ml.blif_0.10_1.00_0_0_inp_exactUNSAT0
z4ml.blif_0.10_1.00_0_1_inp_exactSAT0
toilet_g_15_01.2SAT0
z4ml.blif_0.10_0.20_0_1_inp_exactSAT0
cnt01SAT0
z4ml.blif_0.10_1.00_0_0_out_exactUNSAT0
mutex-4-sSAT0
s27_d2_sSAT0
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
flipflop-3-cUNSAT0
k_ph_p-1UNSAT0
k_ph_n-3SAT0
k_ph_n-1SAT0
toilet_g_06_01.2SAT0
toilet_g_02_01.2SAT0
toilet_g_04_01.2SAT0
toilet_g_10_01.2SAT0
toilet_g_08_01.2SAT0
k_dum_p-6UNSAT0.01
impl06SAT0.01
impl04SAT0.01
eijk.S382.S-d4SAT0.01
irst.dme6.B-d2SAT0.01
k_path_n-4SAT0.01
impl08SAT0.01
s298_d2_sUNSAT0.01
k_dum_p-3UNSAT0.01
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.01
impl12SAT0.01
k_dum_p-2UNSAT0.01
texas.parsesys^1.E-d4SAT0.01
mutex-8-sSAT0.01
lut4_XOR_f1SAT0.01
k_path_n-5SAT0.01
BLOCKS3iii.4UNSAT0.01
C432.blif_0.10_1.00_0_1_inp_exactSAT0.01
k_path_n-3SAT0.01
k_path_p-2UNSAT0.01
k_path_p-5UNSAT0.01
k_poly_p-2UNSAT0.01
flipflop-4-cUNSAT0.01
k_poly_n-2SAT0.01
k_lin_p-4UNSAT0.01
z4ml.blif_0.10_0.20_0_0_out_exactUNSAT0.01
tree-exa2-10UNSAT0.01
CHAIN12v.13UNSAT0.01
mutex-16-sSAT0.01
k_lin_p-2UNSAT0.01
cnt02eSAT0.01
k_dum_p-4UNSAT0.01
k_lin_p-3UNSAT0.01
z4ml.blif_0.10_0.20_0_0_inp_exactUNSAT0.01
k_ph_n-6SAT0.01
k_ph_p-3UNSAT0.01
counter_e_2SAT0.01
k_d4_p-1UNSAT0.01
toilet_g_20_01.2SAT0.01
k_branch_n-2SAT0.01
s386_d2_sSAT0.01
k_d4_n-2SAT0.01
k_dum_n-3SAT0.01
k_d4_n-1SAT0.01
s641_d2_sUNSAT0.01
aim-50-6_0-yes1-3-50UNSAT0.01
k3_1_1SAT0.01
k_ph_n-4SAT0.01
k_dum_n-2SAT0.01
impl10SAT0.01
toilet_c_08_01.6UNSAT0.01
k_dum_n-1SAT0.01
BLOCKS3iii.5UNSAT0.01
k_t4p_n-2SAT0.02
k_lin_n-3SAT0.02
CHAIN16v.17UNSAT0.02
k_path_n-6SAT0.02
k_grz_p-10UNSAT0.02
k_grz_p-5UNSAT0.02
gttt_2_2_0010_3x3_torus_wUNSAT0.02
k_path_p-10UNSAT0.02
k_path_n-9SAT0.02
k_poly_p-4UNSAT0.02
k_lin_p-8UNSAT0.02
tree-exa2-20UNSAT0.02
k_d4_n-3SAT0.02
toilet_c_08_01.7UNSAT0.02
incrementer-enc05-uniform-depth-2UNSAT0.02
k_grz_p-4UNSAT0.02
b12_PR_9_2SAT0.02
C432.blif_0.10_1.00_0_0_inp_exactUNSAT0.02
k_d4_p-4UNSAT0.02
k_lin_p-9UNSAT0.02
k_d4_p-7UNSAT0.02
toilet_a_04_01.6UNSAT0.02
s713_d2_sUNSAT0.02
k_t4p_p-4UNSAT0.02
k_dum_p-12UNSAT0.02
impl16SAT0.02
C499.blif_0.10_1.00_0_1_inp_exactSAT0.02
BLOCKS3ii.4.3UNSAT0.02
k_grz_n-6SAT0.02
impl18SAT0.02
k_grz_n-2SAT0.02
k_branch_n-3SAT0.02
k_ph_p-5UNSAT0.02
flipflop-5-cUNSAT0.02
s01238_PR_8_2SAT0.02
C499.blif_0.10_1.00_0_1_out_exactSAT0.02
par8-1-c-50UNSAT0.02
k_dum_n-9SAT0.02
mutex-32-sSAT0.02
k_grz_n-4SAT0.02
impl14SAT0.02
qshifter_3SAT0.02
BLOCKS3ii.5.2UNSAT0.02
k_grz_n-5SAT0.02
impl20SAT0.02
k_grz_n-8SAT0.02
CHAIN14v.15UNSAT0.02
k_grz_n-7SAT0.02
k_dum_n-5SAT0.02
k_grz_n-10SAT0.02
k_path_n-13SAT0.03
CHAIN17v.18UNSAT0.03
s298_d4_sSAT0.03
k_poly_p-7UNSAT0.03
toilet_c_06_01.8UNSAT0.03
k_dum_p-16UNSAT0.03
p5-5.pddl_planlen=5SAT0.03
k_grz_p-12UNSAT0.03
k_poly_n-7SAT0.03
k_poly_n-5SAT0.03
k_path_p-14UNSAT0.03
rewriting_k_10UNSAT0.03
tree-exa2-30UNSAT0.03
k_path_p-13UNSAT0.03
k_grz_p-16UNSAT0.03
gttt_1_1_001020_3x3_wUNSAT0.03
k_poly_n-6SAT0.03
k_path_n-12SAT0.03
k_grz_p-11UNSAT0.03
term1.blif_0.10_1.00_0_1_out_exactSAT0.03
s386_d3_sSAT0.03
BLOCKS3ii.5.3SAT0.03
s510_d3_sUNSAT0.03
arbiter-07-comp-error01-qbf-hardness-depth-4UNSAT0.03
BLOCKS4iii.6UNSAT0.03
k_dum_p-14UNSAT0.03
s641_d3_sUNSAT0.03
k_d4_p-8UNSAT0.03
s820_d2_sSAT0.03
k_dum_p-17UNSAT0.03
s713_d3_sUNSAT0.03
term1.blif_0.10_1.00_0_1_inp_exactSAT0.03
k_dum_n-12SAT0.03
arbiter-06-comp-error02-qbf-hardness-depth-5UNSAT0.03
k_lin_p-11UNSAT0.03
k_d4_p-10UNSAT0.03
texas.PI_main^16.E-f2UNSAT0.03
k_lin_p-10UNSAT0.03
k_t4p_p-6UNSAT0.03
CHAIN18v.19UNSAT0.03
k_dum_n-11SAT0.03
tree-exa2-25UNSAT0.03
k_grz_p-13UNSAT0.03
k_grz_p-17UNSAT0.03
k_lin_p-12UNSAT0.03
k_t4p_n-4SAT0.04
tree-exa2-35UNSAT0.04
Adder2-2-cUNSAT0.04
k_path_p-15UNSAT0.04
k_poly_p-8UNSAT0.04
k_grz_n-18SAT0.04
k_lin_n-5SAT0.04
k_lin_p-14UNSAT0.04
k_d4_p-11UNSAT0.04
k_grz_p-19UNSAT0.04
k_grz_p-18UNSAT0.04
k_dum_n-18SAT0.04
k_d4_n-7SAT0.04
k_grz_n-21SAT0.04
k_branch_n-4SAT0.04
k_path_p-19UNSAT0.04
k_path_n-16SAT0.04
k_dum_n-17SAT0.04
k_grz_n-20SAT0.04
szymanski-5-sUNSAT0.04
adder-2-unsatUNSAT0.04
k_path_p-18UNSAT0.04
k_dum_p-20UNSAT0.04
stmt41_160_235UNSAT0.04
k_d4_n-8SAT0.04
s641_d4_sUNSAT0.04
cnt05SAT0.04
tree-exa2-40UNSAT0.04
CHAIN19v.20UNSAT0.04
k_dum_p-21UNSAT0.04
k_path_n-14SAT0.04
p5-5.pddl_planlen=6SAT0.04
k_path_p-16UNSAT0.04
k_poly_p-9UNSAT0.04
term1.blif_0.10_1.00_0_0_out_exactSAT0.04
k_ph_n-8SAT0.04
s386_d4_sSAT0.04
CHAIN20v.21UNSAT0.04
cube_c3_ser--opt-6_SAT0.04
k_t4p_p-9UNSAT0.05
arbiter-07-comp-error02-qbf-hardness-depth-6UNSAT0.05
biu.mv.xl_ao.bb-b001-p010-IPF05-c07.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003SAT0.05
tree-exa2-45UNSAT0.05
k_t4p_p-10UNSAT0.05
biu.mv.xl_ao.bb-b001-p010-IPF02-c07.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003SAT0.05
mutex-64-sSAT0.05
k_d4_p-13UNSAT0.05
k_branch_p-5UNSAT0.05
k_dum_n-21SAT0.05
k_d4_p-16UNSAT0.05
nusmv.tcas-t^1.B-d2UNSAT0.05
aim-100-1_6-yes1-2-00SAT0.05
ring_r4_ser--opt-11_UNSAT0.05
k_t4p_n-5SAT0.05
k_t4p_n-6SAT0.05
CHAIN21v.22UNSAT0.05
k_poly_p-11UNSAT0.05
CHAIN22v.23UNSAT0.05
C880.blif_0.10_1.00_0_1_inp_exactSAT0.05
s1196_d2_sSAT0.05
k_path_n-19SAT0.05
k_path_p-21UNSAT0.05
flipflop-6-cUNSAT0.06
BLOCKS3i.5.4SAT0.06
k_poly_p-15UNSAT0.06
k_poly_p-14UNSAT0.06
s499_d7_sUNSAT0.06
k_ph_n-9SAT0.06
s820_d3_sSAT0.06
k_t4p_p-12UNSAT0.06
k_d4_n-10SAT0.06
k_branch_p-6UNSAT0.06
s641_d5_sUNSAT0.06
CHAIN23v.24UNSAT0.06
k_d4_p-20UNSAT0.06
tree-exa2-50UNSAT0.06
k_lin_p-19UNSAT0.06
k_lin_n-6SAT0.06
k_poly_n-14SAT0.06
tlc03-uniform-depth-9UNSAT0.06
k_d4_p-17UNSAT0.06
C499.blif_0.10_1.00_0_0_out_exactSAT0.07
k_poly_n-17SAT0.07
k_poly_n-16SAT0.07
term1.blif_0.10_1.00_0_0_inp_exactUNSAT0.07
s713_d5_sUNSAT0.07
k_poly_p-16UNSAT0.07
k_t4p_n-8SAT0.07
s386_d6_sSAT0.07
k_t4p_p-16UNSAT0.08
k_poly_n-18SAT0.08
s3330_d2_sUNSAT0.08
k_t4p_n-9SAT0.08
lights3_021_0_009SAT0.08
s713_d4_sUNSAT0.08
k_t4p_p-17UNSAT0.08
lights3_021_0_027UNSAT0.08
s641_d6_sUNSAT0.08
k_poly_p-19UNSAT0.08
k_d4_n-14SAT0.08
toilet_c_08_05.4SAT0.08
toilet_a_06_01.6UNSAT0.08
k_t4p_p-15UNSAT0.08
k_poly_n-21SAT0.09
s499_d9_sUNSAT0.09
BLOCKS4i.6.4UNSAT0.09
s386_d7_sSAT0.09
c4_BMC_p2_k128UNSAT0.09
s641_d7_uUNSAT0.09
k_poly_n-20SAT0.09
k_t4p_p-18UNSAT0.09
s1269_d3_sSAT0.09
s1196_d3_uSAT0.09
k_d4_n-15SAT0.09
s713_d6_sUNSAT0.09
k_t4p_p-20UNSAT0.1
s386_d8_uUNSAT0.1
vonNeumann-ripple-carry-5-cUNSAT0.1
k_d4_n-16SAT0.1
aim-100-6_0-yes1-3-50SAT0.1
jnh212-50UNSAT0.1
mutex-128-sSAT0.1
s510_d6_sSAT0.1
k_t4p_n-12SAT0.11
s713_d7_uUNSAT0.11
k_lin_n-7SAT0.11
s641_d8_uUNSAT0.11
stmt17_18_19SAT0.11
C432.blif_0.10_1.00_0_1_out_exactSAT0.11
s298_d10_sSAT0.12
s386_d9_uUNSAT0.12
k_d4_n-20SAT0.12
biu.mv.xl_ao.bb-b001-p010-IPF02-c08.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003SAT0.12
k_t4p_n-13SAT0.12
k_lin_n-8SAT0.13
C5315.blif_0.10_1.00_0_1_inp_exactSAT0.13
lut4_XOR_fORUNSAT0.13
k_t4p_n-14SAT0.13
s499_d12_sUNSAT0.13
flipflop-7-cUNSAT0.13
s713_d8_uUNSAT0.13
C499.blif_0.10_1.00_0_0_inp_exactUNSAT0.13
tlc03-uniform-depth-21UNSAT0.14
k_t4p_n-15SAT0.14
C880.blif_0.10_1.00_0_1_out_exactSAT0.14
s386_d10_uUNSAT0.14
C880.blif_0.10_1.00_0_0_out_exactSAT0.15
s641_d10_uUNSAT0.15
s298_d12_sSAT0.15
s713_d9_uUNSAT0.15
s386_d11_uUNSAT0.15
gttt_2_1_000111_3x3_torus_bUNSAT0.16
szymanski-6-sUNSAT0.16
gttt_1_1_00101121_4x4_torus_wUNSAT0.17
s641_d11_uUNSAT0.17
s1196_d5_uSAT0.18
nusmv.reactor^3.C-d4UNSAT0.18
s713_d10_uUNSAT0.18
s298_d14_sSAT0.18
driverlog01_7SAT0.18
BLOCKS3i.5.3UNSAT0.18
s386_d12_uUNSAT0.18
s499_d15_sUNSAT0.18
lut4_3_fANDSAT0.18
k_lin_n-9SAT0.19
C5315.blif_0.10_1.00_0_0_out_exactSAT0.19
C5315.blif_0.10_1.00_0_1_out_exactSAT0.2
k_ph_n-11SAT0.2
s713_d11_uUNSAT0.2
connect_5x4_3_DUNSAT0.21
s3330_d3_sUNSAT0.21
vonNeumann-ripple-carry-6-cUNSAT0.21
ken.flash^08.C-d4UNSAT0.21
s820_d7_sSAT0.21
s1196_d4_uSAT0.22
s499_d17_sUNSAT0.22
s1196_d6_uSAT0.23
aim-200-1_6-yes1-4-90SAT0.23
s499_d18_sUNSAT0.24
C880.blif_0.10_0.20_0_1_out_exactSAT0.24
s05378_PR_9_2SAT0.24
s510_d11_sSAT0.25
s820_d8_sSAT0.25
s499_d19_sUNSAT0.25
C880.blif_0.10_0.20_0_0_out_exactSAT0.25
s09234_PR_8_2SAT0.26
tlc03-nonuniform-depth-17SAT0.26
lognBWLARGEA1UNSAT0.26
s298_d17_sSAT0.26
s298_d18_sSAT0.27
biu.mv.xl_ao.bb-b001-p010-OPF02-c08.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003SAT0.27
gttt_2_2_001020_4x4_wUNSAT0.27
lights3_035_0_002UNSAT0.28
BLOCKS4ii.7.2UNSAT0.28
arbiter-10-comp-error01-qbf-hardness-depth-10UNSAT0.28
k_lin_n-11SAT0.29
vis.prodcell^01.E-d2SAT0.3
s1196_d7_uSAT0.3
s820_d9_sSAT0.31
lights3_035_0_051UNSAT0.31
s298_d19_uUNSAT0.32
s820_d10_sSAT0.33
flipflop-8-cUNSAT0.34
lights3_035_0_027UNSAT0.35
term1.blif_0.10_0.20_0_1_out_exactSAT0.36
k_branch_p-8UNSAT0.37
tlc04-uniform-depth-36SAT0.38
vonNeumann-ripple-carry-7-cUNSAT0.38
s820_d11_uUNSAT0.39
connect_6x5_5_DUNSAT0.39
term1.blif_0.10_0.20_0_0_out_exactSAT0.4
s298_d22_uUNSAT0.4
incrementer-enc07-uniform-depth-25UNSAT0.41
tlc03-uniform-depth-52UNSAT0.41
c1_BMC_p1_k4UNSAT0.42
ken.flash^03.C-f3UNSAT0.43
s499_d22_uUNSAT0.44
s820_d12_uUNSAT0.45
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-007UNSAT0.46
ken.flash^10.C-f2UNSAT0.47
s298_d25_uUNSAT0.48
biu.mv.xl_ao.bb-b003-p020-IPF03-c03.blif-biu.inv.prop.bb-bmc.with-IOC.unfold-009UNSAT0.49
s3330_d4_sSAT0.49
toilet_c_08_01.11UNSAT0.5
Core1108_tbm_21.tex.module.000027UNSAT0.5
s499_d24_uUNSAT0.51
s499_d25_uUNSAT0.54
s820_d14_uUNSAT0.56
sortnetsort8.AE.stepl.003SAT0.57
vonNeumann-ripple-carry-8-cUNSAT0.6
s820_d15_uUNSAT0.62
Core1108_tbm_21.tex.module.000026UNSAT0.67
tlc01-uniform-depth-73UNSAT0.67
query01_ntrivil_1344UNSAT0.68
s1269_d4_sSAT0.71
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-008UNSAT0.72
par8-4-50UNSAT0.73
lognBWLARGEB1UNSAT0.76
C5315.blif_0.10_1.00_0_0_inp_exactUNSAT0.76
k_ph_n-14SAT0.78
driverlog03_7SAT0.79
tlc02-uniform-depth-114SAT0.82
k_lin_n-14SAT0.82
flipflop-9-cUNSAT0.85
c5_BMC_p1_k32UNSAT0.85
ken.flash^10.C-f3UNSAT0.87
s510_d23_sSAT0.93
toilet_a_08_05.2UNSAT0.95
vonNeumann-ripple-carry-9-cUNSAT0.96
sortnetsort5.v.stepl.004UNSAT0.96
connect_7x6_4_WUNSAT0.97
k_branch_n-8SAT1.02
c3_BMC_p1_k256UNSAT1.02
k_lin_n-15SAT1.04
s510_d24_sSAT1.06
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-010UNSAT1.12
k_lin_n-17SAT1.19
szymanski-8-sUNSAT1.21
ring_r3_ser--opt-8_SAT1.24
c5_BMC_p2_k64UNSAT1.28
biu.mv.xl_ao.bb-b001-p010-MIF01-c01.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004SAT1.32
cnt07eSAT1.34
connect_8x7_7_WUNSAT1.39
vonNeumann-ripple-carry-10-cUNSAT1.43
s510_d28_sSAT1.43
s510_d31_sSAT1.55
biu.mv.xl_ao.bb-b001-p005-OPF05-c02.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004SAT1.6
biu.mv.xl_ao.bb-b001-p005-OPF05-c03.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004SAT1.65
k_ph_n-16SAT1.67
s3330_d8_sSAT1.7
s510_d32_sSAT1.72
fpu-10Xh-error01-uniform-depth-5UNSAT1.83
lut4_AND_f1SAT1.86
s510_d35_sSAT1.95
flipflop-10-cUNSAT2
k_branch_n-9SAT2.01
vonNeumann-ripple-carry-11-cUNSAT2.02
Umbrella_tbm_24.tex.module.000131SAT2.05
s510_d36_sSAT2.05
c5_BMC_p2_k128UNSAT2.17
toilet_a_06_01.10UNSAT2.27
Umbrella_tbm_24.tex.module.000066SAT2.3
toilet_c_10_01.12UNSAT2.39
tlc02-uniform-depth-241SAT2.45
fpu-10Xe-correct01-nonuniform-depth-6UNSAT2.59
query26_query34_1344SAT2.79
k_branch_p-10UNSAT2.88
vonNeumann-ripple-carry-12-cUNSAT2.92
tree-exa10-30SAT3
c4_BMC_p1_k32UNSAT3.08
biu.mv.xl_ao.bb-b001-p010-MIF05-c07.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004SAT3.13
s3330_d12_uSAT3.26
gttt_1_1_000111_3x3_torus_wUNSAT3.27
cnt08eSAT3.47
fpu-10Xh-correct04-uniform-depth-8UNSAT3.54
cnt10SAT3.68
incrementer-enc03-nonuniform-depth-13SAT3.83
vonNeumann-ripple-carry-13-cUNSAT3.92
term1.blif_0.10_0.20_0_1_inp_exactSAT4.39
C880.blif_0.10_1.00_0_0_inp_exactSAT4.52
flipflop-11-cUNSAT4.55
incrementer-enc08-uniform-depth-33UNSAT4.74
biu.mv.xl_ao.bb-b001-p005-OPF03-c09.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003SAT4.92
Core1108_tbm_02.tex.moduleQ3.2S.000015UNSAT5.27
query48_query15_1344UNSAT5.34
incrementer-enc02-nonuniform-depth-31SAT6.34
toilet_a_08_05.9SAT6.53
vonNeumann-ripple-carry-15-cUNSAT6.88
arbiter-07-comp-error01-qbf-hardness-depth-11UNSAT6.92
cnt11SAT7.28
s1269_d8_sSAT7.52
Core1108_tbm_03.tex.moduleQ3.2S.000002UNSAT8.61
C499.blif_0.10_0.20_0_1_out_exactSAT8.73
biu.mv.xl_ao.bb-b001-p010-MIF04-c06.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-005SAT9.35
flipflop-12-cUNSAT9.86
szymanski-10-sUNSAT10.78
arbiter-06-comp-error01-qbf-hardness-depth-12UNSAT11.09
c1_BMC_p2_k512UNSAT11.28
k_branch_p-11UNSAT11.49
k_branch_n-10SAT11.6
gttt_2_2_00101121_3x3_bUNSAT11.65
incrementer-enc02-uniform-depth-58UNSAT12.38
sortnetsort7.v.stepl.007SAT12.91
ev-pr-4x4-5-3-0-0-1-lgSAT13.8
dungeon_i10-m5-u10-v0.pddl_planlen=23UNSAT14.37
k_ph_n-21SAT15.15
Core1108_tbm_21.tex.module.000030SAT15.25
tlc04-nonuniform-depth-56SAT15.27
Umbrella_tbm_25.tex.moduleQ3.2S.000075UNSAT15.6
Core1108_tbm_21.tex.module.000008SAT15.77
incrementer-enc07-nonuniform-depth-17UNSAT19.12
ii32b1-00SAT19.36
rewriting_k_17UNSAT19.8
fpu-10Xe-correct01-nonuniform-depth-24UNSAT21.26
fpu-10Xh-correct04-nonuniform-depth-18UNSAT21.4
c1_BMC_p2_k1024UNSAT21.47
incrementer-enc03-nonuniform-depth-24SAT22.16
p10-10.pddl_planlen=10SAT23.35
fpu-10Xh-correct04-uniform-depth-15UNSAT24.16
incrementer-enc07-nonuniform-depth-21UNSAT25.22
stmt27_16_97UNSAT26.09
par16-1-50UNSAT27.13
C432.blif_0.10_0.20_0_1_inp_exactSAT27.42
ev-pr-6x6-5-5-0-1-2-lgUNSAT30.12
k_branch_p-12UNSAT31.8
C499.blif_0.10_0.20_0_0_out_exactSAT34.23
fpu-10Xh-correct04-uniform-depth-14UNSAT37.74
fpu-10Xh-correct04-nonuniform-depth-27UNSAT38.4
k_branch_n-11SAT40.17
arbiter-06-comp-error01-qbf-hardness-depth-15UNSAT42.95
Umbrella_tbm_05.tex.module.000039SAT43.13
lut4_2_f1SAT45.44
fpu-10Xh-correct04-uniform-depth-16UNSAT50.8
C499.blif_0.10_0.20_0_1_inp_exactSAT51.97
sortnetsort8.v.stepl.009SAT54.96
driverlog10_6UNSAT55.09
szymanski-12-sUNSAT58.24
dungeon_i10-m5-u10-v0.pddl_planlen=134UNSAT68.19
tlc04-nonuniform-depth-98SAT69.58
s1269_d9_sSAT81.91
sortnetsort8.v.stepl.007SAT84.84
b20_C_3_2FAIL100.53
fpu-10Xe-correct01-uniform-depth-22UNSAT101.91
connect_5x4_3_RUNSAT102.39
qshifter_4SAT110.83
p20-20.pddl_planlen=23FAIL116.13
b21_C_3_206FAIL120.23
k_branch_n-12SAT120.27
p20-5.pddl_planlen=17FAIL121.94
depots03_9UNSAT139.85
p20-5.pddl_planlen=32FAIL142.13
lut4_2_fXORSAT159.27
query31_reachqu_1344nSAT160.06
szymanski-14-sUNSAT181.26
arbiter-08-comp-error02-qbf-hardness-depth-9SAT184.35
rewriting_k_19UNSAT191.04
cnt14SAT192.96
p20-1.pddl_planlen=26FAIL193.13
s1269_d5_sSAT199.85
ev-pr-6x6-9-5-0-1-2-lgFAIL213.83
test2_quant_squaring2FAIL215.93
ev-pr-8x8-11-7-0-1-2-lgFAIL225.83
test2_quant_squaring3FAIL234.44
ev-pr-6x6-15-5-0-1-2-lgFAIL236.53
k_ph_p-10UNSAT236.87
p20-1.pddl_planlen=24FAIL237.23
ev-pr-4x4-15-3-0-0-1-lgFAIL237.53
ev-pr-4x4-11-3-0-0-1-lgFAIL240.74
ev-pr-8x8-9-7-0-1-2-lgFAIL240.83
s15850_PR_2_2FAIL244.23
ev-pr-6x6-19-5-0-1-2-lgFAIL250.64
ev-pr-6x6-11-5-0-1-2-lgFAIL252.77
p10-10.pddl_planlen=6FAIL253.9
dungeon_i10-m10-u10-v0.pddl_planlen=187FAIL259.23
p20-1.pddl_planlen=32FAIL259.75
ev-pr-4x4-17-3-0-0-1-lgFAIL261.7
k_branch_p-14UNSAT263.62
b22_C_2_12FAIL265.43
ev-pr-4x4-9-3-0-0-1-lgFAIL279.14
s3330_d5_sSAT286.19
ev-pr-4x4-7-3-0-0-1-lgFAIL288.63
ev-pr-4x4-13-3-0-0-1-lgFAIL293.61
s15850_PR_8_50FAIL293.96
ev-pr-8x8-7-7-0-1-2-lgFAIL294.66
ev-pr-8x8-13-7-0-1-2-lgFAIL295.74
ev-pr-6x6-17-5-0-1-2-lgFAIL296.54
ev-pr-8x8-15-7-0-1-2-lgFAIL303.26
ev-pr-6x6-13-5-0-1-2-lgFAIL316.83
ev-pr-4x4-15-3-0-0-1-sFAIL319.23
ev-pr-6x6-7-5-0-1-2-lgFAIL325.94
small-seq-fixpoint-3FAIL342.13
ev-pr-8x8-5-7-0-1-2-lgFAIL359.33
cache-coherence-2-fixpoint-1FAIL362.53
test1_quant_squaring2FAIL369.34
small-seq-fixpoint-5FAIL373.43
s05378_PR_1_75FAIL375.05
ev-pr-4x4-9-3-0-0-1-sFAIL383.74
b20_PR_7_90FAIL387.04
cache-coherence-3-fixpoint-3FAIL388.33
k8_3_4FAIL393.93
k8_4_3FAIL398.23
s1196_1_5FAIL404.83
dungeon_i25-m12-u3-v0.pddl_planlen=165FAIL413.83
test1_quant_squaring3FAIL418.33
adder-12-satFAIL422.83
c3_Debug_s3_f2_e2_v2FAIL426.49
dungeon_i25-m12-u5-v0.pddl_planlen=170FAIL435.04
s09234_PR_8_5FAIL437.64
lut4_2_f2UNSAT440.59
b22_PR_8_20FAIL446.44
adder-14-satFAIL449.74
ev-pr-4x4-17-3-0-0-1-sFAIL450.43
dungeon_i25-m12-u3-v0.pddl_planlen=130FAIL459.43
small-swap1-fixpoint-3FAIL462.23
ken.oop^2.C-d4FAIL462.95
cache-coherence-2-fixpoint-6FAIL465.53
ev-pr-4x4-11-3-0-0-1-sFAIL474.38
ev-pr-4x4-13-3-0-0-1-sFAIL478.03
k12_4_2FAIL486.73
ev-pr-4x4-7-3-0-0-1-sFAIL493.23
ev-pr-8x8-17-7-0-1-2-lgFAIL499.54
b20_PR_7_20FAIL506.72
query21_ntrivil_1344UNSAT508.17
dungeon_i25-m12-u3-v0.pddl_planlen=190FAIL509.14
c2_Debug_s3_f1_e1_v2FAIL521.63
ken.oop^2.C-d3FAIL540.44
sdlx-fixpoint-3FAIL557.14
k8_3_2FAIL567.13
dungeon_i25-m12-u3-v0.pddl_planlen=72FAIL571.13
k8_2_3FAIL571.93
ev-pr-8x8-19-7-0-1-2-lgFAIL577.78
k6_2_3FAIL583.13
rankfunc22_signed_64FAIL587.24
c1_Debug_s3_f1_e1_v1FAIL596.31
pipesnotankage18_7FAIL596.81
pipesnotankage18_8FAIL596.82
c2_BMC_p1_k2048FAIL598.01
AR-fixpoint-5FAIL598.22
c4_Debug_s3_f1_e1_v2FAIL598.43
pipesnotankage14_10FAIL598.43
c4_Debug_s3_f1_e2_v2FAIL598.43
c4_Debug_s3_f1_e2_v3FAIL598.51
ev-pr-6x6-19-5-0-1-2-sFAIL598.81
ev-pr-6x6-17-5-0-1-2-sFAIL598.91
c2_Debug_s3_f2_e1_v3FAIL598.92
c4_Debug_s3_f2_e2_v2FAIL599.01
ev-pr-6x6-13-5-0-1-2-sFAIL599.11
ev-pr-6x6-15-5-0-1-2-sFAIL599.11
c1_Debug_s5_f1_e1_v2FAIL599.11
ev-pr-6x6-11-5-0-1-2-sFAIL599.21
dungeon_i25-m12-u5-v0.pddl_planlen=65FAIL599.22
k14_2_3FAIL599.31
szymanski-24-sFAIL599.31
ev-pr-6x6-9-5-0-1-2-sFAIL599.32
k_ph_p-20FAIL599.43
ev-pr-6x6-7-5-0-1-2-sFAIL599.43
szymanski-20-sFAIL599.52
ev-pr-6x6-5-5-0-1-2-sFAIL599.52
connect_9x8_6_RFAIL599.53
k_ph_p-19FAIL599.53
qshifter_8FAIL599.53
k_ph_p-18FAIL599.53
k_branch_n-20FAIL599.61
s3330_d10_uFAIL599.61
stmt17_70_98FAIL599.61
network_irda_miniport_nscirda_comm.cFAIL599.61
szymanski-16-sFAIL599.61
input_mouser_cseries.cFAIL599.61
s3330_d9_sFAIL599.61
k_branch_p-21FAIL599.61
stmt19_64_99FAIL599.61
s3330_d14_uFAIL599.61
szymanski-18-sFAIL599.61
dungeon_i15-m7-u4-v0.pddl_planlen=81FAIL599.62
kernel_agplib_intrface.cFAIL599.62
hid_hclient_ecdisp.cFAIL599.62
network_trans_sys_notify.cFAIL599.62
filesys_smbmrx_cvsndrcv.cFAIL599.62
network_irda_miniport_nscirda_settings.cFAIL599.62
connect_8x7_6_RFAIL599.62
connect_8x7_4_RFAIL599.63
rankfunc3_signed_64FAIL599.63
input_pnpi8042_moudep.cFAIL599.63
connect_8x7_5_RFAIL599.63
gttt_2_1_00102030_4x4_torus_bFAIL599.63
uclid-pipe3bFAIL599.71
s1269_d15_uFAIL599.71
C6288.blif_0.10_0.20_0_1_inp_exactFAIL599.71
rewriting_k_75FAIL599.71
k_branch_p-18FAIL599.71
rewriting_k_50FAIL599.71
rewriting_k_23FAIL599.71
C6288.blif_0.10_0.20_0_0_out_exactFAIL599.71
rewriting_k_30FAIL599.71
C6288.blif_0.10_0.20_0_1_out_exactFAIL599.71
k_ph_p-15FAIL599.71
uclid-pipe2FAIL599.71
uclid-pipe3aFAIL599.71
toilet_c_10_01.17FAIL599.71
arbiter-07-comp-error01-qbf-hardness-depth-20FAIL599.71
toilet_a_08_01.13FAIL599.71
C499.blif_0.10_0.20_0_0_inp_exactFAIL599.71
C432.blif_0.10_0.20_0_0_out_exactFAIL599.71
arbiter-10-comp-error01-qbf-hardness-depth-22FAIL599.71
Adder2-8-sFAIL599.71
C5315.blif_0.10_0.20_0_0_inp_exactFAIL599.71
test5_quant_squaring5FAIL599.71
C880.blif_0.10_0.20_0_0_inp_exactFAIL599.71
C5315.blif_0.10_0.20_0_1_out_exactFAIL599.71
C6288.blif_0.10_1.00_0_0_inp_exactFAIL599.71
Adder2-8-cFAIL599.71
test3_quant_squaring4FAIL599.71
adder-10-satFAIL599.71
gttt_2_1_00011020_4x4_bFAIL599.71
C6288.blif_0.10_1.00_0_1_out_exactFAIL599.71
term1.blif_0.10_0.20_0_0_inp_exactFAIL599.71
Adder2-16-sFAIL599.71
rewriting_k_100FAIL599.71
query51_query50_1344FAIL599.71
query42_query06_1344nFAIL599.71
Adder2-10-sFAIL599.71
query11_query21_1344FAIL599.71
test3_quant_squaring2FAIL599.71
query03_query25_1344FAIL599.71
ev-pr-4x4-5-3-0-0-1-sFAIL599.71
gttt_2_1_0010_4x4_torus_bFAIL599.71
nusmv.tcas^3.B-f2FAIL599.71
stmt52_244_394FAIL599.71
stmt17_63_82FAIL599.71
stmt17_70_90FAIL599.71
stmt23_66_96FAIL599.71
stmt17_82_98FAIL599.71
stmt28_68_81FAIL599.71
stmt23_72_76FAIL599.71
C432.blif_0.10_1.00_0_0_out_exactFAIL599.71
rankfunc13_signed_32FAIL599.71
rankfunc51_signed_32FAIL599.71
rankfunc13_unsigned_64FAIL599.71
rankfunc33_signed_32FAIL599.71
rankfunc14_signed_64FAIL599.71
f600-50FAIL599.71
emptyroom_e4_par---21_FAIL599.71
stmt17_86_98FAIL599.71
s3330_d7_sFAIL599.71
stmt21_79_304FAIL599.71
k5_2_3FAIL599.71
stmt21_319_418FAIL599.71
stmt29_226_376FAIL599.71
stmt19_90_266FAIL599.71
qshifter_7FAIL599.71
C6288.blif_0.10_1.00_0_0_out_exactFAIL599.71
s1269_d13_uFAIL599.71
stmt41_738_749FAIL599.71
sortnetsort10.v.stepl.005FAIL599.71
stmt19_217_309FAIL599.71
test4_quant_squaring2FAIL599.71
stmt16_950_951FAIL599.71
s1269_d14_uFAIL599.71
emptyroom_e3_ser--opt-20_FAIL599.71
sortnetsort9.AE.stepl.012FAIL599.71
sortnetsort9.AE.stepl.009FAIL599.71
vis.4-arbit^2.E-f2FAIL599.71
audio_ddksynth_csynth2.cppFAIL599.71
texas.two_proc^4.E-f2FAIL599.71
incrementer-enc06-uniform-depth-24FAIL599.71
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-005FAIL599.71
small-swap2-fixpoint-4FAIL599.71
texas.PI_main^08.E-f3FAIL599.71
small-synabs-fixpoint-9FAIL599.71
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-003FAIL599.71
nusmv.tcas^6.B-f4FAIL599.71
sortnetsort9.v.stepl.007FAIL599.71
cube_c11_par---13_FAIL599.71
connect_5x4_4_RFAIL599.71
sortnetsort9.v.stepl.005FAIL599.71
texas.PI_main^05.E-f3FAIL599.71
stmt24_765_766FAIL599.72
stmt44_916_917FAIL599.72
stmt27_296_297FAIL599.72
s1269_d12_uFAIL599.72
eijk.bs4863.S-d4FAIL599.72
toilet_a_10_05.3FAIL599.72
k5_3_2FAIL599.72
stmt19_3_214FAIL599.72
C5315.blif_0.10_0.20_0_1_inp_exactFAIL599.72
k_branch_p-16FAIL599.72
rewriting_k_25FAIL599.72
C880.blif_0.10_0.20_0_1_inp_exactFAIL599.72
rewriting_k_21FAIL599.72
s1269_d10_sFAIL599.72
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-008FAIL599.72
qshifter_5FAIL599.72
rankfunc5_signed_32FAIL599.72
network_ndis_rtlnwifi_hw_hw_ccmp.cFAIL599.72
k_ph_p-13FAIL599.72
rankfunc17_unsigned_16FAIL599.72
rankfunc5_unsigned_64FAIL599.72
stmt17_62_98FAIL599.72
lut4_AND_fXORFAIL599.72
emptyroom_e4_ser--opt-44_FAIL599.72
cube_c7_ser--opt-24_FAIL599.72
cube_c9_par--opt-11_FAIL599.72
C5315.blif_0.10_0.20_0_0_out_exactFAIL599.72
C432.blif_0.10_0.20_0_0_inp_exactFAIL599.72
qshifter_6FAIL599.72
test4_quant_squaring4FAIL599.72
k_branch_n-16FAIL599.72
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-005FAIL599.72
test5_quant_squaring4FAIL599.72
k_ph_p-12FAIL599.72
query44_query26_1344nFAIL599.81
C6288.blif_0.10_1.00_0_1_inp_exactFAIL599.81
emptyroom_e3_ser---19_FAIL599.81
stmt19_83_412FAIL599.81
cnt16rFAIL599.81
C432.blif_0.10_0.20_0_1_out_exactFAIL599.81
C6288.blif_0.10_0.20_0_0_inp_exactFAIL599.81
c4_Debug_s5_f2_e2_v1FAIL599.81
adder-12-unsatFAIL599.81
stmt25_52_53FAIL599.81