Instances solved by <a href='solver_detail.php?solver=104'>AIGSolve</a> <br> QBFEVAL'16

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

Instance	Result	Time
z4ml.blif_0.10_1.00_0_1_out_exact	SAT	0
mutex-4-s	SAT	0
toilet_g_02_01.2	SAT	0
z4ml.blif_0.10_0.20_0_0_inp_exact	UNSAT	0
impl12	SAT	0
tree-exa2-25	UNSAT	0
z4ml.blif_0.10_0.20_0_0_out_exact	UNSAT	0
impl02	SAT	0
impl08	SAT	0
k_lin_p-2	UNSAT	0
stmt44_107_108	SAT	0
qshifter_3	SAT	0
impl06	SAT	0
toilet_c_08_01.2	UNSAT	0
k_d4_p-1	UNSAT	0
z4ml.blif_0.10_1.00_0_0_out_exact	UNSAT	0
k_ph_n-4	SAT	0
z4ml.blif_0.10_1.00_0_1_inp_exact	SAT	0
tree-exa2-35	UNSAT	0
impl18	SAT	0
k3_1_1	SAT	0
stmt44_107_113	SAT	0
stmt1_30_31	SAT	0
z4ml.blif_0.10_1.00_0_0_inp_exact	UNSAT	0
z4ml.blif_0.10_0.20_0_1_inp_exact	SAT	0
tree-exa2-30	UNSAT	0
CHAIN12v.13	SAT	0
lognBWLARGEB0	UNSAT	0
lognBWLARGEA0	UNSAT	0
k_ph_p-3	UNSAT	0
cnt02e	SAT	0
tree-exa2-20	UNSAT	0
cnt01	SAT	0
tree-exa2-40	UNSAT	0
tree-exa2-50	UNSAT	0
z4ml.blif_0.10_0.20_0_1_out_exact	SAT	0
k_ph_p-1	UNSAT	0
s27_d2_s	SAT	0
k_lin_p-3	UNSAT	0
BLOCKS3iii.4	UNSAT	0
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
impl04	SAT	0
CHAIN14v.15	SAT	0
tree-exa10-10	SAT	0
lut4_XOR_f1	SAT	0
k_ph_n-1	SAT	0
tree-exa2-10	UNSAT	0
k_ph_n-3	SAT	0
mutex-2-s	SAT	0
toilet_c_08_01.6	UNSAT	0
impl10	SAT	0
toilet_a_04_05.2	SAT	0
rewriting_k_21	UNSAT	0
tree-exa10-30	SAT	0
rewriting_k_19	UNSAT	0
rewriting_k_17	UNSAT	0
toilet_a_04_01.6	UNSAT	0
toilet_g_06_01.2	SAT	0
lights3_021_0_027	UNSAT	0
toilet_c_04_01.4	UNSAT	0
toilet_a_04_01.4	UNSAT	0
toilet_c_06_01.4	UNSAT	0
cnt05	SAT	0
toilet_g_15_01.2	SAT	0
tree-exa2-45	UNSAT	0
rewriting_k_23	UNSAT	0
toilet_g_04_01.2	SAT	0
flipflop-3-c	UNSAT	0
toilet_g_10_01.2	SAT	0
counter_e_2	SAT	0
impl14	SAT	0
rewriting_k_30	UNSAT	0
rewriting_k_10	UNSAT	0
impl20	SAT	0
toilet_g_08_01.2	SAT	0
rewriting_k_25	UNSAT	0
impl16	SAT	0
toilet_a_02_10.2	SAT	0
incrementer-enc05-uniform-depth-2	UNSAT	0.01
CHAIN17v.18	SAT	0.01
flipflop-4-c	UNSAT	0.01
toilet_c_06_01.8	UNSAT	0.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-003	UNSAT	0.01
CHAIN19v.20	SAT	0.01
k_path_p-2	UNSAT	0.01
s27_d4_u	UNSAT	0.01
k_poly_n-2	SAT	0.01
CHAIN18v.19	SAT	0.01
rewriting_k_50	UNSAT	0.01
adder-2-unsat	UNSAT	0.01
toilet_c_08_05.4	SAT	0.01
CHAIN20v.21	SAT	0.01
toilet_c_08_01.7	UNSAT	0.01
s27_d3_u	UNSAT	0.01
k_poly_p-2	UNSAT	0.01
lights3_035_0_002	UNSAT	0.01
CHAIN16v.17	SAT	0.01
lut4_XOR_fOR	UNSAT	0.01
lights3_035_0_027	UNSAT	0.01
BLOCKS3ii.4.3	UNSAT	0.01
mutex-8-s	SAT	0.01
k_lin_p-4	UNSAT	0.01
s27_d5_u	UNSAT	0.01
k_d4_n-1	SAT	0.01
k_dum_n-1	SAT	0.01
stmt17_18_19	SAT	0.01
k_ph_p-5	UNSAT	0.02
CHAIN23v.24	SAT	0.02
k_lin_p-8	UNSAT	0.02
texas.parsesys^1.E-d4	SAT	0.02
rewriting_k_75	UNSAT	0.02
lights3_021_0_009	SAT	0.02
qshifter_4	SAT	0.02
eijk.S382.S-d4	SAT	0.02
BLOCKS3ii.5.2	UNSAT	0.02
k_lin_p-9	UNSAT	0.02
BLOCKS3iii.5	SAT	0.02
CHAIN22v.23	SAT	0.02
mutex-16-s	SAT	0.02
stmt27_296_297	SAT	0.02
C432.blif_0.10_1.00_0_1_inp_exact	SAT	0.02
C432.blif_0.10_1.00_0_1_out_exact	SAT	0.02
CHAIN21v.22	SAT	0.02
toilet_g_20_01.2	SAT	0.02
k_dum_n-3	SAT	0.03
k_poly_p-4	UNSAT	0.03
k_dum_n-2	SAT	0.03
tlc03-uniform-depth-9	UNSAT	0.03
k_lin_p-10	UNSAT	0.03
cube_c3_ser--opt-6_	SAT	0.03
toilet_c_08_01.11	UNSAT	0.03
k_lin_p-11	UNSAT	0.03
p5-5.pddl_planlen=5	SAT	0.03
flipflop-5-c	UNSAT	0.03
test3_quant_squaring2	UNSAT	0.03
k_dum_p-3	UNSAT	0.03
k_ph_n-6	SAT	0.03
BLOCKS3ii.5.3	SAT	0.03
k_dum_p-2	UNSAT	0.03
C432.blif_0.10_1.00_0_0_inp_exact	UNSAT	0.04
k_lin_p-12	UNSAT	0.04
k_dum_n-5	SAT	0.04
ken.flash^10.C-f2	UNSAT	0.04
k_poly_n-6	SAT	0.04
stmt44_916_917	SAT	0.04
k_poly_n-5	SAT	0.04
rewriting_k_100	UNSAT	0.04
k_path_n-3	SAT	0.04
k_dum_p-4	UNSAT	0.04
k_lin_p-14	UNSAT	0.05
BLOCKS3i.5.3	UNSAT	0.05
driverlog01_7	SAT	0.05
vis.prodcell^01.E-d2	SAT	0.05
c4_BMC_p1_k32	SAT	0.05
stmt24_765_766	SAT	0.05
vonNeumann-ripple-carry-5-c	UNSAT	0.05
C432.blif_0.10_1.00_0_0_out_exact	UNSAT	0.05
stmt16_950_951	SAT	0.06
k_poly_p-7	UNSAT	0.06
k_d4_n-2	SAT	0.06
k_branch_n-2	SAT	0.06
sortnetsort5.v.stepl.004	UNSAT	0.06
k_path_n-4	SAT	0.06
p5-5.pddl_planlen=6	SAT	0.06
test4_quant_squaring2	UNSAT	0.06
k_dum_p-6	UNSAT	0.06
k_path_p-5	UNSAT	0.06
k_poly_n-7	SAT	0.06
BLOCKS3i.5.4	SAT	0.07
k_poly_p-8	UNSAT	0.07
mutex-32-s	SAT	0.07
driverlog03_7	SAT	0.07
k_grz_n-2	SAT	0.07
toilet_a_06_01.6	UNSAT	0.07
ken.flash^10.C-f3	UNSAT	0.07
lights3_035_0_051	UNSAT	0.07
k_grz_n-4	SAT	0.08
k_dum_n-9	SAT	0.08
k_d4_p-4	UNSAT	0.08
k_grz_p-4	UNSAT	0.08
k_poly_p-9	UNSAT	0.08
k_t4p_n-2	SAT	0.09
irst.dme6.B-d2	SAT	0.09
k_path_n-5	SAT	0.09
b12_PR_9_2	SAT	0.09
term1.blif_0.10_0.20_0_1_out_exact	SAT	0.1
connect_5x4_3_D	UNSAT	0.1
k_lin_p-19	UNSAT	0.1
tlc03-nonuniform-depth-17	UNSAT	0.1
term1.blif_0.10_0.20_0_0_out_exact	UNSAT	0.1
term1.blif_0.10_1.00_0_1_inp_exact	SAT	0.11
k_path_n-6	SAT	0.11
term1.blif_0.10_1.00_0_1_out_exact	SAT	0.11
vonNeumann-ripple-carry-6-c	UNSAT	0.11
s01238_PR_8_2	SAT	0.11
k_dum_p-12	UNSAT	0.11
c4_BMC_p2_k128	UNSAT	0.11
k_dum_n-11	SAT	0.11
Adder2-2-c	UNSAT	0.12
k_dum_n-12	SAT	0.12
flipflop-6-c	UNSAT	0.12
k_d4_n-3	SAT	0.12
term1.blif_0.10_1.00_0_0_inp_exact	UNSAT	0.12
k_grz_p-5	UNSAT	0.13
k_dum_p-14	UNSAT	0.13
C499.blif_0.10_1.00_0_1_inp_exact	SAT	0.14
term1.blif_0.10_1.00_0_0_out_exact	UNSAT	0.14
k_d4_p-7	UNSAT	0.14
C499.blif_0.10_1.00_0_1_out_exact	SAT	0.14
k_dum_p-16	UNSAT	0.15
k_t4p_p-4	UNSAT	0.15
ring_r4_ser--opt-11_	UNSAT	0.15
toilet_c_10_01.12	UNSAT	0.15
tlc03-uniform-depth-21	UNSAT	0.16
k_path_n-9	SAT	0.16
k_d4_p-8	UNSAT	0.16
aim-100-1_6-yes1-2-00	SAT	0.16
stmt41_738_749	SAT	0.16
k_dum_p-17	UNSAT	0.16
k_path_p-10	UNSAT	0.17
k_grz_n-5	SAT	0.17
C432.blif_0.10_0.20_0_0_out_exact	UNSAT	0.18
k_grz_n-6	SAT	0.18
par8-1-c-50	UNSAT	0.18
lognBWLARGEA1	UNSAT	0.18
k_dum_n-17	SAT	0.18
C432.blif_0.10_0.20_0_1_out_exact	UNSAT	0.18
k_dum_p-20	UNSAT	0.19
aim-50-6_0-yes1-3-50	UNSAT	0.19
k_dum_n-18	SAT	0.19
toilet_a_06_01.10	UNSAT	0.19
connect_6x5_5_D	UNSAT	0.19
vis.4-arbit^2.E-f2	SAT	0.2
k_dum_p-21	UNSAT	0.2
s298_d2_s	SAT	0.2
k_grz_n-7	SAT	0.21
k_d4_p-10	UNSAT	0.21
k_t4p_p-6	UNSAT	0.21
C880.blif_0.10_1.00_0_0_out_exact	UNSAT	0.21
term1.blif_0.10_0.20_0_1_inp_exact	SAT	0.22
vonNeumann-ripple-carry-7-c	UNSAT	0.22
C880.blif_0.10_1.00_0_1_out_exact	SAT	0.22
k_t4p_n-4	SAT	0.23
k_dum_n-21	SAT	0.23
k_poly_p-14	UNSAT	0.23
mutex-64-s	SAT	0.24
k_d4_p-11	UNSAT	0.24
incrementer-enc03-nonuniform-depth-13	UNSAT	0.25
k_branch_n-3	SAT	0.25
k_path_n-12	SAT	0.25
k_grz_n-8	SAT	0.26
term1.blif_0.10_0.20_0_0_inp_exact	UNSAT	0.26
k_path_p-13	UNSAT	0.27
qshifter_5	SAT	0.27
k_path_n-13	SAT	0.28
stmt25_52_53	SAT	0.28
k_d4_p-13	UNSAT	0.29
k_t4p_n-5	SAT	0.3
k_path_p-14	UNSAT	0.3
k_path_n-14	SAT	0.31
k_t4p_p-9	UNSAT	0.32
k_poly_p-15	UNSAT	0.32
k_path_p-15	UNSAT	0.33
k_lin_n-3	SAT	0.33
k_grz_p-10	UNSAT	0.34
C880.blif_0.10_0.20_0_0_out_exact	UNSAT	0.34
C880.blif_0.10_0.20_0_1_out_exact	UNSAT	0.34
k_path_p-16	UNSAT	0.35
k_t4p_p-10	UNSAT	0.36
k_path_n-16	SAT	0.37
k_d4_p-16	UNSAT	0.38
k_t4p_n-6	SAT	0.38
k_grz_p-11	UNSAT	0.39
stmt19_3_214	UNSAT	0.4
k_d4_p-17	UNSAT	0.41
tlc01-uniform-depth-73	UNSAT	0.41
vonNeumann-ripple-carry-8-c	UNSAT	0.42
biu.mv.xl_ao.bb-b001-p010-IPF02-c08.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003	SAT	0.42
k_d4_n-7	SAT	0.42
biu.mv.xl_ao.bb-b001-p010-OPF02-c08.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003	SAT	0.43
k_grz_n-10	SAT	0.43
k_t4p_p-12	UNSAT	0.43
k_path_p-18	UNSAT	0.44
k_poly_n-14	SAT	0.45
k_ph_n-8	SAT	0.45
k_grz_p-12	UNSAT	0.46
fpu-10Xh-error01-uniform-depth-5	UNSAT	0.46
k_path_p-19	UNSAT	0.47
aim-100-6_0-yes1-3-50	SAT	0.48
k_path_n-19	SAT	0.49
k_grz_p-13	UNSAT	0.49
flipflop-7-c	UNSAT	0.5
k_d4_n-8	SAT	0.5
query01_ntrivil_1344	UNSAT	0.51
k_d4_p-20	UNSAT	0.51
incrementer-enc07-nonuniform-depth-17	UNSAT	0.51
tlc04-uniform-depth-36	UNSAT	0.53
k_t4p_n-8	SAT	0.54
k_poly_p-11	UNSAT	0.55
k_path_p-21	UNSAT	0.55
C499.blif_0.10_1.00_0_0_inp_exact	UNSAT	0.55
biu.mv.xl_ao.bb-b001-p010-IPF02-c07.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003	SAT	0.56
k_t4p_p-15	UNSAT	0.56
k_branch_n-4	SAT	0.58
k_t4p_p-16	UNSAT	0.61
k_poly_n-16	SAT	0.61
k_t4p_n-9	SAT	0.63
k_t4p_p-17	UNSAT	0.64
k_d4_n-10	SAT	0.66
toilet_c_10_01.17	UNSAT	0.67
lognBWLARGEB1	UNSAT	0.68
k_poly_n-17	SAT	0.69
k_t4p_p-18	UNSAT	0.7
connect_7x6_4_W	UNSAT	0.71
vonNeumann-ripple-carry-9-c	UNSAT	0.73
k_grz_p-16	UNSAT	0.74
incrementer-enc07-nonuniform-depth-21	UNSAT	0.76
tlc03-uniform-depth-52	UNSAT	0.77
gttt_2_2_0010_3x3_torus_w	UNSAT	0.78
rankfunc5_signed_32	SAT	0.78
fpu-10Xe-correct01-nonuniform-depth-6	UNSAT	0.78
k_t4p_p-20	UNSAT	0.79
k_poly_n-18	SAT	0.81
biu.mv.xl_ao.bb-b001-p010-IPF05-c07.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003	SAT	0.83
k_poly_p-16	UNSAT	0.83
szymanski-5-s	UNSAT	0.84
mutex-128-s	SAT	0.85
k_t4p_n-12	SAT	0.9
k_grz_p-18	UNSAT	0.91
k_poly_p-19	UNSAT	0.91
connect_8x7_7_W	UNSAT	0.94
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	0.96
k_grz_p-17	UNSAT	0.97
k_t4p_n-13	SAT	1.01
k_poly_n-20	SAT	1.01
k_d4_n-14	SAT	1.05
k_poly_n-21	SAT	1.1
k_ph_n-9	SAT	1.12
stmt21_79_304	UNSAT	1.13
k_t4p_n-14	SAT	1.13
C5315.blif_0.10_1.00_0_0_out_exact	UNSAT	1.13
k_grz_n-18	SAT	1.14
k_d4_n-15	SAT	1.14
C5315.blif_0.10_1.00_0_1_inp_exact	SAT	1.16
fpu-10Xh-correct04-uniform-depth-8	UNSAT	1.16
driverlog10_6	UNSAT	1.16
ken.flash^03.C-f3	UNSAT	1.17
stmt27_16_97	UNSAT	1.17
vonNeumann-ripple-carry-10-c	UNSAT	1.2
tlc04-nonuniform-depth-56	UNSAT	1.21
k_grz_p-19	UNSAT	1.21
k_d4_n-16	SAT	1.22
k_t4p_n-15	SAT	1.23
texas.PI_main^16.E-f2	SAT	1.24
k_branch_p-5	UNSAT	1.26
stmt19_217_309	UNSAT	1.26
test1_quant_squaring2	SAT	1.3
C5315.blif_0.10_1.00_0_1_out_exact	SAT	1.32
incrementer-enc02-nonuniform-depth-31	UNSAT	1.37
biu.mv.xl_ao.bb-b001-p005-OPF03-c09.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003	SAT	1.44
C5315.blif_0.10_1.00_0_0_inp_exact	UNSAT	1.47
stmt19_90_266	UNSAT	1.55
flipflop-8-c	UNSAT	1.61
test5_quant_squaring4	SAT	1.63
biu.mv.xl_ao.bb-b001-p005-OPF05-c03.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004	SAT	1.63
biu.mv.xl_ao.bb-b001-p005-OPF05-c02.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004	SAT	1.64
C499.blif_0.10_0.20_0_0_out_exact	UNSAT	1.64
k_d4_n-20	SAT	1.68
rankfunc17_unsigned_16	SAT	1.78
C499.blif_0.10_0.20_0_1_out_exact	UNSAT	1.87
gttt_2_2_00101121_3x3_b	UNSAT	1.9
test3_quant_squaring4	UNSAT	1.93
fpu-10Xh-correct04-uniform-depth-14	UNSAT	2.05
vonNeumann-ripple-carry-11-c	UNSAT	2.08
s386_d2_s	SAT	2.09
k_lin_n-5	SAT	2.11
fpu-10Xh-correct04-uniform-depth-15	UNSAT	2.2
cnt07e	SAT	2.24
fpu-10Xh-correct04-uniform-depth-16	UNSAT	2.35
k_branch_p-6	UNSAT	2.46
fpu-10Xh-correct04-nonuniform-depth-18	UNSAT	2.66
k_ph_n-11	SAT	2.77
k_grz_n-20	SAT	2.83
lut4_AND_fXOR	UNSAT	2.83
C499.blif_0.10_1.00_0_0_out_exact	UNSAT	2.89
C432.blif_0.10_0.20_0_0_inp_exact	UNSAT	2.91
small-synabs-fixpoint-9	UNSAT	2.96
C432.blif_0.10_0.20_0_1_inp_exact	SAT	3.02
adder-10-sat	SAT	3.08
fpu-10Xe-correct01-uniform-depth-22	UNSAT	3.25
emptyroom_e3_ser--opt-20_	SAT	3.44
vonNeumann-ripple-carry-12-c	UNSAT	3.45
fpu-10Xe-correct01-nonuniform-depth-24	UNSAT	3.56
cache-coherence-2-fixpoint-1	UNSAT	3.58
cnt10	SAT	3.59
rankfunc5_unsigned_64	SAT	3.67
k_grz_n-21	SAT	3.7
rankfunc33_signed_32	SAT	3.75
rankfunc13_signed_32	SAT	3.8
c1_BMC_p2_k512	UNSAT	3.85
incrementer-enc03-nonuniform-depth-24	UNSAT	3.91
fpu-10Xh-correct04-nonuniform-depth-27	UNSAT	4.03
k_lin_n-6	SAT	4.07
szymanski-6-s	UNSAT	4.16
texas.two_proc^4.E-f2	SAT	4.27
qshifter_6	SAT	4.3
test4_quant_squaring4	UNSAT	4.39
biu.mv.xl_ao.bb-b001-p010-MIF05-c07.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004	SAT	4.4
dungeon_i10-m5-u10-v0.pddl_planlen=23	UNSAT	4.59
ken.oop^2.C-d3	UNSAT	4.63
ring_r3_ser--opt-8_	SAT	4.69
biu.mv.xl_ao.bb-b001-p010-MIF01-c01.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004	SAT	4.85
incrementer-enc07-uniform-depth-25	UNSAT	5
vonNeumann-ripple-carry-13-c	UNSAT	5.17
flipflop-9-c	UNSAT	5.33
cnt08e	SAT	5.55
p10-10.pddl_planlen=6	UNSAT	5.57
adder-12-sat	SAT	5.69
cnt11	SAT	5.92
c1_BMC_p1_k4	SAT	5.99
small-swap1-fixpoint-3	SAT	6.37
depots03_9	UNSAT	6.41
s713_d2_s	SAT	6.62
s510_d3_s	SAT	6.65
k_branch_p-8	UNSAT	6.76
s09234_PR_8_2	SAT	6.87
k_lin_n-7	SAT	7.03
k_branch_n-8	SAT	7.32
s09234_PR_8_5	SAT	7.34
c1_BMC_p2_k1024	UNSAT	7.5
incrementer-enc08-uniform-depth-33	SAT	7.69
tlc02-uniform-depth-114	UNSAT	8.06
tlc04-nonuniform-depth-98	UNSAT	8.11
toilet_a_08_05.2	UNSAT	8.33
k5_2_3	SAT	8.39
s641_d2_s	SAT	8.44
incrementer-enc06-uniform-depth-24	UNSAT	8.52
stmt19_83_412	UNSAT	8.56
toilet_a_08_01.13	UNSAT	8.57
C499.blif_0.10_0.20_0_1_inp_exact	SAT	8.59
uclid-pipe3a	SAT	8.68
toilet_a_08_05.9	SAT	8.69
s298_d4_s	SAT	8.71
adder-14-sat	SAT	9.06
s05378_PR_9_2	SAT	9.22
small-swap2-fixpoint-4	SAT	9.26
gttt_2_1_0010_4x4_torus_b	UNSAT	9.61
texas.PI_main^05.E-f3	SAT	9.72
C499.blif_0.10_0.20_0_0_inp_exact	UNSAT	9.75
nusmv.reactor^3.C-d4	SAT	9.93
s820_d2_s	SAT	10.5
stmt17_63_82	SAT	10.55
s05378_PR_1_75	UNSAT	11.09
s386_d3_s	SAT	11.68
ken.oop^2.C-d4	UNSAT	11.74
k_lin_n-8	SAT	11.85
lut4_2_f2	UNSAT	11.95
k_branch_n-9	SAT	11.98
dungeon_i25-m12-u3-v0.pddl_planlen=72	UNSAT	12.09
c5_BMC_p1_k32	SAT	12.15
stmt19_64_99	SAT	12.44
vonNeumann-ripple-carry-15-c	UNSAT	12.74
dungeon_i25-m12-u5-v0.pddl_planlen=65	UNSAT	13.15
ken.flash^08.C-d4	UNSAT	13.28
stmt23_66_96	SAT	13.96
stmt28_68_81	SAT	14.55
par8-4-50	UNSAT	14.61
k5_3_2	SAT	15.14
p10-10.pddl_planlen=10	SAT	15.35
stmt23_72_76	SAT	15.37
dungeon_i25-m12-u3-v0.pddl_planlen=130	UNSAT	15.8
flipflop-10-c	UNSAT	15.81
stmt41_160_235	UNSAT	16.67
biu.mv.xl_ao.bb-b001-p010-MIF04-c06.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-005	SAT	16.81
cnt14	SAT	16.83
k_ph_n-14	SAT	17.82
k_lin_n-9	SAT	17.88
dungeon_i25-m12-u3-v0.pddl_planlen=165	UNSAT	18.13
test1_quant_squaring3	SAT	18.2
stmt17_62_98	SAT	18.67
dungeon_i10-m10-u10-v0.pddl_planlen=187	UNSAT	19.26
stmt17_70_98	SAT	19.44
Adder2-8-s	SAT	19.48
stmt17_86_98	SAT	19.5
dungeon_i25-m12-u3-v0.pddl_planlen=190	UNSAT	19.62
stmt17_70_90	SAT	19.68
rankfunc13_unsigned_64	SAT	20.56
rankfunc51_signed_32	SAT	21.1
test5_quant_squaring5	SAT	21.26
rankfunc22_signed_64	SAT	21.75
stmt17_82_98	SAT	21.95
rankfunc14_signed_64	SAT	21.97
dungeon_i10-m5-u10-v0.pddl_planlen=134	UNSAT	22.92
dungeon_i25-m12-u5-v0.pddl_planlen=170	UNSAT	22.96
C880.blif_0.10_1.00_0_1_inp_exact	SAT	24.28
texas.PI_main^08.E-f3	SAT	24.3
lut4_AND_f1	SAT	25.15
k_branch_p-11	UNSAT	25.18
k_branch_n-11	SAT	25.54
s386_d4_s	SAT	27.71
szymanski-8-s	UNSAT	28.81
pipesnotankage14_10	UNSAT	28.93
rankfunc3_signed_64	SAT	29.65
k_branch_n-10	SAT	32.71
s499_d7_s	SAT	33.33
k_lin_n-11	SAT	33.81
C880.blif_0.10_1.00_0_0_inp_exact	UNSAT	34.65
s510_d6_s	SAT	36.6
k_ph_n-16	SAT	36.92
gttt_2_1_000111_3x3_torus_b	SAT	38.5
incrementer-enc02-uniform-depth-58	UNSAT	39.29
k_branch_p-10	UNSAT	40.67
small-seq-fixpoint-3	UNSAT	41.5
query48_query15_1344	UNSAT	42.01
ev-pr-8x8-5-7-0-1-2-lg	UNSAT	42.83
arbiter-07-comp-error01-qbf-hardness-depth-4	UNSAT	43.82
sdlx-fixpoint-3	UNSAT	47.02
s713_d3_s	SAT	49.88
Adder2-10-s	SAT	50.09
k_branch_p-12	UNSAT	50.44
flipflop-11-c	UNSAT	50.99
s499_d9_s	SAT	51.65
stmt52_244_394	UNSAT	52.57
k_branch_n-12	SAT	53.8
s641_d3_s	SAT	55.07
Umbrella_tbm_24.tex.module.000131	SAT	56.93
Umbrella_tbm_24.tex.module.000066	SAT	57.66
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	66.1
jnh212-50	UNSAT	69.71
s499_d12_s	SAT	71.83
pipesnotankage18_8	UNSAT	72.72
pipesnotankage18_7	UNSAT	73.05
s298_d12_s	SAT	73.66
qshifter_7	SAT	74.86
par16-1-50	UNSAT	77.06
s298_d10_s	SAT	77.76
k_lin_n-14	SAT	79.35
small-seq-fixpoint-5	UNSAT	79.45
cnt16r	SAT	80.35
cache-coherence-3-fixpoint-3	UNSAT	83.58
flipflop-12-c	UNSAT	89.31
cache-coherence-2-fixpoint-6	UNSAT	90.69
s713_d4_s	SAT	92.29
stmt29_226_376	UNSAT	96.9
k_lin_n-15	SAT	100.53
tlc02-uniform-depth-241	UNSAT	106.55
k_ph_p-10	UNSAT	111.71
s386_d6_s	SAT	112.47
k_branch_p-14	UNSAT	113.7
s3330_d8_s	FAIL	120
c3_BMC_p1_k256	SAT	120.11
k_branch_p-16	UNSAT	120.33
szymanski-10-s	UNSAT	120.92
s499_d15_s	SAT	132.35
k_branch_n-16	SAT	146.11
s641_d4_s	SAT	149.62
s3330_d9_s	FAIL	150.62
s499_d17_s	SAT	153.64
k_lin_n-17	SAT	165.08
s386_d7_s	SAT	167.36
s386_d8_u	UNSAT	175.05
emptyroom_e3_ser---19_	UNSAT	177.11
s3330_d10_u	FAIL	183.21
Adder2-8-c	UNSAT	185.42
stmt21_319_418	SAT	188.47
gttt_1_1_000111_3x3_torus_w	UNSAT	202.84
s499_d18_s	SAT	203.96
s386_d9_u	UNSAT	220.15
s499_d19_s	SAT	234.88
s386_d10_u	UNSAT	243.84
s510_d11_s	SAT	246.78
gttt_1_1_001020_3x3_w	UNSAT	267.7
s3330_d12_u	FAIL	271.8
s298_d17_s	SAT	284.32
C880.blif_0.10_0.20_0_0_inp_exact	FAIL	286.45
ev-pr-4x4-5-3-0-0-1-s	SAT	304.38
C880.blif_0.10_0.20_0_1_inp_exact	FAIL	307.08
s298_d14_s	SAT	314.04
nusmv.tcas-t^1.B-d2	SAT	316.39
s499_d22_u	UNSAT	320.01
uclid-pipe2	FAIL	333.16
Adder2-16-s	SAT	335.03
Core1108_tbm_21.tex.module.000027	UNSAT	335.91
ev-pr-4x4-15-3-0-0-1-lg	FAIL	343.67
cube_c9_par--opt-11_	SAT	349.47
ev-pr-4x4-5-3-0-0-1-lg	SAT	351.54
szymanski-12-s	UNSAT	353.12
s298_d18_s	SAT	355.16
emptyroom_e4_ser--opt-44_	FAIL	384.61
s386_d11_u	UNSAT	386.17
s499_d24_u	UNSAT	395.7
s3330_d14_u	FAIL	404.64
s386_d12_u	UNSAT	422.27
s298_d19_u	UNSAT	442.91
s820_d3_s	SAT	483.4
s3330_d7_s	FAIL	486.26
s499_d25_u	UNSAT	501.4
AR-fixpoint-5	FAIL	535.61
arbiter-06-comp-error02-qbf-hardness-depth-5	UNSAT	541.1
BLOCKS4ii.7.2	UNSAT	541.33
k_branch_p-21	FAIL	547.99
uclid-pipe3b	FAIL	548.43
arbiter-07-comp-error01-qbf-hardness-depth-11	FAIL	562.43
lut4_2_fXOR	SAT	563.63
k_branch_n-20	FAIL	564.74
gttt_2_1_00011020_4x4_b	FAIL	570.49
gttt_2_1_00102030_4x4_torus_b	FAIL	584.57
arbiter-06-comp-error01-qbf-hardness-depth-12	FAIL	588.99
ev-pr-8x8-11-7-0-1-2-lg	FAIL	589.86
ev-pr-8x8-7-7-0-1-2-lg	FAIL	592.37
emptyroom_e4_par---21_	FAIL	594.11
ev-pr-8x8-9-7-0-1-2-lg	FAIL	596.66
p20-1.pddl_planlen=32	FAIL	599.71
b22_C_2_12	FAIL	599.71
s15850_PR_2_2	FAIL	599.71
f600-50	FAIL	599.71
c4_Debug_s3_f2_e2_v2	FAIL	599.71
p20-1.pddl_planlen=24	FAIL	599.71
toilet_a_10_05.3	FAIL	599.71
c4_Debug_s3_f1_e2_v2	FAIL	599.71
s1269_d5_s	FAIL	599.71
k_ph_p-13	FAIL	599.71
szymanski-18-s	FAIL	599.71
c4_Debug_s3_f1_e1_v2	FAIL	599.71
network_irda_miniport_nscirda_settings.c	FAIL	599.71
szymanski-16-s	FAIL	599.71
hid_hclient_ecdisp.c	FAIL	599.71
C6288.blif_0.10_1.00_0_1_out_exact	FAIL	599.71
szymanski-24-s	FAIL	599.71
s15850_PR_8_50	FAIL	599.71
network_trans_sys_notify.c	FAIL	599.71
input_pnpi8042_moudep.c	FAIL	599.71
qshifter_8	FAIL	599.71
query42_query06_1344n	FAIL	599.72
s713_d11_u	FAIL	599.72
s713_d7_u	FAIL	599.72
s820_d7_s	FAIL	599.72
s1269_d8_s	FAIL	599.72
s1196_d3_u	FAIL	599.72
query21_ntrivil_1344	FAIL	599.72
b20_PR_7_20	FAIL	599.72
k_branch_p-18	FAIL	599.72
connect_8x7_4_R	FAIL	599.72
connect_8x7_6_R	FAIL	599.72
C5315.blif_0.10_0.20_0_0_inp_exact	FAIL	599.72
s820_d11_u	FAIL	599.72
C6288.blif_0.10_1.00_0_0_out_exact	FAIL	599.72
b21_C_3_206	FAIL	599.72
szymanski-20-s	FAIL	599.72
s3330_d2_s	FAIL	599.72
network_irda_miniport_nscirda_comm.c	FAIL	599.72
ev-pr-6x6-7-5-0-1-2-s	FAIL	599.72
kernel_agplib_intrface.c	FAIL	599.72
sortnetsort10.v.stepl.005	FAIL	599.72
s1269_d3_s	FAIL	599.72
BLOCKS4i.6.4	FAIL	599.72
c4_Debug_s3_f1_e2_v3	FAIL	599.72
s3330_d3_s	FAIL	599.72
s641_d10_u	FAIL	599.72
s641_d8_u	FAIL	599.72
s641_d11_u	FAIL	599.72
s641_d5_s	FAIL	599.72
s3330_d4_s	FAIL	599.72
connect_8x7_5_R	FAIL	599.72
s713_d8_u	FAIL	599.72
s713_d10_u	FAIL	599.72
p20-1.pddl_planlen=26	FAIL	599.72
sortnetsort9.v.stepl.007	FAIL	599.72
s1269_d4_s	FAIL	599.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-010	FAIL	599.72
c2_Debug_s3_f1_e1_v2	FAIL	599.72
cube_c11_par---13_	FAIL	599.72
s820_d10_s	FAIL	599.72
c2_Debug_s3_f2_e1_v3	FAIL	599.72
s298_d22_u	FAIL	599.72
s713_d5_s	FAIL	599.72
s820_d14_u	FAIL	599.72
c4_Debug_s5_f2_e2_v1	FAIL	599.72
s298_d25_u	FAIL	599.72
c1_Debug_s3_f1_e1_v1	FAIL	599.72
c1_Debug_s5_f1_e1_v2	FAIL	599.72
ev-pr-6x6-9-5-0-1-2-s	FAIL	599.73
eijk.bs4863.S-d4	FAIL	599.73
s713_d9_u	FAIL	599.73
s1196_d6_u	FAIL	599.73
s713_d6_s	FAIL	599.73
s820_d12_u	FAIL	599.73
s1269_d9_s	FAIL	599.73
query44_query26_1344n	FAIL	599.73
ii32b1-00	FAIL	599.73
C5315.blif_0.10_0.20_0_1_inp_exact	FAIL	599.73
s641_d6_s	FAIL	599.73
k8_2_3	FAIL	599.73
s1196_d5_u	FAIL	599.73
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.74
connect_9x8_6_R	FAIL	599.74
C6288.blif_0.10_0.20_0_1_out_exact	FAIL	599.74
s1269_d10_s	FAIL	599.74
b20_PR_7_90	FAIL	599.74
s510_d23_s	FAIL	599.74
k8_3_2	FAIL	599.74
s820_d15_u	FAIL	599.74
k_ph_n-21	FAIL	599.74
b20_C_3_2	FAIL	599.74
sortnetsort8.v.stepl.007	FAIL	599.75
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	FAIL	599.75
C6288.blif_0.10_0.20_0_0_out_exact	FAIL	599.75
k8_4_3	FAIL	599.75
ev-pr-4x4-15-3-0-0-1-s	FAIL	599.75
Core1108_tbm_03.tex.moduleQ3.2S.000002	FAIL	599.75
ev-pr-6x6-11-5-0-1-2-s	FAIL	599.75
ev-pr-6x6-13-5-0-1-2-lg	FAIL	599.76
ev-pr-6x6-7-5-0-1-2-lg	FAIL	599.76
sortnetsort7.v.stepl.007	FAIL	599.76
filesys_smbmrx_cvsndrcv.c	FAIL	599.76
s510_d24_s	FAIL	599.76
b22_PR_8_20	FAIL	599.76
BLOCKS4iii.6	FAIL	599.77
ev-pr-6x6-11-5-0-1-2-lg	FAIL	599.77
ev-pr-6x6-5-5-0-1-2-s	FAIL	599.77
ev-pr-6x6-13-5-0-1-2-s	FAIL	599.77
s3330_d5_s	FAIL	599.77
ev-pr-8x8-17-7-0-1-2-lg	FAIL	599.78
s1269_d12_u	FAIL	599.78
arbiter-10-comp-error01-qbf-hardness-depth-22	FAIL	599.78
ev-pr-8x8-19-7-0-1-2-lg	FAIL	599.78
test2_quant_squaring2	FAIL	599.78
aim-200-1_6-yes1-4-90	FAIL	599.78
ev-pr-6x6-15-5-0-1-2-s	FAIL	599.78
Core1108_tbm_21.tex.module.000008	FAIL	599.78
s510_d28_s	FAIL	599.79
ev-pr-8x8-15-7-0-1-2-lg	FAIL	599.8
szymanski-14-s	FAIL	599.8
ev-pr-6x6-17-5-0-1-2-s	FAIL	599.8
test2_quant_squaring3	FAIL	599.8
s1269_d13_u	FAIL	599.81
c3_Debug_s3_f2_e2_v2	FAIL	599.81
dungeon_i15-m7-u4-v0.pddl_planlen=81	FAIL	599.81
arbiter-07-comp-error02-qbf-hardness-depth-6	FAIL	599.81
s510_d31_s	FAIL	599.81
C6288.blif_0.10_1.00_0_0_inp_exact	FAIL	599.81
p20-20.pddl_planlen=23	FAIL	599.82
query11_query21_1344	FAIL	599.82
query31_reachqu_1344n	FAIL	599.82
s1196_1_5	FAIL	599.82
s510_d32_s	FAIL	599.82
query03_query25_1344	FAIL	599.82
network_ndis_rtlnwifi_hw_hw_ccmp.c	FAIL	599.82
ev-pr-4x4-11-3-0-0-1-s	FAIL	599.82
s641_d7_u	FAIL	599.82
Umbrella_tbm_25.tex.moduleQ3.2S.000075	FAIL	599.82
k_ph_p-12	FAIL	599.82
C6288.blif_0.10_0.20_0_0_inp_exact	FAIL	599.82
ev-pr-4x4-7-3-0-0-1-s	FAIL	599.82
sortnetsort8.v.stepl.009	FAIL	599.82
k6_2_3	FAIL	599.82
s820_d9_s	FAIL	599.82
k_ph_p-15	FAIL	599.82
Core1108_tbm_02.tex.moduleQ3.2S.000015	FAIL	599.82
adder-12-unsat	FAIL	599.82
s1196_d2_s	FAIL	599.82
s820_d8_s	FAIL	599.82
lut4_2_f1	FAIL	599.82
c5_BMC_p2_k128	FAIL	599.82
c5_BMC_p2_k64	FAIL	599.82
ev-pr-4x4-9-3-0-0-1-s	FAIL	599.82
sortnetsort9.v.stepl.005	FAIL	599.82
s1196_d4_u	FAIL	599.82
lut4_3_fAND	FAIL	599.83
s1196_d7_u	FAIL	599.83
arbiter-08-comp-error02-qbf-hardness-depth-9	FAIL	599.83
arbiter-06-comp-error01-qbf-hardness-depth-15	FAIL	599.83
input_mouser_cseries.c	FAIL	599.83
query51_query50_1344	FAIL	599.83
s1269_d14_u	FAIL	599.83
C6288.blif_0.10_0.20_0_1_inp_exact	FAIL	599.83
query26_query34_1344	FAIL	599.83
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	FAIL	599.83
ev-pr-4x4-13-3-0-0-1-s	FAIL	599.84
C5315.blif_0.10_0.20_0_1_out_exact	FAIL	599.84
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	599.84
biu.mv.xl_ao.bb-b003-p020-IPF03-c03.blif-biu.inv.prop.bb-bmc.with-IOC.unfold-009	FAIL	599.84
arbiter-07-comp-error01-qbf-hardness-depth-20	FAIL	599.84
k8_3_4	FAIL	599.84
gttt_1_1_00101121_4x4_torus_w	FAIL	599.85
ev-pr-4x4-11-3-0-0-1-lg	FAIL	599.85
C5315.blif_0.10_0.20_0_0_out_exact	FAIL	599.85
ev-pr-4x4-9-3-0-0-1-lg	FAIL	599.85
ev-pr-4x4-17-3-0-0-1-s	FAIL	599.86
ev-pr-4x4-13-3-0-0-1-lg	FAIL	599.86
Core1108_tbm_21.tex.module.000030	FAIL	599.87
k_ph_p-19	FAIL	599.87
s510_d36_s	FAIL	599.87
k12_4_2	FAIL	599.87
s1269_d15_u	FAIL	599.88
ev-pr-6x6-5-5-0-1-2-lg	FAIL	599.88
sortnetsort9.AE.stepl.009	FAIL	599.88
ev-pr-6x6-9-5-0-1-2-lg	FAIL	599.88
ev-pr-6x6-15-5-0-1-2-lg	FAIL	599.88
sortnetsort9.AE.stepl.012	FAIL	599.89
Core1108_tbm_21.tex.module.000026	FAIL	599.89
s510_d35_s	FAIL	599.9
k_ph_p-20	FAIL	599.9
ev-pr-4x4-17-3-0-0-1-lg	FAIL	599.9
C6288.blif_0.10_1.00_0_1_inp_exact	FAIL	599.9
ev-pr-4x4-7-3-0-0-1-lg	FAIL	599.92
nusmv.tcas^6.B-f4	FAIL	599.92
ev-pr-6x6-17-5-0-1-2-lg	FAIL	599.92
k_ph_p-18	FAIL	599.92
cube_c7_ser--opt-24_	FAIL	599.93
ev-pr-6x6-19-5-0-1-2-lg	FAIL	599.93
p20-5.pddl_planlen=32	FAIL	599.93
ev-pr-8x8-13-7-0-1-2-lg	FAIL	599.93
arbiter-10-comp-error01-qbf-hardness-depth-10	FAIL	599.95
k14_2_3	FAIL	599.96
sortnetsort8.AE.stepl.003	FAIL	599.97
ev-pr-6x6-19-5-0-1-2-s	FAIL	599.97
Umbrella_tbm_05.tex.module.000039	FAIL	599.98
gttt_2_2_001020_4x4_w	FAIL	599.99
c2_BMC_p1_k2048	FAIL	600
p20-5.pddl_planlen=17	FAIL	600.02
connect_5x4_3_R	FAIL	600.06
nusmv.tcas^3.B-f2	FAIL	604.01
audio_ddksynth_csynth2.cpp	FAIL	635.3
connect_5x4_4_R	FAIL	651.69

QBF Solver Evaluation Portal

QBFEVALs

QBF GALLERIES

DOWNLOADS

qbflib.org

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

QBF Solver Evaluation Portal

QBFEVALs

QBF GALLERIES

DOWNLOADS

qbflib.org

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

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