Instances solved by <a href='solver_detail.php?solver=241'>iprover-QBF</a> <br> QBFEVAL'16

Instances solved by iprover-QBF
QBFEVAL'16 - Prenex CNF Track.

Instance	Result	Time
k_ph_n-1	SAT	0.04
small-swap1-fixpoint-3	FAIL	0.04
k_ph_p-1	UNSAT	0.04
tree-exa10-10	SAT	0.04
small-swap2-fixpoint-4	FAIL	0.04
cnt01	SAT	0.04
toilet_g_04_01.2	SAT	0.04
toilet_g_02_01.2	SAT	0.04
tree-exa2-10	UNSAT	0.04
qshifter_3	SAT	0.05
cache-coherence-3-fixpoint-3	FAIL	0.05
impl06	SAT	0.05
tree-exa2-25	UNSAT	0.05
small-seq-fixpoint-3	FAIL	0.05
toilet_c_08_01.2	UNSAT	0.05
impl02	SAT	0.05
tree-exa2-20	UNSAT	0.05
toilet_c_04_01.4	UNSAT	0.05
sdlx-fixpoint-3	FAIL	0.05
toilet_g_10_01.2	SAT	0.05
lognBWLARGEA0	UNSAT	0.05
toilet_g_08_01.2	SAT	0.05
flipflop-3-c	UNSAT	0.05
toilet_g_06_01.2	SAT	0.05
cache-coherence-2-fixpoint-1	FAIL	0.05
small-synabs-fixpoint-9	FAIL	0.05
impl04	SAT	0.05
tree-exa10-30	SAT	0.05
stmt44_107_108	SAT	0.05
impl08	SAT	0.06
toilet_a_04_01.4	UNSAT	0.06
toilet_c_06_01.4	UNSAT	0.06
p5-5.pddl_planlen=5	FAIL	0.06
p5-5.pddl_planlen=6	FAIL	0.06
toilet_g_15_01.2	SAT	0.06
rewriting_k_10	UNSAT	0.06
tree-exa2-30	UNSAT	0.06
impl10	SAT	0.06
cache-coherence-2-fixpoint-6	FAIL	0.06
stmt44_107_113	SAT	0.06
stmt1_30_31	SAT	0.06
lognBWLARGEB0	UNSAT	0.07
tree-exa2-40	UNSAT	0.07
small-seq-fixpoint-5	FAIL	0.07
toilet_a_04_05.2	SAT	0.07
tree-exa2-35	UNSAT	0.07
impl12	SAT	0.07
toilet_a_02_10.2	SAT	0.07
toilet_g_20_01.2	SAT	0.07
mutex-2-s	SAT	0.08
toilet_a_04_01.6	UNSAT	0.08
impl14	SAT	0.08
tree-exa2-45	UNSAT	0.08
tree-exa2-50	UNSAT	0.09
impl18	SAT	0.09
impl16	SAT	0.09
cnt02e	SAT	0.09
counter_e_2	SAT	0.09
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-001	UNSAT	0.09
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-003	UNSAT	0.1
rewriting_k_17	UNSAT	0.1
impl20	SAT	0.1
qshifter_4	SAT	0.1
p20-1.pddl_planlen=26	FAIL	0.11
p20-1.pddl_planlen=24	FAIL	0.11
rewriting_k_19	UNSAT	0.11
rewriting_k_21	UNSAT	0.13
p20-1.pddl_planlen=32	FAIL	0.13
flipflop-4-c	UNSAT	0.14
toilet_c_08_01.6	UNSAT	0.15
rewriting_k_23	UNSAT	0.15
BLOCKS3iii.4	UNSAT	0.15
rewriting_k_25	UNSAT	0.17
z4ml.blif_0.10_1.00_0_1_inp_exact	SAT	0.17
p10-10.pddl_planlen=6	FAIL	0.19
z4ml.blif_0.10_1.00_0_0_inp_exact	UNSAT	0.19
k_d4_p-1	UNSAT	0.19
lights3_021_0_027	UNSAT	0.2
toilet_c_08_01.7	UNSAT	0.23
rewriting_k_30	UNSAT	0.23
z4ml.blif_0.10_0.20_0_1_inp_exact	SAT	0.24
k_ph_n-3	SAT	0.25
z4ml.blif_0.10_1.00_0_1_out_exact	SAT	0.26
z4ml.blif_0.10_0.20_0_0_inp_exact	UNSAT	0.26
BLOCKS3ii.4.3	UNSAT	0.27
z4ml.blif_0.10_0.20_0_1_out_exact	SAT	0.28
toilet_c_06_01.8	UNSAT	0.29
z4ml.blif_0.10_1.00_0_0_out_exact	UNSAT	0.3
p10-10.pddl_planlen=10	FAIL	0.3
k_d4_n-1	SAT	0.3
mutex-4-s	SAT	0.3
toilet_a_06_01.6	UNSAT	0.32
z4ml.blif_0.10_0.20_0_0_out_exact	UNSAT	0.34
k3_1_1	SAT	0.34
incrementer-enc05-uniform-depth-2	UNSAT	0.37
k_path_p-2	UNSAT	0.37
k_ph_p-3	UNSAT	0.38
flipflop-5-c	UNSAT	0.4
lights3_035_0_027	UNSAT	0.41
lights3_035_0_002	UNSAT	0.41
lights3_021_0_009	SAT	0.45
CHAIN12v.13	SAT	0.45
p20-5.pddl_planlen=17	FAIL	0.47
k_dum_n-1	SAT	0.5
Adder2-2-c	UNSAT	0.57
cnt05	SAT	0.6
texas.parsesys^1.E-d4	SAT	0.62
CHAIN14v.15	SAT	0.67
rewriting_k_50	UNSAT	0.68
qshifter_5	SAT	0.71
k_poly_n-2	SAT	0.71
k_lin_p-2	UNSAT	0.75
tlc03-uniform-depth-9	UNSAT	0.82
k_poly_p-2	UNSAT	0.84
p20-5.pddl_planlen=32	FAIL	0.86
adder-2-unsat	UNSAT	0.86
ring_r4_ser--opt-11_	UNSAT	0.9
k_dum_n-3	SAT	0.93
lut4_XOR_f1	SAT	0.93
k_dum_n-2	SAT	0.93
AR-fixpoint-5	FAIL	0.96
CHAIN16v.17	SAT	0.98
k_dum_p-3	UNSAT	1.01
k_dum_p-2	UNSAT	1.02
k_ph_n-4	SAT	1.08
flipflop-6-c	UNSAT	1.1
CHAIN17v.18	SAT	1.14
k_dum_p-4	UNSAT	1.24
k_lin_p-3	UNSAT	1.32
query48_query15_1344	UNSAT	1.33
CHAIN18v.19	SAT	1.33
BLOCKS3iii.5	SAT	1.4
tlc03-nonuniform-depth-17	UNSAT	1.41
toilet_a_06_01.10	UNSAT	1.45
cube_c3_ser--opt-6_	SAT	1.52
CHAIN19v.20	SAT	1.55
lights3_035_0_051	UNSAT	1.67
toilet_a_08_05.2	UNSAT	1.73
BLOCKS3ii.5.2	UNSAT	1.76
CHAIN20v.21	SAT	1.8
k_dum_n-5	SAT	1.88
s27_d2_s	SAT	1.92
C432.blif_0.10_1.00_0_1_inp_exact	SAT	1.92
C432.blif_0.10_1.00_0_0_inp_exact	UNSAT	1.96
k_grz_n-2	SAT	1.98
k_branch_n-2	SAT	2
c4_BMC_p1_k32	SAT	2
connect_5x4_3_D	UNSAT	2.03
CHAIN21v.22	SAT	2.07
mutex-8-s	SAT	2.08
rewriting_k_75	UNSAT	2.11
k_path_n-3	SAT	2.22
k_lin_p-4	UNSAT	2.26
CHAIN22v.23	SAT	2.36
b12_PR_9_2	SAT	2.39
C432.blif_0.10_1.00_0_1_out_exact	SAT	2.43
C432.blif_0.10_1.00_0_0_out_exact	UNSAT	2.5
k_poly_p-4	UNSAT	2.51
toilet_c_08_01.11	UNSAT	2.53
k_dum_p-6	UNSAT	2.56
lut4_XOR_fOR	UNSAT	2.57
BLOCKS3ii.5.3	SAT	2.65
flipflop-7-c	UNSAT	2.67
CHAIN23v.24	SAT	2.74
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-003	UNSAT	2.79
tlc03-uniform-depth-21	UNSAT	3.07
k_ph_p-5	UNSAT	3.14
k_grz_n-4	SAT	3.17
C499.blif_0.10_1.00_0_1_inp_exact	SAT	3.59
C499.blif_0.10_1.00_0_1_out_exact	SAT	3.64
k_poly_n-5	SAT	3.68
C499.blif_0.10_1.00_0_0_inp_exact	UNSAT	3.79
BLOCKS3i.5.3	UNSAT	3.91
vis.prodcell^01.E-d2	SAT	3.94
toilet_c_08_05.4	SAT	4.1
k_lin_p-8	UNSAT	4.3
k_grz_n-5	SAT	4.4
term1.blif_0.10_1.00_0_1_inp_exact	SAT	4.46
lut4_AND_fXOR	UNSAT	4.56
k_d4_n-2	SAT	4.59
term1.blif_0.10_1.00_0_0_inp_exact	UNSAT	4.59
k_path_p-5	UNSAT	4.66
k_poly_n-6	SAT	4.7
irst.dme6.B-d2	SAT	4.7
BLOCKS3i.5.4	SAT	4.78
s01238_PR_8_2	SAT	4.88
toilet_c_10_01.12	UNSAT	4.94
C499.blif_0.10_1.00_0_0_out_exact	UNSAT	4.99
k_lin_p-9	UNSAT	5.11
ring_r3_ser--opt-8_	SAT	5.27
query01_ntrivil_1344	UNSAT	5.32
szymanski-5-s	UNSAT	5.51
s298_d2_s	SAT	5.54
connect_6x5_5_D	UNSAT	5.57
rewriting_k_100	UNSAT	5.59
k_grz_n-7	SAT	5.62
k_dum_n-9	SAT	5.74
driverlog01_7	SAT	5.85
flipflop-8-c	UNSAT	5.86
k_ph_n-6	SAT	5.9
term1.blif_0.10_1.00_0_1_out_exact	SAT	5.94
k_d4_p-4	UNSAT	5.94
qshifter_6	SAT	6.05
term1.blif_0.10_1.00_0_0_out_exact	UNSAT	6.11
cnt07e	SAT	6.43
k_lin_p-10	UNSAT	6.68
k_poly_n-7	SAT	7.21
toilet_a_08_01.13	UNSAT	7.4
k_lin_p-11	UNSAT	7.41
vonNeumann-ripple-carry-5-c	UNSAT	7.59
k_branch_n-3	SAT	7.74
k_poly_p-7	UNSAT	8
BLOCKS4iii.6	UNSAT	8.12
c4_BMC_p2_k128	UNSAT	8.15
sortnetsort5.v.stepl.004	UNSAT	8.21
k_dum_n-11	SAT	8.26
k_lin_p-12	UNSAT	8.39
p20-20.pddl_planlen=23	FAIL	8.52
mutex-16-s	SAT	9.19
k_ph_n-8	SAT	9.83
k_grz_n-8	SAT	9.88
k_dum_p-12	UNSAT	10.15
k_grz_n-6	SAT	10.19
k_path_n-6	SAT	11.27
toilet_a_10_05.3	UNSAT	11.33
k_lin_p-14	UNSAT	11.34
k_dum_n-12	SAT	11.36
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-005	UNSAT	11.67
flipflop-9-c	UNSAT	11.93
eijk.S382.S-d4	SAT	12
k_poly_p-9	UNSAT	12.29
k_grz_p-5	UNSAT	12.39
k_poly_p-8	UNSAT	12.39
query11_query21_1344	UNSAT	13.21
driverlog03_7	SAT	13.61
k_lin_p-19	UNSAT	14.12
vis.4-arbit^2.E-f2	SAT	14.36
k_path_n-4	SAT	14.49
ken.flash^10.C-f2	UNSAT	16.2
term1.blif_0.10_0.20_0_1_out_exact	SAT	16.28
lut4_2_f1	SAT	16.29
tlc03-uniform-depth-52	UNSAT	16.46
k_dum_p-14	UNSAT	16.48
k_grz_p-4	UNSAT	17.5
k_ph_n-9	SAT	17.82
k_lin_n-3	SAT	18.74
k_dum_p-17	UNSAT	19.09
k_dum_n-18	SAT	19.35
term1.blif_0.10_0.20_0_1_inp_exact	SAT	19.4
vonNeumann-ripple-carry-6-c	UNSAT	19.65
k_dum_p-20	UNSAT	20.59
k_path_n-5	SAT	20.73
ev-pr-4x4-7-3-0-0-1-lg	SAT	20.8
incrementer-enc03-nonuniform-depth-13	UNSAT	21.4
s510_d24_s	FAIL	21.54
k_poly_p-11	UNSAT	21.61
C5315.blif_0.10_1.00_0_1_inp_exact	SAT	21.66
szymanski-16-s	FAIL	21.83
szymanski-18-s	FAIL	21.94
s1269_d10_s	FAIL	22.04
s510_d28_s	FAIL	22.04
szymanski-20-s	FAIL	22.06
cnt08e	SAT	22.13
s510_d36_s	FAIL	22.14
s1269_d14_u	FAIL	22.15
s510_d31_s	FAIL	22.23
s1269_d15_u	FAIL	22.24
s510_d35_s	FAIL	22.24
s3330_d5_s	FAIL	22.33
s1269_d13_u	FAIL	22.33
s1269_d12_u	FAIL	22.35
s3330_d4_s	FAIL	22.43
k_dum_p-21	UNSAT	22.44
s510_d32_s	FAIL	22.53
s3330_d7_s	FAIL	22.64
query21_ntrivil_1344	UNSAT	22.82
flipflop-10-c	UNSAT	22.83
s3330_d8_s	FAIL	23.03
fpu-10Xh-error01-uniform-depth-5	FAIL	23.44
s3330_d9_s	FAIL	23.53
szymanski-24-s	FAIL	23.64
connect_7x6_4_W	UNSAT	23.95
s3330_d10_u	FAIL	24.03
fpu-10Xe-correct01-nonuniform-depth-6	FAIL	24.24
C5315.blif_0.10_1.00_0_1_out_exact	SAT	24.56
fpu-10Xh-correct04-uniform-depth-8	FAIL	24.93
lut4_2_f2	UNSAT	25.03
s510_d23_s	FAIL	25.23
vonNeumann-ripple-carry-11-c	FAIL	25.24
toilet_a_08_05.9	SAT	25.62
BLOCKS4i.6.4	UNSAT	25.63
s3330_d12_u	FAIL	26.14
ev-pr-6x6-19-5-0-1-2-s	FAIL	26.24
k_t4p_p-4	UNSAT	26.89
BLOCKS4ii.7.2	UNSAT	27.41
fpu-10Xh-correct04-uniform-depth-14	FAIL	27.55
fpu-10Xh-correct04-uniform-depth-15	FAIL	27.65
k_branch_p-5	UNSAT	27.83
c1_BMC_p1_k4	SAT	28.1
fpu-10Xh-correct04-uniform-depth-16	FAIL	28.15
qshifter_8	FAIL	28.23
emptyroom_e3_ser--opt-20_	SAT	28.3
s3330_d14_u	FAIL	28.34
fpu-10Xh-correct04-nonuniform-depth-18	FAIL	28.43
vonNeumann-ripple-carry-12-c	FAIL	28.83
vonNeumann-ripple-carry-13-c	FAIL	29.25
lut4_2_fXOR	SAT	29.53
C5315.blif_0.10_1.00_0_0_inp_exact	UNSAT	29.59
k5_2_3	SAT	29.76
dungeon_i15-m7-u4-v0.pddl_planlen=81	UNSAT	29.93
fpu-10Xe-correct01-uniform-depth-22	FAIL	30.14
k_dum_n-17	SAT	30.58
k_d4_n-3	SAT	30.82
fpu-10Xe-correct01-nonuniform-depth-24	FAIL	30.85
tlc01-uniform-depth-73	UNSAT	30.93
fpu-10Xh-correct04-nonuniform-depth-27	FAIL	31.44
ken.flash^03.C-f3	UNSAT	32.22
k_dum_p-16	UNSAT	32.99
k_grz_p-11	UNSAT	33.68
s1269_d9_s	FAIL	33.73
ev-pr-6x6-17-5-0-1-2-s	FAIL	33.94
k_branch_n-4	SAT	34.4
vonNeumann-ripple-carry-15-c	FAIL	34.44
lognBWLARGEA1	UNSAT	35.17
k_grz_p-10	UNSAT	35.85
szymanski-14-s	FAIL	36.35
s820_d15_u	FAIL	38.03
dungeon_i10-m5-u10-v0.pddl_planlen=23	UNSAT	38.49
mutex-32-s	SAT	39.65
ken.flash^10.C-f3	UNSAT	40.09
k_grz_p-13	UNSAT	40.22
k_grz_p-12	UNSAT	40.93
flipflop-11-c	UNSAT	42.16
vonNeumann-ripple-carry-7-c	UNSAT	43.32
k_poly_p-14	UNSAT	43.45
C5315.blif_0.10_1.00_0_0_out_exact	UNSAT	44.39
k_ph_n-11	SAT	45.05
s820_d14_u	FAIL	46.34
connect_8x7_7_W	UNSAT	47.28
k_grz_p-19	UNSAT	47.69
s1269_d8_s	FAIL	48.33
c1_Debug_s3_f1_e1_v1	FAIL	49.04
k_grz_p-17	UNSAT	49.4
k_dum_n-21	SAT	50.38
k_lin_n-9	SAT	50.97
k_poly_n-14	SAT	51.2
s499_d25_u	FAIL	51.21
k_path_p-10	UNSAT	52.52
c4_Debug_s3_f1_e1_v2	FAIL	52.73
c4_Debug_s3_f1_e2_v2	FAIL	52.75
s499_d24_u	FAIL	55.33
k_branch_p-6	UNSAT	55.54
s713_d11_u	FAIL	56.03
lut4_AND_f1	SAT	58.14
k14_2_3	FAIL	58.47
k5_3_2	SAT	58.53
k_t4p_n-2	SAT	58.55
vonNeumann-ripple-carry-10-c	FAIL	58.93
s641_d11_u	FAIL	60.65
c2_Debug_s3_f1_e1_v2	FAIL	61.34
c4_Debug_s5_f2_e2_v1	FAIL	61.66
c1_BMC_p2_k512	FAIL	62.46
s820_d12_u	FAIL	62.85
c4_Debug_s3_f1_e2_v3	FAIL	63.54
s499_d22_u	FAIL	63.85
s713_d10_u	FAIL	64.73
s3330_d3_s	FAIL	66.83
pipesnotankage14_10	FAIL	67.28
toilet_c_10_01.17	UNSAT	67.43
ev-pr-4x4-11-3-0-0-1-lg	SAT	67.68
k_grz_p-18	UNSAT	67.72
s641_d10_u	FAIL	68.53
s1196_d7_u	FAIL	68.83
k_poly_p-16	UNSAT	70.17
s820_d11_u	FAIL	70.44
s27_d3_u	UNSAT	71
s713_d9_u	FAIL	73.33
c2_BMC_p1_k2048	FAIL	73.95
flipflop-12-c	UNSAT	74.13
s27_d4_u	UNSAT	74.65
s499_d19_s	FAIL	75.03
s298_d25_u	FAIL	75.83
k_grz_p-16	UNSAT	77
s27_d5_u	UNSAT	77.22
s820_d10_s	FAIL	77.33
incrementer-enc07-nonuniform-depth-17	UNSAT	78.03
s499_d18_s	FAIL	78.35
mutex-64-s	SAT	80.3
s1196_d6_u	FAIL	80.44
s713_d8_u	FAIL	81.13
s499_d17_s	FAIL	81.54
k_poly_n-16	SAT	81.62
s298_d22_u	FAIL	83.23
s820_d9_s	FAIL	83.83
driverlog10_6	UNSAT	84.7
s641_d8_u	FAIL	85.23
c1_BMC_p2_k1024	FAIL	85.95
pipesnotankage18_7	FAIL	89.55
pipesnotankage18_8	FAIL	89.55
s499_d15_s	FAIL	89.93
s1269_d5_s	FAIL	90.14
s641_d7_u	FAIL	90.93
k_poly_p-15	UNSAT	91.16
s298_d18_s	FAIL	91.84
s298_d19_u	FAIL	91.93
vonNeumann-ripple-carry-8-c	UNSAT	91.94
s713_d7_u	FAIL	92.13
s1196_d5_u	FAIL	92.74
s510_d11_s	FAIL	93.64
s820_d8_s	FAIL	94.13
ev-pr-6x6-15-5-0-1-2-s	FAIL	95.03
lognBWLARGEB1	UNSAT	95.51
k_grz_n-10	SAT	97.64
k_poly_p-19	UNSAT	97.82
szymanski-12-s	FAIL	99.33
k_d4_p-7	UNSAT	100.38
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-005	UNSAT	103.53
Adder2-16-s	FAIL	105.44
k_grz_n-18	SAT	109.25
k_d4_p-8	UNSAT	109.29
gttt_2_2_0010_3x3_torus_w	UNSAT	109.68
k_grz_n-20	SAT	112.87
k_grz_n-21	SAT	114.16
ev-pr-6x6-13-5-0-1-2-s	FAIL	115.94
tlc04-uniform-depth-36	UNSAT	116.1
k_d4_p-11	UNSAT	117.74
k_lin_n-5	SAT	118.25
s298_d17_s	FAIL	121.93
arbiter-06-comp-error02-qbf-hardness-depth-5	UNSAT	122.38
s05378_PR_9_2	SAT	122.78
incrementer-enc07-nonuniform-depth-21	UNSAT	123.59
k_ph_p-10	UNSAT	125.64
b20_PR_7_90	UNSAT	127.59
s05378_PR_1_75	UNSAT	132.42
cnt10	SAT	134.47
incrementer-enc03-nonuniform-depth-24	UNSAT	134.49
s820_d7_s	FAIL	135.34
vonNeumann-ripple-carry-9-c	FAIL	136.14
k_d4_p-13	UNSAT	136.59
arbiter-07-comp-error01-qbf-hardness-depth-4	UNSAT	137.86
rankfunc17_unsigned_16	SAT	138.84
Adder2-8-c	UNSAT	138.93
k_poly_n-17	SAT	143.7
k_d4_p-10	UNSAT	145.36
k_poly_n-18	SAT	151.9
c3_Debug_s3_f2_e2_v2	FAIL	151.97
dungeon_i25-m12-u5-v0.pddl_planlen=65	UNSAT	153.01
k_lin_n-6	SAT	155.42
k_ph_n-14	SAT	167.88
query03_query25_1344	UNSAT	169.67
k12_4_2	FAIL	173.77
ev-pr-6x6-11-5-0-1-2-s	FAIL	178.35
k6_2_3	SAT	178.62
cube_c11_par---13_	FAIL	187.05
s386_d12_u	FAIL	187.93
qshifter_7	FAIL	190.84
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-010	FAIL	192.03
query26_query34_1344	SAT	195.62
k_branch_p-8	UNSAT	196.67
sortnetsort9.AE.stepl.012	FAIL	196.83
k_poly_n-20	SAT	197.51
stmt27_296_297	FAIL	204.25
biu.mv.xl_ao.bb-b001-p010-IPF02-c07.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003	FAIL	212.45
s386_d4_s	FAIL	212.73
s713_d6_s	FAIL	216.53
k_poly_n-21	SAT	217.92
incrementer-enc02-nonuniform-depth-31	UNSAT	223.17
depots03_9	UNSAT	225.28
c5_BMC_p1_k32	SAT	232.66
test1_quant_squaring2	FAIL	234.84
biu.mv.xl_ao.bb-b001-p005-OPF03-c09.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003	FAIL	235.25
b22_PR_8_20	FAIL	236.65
s499_d12_s	FAIL	237.53
s1196_d2_s	FAIL	238.36
ev-pr-6x6-9-5-0-1-2-s	FAIL	239.24
k_path_p-14	FAIL	245.84
k_path_n-9	FAIL	247.35
k_path_p-15	FAIL	248.66
nusmv.reactor^3.C-d4	FAIL	255.35
cnt14	FAIL	255.6
Adder2-10-s	FAIL	258.35
k_lin_n-15	SAT	258.88
k_path_n-12	FAIL	259.76
sortnetsort7.v.stepl.007	SAT	259.89
adder-14-sat	FAIL	260.33
stmt19_83_412	FAIL	267.13
k_path_n-13	FAIL	269.44
query44_query26_1344n	FAIL	270.13
biu.mv.xl_ao.bb-b001-p010-IPF05-c07.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003	FAIL	270.65
mutex-128-s	FAIL	277.13
k_path_n-14	FAIL	277.44
Core1108_tbm_21.tex.module.000026	FAIL	280.65
c1_Debug_s5_f1_e1_v2	FAIL	281.15
k_d4_n-8	FAIL	281.86
cnt16r	FAIL	282.3
rankfunc22_signed_64	FAIL	282.75
test1_quant_squaring3	FAIL	283.74
biu.mv.xl_ao.bb-b001-p010-IPF02-c08.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003	FAIL	286.74
szymanski-8-s	FAIL	287.24
ev-pr-4x4-7-3-0-0-1-s	FAIL	290.04
biu.mv.xl_ao.bb-b001-p010-OPF02-c08.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003	FAIL	291.84
k_ph_p-15	FAIL	292.55
k_d4_n-10	FAIL	294.45
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-008	FAIL	296.24
tlc04-nonuniform-depth-56	UNSAT	300.21
k_path_p-18	FAIL	301.81
k_path_n-16	FAIL	303.3
rankfunc14_signed_64	FAIL	303.84
Umbrella_tbm_25.tex.moduleQ3.2S.000075	FAIL	307.54
cube_c7_ser--opt-24_	FAIL	307.75
k_branch_n-8	FAIL	308.26
Core1108_tbm_02.tex.moduleQ3.2S.000015	FAIL	310.84
s1269_d4_s	FAIL	311.23
k_d4_n-7	FAIL	311.47
s641_d6_s	FAIL	313.54
k_lin_n-17	FAIL	314.25
s3330_d2_s	FAIL	315.84
test2_quant_squaring2	FAIL	317.33
k_t4p_p-6	FAIL	317.76
k_t4p_n-4	FAIL	321.04
stmt21_79_304	FAIL	324.04
k_path_p-13	FAIL	324.36
s820_d3_s	FAIL	325.23
stmt17_18_19	FAIL	327.15
cube_c9_par--opt-11_	FAIL	327.55
ev-pr-4x4-9-3-0-0-1-lg	FAIL	327.65
k_ph_p-13	FAIL	329.42
ev-pr-6x6-7-5-0-1-2-lg	FAIL	331.05
cnt11	FAIL	332.15
k_t4p_p-9	FAIL	334.34
biu.mv.xl_ao.bb-b001-p005-OPF05-c03.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004	FAIL	341.34
rankfunc5_unsigned_64	FAIL	342.94
test5_quant_squaring4	FAIL	343.05
ev-pr-6x6-5-5-0-1-2-lg	FAIL	343.15
stmt19_217_309	FAIL	344.23
k_path_p-16	FAIL	345.05
k_t4p_p-15	FAIL	345.45
k_t4p_n-6	FAIL	345.75
biu.mv.xl_ao.bb-b001-p005-OPF05-c02.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004	FAIL	346.24
k_lin_n-14	FAIL	347.25
k_d4_n-14	FAIL	348.45
stmt44_916_917	FAIL	348.55
k_t4p_p-12	FAIL	348.65
ev-pr-4x4-5-3-0-0-1-lg	FAIL	351.35
k_ph_n-16	FAIL	351.95
k_path_p-21	FAIL	352.16
rankfunc51_signed_32	FAIL	355.74
ev-pr-4x4-13-3-0-0-1-lg	FAIL	356.05
test5_quant_squaring5	FAIL	356.85
k_t4p_p-20	FAIL	358.87
k8_3_4	FAIL	362.03
tlc02-uniform-depth-114	UNSAT	362.25
k_t4p_n-9	FAIL	363.27
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-008	UNSAT	363.27
rankfunc13_signed_32	FAIL	363.64
k_t4p_n-5	FAIL	366.56
stmt21_319_418	FAIL	367.34
s386_d11_u	FAIL	368.83
connect_5x4_3_R	FAIL	370.05
biu.mv.xl_ao.bb-b003-p020-IPF03-c03.blif-biu.inv.prop.bb-bmc.with-IOC.unfold-009	FAIL	370.13
ev-pr-4x4-15-3-0-0-1-lg	FAIL	371.15
Umbrella_tbm_24.tex.module.000131	FAIL	375.54
k_d4_p-20	FAIL	377.15
ev-pr-8x8-7-7-0-1-2-lg	FAIL	379.74
arbiter-06-comp-error01-qbf-hardness-depth-15	FAIL	379.93
k_t4p_n-8	FAIL	380.26
ken.oop^2.C-d4	FAIL	381.24
k_path_p-19	FAIL	382.14
C432.blif_0.10_0.20_0_0_inp_exact	FAIL	382.86
stmt24_765_766	FAIL	384.44
adder-10-sat	FAIL	385.14
C880.blif_0.10_1.00_0_0_inp_exact	FAIL	385.46
arbiter-07-comp-error01-qbf-hardness-depth-11	FAIL	386.04
ev-pr-6x6-7-5-0-1-2-s	FAIL	389.04
Core1108_tbm_21.tex.module.000027	FAIL	389.74
emptyroom_e4_ser--opt-44_	FAIL	390.11
k_t4p_p-16	FAIL	390.24
k_t4p_p-18	FAIL	391.15
k_d4_p-16	FAIL	391.35
k_d4_n-16	FAIL	393.75
k_t4p_p-10	FAIL	394.55
k_path_n-19	FAIL	395.1
k_lin_n-7	SAT	395.16
b22_C_2_12	FAIL	397.54
C880.blif_0.10_1.00_0_1_inp_exact	FAIL	399.57
ev-pr-4x4-5-3-0-0-1-s	FAIL	399.94
incrementer-enc07-uniform-depth-25	UNSAT	400.06
stmt16_950_951	FAIL	403.76
ev-pr-8x8-5-7-0-1-2-lg	FAIL	404.86
C432.blif_0.10_0.20_0_1_inp_exact	FAIL	405.24
k_t4p_p-17	FAIL	406.07
s510_d3_s	FAIL	408.63
stmt23_72_76	FAIL	412.65
k_d4_p-17	FAIL	414.55
rankfunc33_signed_32	FAIL	415.54
Umbrella_tbm_05.tex.module.000039	FAIL	417.63
test2_quant_squaring3	FAIL	418.14
stmt41_738_749	FAIL	419.74
rankfunc5_signed_32	FAIL	419.93
ev-pr-6x6-9-5-0-1-2-lg	FAIL	420.75
szymanski-10-s	FAIL	425.23
k_t4p_n-12	FAIL	427.25
s713_d2_s	FAIL	432.03
C499.blif_0.10_0.20_0_0_inp_exact	FAIL	433.68
k_d4_n-20	FAIL	434.85
s641_d3_s	FAIL	436.35
k_branch_n-9	FAIL	441.81
sortnetsort10.v.stepl.005	FAIL	444.85
sortnetsort8.AE.stepl.003	FAIL	449.95
test4_quant_squaring4	FAIL	451.15
emptyroom_e4_par---21_	FAIL	451.35
uclid-pipe3a	FAIL	455.24
biu.mv.xl_ao.bb-b001-p010-MIF04-c06.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-005	FAIL	455.94
arbiter-06-comp-error01-qbf-hardness-depth-12	FAIL	455.94
stmt25_52_53	FAIL	457.34
ev-pr-6x6-11-5-0-1-2-lg	FAIL	460.14
k_t4p_n-15	FAIL	461.64
k_branch_n-11	FAIL	467.25
C880.blif_0.10_1.00_0_1_out_exact	FAIL	467.95
s298_d4_s	FAIL	468.34
C880.blif_0.10_1.00_0_0_out_exact	FAIL	470.24
test3_quant_squaring4	FAIL	470.54
dungeon_i10-m10-u10-v0.pddl_planlen=187	UNSAT	471.12
ev-pr-4x4-9-3-0-0-1-s	FAIL	472.64
s641_d2_s	FAIL	476.53
s1196_d4_u	FAIL	477.44
sortnetsort9.v.stepl.005	FAIL	477.95
nusmv.tcas^3.B-f2	FAIL	479.84
k_branch_n-16	FAIL	480.24
k_branch_p-16	FAIL	480.34
k8_3_2	FAIL	480.76
stmt17_63_82	FAIL	480.84
k_branch_p-11	FAIL	481.14
stmt23_66_96	FAIL	482.63
Core1108_tbm_21.tex.module.000008	FAIL	484.83
k_lin_n-8	SAT	485.67
sortnetsort9.v.stepl.007	FAIL	486.27
C499.blif_0.10_0.20_0_1_inp_exact	FAIL	486.35
C880.blif_0.10_0.20_0_0_out_exact	FAIL	486.65
s713_d3_s	FAIL	488.93
test4_quant_squaring2	FAIL	489.95
k_branch_p-10	FAIL	495.24
Core1108_tbm_21.tex.module.000030	FAIL	496.04
s1196_1_5	FAIL	496.34
k_branch_p-12	FAIL	499.35
connect_5x4_4_R	FAIL	501.54
ken.flash^08.C-d4	FAIL	501.65
s298_d14_s	FAIL	502.75
biu.mv.xl_ao.bb-b001-p010-MIF01-c01.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004	FAIL	503.24
Umbrella_tbm_24.tex.module.000066	FAIL	503.85
stmt28_68_81	FAIL	505.63
stmt19_64_99	FAIL	509.44
k_t4p_n-14	FAIL	511.74
k_d4_n-15	FAIL	513.24
gttt_1_1_00101121_4x4_torus_w	FAIL	514.85
Adder2-8-s	FAIL	520.63
stmt17_62_98	FAIL	520.73
biu.mv.xl_ao.bb-b001-p010-MIF05-c07.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004	FAIL	523.05
k_t4p_n-13	FAIL	523.64
s820_d2_s	FAIL	525.64
ev-pr-8x8-9-7-0-1-2-lg	FAIL	526.45
nusmv.tcas^6.B-f4	FAIL	529.35
stmt17_70_98	FAIL	529.73
f600-50	FAIL	530.44
b21_C_3_206	FAIL	535.75
ev-pr-4x4-17-3-0-0-1-lg	FAIL	536.05
uclid-pipe2	FAIL	540.15
k_branch_n-12	FAIL	545.95
gttt_2_1_000111_3x3_torus_b	FAIL	553.15
s713_d5_s	FAIL	554.93
stmt17_82_98	FAIL	558.63
s386_d6_s	FAIL	561.43
k_lin_n-11	FAIL	565.56
stmt17_86_98	FAIL	568.13
s386_d10_u	FAIL	568.23
ev-pr-8x8-11-7-0-1-2-lg	FAIL	572.35
C880.blif_0.10_0.20_0_1_out_exact	FAIL	575.15
s641_d5_s	FAIL	579.63
k8_2_3	FAIL	583.25
ev-pr-6x6-15-5-0-1-2-lg	FAIL	590.04
ev-pr-6x6-5-5-0-1-2-s	FAIL	599.12
query51_query50_1344	FAIL	599.12
filesys_smbmrx_cvsndrcv.c	FAIL	599.12
input_pnpi8042_moudep.c	FAIL	599.12
par8-4-50	FAIL	599.12
stmt27_16_97	FAIL	599.12
texas.two_proc^4.E-f2	FAIL	599.12
C6288.blif_0.10_0.20_0_1_inp_exact	FAIL	599.12
szymanski-6-s	FAIL	599.12
s510_d6_s	FAIL	599.12
s1269_d3_s	FAIL	599.12
stmt19_90_266	FAIL	599.12
C432.blif_0.10_0.20_0_0_out_exact	FAIL	599.21
gttt_2_2_00101121_3x3_b	FAIL	599.22
gttt_2_2_001020_4x4_w	FAIL	599.22
C6288.blif_0.10_0.20_0_1_out_exact	FAIL	599.22
C5315.blif_0.10_0.20_0_1_inp_exact	FAIL	599.22
ev-pr-8x8-19-7-0-1-2-lg	FAIL	599.22
dungeon_i25-m12-u5-v0.pddl_planlen=170	FAIL	599.22
ev-pr-8x8-17-7-0-1-2-lg	FAIL	599.22
c3_BMC_p1_k256	FAIL	599.22
k_branch_p-14	FAIL	599.22
C880.blif_0.10_0.20_0_1_inp_exact	FAIL	599.22
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-007	FAIL	599.22
k_branch_p-18	FAIL	599.22
c2_Debug_s3_f2_e1_v3	FAIL	599.22
gttt_2_1_00102030_4x4_torus_b	FAIL	599.22
emptyroom_e3_ser---19_	FAIL	599.22
ev-pr-4x4-17-3-0-0-1-s	FAIL	599.22
dungeon_i10-m5-u10-v0.pddl_planlen=134	FAIL	599.22
uclid-pipe3b	FAIL	599.22
C432.blif_0.10_0.20_0_1_out_exact	FAIL	599.22
gttt_1_1_000111_3x3_torus_w	FAIL	599.22
ev-pr-4x4-13-3-0-0-1-s	FAIL	599.22
gttt_1_1_001020_3x3_w	FAIL	599.22
connect_8x7_5_R	FAIL	599.22
gttt_2_1_00011020_4x4_b	FAIL	599.22
k_branch_n-10	FAIL	599.22
k_branch_n-20	FAIL	599.22
gttt_2_1_0010_4x4_torus_b	FAIL	599.22
query31_reachqu_1344n	FAIL	599.22
s713_d4_s	FAIL	599.22
k_ph_p-18	FAIL	599.22
lut4_3_fAND	FAIL	599.22
k_ph_p-19	FAIL	599.22
C6288.blif_0.10_0.20_0_0_out_exact	FAIL	599.22
s499_d7_s	FAIL	599.22
ev-pr-4x4-15-3-0-0-1-s	FAIL	599.22
s386_d3_s	FAIL	599.22
connect_8x7_6_R	FAIL	599.22
s386_d9_u	FAIL	599.22
s298_d10_s	FAIL	599.22
s09234_PR_8_2	FAIL	599.22
s09234_PR_8_5	FAIL	599.22
s15850_PR_2_2	FAIL	599.22
eijk.bs4863.S-d4	FAIL	599.22
ken.oop^2.C-d3	FAIL	599.22
query42_query06_1344n	FAIL	599.22
sortnetsort9.AE.stepl.009	FAIL	599.22
C6288.blif_0.10_0.20_0_0_inp_exact	FAIL	599.22
sortnetsort8.v.stepl.007	FAIL	599.22
s386_d7_s	FAIL	599.22
s386_d2_s	FAIL	599.22
connect_8x7_4_R	FAIL	599.22
texas.PI_main^16.E-f2	FAIL	599.22
ev-pr-6x6-19-5-0-1-2-lg	FAIL	599.22
C6288.blif_0.10_1.00_0_0_out_exact	FAIL	599.22
texas.PI_main^08.E-f3	FAIL	599.22
ev-pr-8x8-13-7-0-1-2-lg	FAIL	599.22
texas.PI_main^05.E-f3	FAIL	599.22
nusmv.tcas-t^1.B-d2	FAIL	599.22
s15850_PR_8_50	FAIL	599.22
ev-pr-6x6-13-5-0-1-2-lg	FAIL	599.22
rankfunc13_unsigned_64	FAIL	599.22
s1196_d3_u	FAIL	599.22
network_irda_miniport_nscirda_settings.c	FAIL	599.22
network_ndis_rtlnwifi_hw_hw_ccmp.c	FAIL	599.22
hid_hclient_ecdisp.c	FAIL	599.22
network_trans_sys_notify.c	FAIL	599.22
audio_ddksynth_csynth2.cpp	FAIL	599.22
kernel_agplib_intrface.c	FAIL	599.22
incrementer-enc02-uniform-depth-58	FAIL	599.22
stmt41_160_235	FAIL	599.22
stmt19_3_214	FAIL	599.22
stmt29_226_376	FAIL	599.22
incrementer-enc06-uniform-depth-24	FAIL	599.22
adder-12-unsat	FAIL	599.22
C499.blif_0.10_0.20_0_0_out_exact	FAIL	599.22
incrementer-enc08-uniform-depth-33	FAIL	599.22
stmt52_244_394	FAIL	599.22
ev-pr-4x4-11-3-0-0-1-s	FAIL	599.22
rankfunc3_signed_64	FAIL	599.22
test3_quant_squaring2	FAIL	599.22
ev-pr-6x6-17-5-0-1-2-lg	FAIL	599.22
C6288.blif_0.10_1.00_0_0_inp_exact	FAIL	599.22
C5315.blif_0.10_0.20_0_1_out_exact	FAIL	599.22
Core1108_tbm_03.tex.moduleQ3.2S.000002	FAIL	599.22
adder-12-sat	FAIL	599.22
s298_d12_s	FAIL	599.22
ev-pr-8x8-15-7-0-1-2-lg	FAIL	599.22
C6288.blif_0.10_1.00_0_1_out_exact	FAIL	599.22
term1.blif_0.10_0.20_0_0_inp_exact	FAIL	599.22
s499_d9_s	FAIL	599.22
k8_4_3	FAIL	599.22
C880.blif_0.10_0.20_0_0_inp_exact	FAIL	599.22
k_ph_n-21	FAIL	599.22
k_branch_p-21	FAIL	599.22
stmt17_70_90	FAIL	599.22
C5315.blif_0.10_0.20_0_0_inp_exact	FAIL	599.22
C499.blif_0.10_0.20_0_1_out_exact	FAIL	599.22
s641_d4_s	FAIL	599.22
C6288.blif_0.10_1.00_0_1_inp_exact	FAIL	599.22
connect_9x8_6_R	FAIL	599.22
arbiter-10-comp-error01-qbf-hardness-depth-22	FAIL	599.22
aim-100-6_0-yes1-3-50	FAIL	599.22
aim-100-1_6-yes1-2-00	FAIL	599.22
c5_BMC_p2_k64	FAIL	599.22
arbiter-10-comp-error01-qbf-hardness-depth-10	FAIL	599.22
arbiter-08-comp-error02-qbf-hardness-depth-9	FAIL	599.22
arbiter-07-comp-error02-qbf-hardness-depth-6	FAIL	599.22
aim-200-1_6-yes1-4-90	FAIL	599.22
b20_C_3_2	FAIL	599.22
tlc02-uniform-depth-241	FAIL	599.22
C5315.blif_0.10_0.20_0_0_out_exact	FAIL	599.22
term1.blif_0.10_0.20_0_0_out_exact	FAIL	599.22
par8-1-c-50	FAIL	599.22
k_ph_p-12	FAIL	599.22
par16-1-50	FAIL	599.22
jnh212-50	FAIL	599.22
input_mouser_cseries.c	FAIL	599.22
s386_d8_u	FAIL	599.22
ii32b1-00	FAIL	599.22
b20_PR_7_20	FAIL	599.22
aim-50-6_0-yes1-3-50	FAIL	599.22
arbiter-07-comp-error01-qbf-hardness-depth-20	FAIL	599.22
c5_BMC_p2_k128	FAIL	599.32
dungeon_i25-m12-u3-v0.pddl_planlen=130	FAIL	599.32
dungeon_i25-m12-u3-v0.pddl_planlen=165	FAIL	599.32
dungeon_i25-m12-u3-v0.pddl_planlen=190	FAIL	599.32
dungeon_i25-m12-u3-v0.pddl_planlen=72	FAIL	599.32
c4_Debug_s3_f2_e2_v2	FAIL	599.32
tlc04-nonuniform-depth-98	FAIL	599.32
network_irda_miniport_nscirda_comm.c	FAIL	599.32
k_ph_p-20	FAIL	599.32
sortnetsort8.v.stepl.009	FAIL	599.32

QBF Solver Evaluation Portal

QBFEVALs

QBF GALLERIES

DOWNLOADS

qbflib.org

Instances solved by iprover-QBF
QBFEVAL'16 - Prenex CNF Track.

QBF Solver Evaluation Portal

QBFEVALs

QBF GALLERIES

DOWNLOADS

qbflib.org

Instances solved by iprover-QBF QBFEVAL'16 - Prenex CNF Track.

Instances solved by iprover-QBF
QBFEVAL'16 - Prenex CNF Track.