TIME/MEM OUT | SOLVED | WIN | UNIQUE | NOT SOLVED |
Problem | QFUN | CQESTO | QuAbS | GQ | Qute |
---|---|---|---|---|---|
halfadder_match2.sat (2) | 0 s cnf 1 |
0 s cnf 1 |
0 s cnf 1 |
0 s cnf 1 |
0 s cnf 1 |
halfadder_match2.unsat (3) | 0 s cnf 0 |
0 s cnf 0 |
0 s cnf 0 |
0 s cnf 0 |
0 s cnf 0 |
mvs16y.sat (2) | 127 s cnf 1 |
600 | 40 s cnf 1 |
600 | 0 s cnf 1 |
mvs16y.unsat (3) | 0 s cnf 0 |
0 s cnf 0 |
0 s cnf 0 |
0 s cnf 0 |
0 s cnf 0 |
C880.blif_0.10_1.00_0_0_inp_exact (3) | 1 s cnf 0 |
86 s cnf 0 |
600 | 600 | 600 |
C880.blif_0.10_0.20_0_1_inp_exact (19) | 600 | 600 | 600 | 600 | 600 |
test3_quant_squaring2 (3) | 600 | 600 | 600 | 600 | 600 |
mutex-4-s (2) | 0 s cnf 1 |
0 s cnf 1 |
0 s cnf 1 |
600 | 0 s cnf 1 |
C499.blif_0.10_1.00_0_0_out_exact (2) | 0 s cnf 0 |
2 s cnf 0 |
600 | 1 s cnf 0 |
600 |
C499.blif_0.10_0.20_0_1_out_exact (2) | 1 s cnf 0 |
39 s cnf 0 |
600 | 600 | 600 |
C499.blif_0.10_0.20_0_0_out_exact (2) | 1 s cnf 0 |
42 s cnf 0 |
600 | 600 | 600 |
klieber2017q-074-18-eq (2) | 0 s cnf 1 |
4 s cnf 1 |
22 s cnf 1 |
8 s cnf 1 |
600 |
klieber2017q-076-19-t1 (2) | 0 s cnf 0 |
0 s cnf 0 |
38 s cnf 0 |
7 s cnf 0 |
600 |
klieber2017q-076-19-eq (2) | 0 s cnf 1 |
9 s cnf 1 |
39 s cnf 1 |
5 s cnf 1 |
600 |
klieber2017q-078-19-t1 (2) | 0 s cnf 0 |
1 s cnf 0 |
10 s cnf 0 |
29 s cnf 0 |
0 s cnf 0 |
klieber2017q-078-19-eq (2) | 0 s cnf 1 |
2 s cnf 1 |
38 s cnf 1 |
5 s cnf 1 |
600 |
klieber2017q-080-20-t1 (2) | 0 s cnf 0 |
2 s cnf 0 |
13 s cnf 0 |
15 s cnf 0 |
5 s cnf 0 |
klieber2017q-074-18-t1 (2) | 0 s cnf 0 |
1 s cnf 0 |
5 s cnf 0 |
7 s cnf 0 |
197 s cnf 0 |
klieber2017q-080-20-eq (2) | 0 s cnf 1 |
35 s cnf 1 |
17 s cnf 1 |
146 s cnf 1 |
600 |
klieber2017q-084-21-eq (2) | 0 s cnf 1 |
1 s cnf 1 |
31 s cnf 1 |
16 s cnf 1 |
600 |
klieber2017q-084-21-t1 (2) | 0 s cnf 0 |
8 s cnf 0 |
35 s cnf 0 |
101 s cnf 0 |
600 |
klieber2017q-082-20-eq (2) | 0 s cnf 1 |
15 s cnf 1 |
43 s cnf 1 |
26 s cnf 1 |
600 |
klieber2017q-082-20-t1 (2) | 0 s cnf 0 |
1 s cnf 0 |
15 s cnf 0 |
7 s cnf 0 |
0 s cnf 0 |
klieber2017q-088-22-t1 (2) | 0 s cnf 0 |
90 s cnf 0 |
7 s cnf 0 |
24 s cnf 0 |
0 s cnf 0 |
klieber2017q-086-21-eq (2) | 0 s cnf 1 |
2 s cnf 1 |
72 s cnf 1 |
9 s cnf 1 |
600 |
klieber2017q-086-21-t1 (2) | 0 s cnf 0 |
0 s cnf 0 |
36 s cnf 0 |
40 s cnf 0 |
3 s cnf 0 |
klieber2017q-092-23-eq (2) | 1 s cnf 1 |
8 s cnf 1 |
35 s cnf 1 |
40 s cnf 1 |
600 |
klieber2017q-092-23-t1 (2) | 0 s cnf 0 |
1 s cnf 0 |
45 s cnf 0 |
17 s cnf 0 |
64 s cnf 0 |
klieber2017q-088-22-eq (2) | 0 s cnf 1 |
2 s cnf 1 |
42 s cnf 1 |
48 s cnf 1 |
600 |
klieber2017q-100-25-eq (2) | 1 s cnf 1 |
3 s cnf 1 |
85 s cnf 1 |
18 s cnf 1 |
600 |
klieber2017q-096-24-t1 (2) | 0 s cnf 0 |
290 s cnf 0 |
99 s cnf 0 |
22 s cnf 0 |
19 s cnf 0 |
stmt16_950_951 (2) | 0 s cnf 1 |
0 s cnf 1 |
600 | 0 s cnf 1 |
88 s cnf 1 |
klieber2017q-100-25-t1 (2) | 0 s cnf 0 |
1 s cnf 0 |
29 s cnf 0 |
14 s cnf 0 |
600 |
klieber2017q-104-26-eq (2) | 1 s cnf 1 |
600 | 69 s cnf 1 |
39 s cnf 1 |
600 |
klieber2017q-096-24-eq (2) | 1 s cnf 1 |
2 s cnf 1 |
30 s cnf 1 |
44 s cnf 1 |
600 |
klieber2017q-104-26-t1 (2) | 1 s cnf 0 |
2 s cnf 0 |
8 s cnf 0 |
5 s cnf 0 |
198 s cnf 0 |
klieber2017q-108-27-t1 (2) | 0 s cnf 0 |
19 s cnf 0 |
26 s cnf 0 |
6 s cnf 0 |
9 s cnf 0 |
test3_quant_squaring4 (7) | 600 | 600 | 600 | 600 | 600 |
klieber2017q-112-28-eq (2) | 1 s cnf 1 |
2 s cnf 1 |
83 s cnf 1 |
153 s cnf 1 |
600 |
klieber2017q-112-28-t1 (2) | 0 s cnf 0 |
4 s cnf 0 |
60 s cnf 0 |
12 s cnf 0 |
0 s cnf 0 |
klieber2017q-108-27-eq (2) | 1 s cnf 1 |
30 s cnf 1 |
75 s cnf 1 |
600 | 600 |
uclid-pipe2 (4) | 600 | 600 | 600 | 600 | 600 |
uclid-pipe3a (4) | 27 s cnf 1 |
4 s cnf 1 |
600 | 600 | 10 s cnf 1 |
klieber2017q-116-29-t1 (2) | 1 s cnf 0 |
11 s cnf 0 |
97 s cnf 0 |
358 s cnf 0 |
600 |
klieber2017q-116-29-eq (2) | 1 s cnf 1 |
123 s cnf 1 |
219 s cnf 1 |
53 s cnf 1 |
600 |
ci.e#1.a#3.E#40.A#60.c#312.w#2.s#3.asp (2) | 600 | 233 s cnf 1 |
67 s cnf 1 |
600 | 600 |
driver_d9y.sat (2) | 281 s cnf 1 |
600 | 600 | 600 | 600 |
driver_d9y.unsat (3) | 0 s cnf 0 |
20 s cnf 0 |
0 s cnf 0 |
0 s cnf 0 |
0 s cnf 0 |
stmt41_738_749 (2) | 0 s cnf 1 |
0 s cnf 1 |
600 | 0 s cnf 1 |
600 |
ci.e#1.a#3.E#40.A#60.c#376.w#2.s#4.asp (2) | 600 | 600 600 | 600 | 600 | 600 |
ci.e#1.a#3.E#40.A#60.c#400.w#2.s#1.asp (2) | 600 | 600 | 24 s cnf 0 |
600 | 12 s cnf 0 |
stmt41_160_235 (2) | 600 | 600 | 600 | 600 | 600 |
ci.e#1.a#3.E#40.A#60.c#416.w#2.s#3.asp (2) | 600 | 600 | 183 s cnf 0 |
600 | 19 s cnf 0 |
ci.e#1.a#3.E#40.A#60.c#424.w#2.s#1.asp (2) | 600 | 600 | 0 s cnf 0 |
600 | 15 s cnf 0 |
ci.e#1.a#3.E#40.A#60.c#432.w#2.s#8.asp (2) | 600 | 600 | 0 s cnf 0 |
600 | 0 s cnf 0 |
ci.e#1.a#3.E#40.A#60.c#264.w#4.s#2.asp (2) | 600 | 2 s cnf 1 |
4 s cnf 1 |
32 s cnf 1 |
0 s cnf 1 |
ci.e#1.a#3.E#40.A#60.c#288.w#4.s#8.asp (2) | 600 | 127 s cnf 1 |
19 s cnf 1 |
600 | 600 |
Umbrella_tbm_05.tex.module.000039 (3) | 600 | 392 s cnf 1 |
600 | 600 | 600 |
ci.e#1.a#3.E#40.A#60.c#200.w#6.s#6.asp (2) | 20 s cnf 1 |
1 s cnf 1 |
0 s cnf 1 |
2 s cnf 1 |
1 s cnf 1 |
amba2f9n.sat (2) | 600 | 600 | 600 | 600 | 600 |
amba2f9n.unsat (3) | 11 s cnf 0 |
600 | 263 s cnf 0 |
23 s cnf 0 |
600 |
ci.e#1.a#3.E#40.A#60.c#304.w#4.s#7.asp (2) | 600 | 600 | 85 s cnf 1 |
600 | 600 |
ci.e#1.a#3.E#40.A#60.c#208.w#6.s#8.asp (2) | 418 s cnf 1 |
1 s cnf 1 |
1 s cnf 1 |
5 s cnf 1 |
4 s cnf 1 |
ci.e#1.a#3.E#40.A#60.c#320.w#4.s#8.asp (2) | 600 | 385 s cnf 1 |
38 s cnf 1 |
600 | 600 |
ci.e#1.a#3.E#40.A#60.c#336.w#4.s#5.asp (2) | 600 | 600 | 600 | 600 | 600 |
test1_quant_squaring3 (5) | 600 | 600 | 600 | 600 | 600 |
szymanski-5-s (3) | 0 s cnf 0 |
0 s cnf 0 |
0 s cnf 0 |
600 | 0 s cnf 0 |
ci.e#1.a#3.E#40.A#60.c#344.w#4.s#5.asp (2) | 600 | 600 | 600 | 600 | 600 |
C5315.blif_0.10_0.20_0_0_out_exact (2) | 600 | 600 | 600 | 600 | 600 |
k5_2_3 (3) | 449 s cnf 1 |
600 | 600 | 600 | 600 |
k_ph_p-12 (4) | 18 s cnf 0 |
600 | 600 | 600 | 600 |
rankfunc17_unsigned_16 (2) | 600 | 600 | 600 | 600 | 600 |
small-swap1-fixpoint-3 (2) | 600 | 600 | 600 | 600 | 600 |
ci.e#1.a#3.E#40.A#60.c#408.w#4.s#3.asp (2) | 600 | 600 | 600 | 600 | 600 |
C6288.blif_0.10_1.00_0_0_out_exact (2) | 600 | 600 | 600 | 600 | 600 |
ci.e#1.a#3.E#40.A#60.c#280.w#6.s#7.asp (2) | 600 | 88 s cnf 1 |
97 s cnf 1 |
423 s cnf 1 |
600 |
ltl2dba_C2-6_comp3_REAL.unsat (3) | 0 s cnf 0 |
1 s cnf 0 |
156 s cnf 0 |
0 s cnf 0 |
33 s cnf 0 |
ltl2dba_C2-6_comp3_REAL.sat (2) | 600 | 600 | 600 | 600 | 600 |
ci.e#1.a#3.E#40.A#60.c#296.w#6.s#7.asp (2) | 600 | 456 s cnf 1 |
29 s cnf 1 |
600 | 600 |
ci.e#1.a#3.E#40.A#60.c#304.w#6.s#8.asp (2) | 600 | 600 | 60 s cnf 1 |
600 | 600 |
C6288.blif_0.10_0.20_0_0_out_exact (2) | 600 | 600 | 600 | 600 | 600 |
sortnetsort9.v.stepl.005 (3) | 143 s cnf 0 |
600 | 600 | 600 | 600 |
arbiter-08-comp-error02-qbf-hardness-depth-9 (20) | 600 | 8 s cnf 1 |
7 s cnf 1 |
600 | 600 |
C6288.blif_0.10_0.20_0_1_out_exact (2) | 600 | 600 | 600 | 600 | 600 |
C6288.blif_0.10_0.20_0_0_inp_exact (13) | 600 | 600 | 600 | 600 | 600 |
small-swap2-fixpoint-4 (2) | 600 | 600 | 600 | 600 | 600 |
ci.e#1.a#3.E#40.A#60.c#384.w#6.s#8.asp (2) | 600 | 600 | 600 | 600 | 600 |
ci.e#1.a#3.E#40.A#60.c#392.w#6.s#4.asp (2) | 600 | 600 | 600 | 600 | 600 |
rankfunc5_unsigned_64 (2) | 600 | 600 | 600 | 600 | 600 |
JP-unsat-02-07-2 (2) | 3 s cnf 0 |
1 s cnf 0 |
1 s cnf 0 |
3 s cnf 0 |
10 s cnf 0 |
rankfunc33_signed_32 (2) | 600 | 600 | 600 | 600 | 600 |
sortnetsort10.v.stepl.005 (3) | 600 | 600 | 600 | 600 | 600 |
sdlx-fixpoint-3 (2) | 600 | 600 | 600 | 600 | 600 |
rankfunc14_signed_64 (2) | 600 | 600 | 600 | 600 | 600 |
small-synabs-fixpoint-9 (2) | 600 | 600 | 600 | 600 | 600 |
sortnetsort9.v.stepl.007 (3) | 30 s cnf 1 |
600 | 600 | 600 | 600 |
cnt14 (29) | 600 | 600 | 600 | 600 | 43 s cnf 1 |
adder-10-sat (4) | 600 | 600 | 600 | 600 | 600 |
genbuf9b4n.sat (2) | 600 | 600 | 600 | 600 | 600 |
genbuf9b4n.unsat (3) | 148 s cnf 0 |
600 | 600 | 224 s cnf 0 |
600 |
szymanski-6-s (3) | 1 s cnf 0 |
2 s cnf 0 |
1 s cnf 0 |
600 | 0 s cnf 0 |
genbuf10b4n.sat (2) | 600 | 600 | 600 | 600 | 600 |
genbuf10b4n.unsat (3) | 242 s cnf 0 |
600 | 600 | 319 s cnf 0 |
600 |
mutex-32-s (2) | 0 s cnf 1 |
0 s cnf 1 |
1 s cnf 1 |
600 | 0 s cnf 1 |
CHAIN20v.21 (3) | 0 s cnf 1 |
0 s cnf 1 |
600 | 600 | 0 s cnf 1 |
rankfunc13_unsigned_64 (2) | 600 | 600 | 600 | 600 | 600 |
Core1108_tbm_02.tex.moduleQ3.2S.000015 (3) | 600 | 4 s cnf 0 |
0 s cnf 0 |
600 | 133 s cnf 0 |
JP-unsat-02-06-3 (2) | 17 s cnf 0 |
2 s cnf 0 |
2 s cnf 0 |
11 s cnf 0 |
600 |
k_branch_n-10 (24) | 600 | 600 | 100 s cnf 1 |
600 | 600 |
k_branch_p-10 (24) | 600 | 600 | 2 s cnf 0 |
600 | 600 |
ken.oop^2.C-d4 (2) | 600 | 600 | 600 | 600 | 600 |
SR-unsat-03-01-07-1 (2) | 1 s cnf 0 |
0 s cnf 0 |
0 s cnf 0 |
3 s cnf 0 |
3 s cnf 0 |
cnt16r (33) | 600 | 600 | 600 | 600 | 600 |
driver_a9n.sat (2) | 600 | 600 | 600 | 600 | 600 |
driver_a9n.unsat (3) | 9 s cnf 0 |
600 | 600 | 22 s cnf 0 |
600 |
k8_2_3 (3) | 600 | 600 | 600 | 600 | 600 |
cycle_sched_6_7_1.sat (2) | 600 | 600 | 600 | 600 | 600 |
cycle_sched_6_7_1.unsat (3) | 600 | 600 | 600 | 600 | 600 |
ltl2dpa_C26_comp2_REAL.sat (2) | 600 | 600 | 600 | 600 | 600 |
ltl2dpa_C26_comp2_REAL.unsat (3) | 0 s cnf 0 |
600 | 600 | 1 s cnf 0 |
600 |
k_branch_p-11 (26) | 600 | 600 | 20 s cnf 0 |
600 | 600 |
amba4b9y.sat (2) | 600 | 600 | 600 | 600 | 600 |
amba4b9y.unsat (3) | 600 | 600 | 600 | 600 | 600 |
CHAIN22v.23 (3) | 0 s cnf 1 |
0 s cnf 1 |
600 | 600 | 0 s cnf 1 |
adder-12-unsat (3) | 600 | 600 | 600 | 600 | 600 |
stmt17_63_82 (2) | 29 s cnf 1 |
21 s cnf 1 |
600 | 413 s cnf 1 |
600 |
test2_quant_squaring2 (3) | 600 | 600 | 600 | 600 | 600 |
CHAIN23v.24 (3) | 0 s cnf 1 |
0 s cnf 1 |
600 | 600 | 0 s cnf 1 |
stmt28_68_81 (2) | 30 s cnf 1 |
23 s cnf 1 |
600 | 174 s cnf 1 |
600 |
stay24n.sat (2) | 599 s cnf 1 |
600 | 600 | 600 | 14 s cnf 1 |
stay24n.unsat (3) | 0 s cnf 0 |
0 s cnf 0 |
0 s cnf 0 |
1 s cnf 0 |
0 s cnf 0 |
BLOCKS4iii.6 (3) | 0 s cnf 0 |
6 s cnf 0 |
600 | 1 s cnf 0 |
1 s cnf 0 |
k_branch_n-12 (28) | 600 | 600 | 600 | 600 | 600 |
incrementer-enc07-uniform-depth-25 (3) | 0 s cnf 0 |
7 s cnf 0 |
600 | 7 s cnf 0 |
600 |
ev-pr-4x4-11-3-0-0-1-lg (11) | 600 | 406 s cnf 1 |
305 s cnf 1 |
247 s cnf 1 |
1 s cnf 1 |
k_ph_p-19 (5) | 600 | 600 | 600 | 600 | 600 |
stmt19_64_99 (2) | 33 s cnf 1 |
32 s cnf 1 |
600 | 465 s cnf 1 |
600 |
stmt17_70_90 (2) | 42 s cnf 1 |
30 s cnf 1 |
600 | 336 s cnf 1 |
600 |
p20-1.pddl_planlen=24 (3) | 74 s cnf 0 |
600 | 600 | 600 | 600 |
incrementer-enc08-uniform-depth-33 (3) | 0 s cnf 1 |
10 s cnf 1 |
600 | 3 s cnf 1 |
600 |
consistency_0_1 (143) | 600 | 3 s cnf 1 |
600 | 600 | 0 s cnf 1 |
possibility10_0_1 (144) | 600 | 51 s cnf 0 |
600 | 29 s cnf 0 |
1 s cnf 0 |
assertion12_0_1 (144) | 0 s cnf 0 |
1 s cnf 0 |
7 s cnf 0 |
1 s cnf 0 |
0 s cnf 0 |
b20_PR_7_20 (3) | 2 s cnf 1 |
600 | 600 | 50 s cnf 1 |
0 s cnf 1 |
possibility8_0_1 (143) | 600 | 13 s cnf 1 |
600 | 600 | 1 s cnf 1 |
possibility5_0_1 (147) | 600 | 10 s cnf 0 |
600 | 25 s cnf 0 |
8 s cnf 0 |
adder-14-sat (4) | 600 | 600 | 600 | 600 | 600 |
f600-50 (2) | 600 | 600 | 600 | 600 | 600 |
ev-pr-4x4-13-3-0-0-1-lg (13) | 96 s cnf 1 |
3 s cnf 1 |
600 | 475 s cnf 1 |
1 s cnf 1 |
ken.flash^08.C-d4 (2) | 154 s cnf 0 |
600 | 498 s cnf 0 |
600 | 600 |
k_ph_n-21 (5) | 282 s cnf 1 |
24 s cnf 1 |
4 s cnf 1 |
600 | 0 s cnf 1 |
test2_quant_squaring3 (5) | 600 | 600 | 600 | 600 | 600 |
mutex-64-s (2) | 0 s cnf 1 |
0 s cnf 1 |
2 s cnf 1 |
600 | 1 s cnf 1 |
stmt17_86_98 (2) | 66 s cnf 1 |
39 s cnf 1 |
600 | 311 s cnf 1 |
600 |
network_ndis_rtlnwifi_hw_hw_ccmp.c (3) | 600 | 600 | 600 | 600 | 600 |
mult_bool_matrix_10_9_11.sat (2) | 600 | 600 | 600 | 600 | 600 |
mult_bool_matrix_10_9_11.unsat (3) | 600 | 600 | 600 | 600 | 600 |
cube_c7_ser--opt-24_ (3) | 7 s cnf 1 |
600 | 600 | 203 s cnf 1 |
600 |
k_branch_p-16 (36) | 600 | 600 | 231 s cnf 0 |
600 | 600 |
szymanski-8-s (3) | 6 s cnf 0 |
12 s cnf 0 |
3 s cnf 0 |
600 | 0 s cnf 0 |
sortnetsort9.AE.stepl.012 (2) | 2 s cnf 0 |
5 s cnf 0 |
158 s cnf 0 |
600 | 600 |
b22_PR_8_20 (3) | 10 s cnf 1 |
600 | 600 | 50 s cnf 1 |
600 |
s15850_PR_8_50 (3) | 600 | 600 | 600 | 600 | 600 |
incrementer-enc02-uniform-depth-58 (3) | 0 s cnf 0 |
33 s cnf 0 |
600 | 158 s cnf 0 |
600 |
audio_ddksynth_csynth2.cpp (3) | 600 | 600 | 600 | 600 | 600 |
ev-pr-6x6-9-5-0-1-2-lg (9) | 600 | 536 s cnf 0 |
259 s cnf 0 |
507 s cnf 0 |
600 |
SR-unsat-04-01-08-1 (2) | 39 s cnf 0 |
8 s cnf 0 |
7 s cnf 0 |
30 s cnf 0 |
600 |
arbiter-10-comp-error01-qbf-hardness-depth-22 (46) | 600 | 600 | 600 | 600 | 25 s cnf 0 |
query44_query26_1344n (2) | 600 | 600 | 600 | 600 | 600 |
cache-coherence-2-fixpoint-6 (2) | 600 | 600 | 600 | 600 | 600 |
consistency_0_2 (307) | 600 | 13 s cnf 1 |
600 | 1 | 1 s cnf 1 |
possibility10_0_2 (310) | 600 | 600 | 600 | 1 | 600 |
assertion12_0_2 (314) | 600 | 600 | 600 | 1 | 600 |
ev-pr-6x6-11-5-0-1-2-lg (11) | 600 | 600 | 600 | 600 | 600 |
emptyroom_e4_ser--opt-44_ (3) | 296 s cnf 1 |
600 | 600 | 600 | 600 |
load_3c_comp_comp7_REAL.sat (2) | 600 | 600 | 600 | 600 | 600 |
load_3c_comp_comp7_REAL.unsat (3) | 2 s cnf 0 |
600 | 600 | 28 s cnf 0 |
600 |
ev-pr-8x8-7-7-0-1-2-lg (7) | 19 s cnf 0 |
105 s cnf 0 |
24 s cnf 0 |
600 | 132 s cnf 0 |
CM-unsat-07-01-06-2 (2) | 600 | 198 s cnf 0 |
162 s cnf 0 |
600 | 600 |
s1269_d12_u (2) | 600 | 600 | 600 | 600 | 600 |
cycle_sched_4_7_1.sat (2) | 600 | 600 | 600 | 600 | 600 |
cycle_sched_4_7_1.unsat (3) | 417 s cnf 0 |
600 | 600 | 600 | 600 |
s1269_d13_u (2) | 600 | 600 | 600 | 600 | 600 |
ev-pr-6x6-17-5-0-1-2-lg (17) | 600 | 600 | 600 | 600 | 600 |
possibility1_0_3 (481) | 600 | 600 | 600 | 1 | 600 |
consistency_0_3 (481) | 600 | 33 s cnf 1 |
600 | 1 | 2 s cnf 1 |
possibility7_0_3 (481) | 600 | 600 | 600 | 1 | 67 s cnf 1 |
possibility6_0_3 (481) | 600 | 600 | 600 | 1 | 3 s cnf 0 |
possibility3_0_3 (481) | 600 | 600 | 600 | 1 | 600 |
assertion9_0_3 (492) | 600 | 600 | 600 | 1 | 600 |
assertion6_0_3 (481) | 600 | 600 | 600 | 1 | 1 s cnf 0 |
k12_4_2 (3) | 600 | 600 | 600 | 600 | 600 |
assertion2_0_3 (492) | 600 | 600 | 600 | 1 | 600 |
assertion7_0_3 (481) | 600 | 600 | 600 | 1 | 7 s cnf 0 |
s1269_d15_u (2) | 600 | 600 | 600 | 600 | 600 |
b21_C_3_206 (3) | 4 s cnf 1 |
600 | 600 | 600 | 600 |
Adder2-16-s (6) | 600 | 600 | 600 | 600 | 600 |
ev-pr-6x6-19-5-0-1-2-lg (19) | 600 | 600 | 600 | 600 | 600 |
qshifter_7 (2) | 600 | 600 | 600 | 600 | 600 |
ev-pr-4x4-7-3-0-0-1-s (7) | 600 | 600 | 600 | 600 | 600 |
DW-unsat-08-21-1 (2) | 73 s cnf 0 |
20 s cnf 0 |
33 s cnf 0 |
79 s cnf 0 |
131 s cnf 0 |
load_full_4_comp3_REAL.sat (2) | 600 | 600 | 600 | 600 | 600 |
load_full_4_comp3_REAL.unsat (3) | 64 s cnf 0 |
600 | 600 | 600 | 600 |
DW-sat-08-22-1 (2) | 82 s cnf 1 |
3 s cnf 1 |
3 s cnf 1 |
67 s cnf 1 |
600 |
consistency_0_4 (669) | 600 | 68 s cnf 1 |
600 | 1 | 4 s cnf 1 |
input_pnpi8042_moudep.c (3) | 600 | 600 | 600 | 600 | 600 |
assertion1_0_4 (676) | 600 | 600 | 600 | 2 | 5 s cnf 1 |
possibility5_0_4 (685) | 600 | 600 | 600 | 2 | 600 |
assertion7_0_4 (669) | 600 | 600 | 600 | 2 | 600 |
ev-pr-8x8-13-7-0-1-2-lg (13) | 600 | 600 | 600 | 600 | 600 |
DW-sat-08-23-1 (2) | 85 s cnf 1 |
6 s cnf 1 |
2 s cnf 1 |
81 s cnf 1 |
600 |
DW-unsat-09-22-1 (2) | 189 s cnf 0 |
50 s cnf 0 |
78 s cnf 0 |
153 s cnf 0 |
600 |
network_irda_miniport_nscirda_comm.c (3) | 600 | 600 | 600 | 600 | 600 |
s3330_d9_s (2) | 600 | 600 | 600 | 600 | 600 |
DW-sat-08-24-1 (2) | 92 s cnf 1 |
13 s cnf 1 |
12 s cnf 1 |
53 s cnf 1 |
316 s cnf 1 |
k14_2_3 (3) | 600 | 600 | 600 | 600 | 600 |
DW-unsat-09-23-1 (2) | 202 s cnf 0 |
51 s cnf 0 |
76 s cnf 0 |
201 s cnf 0 |
226 s cnf 0 |
JP-unsat-03-07-4 (2) | 600 | 176 s cnf 0 |
141 s cnf 0 |
600 | 600 |
ev-pr-8x8-15-7-0-1-2-lg (15) | 600 | 600 | 600 | 600 | 600 |
c5_BMC_p2_k64 (3) | 600 | 600 | 600 | 600 | 600 |
query42_query06_1344n (2) | 600 | 600 | 600 | 600 | 600 |
filesys_smbmrx_cvsndrcv.c (3) | 0 s cnf 0 |
4 s cnf 0 |
600 | 600 | 600 |
CM-unsat-07-01-05-3 (2) | 600 | 600 | 600 | 600 | 600 |
consistency_0_5 (871) | 600 | 122 s cnf 1 |
600 | 2 | 8 s cnf 1 |
possibility4_0_5 (871) | 600 | 600 | 600 | 2 | 600 |
assertion2_0_5 (890) | 600 | 600 | 600 | 2 | 600 |
mult_bool_matrix_17_17_17.unsat (3) | 600 | 600 | 600 | 600 | 600 |
mult_bool_matrix_17_17_17.sat (2) | 600 | 600 | 600 | 600 | 600 |
ev-pr-8x8-19-7-0-1-2-lg (19) | 600 | 600 | 600 | 600 | 600 |
dungeon_i15-m7-u4-v0.pddl_planlen=81 (3) | 151 s cnf 0 |
600 | 600 | 600 | 600 |
beemldelec4b1_c0to127.unsat (3) | 0 s cnf 0 |
67 s cnf 0 |
1 s cnf 0 |
7 s cnf 0 |
2 s cnf 0 |
beemldelec4b1_c0to127.sat (2) | 600 | 600 | 600 | 600 | 600 |
s3330_d12_u (2) | 600 | 600 | 600 | 600 | 600 |
JP-sat-03-09-4 (2) | 600 | 600 | 600 | 600 | 600 |
CM-sat-07-01-06-3 (2) | 164 s cnf 1 |
56 s cnf 1 |
145 s cnf 1 |
115 s cnf 1 |
600 |
DWs-sat-10-23-1 (2) | 365 s cnf 1 |
4 s cnf 1 |
4 s cnf 1 |
315 s cnf 1 |
600 |
consistency_0_6 (1087) | 600 | 118 | 214 | 2 | 14 s cnf 1 |
CM-unsat-08-01-05-3 (2) | 600 | 600 | 600 | 600 | 600 |
possibility7_0_6 (1087) | 600 | 123 | 218 | 3 | 600 |
possibility3_0_6 (1087) | 600 | 123 | 203 | 3 | 600 |
assertion10_0_6 (1098) | 600 | 121 | 218 | 3 | 600 |
assertion3_0_6 (1087) | 600 | 122 | 205 | 3 | 600 |
assertion2_0_6 (1110) | 600 | 116 | 222 | 2 | 600 |
oski3ub5i_c0to255.unsat (3) | 0 s cnf 0 |
2 s cnf 0 |
6 s cnf 0 |
12 s cnf 0 |
2 s cnf 0 |
oski3ub5i_c0to255.sat (2) | 600 | 600 | 600 | 600 | 600 |
DWs-sat-10-24-1 (2) | 78 s cnf 1 |
4 s cnf 1 |
108 s cnf 1 |
182 s cnf 1 |
600 |
ev-pr-4x4-13-3-0-0-1-s (13) | 600 | 600 | 600 | 600 | 600 |
DWs-unsat-11-23-1 (2) | 600 | 315 s cnf 0 |
118 s cnf 0 |
431 s cnf 0 |
600 |
szymanski-14-s (3) | 553 s cnf 0 |
598 s cnf 0 |
94 s cnf 0 |
600 | 12 s cnf 0 |
DWs-sat-10-25-1 (2) | 257 s cnf 1 |
4 s cnf 1 |
6 s cnf 1 |
72 s cnf 1 |
415 s cnf 1 |
ring_r6_ser--opt-17_ (3) | 600 | 600 | 600 | 600 | 600 |
c5_BMC_p2_k128 (3) | 600 | 600 | 600 | 600 | 600 |
connect_8x7_6_R (57) | 600 | 600 | 600 | 600 | 600 |
DWs-unsat-11-24-1 (2) | 600 | 219 s cnf 0 |
187 s cnf 0 |
600 | 600 |
CM-sat-07-01-07-3 (2) | 600 | 38 s cnf 1 |
42 s cnf 1 |
555 s cnf 1 |
600 |
ev-pr-4x4-15-3-0-0-1-s (15) | 600 | 600 | 600 | 600 | 600 |
assertion11_0_7 (1317) | 600 | 9 | 305 | 3 | 600 |
possibility10_0_7 (1330) | 600 | 9 | 287 | 3 | 600 |
consistency_0_7 (1317) | 600 | 9 | 304 | 3 | 24 s cnf 1 |
possibility11_0_7 (1317) | 600 | 9 | 285 | 3 | 600 |
possibility4_0_7 (1317) | 600 | 9 | 304 | 3 | 600 |
assertion9_0_7 (1344) | 600 | 9 | 294 | 3 | 600 |
possibility6_0_7 (1317) | 600 | 9 | 301 | 3 | 36 s cnf 0 |
possibility8_0_7 (1317) | 600 | 9 | 201 | 3 | 600 |
DWs-unsat-12-25-1 (2) | 600 | 445 s cnf 0 |
262 268 | 600 | 600 |
ev-pr-4x4-17-3-0-0-1-s (17) | 600 | 600 | 600 | 600 | 600 |
consistency_0_8 (1561) | 600 | 9 | 262 | 4 | 34 s cnf 1 |
possibility1_0_8 (1561) | 600 | 9 | 275 | 4 | 600 |
assertion2_0_8 (1592) | 600 | 9 | 267 | 4 | 600 |
CM-unsat-17-01-06-2 (2) | 600 | 600 | 600 | 600 | 600 |
b20_C_3_2 (3) | 71 s cnf 1 |
600 | 600 | 600 | 600 |
szymanski-16-s (3) | 600 | 600 | 202 s cnf 0 |
600 | 24 s cnf 0 |
JP-sat-03-08-5 (2) | 600 | 600 | 600 | 600 | 600 |
qshifter_8 (2) | 600 | 600 | 600 | 600 | 600 |
consistency_0_9 (1819) | 600 | 9 | 228 | 4 | 52 s cnf 1 |
assertion10_0_9 (1836) | 600 | 9 | 239 | 4 | 600 |
assertion5_0_9 (1854) | 600 | 9 | 232 | 4 | 600 |
connect_9x8_6_R (73) | 600 | 600 | 600 | 600 | 600 |
assertion1_0_9 (1836) | 600 | 9 | 238 | 4 | 62 s cnf 1 |
possibility5_0_9 (1855) | 600 | 9 | 231 | 5 | 600 |
JP-sat-03-09-5 (2) | 600 | 600 | 600 | 600 | 600 |
SR-sat-03-01-08-2 (2) | 600 | 38 s cnf 1 |
94 s cnf 1 |
600 | 600 |
p20-5.pddl_planlen=32 (3) | 600 | 600 | 600 | 600 | 600 |
consistency_0_10 (2091) | 600 | 9 | 313 | 6 | 72 s cnf 1 |
possibility6_0_10 (2091) | 600 | 10 | 306 | 5 | 97 s cnf 0 |
assertion1_0_10 (2110) | 600 | 10 | 318 | 6 | 86 s cnf 1 |
assertion4_0_10 (2130) | 600 | 10 | 309 | 5 | 600 |
CM-sat-07-01-06-4 (2) | 219 s cnf 1 |
600 | 54 s cnf 1 |
600 | 600 |
fpu-10Xe-correct01-nonuniform-depth-24 (43) | 16 s cnf 0 |
600 | 14 s cnf 0 |
35 s cnf 0 |
8 s cnf 0 |
DW-unsat-19-42-1 (2) | 600 | 600 | 600 | 600 | 600 |
fpu-10Xh-correct04-nonuniform-depth-27 (49) | 22 s cnf 0 |
600 | 19 s cnf 0 |
41 s cnf 0 |
9 s cnf 0 |
CM-unsat-17-01-05-3 (2) | 600 | 600 | 600 | 600 | 600 |
DW-unsat-19-43-1 (2) | 600 | 600 | 600 | 600 | 600 |
ev-pr-6x6-9-5-0-1-2-s (9) | 600 | 600 | 600 | 600 | 600 |
DW-sat-19-44-1 (2) | 600 | 600 | 78 s cnf 1 |
600 | 600 |
DW-sat-19-45-1 (2) | 600 | 600 | 72 s cnf 1 |
600 | 600 |
DW-unsat-20-44-1 (2) | 600 | 600 | 600 | 600 | 600 |
CM-unsat-18-01-05-3 (2) | 600 | 600 | 600 | 600 | 600 |
DW-sat-19-46-1 (2) | 600 | 600 | 87 s cnf 1 |
600 | 600 |
CM-sat-17-01-06-3 (2) | 600 | 600 | 110 s cnf 1 |
600 | 600 |
ev-pr-6x6-11-5-0-1-2-s (11) | 600 | 600 | 600 | 600 | 600 |
c1_Debug_s5_f1_e1_v2 (5) | 600 | 600 | 600 | 600 | 600 |
c2_Debug_s3_f1_e1_v2 (3) | 600 | 600 | 600 | 600 | 600 |
CM-sat-17-01-07-3 (2) | 600 | 600 | 600 | 600 | 600 |
ev-pr-6x6-13-5-0-1-2-s (13) | 600 | 600 | 600 | 600 | 600 |
c4_Debug_s3_f2_e2_v2 (3) | 600 | 600 | 600 | 600 | 600 |
c4_Debug_s5_f2_e2_v1 (5) | 600 | 600 | 600 | 600 | 600 |
c2_BMC_p1_k2048 (3) | 28 s cnf 1 |
600 | 600 | 600 | 600 |
ev-pr-6x6-17-5-0-1-2-s (17) | 600 | 600 | 600 | 600 | 600 |
SR-unsat-04-01-07-2 (2) | 600 | 600 | 600 | 600 | 600 |
SR-sat-04-01-08-2 (2) | 600 | 600 | 600 | 600 | 600 |
dungeon_i25-m12-u3-v0.pddl_planlen=165 (3) | 600 | 600 | 600 | 600 | 600 |
dungeon_i25-m12-u3-v0.pddl_planlen=190 (3) | 600 | 600 | 600 | 600 | 600 |
CM-sat-17-01-06-4 (2) | 600 | 600 | 600 | 600 | 600 |
vonNeumann-ripple-carry-12-c (3) | 105 s cnf 0 |
17 s cnf 0 |
479 s cnf 0 |
78 s cnf 0 |
25 s cnf 0 |
pipesnotankage14_10 (7) | 131 s cnf 0 |
600 | 600 | 600 | 600 |
p20-20.pddl_planlen=23 (3) | 202 s cnf 1 |
600 | 600 | 600 | 300 s cnf 1 |
SR-sat-03-01-07-3 (2) | 600 | 600 | 600 | 600 | 600 |
pipesnotankage18_8 (7) | 309 s cnf 0 |
600 | 600 | 600 | 600 |
c3_Debug_s3_f2_e2_v2 (3) | 600 | 600 | 600 | 600 | 600 |
TOTAL (320) | solved:118 wins:84 |
solved:112 wins:39 |
solved:103 wins:41 |
solved:87 wins:7 |
solved:83 wins:56 |
QFUN | CQESTO | QuAbS | GQ | Qute |