Problem Mneimneh-Sakallah_gq.ts Mneimneh-Sakallah_gqc.ts Mneimneh-Sakallah_nq72.ts Mneimneh-Sakallah_quantor.ts Mneimneh-Sakallah_rareqsuuh3pb.ts Mneimneh-Sakallah_znenofex.ts
s1196_d2_s.qdimacs.gz 1 (1+0)
s cnf 1 (s cnf 1)
1 (1+0)
s cnf 1 (s cnf 1)
0 (0+0)
s cnf 1 (s cnf 1)
305 (300+5) 0 (0+0)
s cnf 1 (s cnf 1)
122 (121+1)
s cnf 1 (s cnf 1 1956 3511)
s1196_d3_u.qdimacs.gz 65 (65+0)
s cnf 0 (s cnf 0)
115 (115+0)
s cnf 0 (s cnf 0)
800 (800+0) 800 (793+7) 408 (333+75)
s cnf 0 (s cnf 0)
437 (433+4)
s1196_d4_u.qcnf.gz 93 (93+0)
s cnf 0 (s cnf 0)
165 (164+0)
s cnf 0 (s cnf 0)
800 (800+0) 307 (304+3) 800 (652+148) 800 (800+0)
s1196_d5_u.qcnf.gz 124 (123+1)
s cnf 0 (s cnf 0)
209 (209+1)
s cnf 0 (s cnf 0)
800 (800+0) 131 (129+2) 800 (573+227) 800 (800+0)
s1196_d6_u.qcnf.gz 160 (159+1)
s cnf 0 (s cnf 0)
258 (258+1)
s cnf 0 (s cnf 0)
800 (800+0) 21 (19+2) 800 (611+189) 800 (800+0)
s1196_d7_u.qcnf.gz 206 (205+1)
s cnf 0 (s cnf 0)
299 (298+1)
s cnf 0 (s cnf 0)
800 (800+0) 631 (625+6) 800 (566+234) 363 (361+2)
s1269_d10_s.qdimacs.gz 800 (797+3) 800 (798+2) 800 (800+0) 35 (33+2) 800 (799+1) 800 (800+0)
s1269_d11_u.qdimacs.gz 800 (797+3) 800 (798+2) 800 (800+0) 25 (23+2) 800 (799+1) 800 (800+0)
s1269_d12_u.qcnf.gz 800 (797+3) 800 (798+2) 800 (799+1) 19 (17+2) 800 (799+1) 800 (800+0)
s1269_d13_u.qcnf.gz 800 (798+2) 800 (799+1) 800 (799+1) 30 (28+2) 800 (799+1) 800 (800+0)
s1269_d14_u.qcnf.gz 800 (798+2) 800 (799+1) 800 (800+0) 72 (70+2) 800 (799+1) 800 (800+0)
s1269_d15_u.qcnf.gz 800 (799+1) 800 (799+1) 800 (799+1) 24 (22+2) 800 (799+1) 800 (800+0)
s1269_d2_s.qdimacs.gz 1 (1+0)
s cnf 1 (s cnf 1)
2 (2+0)
s cnf 1 (s cnf 1)
0 (0+0)
s cnf 1 (s cnf 1)
800 (793+7) 0 (0+0)
s cnf 1 (s cnf 1)
18 (18+0)
s cnf 1 (s cnf 1 1839 3477)
s1269_d3_s.qcnf.gz 3 (3+0)
s cnf 1 (s cnf 1)
4 (4+0)
s cnf 1 (s cnf 1)
5 (5+0)
s cnf 1 (s cnf 1)
469 (466+3) 9 (8+0)
s cnf 1 (s cnf 1)
257 (254+3)
s1269_d4_s.qdimacs.gz 7 (6+0)
s cnf 1 (s cnf 1)
7 (7+0)
s cnf 1 (s cnf 1)
800 (799+1) 71 (69+2) 800 (688+112) 800 (800+0)
s1269_d5_s.qcnf.gz 11 (11+0)
s cnf 1 (s cnf 1)
13 (13+0)
s cnf 1 (s cnf 1)
800 (800+1) 800 (793+7) 59 (59+0)
s cnf 1 (s cnf 1)
367 (365+3)
s1269_d6_s.qcnf.gz 17 (17+0)
s cnf 1 (s cnf 1)
19 (18+0)
s cnf 1 (s cnf 1)
800 (800+0) 34 (32+2) 800 (628+172) 800 (800+0)
s1269_d7_s.qcnf.gz 24 (24+0)
s cnf 1 (s cnf 1)
26 (26+0)
s cnf 1 (s cnf 1)
800 (800+0) 34 (32+2) 800 (675+125) 800 (800+0)
s1269_d8_s.qdimacs.gz 33 (33+0)
s cnf 1 (s cnf 1)
37 (37+0)
s cnf 1 (s cnf 1)
800 (799+1) 46 (43+2) 800 (713+87) 800 (800+0)
s1269_d9_s.qcnf.gz 422 (421+1)
s cnf 1 (s cnf 1)
800 (799+1) 800 (800+0) 20 (17+3) 800 (751+49) 800 (800+0)
s298_d10_s.qcnf.gz 4 (4+0)
s cnf 1 (s cnf 1)
5 (5+0)
s cnf 1 (s cnf 1)
7 (7+0)
s cnf 1 (s cnf 1)
800 (794+6) 4 (4+0)
s cnf 1 (s cnf 1)
253 (251+2)
s298_d11_s.qcnf.gz 5 (5+0)
s cnf 1 (s cnf 1)
5 (5+0)
s cnf 1 (s cnf 1)
26 (26+0)
s cnf 1 (s cnf 1)
472 (468+4) 4 (4+0)
s cnf 1 (s cnf 1)
509 (503+6)
s298_d12_s.qcnf.gz 5 (5+0)
s cnf 1 (s cnf 1)
6 (6+0)
s cnf 1 (s cnf 1)
45 (45+0)
s cnf 1 (s cnf 1)
415 (412+4) 6 (6+0)
s cnf 1 (s cnf 1)
800 (796+4)
s298_d13_s.qcnf.gz 6 (6+0)
s cnf 1 (s cnf 1)
8 (7+0)
s cnf 1 (s cnf 1)
80 (80+0)
s cnf 1 (s cnf 1)
800 (792+9) 11 (11+0)
s cnf 1 (s cnf 1)
252 (251+2)
s298_d14_s.qcnf.gz 8 (8+0)
s cnf 1 (s cnf 1)
13 (13+0)
s cnf 1 (s cnf 1)
11 (10+0)
s cnf 1 (s cnf 1)
800 (791+9) 11 (11+0)
s cnf 1 (s cnf 1)
800 (800+0)
s298_d15_s.qcnf.gz 8 (8+0)
s cnf 1 (s cnf 1)
10 (10+0)
s cnf 1 (s cnf 1)
126 (126+0)
s cnf 1 (s cnf 1)
800 (793+7) 17 (16+0)
s cnf 1 (s cnf 1)
440 (438+2)
s298_d16_s.qdimacs.gz 9 (9+0)
s cnf 1 (s cnf 1)
11 (11+0)
s cnf 1 (s cnf 1)
135 (135+0)
s cnf 1 (s cnf 1)
181 (179+2) 28 (28+0)
s cnf 1 (s cnf 1)
800 (799+1)
s298_d17_s.qcnf.gz 13 (13+0)
s cnf 1 (s cnf 1)
16 (16+0)
s cnf 1 (s cnf 1)
105 (105+0)
s cnf 1 (s cnf 1)
195 (193+2) 23 (23+0)
s cnf 1 (s cnf 1)
800 (800+0)
s298_d18_s.qdimacs.gz 14 (14+0)
s cnf 1 (s cnf 1)
15 (15+0)
s cnf 1 (s cnf 1)
414 (414+0)
s cnf 1 (s cnf 1)
106 (104+2) 53 (52+1)
s cnf 1 (s cnf 1)
800 (799+1)
s298_d19_u.qdimacs.gz 18 (18+0)
s cnf 0 (s cnf 0)
26 (26+0)
s cnf 0 (s cnf 0)
339 (339+0)
s cnf 0 (s cnf 0)
48 (46+2) 40 (39+1)
s cnf 0 (s cnf 0)
800 (800+0)
s298_d20_u.qcnf.gz 20 (20+0)
s cnf 0 (s cnf 0)
36 (36+0)
s cnf 0 (s cnf 0)
536 (536+0)
s cnf 0 (s cnf 0)
643 (641+2) 111 (110+1)
s cnf 0 (s cnf 0)
800 (800+0)
s298_d21_u.qcnf.gz 22 (22+0)
s cnf 0 (s cnf 0)
35 (35+0)
s cnf 0 (s cnf 0)
608 (607+0)
s cnf 0 (s cnf 0)
29 (27+2) 61 (60+1)
s cnf 0 (s cnf 0)
800 (800+0)
s298_d22_u.qcnf.gz 24 (23+0)
s cnf 0 (s cnf 0)
36 (36+0)
s cnf 0 (s cnf 0)
406 (405+0)
s cnf 0 (s cnf 0)
41 (38+2) 85 (84+1)
s cnf 0 (s cnf 0)
800 (800+0)
s298_d23_u.qcnf.gz 25 (25+0)
s cnf 0 (s cnf 0)
41 (40+0)
s cnf 0 (s cnf 0)
491 (491+0)
s cnf 0 (s cnf 0)
102 (99+2) 201 (199+2)
s cnf 0 (s cnf 0)
800 (800+0)
s298_d24_u.qcnf.gz 28 (28+0)
s cnf 0 (s cnf 0)
48 (48+0)
s cnf 0 (s cnf 0)
800 (800+0) 97 (95+2) 522 (519+3)
s cnf 0 (s cnf 0)
800 (800+0)
s298_d25_u.qcnf.gz 30 (30+0)
s cnf 0 (s cnf 0)
48 (48+0)
s cnf 0 (s cnf 0)
800 (800+0) 18 (15+2) 240 (239+2)
s cnf 0 (s cnf 0)
800 (800+0)
s298_d5_s.qcnf.gz 1 (1+0)
s cnf 1 (s cnf 1)
1 (1+0)
s cnf 1 (s cnf 1)
0 (0+0)
s cnf 1 (s cnf 1)
157 (157+1)
s cnf 1 (s TRUE)
0 (0+0)
s cnf 1 (s cnf 1)
12 (12+0)
s cnf 1 (s cnf 1 1605 2752)
s298_d6_s.qcnf.gz 2 (2+0)
s cnf 1 (s cnf 1)
2 (2+0)
s cnf 1 (s cnf 1)
0 (0+0)
s cnf 1 (s cnf 1)
800 (796+5) 1 (1+0)
s cnf 1 (s cnf 1)
17 (17+0)
s cnf 1 (s cnf 1 2187 3762)
s298_d7_s.qcnf.gz 2 (2+0)
s cnf 1 (s cnf 1)
2 (2+0)
s cnf 1 (s cnf 1)
0 (0+0)
s cnf 1 (s cnf 1)
800 (797+3) 1 (1+0)
s cnf 1 (s cnf 1)
32 (32+0)
s cnf 1 (s cnf 1 2063 3576)
s298_d8_s.qdimacs.gz 3 (3+0)
s cnf 1 (s cnf 1)
3 (3+0)
s cnf 1 (s cnf 1)
3 (3+0)
s cnf 1 (s cnf 1)
340 (337+3) 1 (1+0)
s cnf 1 (s cnf 1)
800 (800+0)
s298_d9_s.qcnf.gz 4 (4+0)
s cnf 1 (s cnf 1)
4 (4+0)
s cnf 1 (s cnf 1)
11 (11+0)
s cnf 1 (s cnf 1)
800 (794+6) 3 (3+0)
s cnf 1 (s cnf 1)
46 (46+0)
s cnf 1 (s cnf 1 3632 6500)
s3330_d10_u.qdimacs.gz 800 (799+1) 800 (799+1) 800 (800+0) 29 (26+2) 800 (799+1) 800 (800+0)
s3330_d11_u.qcnf.gz 800 (799+1) 800 (799+1) 800 (800+0) 19 (17+2) 800 (799+1) 800 (800+0)
s3330_d12_u.qcnf.gz 800 (799+1) 800 (799+1) 800 (800+0) 36 (33+2) 800 (799+1) 800 (800+0)
s3330_d13_u.qcnf.gz 800 (799+1) 800 (800+0) 800 (800+0) 18 (16+2) 800 (799+1) 800 (800+0)
s3330_d14_u.qcnf.gz 800 (799+1) 800 (799+1) 800 (800+0) 29 (27+2) 800 (799+1) 800 (800+0)
s3330_d2_s.qdimacs.gz 7 (7+0)
s cnf 1 (s cnf 1)
7 (7+0)
s cnf 1 (s cnf 1)
0 (0+0)
s cnf 1 (s cnf 1)
0 (0+0)
s cnf 1 (s SATISFIABLE)
0 (0+0)
s cnf 1 (s cnf 1)
0 (0+0)
s cnf 1 (s cnf 1 52 105)
s3330_d3_s.qcnf.gz 23 (23+0)
s cnf 1 (s cnf 1)
24 (24+0)
s cnf 1 (s cnf 1)
13 (13+0)
s cnf 1 (s cnf 1)
310 (307+2) 30 (29+0)
s cnf 1 (s cnf 1)
800 (800+0)
s3330_d4_s.qdimacs.gz 48 (48+0)
s cnf 1 (s cnf 1)
57 (57+0)
s cnf 1 (s cnf 1)
800 (800+0) 50 (48+3) 109 (109+1)
s cnf 1 (s cnf 1)
385 (382+3)
s3330_d5_s.qcnf.gz 80 (80+0)
s cnf 1 (s cnf 1)
88 (87+0)
s cnf 1 (s cnf 1)
800 (800+0) 206 (204+2) 320 (319+1)
s cnf 1 (s cnf 1)
800 (800+0)
s3330_d6_s.qcnf.gz 235 (235+1)
s cnf 1 (s cnf 1)
205 (205+1)
s cnf 1 (s cnf 1)
800 (800+0) 23 (21+2) 800 (799+1) 800 (800+0)
s3330_d7_s.qcnf.gz 800 (799+1) 677 (676+1)
s cnf 1 (s cnf 1)
800 (800+0) 23 (21+2) 800 (799+1) 800 (800+0)
s3330_d8_s.qdimacs.gz 800 (799+1) 800 (799+1) 800 (800+0) 32 (30+2) 800 (799+1) 800 (800+0)
s3330_d9_s.qdimacs.gz 800 (799+2) 800 (799+1) 800 (800+0) 18 (15+2) 800 (799+1) 800 (800+0)
s386_d10_u.qcnf.gz 6 (6+0)
s cnf 0 (s cnf 0)
8 (8+0)
s cnf 0 (s cnf 0)
17 (17+0)
s cnf 0 (s cnf 0)
66 (63+2) 10 (10+0)
s cnf 0 (s cnf 0)
800 (800+0)
s386_d11_u.qcnf.gz 8 (7+0)
s cnf 0 (s cnf 0)
10 (10+0)
s cnf 0 (s cnf 0)
19 (19+0)
s cnf 0 (s cnf 0)
240 (237+2) 12 (12+0)
s cnf 0 (s cnf 0)
800 (800+0)
s386_d12_u.qcnf.gz 9 (9+0)
s cnf 0 (s cnf 0)
11 (11+0)
s cnf 0 (s cnf 0)
29 (29+0)
s cnf 0 (s cnf 0)
53 (51+2) 14 (14+0)
s cnf 0 (s cnf 0)
800 (799+1)
s386_d4_s.qdimacs.gz 1 (1+0)
s cnf 1 (s cnf 1)
1 (1+0)
s cnf 1 (s cnf 1)
1 (1+0)
s cnf 1 (s cnf 1)
288 (285+3) 0 (0+0)
s cnf 1 (s cnf 1)
16 (16+0)
s cnf 1 (s cnf 1 1741 3043)
s386_d5_s.qcnf.gz 2 (2+0)
s cnf 1 (s cnf 1)
2 (2+0)
s cnf 1 (s cnf 1)
1 (1+0)
s cnf 1 (s cnf 1)
160 (157+3) 1 (1+0)
s cnf 1 (s cnf 1)
390 (387+3)
s386_d6_s.qcnf.gz 3 (3+0)
s cnf 1 (s cnf 1)
3 (3+0)
s cnf 1 (s cnf 1)
2 (2+0)
s cnf 1 (s cnf 1)
204 (202+2) 1 (1+0)
s cnf 1 (s cnf 1)
538 (535+3)
s386_d7_s.qdimacs.gz 3 (3+0)
s cnf 1 (s cnf 1)
4 (3+0)
s cnf 1 (s cnf 1)
4 (4+0)
s cnf 1 (s cnf 1)
214 (210+4) 2 (2+0)
s cnf 1 (s cnf 1)
242 (240+2)
s386_d8_u.qdimacs.gz 4 (4+0)
s cnf 0 (s cnf 0)
4 (4+0)
s cnf 0 (s cnf 0)
8 (8+0)
s cnf 0 (s cnf 0)
283 (280+3) 2 (2+0)
s cnf 0 (s cnf 0)
800 (800+0)
s386_d9_u.qcnf.gz 5 (5+0)
s cnf 0 (s cnf 0)
7 (6+0)
s cnf 0 (s cnf 0)
15 (15+0)
s cnf 0 (s cnf 0)
144 (142+2) 8 (8+0)
s cnf 0 (s cnf 0)
800 (800+0)
s499_d10_s.qcnf.gz 6 (6+0)
s cnf 1 (s cnf 1)
7 (6+0)
s cnf 1 (s cnf 1)
34 (34+0)
s cnf 1 (s cnf 1)
115 (112+2) 7 (7+0)
s cnf 1 (s cnf 1)
800 (800+0)
s499_d11_s.qcnf.gz 7 (7+0)
s cnf 1 (s cnf 1)
8 (8+0)
s cnf 1 (s cnf 1)
21 (21+0)
s cnf 1 (s cnf 1)
163 (160+3) 7 (7+0)
s cnf 1 (s cnf 1)
800 (800+0)
s499_d12_s.qcnf.gz 9 (8+0)
s cnf 1 (s cnf 1)
9 (9+0)
s cnf 1 (s cnf 1)
28 (28+0)
s cnf 1 (s cnf 1)
677 (673+4) 10 (10+0)
s cnf 1 (s cnf 1)
61 (61+0)
s cnf 1 (s cnf 1 6316 11737)
s499_d13_s.qcnf.gz 12 (11+0)
s cnf 1 (s cnf 1)
13 (12+0)
s cnf 1 (s cnf 1)
15 (15+0)
s cnf 1 (s cnf 1)
80 (78+2) 16 (16+0)
s cnf 1 (s cnf 1)
800 (800+0)
s499_d14_s.qcnf.gz 14 (13+0)
s cnf 1 (s cnf 1)
15 (15+0)
s cnf 1 (s cnf 1)
17 (17+0)
s cnf 1 (s cnf 1)
73 (70+2) 26 (26+0)
s cnf 1 (s cnf 1)
800 (800+0)
s499_d15_s.qcnf.gz 15 (15+0)
s cnf 1 (s cnf 1)
16 (16+0)
s cnf 1 (s cnf 1)
25 (25+0)
s cnf 1 (s cnf 1)
86 (83+3) 33 (33+0)
s cnf 1 (s cnf 1)
800 (800+0)
s499_d16_s.qdimacs.gz 18 (17+0)
s cnf 1 (s cnf 1)
18 (18+0)
s cnf 1 (s cnf 1)
103 (103+0)
s cnf 1 (s cnf 1)
800 (794+6) 43 (43+0)
s cnf 1 (s cnf 1)
108 (108+0)
s cnf 1 (s cnf 1 9652 18278)
s499_d17_s.qcnf.gz 20 (19+0)
s cnf 1 (s cnf 1)
21 (21+0)
s cnf 1 (s cnf 1)
147 (147+0)
s cnf 1 (s cnf 1)
98 (96+2) 48 (48+0)
s cnf 1 (s cnf 1)
800 (800+0)
s499_d18_s.qcnf.gz 22 (22+0)
s cnf 1 (s cnf 1)
24 (24+0)
s cnf 1 (s cnf 1)
172 (172+0)
s cnf 1 (s cnf 1)
800 (795+5) 68 (68+0)
s cnf 1 (s cnf 1)
481 (479+2)
s499_d19_s.qcnf.gz 24 (24+0)
s cnf 1 (s cnf 1)
25 (25+0)
s cnf 1 (s cnf 1)
344 (344+0)
s cnf 1 (s cnf 1)
193 (190+3) 80 (79+0)
s cnf 1 (s cnf 1)
800 (800+0)
s499_d20_s.qcnf.gz 26 (25+0)
s cnf 1 (s cnf 1)
27 (27+0)
s cnf 1 (s cnf 1)
164 (164+0)
s cnf 1 (s cnf 1)
522 (517+4) 94 (93+0)
s cnf 1 (s cnf 1)
157 (156+0)
s cnf 1 (s cnf 1 11808 22934)
s499_d21_s.qdimacs.gz 33 (32+0)
s cnf 1 (s cnf 1)
31 (31+0)
s cnf 1 (s cnf 1)
569 (568+1)
s cnf 1 (s cnf 1)
35 (33+2) 288 (287+1)
s cnf 1 (s cnf 1)
800 (799+1)
s499_d22_u.qdimacs.gz 35 (34+0)
s cnf 0 (s cnf 0)
36 (36+0)
s cnf 0 (s cnf 0)
660 (660+1)
s cnf 0 (s cnf 0)
285 (282+3) 160 (159+1)
s cnf 0 (s cnf 0)
800 (800+0)
s499_d23_u.qcnf.gz 39 (39+0)
s cnf 0 (s cnf 0)
42 (41+0)
s cnf 0 (s cnf 0)
800 (799+1) 47 (45+2) 346 (345+1)
s cnf 0 (s cnf 0)
800 (799+1)
s499_d24_u.qcnf.gz 41 (41+0)
s cnf 0 (s cnf 0)
44 (44+0)
s cnf 0 (s cnf 0)
800 (799+1) 25 (23+2) 272 (271+1)
s cnf 0 (s cnf 0)
800 (800+0)
s499_d25_u.qcnf.gz 46 (45+0)
s cnf 0 (s cnf 0)
52 (52+1)
s cnf 0 (s cnf 0)
800 (799+1) 65 (63+2) 654 (652+2)
s cnf 0 (s cnf 0)
800 (800+0)
s499_d26_u.qcnf.gz 48 (48+0)
s cnf 0 (s cnf 0)
51 (51+1)
s cnf 0 (s cnf 0)
800 (799+1) 40 (38+2) 348 (347+1)
s cnf 0 (s cnf 0)
800 (800+0)
s499_d4_s.qdimacs.gz 1 (1+0)
s cnf 1 (s cnf 1)
1 (1+0)
s cnf 1 (s cnf 1)
0 (0+0)
s cnf 1 (s cnf 1)
19 (18+0)
s cnf 1 (s TRUE)
0 (0+0)
s cnf 1 (s cnf 1)
14 (14+0)
s cnf 1 (s cnf 1 1758 3036)
s499_d5_s.qcnf.gz 2 (2+0)
s cnf 1 (s cnf 1)
2 (2+0)
s cnf 1 (s cnf 1)
1 (1+0)
s cnf 1 (s cnf 1)
800 (798+2) 1 (1+0)
s cnf 1 (s cnf 1)
731 (730+1)
s cnf 1 (s cnf 1 2105 3710)
s499_d6_s.qcnf.gz 3 (3+0)
s cnf 1 (s cnf 1)
3 (3+0)
s cnf 1 (s cnf 1)
1 (1+0)
s cnf 1 (s cnf 1)
800 (793+7) 1 (1+0)
s cnf 1 (s cnf 1)
19 (19+0)
s cnf 1 (s cnf 1 2318 4163)
s499_d7_s.qcnf.gz 3 (3+0)
s cnf 1 (s cnf 1)
4 (3+0)
s cnf 1 (s cnf 1)
3 (3+0)
s cnf 1 (s cnf 1)
401 (398+3) 2 (2+0)
s cnf 1 (s cnf 1)
800 (800+0)
s499_d8_s.qdimacs.gz 4 (4+0)
s cnf 1 (s cnf 1)
4 (4+0)
s cnf 1 (s cnf 1)
5 (5+0)
s cnf 1 (s cnf 1)
800 (797+3) 3 (3+0)
s cnf 1 (s cnf 1)
800 (800+0)
s499_d9_s.qcnf.gz 5 (5+0)
s cnf 1 (s cnf 1)
5 (5+0)
s cnf 1 (s cnf 1)
9 (9+0)
s cnf 1 (s cnf 1)
800 (797+4) 3 (3+0)
s cnf 1 (s cnf 1)
42 (42+0)
s cnf 1 (s cnf 1 4388 7951)
s510_d10_s.qcnf.gz 11 (10+0)
s cnf 1 (s cnf 1)
11 (11+0)
s cnf 1 (s cnf 1)
26 (26+0)
s cnf 1 (s cnf 1)
132 (130+2) 9 (9+0)
s cnf 1 (s cnf 1)
800 (800+0)
s510_d11_s.qcnf.gz 13 (13+0)
s cnf 1 (s cnf 1)
14 (14+0)
s cnf 1 (s cnf 1)
30 (30+0)
s cnf 1 (s cnf 1)
556 (553+3) 11 (11+0)
s cnf 1 (s cnf 1)
800 (800+0)
s510_d12_s.qcnf.gz 15 (15+0)
s cnf 1 (s cnf 1)
16 (16+0)
s cnf 1 (s cnf 1)
58 (58+0)
s cnf 1 (s cnf 1)
184 (181+3) 16 (16+0)
s cnf 1 (s cnf 1)
800 (800+0)
s510_d13_s.qcnf.gz 18 (18+0)
s cnf 1 (s cnf 1)
20 (19+0)
s cnf 1 (s cnf 1)
78 (78+0)
s cnf 1 (s cnf 1)
39 (37+2) 94 (93+0)
s cnf 1 (s cnf 1)
800 (800+0)
s510_d14_s.qcnf.gz 21 (21+0)
s cnf 1 (s cnf 1)
23 (23+0)
s cnf 1 (s cnf 1)
324 (324+0)
s cnf 1 (s cnf 1)
22 (19+2) 139 (138+1)
s cnf 1 (s cnf 1)
800 (800+0)
s510_d15_s.qcnf.gz 26 (25+0)
s cnf 1 (s cnf 1)
27 (27+0)
s cnf 1 (s cnf 1)
800 (800+0) 122 (120+2) 59 (59+0)
s cnf 1 (s cnf 1)
800 (800+0)
s510_d16_s.qdimacs.gz 30 (30+0)
s cnf 1 (s cnf 1)
33 (32+0)
s cnf 1 (s cnf 1)
621 (621+0)
s cnf 1 (s cnf 1)
263 (260+2) 56 (56+0)
s cnf 1 (s cnf 1)
800 (800+0)
s510_d17_s.qcnf.gz 33 (33+0)
s cnf 1 (s cnf 1)
38 (37+0)
s cnf 1 (s cnf 1)
800 (800+0) 28 (26+2) 267 (266+1)
s cnf 1 (s cnf 1)
800 (800+0)
s510_d18_s.qcnf.gz 39 (39+0)
s cnf 1 (s cnf 1)
42 (41+0)
s cnf 1 (s cnf 1)
718 (718+0)
s cnf 1 (s cnf 1)
800 (797+3) 85 (85+0)
s cnf 1 (s cnf 1)
446 (444+2)
s510_d19_s.qcnf.gz 45 (45+0)
s cnf 1 (s cnf 1)
45 (45+0)
s cnf 1 (s cnf 1)
800 (800+0) 28 (26+2) 800 (798+2) 800 (800+0)
s510_d20_s.qcnf.gz 47 (47+0)
s cnf 1 (s cnf 1)
52 (51+0)
s cnf 1 (s cnf 1)
800 (800+0) 174 (171+2) 247 (246+1)
s cnf 1 (s cnf 1)
800 (800+0)
s510_d21_s.qcnf.gz 58 (57+1)
s cnf 1 (s cnf 1)
56 (56+0)
s cnf 1 (s cnf 1)
800 (800+0) 27 (24+2) 800 (798+2) 800 (800+0)
s510_d22_s.qcnf.gz 68 (67+1)
s cnf 1 (s cnf 1)
64 (64+0)
s cnf 1 (s cnf 1)
800 (800+0) 28 (26+2) 735 (734+2)
s cnf 1 (s cnf 1)
800 (800+0)
s510_d23_s.qcnf.gz 66 (66+1)
s cnf 1 (s cnf 1)
79 (78+1)
s cnf 1 (s cnf 1)
0 (0+0) 44 (41+2) 630 (629+1)
s cnf 1 (s cnf 1)
800 (800+0)
s510_d24_s.qcnf.gz 81 (80+1)
s cnf 1 (s cnf 1)
82 (81+1)
s cnf 1 (s cnf 1)
800 (800+0) 800 (798+2) 229 (228+1)
s cnf 1 (s cnf 1)
429 (427+2)
s510_d25_s.qcnf.gz 86 (86+1)
s cnf 1 (s cnf 1)
88 (87+1)
s cnf 1 (s cnf 1)
800 (800+0) 25 (23+2) 800 (798+2) 800 (800+0)
s510_d26_s.qcnf.gz 96 (95+1)
s cnf 1 (s cnf 1)
131 (130+1)
s cnf 1 (s cnf 1)
800 (800+0) 25 (22+2) 800 (799+1) 800 (800+0)
s510_d27_s.qcnf.gz 109 (109+1)
s cnf 1 (s cnf 1)
127 (126+1)
s cnf 1 (s cnf 1)
800 (800+0) 99 (97+2) 800 (799+1) 800 (800+0)
s510_d28_s.qcnf.gz 118 (118+1)
s cnf 1 (s cnf 1)
134 (133+1)
s cnf 1 (s cnf 1)
800 (800+0) 26 (24+2) 800 (799+1) 800 (800+0)
s510_d29_s.qcnf.gz 140 (139+1)
s cnf 1 (s cnf 1)
142 (142+1)
s cnf 1 (s cnf 1)
800 (800+0) 28 (26+2) 800 (799+1) 800 (800+0)
s510_d30_s.qcnf.gz 164 (163+1)
s cnf 1 (s cnf 1)
152 (151+1)
s cnf 1 (s cnf 1)
800 (800+0) 18 (16+2) 800 (799+1) 800 (800+0)
s510_d31_s.qcnf.gz 170 (169+1)
s cnf 1 (s cnf 1)
190 (189+1)
s cnf 1 (s cnf 1)
800 (799+1) 23 (20+2) 800 (799+2) 800 (800+0)
s510_d32_s.qdimacs.gz 168 (167+1)
s cnf 1 (s cnf 1)
223 (221+1)
s cnf 1 (s cnf 1)
800 (799+1) 19 (17+2) 800 (799+1) 800 (800+0)
s510_d33_s.qcnf.gz 197 (196+1)
s cnf 1 (s cnf 1)
239 (238+1)
s cnf 1 (s cnf 1)
800 (800+0) 23 (20+2) 800 (799+1) 800 (800+0)
s510_d34_s.qcnf.gz 183 (182+1)
s cnf 1 (s cnf 1)
212 (211+1)
s cnf 1 (s cnf 1)
800 (799+1) 24 (22+2) 800 (799+1) 800 (800+0)
s510_d35_s.qcnf.gz 221 (220+1)
s cnf 1 (s cnf 1)
215 (214+1)
s cnf 1 (s cnf 1)
800 (800+0) 101 (98+3) 800 (799+1) 800 (800+0)
s510_d36_s.qcnf.gz 247 (246+1)
s cnf 1 (s cnf 1)
252 (250+1)
s cnf 1 (s cnf 1)
800 (800+0) 26 (24+2) 800 (799+1) 800 (800+0)
s510_d37_s.qcnf.gz 325 (323+2)
s cnf 1 (s cnf 1)
339 (337+2)
s cnf 1 (s cnf 1)
800 (800+1) 21 (19+2) 800 (799+1) 800 (800+0)
s510_d38_s.qcnf.gz 309 (308+1)
s cnf 1 (s cnf 1)
378 (376+2)
s cnf 1 (s cnf 1)
800 (799+1) 19 (17+2) 800 (799+1) 800 (800+0)
s510_d39_s.qcnf.gz 364 (362+2)
s cnf 1 (s cnf 1)
399 (397+2)
s cnf 1 (s cnf 1)
800 (800+0) 17 (15+2) 800 (799+1) 800 (800+0)
s510_d3_s.qcnf.gz 1 (1+0)
s cnf 1 (s cnf 1)
1 (1+0)
s cnf 1 (s cnf 1)
0 (0+0)
s cnf 1 (s cnf 1)
72 (69+3) 0 (0+0)
s cnf 1 (s cnf 1)
13 (13+0)
s cnf 1 (s cnf 1 1425 2297)
s510_d40_s.qcnf.gz 384 (382+2)
s cnf 1 (s cnf 1)
351 (349+1)
s cnf 1 (s cnf 1)
800 (800+0) 30 (28+2) 800 (799+1) 800 (800+0)
s510_d41_s.qcnf.gz 357 (355+2)
s cnf 1 (s cnf 1)
452 (449+2)
s cnf 1 (s cnf 1)
800 (800+0) 44 (41+2) 800 (799+1) 800 (800+0)
s510_d42_s.qcnf.gz 426 (425+2)
s cnf 1 (s cnf 1)
395 (393+1)
s cnf 1 (s cnf 1)
800 (800+0) 31 (29+2) 800 (799+1) 800 (800+0)
s510_d43_s.qcnf.gz 433 (431+2)
s cnf 1 (s cnf 1)
455 (452+2)
s cnf 1 (s cnf 1)
800 (800+0) 20 (18+2) 800 (799+1) 800 (800+0)
s510_d44_s.qcnf.gz 485 (483+2)
s cnf 1 (s cnf 1)
524 (519+5) 800 (800+1) 24 (22+2) 800 (799+1) 800 (800+0)
s510_d45_s.qcnf.gz 501 (498+2)
s cnf 1 (s cnf 1)
500 (496+5) 800 (800+0) 17 (15+2) 800 (799+1) 800 (800+0)
s510_d46_s.qdimacs.gz 550 (547+3)
s cnf 1 (s cnf 1)
530 (527+3) 800 (800+0) 20 (18+2) 800 (799+1) 800 (800+0)
s510_d47_u.qdimacs.gz 599 (594+5) 505 (503+2)
s cnf 0 (s cnf 0)
800 (800+1) 23 (21+2) 800 (799+1) 800 (800+0)
s510_d48_u.qcnf.gz 473 (471+2)
s cnf 0 (s cnf 0)
597 (595+3) 800 (800+0) 18 (16+2) 800 (799+1) 800 (800+0)
s510_d49_u.qcnf.gz 557 (555+3)
s cnf 0 (s cnf 0)
609 (607+3) 800 (800+0) 23 (21+2) 800 (799+1) 800 (800+0)
s510_d4_s.qdimacs.gz 2 (2+0)
s cnf 1 (s cnf 1)
2 (2+0)
s cnf 1 (s cnf 1)
0 (0+0)
s cnf 1 (s cnf 1)
800 (792+8) 0 (0+0)
s cnf 1 (s cnf 1)
14 (14+0)
s cnf 1 (s cnf 1 1791 3014)
s510_d50_u.qcnf.gz 608 (605+3)
s cnf 0 (s cnf 0)
634 (631+3) 800 (800+0) 39 (37+2) 800 (799+1) 800 (800+0)
s510_d51_u.qcnf.gz 613 (610+3)
s cnf 0 (s cnf 0)
701 (698+3) 800 (800+0) 30 (28+2) 800 (799+1) 800 (800+0)
s510_d5_s.qcnf.gz 3 (3+0)
s cnf 1 (s cnf 1)
3 (3+0)
s cnf 1 (s cnf 1)
5 (5+0)
s cnf 1 (s cnf 1)
800 (797+4) 3 (3+0)
s cnf 1 (s cnf 1)
800 (800+0)
s510_d6_s.qcnf.gz 3 (3+0)
s cnf 1 (s cnf 1)
4 (4+0)
s cnf 1 (s cnf 1)
2 (2+0)
s cnf 1 (s cnf 1)
87 (85+2) 2 (2+0)
s cnf 1 (s cnf 1)
800 (800+0)
s510_d7_s.qcnf.gz 5 (4+0)
s cnf 1 (s cnf 1)
5 (5+0)
s cnf 1 (s cnf 1)
5 (5+0)
s cnf 1 (s cnf 1)
800 (796+5) 4 (4+0)
s cnf 1 (s cnf 1)
800 (800+0)
s510_d8_s.qdimacs.gz 6 (6+0)
s cnf 1 (s cnf 1)
6 (6+0)
s cnf 1 (s cnf 1)
7 (7+0)
s cnf 1 (s cnf 1)
550 (545+6) 4 (4+0)
s cnf 1 (s cnf 1)
125 (124+1)
s cnf 1 (s cnf 1 5132 8713)
s510_d9_s.qcnf.gz 7 (7+0)
s cnf 1 (s cnf 1)
8 (8+0)
s cnf 1 (s cnf 1)
27 (27+0)
s cnf 1 (s cnf 1)
304 (302+2) 25 (24+0)
s cnf 1 (s cnf 1)
800 (799+1)
s641_d10_u.qcnf.gz 41 (40+0)
s cnf 0 (s cnf 0)
126 (125+1)
s cnf 0 (s cnf 0)
800 (800+0)
s cnf 0 (s cnf 0)
800 (795+5) 91 (81+10)
s cnf 0 (s cnf 0)
800 (800+0)
s641_d11_u.qcnf.gz 48 (48+0)
s cnf 0 (s cnf 0)
177 (175+1)
s cnf 0 (s cnf 0)
773 (773+0)
s cnf 0 (s cnf 0)
42 (40+2) 127 (112+15)
s cnf 0 (s cnf 0)
800 (800+0)
s641_d3_s.qcnf.gz 2 (2+0)
s cnf 1 (s cnf 1)
2 (2+0)
s cnf 1 (s cnf 1)
1 (1+0)
s cnf 1 (s cnf 1)
800 (798+2) 1 (1+0)
s cnf 1 (s cnf 1)
800 (799+1)
s641_d5_s.qcnf.gz 4 (4+0)
s cnf 1 (s cnf 1)
4 (4+0)
s cnf 1 (s cnf 1)
38 (38+0)
s cnf 1 (s cnf 1)
212 (206+6) 3 (3+0)
s cnf 1 (s cnf 1)
51 (51+0)
s cnf 1 (s cnf 1 4958 7459)
s641_d8_u.qcnf.gz 28 (28+0)
s cnf 0 (s cnf 0)
47 (47+0)
s cnf 0 (s cnf 0)
519 (519+0)
s cnf 0 (s cnf 0)
376 (373+3) 77 (70+6)
s cnf 0 (s cnf 0)
800 (800+0)
s641_d9_u.qcnf.gz 34 (34+0)
s cnf 0 (s cnf 0)
92 (91+1)
s cnf 0 (s cnf 0)
650 (650+0)
s cnf 0 (s cnf 0)
800 (795+6) 82 (73+10)
s cnf 0 (s cnf 0)
800 (800+0)
s713_d10_u.qcnf.gz 69 (68+0)
s cnf 0 (s cnf 0)
277 (276+2)
s cnf 0 (s cnf 0)
800 (800+0) 283 (280+3) 343 (262+81)
s cnf 0 (s cnf 0)
621 (619+2)
s713_d11_u.qcnf.gz 80 (79+0)
s cnf 0 (s cnf 0)
331 (327+4) 800 (800+0) 800 (798+2) 364 (271+94)
s cnf 0 (s cnf 0)
293 (291+2)
s713_d3_s.qcnf.gz 2 (2+0)
s cnf 1 (s cnf 1)
2 (2+0)
s cnf 1 (s cnf 1)
1 (1+0)
s cnf 1 (s cnf 1)
800 (797+3) 1 (1+0)
s cnf 1 (s cnf 1)
800 (798+2)
s713_d4_s.qdimacs.gz 3 (3+0)
s cnf 1 (s cnf 1)
3 (3+0)
s cnf 1 (s cnf 1)
1 (1+0)
s cnf 1 (s cnf 1)
137 (133+3) 2 (2+0)
s cnf 1 (s cnf 1)
30 (30+0)
s cnf 1 (s cnf 1 3960 6114)
s713_d5_s.qcnf.gz 5 (4+0)
s cnf 1 (s cnf 1)
5 (5+0)
s cnf 1 (s cnf 1)
27 (27+0)
s cnf 1 (s cnf 1)
800 (797+3) 2 (2+0)
s cnf 1 (s cnf 1)
800 (800+0)
s713_d6_s.qdimacs.gz 7 (7+0)
s cnf 1 (s cnf 1)
8 (8+0)
s cnf 1 (s cnf 1)
44 (44+0)
s cnf 1 (s cnf 1)
131 (129+2) 6 (6+0)
s cnf 1 (s cnf 1)
800 (800+0)
s713_d7_u.qdimacs.gz 37 (37+0)
s cnf 0 (s cnf 0)
95 (94+0)
s cnf 0 (s cnf 0)
599 (599+0)
s cnf 0 (s cnf 0)
376 (373+3) 165 (139+26)
s cnf 0 (s cnf 0)
800 (800+0)
s713_d8_u.qcnf.gz 48 (47+0)
s cnf 0 (s cnf 0)
140 (139+1)
s cnf 0 (s cnf 0)
742 (742+0)
s cnf 0 (s cnf 0)
31 (29+2) 234 (186+47)
s cnf 0 (s cnf 0)
800 (800+0)
s713_d9_u.qcnf.gz 58 (57+0)
s cnf 0 (s cnf 0)
212 (211+1)
s cnf 0 (s cnf 0)
800 (800+0) 55 (53+2) 308 (245+63)
s cnf 0 (s cnf 0)
800 (800+0)
s820_d10_s.qdimacs.gz 27 (26+0)
s cnf 1 (s cnf 1)
32 (32+0)
s cnf 1 (s cnf 1)
284 (283+0)
s cnf 1 (s cnf 1)
69 (67+2) 119 (118+0)
s cnf 1 (s cnf 1)
800 (800+0)
s820_d11_u.qdimacs.gz 31 (31+0)
s cnf 0 (s cnf 0)
40 (40+0)
s cnf 0 (s cnf 0)
754 (754+0)
s cnf 0 (s cnf 0)
24 (22+2) 144 (144+0)
s cnf 0 (s cnf 0)
800 (800+0)
s820_d12_u.qcnf.gz 37 (37+0)
s cnf 0 (s cnf 0)
53 (52+0)
s cnf 0 (s cnf 0)
729 (729+0)
s cnf 0 (s cnf 0)
379 (377+2) 143 (142+0)
s cnf 0 (s cnf 0)
800 (800+0)
s820_d13_u.qcnf.gz 44 (44+0)
s cnf 0 (s cnf 0)
72 (72+1)
s cnf 0 (s cnf 0)
789 (788+0)
s cnf 0 (s cnf 0)
22 (20+2) 177 (177+1)
s cnf 0 (s cnf 0)
800 (800+0)
s820_d14_u.qcnf.gz 50 (49+0)
s cnf 0 (s cnf 0)
86 (85+1)
s cnf 0 (s cnf 0)
800 (800+0) 39 (37+2) 187 (186+1)
s cnf 0 (s cnf 0)
800 (800+0)
s820_d15_u.qcnf.gz 57 (57+0)
s cnf 0 (s cnf 0)
105 (104+1)
s cnf 0 (s cnf 0)
800 (800+0) 18 (16+2) 327 (327+1)
s cnf 0 (s cnf 0)
800 (800+0)
s820_d3_s.qcnf.gz 2 (2+0)
s cnf 1 (s cnf 1)
2 (2+0)
s cnf 1 (s cnf 1)
1 (1+0)
s cnf 1 (s cnf 1)
268 (265+4) 1 (1+0)
s cnf 1 (s cnf 1)
17 (17+0)
s cnf 1 (s cnf 1 2186 3903)
s820_d4_s.qdimacs.gz 4 (4+0)
s cnf 1 (s cnf 1)
4 (4+0)
s cnf 1 (s cnf 1)
2 (2+0)
s cnf 1 (s cnf 1)
800 (797+3) 2 (2+0)
s cnf 1 (s cnf 1)
128 (126+2)
s cnf 1 (s cnf 1 3587 6520)
s820_d5_s.qcnf.gz 5 (5+0)
s cnf 1 (s cnf 1)
6 (6+0)
s cnf 1 (s cnf 1)
6 (6+0)
s cnf 1 (s cnf 1)
800 (793+8) 3 (3+0)
s cnf 1 (s cnf 1)
406 (403+2)
s820_d6_s.qcnf.gz 8 (8+0)
s cnf 1 (s cnf 1)
9 (9+0)
s cnf 1 (s cnf 1)
11 (11+0)
s cnf 1 (s cnf 1)
800 (796+4) 5 (5+0)
s cnf 1 (s cnf 1)
291 (289+2)
s820_d7_s.qcnf.gz 12 (12+0)
s cnf 1 (s cnf 1)
13 (13+0)
s cnf 1 (s cnf 1)
35 (35+0)
s cnf 1 (s cnf 1)
65 (63+2) 18 (18+0)
s cnf 1 (s cnf 1)
800 (800+0)
s820_d8_s.qdimacs.gz 16 (16+0)
s cnf 1 (s cnf 1)
20 (20+0)
s cnf 1 (s cnf 1)
176 (176+0)
s cnf 1 (s cnf 1)
72 (68+4) 122 (121+0)
s cnf 1 (s cnf 1)
800 (800+0)
s820_d9_s.qcnf.gz 21 (21+0)
s cnf 1 (s cnf 1)
27 (26+0)
s cnf 1 (s cnf 1)
71 (71+0)
s cnf 1 (s cnf 1)
800 (798+2) 25 (25+0)
s cnf 1 (s cnf 1)
800 (800+0)
TOTAL solved: 148
wins: 102
solved: 141
wins: 15
solved: 89
wins: 19
solved: 3
wins: 1
solved: 110
wins: 37
solved: 22
wins: 1
Mneimneh-Sakallah_gq.ts Mneimneh-Sakallah_gqc.ts Mneimneh-Sakallah_nq72.ts Mneimneh-Sakallah_quantor.ts Mneimneh-Sakallah_rareqsuuh3pb.ts Mneimneh-Sakallah_znenofex.ts