| TIME/MEM OUT | SOLVED | WIN |
| Problem | qfun-64 | qfun-128 | qfun-16 | rareqs | qfun-64-f | quabs | ghostq |
|---|---|---|---|---|---|---|---|
| halfadder_match2.sat | 0 (0+0) s cnf 1 |
0 (0+0) s cnf 1 |
0 (0+0) s cnf 1 |
0 (0+0) s cnf 1 |
0 (0+0) s cnf 1 |
0 (0+0) s cnf 1 |
0 (0+0) s cnf 1 |
| halfadder_match2.unsat | 0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
| mvs16y.sat | 204 (204+0) s cnf 1 |
276 (276+0) s cnf 1 |
0 (0+0) s cnf 1 |
800 (800+0) | 584 (584+0) s cnf 1 |
63 (63+0) s cnf 1 |
800 (800+0) |
| mvs16y.unsat | 0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
| C880.blif_0.10_1.00_0_0_inp_exact | 3 (3+0) s cnf 0 |
3 (3+0) s cnf 0 |
4 (4+0) s cnf 0 |
3 (3+0) s cnf 0 |
3 (3+0) s cnf 0 |
800 (798+2) | 800 (800+0) |
| C880.blif_0.10_0.20_0_1_inp_exact | 662 (661+1) | 662 (661+1) | 663 (662+1) | 800 (799+1) | 343 (342+1) | 800 (798+2) | 800 (800+0) |
| test3_quant_squaring2 | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (799+1) | 800 (797+3) |
| mutex-4-s | 0 (0+0) s cnf 1 |
0 (0+0) s cnf 1 |
0 (0+0) s cnf 1 |
0 (0+0) s cnf 1 |
0 (0+0) s cnf 1 |
0 (0+0) s cnf 1 |
800 (799+1) |
| C499.blif_0.10_1.00_0_0_out_exact | 0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
800 (798+2) | 1 (1+0) s cnf 0 |
| C499.blif_0.10_0.20_0_1_out_exact | 1 (1+0) s cnf 0 |
1 (1+0) s cnf 0 |
2 (2+0) s cnf 0 |
1 (1+0) s cnf 0 |
1 (1+0) s cnf 0 |
800 (798+2) | 800 (799+1) |
| C499.blif_0.10_0.20_0_0_out_exact | 1 (1+0) s cnf 0 |
1 (1+0) s cnf 0 |
2 (2+0) s cnf 0 |
1 (1+0) s cnf 0 |
1 (1+0) s cnf 0 |
800 (798+2) | 800 (799+1) |
| klieber2017q-074-18-eq | 0 (0+0) s cnf 1 |
0 (0+0) s cnf 1 |
0 (0+0) s cnf 1 |
0 (0+0) s cnf 1 |
0 (0+0) s cnf 1 |
26 (26+0) s cnf 1 |
17 (17+0) s cnf 1 |
| klieber2017q-076-19-t1 | 0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
50 (50+0) s cnf 0 |
15 (15+0) s cnf 0 |
| klieber2017q-076-19-eq | 0 (0+0) s cnf 1 |
0 (0+0) s cnf 1 |
1 (1+0) s cnf 1 |
0 (0+0) s cnf 1 |
0 (0+0) s cnf 1 |
51 (51+0) s cnf 1 |
10 (10+0) s cnf 1 |
| klieber2017q-078-19-t1 | 0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
11 (11+0) s cnf 0 |
75 (75+0) s cnf 0 |
| klieber2017q-078-19-eq | 0 (0+0) s cnf 1 |
0 (0+0) s cnf 1 |
1 (1+0) s cnf 1 |
0 (0+0) s cnf 1 |
0 (0+0) s cnf 1 |
46 (46+0) s cnf 1 |
9 (9+0) s cnf 1 |
| klieber2017q-080-20-t1 | 0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
15 (15+0) s cnf 0 |
39 (39+0) s cnf 0 |
| klieber2017q-074-18-t1 | 0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
5 (5+0) s cnf 0 |
17 (16+0) s cnf 0 |
| klieber2017q-080-20-eq | 0 (0+0) s cnf 1 |
0 (0+0) s cnf 1 |
1 (1+0) s cnf 1 |
0 (0+0) s cnf 1 |
0 (0+0) s cnf 1 |
20 (20+0) s cnf 1 |
470 (469+1) s cnf 1 |
| klieber2017q-084-21-eq | 0 (0+0) s cnf 1 |
0 (0+0) s cnf 1 |
0 (0+0) s cnf 1 |
0 (0+0) s cnf 1 |
0 (0+0) s cnf 1 |
38 (38+0) s cnf 1 |
37 (37+0) s cnf 1 |
| klieber2017q-084-21-t1 | 0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
1 (1+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
43 (43+0) s cnf 0 |
342 (341+0) s cnf 0 |
| klieber2017q-082-20-eq | 0 (0+0) s cnf 1 |
1 (0+0) s cnf 1 |
1 (0+0) s cnf 1 |
1 (0+0) s cnf 1 |
0 (0+0) s cnf 1 |
54 (54+0) s cnf 1 |
28 (28+0) s cnf 1 |
| klieber2017q-082-20-t1 | 0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
18 (18+0) s cnf 0 |
16 (16+0) s cnf 0 |
| klieber2017q-088-22-t1 | 0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
7 (7+0) s cnf 0 |
65 (64+0) s cnf 0 |
| klieber2017q-086-21-eq | 0 (0+0) s cnf 1 |
0 (0+0) s cnf 1 |
0 (0+0) s cnf 1 |
0 (0+0) s cnf 1 |
0 (0+0) s cnf 1 |
117 (117+0) s cnf 1 |
20 (20+0) s cnf 1 |
| klieber2017q-086-21-t1 | 0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
44 (44+0) s cnf 0 |
120 (120+0) s cnf 0 |
| klieber2017q-092-23-eq | 1 (1+0) s cnf 1 |
1 (0+0) s cnf 1 |
1 (1+0) s cnf 1 |
1 (1+0) s cnf 1 |
1 (1+0) s cnf 1 |
41 (41+0) s cnf 1 |
104 (104+0) s cnf 1 |
| klieber2017q-092-23-t1 | 0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
1 (1+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
54 (54+0) s cnf 0 |
41 (41+0) s cnf 0 |
| klieber2017q-088-22-eq | 1 (1+0) s cnf 1 |
1 (1+0) s cnf 1 |
1 (1+0) s cnf 1 |
1 (1+0) s cnf 1 |
1 (1+0) s cnf 1 |
53 (53+0) s cnf 1 |
139 (139+0) s cnf 1 |
| klieber2017q-100-25-eq | 1 (1+0) s cnf 1 |
1 (1+0) s cnf 1 |
1 (1+0) s cnf 1 |
1 (1+0) s cnf 1 |
1 (1+0) s cnf 1 |
131 (131+0) s cnf 1 |
42 (42+0) s cnf 1 |
| klieber2017q-096-24-t1 | 1 (1+0) s cnf 0 |
0 (0+0) s cnf 0 |
1 (1+0) s cnf 0 |
0 (0+0) s cnf 0 |
1 (1+0) s cnf 0 |
179 (178+0) s cnf 0 |
57 (57+0) s cnf 0 |
| stmt16_950_951 | 0 (0+0) s cnf 1 |
0 (0+0) s cnf 1 |
0 (0+0) s cnf 1 |
0 (0+0) s cnf 1 |
0 (0+0) s cnf 1 |
800 (799+1) | 0 (0+0) s cnf 1 |
| klieber2017q-100-25-t1 | 0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
34 (34+0) s cnf 0 |
37 (37+0) s cnf 0 |
| klieber2017q-104-26-eq | 1 (1+0) s cnf 1 |
1 (1+0) s cnf 1 |
1 (1+0) s cnf 1 |
1 (1+0) s cnf 1 |
1 (1+0) s cnf 1 |
87 (86+0) s cnf 1 |
91 (91+0) s cnf 1 |
| klieber2017q-096-24-eq | 1 (1+0) s cnf 1 |
1 (1+0) s cnf 1 |
1 (1+0) s cnf 1 |
1 (1+0) s cnf 1 |
1 (1+0) s cnf 1 |
36 (36+0) s cnf 1 |
122 (122+0) s cnf 1 |
| klieber2017q-104-26-t1 | 1 (1+0) s cnf 0 |
1 (1+0) s cnf 0 |
1 (1+0) s cnf 0 |
1 (1+0) s cnf 0 |
1 (1+0) s cnf 0 |
9 (9+0) s cnf 0 |
11 (11+0) s cnf 0 |
| klieber2017q-108-27-t1 | 0 (0+0) s cnf 0 |
1 (1+0) s cnf 0 |
1 (1+0) s cnf 0 |
1 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
30 (30+0) s cnf 0 |
13 (13+0) s cnf 0 |
| test3_quant_squaring4 | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (799+2) | 621 (618+2) |
| klieber2017q-112-28-eq | 1 (1+0) s cnf 1 |
1 (1+0) s cnf 1 |
2 (2+0) s cnf 1 |
1 (1+0) s cnf 1 |
1 (1+0) s cnf 1 |
128 (128+0) s cnf 1 |
493 (492+1) s cnf 1 |
| klieber2017q-112-28-t1 | 1 (1+0) s cnf 0 |
0 (0+0) s cnf 0 |
1 (1+0) s cnf 0 |
0 (0+0) s cnf 0 |
1 (1+0) s cnf 0 |
80 (79+0) s cnf 0 |
27 (26+0) s cnf 0 |
| klieber2017q-108-27-eq | 1 (1+0) s cnf 1 |
1 (1+0) s cnf 1 |
1 (1+0) s cnf 1 |
1 (1+0) s cnf 1 |
1 (1+0) s cnf 1 |
108 (107+0) s cnf 1 |
800 (799+1) |
| uclid-pipe2 | 800 (800+0) | 800 (800+0) | 9 (9+0) s cnf 1 |
800 (800+0) | 800 (800+0) | 800 (798+2) | 800 (800+0) |
| uclid-pipe3a | 40 (40+0) s cnf 1 |
40 (40+0) s cnf 1 |
2 (2+0) s cnf 1 |
41 (40+0) s cnf 1 |
41 (41+0) s cnf 1 |
800 (798+2) | 800 (800+0) |
| klieber2017q-116-29-t1 | 1 (1+0) s cnf 0 |
1 (0+0) s cnf 0 |
1 (1+0) s cnf 0 |
1 (0+0) s cnf 0 |
1 (1+0) s cnf 0 |
169 (169+0) s cnf 0 |
800 (799+1) |
| klieber2017q-116-29-eq | 3 (3+0) s cnf 1 |
3 (3+0) s cnf 1 |
5 (5+0) s cnf 1 |
3 (3+0) s cnf 1 |
3 (3+0) s cnf 1 |
524 (523+1) s cnf 1 |
138 (138+0) s cnf 1 |
| ci.e#1.a#3.E#40.A#60.c#312.w#2.s#3.asp | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 137 (137+0) s cnf 1 |
800 (800+0) |
| driver_d9y.sat | 266 (265+0) s cnf 1 |
800 (800+0) | 161 (161+0) s cnf 1 |
800 (800+0) | 800 (800+0) | 800 (798+2) | 800 (800+0) |
| driver_d9y.unsat | 0 (0+0) s cnf 0 |
1 (1+0) s cnf 0 |
0 (0+0) s cnf 0 |
5 (5+0) s cnf 0 |
1 (1+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
| stmt41_738_749 | 0 (0+0) s cnf 1 |
0 (0+0) s cnf 1 |
0 (0+0) s cnf 1 |
0 (0+0) s cnf 1 |
0 (0+0) s cnf 1 |
800 (798+2) | 1 (0+0) s cnf 1 |
| ci.e#1.a#3.E#40.A#60.c#376.w#2.s#4.asp | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (799+1) | 800 (800+0) |
| ci.e#1.a#3.E#40.A#60.c#400.w#2.s#1.asp | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 33 (33+0) s cnf 0 |
800 (800+0) |
| stmt41_160_235 | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (799+1) | 800 (800+0) | 800 (799+1) | 800 (800+0) |
| ci.e#1.a#3.E#40.A#60.c#416.w#2.s#3.asp | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 534 (533+1) s cnf 0 |
800 (800+0) |
| ci.e#1.a#3.E#40.A#60.c#424.w#2.s#1.asp | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 0 (0+0) s cnf 0 |
800 (800+0) |
| ci.e#1.a#3.E#40.A#60.c#432.w#2.s#8.asp | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 0 (0+0) s cnf 0 |
800 (800+0) |
| ci.e#1.a#3.E#40.A#60.c#264.w#4.s#2.asp | 800 (800+0) | 800 (800+0) | 800 (800+0) | 323 (322+0) s cnf 1 |
800 (800+0) | 4 (4+0) s cnf 1 |
96 (96+0) s cnf 1 |
| ci.e#1.a#3.E#40.A#60.c#288.w#4.s#8.asp | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 22 (22+0) s cnf 1 |
800 (800+0) |
| Umbrella_tbm_05.tex.module.000039 | 800 (800+1) | 800 (800+0) | 800 (799+1) | 800 (800+1) | 800 (800+0) | 800 (799+1) | 800 (800+0) |
| ci.e#1.a#3.E#40.A#60.c#200.w#6.s#6.asp | 29 (29+0) s cnf 1 |
25 (25+0) s cnf 1 |
98 (98+0) s cnf 1 |
4 (4+0) s cnf 1 |
32 (32+0) s cnf 1 |
0 (0+0) s cnf 1 |
5 (4+0) s cnf 1 |
| amba2f9n.sat | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (799+1) | 800 (800+0) |
| amba2f9n.unsat | 22 (22+0) s cnf 0 |
33 (33+0) s cnf 0 |
19 (19+0) s cnf 0 |
30 (30+0) s cnf 0 |
22 (22+0) s cnf 0 |
678 (676+2) s cnf 0 |
51 (51+0) s cnf 0 |
| ci.e#1.a#3.E#40.A#60.c#304.w#4.s#7.asp | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 160 (160+0) s cnf 1 |
800 (800+0) |
| ci.e#1.a#3.E#40.A#60.c#208.w#6.s#8.asp | 800 (800+0) | 237 (237+0) s cnf 1 |
800 (800+0) | 86 (86+0) s cnf 1 |
503 (503+0) s cnf 1 |
1 (1+0) s cnf 1 |
17 (17+0) s cnf 1 |
| ci.e#1.a#3.E#40.A#60.c#320.w#4.s#8.asp | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 54 (54+0) s cnf 1 |
800 (800+0) |
| ci.e#1.a#3.E#40.A#60.c#336.w#4.s#5.asp | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (799+1) | 800 (800+0) |
| test1_quant_squaring3 | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (799+1) | 557 (555+2) |
| szymanski-5-s | 0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
1 (1+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
800 (799+1) |
| ci.e#1.a#3.E#40.A#60.c#344.w#4.s#5.asp | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) |
| C5315.blif_0.10_0.20_0_0_out_exact | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (798+2) | 800 (800+0) |
| k5_2_3 | 471 (470+1) s cnf 1 |
471 (470+1) s cnf 1 |
688 (686+2) s cnf 1 |
472 (471+1) s cnf 1 |
471 (470+1) s cnf 1 |
800 (798+2) | 800 (799+1) |
| k_ph_p-12 | 41 (41+0) s cnf 0 |
285 (285+0) s cnf 0 |
102 (102+0) s cnf 0 |
130 (129+0) s cnf 0 |
41 (41+0) s cnf 0 |
800 (800+0) | 800 (799+1) |
| rankfunc17_unsigned_16 | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (799+1) | 800 (800+0) | 800 (798+2) | 800 (800+1) |
| small-swap1-fixpoint-3 | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (798+2) | 600 (598+2) |
| ci.e#1.a#3.E#40.A#60.c#408.w#4.s#3.asp | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (799+1) | 800 (800+0) |
| C6288.blif_0.10_1.00_0_0_out_exact | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (799+1) | 800 (800+0) |
| ci.e#1.a#3.E#40.A#60.c#280.w#6.s#7.asp | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 173 (173+0) s cnf 1 |
800 (800+0) |
| ltl2dba_C2-6_comp3_REAL.unsat | 0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
0 (0+0) s cnf 0 |
445 (444+1) s cnf 0 |
0 (0+0) s cnf 0 |
| ltl2dba_C2-6_comp3_REAL.sat | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (798+2) | 800 (800+0) |
| ci.e#1.a#3.E#40.A#60.c#296.w#6.s#7.asp | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 38 (37+0) s cnf 1 |
800 (800+0) |
| ci.e#1.a#3.E#40.A#60.c#304.w#6.s#8.asp | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 101 (101+0) s cnf 1 |
800 (800+0) |
| C6288.blif_0.10_0.20_0_0_out_exact | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (799+1) | 800 (800+0) |
| sortnetsort9.v.stepl.005 | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (798+2) | 800 (800+1) |
| arbiter-08-comp-error02-qbf-hardness-depth-9 | 69 (68+1) | 69 (68+1) | 69 (68+1) | 800 (799+1) | 28 (27+1) | 11 (11+0) s cnf 1 |
800 (799+1) |
| C6288.blif_0.10_0.20_0_1_out_exact | 800 (800+0) | 800 (800+0) | 25 (25+0) s cnf 1 |
800 (800+0) | 800 (800+0) | 800 (799+1) | 800 (800+0) |
| C6288.blif_0.10_0.20_0_0_inp_exact | 458 (457+1) | 458 (457+1) | 458 (457+1) | 800 (799+2) | 363 (362+1) | 800 (798+2) | 800 (800+0) |
| small-swap2-fixpoint-4 | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (798+2) | 675 (672+2) |
| ci.e#1.a#3.E#40.A#60.c#384.w#6.s#8.asp | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (799+1) | 800 (800+0) |
| ci.e#1.a#3.E#40.A#60.c#392.w#6.s#4.asp | 800 (800+0) | 800 (800+0) | 800 (799+1) | 800 (800+0) | 800 (800+0) | 800 (799+1) | 800 (800+0) |
| rankfunc5_unsigned_64 | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (799+1) | 800 (800+0) | 800 (798+2) | 800 (800+0) |
| JP-unsat-02-07-2 | 4 (4+0) s cnf 0 |
4 (4+0) s cnf 0 |
7 (6+0) s cnf 0 |
3 (3+0) s cnf 0 |
4 (4+0) s cnf 0 |
1 (1+0) s cnf 0 |
7 (7+0) s cnf 0 |
| rankfunc33_signed_32 | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (799+1) | 800 (800+0) |
| sortnetsort10.v.stepl.005 | 800 (799+1) | 800 (799+1) | 800 (800+0) | 800 (800+0) | 800 (799+1) | 800 (798+2) | 800 (800+0) |
| sdlx-fixpoint-3 | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+1) | 800 (800+0) | 800 (798+2) | 800 (799+1) |
| rankfunc14_signed_64 | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (799+1) | 800 (800+0) | 800 (798+2) | 800 (800+0) |
| small-synabs-fixpoint-9 | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (798+2) | 717 (715+2) |
| sortnetsort9.v.stepl.007 | 38 (38+0) s cnf 1 |
10 (10+0) s cnf 1 |
59 (59+0) s cnf 1 |
10 (10+0) s cnf 1 |
40 (40+0) s cnf 1 |
800 (798+2) | 800 (799+1) |
| cnt14 | 800 (799+1) | 800 (799+1) | 800 (799+1) | 800 (799+1) | 800 (799+1) | 614 (612+2) | 800 (800+0) |
| adder-10-sat | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (799+1) | 800 (800+0) |
| genbuf9b4n.sat | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (799+1) | 800 (799+1) |
| genbuf9b4n.unsat | 246 (246+0) s cnf 0 |
336 (336+0) s cnf 0 |
235 (235+0) s cnf 0 |
800 (800+0) | 800 (800+0) | 800 (798+2) | 500 (498+1) s cnf 0 |
| szymanski-6-s | 1 (1+0) s cnf 0 |
2 (1+0) s cnf 0 |
2 (2+0) s cnf 0 |
1 (1+0) s cnf 0 |
1 (1+0) s cnf 0 |
1 (1+0) s cnf 0 |
800 (800+0) |
| genbuf10b4n.sat | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (799+1) | 800 (799+1) |
| genbuf10b4n.unsat | 374 (374+0) s cnf 0 |
469 (469+0) s cnf 0 |
349 (349+0) s cnf 0 |
800 (800+0) | 800 (800+0) | 800 (798+2) | 741 (740+2) s cnf 0 |
| mutex-32-s | 1 (1+0) s cnf 1 |
1 (1+0) s cnf 1 |
1 (1+0) s cnf 1 |
1 (1+0) s cnf 1 |
1 (1+0) s cnf 1 |
1 (1+0) s cnf 1 |
800 (800+0) |
| CHAIN20v.21 | 1 (1+0) s cnf 1 |
1 (1+0) s cnf 1 |
1 (1+0) s cnf 1 |
1 (1+0) s cnf 1 |
1 (1+0) s cnf 1 |
800 (799+1) | 776 (773+3) |
| rankfunc13_unsigned_64 | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (798+2) | 800 (799+1) |
| Core1108_tbm_02.tex.moduleQ3.2S.000015 | 800 (800+0) | 800 (799+1) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 0 (0+0) s cnf 0 |
800 (800+0) |
| JP-unsat-02-06-3 | 26 (26+0) s cnf 0 |
22 (22+0) s cnf 0 |
37 (37+0) s cnf 0 |
13 (13+0) s cnf 0 |
31 (31+0) s cnf 0 |
2 (2+0) s cnf 0 |
27 (27+0) s cnf 0 |
| k_branch_n-10 | 800 (799+1) | 800 (799+1) | 800 (799+1) | 800 (799+1) | 800 (799+1) | 149 (148+1) s cnf 1 |
800 (800+0) |
| k_branch_p-10 | 800 (799+1) | 800 (799+1) | 800 (799+1) | 800 (799+1) | 800 (799+1) | 3 (3+0) s cnf 0 |
800 (800+1) |
| ken.oop^2.C-d4 | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (799+1) | 800 (800+0) | 800 (799+1) | 800 (799+1) |
| SR-unsat-03-01-07-1 | 2 (2+0) s cnf 0 |
2 (2+0) s cnf 0 |
2 (2+0) s cnf 0 |
2 (2+0) s cnf 0 |
2 (2+0) s cnf 0 |
0 (0+0) s cnf 0 |
7 (7+0) s cnf 0 |
| cnt16r | 800 (799+1) | 800 (799+1) | 800 (799+1) | 800 (799+1) | 800 (799+1) | 800 (798+2) | 800 (800+0) |
| driver_a9n.sat | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (798+2) | 800 (799+1) |
| driver_a9n.unsat | 7 (7+0) s cnf 0 |
38 (38+0) s cnf 0 |
2 (2+0) s cnf 0 |
800 (800+0) | 800 (800+0) | 800 (798+2) | 42 (42+0) s cnf 0 |
| k8_2_3 | 800 (799+1) | 800 (799+1) | 800 (799+1) | 800 (799+1) | 800 (799+1) | 800 (798+2) | 800 (799+1) |
| cycle_sched_6_7_1.sat | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (799+1) | 800 (800+0) | 800 (798+2) | 800 (799+1) |
| cycle_sched_6_7_1.unsat | 800 (800+0) | 800 (800+1) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (798+2) | 800 (799+1) |
| ltl2dpa_C26_comp2_REAL.sat | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (798+2) | 800 (799+1) |
| ltl2dpa_C26_comp2_REAL.unsat | 1 (1+0) s cnf 0 |
1 (1+0) s cnf 0 |
1 (1+0) s cnf 0 |
1 (1+0) s cnf 0 |
1 (1+0) s cnf 0 |
800 (798+2) | 1 (1+0) s cnf 0 |
| k_branch_p-11 | 800 (799+1) | 800 (799+1) | 800 (798+2) | 800 (799+1) | 800 (799+1) | 28 (28+0) s cnf 0 |
800 (799+1) |
| amba4b9y.sat | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (799+1) | 800 (799+1) |
| amba4b9y.unsat | 800 (800+0) | 800 (800+1) | 800 (800+1) | 800 (800+0) | 800 (800+0) | 800 (798+2) | 800 (799+1) |
| CHAIN22v.23 | 2 (2+0) s cnf 1 |
2 (2+0) s cnf 1 |
2 (2+0) s cnf 1 |
2 (2+0) s cnf 1 |
2 (2+0) s cnf 1 |
800 (799+1) | 381 (379+2) |
| adder-12-unsat | 268 (267+1) | 594 (593+1) | 225 (223+1) | 800 (799+1) | 258 (257+1) | 800 (798+2) | 800 (800+0) |
| stmt17_63_82 | 54 (53+0) s cnf 1 |
50 (50+0) s cnf 1 |
70 (70+0) s cnf 1 |
21 (20+0) s cnf 1 |
51 (51+0) s cnf 1 |
800 (799+1) | 800 (799+1) |
| test2_quant_squaring2 | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (798+2) | 411 (409+2) |
| CHAIN23v.24 | 2 (2+0) s cnf 1 |
2 (2+0) s cnf 1 |
2 (2+0) s cnf 1 |
2 (2+0) s cnf 1 |
2 (2+0) s cnf 1 |
800 (799+1) | 206 (204+2) |
| stmt28_68_81 | 47 (47+0) s cnf 1 |
88 (87+0) s cnf 1 |
73 (73+0) s cnf 1 |
23 (23+0) s cnf 1 |
46 (46+0) s cnf 1 |
800 (799+1) | 370 (370+0) s cnf 1 |
| stay24n.sat | 77 (77+0) s cnf 1 |
46 (46+0) s cnf 1 |
13 (13+0) s cnf 1 |
800 (800+0) | 800 (800+0) | 800 (798+2) | 800 (800+0) |
| stay24n.unsat | 1 (1+0) s cnf 0 |
1 (1+0) s cnf 0 |
1 (1+0) s cnf 0 |
1 (1+0) s cnf 0 |
1 (1+0) s cnf 0 |
0 (0+0) s cnf 0 |
1 (1+0) s cnf 0 |
| BLOCKS4iii.6 | 1 (1+0) s cnf 0 |
1 (1+0) s cnf 0 |
1 (1+0) s cnf 0 |
1 (1+0) s cnf 0 |
1 (1+0) s cnf 0 |
800 (798+2) | 2 (2+0) s cnf 0 |
| k_branch_n-12 | 800 (799+1) | 800 (799+1) | 800 (795+5) | 800 (799+1) | 800 (799+1) | 800 (797+3) | 800 (800+1) |
| incrementer-enc07-uniform-depth-25 | 1 (1+0) s cnf 0 |
1 (1+0) s cnf 0 |
1 (1+0) s cnf 0 |
1 (1+0) s cnf 0 |
1 (1+0) s cnf 0 |
800 (799+1) | 15 (14+0) s cnf 0 |
| ev-pr-4x4-11-3-0-0-1-lg | 800 (799+1) | 800 (800+1) | 800 (799+1) | 800 (799+1) | 800 (799+1) | 535 (533+1) s cnf 1 |
501 (500+1) s cnf 1 |
| k_ph_p-19 | 800 (800+1) | 800 (799+1) | 800 (799+1) | 800 (799+1) | 800 (799+1) | 800 (799+1) | 800 (799+1) |
| stmt19_64_99 | 60 (60+0) s cnf 1 |
54 (54+0) s cnf 1 |
82 (81+0) s cnf 1 |
25 (25+0) s cnf 1 |
63 (63+0) s cnf 1 |
800 (799+1) | 800 (800+0) |
| stmt17_70_90 | 58 (58+0) s cnf 1 |
53 (53+0) s cnf 1 |
94 (94+0) s cnf 1 |
26 (26+0) s cnf 1 |
62 (61+0) s cnf 1 |
800 (799+1) | 800 (800+0) |
| p20-1.pddl_planlen=24 | 107 (107+0) s cnf 0 |
107 (107+0) s cnf 0 |
165 (165+0) s cnf 0 |
108 (108+0) s cnf 0 |
107 (107+0) s cnf 0 |
800 (800+1) | 800 (800+0) |
| incrementer-enc08-uniform-depth-33 | 2 (2+0) s cnf 1 |
2 (2+0) s cnf 1 |
2 (2+0) s cnf 1 |
2 (2+0) s cnf 1 |
2 (2+0) s cnf 1 |
800 (799+1) | 5 (5+0) s cnf 1 |
| consistency_0_1 | 13 (12+0) s cnf 1 |
13 (12+0) s cnf 1 |
13 (13+0) s cnf 1 |
12 (12+0) s cnf 1 |
13 (12+0) s cnf 1 |
800 (798+2) | 800 (800+0) |
| possibility10_0_1 | 800 (799+1) | 800 (800+0) | 800 (799+1) | 800 (800+0) | 800 (799+1) | 800 (798+2) | 64 (64+0) s cnf 0 |
| assertion12_0_1 | 1 (1+0) s cnf 0 |
1 (1+0) s cnf 0 |
1 (1+0) s cnf 0 |
1 (1+0) s cnf 0 |
1 (1+0) s cnf 0 |
10 (10+0) s cnf 0 |
1 (1+0) s cnf 0 |
| b20_PR_7_20 | 7 (7+0) s cnf 1 |
7 (7+0) s cnf 1 |
15 (15+0) s cnf 1 |
800 (800+0) | 800 (800+0) | 800 (799+1) | 110 (109+1) s cnf 1 |
| possibility8_0_1 | 316 (316+1) s cnf 1 |
180 (180+0) s cnf 1 |
663 (662+1) s cnf 1 |
123 (122+0) s cnf 1 |
324 (323+1) s cnf 1 |
800 (798+2) | 800 (800+0) |
| possibility5_0_1 | 800 (800+0) | 800 (800+0) | 800 (799+1) | 128 (128+0) s cnf 0 |
800 (799+1) | 800 (798+2) | 53 (52+0) s cnf 0 |
| adder-14-sat | 800 (799+1) | 800 (799+1) | 800 (799+1) | 800 (799+1) | 800 (799+1) | 800 (799+1) | 800 (800+1) |
| f600-50 | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (799+1) |
| ev-pr-4x4-13-3-0-0-1-lg | 800 (799+1) | 800 (799+1) | 800 (799+1) | 800 (799+1) | 800 (799+1) | 800 (798+2) | 592 (590+1) |
| ken.flash^08.C-d4 | 499 (499+0) s cnf 0 |
274 (273+0) s cnf 0 |
160 (160+0) s cnf 0 |
696 (695+1) s cnf 0 |
670 (670+0) s cnf 0 |
800 (799+1) | 800 (800+1) |
| k_ph_n-21 | 130 (130+0) s cnf 1 |
23 (23+0) s cnf 1 |
474 (473+1) s cnf 1 |
54 (54+0) s cnf 1 |
131 (130+0) s cnf 1 |
6 (6+0) s cnf 1 |
800 (799+1) |
| test2_quant_squaring3 | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (798+2) | 453 (452+1) |
| mutex-64-s | 1 (1+0) s cnf 1 |
1 (1+0) s cnf 1 |
1 (1+0) s cnf 1 |
1 (1+0) s cnf 1 |
1 (1+0) s cnf 1 |
3 (3+0) s cnf 1 |
800 (799+1) |
| stmt17_86_98 | 110 (110+0) s cnf 1 |
83 (83+0) s cnf 1 |
179 (179+0) s cnf 1 |
35 (35+0) s cnf 1 |
112 (112+0) s cnf 1 |
800 (799+1) | 676 (676+0) s cnf 1 |
| network_ndis_rtlnwifi_hw_hw_ccmp.c | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (799+1) | 800 (800+0) | 800 (799+1) | 501 (500+1) |
| mult_bool_matrix_10_9_11.sat | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (799+1) | 800 (800+0) | 800 (799+1) | 800 (800+0) |
| mult_bool_matrix_10_9_11.unsat | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (799+1) | 800 (800+0) | 800 (799+1) | 800 (800+0) |
| cube_c7_ser--opt-24_ | 9 (9+0) s cnf 1 |
8 (8+0) s cnf 1 |
12 (12+0) s cnf 1 |
8 (8+0) s cnf 1 |
9 (9+0) s cnf 1 |
800 (799+1) | 538 (537+1) s cnf 1 |
| k_branch_p-16 | 800 (799+1) | 800 (799+1) | 800 (797+3) | 800 (799+1) | 800 (799+1) | 359 (357+2) s cnf 0 |
800 (799+1) |
| szymanski-8-s | 9 (9+0) s cnf 0 |
9 (9+0) s cnf 0 |
14 (13+1) s cnf 0 |
9 (9+0) s cnf 0 |
9 (9+0) s cnf 0 |
5 (5+0) s cnf 0 |
800 (800+1) |
| sortnetsort9.AE.stepl.012 | 7 (7+0) s cnf 0 |
15 (14+1) s cnf 0 |
5 (5+0) s cnf 0 |
12 (11+1) s cnf 0 |
7 (7+0) s cnf 0 |
298 (297+0) s cnf 0 |
800 (799+1) |
| b22_PR_8_20 | 36 (35+0) s cnf 1 |
36 (35+0) s cnf 1 |
32 (32+0) s cnf 1 |
800 (799+1) | 800 (799+1) | 800 (799+1) | 103 (102+1) s cnf 1 |
| s15850_PR_8_50 | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (799+1) | 800 (800+0) | 800 (799+1) | 800 (799+1) |
| incrementer-enc02-uniform-depth-58 | 4 (3+0) s cnf 0 |
4 (3+0) s cnf 0 |
4 (3+0) s cnf 0 |
4 (3+0) s cnf 0 |
4 (3+0) s cnf 0 |
800 (799+1) | 407 (406+1) s cnf 0 |
| audio_ddksynth_csynth2.cpp | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (799+1) | 800 (800+0) | 800 (799+1) | 516 (515+1) |
| ev-pr-6x6-9-5-0-1-2-lg | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 446 (445+1) s cnf 0 |
236 (235+1) |
| SR-unsat-04-01-08-1 | 76 (75+2) s cnf 0 |
70 (69+2) s cnf 0 |
96 (94+2) s cnf 0 |
101 (99+1) s cnf 0 |
77 (74+2) s cnf 0 |
12 (12+0) s cnf 0 |
71 (71+0) s cnf 0 |
| arbiter-10-comp-error01-qbf-hardness-depth-22 | 239 (237+2) | 239 (237+2) | 253 (251+2) | 239 (237+2) | 240 (238+2) | 800 (798+2) | 800 (799+1) |
| query44_query26_1344n | 800 (794+6) | 800 (795+5) | 800 (795+5) | 800 (765+35) | 800 (772+28) | 800 (799+1) | 800 (799+1) |
| cache-coherence-2-fixpoint-6 | 800 (776+24) | 800 (780+20) | 800 (775+25) | 800 (765+35) | 800 (774+27) | 800 (799+1) | 738 (737+1) |
| consistency_0_2 | 2 (1+0) | 2 (1+0) | 2 (1+0) | 2 (1+0) | 1 (1+0) | 10 (9+1) | 1 (1+0) |
| possibility10_0_2 | 2 (1+0) | 2 (1+0) | 2 (1+0) | 2 (1+0) | 1 (1+0) | 10 (9+1) | 1 (1+0) |
| assertion12_0_2 | 2 (1+0) | 2 (1+0) | 2 (1+0) | 2 (1+0) | 2 (1+0) | 10 (9+1) | 1 (1+0) |
| ev-pr-6x6-11-5-0-1-2-lg | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+1) | 800 (799+1) | 168 (167+1) |
| emptyroom_e4_ser--opt-44_ | 147 (147+0) s cnf 1 |
147 (147+0) s cnf 1 |
390 (389+1) s cnf 1 |
146 (146+0) s cnf 1 |
147 (146+0) s cnf 1 |
800 (799+1) | 800 (799+1) |
| load_3c_comp_comp7_REAL.sat | 800 (788+12) | 800 (797+3) | 800 (795+5) | 800 (772+28) | 800 (796+4) | 800 (799+2) | 800 (799+1) |
| load_3c_comp_comp7_REAL.unsat | 6 (6+0) s cnf 0 |
6 (6+0) s cnf 0 |
6 (6+0) s cnf 0 |
6 (6+0) s cnf 0 |
6 (6+0) s cnf 0 |
800 (798+2) | 68 (67+0) s cnf 0 |
| ev-pr-8x8-7-7-0-1-2-lg | 152 (151+0) s cnf 0 |
149 (148+0) s cnf 0 |
146 (146+0) s cnf 0 |
149 (149+0) s cnf 0 |
142 (142+0) s cnf 0 |
40 (40+0) s cnf 0 |
327 (326+1) |
| CM-unsat-07-01-06-2 | 800 (797+3) | 800 (796+4) | 800 (798+2) | 800 (761+39) | 800 (797+3) | 287 (287+0) s cnf 0 |
800 (799+1) |
| s1269_d12_u | 800 (798+2) | 800 (798+2) | 800 (798+2) | 800 (749+51) | 800 (798+2) | 800 (799+1) | 800 (799+1) |
| cycle_sched_4_7_1.sat | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (799+1) | 800 (799+1) |
| cycle_sched_4_7_1.unsat | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (799+1) | 800 (799+1) |
| s1269_d13_u | 800 (798+2) | 800 (798+2) | 800 (798+2) | 800 (750+50) | 800 (798+2) | 800 (799+1) | 800 (799+1) |
| ev-pr-6x6-17-5-0-1-2-lg | 800 (800+1) | 800 (800+1) | 800 (799+1) | 800 (800+0) | 800 (799+1) | 800 (799+1) | 144 (143+1) |
| possibility1_0_3 | 2 (2+0) | 2 (2+0) | 2 (2+0) | 2 (2+0) | 2 (2+0) | 9 (8+1) | 1 (1+0) |
| consistency_0_3 | 2 (2+0) | 2 (2+0) | 2 (2+0) | 2 (2+0) | 2 (2+0) | 9 (8+1) | 1 (1+0) |
| possibility7_0_3 | 2 (2+0) | 2 (2+0) | 2 (2+0) | 2 (2+0) | 2 (2+0) | 9 (8+1) | 1 (1+0) |
| possibility6_0_3 | 2 (2+0) | 2 (2+0) | 2 (2+0) | 2 (2+0) | 2 (2+0) | 9 (8+1) | 1 (1+0) |
| possibility3_0_3 | 2 (2+0) | 2 (2+0) | 2 (2+0) | 2 (2+0) | 2 (2+0) | 9 (8+1) | 1 (1+0) |
| assertion9_0_3 | 2 (2+0) | 2 (2+0) | 2 (2+0) | 2 (2+0) | 2 (2+0) | 9 (8+1) | 1 (1+0) |
| assertion6_0_3 | 2 (2+0) | 2 (2+0) | 2 (2+0) | 2 (2+0) | 2 (2+0) | 9 (8+1) | 1 (1+0) |
| k12_4_2 | 800 (800+1) | 800 (800+1) | 800 (800+0) | 800 (799+1) | 800 (800+1) | 800 (799+1) | 680 (679+1) |
| assertion2_0_3 | 2 (2+0) | 2 (2+0) | 2 (2+0) | 2 (2+0) | 2 (2+0) | 9 (8+1) | 1 (1+0) |
| assertion7_0_3 | 2 (2+0) | 2 (2+0) | 2 (2+0) | 2 (2+0) | 2 (2+0) | 9 (8+1) | 1 (1+0) |
| s1269_d15_u | 800 (797+3) | 800 (798+2) | 800 (796+4) | 800 (756+44) | 800 (797+3) | 800 (799+1) | 800 (799+1) |
| b21_C_3_206 | 10 (10+0) s cnf 1 |
9 (9+0) s cnf 1 |
13 (13+0) s cnf 1 |
800 (800+1) | 800 (800+0) | 800 (799+1) | 112 (111+1) |
| Adder2-16-s | 800 (772+28) | 800 (776+24) | 800 (764+36) | 800 (763+37) | 800 (774+26) | 800 (799+1) | 800 (799+1) |
| ev-pr-6x6-19-5-0-1-2-lg | 800 (799+1) | 800 (800+1) | 800 (799+1) | 800 (800+0) | 800 (799+1) | 800 (799+1) | 110 (109+1) |
| qshifter_7 | 800 (798+2) | 800 (798+3) | 800 (798+2) | 800 (797+3) | 800 (797+3) | 698 (696+2) | 252 (251+1) |
| ev-pr-4x4-7-3-0-0-1-s | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+1) | 800 (799+1) | 141 (140+1) |
| DW-unsat-08-21-1 | 323 (319+4) s cnf 0 |
280 (274+5) s cnf 0 |
695 (691+4) s cnf 0 |
226 (218+8) s cnf 0 |
287 (282+5) s cnf 0 |
51 (51+0) s cnf 0 |
172 (171+0) s cnf 0 |
| load_full_4_comp3_REAL.sat | 800 (794+6) | 800 (790+10) | 800 (798+2) | 800 (760+40) | 800 (794+6) | 800 (799+1) | 676 (675+1) |
| load_full_4_comp3_REAL.unsat | 203 (203+0) s cnf 0 |
203 (203+0) s cnf 0 |
203 (203+0) s cnf 0 |
203 (203+0) s cnf 0 |
203 (203+0) s cnf 0 |
800 (798+2) | 800 (799+1) |
| DW-sat-08-22-1 | 201 (197+4) s cnf 1 |
189 (185+4) s cnf 1 |
265 (262+3) s cnf 1 |
159 (155+4) s cnf 1 |
185 (180+5) s cnf 1 |
4 (4+0) s cnf 1 |
144 (144+0) s cnf 1 |
| consistency_0_4 | 2 (2+0) | 2 (2+0) | 2 (2+0) | 2 (2+0) | 2 (2+0) | 14 (13+1) | 2 (2+0) |
| input_pnpi8042_moudep.c | 800 (759+41) | 800 (763+37) | 800 (756+44) | 800 (753+47) | 800 (750+50) | 800 (800+0) | 393 (392+1) |
| assertion1_0_4 | 2 (2+0) | 2 (2+0) | 2 (2+0) | 2 (2+0) | 2 (2+0) | 10 (9+1) | 2 (2+0) |
| possibility5_0_4 | 2 (2+0) | 2 (2+0) | 2 (2+0) | 2 (2+0) | 2 (2+0) | 10 (9+1) | 2 (2+0) |
| assertion7_0_4 | 2 (2+0) | 2 (2+0) | 2 (2+0) | 2 (2+0) | 2 (2+0) | 10 (9+1) | 2 (2+0) |
| ev-pr-8x8-13-7-0-1-2-lg | 800 (799+1) | 800 (800+0) | 800 (799+1) | 800 (800+1) | 800 (799+1) | 800 (799+1) | 116 (115+1) |
| DW-sat-08-23-1 | 76 (74+2) s cnf 1 |
79 (76+3) s cnf 1 |
69 (67+2) s cnf 1 |
49 (47+2) s cnf 1 |
125 (121+4) s cnf 1 |
4 (4+0) s cnf 1 |
160 (159+0) s cnf 1 |
| DW-unsat-09-22-1 | 374 (360+14) s cnf 0 |
341 (329+12) s cnf 0 |
179 (172+7) s cnf 0 |
226 (218+8) s cnf 0 |
204 (196+8) s cnf 0 |
121 (120+0) s cnf 0 |
293 (292+1) s cnf 0 |
| network_irda_miniport_nscirda_comm.c | 800 (755+45) | 800 (758+42) | 800 (756+44) | 800 (751+49) | 800 (751+49) | 800 (800+1) | 421 (420+1) |
| s3330_d9_s | 586 (581+5) | 677 (674+4) | 674 (667+7) | 800 (773+27) | 702 (697+5) | 800 (799+1) | 800 (799+1) |
| DW-sat-08-24-1 | 82 (80+2) s cnf 1 |
66 (65+1) s cnf 1 |
148 (145+2) s cnf 1 |
59 (58+1) s cnf 1 |
145 (142+3) s cnf 1 |
19 (19+0) s cnf 1 |
116 (116+1) s cnf 1 |
| k14_2_3 | 800 (799+1) | 800 (799+1) | 800 (799+1) | 800 (799+1) | 800 (799+1) | 800 (799+1) | 800 (799+1) |
| DW-unsat-09-23-1 | 800 (794+6) | 698 (689+9) s cnf 0 |
800 (797+3) | 467 (449+18) s cnf 0 |
698 (690+8) s cnf 0 |
117 (117+0) s cnf 0 |
390 (389+1) s cnf 0 |
| JP-unsat-03-07-4 | 800 (793+7) | 800 (790+10) | 800 (797+3) | 800 (755+45) | 800 (793+7) | 250 (249+0) s cnf 0 |
800 (800+1) |
| ev-pr-8x8-15-7-0-1-2-lg | 800 (799+1) | 800 (799+1) | 800 (799+1) | 800 (800+1) | 800 (799+1) | 800 (799+1) | 148 (147+1) |
| c5_BMC_p2_k64 | 800 (799+1) | 800 (799+1) | 800 (799+1) | 800 (799+1) | 800 (799+1) | 800 (800+1) | 800 (799+1) |
| query42_query06_1344n | 800 (778+22) | 800 (785+15) | 800 (778+22) | 800 (764+36) | 800 (774+26) | 800 (799+1) | 347 (346+1) |
| filesys_smbmrx_cvsndrcv.c | 12 (12+0) s cnf 0 |
12 (12+0) s cnf 0 |
12 (12+0) s cnf 0 |
12 (12+0) s cnf 0 |
12 (12+0) s cnf 0 |
800 (799+1) | 371 (370+1) |
| CM-unsat-07-01-05-3 | 800 (793+7) | 800 (794+6) | 800 (790+10) | 800 (779+21) | 800 (790+10) | 800 (799+1) | 800 (799+1) |
| consistency_0_5 | 3 (3+0) | 3 (3+0) | 3 (3+0) | 3 (3+0) | 3 (3+0) | 16 (14+1) | 2 (2+0) |
| possibility4_0_5 | 3 (3+0) | 3 (3+0) | 3 (3+0) | 3 (3+0) | 3 (3+0) | 16 (14+1) | 2 (2+0) |
| assertion2_0_5 | 3 (3+0) | 3 (3+0) | 3 (3+0) | 6 (5+1) | 3 (3+0) | 16 (15+1) | 2 (2+0) |
| mult_bool_matrix_17_17_17.unsat | 800 (800+0) | 800 (800+0) | 800 (800+1) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (799+1) |
| mult_bool_matrix_17_17_17.sat | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (800+0) | 800 (799+1) | 800 (800+1) |
| ev-pr-8x8-19-7-0-1-2-lg | 800 (799+1) | 800 (799+1) | 800 (799+1) | 800 (799+1) | 800 (799+1) | 800 (799+1) | 141 (139+1) |
| dungeon_i15-m7-u4-v0.pddl_planlen=81 | 565 (564+1) s cnf 0 |
565 (564+1) s cnf 0 |
565 (565+1) s cnf 0 |
565 (564+1) s cnf 0 |
565 (564+1) s cnf 0 |
800 (800+0) | 744 (742+2) |
| beemldelec4b1_c0to127.unsat | 10 (9+0) s cnf 0 |
10 (9+0) s cnf 0 |
10 (10+0) s cnf 0 |
10 (9+0) s cnf 0 |
10 (9+0) s cnf 0 |
1 (1+0) s cnf 0 |
10 (10+0) s cnf 0 |
| beemldelec4b1_c0to127.sat | 800 (799+1) | 800 (799+2) | 800 (799+1) | 800 (788+12) | 800 (799+1) | 800 (799+1) | 171 (169+1) |
| s3330_d12_u | 658 (652+6) | 770 (765+6) | 782 (771+10) | 800 (781+19) | 648 (642+6) | 800 (800+0) | 800 (799+1) |
| JP-sat-03-09-4 | 800 (796+4) | 800 (793+7) | 800 (798+2) | 800 (772+28) | 800 (797+3) | 800 (799+1) | 800 (799+1) |
| CM-sat-07-01-06-3 | 225 (220+6) s cnf 1 |
337 (329+8) s cnf 1 |
271 (264+7) s cnf 1 |
191 (188+3) s cnf 1 |
358 (349+9) s cnf 1 |
251 (250+0) s cnf 1 |
277 (276+1) s cnf 1 |
| DWs-sat-10-23-1 | 485 (473+12) s cnf 1 |
696 (678+17) s cnf 1 |
800 (785+15) | 254 (246+8) s cnf 1 |
543 (530+13) s cnf 1 |
7 (7+0) s cnf 1 |
707 (707+1) s cnf 1 |
| consistency_0_6 | 4 (3+0) | 4 (3+0) | 4 (3+0) | 4 (3+0) | 4 (3+0) | 16 (15+1) | 3 (3+0) |
| CM-unsat-08-01-05-3 | 800 (783+17) | 800 (783+17) | 800 (785+15) | 800 (771+29) | 800 (785+15) | 800 (799+1) | 800 (799+1) |
| possibility7_0_6 | 4 (3+0) | 4 (3+0) | 4 (3+0) | 4 (3+0) | 4 (3+0) | 16 (14+1) | 3 (3+0) |
| possibility3_0_6 | 4 (3+0) | 4 (3+0) | 4 (3+0) | 4 (3+0) | 4 (3+0) | 16 (15+1) | 3 (3+0) |
| assertion10_0_6 | 4 (3+0) | 4 (3+0) | 4 (3+0) | 4 (3+0) | 4 (3+0) | 16 (15+1) | 3 (3+0) |
| assertion3_0_6 | 4 (3+0) | 4 (3+0) | 4 (3+0) | 4 (3+0) | 4 (3+0) | 16 (15+1) | 3 (3+0) |
| assertion2_0_6 | 4 (3+0) | 4 (3+0) | 4 (3+0) | 4 (3+0) | 4 (3+0) | 16 (15+1) | 3 (3+0) |
| oski3ub5i_c0to255.unsat | 10 (10+0) s cnf 0 |
10 (10+0) s cnf 0 |
10 (10+0) s cnf 0 |
10 (10+0) s cnf 0 |
10 (10+0) s cnf 0 |
7 (7+0) s cnf 0 |
19 (19+0) s cnf 0 |
| oski3ub5i_c0to255.sat | 800 (767+33) | 800 (771+29) | 800 (765+35) | 800 (758+42) | 800 (766+34) | 800 (799+1) | 800 (799+1) |
| DWs-sat-10-24-1 | 136 (133+3) s cnf 1 |
720 (707+13) s cnf 1 |
223 (219+4) s cnf 1 |
300 (296+4) s cnf 1 |
457 (446+11) s cnf 1 |
167 (167+0) s cnf 1 |
403 (402+1) s cnf 1 |
| ev-pr-4x4-13-3-0-0-1-s | 800 (800+1) | 800 (800+0) | 800 (800+0) | 800 (799+1) | 800 (800+0) | 800 (799+1) | 148 (147+1) |
| DWs-unsat-11-23-1 | 800 (787+13) | 800 (785+15) | 800 (784+16) | 800 (779+21) | 800 (787+13) | 187 (187+0) s cnf 0 |
800 (799+1) |
| szymanski-14-s | 800 (788+13) | 800 (788+12) | 800 (777+23) | 800 (780+20) | 800 (786+14) | 166 (166+0) s cnf 0 |
800 (799+1) |
| DWs-sat-10-25-1 | 474 (465+9) s cnf 1 |
800 (787+13) | 800 (786+14) | 800 (785+15) | 768 (755+14) s cnf 1 |
9 (9+0) s cnf 1 |
164 (163+1) s cnf 1 |
| ring_r6_ser--opt-17_ | 800 (799+1) | 800 (799+1) | 800 (799+1) | 800 (799+1) | 800 (799+1) | 800 (800+1) | 227 (226+1) |
| c5_BMC_p2_k128 | 800 (799+1) | 800 (799+1) | 800 (798+2) | 800 (798+2) | 800 (799+2) | 800 (800+0) | 800 (799+1) |
| connect_8x7_6_R | 800 (799+1) | 800 (799+1) | 800 (799+1) | 800 (799+1) | 800 (799+1) | 228 (227+1) | 161 (160+1) |
| DWs-unsat-11-24-1 | 800 (778+22) | 800 (788+12) | 800 (775+25) | 800 (771+29) | 800 (777+23) | 299 (299+0) s cnf 0 |
800 (799+1) |
| CM-sat-07-01-07-3 | 196 (190+6) s cnf 1 |
376 (365+11) s cnf 1 |
381 (372+9) s cnf 1 |
403 (384+19) s cnf 1 |
522 (510+12) s cnf 1 |
74 (74+0) s cnf 1 |
800 (799+1) |
| ev-pr-4x4-15-3-0-0-1-s | 800 (800+0) | 800 (799+1) | 800 (800+0) | 800 (799+1) | 800 (799+1) | 800 (799+1) | 157 (155+1) |
| assertion11_0_7 | 4 (4+0) | 4 (4+0) | 4 (4+0) | 4 (4+0) | 4 (4+0) | 22 (20+1) | 4 (4+0) |
| possibility10_0_7 | 4 (4+0) | 4 (4+0) | 4 (4+0) | 4 (4+0) | 4 (4+0) | 22 (21+1) | 4 (4+0) |
| consistency_0_7 | 4 (4+0) | 4 (4+0) | 4 (4+0) | 4 (4+0) | 4 (4+0) | 22 (20+1) | 4 (4+0) |
| possibility11_0_7 | 4 (4+0) | 4 (4+0) | 4 (4+0) | 4 (4+0) | 4 (4+0) | 22 (20+1) | 4 (4+0) |
| possibility4_0_7 | 4 (4+0) | 4 (4+0) | 4 (4+0) | 4 (4+0) | 4 (4+0) | 22 (20+1) | 4 (4+0) |
| assertion9_0_7 | 4 (4+0) | 4 (4+0) | 4 (4+0) | 4 (4+0) | 4 (4+0) | 23 (21+1) | 4 (4+0) |
| possibility6_0_7 | 4 (4+0) | 4 (4+0) | 4 (4+0) | 4 (4+0) | 4 (4+0) | 22 (20+1) | 4 (4+0) |
| possibility8_0_7 | 4 (4+0) | 4 (4+0) | 4 (4+0) | 4 (4+0) | 4 (4+0) | 16 (15+1) | 4 (4+0) |
| DWs-unsat-12-25-1 | 800 (787+13) | 800 (785+15) | 800 (786+14) | 800 (786+14) | 800 (785+15) | 434 (434+0) s cnf 0 |
800 (799+1) |
| ev-pr-4x4-17-3-0-0-1-s | 800 (800+0) | 800 (799+1) | 800 (799+1) | 800 (799+1) | 800 (800+0) | 800 (799+1) | 164 (163+1) |
| consistency_0_8 | 5 (5+0) | 5 (5+0) | 5 (5+0) | 5 (5+0) | 5 (5+0) | 21 (20+1) | 5 (4+0) |
| possibility1_0_8 | 5 (5+0) | 5 (5+0) | 5 (5+0) | 5 (5+0) | 5 (5+0) | 21 (20+1) | 5 (4+0) |
| assertion2_0_8 | 5 (5+0) | 5 (5+0) | 5 (5+0) | 5 (5+0) | 5 (5+0) | 22 (21+1) | 5 (4+0) |
| CM-unsat-17-01-06-2 | 800 (782+18) | 800 (786+14) | 800 (783+17) | 800 (775+25) | 800 (783+17) | 800 (799+1) | 30 (29+1) |
| b20_C_3_2 | 315 (314+1) s cnf 1 |
242 (241+1) s cnf 1 |
800 (799+1) | 800 (799+1) | 800 (799+1) | 508 (507+1) | 199 (198+1) |
| szymanski-16-s | 800 (783+17) | 800 (784+16) | 800 (783+17) | 800 (771+29) | 800 (782+18) | 367 (366+1) s cnf 0 |
800 (800+0) |
| JP-sat-03-08-5 | 800 (780+20) | 800 (782+18) | 800 (785+15) | 800 (768+32) | 800 (781+19) | 800 (800+0) | 800 (799+1) |
| qshifter_8 | 800 (788+12) | 800 (788+12) | 800 (789+11) | 800 (786+14) | 800 (788+12) | 242 (240+1) | 274 (272+1) |
| consistency_0_9 | 6 (6+0) | 6 (6+0) | 6 (6+0) | 6 (6+0) | 6 (6+0) | 19 (18+1) | 6 (5+0) |
| assertion10_0_9 | 6 (6+0) | 6 (6+0) | 6 (6+0) | 6 (6+0) | 6 (6+0) | 20 (19+1) | 6 (5+0) |
| assertion5_0_9 | 6 (6+0) | 6 (6+0) | 6 (6+0) | 6 (6+0) | 6 (6+0) | 20 (19+1) | 6 (5+0) |
| connect_9x8_6_R | 800 (798+2) | 800 (798+2) | 800 (798+2) | 800 (798+2) | 800 (798+2) | 16 (15+1) | 212 (211+1) |
| assertion1_0_9 | 6 (6+0) | 6 (6+0) | 6 (6+0) | 6 (6+0) | 6 (6+0) | 20 (19+1) | 6 (5+0) |
| possibility5_0_9 | 6 (6+0) | 6 (6+0) | 6 (6+0) | 6 (6+0) | 6 (6+0) | 19 (18+1) | 6 (5+0) |
| JP-sat-03-09-5 | 800 (779+21) | 800 (778+22) | 800 (782+19) | 800 (768+32) | 800 (778+22) | 800 (800+0) | 800 (799+1) |
| SR-sat-03-01-08-2 | 800 (782+18) | 800 (782+18) | 800 (781+19) | 800 (777+23) | 800 (780+20) | 176 (176+0) s cnf 1 |
800 (799+1) |
| p20-5.pddl_planlen=32 | 800 (798+2) | 800 (798+2) | 800 (799+2) | 800 (799+1) | 800 (799+1) | 382 (381+1) | 800 (798+2) |
| consistency_0_10 | 7 (7+0) | 7 (7+0) | 7 (7+0) | 7 (7+0) | 7 (7+0) | 24 (23+1) | 7 (6+0) |
| possibility6_0_10 | 7 (7+0) | 7 (7+0) | 7 (7+0) | 7 (7+0) | 7 (7+0) | 24 (23+1) | 7 (6+0) |
| assertion1_0_10 | 7 (7+0) | 7 (7+0) | 7 (7+0) | 7 (7+0) | 7 (7+0) | 25 (24+1) | 7 (6+0) |
| assertion4_0_10 | 7 (7+0) | 7 (7+0) | 7 (7+0) | 7 (7+0) | 7 (7+0) | 25 (24+1) | 7 (7+0) |
| CM-sat-07-01-06-4 | 800 (781+19) | 800 (780+20) | 800 (783+18) | 678 (662+16) s cnf 1 |
800 (781+19) | 103 (102+0) s cnf 1 |
180 (179+1) |
| fpu-10Xe-correct01-nonuniform-depth-24 | 79 (77+2) s cnf 0 |
78 (76+2) s cnf 0 |
79 (77+2) s cnf 0 |
79 (77+2) s cnf 0 |
78 (76+2) s cnf 0 |
25 (25+0) s cnf 0 |
53 (51+2) |
| DW-unsat-19-42-1 | 800 (784+16) | 800 (788+12) | 800 (782+18) | 800 (788+12) | 800 (785+15) | 800 (800+0) | 43 (42+2) |
| fpu-10Xh-correct04-nonuniform-depth-27 | 99 (96+3) s cnf 0 |
99 (96+3) s cnf 0 |
99 (96+3) s cnf 0 |
99 (96+3) s cnf 0 |
98 (96+3) s cnf 0 |
33 (33+0) s cnf 0 |
61 (59+2) |
| CM-unsat-17-01-05-3 | 800 (779+21) | 800 (777+23) | 800 (781+19) | 800 (774+26) | 800 (782+18) | 800 (799+1) | 76 (74+2) |
| DW-unsat-19-43-1 | 800 (783+17) | 800 (784+16) | 800 (785+15) | 800 (786+14) | 800 (785+15) | 800 (800+1) | 45 (43+2) |
| ev-pr-6x6-9-5-0-1-2-s | 800 (779+21) | 800 (783+17) | 800 (772+28) | 800 (764+36) | 800 (777+23) | 800 (799+1) | 66 (64+2) |
| DW-sat-19-44-1 | 800 (782+18) | 800 (786+14) | 800 (782+18) | 800 (785+16) | 800 (782+18) | 154 (154+0) s cnf 1 |
46 (45+2) |
| DW-sat-19-45-1 | 800 (783+17) | 800 (783+17) | 800 (785+15) | 800 (784+16) | 800 (784+16) | 138 (138+0) s cnf 1 |
48 (47+2) |
| DW-unsat-20-44-1 | 800 (783+17) | 800 (783+17) | 800 (784+16) | 800 (782+18) | 800 (784+16) | 800 (800+0) | 50 (48+2) |
| CM-unsat-18-01-05-3 | 800 (775+25) | 800 (777+23) | 800 (778+23) | 800 (776+25) | 800 (778+22) | 800 (799+1) | 87 (85+2) |
| DW-sat-19-46-1 | 800 (782+18) | 800 (781+19) | 800 (783+17) | 800 (780+20) | 800 (783+17) | 171 (171+0) s cnf 1 |
50 (49+2) |
| CM-sat-17-01-06-3 | 800 (782+18) | 800 (781+19) | 800 (782+18) | 800 (779+21) | 800 (783+18) | 199 (198+1) s cnf 1 |
95 (93+2) |
| ev-pr-6x6-11-5-0-1-2-s | 800 (783+17) | 800 (788+12) | 800 (764+36) | 800 (762+38) | 800 (779+21) | 106 (105+1) | 56 (54+2) |
| c1_Debug_s5_f1_e1_v2 | 800 (796+4) | 800 (796+4) | 800 (795+5) | 800 (796+5) | 800 (796+4) | 149 (148+1) | 69 (67+2) |
| c2_Debug_s3_f1_e1_v2 | 800 (792+8) | 800 (792+8) | 465 (459+7) | 800 (792+8) | 800 (792+8) | 800 (799+1) | 78 (76+2) |
| CM-sat-17-01-07-3 | 800 (778+22) | 800 (776+24) | 673 (659+15) | 800 (774+26) | 800 (779+21) | 800 (799+1) | 113 (111+2) |
| ev-pr-6x6-13-5-0-1-2-s | 800 (775+25) | 800 (784+16) | 800 (767+33) | 800 (763+37) | 800 (778+22) | 145 (144+1) | 66 (64+2) |
| c4_Debug_s3_f2_e2_v2 | 334 (328+6) | 334 (328+6) | 238 (234+4) | 334 (328+6) | 333 (328+6) | 800 (799+1) | 65 (63+2) |
| c4_Debug_s5_f2_e2_v1 | 800 (796+4) | 800 (796+4) | 800 (796+4) | 800 (796+5) | 800 (796+4) | 209 (208+1) | 95 (93+2) |
| c2_BMC_p1_k2048 | 142 (139+3) s cnf 1 |
142 (139+3) s cnf 1 |
142 (138+3) s cnf 1 |
142 (139+3) s cnf 1 |
141 (138+3) s cnf 1 |
29 (28+1) | 117 (115+3) |
| ev-pr-6x6-17-5-0-1-2-s | 800 (771+29) | 800 (772+28) | 800 (772+28) | 800 (771+29) | 800 (774+26) | 242 (241+1) | 87 (85+2) |
| SR-unsat-04-01-07-2 | 800 (780+20) | 800 (784+16) | 800 (779+21) | 800 (786+15) | 800 (781+19) | 800 (799+1) | 114 (112+2) |
| SR-sat-04-01-08-2 | 800 (775+25) | 800 (775+25) | 679 (661+19) | 800 (775+25) | 800 (776+24) | 800 (799+1) | 134 (132+2) |
| dungeon_i25-m12-u3-v0.pddl_planlen=165 | 800 (796+4) | 800 (796+4) | 800 (796+4) | 800 (796+4) | 800 (796+4) | 800 (799+1) | 97 (94+3) |
| dungeon_i25-m12-u3-v0.pddl_planlen=190 | 800 (796+4) | 800 (796+4) | 800 (796+4) | 800 (796+4) | 800 (796+4) | 646 (645+1) | 112 (109+3) |
| CM-sat-17-01-06-4 | 217 (215+2) | 216 (214+2) | 216 (214+2) | 216 (214+2) | 216 (214+2) | 472 (471+1) | 228 (225+3) |
| vonNeumann-ripple-carry-12-c | 489 (485+4) s cnf 0 |
494 (490+4) s cnf 0 |
494 (489+5) s cnf 0 |
494 (490+4) s cnf 0 |
490 (486+4) s cnf 0 |
539 (538+0) s cnf 0 |
112 (109+3) |
| pipesnotankage14_10 | 213 (208+5) | 213 (208+5) | 213 (208+5) | 213 (208+5) | 213 (208+5) | 576 (575+1) | 134 (131+3) |
| p20-20.pddl_planlen=23 | 157 (154+3) | 156 (153+3) | 156 (153+3) | 156 (153+3) | 156 (153+3) | 800 (800+1) | 156 (153+3) |
| SR-sat-03-01-07-3 | 255 (252+3) | 255 (252+3) | 254 (252+3) | 254 (252+3) | 255 (252+2) | 236 (235+1) | 254 (251+2) |
| pipesnotankage18_8 | 231 (228+4) | 231 (228+4) | 231 (228+4) | 232 (228+4) | 230 (227+3) | 800 (800+0) | 232 (228+4) |
| c3_Debug_s3_f2_e2_v2 | 80 (78+2) | 80 (78+2) | 79 (78+2) | 80 (78+2) | 80 (78+2) | 800 (799+1) | 79 (78+2) |
| TOTAL (320) | solved:111 wins:63 |
solved:111 wins:62 |
solved:110 wins:56 |
solved:105 wins:67 |
solved:104 wins:60 |
solved:103 wins:63 |
solved:75 wins:11 |
| qfun-64 | qfun-128 | qfun-16 | rareqs | qfun-64-f | quabs | ghostq |