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

InstanceResultTime
k_ph_n-4SAT0
toilet_c_06_01.8UNSAT0
toilet_c_04_01.4UNSAT0
toilet_c_08_01.6UNSAT0
toilet_c_06_01.4UNSAT0
toilet_a_04_01.4UNSAT0
qshifter_3SAT0
mutex-4-sSAT0
toilet_a_06_01.6UNSAT0
stmt44_107_108SAT0
toilet_a_04_01.6UNSAT0
impl12SAT0
toilet_g_15_01.2SAT0
toilet_g_20_01.2SAT0
k_dum_n-5SAT0
k_dum_n-3SAT0
k_dum_n-2SAT0
tree-exa2-35UNSAT0
k_d4_n-1SAT0
k_branch_n-2SAT0
toilet_g_06_01.2SAT0
toilet_g_02_01.2SAT0
toilet_g_10_01.2SAT0
toilet_g_08_01.2SAT0
toilet_g_04_01.2SAT0
tree-exa2-25UNSAT0
toilet_a_02_10.2SAT0
lognBWLARGEA0UNSAT0
lognBWLARGEB0UNSAT0
z4ml.blif_0.10_1.00_0_1_inp_exactSAT0
impl04SAT0
ring_r4_ser--opt-11_UNSAT0
mutex-8-sSAT0
impl06SAT0
tree-exa2-10UNSAT0
tree-exa2-30UNSAT0
tree-exa2-20UNSAT0
impl02SAT0
impl18SAT0
k_dum_p-4UNSAT0
toilet_a_04_05.2SAT0
k_poly_p-4UNSAT0
impl08SAT0
cnt01SAT0
CHAIN14v.15SAT0
cnt02eSAT0
impl14SAT0
z4ml.blif_0.10_1.00_0_0_inp_exactUNSAT0
CHAIN12v.13SAT0
toilet_c_08_01.2UNSAT0
aim-100-1_6-yes1-2-00SAT0
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
stmt1_30_31SAT0
k_poly_p-2UNSAT0
k_ph_p-1UNSAT0
rewriting_k_30UNSAT0
rewriting_k_25UNSAT0
tree-exa2-40UNSAT0
tree-exa2-45UNSAT0
rewriting_k_23UNSAT0
rewriting_k_21UNSAT0
rewriting_k_19UNSAT0
qshifter_4SAT0
rewriting_k_17UNSAT0
rewriting_k_50UNSAT0
tree-exa10-30SAT0
mutex-2-sSAT0
counter_e_2SAT0
flipflop-3-cUNSAT0
k_poly_n-5SAT0
impl20SAT0
k_poly_n-6SAT0
k_poly_n-2SAT0
tree-exa10-10SAT0
k_ph_p-3UNSAT0
tree-exa2-50UNSAT0
impl10SAT0
k_ph_n-3SAT0
k_ph_n-1SAT0
stmt44_107_113SAT0
k_d4_p-1UNSAT0
flipflop-4-cUNSAT0
k_grz_n-2SAT0
rewriting_k_10UNSAT0
incrementer-enc05-uniform-depth-2UNSAT0
k_dum_p-3UNSAT0
k_dum_p-2UNSAT0
s27_d2_sSAT0
k_dum_n-1SAT0
k_lin_p-2UNSAT0
impl16SAT0
k_path_p-2UNSAT0
k_lin_p-3UNSAT0
stmt17_18_19SAT0
k_path_n-3SAT0
CHAIN19v.20SAT0.01
qshifter_5SAT0.01
rankfunc51_signed_32SAT0.01
BLOCKS3iii.4UNSAT0.01
rankfunc13_signed_32SAT0.01
rankfunc17_unsigned_16SAT0.01
z4ml.blif_0.10_0.20_0_1_out_exactSAT0.01
CHAIN22v.23SAT0.01
rankfunc5_signed_32SAT0.01
k_poly_p-16UNSAT0.01
k_d4_p-4UNSAT0.01
k_ph_n-8SAT0.01
mutex-16-sSAT0.01
CHAIN17v.18SAT0.01
CHAIN21v.22SAT0.01
k3_1_1SAT0.01
stmt27_296_297SAT0.01
k_dum_p-12UNSAT0.01
toilet_c_08_05.4SAT0.01
z4ml.blif_0.10_0.20_0_1_inp_exactSAT0.01
k_lin_p-4UNSAT0.01
k_grz_p-4UNSAT0.01
k_path_p-5UNSAT0.01
k_t4p_n-2SAT0.01
k_path_n-6SAT0.01
k_path_n-5SAT0.01
k_grz_p-5UNSAT0.01
k_grz_n-6SAT0.01
k_grz_n-5SAT0.01
k_dum_p-14UNSAT0.01
k_ph_n-6SAT0.01
k_poly_p-15UNSAT0.01
k_poly_n-14SAT0.01
k_poly_n-7SAT0.01
k_poly_n-18SAT0.01
k_poly_p-9UNSAT0.01
k_poly_p-11UNSAT0.01
k_poly_p-19UNSAT0.01
k_poly_p-14UNSAT0.01
k_ph_p-5UNSAT0.01
k_dum_p-6UNSAT0.01
k_dum_n-11SAT0.01
s298_d2_sSAT0.01
CHAIN16v.17SAT0.01
k_poly_p-8UNSAT0.01
texas.parsesys^1.E-d4SAT0.01
z4ml.blif_0.10_0.20_0_0_inp_exactUNSAT0.01
k_dum_p-16UNSAT0.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
z4ml.blif_0.10_0.20_0_0_out_exactUNSAT0.01
k_path_n-4SAT0.01
z4ml.blif_0.10_1.00_0_0_out_exactUNSAT0.01
k_dum_n-9SAT0.01
k_d4_n-3SAT0.01
k_d4_n-2SAT0.01
toilet_c_08_01.7UNSAT0.01
toilet_a_06_01.10UNSAT0.01
k_dum_n-12SAT0.01
cnt05SAT0.01
k_poly_n-21SAT0.01
k_poly_n-17SAT0.01
rewriting_k_75UNSAT0.01
rewriting_k_100UNSAT0.01
k_poly_p-7UNSAT0.01
CHAIN18v.19SAT0.01
k_grz_n-4SAT0.01
k_poly_n-20SAT0.01
CHAIN20v.21SAT0.01
z4ml.blif_0.10_1.00_0_1_out_exactSAT0.01
k_t4p_p-4UNSAT0.01
k_poly_n-16SAT0.01
flipflop-5-cUNSAT0.01
k_path_p-10UNSAT0.02
CHAIN23v.24SAT0.02
stmt24_765_766SAT0.02
k_grz_n-7SAT0.02
k_lin_p-11UNSAT0.02
k_path_n-9SAT0.02
k_d4_p-8UNSAT0.02
k_dum_n-17SAT0.02
k_path_n-12SAT0.02
stmt44_916_917SAT0.02
k_path_n-13SAT0.02
s27_d3_uUNSAT0.02
k_grz_p-13UNSAT0.02
k_path_p-14UNSAT0.02
k_grz_p-12UNSAT0.02
k_path_p-13UNSAT0.02
k_lin_n-3SAT0.02
k_grz_p-10UNSAT0.02
k_t4p_n-4SAT0.02
k_ph_n-9SAT0.02
stmt16_950_951SAT0.02
k_dum_n-21SAT0.02
k_lin_p-8UNSAT0.02
k_dum_p-17UNSAT0.02
rankfunc5_unsigned_64SAT0.02
k_d4_p-7UNSAT0.02
k_dum_n-18SAT0.02
k_t4p_p-6UNSAT0.02
toilet_c_08_01.11UNSAT0.02
k_branch_n-3SAT0.02
k_dum_p-21UNSAT0.02
k_lin_p-12UNSAT0.02
k_grz_n-8SAT0.02
k_dum_p-20UNSAT0.02
rankfunc33_signed_32SAT0.02
k_lin_p-9UNSAT0.03
k_lin_p-14UNSAT0.03
k_d4_p-10UNSAT0.03
p5-5.pddl_planlen=5SAT0.03
k_t4p_p-10UNSAT0.03
k_t4p_n-6SAT0.03
k_t4p_p-9UNSAT0.03
flipflop-6-cUNSAT0.03
k_grz_p-11UNSAT0.03
vis.4-arbit^2.E-f2SAT0.03
BLOCKS3ii.4.3UNSAT0.03
connect_5x4_3_DUNSAT0.03
toilet_a_08_05.2UNSAT0.03
k_path_n-14SAT0.03
BLOCKS3iii.5SAT0.03
gttt_2_2_0010_3x3_torus_wUNSAT0.03
k_grz_n-10SAT0.03
szymanski-5-sUNSAT0.03
k_path_n-16SAT0.03
k_d4_p-11UNSAT0.03
vis.prodcell^01.E-d2SAT0.03
k_d4_p-13UNSAT0.03
k_t4p_n-5SAT0.03
k_path_p-16UNSAT0.03
adder-2-unsatUNSAT0.03
rankfunc13_unsigned_64SAT0.03
rankfunc14_signed_64SAT0.03
k_branch_n-4SAT0.03
C432.blif_0.10_1.00_0_1_out_exactSAT0.03
k_grz_p-17UNSAT0.03
vonNeumann-ripple-carry-5-cUNSAT0.03
k_path_p-18UNSAT0.03
k_grz_p-16UNSAT0.03
k_path_p-19UNSAT0.03
k_path_p-15UNSAT0.03
Adder2-2-cUNSAT0.04
k_t4p_p-12UNSAT0.04
p5-5.pddl_planlen=6SAT0.04
C432.blif_0.10_1.00_0_0_inp_exactUNSAT0.04
lut4_XOR_fORUNSAT0.04
k_grz_p-19UNSAT0.04
stmt41_738_749SAT0.04
k_grz_p-18UNSAT0.04
mutex-32-sSAT0.04
k_t4p_p-15UNSAT0.04
ken.flash^10.C-f2UNSAT0.04
k_path_n-19SAT0.04
k_path_p-21UNSAT0.04
k_d4_p-17UNSAT0.04
C432.blif_0.10_1.00_0_1_inp_exactSAT0.04
k_d4_p-16UNSAT0.04
k_lin_p-19UNSAT0.04
k_lin_p-10UNSAT0.04
C432.blif_0.10_1.00_0_0_out_exactUNSAT0.04
qshifter_6SAT0.04
k_t4p_n-8SAT0.04
k_t4p_p-17UNSAT0.05
k_d4_n-7SAT0.05
k_d4_n-8SAT0.05
k_d4_p-20UNSAT0.05
k_ph_n-11SAT0.05
cnt10SAT0.05
cnt11SAT0.05
b12_PR_9_2SAT0.05
lut4_XOR_f1SAT0.05
k_t4p_p-16UNSAT0.05
tlc03-uniform-depth-9UNSAT0.05
k_t4p_n-9SAT0.05
k_t4p_p-18UNSAT0.05
k_lin_n-5SAT0.05
connect_6x5_5_DUNSAT0.05
cube_c3_ser--opt-6_SAT0.06
query48_query15_1344UNSAT0.06
k_t4p_p-20UNSAT0.06
stmt25_52_53SAT0.06
term1.blif_0.10_0.20_0_1_out_exactSAT0.06
BLOCKS4iii.6UNSAT0.06
k_lin_n-6SAT0.06
term1.blif_0.10_1.00_0_1_inp_exactSAT0.06
toilet_c_10_01.12UNSAT0.06
lut4_AND_fXORUNSAT0.06
s01238_PR_8_2SAT0.07
term1.blif_0.10_1.00_0_1_out_exactSAT0.07
lut4_2_fXORSAT0.07
query01_ntrivil_1344UNSAT0.07
k_t4p_n-13SAT0.07
rankfunc22_signed_64SAT0.07
k_grz_n-18SAT0.07
k_d4_n-10SAT0.07
ken.flash^10.C-f3UNSAT0.07
C499.blif_0.10_1.00_0_1_out_exactSAT0.07
vonNeumann-ripple-carry-6-cUNSAT0.07
k_t4p_n-12SAT0.07
C499.blif_0.10_1.00_0_1_inp_exactSAT0.07
lut4_2_f1SAT0.07
flipflop-7-cUNSAT0.07
sortnetsort5.v.stepl.004UNSAT0.07
szymanski-6-sUNSAT0.07
ring_r3_ser--opt-8_SAT0.08
k_t4p_n-14SAT0.08
k_grz_n-20SAT0.08
texas.PI_main^16.E-f2SAT0.08
cnt14SAT0.08
c4_BMC_p1_k32SAT0.08
term1.blif_0.10_0.20_0_1_inp_exactSAT0.09
k_grz_n-21SAT0.09
toilet_a_08_05.9SAT0.09
k_t4p_n-15SAT0.09
driverlog01_7SAT0.09
term1.blif_0.10_1.00_0_0_inp_exactUNSAT0.09
BLOCKS3i.5.4SAT0.09
s27_d4_uUNSAT0.09
term1.blif_0.10_1.00_0_0_out_exactUNSAT0.1
k_branch_p-5UNSAT0.1
connect_7x6_4_WUNSAT0.1
lut4_AND_f1SAT0.1
rankfunc3_signed_64SAT0.1
BLOCKS3ii.5.2UNSAT0.1
query21_ntrivil_1344UNSAT0.1
arbiter-07-comp-error01-qbf-hardness-depth-4UNSAT0.1
BLOCKS3i.5.3UNSAT0.1
mutex-64-sSAT0.11
BLOCKS4i.6.4UNSAT0.11
biu.mv.xl_ao.bb-b001-p010-IPF02-c07.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003SAT0.11
BLOCKS3ii.5.3SAT0.11
C499.blif_0.10_1.00_0_0_inp_exactUNSAT0.11
arbiter-06-comp-error02-qbf-hardness-depth-5UNSAT0.12
C880.blif_0.10_1.00_0_1_out_exactSAT0.12
vonNeumann-ripple-carry-7-cUNSAT0.12
k_d4_n-14SAT0.12
C880.blif_0.10_1.00_0_1_inp_exactSAT0.12
driverlog03_7SAT0.12
k_d4_n-15SAT0.13
connect_8x7_7_WUNSAT0.13
small-swap1-fixpoint-3SAT0.13
eijk.S382.S-d4SAT0.13
arbiter-07-comp-error02-qbf-hardness-depth-6UNSAT0.14
flipflop-8-cUNSAT0.14
k_lin_n-7SAT0.14
k_d4_n-16SAT0.14
stmt27_16_97UNSAT0.14
lights3_021_0_027UNSAT0.15
query11_query21_1344UNSAT0.15
biu.mv.xl_ao.bb-b001-p005-OPF03-c09.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003SAT0.15
c4_BMC_p2_k128UNSAT0.16
biu.mv.xl_ao.bb-b001-p010-IPF05-c07.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003SAT0.16
k_branch_p-6UNSAT0.16
ev-pr-4x4-5-3-0-0-1-lgSAT0.17
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.17
k_lin_n-8SAT0.18
mutex-128-sSAT0.19
toilet_a_08_01.13UNSAT0.19
gttt_2_2_00101121_3x3_bUNSAT0.19
irst.dme6.B-d2SAT0.2
k_d4_n-20SAT0.2
gttt_2_1_000111_3x3_torus_bSAT0.2
vonNeumann-ripple-carry-8-cUNSAT0.2
C499.blif_0.10_1.00_0_0_out_exactUNSAT0.21
lights3_021_0_009SAT0.21
small-synabs-fixpoint-9UNSAT0.21
BLOCKS4ii.7.2UNSAT0.22
k_branch_p-8UNSAT0.22
s386_d2_sSAT0.22
k_branch_n-8SAT0.22
biu.mv.xl_ao.bb-b001-p010-IPF02-c08.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003SAT0.22
tlc03-nonuniform-depth-17UNSAT0.22
k_ph_n-14SAT0.23
aim-50-6_0-yes1-3-50UNSAT0.23
query26_query34_1344SAT0.24
par8-1-c-50UNSAT0.25
k_lin_n-9SAT0.25
biu.mv.xl_ao.bb-b001-p010-OPF02-c08.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003SAT0.25
dungeon_i10-m5-u10-v0.pddl_planlen=23UNSAT0.26
tlc03-uniform-depth-21UNSAT0.26
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-005UNSAT0.26
flipflop-9-cUNSAT0.26
query51_query50_1344UNSAT0.27
szymanski-8-sUNSAT0.28
vonNeumann-ripple-carry-9-cUNSAT0.32
biu.mv.xl_ao.bb-b001-p010-MIF04-c06.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-005SAT0.35
s27_d5_uUNSAT0.35
C5315.blif_0.10_1.00_0_1_out_exactSAT0.39
s05378_PR_1_75UNSAT0.39
qshifter_7SAT0.39
lut4_3_fANDSAT0.4
C5315.blif_0.10_1.00_0_1_inp_exactSAT0.42
cnt07eSAT0.42
fpu-10Xh-error01-uniform-depth-5UNSAT0.45
query03_query25_1344UNSAT0.45
cache-coherence-2-fixpoint-1UNSAT0.45
C432.blif_0.10_0.20_0_1_inp_exactSAT0.46
flipflop-10-cUNSAT0.46
vonNeumann-ripple-carry-10-cUNSAT0.47
s09234_PR_8_2SAT0.48
sortnetsort7.v.stepl.007SAT0.48
Core1108_tbm_21.tex.module.000026UNSAT0.49
s09234_PR_8_5SAT0.49
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-005UNSAT0.52
k_lin_n-11SAT0.53
fpu-10Xe-correct01-nonuniform-depth-6UNSAT0.55
gttt_1_1_000111_3x3_torus_wUNSAT0.55
stmt21_79_304UNSAT0.56
ev-pr-6x6-5-5-0-1-2-lgUNSAT0.57
s05378_PR_9_2SAT0.57
ken.flash^03.C-f3UNSAT0.6
k_ph_n-16SAT0.61
k_branch_p-16UNSAT0.63
k_branch_n-16SAT0.66
lut4_2_f2UNSAT0.67
vonNeumann-ripple-carry-11-cUNSAT0.67
lognBWLARGEA1UNSAT0.68
c1_BMC_p1_k4SAT0.69
tlc01-uniform-depth-73UNSAT0.71
stmt19_217_309UNSAT0.72
tlc03-uniform-depth-52UNSAT0.73
lights3_035_0_002UNSAT0.75
fpu-10Xh-correct04-uniform-depth-8UNSAT0.75
flipflop-11-cUNSAT0.77
tlc04-uniform-depth-36UNSAT0.79
p10-10.pddl_planlen=10SAT0.8
ev-pr-4x4-9-3-0-0-1-lgSAT0.8
gttt_1_1_001020_3x3_wUNSAT0.82
szymanski-10-sUNSAT0.82
emptyroom_e3_ser--opt-20_SAT0.85
incrementer-enc03-nonuniform-depth-13UNSAT0.87
network_trans_sys_notify.cUNSAT0.87
lights3_035_0_051UNSAT0.91
vonNeumann-ripple-carry-12-cUNSAT0.94
filesys_smbmrx_cvsndrcv.cUNSAT0.95
b20_PR_7_90UNSAT0.99
lights3_035_0_027UNSAT1.08
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-008UNSAT1.13
toilet_a_10_05.3UNSAT1.14
dungeon_i10-m5-u10-v0.pddl_planlen=134UNSAT1.21
flipflop-12-cUNSAT1.26
vonNeumann-ripple-carry-13-cUNSAT1.26
fpu-10Xh-correct04-uniform-depth-14UNSAT1.28
fpu-10Xh-correct04-uniform-depth-15UNSAT1.35
C499.blif_0.10_0.20_0_1_inp_exactSAT1.44
fpu-10Xh-correct04-uniform-depth-16UNSAT1.44
k_lin_n-14SAT1.48
incrementer-enc08-uniform-depth-33SAT1.56
tlc04-nonuniform-depth-56UNSAT1.57
dungeon_i10-m10-u10-v0.pddl_planlen=187UNSAT1.63
fpu-10Xh-correct04-nonuniform-depth-18UNSAT1.63
incrementer-enc06-uniform-depth-24UNSAT1.78
k_lin_n-15SAT1.85
fpu-10Xe-correct01-uniform-depth-22UNSAT1.9
small-swap2-fixpoint-4SAT2
gttt_2_1_0010_4x4_torus_bUNSAT2.04
fpu-10Xe-correct01-nonuniform-depth-24UNSAT2.05
sortnetsort8.v.stepl.007SAT2.11
stmt19_90_266UNSAT2.15
vonNeumann-ripple-carry-15-cUNSAT2.19
aim-100-6_0-yes1-3-50SAT2.2
fpu-10Xh-correct04-nonuniform-depth-27UNSAT2.31
s15850_PR_8_50SAT2.34
ev-pr-8x8-5-7-0-1-2-lgUNSAT2.38
szymanski-12-sUNSAT2.39
s15850_PR_2_2SAT2.72
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-007UNSAT2.78
incrementer-enc02-uniform-depth-58UNSAT2.81
k_lin_n-17SAT3.07
ev-pr-6x6-7-5-0-1-2-lgUNSAT3.16
cube_c11_par---13_UNSAT3.28
lognBWLARGEB1UNSAT3.35
tlc04-nonuniform-depth-98UNSAT3.46
tlc02-uniform-depth-114UNSAT3.79
incrementer-enc07-nonuniform-depth-17UNSAT3.94
gttt_2_2_001020_4x4_wUNSAT4.42
s820_d2_sSAT4.61
szymanski-14-sUNSAT4.7
ev-pr-4x4-7-3-0-0-1-lgSAT4.99
C432.blif_0.10_0.20_0_0_out_exactUNSAT5.15
aim-200-1_6-yes1-4-90SAT5.43
s298_d4_sSAT5.54
qshifter_8SAT5.9
C5315.blif_0.10_1.00_0_0_inp_exactUNSAT6.26
szymanski-16-sUNSAT7.43
c1_BMC_p2_k512UNSAT7.49
term1.blif_0.10_0.20_0_0_out_exactUNSAT7.58
jnh212-50UNSAT8.85
s641_d2_sSAT9.95
C5315.blif_0.10_1.00_0_0_out_exactUNSAT10.4
s713_d2_sSAT11.43
incrementer-enc07-uniform-depth-25UNSAT12.59
incrementer-enc07-nonuniform-depth-21UNSAT13.03
sortnetsort8.v.stepl.009SAT13.22
c1_BMC_p2_k1024UNSAT13.28
szymanski-18-sUNSAT14.03
incrementer-enc03-nonuniform-depth-24UNSAT14.14
tlc02-uniform-depth-241UNSAT14.61
cube_c7_ser--opt-24_SAT16.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-010UNSAT20.75
ev-pr-8x8-7-7-0-1-2-lgUNSAT21.95
szymanski-20-sUNSAT22.4
s386_d3_sSAT22.59
biu.mv.xl_ao.bb-b001-p010-MIF01-c01.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004SAT25.36
par8-4-50UNSAT25.6
s3330_d2_sSAT28.54
c5_BMC_p1_k32SAT31.53
s1196_1_5SAT31.81
incrementer-enc02-nonuniform-depth-31UNSAT32.06
connect_5x4_3_RUNSAT36.08
toilet_c_10_01.17UNSAT36.54
c2_BMC_p1_k2048SAT45.01
emptyroom_e4_par---21_UNSAT50.92
sortnetsort8.AE.stepl.003SAT53.95
emptyroom_e3_ser---19_UNSAT54.32
szymanski-24-sUNSAT63.89
input_pnpi8042_moudep.cFAIL67.82
network_irda_miniport_nscirda_settings.cFAIL70.63
cube_c9_par--opt-11_SAT72.85
hid_hclient_ecdisp.cFAIL73.02
k_ph_n-21SAT79.07
kernel_agplib_intrface.cFAIL90.62
k5_2_3SAT91.5
k_ph_p-19FAIL94.02
input_mouser_cseries.cFAIL104.12
ev-pr-8x8-15-7-0-1-2-lgFAIL115.33
ev-pr-6x6-9-5-0-1-2-lgUNSAT122.08
connect_8x7_4_RFAIL125.42
sortnetsort9.v.stepl.007SAT126.71
ev-pr-6x6-5-5-0-1-2-sFAIL131.12
b22_PR_8_20FAIL135.82
ev-pr-6x6-17-5-0-1-2-lgFAIL138.12
ev-pr-6x6-7-5-0-1-2-sFAIL139.22
ev-pr-8x8-17-7-0-1-2-lgFAIL147.62
emptyroom_e4_ser--opt-44_SAT161.54
c3_BMC_p1_k256SAT162.34
ev-pr-4x4-15-3-0-0-1-sFAIL165.42
query42_query06_1344nFAIL168.22
Adder2-10-sFAIL169.43
b20_C_3_2FAIL177.12
ev-pr-4x4-17-3-0-0-1-sFAIL177.22
Adder2-16-sFAIL179.72
ev-pr-8x8-19-7-0-1-2-lgFAIL182.12
b20_PR_7_20FAIL188.12
network_ndis_rtlnwifi_hw_hw_ccmp.cFAIL189.42
ev-pr-6x6-11-5-0-1-2-sFAIL195.42
s499_d17_sFAIL198.22
connect_9x8_6_RFAIL200.22
arbiter-07-comp-error01-qbf-hardness-depth-11UNSAT200.92
small-seq-fixpoint-5FAIL202.13
ev-pr-6x6-9-5-0-1-2-sFAIL216.93
eijk.bs4863.S-d4FAIL219.32
ev-pr-6x6-19-5-0-1-2-sFAIL219.83
nusmv.tcas^6.B-f4FAIL224.23
ev-pr-6x6-13-5-0-1-2-sFAIL229.02
ev-pr-8x8-11-7-0-1-2-lgFAIL229.52
ev-pr-6x6-19-5-0-1-2-lgFAIL231.72
par16-1-50UNSAT231.79
ev-pr-4x4-11-3-0-0-1-sFAIL234.72
connect_8x7_5_RFAIL236.62
p20-20.pddl_planlen=23FAIL240.98
ev-pr-6x6-15-5-0-1-2-lgFAIL241.32
s820_d10_sFAIL248.62
s820_d9_sFAIL248.82
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-008UNSAT260.61
ev-pr-4x4-7-3-0-0-1-sFAIL264.62
ev-pr-6x6-15-5-0-1-2-sFAIL265.32
ev-pr-6x6-13-5-0-1-2-lgFAIL266.42
s499_d18_sFAIL284.02
s499_d19_sFAIL295.02
ev-pr-4x4-13-3-0-0-1-sFAIL295.92
c3_Debug_s3_f2_e2_v2FAIL296.46
audio_ddksynth_csynth2.cppFAIL297.62
s1196_d7_uFAIL298.42
C6288.blif_0.10_1.00_0_1_out_exactFAIL303.92
arbiter-10-comp-error01-qbf-hardness-depth-10UNSAT304.69
k_ph_p-10UNSAT305.74
ev-pr-8x8-13-7-0-1-2-lgFAIL308.02
s820_d11_uFAIL308.72
C6288.blif_0.10_0.20_0_0_out_exactFAIL317.42
s386_d11_uFAIL317.52
adder-14-satFAIL318.12
k5_3_2SAT323.4
ev-pr-6x6-17-5-0-1-2-sFAIL324.62
s713_d4_sFAIL327.22
C6288.blif_0.10_1.00_0_0_inp_exactFAIL337.82
s298_d25_uFAIL342.22
adder-12-satFAIL344.32
s1269_d4_sFAIL349.92
s820_d12_uFAIL352.32
s386_d12_uFAIL358.33
cache-coherence-2-fixpoint-6FAIL360.53
s499_d24_uFAIL363.22
s499_d22_uFAIL366.52
s499_d7_sFAIL368.12
s499_d12_sFAIL368.42
pipesnotankage18_8FAIL372.32
s820_d14_uFAIL373.22
s1269_d10_sFAIL373.62
C6288.blif_0.10_0.20_0_1_out_exactFAIL374.72
s1196_d4_uFAIL379.82
ev-pr-4x4-9-3-0-0-1-sFAIL380.52
s298_d14_sFAIL382.12
pipesnotankage18_7FAIL382.32
s298_d17_sFAIL386.12
query44_query26_1344nFAIL387.92
s499_d15_sFAIL396.22
s713_d11_uFAIL396.22
s298_d10_sFAIL398.42
ev-pr-4x4-5-3-0-0-1-sFAIL399.03
s499_d9_sFAIL399.22
s510_d6_sFAIL402.62
s1269_d8_sFAIL408.93
s820_d7_sFAIL410.62
s820_d15_uFAIL413.33
s641_d6_sFAIL416.52
sortnetsort9.AE.stepl.009FAIL422.02
ev-pr-6x6-11-5-0-1-2-lgFAIL423.62
s298_d19_uFAIL426.92
s510_d11_sFAIL430.62
s1196_d3_uFAIL436.92
s1196_d5_uFAIL446.72
p20-5.pddl_planlen=32FAIL447.65
s820_d8_sFAIL452.42
s298_d18_sFAIL452.82
s510_d28_sFAIL455.92
C6288.blif_0.10_1.00_0_1_inp_exactFAIL461.12
s386_d9_uFAIL461.73
s713_d6_sFAIL461.73
s641_d7_uFAIL462.22
s386_d7_sFAIL464.12
s713_d7_uFAIL464.72
test2_quant_squaring3FAIL468.72
C6288.blif_0.10_1.00_0_0_out_exactFAIL468.92
s1269_d3_sFAIL473.52
k_branch_n-9SAT474.78
s641_d4_sFAIL475.92
s713_d5_sFAIL476.42
s386_d10_uFAIL476.72
s499_d25_uFAIL479.33
term1.blif_0.10_0.20_0_0_inp_exactUNSAT480.5
s386_d6_sFAIL483.02
ev-pr-8x8-9-7-0-1-2-lgFAIL486.03
s386_d8_uFAIL487.52
s1269_d5_sFAIL492.02
C5315.blif_0.10_0.20_0_0_out_exactFAIL507.42
s1269_d12_uFAIL508.22
s3330_d5_sFAIL512.43
s1196_d6_uFAIL516.32
s713_d8_uFAIL519.12
s298_d22_uFAIL521.72
s1196_d2_sFAIL528.22
s298_d12_sFAIL528.93
s510_d23_sFAIL534.72
s713_d3_sFAIL546.32
small-seq-fixpoint-3FAIL548.82
s641_d8_uFAIL555.82
s510_d31_sFAIL558.72
sortnetsort9.AE.stepl.012FAIL566.23
s1269_d13_uFAIL570.63
s3330_d4_sFAIL571.32
stmt17_86_98FAIL577.33
s1269_d9_sFAIL582.73
s641_d5_sFAIL592.73
s3330_d3_sFAIL597.03
c4_Debug_s3_f2_e2_v2FAIL598.81
c4_Debug_s3_f1_e1_v2FAIL599.11
c4_Debug_s3_f1_e2_v2FAIL599.11
AR-fixpoint-5FAIL599.11
c4_Debug_s3_f1_e2_v3FAIL599.21
pipesnotankage14_10FAIL599.21
c2_Debug_s3_f1_e1_v2FAIL599.31
dungeon_i25-m12-u3-v0.pddl_planlen=190FAIL599.43
c4_Debug_s5_f2_e2_v1FAIL599.52
dungeon_i25-m12-u3-v0.pddl_planlen=165FAIL599.52
c2_Debug_s3_f2_e1_v3FAIL599.52
dungeon_i25-m12-u5-v0.pddl_planlen=170FAIL599.53
dungeon_i25-m12-u3-v0.pddl_planlen=130FAIL599.53
s3330_d10_uFAIL599.61
s1269_d15_uFAIL599.61
c5_BMC_p2_k128FAIL599.61
dungeon_i25-m12-u5-v0.pddl_planlen=65FAIL599.61
Umbrella_tbm_25.tex.moduleQ3.2S.000075FAIL599.61
s3330_d12_uFAIL599.61
s3330_d14_uFAIL599.61
c1_Debug_s5_f1_e1_v2FAIL599.61
dungeon_i25-m12-u3-v0.pddl_planlen=72FAIL599.63
s3330_d8_sFAIL599.63
depots03_9FAIL599.71
dungeon_i15-m7-u4-v0.pddl_planlen=81FAIL599.71
s510_d32_sFAIL599.71
p20-1.pddl_planlen=24FAIL599.71
adder-10-satFAIL599.71
ev-pr-4x4-13-3-0-0-1-lgFAIL599.71
network_irda_miniport_nscirda_comm.cFAIL599.71
p20-1.pddl_planlen=32FAIL599.71
arbiter-06-comp-error01-qbf-hardness-depth-12FAIL599.71
k_ph_p-12FAIL599.71
driverlog10_6FAIL599.71
gttt_2_1_00011020_4x4_bFAIL599.71
k_branch_n-20FAIL599.71
biu.mv.xl_ao.bb-b001-p005-OPF05-c02.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004FAIL599.71
C880.blif_0.10_1.00_0_0_out_exactFAIL599.71
p20-5.pddl_planlen=17FAIL599.71
p10-10.pddl_planlen=6FAIL599.71
p20-1.pddl_planlen=26FAIL599.71
test5_quant_squaring4FAIL599.71
ken.oop^2.C-d4FAIL599.71
s713_d10_uFAIL599.71
biu.mv.xl_ao.bb-b003-p020-IPF03-c03.blif-biu.inv.prop.bb-bmc.with-IOC.unfold-009FAIL599.71
s713_d9_uFAIL599.71
k12_4_2FAIL599.71
k8_2_3FAIL599.71
Adder2-8-sFAIL599.71
k14_2_3FAIL599.71
k6_2_3FAIL599.71
cnt16rFAIL599.71
test3_quant_squaring2FAIL599.71
nusmv.tcas^3.B-f2FAIL599.71
c5_BMC_p2_k64FAIL599.71
f600-50FAIL599.71
stmt19_64_99FAIL599.71
test4_quant_squaring2FAIL599.71
test5_quant_squaring5FAIL599.71
adder-12-unsatFAIL599.71
sortnetsort10.v.stepl.005FAIL599.71
Adder2-8-cFAIL599.71
texas.PI_main^05.E-f3FAIL599.71
cnt08eFAIL599.71
Core1108_tbm_21.tex.module.000030FAIL599.71
k_branch_p-21FAIL599.71
Umbrella_tbm_24.tex.module.000066FAIL599.71
Umbrella_tbm_24.tex.module.000131FAIL599.71
k_branch_p-18FAIL599.71
k_ph_p-18FAIL599.71
Umbrella_tbm_05.tex.module.000039FAIL599.71
Core1108_tbm_21.tex.module.000008FAIL599.71
s3330_d9_sFAIL599.71
k8_3_4FAIL599.71
Core1108_tbm_02.tex.moduleQ3.2S.000015FAIL599.71
Core1108_tbm_21.tex.module.000027FAIL599.71
s510_d36_sFAIL599.71
Core1108_tbm_03.tex.moduleQ3.2S.000002FAIL599.71
s3330_d7_sFAIL599.71
k_ph_p-15FAIL599.72
biu.mv.xl_ao.bb-b001-p005-OPF05-c03.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004FAIL599.81
C499.blif_0.10_0.20_0_0_out_exactFAIL599.81
C6288.blif_0.10_0.20_0_0_inp_exactFAIL599.81
connect_5x4_4_RFAIL599.81
c1_Debug_s3_f1_e1_v1FAIL599.81
k_ph_p-13FAIL599.81
gttt_2_1_00102030_4x4_torus_bFAIL599.81
query31_reachqu_1344nFAIL599.81
C880.blif_0.10_0.20_0_0_out_exactFAIL599.81
test4_quant_squaring4FAIL599.81
biu.mv.xl_ao.bb-b001-p010-MIF05-c07.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004FAIL599.81
sortnetsort9.v.stepl.005FAIL599.81
texas.two_proc^4.E-f2FAIL599.81
nusmv.tcas-t^1.B-d2FAIL599.81
uclid-pipe3bFAIL599.81
k_branch_n-12FAIL599.81
s641_d10_uFAIL599.81
connect_8x7_6_RFAIL599.81
s641_d11_uFAIL599.81
s641_d3_sFAIL599.81
k_branch_n-10FAIL599.81
k_branch_p-10FAIL599.81
k_branch_p-14FAIL599.81
s820_d3_sFAIL599.81
ken.oop^2.C-d3FAIL599.81
nusmv.reactor^3.C-d4FAIL599.81
C5315.blif_0.10_0.20_0_0_inp_exactFAIL599.81
test1_quant_squaring2FAIL599.81
C499.blif_0.10_0.20_0_0_inp_exactFAIL599.81
texas.PI_main^08.E-f3FAIL599.81
ev-pr-4x4-15-3-0-0-1-lgFAIL599.81
cache-coherence-3-fixpoint-3FAIL599.81
k8_3_2FAIL599.81
test1_quant_squaring3FAIL599.81
stmt52_244_394FAIL599.81
stmt19_83_412FAIL599.81
stmt41_160_235FAIL599.81
stmt19_3_214FAIL599.81
C880.blif_0.10_0.20_0_0_inp_exactFAIL599.81
arbiter-06-comp-error01-qbf-hardness-depth-15FAIL599.81
stmt21_319_418FAIL599.81
k8_4_3FAIL599.81
s510_d3_sFAIL599.81
C499.blif_0.10_0.20_0_1_out_exactFAIL599.81
k_branch_p-12FAIL599.81
C880.blif_0.10_1.00_0_0_inp_exactFAIL599.81
ev-pr-4x4-11-3-0-0-1-lgFAIL599.81
sdlx-fixpoint-3FAIL599.81
s510_d35_sFAIL599.81
C6288.blif_0.10_0.20_0_1_inp_exactFAIL599.81
s1269_d14_uFAIL599.81
k_ph_p-20FAIL599.81
s510_d24_sFAIL599.81
stmt29_226_376FAIL599.81
C880.blif_0.10_0.20_0_1_inp_exactFAIL599.81
stmt17_63_82FAIL599.81
stmt17_70_90FAIL599.81
stmt23_66_96FAIL599.81
stmt17_62_98FAIL599.81
C5315.blif_0.10_0.20_0_1_inp_exactFAIL599.81
stmt17_70_98FAIL599.81
stmt28_68_81FAIL599.81
stmt23_72_76FAIL599.81
b22_C_2_12FAIL599.81
b21_C_3_206FAIL599.81
uclid-pipe2FAIL599.81
C432.blif_0.10_0.20_0_0_inp_exactFAIL599.81
uclid-pipe3aFAIL599.81
arbiter-10-comp-error01-qbf-hardness-depth-22FAIL599.81
arbiter-08-comp-error02-qbf-hardness-depth-9FAIL599.81
ev-pr-4x4-17-3-0-0-1-lgFAIL599.81
s386_d4_sFAIL599.81
gttt_1_1_00101121_4x4_torus_wFAIL599.81
C5315.blif_0.10_0.20_0_1_out_exactFAIL599.82
arbiter-07-comp-error01-qbf-hardness-depth-20FAIL599.82
k_branch_n-11FAIL599.82
ken.flash^08.C-d4FAIL599.82
test3_quant_squaring4FAIL599.82
C432.blif_0.10_0.20_0_1_out_exactFAIL599.91
stmt17_82_98FAIL599.91
ii32b1-00FAIL599.91
test2_quant_squaring2FAIL599.91
C880.blif_0.10_0.20_0_1_out_exactFAIL599.91
k_branch_p-11FAIL600