Instances solved by rareqs-nn
QBFEVAL'16 - Prenex non-CNF Track.

InstanceResultTime
incrementer-enc05-uniform-depth-2UNSAT0.05
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.05
stmt44_107_108SAT0.06
flipflop-3-cUNSAT0.06
toilet_g_04_01.2SAT0.06
z4ml.blif_0.10_0.20_0_1_out_exactSAT0.07
counter5_2SAT0.07
mutex-2-sSAT0.07
counter4_3SAT0.07
rewriting_k_10UNSAT0.07
counter4_2SAT0.07
z4ml.blif_0.10_1.00_0_1_out_exactSAT0.07
counter4_4SAT0.08
counter7_2SAT0.08
rewriting_k_21UNSAT0.08
z4ml.blif_0.10_0.20_0_1_inp_exactSAT0.08
qshifter_3SAT0.08
counter6_2SAT0.08
ring5_2SAT0.08
z4ml.blif_0.10_1.00_0_0_inp_exactUNSAT0.08
toilet_g_08_01.2SAT0.08
ring6_2SAT0.08
ring4_2SAT0.08
toilet_a_04_01.4UNSAT0.08
rewriting_k_17UNSAT0.08
rewriting_k_19UNSAT0.08
ring4_3SAT0.09
counter8_2SAT0.09
counter5_4SAT0.09
counter4_5SAT0.09
toilet_c_06_01.4UNSAT0.1
semaphore_2SAT0.1
counter4_6SAT0.1
s27_d4_uUNSAT0.1
toilet_a_04_01.6UNSAT0.1
stmt17_18_19SAT0.1
counter4_7SAT0.11
ring4_4SAT0.11
ring5_4SAT0.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
counter6_4SAT0.11
ring4_5SAT0.12
mutex-4-sSAT0.12
counter4_8SAT0.12
eijk.S382.S-d4SAT0.12
counter7_4SAT0.12
k_ph_p-3UNSAT0.12
s27_d5_uUNSAT0.12
counter4_9SAT0.13
ring6_4SAT0.13
semaphore3_2SAT0.13
ring4_6SAT0.14
semaphore_3SAT0.14
counter5_8SAT0.14
counter4_10SAT0.14
counter8_4SAT0.14
counter4_11SAT0.15
ring4_7SAT0.15
counter4_12SAT0.15
semaphore4_2SAT0.16
ring4_8SAT0.16
counter4_14SAT0.17
counter4_13SAT0.17
counter6_8SAT0.17
counter4_15SAT0.18
rewriting_k_100UNSAT0.18
ring5_8SAT0.18
semaphore_4SAT0.18
semaphore3_3SAT0.19
counter4_16SAT0.19
toilet_a_06_01.6UNSAT0.2
C5315.blif_0.10_1.00_0_0_out_exactUNSAT0.2
Adder2-2-cUNSAT0.2
semaphore5_2SAT0.2
dmeSmall_2SAT0.21
counter7_8SAT0.21
ring6_8SAT0.21
s641_d2_sSAT0.21
semaphore_5SAT0.22
toilet_g_15_01.2SAT0.22
semaphore6_2SAT0.22
s713_d2_sSAT0.22
counter_e_2SAT0.22
stmt27_296_297SAT0.23
Core1108_tbm_21.tex.module.000091UNSAT0.23
semaphore4_3SAT0.24
k_lin_p-2UNSAT0.24
tree-exa10-10SAT0.25
C5315.blif_0.10_1.00_0_0_inp_exactUNSAT0.25
semaphore3_4SAT0.25
Core1108_tbm_21.tex.module.000017UNSAT0.26
s510_d3_sSAT0.26
counter8_8SAT0.26
Umbrella_tbm_24.tex.module.000103UNSAT0.27
counter5_16SAT0.28
dme1_2SAT0.29
Core1108_tbm_03.tex.module.000092UNSAT0.29
Core1108_tbm_21.tex.module.000023UNSAT0.29
Core1108_tbm_03.tex.module.000090UNSAT0.29
Core1108_tbm_21.tex.module.000026UNSAT0.29
Core1108_tbm_21.tex.module.000030UNSAT0.29
Umbrella_tbm_24.tex.module.000066UNSAT0.29
semaphore5_3SAT0.3
Core1108_tbm_03.tex.module.000065UNSAT0.3
Core1108_tbm_03.tex.module.000056UNSAT0.3
Core1108_tbm_03.tex.module.000057UNSAT0.3
k_path_p-2UNSAT0.3
Core1108_tbm_03.tex.module.000058UNSAT0.3
Core1108_tbm_21.tex.module.000014UNSAT0.3
Core1108_tbm_03.tex.module.000064UNSAT0.3
Core1108_tbm_21.tex.module.000008UNSAT0.31
Core1108_tbm_03.tex.module.000037UNSAT0.31
Umbrella_tbm_29.tex.module.000078UNSAT0.31
Core1108_tbm_03.tex.module.000048UNSAT0.31
ring5_16SAT0.31
Core1108_tbm_21.tex.module.000010UNSAT0.31
s1196_d2_sSAT0.31
counter6_16SAT0.31
Core1108_tbm_03.tex.module.000039UNSAT0.31
Core1108_tbm_21.tex.module.000009UNSAT0.31
Core1108_tbm_03.tex.module.000023UNSAT0.32
Core1108_tbm_03.tex.module.000034UNSAT0.32
b12_PR_9_2SAT0.32
Core1108_tbm_03.tex.module.000031UNSAT0.32
Core1108_tbm_03.tex.module.000003UNSAT0.32
Core1108_tbm_03.tex.module.000021UNSAT0.32
Core1108_tbm_03.tex.module.000019UNSAT0.32
semaphore4_4SAT0.33
Core1108_tbm_21.tex.module.000027UNSAT0.34
vis.4-arbit^2.E-f2SAT0.34
semaphore6_3SAT0.36
Umbrella_tbm_29.tex.module.000010UNSAT0.37
k3_1_1SAT0.37
Umbrella_tbm_29.tex.module.000009UNSAT0.37
ring6_16SAT0.38
dmeSmall_4SAT0.39
counter7_16SAT0.4
semaphore5_4SAT0.41
Umbrella_tbm_05.tex.module.000065UNSAT0.42
dme1_3SAT0.42
Core1108_tbm_09.tex.module.000028UNSAT0.43
irst.dme6.B-d2SAT0.44
Core1108_tbm_03.tex.module.000038UNSAT0.44
Umbrella_tbm_21.tex.module.000149UNSAT0.44
term1.blif_0.10_1.00_0_0_out_exactUNSAT0.44
Umbrella_tbm_21.tex.module.000129UNSAT0.45
Umbrella_tbm_21.tex.module.000134UNSAT0.45
Umbrella_tbm_21.tex.module.000139UNSAT0.45
Umbrella_tbm_21.tex.module.000079UNSAT0.46
s386_d3_sSAT0.46
Umbrella_tbm_05.tex.module.000043UNSAT0.47
Umbrella_tbm_05.tex.module.000088UNSAT0.47
Umbrella_tbm_21.tex.module.000069UNSAT0.47
Core1108_tbm_09.tex.module.000033UNSAT0.47
Umbrella_tbm_21.tex.module.000056UNSAT0.48
counter5_32SAT0.48
Umbrella_tbm_21.tex.module.000049UNSAT0.48
Umbrella_tbm_21.tex.module.000044UNSAT0.48
semaphore6_4SAT0.49
Umbrella_tbm_26.tex.module.000061UNSAT0.49
counter8_16SAT0.49
Umbrella_tbm_26.tex.module.000041UNSAT0.5
BLOCKS3ii.4.3UNSAT0.5
counter5_33SAT0.5
Core1108_tbm_09.tex.module.000008UNSAT0.51
k_lin_p-4UNSAT0.51
Umbrella_tbm_21.tex.module.000029UNSAT0.51
Umbrella_tbm_21.tex.module.000024UNSAT0.52
Umbrella_tbm_05.tex.module.000079UNSAT0.52
Core1108_tbm_09.tex.module.000010UNSAT0.52
Core1108_tbm_09.tex.module.000009UNSAT0.52
Umbrella_tbm_26.tex.module.000021UNSAT0.53
Umbrella_tbm_26.tex.module.000004UNSAT0.53
toilet_g_20_01.2SAT0.54
Umbrella_tbm_05.tex.module.000064UNSAT0.54
s499_d7_sSAT0.55
dme1_4SAT0.57
Umbrella_tbm_05.tex.module.000053UNSAT0.57
s641_d4_sSAT0.57
Umbrella_tbm_25.tex.module.000121UNSAT0.59
ring5_32SAT0.59
toilet_c_08_01.11UNSAT0.59
ring5_33SAT0.6
s820_d3_sSAT0.6
stmt16_950_951SAT0.6
Umbrella_tbm_25.tex.module.000087UNSAT0.61
Umbrella_tbm_25.tex.module.000106UNSAT0.61
Umbrella_tbm_25.tex.module.000084UNSAT0.61
toilet_c_08_05.4SAT0.61
Umbrella_tbm_05.tex.module.000030UNSAT0.62
flipflop-5-cUNSAT0.62
Umbrella_tbm_05.tex.module.000025UNSAT0.63
counter6_32SAT0.64
Umbrella_tbm_25.tex.module.000099UNSAT0.65
Umbrella_tbm_05.tex.module.000015UNSAT0.66
Umbrella_tbm_05.tex.module.000011UNSAT0.67
biu.mv.xl_ao.bb-b001-p010-IPF05-c07.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003SAT0.68
biu.mv.xl_ao.bb-b001-p010-IPF02-c08.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003SAT0.68
mutex-32-sSAT0.69
W3-Umbrella_tbm_21.tex.moduleQ3.6S.000001UNSAT0.7
Umbrella_tbm_25.tex.module.000041UNSAT0.7
dme1_5SAT0.71
s713_d4_sSAT0.71
biu.mv.xl_ao.bb-b001-p010-OPF02-c08.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003SAT0.71
toilet_a_08_05.2UNSAT0.71
Umbrella_tbm_25.tex.module.000031UNSAT0.72
Umbrella_tbm_25.tex.module.000003UNSAT0.72
ring6_32SAT0.74
s3330_d2_sSAT0.74
par8-1-c-50UNSAT0.76
dmeSmall_8SAT0.77
possibility9_0_2FAIL0.78
possibility10_0_2FAIL0.78
assertion5_0_2FAIL0.78
possibility6_0_2FAIL0.78
W4-Umbrella_tbm_21.tex.moduleQ3.6S.000001UNSAT0.78
possibility2_0_2FAIL0.79
assertion10_0_2FAIL0.79
possibility5_0_2FAIL0.79
assertion3_0_2FAIL0.79
possibility1_0_2FAIL0.79
assertion11_0_2FAIL0.79
possibility4_0_2FAIL0.79
assertion9_0_2FAIL0.79
assertion6_0_2FAIL0.79
possibility7_0_2FAIL0.79
assertion2_0_2FAIL0.79
possibility3_0_2FAIL0.79
possibility12_0_2FAIL0.79
assertion1_0_2FAIL0.79
assertion8_0_2FAIL0.79
possibility11_0_2FAIL0.79
consistency_0_2FAIL0.79
assertion4_0_2FAIL0.8
assertion7_0_2FAIL0.8
Core1108_tbm_21.tex.moduleQ3.2S.000027UNSAT0.8
Core1108_tbm_21.tex.moduleQ3.2S.000014UNSAT0.8
Core1108_tbm_21.tex.moduleQ3.2S.000002UNSAT0.8
possibility8_0_2FAIL0.8
assertion12_0_2FAIL0.8
Core1108_tbm_21.tex.moduleQ3.2S.000007UNSAT0.8
Core1108_tbm_21.tex.moduleQ3.2S.000019UNSAT0.8
Core1108_tbm_21.tex.moduleQ3.2S.000024UNSAT0.81
Core1108_tbm_21.tex.moduleQ3.2S.000011UNSAT0.81
counter7_32SAT0.81
Core1108_tbm_21.tex.moduleQ3.2S.000015UNSAT0.81
dme1_6SAT0.86
dmeSmall_9SAT0.87
Core1108_tbm_28.tex.moduleQ2.2S.000003UNSAT0.88
query01_ntrivil_1344UNSAT0.89
Core1108_tbm_03.tex.moduleQ3.2S.000002UNSAT0.9
Core1108_tbm_03.tex.moduleQ3.2S.000018UNSAT0.91
Core1108_tbm_03.tex.moduleQ3.2S.000009UNSAT0.91
Core1108_tbm_03.tex.moduleQ3.2S.000048UNSAT0.91
Core1108_tbm_03.tex.moduleQ3.2S.000003UNSAT0.91
Core1108_tbm_03.tex.moduleQ3.2S.000011UNSAT0.91
query48_query15_1344UNSAT0.92
s386_d4_sSAT0.96
C499.blif_0.10_1.00_0_1_inp_exactSAT0.98
dme1_7SAT1.02
counter8_32SAT1.02
stmt41_738_749SAT1.09
possibility4_0_3FAIL1.11
assertion8_0_3FAIL1.11
possibility3_0_3FAIL1.12
possibility6_0_3FAIL1.12
possibility2_0_3FAIL1.12
lut4_XOR_fORUNSAT1.12
possibility11_0_3FAIL1.12
possibility10_0_3FAIL1.12
possibility1_0_3FAIL1.12
consistency_0_3FAIL1.12
W4-Umbrella_tbm_26.tex.moduleQ3.7S.000003UNSAT1.12
assertion4_0_3FAIL1.12
assertion11_0_3FAIL1.12
assertion2_0_3FAIL1.12
assertion10_0_3FAIL1.12
assertion12_0_3FAIL1.12
assertion5_0_3FAIL1.13
assertion9_0_3FAIL1.13
assertion3_0_3FAIL1.13
possibility12_0_3FAIL1.13
assertion6_0_3FAIL1.13
possibility9_0_3FAIL1.13
assertion7_0_3FAIL1.14
dme1_8SAT1.16
ring_r4_ser--opt-11_UNSAT1.19
arbiter-07-comp-error01-qbf-hardness-depth-4UNSAT1.19
W5-Umbrella_tbm_26.tex.moduleQ3.7S.000003UNSAT1.21
nusmv.tcas-t^1.B-d2SAT1.21
toilet_c_10_01.12UNSAT1.25
assertion1_0_3FAIL1.28
counter6_64SAT1.34
counter6_65SAT1.35
mutex-64-sSAT1.39
k_d4_n-1SAT1.4
Core1108_tbm_02.tex.moduleQ3.2S.000015UNSAT1.44
possibility5_0_3FAIL1.45
W5-Umbrella_tbm_05.tex.moduleQ3.8S.000001UNSAT1.48
possibility2_0_4FAIL1.49
consistency_0_4FAIL1.49
s1269_d3_sSAT1.49
assertion11_0_4FAIL1.49
possibility7_0_4FAIL1.49
possibility4_0_4FAIL1.49
possibility11_0_4FAIL1.5
assertion6_0_4FAIL1.5
possibility3_0_4FAIL1.5
assertion10_0_4FAIL1.5
assertion9_0_4FAIL1.5
assertion12_0_4FAIL1.5
possibility9_0_4FAIL1.5
assertion8_0_4FAIL1.5
possibility8_0_3FAIL1.5
assertion1_0_4FAIL1.5
assertion4_0_4FAIL1.51
possibility5_0_4FAIL1.51
possibility6_0_4FAIL1.51
W4-Umbrella_tbm_25.tex.moduleQ3.7S.000003UNSAT1.51
assertion5_0_4FAIL1.51
possibility1_0_4FAIL1.51
possibility10_0_4FAIL1.51
assertion2_0_4FAIL1.51
assertion7_0_4FAIL1.52
assertion3_0_4FAIL1.52
Core1108_tbm_02.tex.moduleQ3.2S.000095UNSAT1.53
Core1108_tbm_02.tex.moduleQ3.2S.000077UNSAT1.53
Core1108_tbm_02.tex.moduleQ3.2S.000056UNSAT1.53
possibility12_0_4FAIL1.53
possibility8_0_4FAIL1.53
ring6_64SAT1.54
Core1108_tbm_02.tex.moduleQ3.2S.000026UNSAT1.54
Core1108_tbm_02.tex.moduleQ3.2S.000099UNSAT1.54
Core1108_tbm_02.tex.moduleQ3.2S.000108UNSAT1.54
Core1108_tbm_02.tex.moduleQ3.2S.000098UNSAT1.56
Core1108_tbm_02.tex.moduleQ3.2S.000007UNSAT1.57
flipflop-6-cUNSAT1.57
ring6_65SAT1.57
W4-Umbrella_tbm_05.tex.moduleQ3.8S.000001UNSAT1.65
k_ph_p-5UNSAT1.7
counter7_64SAT1.7
Umbrella_tbm_24.tex.moduleQ2.1S.000136UNSAT1.74
Umbrella_tbm_24.tex.moduleQ2.1S.000188UNSAT1.75
Umbrella_tbm_24.tex.moduleQ2.1S.000022UNSAT1.75
W5-Umbrella_tbm_25.tex.moduleQ3.7S.000003UNSAT1.77
Umbrella_tbm_29.tex.moduleQ2.2S.000001UNSAT1.87
C432.blif_0.10_1.00_0_1_out_exactSAT1.89
possibility1_0_5FAIL1.93
assertion11_0_5FAIL1.93
consistency_0_5FAIL1.93
possibility4_0_5FAIL1.93
assertion6_0_5FAIL1.94
possibility2_0_5FAIL1.94
assertion1_0_5FAIL1.94
assertion5_0_5FAIL1.94
assertion7_0_5FAIL1.94
possibility11_0_5FAIL1.94
possibility9_0_5FAIL1.94
possibility7_0_5FAIL1.94
possibility10_0_5FAIL1.94
assertion8_0_5FAIL1.95
assertion3_0_5FAIL1.95
assertion12_0_5FAIL1.95
assertion10_0_5FAIL1.95
assertion4_0_5FAIL1.95
assertion9_0_5FAIL1.95
possibility3_0_5FAIL1.95
possibility6_0_5FAIL1.95
assertion2_0_5FAIL1.95
possibility12_0_5FAIL1.96
possibility5_0_5FAIL1.97
Umbrella_tbm_23.tex.moduleQ1.2S.000001UNSAT1.97
possibility8_0_5FAIL1.98
k_lin_p-9UNSAT2.06
biu.mv.xl_ao.bb-b001-p010-MIF01-c01.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004SAT2.13
possibility7_0_3FAIL2.16
biu.mv.xl_ao.bb-b001-p005-OPF05-c02.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004SAT2.22
counter8_64SAT2.42
possibility10_0_6FAIL2.45
consistency_0_6FAIL2.46
possibility2_0_6FAIL2.46
assertion11_0_6FAIL2.46
assertion10_0_6FAIL2.46
assertion12_0_6FAIL2.47
assertion6_0_6FAIL2.47
possibility6_0_6FAIL2.47
assertion9_0_6FAIL2.47
possibility1_0_6FAIL2.47
possibility11_0_6FAIL2.47
possibility4_0_6FAIL2.47
assertion5_0_6FAIL2.48
Umbrella_tbm_14.tex.moduleQ2.1S.000792UNSAT2.48
assertion4_0_6FAIL2.48
Umbrella_tbm_26.tex.moduleQ3.2S.000041UNSAT2.48
assertion1_0_6FAIL2.48
assertion2_0_6FAIL2.48
Umbrella_tbm_14.tex.moduleQ2.2S.000002UNSAT2.48
Umbrella_tbm_14.tex.moduleQ2.1S.000812UNSAT2.49
Umbrella_tbm_14.tex.moduleQ2.2S.000001UNSAT2.49
Umbrella_tbm_14.tex.moduleQ2.1S.000720UNSAT2.49
Umbrella_tbm_14.tex.moduleQ2.1S.000757UNSAT2.49
possibility5_0_6FAIL2.49
Umbrella_tbm_14.tex.moduleQ2.1S.000808UNSAT2.49
possibility12_0_6FAIL2.5
Umbrella_tbm_14.tex.moduleQ2.1S.000787UNSAT2.5
assertion7_0_6FAIL2.5
Umbrella_tbm_14.tex.moduleQ2.1S.000773UNSAT2.5
assertion3_0_6FAIL2.5
Umbrella_tbm_14.tex.moduleQ2.2S.000003UNSAT2.5
Umbrella_tbm_14.tex.moduleQ2.1S.000749UNSAT2.51
Umbrella_tbm_26.tex.moduleQ3.2S.000037UNSAT2.51
possibility9_0_6FAIL2.51
assertion8_0_6FAIL2.51
Umbrella_tbm_26.tex.moduleQ3.2S.000009UNSAT2.52
Umbrella_tbm_26.tex.moduleQ3.2S.000020UNSAT2.52
Umbrella_tbm_26.tex.moduleQ3.2S.000014UNSAT2.52
possibility8_0_6FAIL2.54
s499_d15_sSAT2.56
possibility7_0_6FAIL2.76
BLOCKS4iii.6UNSAT2.82
k_ph_n-6SAT2.82
possibility7_0_7FAIL3.04
consistency_0_7FAIL3.04
possibility9_0_7FAIL3.05
BLOCKS3iii.5SAT3.05
assertion11_0_7FAIL3.05
possibility2_0_7FAIL3.05
possibility5_0_7FAIL3.06
assertion5_0_7FAIL3.06
possibility3_0_7FAIL3.06
assertion10_0_7FAIL3.06
possibility10_0_7FAIL3.07
possibility1_0_7FAIL3.07
assertion3_0_7FAIL3.07
possibility11_0_7FAIL3.07
assertion12_0_7FAIL3.07
assertion7_0_7FAIL3.07
assertion1_0_7FAIL3.07
stmt27_16_97UNSAT3.07
assertion9_0_7FAIL3.07
possibility6_0_7FAIL3.08
possibility4_0_7FAIL3.08
assertion6_0_7FAIL3.08
assertion2_0_7FAIL3.08
assertion8_0_7FAIL3.09
assertion4_0_7FAIL3.1
possibility3_0_6FAIL3.12
possibility12_0_7FAIL3.12
possibility8_0_7FAIL3.16
Core1108_tbm_09.tex.moduleQ3.9S.000001UNSAT3.42
Core1108_tbm_09.tex.moduleQ3.10S.000001UNSAT3.42
Core1108_tbm_09.tex.moduleQ3.2S.000011UNSAT3.44
possibility1_0_8FAIL3.71
ken.flash^10.C-f3UNSAT3.71
assertion11_0_8FAIL3.72
assertion12_0_8FAIL3.72
possibility6_0_8FAIL3.73
assertion1_0_8FAIL3.73
consistency_0_8FAIL3.73
possibility4_0_8FAIL3.73
possibility3_0_8FAIL3.73
assertion7_0_8FAIL3.74
possibility7_0_8FAIL3.74
assertion9_0_8FAIL3.74
possibility11_0_8FAIL3.75
possibility5_0_8FAIL3.75
assertion3_0_8FAIL3.76
assertion6_0_8FAIL3.76
assertion2_0_8FAIL3.77
assertion10_0_8FAIL3.77
assertion4_0_8FAIL3.78
assertion5_0_8FAIL3.78
possibility12_0_8FAIL3.81
possibility9_0_8FAIL3.82
assertion8_0_8FAIL3.82
counter7_129SAT3.85
possibility8_0_8FAIL3.87
k_lin_p-10UNSAT3.95
Core1108_tbm_09.tex.moduleQ3.2S.000005UNSAT3.97
C880.blif_0.10_1.00_0_0_out_exactUNSAT3.98
toilet_a_10_05.3UNSAT4.07
possibility10_0_8FAIL4.07
driverlog03_7SAT4.14
Core1108_tbm_09.tex.moduleQ3.2S.000007UNSAT4.15
s298_d12_sSAT4.16
Core1108_tbm_09.tex.moduleQ3.2S.000003UNSAT4.16
counter7_128SAT4.19
nusmv.tcas^3.B-f2SAT4.2
possibility2_0_8FAIL4.28
Core1108_tbm_09.tex.moduleQ3.2S.000010UNSAT4.31
s298_d14_sSAT4.44
assertion11_0_9FAIL4.51
possibility4_0_9FAIL4.56
possibility2_0_9FAIL4.56
possibility10_0_9FAIL4.56
assertion12_0_9FAIL4.56
assertion1_0_9FAIL4.57
possibility11_0_9FAIL4.57
possibility9_0_9FAIL4.57
consistency_0_9FAIL4.58
assertion3_0_9FAIL4.58
assertion7_0_9FAIL4.58
possibility6_0_9FAIL4.59
assertion10_0_9FAIL4.59
s499_d17_sSAT4.6
assertion2_0_9FAIL4.6
possibility7_0_9FAIL4.6
assertion4_0_9FAIL4.61
assertion6_0_9FAIL4.62
assertion9_0_9FAIL4.62
assertion8_0_9FAIL4.63
counter8_128SAT4.63
assertion5_0_9FAIL4.64
possibility5_0_9FAIL4.66
possibility12_0_9FAIL4.66
possibility8_0_9FAIL4.66
possibility1_0_9FAIL4.76
connect_6x5_5_DUNSAT4.88
Umbrella_tbm_25.tex.moduleQ3.2S.000052UNSAT4.88
Umbrella_tbm_25.tex.moduleQ3.2S.000063UNSAT4.89
Umbrella_tbm_25.tex.moduleQ3.2S.000120UNSAT4.91
CHAIN14v.15SAT4.98
possibility3_0_9FAIL5.05
assertion10_0_10FAIL5.43
assertion11_0_10FAIL5.44
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-003UNSAT5.44
possibility1_0_10FAIL5.45
assertion6_0_10FAIL5.46
assertion12_0_10FAIL5.47
possibility5_0_10FAIL5.47
possibility3_0_10FAIL5.47
assertion9_0_10FAIL5.47
possibility7_0_10FAIL5.48
possibility11_0_10FAIL5.48
possibility4_0_10FAIL5.49
consistency_0_10FAIL5.5
possibility10_0_10FAIL5.5
possibility6_0_10FAIL5.51
assertion3_0_10FAIL5.51
possibility2_0_10FAIL5.51
assertion2_0_10FAIL5.52
assertion8_0_10FAIL5.53
assertion1_0_10FAIL5.54
possibility9_0_10FAIL5.54
assertion5_0_10FAIL5.55
assertion7_0_10FAIL5.56
s1269_d8_sSAT5.57
assertion4_0_10FAIL5.58
possibility12_0_10FAIL5.6
possibility8_0_10FAIL5.67
c4_BMC_p1_k32SAT5.8
s386_d8_uUNSAT5.93
lut4_AND_fXORUNSAT6.01
BLOCKS3ii.5.3SAT6.26
Umbrella_tbm_25.tex.moduleQ3.2S.000075UNSAT6.38
arbiter-06-comp-error02-qbf-hardness-depth-5UNSAT7.1
par8-4-50UNSAT7.41
BLOCKS3i.5.3UNSAT7.56
term1.blif_0.10_1.00_0_1_out_exactSAT7.73
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-005UNSAT7.78
fpu-10Xh-error01-uniform-depth-5UNSAT8.03
vonNeumann-ripple-carry-5-cUNSAT8.33
CHAIN16v.17SAT8.35
term1.blif_0.10_0.20_0_0_out_exactUNSAT8.54
tlc03-uniform-depth-21UNSAT9.34
fpu-10Xe-correct01-nonuniform-depth-6UNSAT9.67
assertion11_0_1UNSAT10.22
s386_d10_uUNSAT10.23
assertion12_0_1UNSAT10.33
s510_d11_sSAT10.47
connect_7x6_4_WUNSAT10.64
emptyroom_e3_ser--opt-20_SAT13.3
szymanski-5-sUNSAT13.57
connect_8x7_7_WUNSAT13.74
term1.blif_0.10_0.20_0_1_inp_exactSAT13.84
counter8_256SAT14.47
counter8_257SAT15.22
s386_d12_uUNSAT15.63
ring_r3_ser--opt-8_SAT17.09
assertion5_0_1UNSAT18.25
vonNeumann-ripple-carry-6-cUNSAT19.38
lognBWLARGEA1UNSAT19.9
k_branch_n-2SAT20.6
CHAIN20v.21SAT20.89
k_lin_p-19UNSAT24.63
vonNeumann-ripple-carry-7-cUNSAT26.06
flipflop-10-cUNSAT27.79
filesys_smbmrx_cvsndrcv.cUNSAT30.25
CHAIN22v.23SAT30.93
s820_d8_sSAT33.82
C432.blif_0.10_0.20_0_1_inp_exactSAT35.21
C499.blif_0.10_1.00_0_0_out_exactUNSAT35.42
CHAIN23v.24SAT37.64
tlc01-uniform-depth-73UNSAT41.86
k_dum_n-1SAT42.16
flipflop-11-cUNSAT47.1
stmt19_90_266UNSAT56.42
lut4_2_f2UNSAT56.43
lognBWLARGEB1UNSAT57.36
p10-10.pddl_planlen=6UNSAT57.71
k_ph_n-9SAT59.07
c4_BMC_p2_k128UNSAT87.6
tlc03-uniform-depth-52UNSAT89.05
k_lin_n-3SAT92.28
lut4_2_fXORSAT101.94
s713_d6_sSAT102.82
C432.blif_0.10_1.00_0_0_out_exactUNSAT130.24
vonNeumann-ripple-carry-11-cUNSAT130.79
s820_d11_uUNSAT133.31
stmt21_79_304UNSAT144.62
szymanski-6-sUNSAT151.14
s820_d12_uUNSAT165.89
s499_d22_uUNSAT167.87
vonNeumann-ripple-carry-12-cUNSAT178.24
ev-pr-6x6-9-5-0-1-2-sFAIL193.02
s510_d24_sSAT198.3
ev-pr-6x6-11-5-0-1-2-sFAIL202.23
query51_query50_1344UNSAT206.46
s3330_d3_sSAT206.57
ev-pr-6x6-13-5-0-1-2-sFAIL211.72
par16-1-50UNSAT219.39
ev-pr-6x6-17-5-0-1-2-sFAIL231.42
s499_d24_uUNSAT246.17
s820_d15_uUNSAT274.38
s3330_d4_sSAT277.18
C432.blif_0.10_0.20_0_0_out_exactUNSAT289.15
C880.blif_0.10_0.20_0_1_out_exactUNSAT317.82
texas.PI_main^05.E-f3SAT339.49
s641_d6_sSAT407.75
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-005UNSAT429.84
p10-10.pddl_planlen=10SAT445.13
s510_d31_sSAT483.5
c3_Debug_s3_f2_e2_v2FAIL580.51
pipesnotankage18_8FAIL585.31
p20-20.pddl_planlen=23FAIL588.71
c2_BMC_p1_k2048FAIL593.11
pipesnotankage14_10FAIL593.41
dungeon_i25-m12-u3-v0.pddl_planlen=190FAIL593.71
dungeon_i25-m12-u3-v0.pddl_planlen=165FAIL594.51
c4_Debug_s5_f2_e2_v1FAIL594.81
c2_Debug_s3_f1_e1_v2FAIL595.71
c1_Debug_s5_f1_e1_v2FAIL596.01
fpu-10Xh-correct04-nonuniform-depth-27FAIL596.22
c4_Debug_s3_f2_e2_v2FAIL596.22
fpu-10Xe-correct01-uniform-depth-22FAIL596.61
fpu-10Xe-correct01-nonuniform-depth-24FAIL596.71
qshifter_8FAIL598.42
p20-5.pddl_planlen=32FAIL598.71
c5_BMC_p2_k128FAIL598.71
connect_9x8_6_RFAIL598.91
b20_C_3_2FAIL598.91
ring_r6_ser--opt-17_FAIL598.91
szymanski-16-sFAIL599.01
c5_BMC_p2_k64FAIL599.12
ev-pr-8x8-15-7-0-1-2-lgFAIL599.21
network_irda_miniport_nscirda_comm.cFAIL599.21
szymanski-14-sFAIL599.21
ev-pr-4x4-17-3-0-0-1-sFAIL599.21
connect_8x7_6_RFAIL599.31
dungeon_i15-m7-u4-v0.pddl_planlen=81FAIL599.31
ev-pr-4x4-13-3-0-0-1-sFAIL599.31
ev-pr-4x4-15-3-0-0-1-sFAIL599.31
input_pnpi8042_moudep.cFAIL599.31
s3330_d12_uFAIL599.31
ev-pr-8x8-19-7-0-1-2-lgFAIL599.31
qshifter_7FAIL599.32
dungeon_i10-m10-u10-v0.pddl_planlen=187FAIL599.42
s3330_d9_sFAIL599.42
k14_2_3FAIL599.42
query42_query06_1344nFAIL599.42
ev-pr-8x8-13-7-0-1-2-lgFAIL599.42
k12_4_2FAIL599.43
s1269_d15_uFAIL599.52
stmt17_86_98FAIL599.52
audio_ddksynth_csynth2.cppFAIL599.52
ev-pr-4x4-7-3-0-0-1-sFAIL599.52
s1269_d12_uFAIL599.52
arbiter-10-comp-error01-qbf-hardness-depth-22FAIL599.52
ev-pr-6x6-11-5-0-1-2-lgFAIL599.52
ev-pr-6x6-17-5-0-1-2-lgFAIL599.52
emptyroom_e4_ser--opt-44_FAIL599.52
s510_d36_sFAIL599.52
s15850_PR_8_50FAIL599.52
b22_PR_8_20FAIL599.52
b21_C_3_206FAIL599.52
ev-pr-6x6-19-5-0-1-2-lgFAIL599.52
Adder2-16-sFAIL599.53
incrementer-enc02-uniform-depth-58FAIL599.53
ev-pr-8x8-7-7-0-1-2-lgFAIL599.53
s1269_d13_uFAIL599.53
k_ph_n-16FAIL599.61
szymanski-8-sFAIL599.61
C6288.blif_0.10_0.20_0_1_out_exactFAIL599.61
ev-pr-4x4-11-3-0-0-1-lgFAIL599.61
s1196_d5_uFAIL599.61
cube_c7_ser--opt-24_FAIL599.61
f600-50FAIL599.61
texas.PI_main^08.E-f3FAIL599.61
k_d4_n-20FAIL599.61
C5315.blif_0.10_0.20_0_0_out_exactFAIL599.61
gttt_2_1_00102030_4x4_torus_bFAIL599.61
stmt52_244_394FAIL599.61
test2_quant_squaring2FAIL599.61
ev-pr-4x4-13-3-0-0-1-lgFAIL599.61
k_branch_p-10FAIL599.61
k_branch_p-11FAIL599.61
k_ph_p-19FAIL599.61
k_lin_n-17FAIL599.61
s298_d22_uFAIL599.61
s09234_PR_8_2FAIL599.61
k_branch_p-16FAIL599.61
arbiter-10-comp-error01-qbf-hardness-depth-10FAIL599.61
b20_PR_7_20FAIL599.61
query44_query26_1344nFAIL599.61
dungeon_i10-m5-u10-v0.pddl_planlen=23FAIL599.61
possibility8_0_1FAIL599.61
rankfunc17_unsigned_16FAIL599.61
incrementer-enc07-uniform-depth-25FAIL599.61
ken.flash^08.C-d4FAIL599.61
stmt28_68_81FAIL599.61
possibility2_0_1FAIL599.61
assertion3_0_1FAIL599.61
ev-pr-6x6-9-5-0-1-2-lgFAIL599.61
test2_quant_squaring3FAIL599.61
stmt17_70_90FAIL599.61
s298_d19_uFAIL599.61
stmt17_63_82FAIL599.61
stmt19_64_99FAIL599.61
cnt14FAIL599.61
possibility3_0_1FAIL599.61
cache-coherence-2-fixpoint-6FAIL599.62
k_ph_n-21FAIL599.62
adder-12-unsatFAIL599.62
adder-10-satFAIL599.62
adder-14-satFAIL599.62
sortnetsort9.AE.stepl.012FAIL599.62
k_ph_p-12FAIL599.62
s298_d25_uFAIL599.62
tlc04-nonuniform-depth-56FAIL599.62
network_ndis_rtlnwifi_hw_hw_ccmp.cFAIL599.63
incrementer-enc08-uniform-depth-33FAIL599.63
rankfunc5_unsigned_64FAIL599.71
k_t4p_p-4FAIL599.71
tree-exa2-20FAIL599.71
possibility9_0_1FAIL599.71
uclid-pipe3aFAIL599.71
Umbrella_tbm_24.tex.module.000131FAIL599.71
rankfunc14_signed_64FAIL599.71
impl10FAIL599.71
rankfunc33_signed_32FAIL599.71
C499.blif_0.10_0.20_0_1_out_exactFAIL599.71
k8_2_3FAIL599.71
possibility4_0_1FAIL599.71
ii32b1-00FAIL599.71
stmt41_160_235FAIL599.71
C6288.blif_0.10_0.20_0_0_inp_exactFAIL599.71
tree-exa2-25FAIL599.71
possibility12_0_1FAIL599.71
impl08FAIL599.71
impl16FAIL599.71
C6288.blif_0.10_1.00_0_0_out_exactFAIL599.71
lut4_3_fANDFAIL599.71
rankfunc13_unsigned_64FAIL599.71
possibility5_0_1FAIL599.71
k_path_p-16FAIL599.71
tree-exa2-45FAIL599.71
C6288.blif_0.10_0.20_0_0_out_exactFAIL599.71
possibility7_0_1FAIL599.71
possibility11_0_1FAIL599.71
k_d4_p-20FAIL599.71
C5315.blif_0.10_0.20_0_1_inp_exactFAIL599.71
k_t4p_n-2FAIL599.71
k_d4_n-14FAIL599.71
k_d4_n-15FAIL599.71
k_d4_p-17FAIL599.71
k_d4_p-13FAIL599.71
k_d4_p-11FAIL599.71
k_dum_n-18FAIL599.71
assertion10_0_1FAIL599.71
k_path_p-14FAIL599.71
k_path_p-10FAIL599.71
k_dum_n-17FAIL599.71
k_dum_p-2FAIL599.71
k_ph_n-11FAIL599.71
k_ph_p-10FAIL599.71
k_poly_n-18FAIL599.71
k_dum_n-12FAIL599.71
k_poly_p-4FAIL599.71
k_poly_p-19FAIL599.71
toilet_c_10_01.17FAIL599.71
k_branch_n-10FAIL599.71
k_poly_p-7FAIL599.71
k_poly_n-17FAIL599.71
k_poly_n-7FAIL599.71
k_poly_n-2FAIL599.71
k_branch_n-3FAIL599.71
k_branch_p-5FAIL599.71
k_dum_p-3FAIL599.71
k_dum_p-6FAIL599.71
k_path_n-9FAIL599.71
k_grz_p-13FAIL599.71
arbiter-08-comp-error02-qbf-hardness-depth-9FAIL599.71
k_path_n-5FAIL599.71
tlc03-nonuniform-depth-17FAIL599.71
k_lin_n-6FAIL599.71
k_lin_n-5FAIL599.71
incrementer-enc03-nonuniform-depth-24FAIL599.71
small-swap2-fixpoint-4FAIL599.71
small-synabs-fixpoint-9FAIL599.71
small-swap1-fixpoint-3FAIL599.71
gttt_1_1_001020_3x3_wFAIL599.71
gttt_2_1_000111_3x3_torus_bFAIL599.71
k_path_n-13FAIL599.71
k_path_p-5FAIL599.71
assertion1_0_1FAIL599.71
gttt_1_1_000111_3x3_torus_wFAIL599.71
k_grz_n-5FAIL599.71
k_grz_n-10FAIL599.71
k_grz_p-18FAIL599.71
k_grz_p-10FAIL599.71
k_grz_p-11FAIL599.71
p20-1.pddl_planlen=24FAIL599.71
lights3_035_0_051FAIL599.71
lights3_035_0_027FAIL599.71
sdlx-fixpoint-3FAIL599.71
Umbrella_tbm_05.tex.module.000039FAIL599.71
possibility1_0_1FAIL599.71
ken.oop^2.C-d4FAIL599.71
k_t4p_p-12FAIL599.71
test3_quant_squaring4FAIL599.71
test3_quant_squaring2FAIL599.71
k_t4p_p-15FAIL599.71
assertion7_0_1FAIL599.71
s713_d8_uFAIL599.71
s641_d8_uFAIL599.71
k_poly_p-16FAIL599.71
assertion6_0_1FAIL599.71
k_dum_p-12FAIL599.71
assertion8_0_1FAIL599.71
ev-pr-4x4-7-3-0-0-1-lgFAIL599.71
test1_quant_squaring3FAIL599.71
s713_d7_uFAIL599.71
consistency_0_1FAIL599.71
k_t4p_p-16FAIL599.71
sortnetsort9.v.stepl.007FAIL599.71
ev-pr-4x4-9-3-0-0-1-lgFAIL599.71
k_lin_n-8FAIL599.71
assertion9_0_1FAIL599.71
sortnetsort8.v.stepl.009FAIL599.71
s1196_d3_uFAIL599.71
sortnetsort10.v.stepl.005FAIL599.71
k_path_n-12FAIL599.71
k_dum_p-16FAIL599.71
s641_d7_uFAIL599.71
k_poly_p-8FAIL599.71
k_path_n-16FAIL599.71
k_grz_n-21FAIL599.71
k_t4p_p-18FAIL599.71
cnt10FAIL599.71
assertion4_0_1FAIL599.71
k_t4p_n-13FAIL599.71
k_t4p_n-5FAIL599.71
cnt16rFAIL599.71
k_t4p_n-15FAIL599.71
k_grz_n-20FAIL599.71
C499.blif_0.10_0.20_0_0_out_exactFAIL599.71
k_branch_n-8FAIL599.71
k_t4p_n-14FAIL599.71
k_poly_n-21FAIL599.71
assertion2_0_1FAIL599.71
k5_2_3FAIL599.72
gttt_2_2_001020_4x4_wFAIL599.72
C880.blif_0.10_0.20_0_1_inp_exactFAIL599.72
k_d4_n-2FAIL599.81
k_d4_p-8FAIL599.81
k_dum_n-5FAIL599.81
tree-exa2-35FAIL599.81
impl20FAIL599.81
uclid-pipe2FAIL599.81
sortnetsort9.v.stepl.005FAIL599.81
k_grz_n-2FAIL599.81
cnt05FAIL599.81
s01238_PR_8_2FAIL599.81
C880.blif_0.10_1.00_0_0_inp_exactFAIL599.81
impl12FAIL599.81
k_grz_p-17FAIL599.81
k_branch_n-12FAIL600
possibility10_0_1FAIL600
k_branch_p-6FAIL600
possibility6_0_1FAIL600