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