Problem BMC_gq.ts BMC_gqc.ts BMC_nq72.ts BMC_quantor.ts BMC_rareqsuuh3pb.ts BMC_znenofex.ts
c1_BMC_p1_k1024.qdimacs.gz 800 (800+0) 800 (800+0) 800 (800+0) 18 (16+2) 10 (9+1)
s cnf 1 (s cnf 1)
37 (35+2)
c1_BMC_p1_k128.qdimacs.gz 800 (799+1) 800 (799+1) 800 (800+0) 7 (6+1)
s cnf 1 (s TRUE)
2 (2+0)
s cnf 1 (s cnf 1)
22 (21+1)
s cnf 1 (s cnf 1 23675 103953)
c1_BMC_p1_k16.qdimacs.gz 800 (799+1) 76 (75+1)
s cnf 1 (s cnf 1)
800 (800+0) 2 (2+0)
s cnf 1 (s TRUE)
8 (7+0)
s cnf 1 (s cnf 1)
6 (5+0)
s cnf 1 (s cnf 1 20584 68696)
c1_BMC_p1_k2.qdimacs.gz 43 (42+1)
s cnf 1 (s cnf 1)
10 (10+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 36 160)
c1_BMC_p1_k2048.qdimacs.gz 800 (800+0) 800 (800+0) 800 (800+0) 19 (17+2) 19 (18+1)
s cnf 1 (s cnf 1)
51 (49+2)
c1_BMC_p1_k256.qdimacs.gz 800 (799+1) 800 (799+1) 800 (800+0) 20 (18+1)
s cnf 1 (s TRUE)
2 (2+0)
s cnf 1 (s cnf 1)
31 (29+1)
s cnf 1 (s cnf 1 26931 139538)
c1_BMC_p1_k32.qdimacs.gz 800 (799+1) 113 (111+1)
s cnf 1 (s cnf 1)
800 (800+0) 2 (2+0)
s cnf 1 (s TRUE)
4 (4+0)
s cnf 1 (s cnf 1)
7 (7+0)
s cnf 1 (s cnf 1 21174 76308)
c1_BMC_p1_k4.qdimacs.gz 315 (314+1)
s cnf 1 (s cnf 1)
20 (20+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 37 164)
c1_BMC_p1_k512.qdimacs.gz 800 (799+1) 800 (799+1) 800 (800+0) 82 (80+2)
s cnf 1 (s TRUE)
6 (6+0)
s cnf 1 (s cnf 1)
31 (30+2)
c1_BMC_p1_k64.qdimacs.gz 800 (799+1) 800 (799+1) 800 (800+0) 4 (3+0)
s cnf 1 (s TRUE)
2 (2+0)
s cnf 1 (s cnf 1)
13 (12+0)
s cnf 1 (s cnf 1 22048 86570)
c1_BMC_p1_k8.qdimacs.gz 800 (799+1) 49 (49+1)
s cnf 1 (s cnf 1)
465 (465+0)
s cnf 1 (s cnf 1)
1 (1+0)
s cnf 1 (s TRUE)
1 (1+0)
s cnf 1 (s cnf 1)
2 (2+0)
s cnf 1 (s cnf 1 8956 34821)
c2_BMC_p1_k1024.qdimacs.gz 425 (423+2) 383 (382+2) 800 (799+1) 15 (13+2) 2 (2+0)
s cnf 1 (s cnf 1)
60 (58+2)
c2_BMC_p1_k128.qdimacs.gz 800 (799+1) 433 (431+2) 800 (800+0) 27 (22+5)
s cnf 1 (s TRUE)
7 (7+0)
s cnf 1 (s cnf 1)
26 (25+1)
s cnf 1 (s cnf 1 10602 65109)
c2_BMC_p1_k16.qdimacs.gz 800 (800+0) 59 (59+1)
s cnf 1 (s cnf 1)
800 (800+0) 2 (1+1)
s cnf 1 (s TRUE)
5 (4+0)
s cnf 1 (s cnf 1)
2 (2+0)
s cnf 1 (s cnf 1 6775 28807)
c2_BMC_p1_k2048.qdimacs.gz 643 (641+2) 569 (567+2) 800 (799+1) 15 (13+2) 3 (2+0)
s cnf 1 (s cnf 1)
102 (100+2)
c2_BMC_p1_k256.qdimacs.gz 800 (799+1) 800 (799+1) 800 (800+0) 81 (72+9)
s cnf 1 (s TRUE)
0 (0+0)
s cnf 1 (s cnf 1)
91 (90+1)
s cnf 1 (s cnf 1 15032 106299)
c2_BMC_p1_k32.qdimacs.gz 800 (799+1) 160 (159+1)
s cnf 1 (s cnf 1)
800 (800+0) 5 (4+1)
s cnf 1 (s TRUE)
7 (7+0)
s cnf 1 (s cnf 1)
8 (8+0)
s cnf 1 (s cnf 1 7302 34059)
c2_BMC_p1_k4.qdimacs.gz 47 (46+0)
s cnf 1 (s cnf 1)
6 (6+0)
s cnf 1 (s cnf 1)
2 (1+0)
s cnf 1 (s cnf 1)
0 (0+0)
s cnf 1 (s TRUE)
0 (0+0)
s cnf 1 (s cnf 1)
0 (0+0)
s cnf 1 (s cnf 1 1188 7119)
c2_BMC_p1_k512.qdimacs.gz 800 (798+2) 800 (798+2) 800 (800+0) 800 (782+18) 1 (1+0)
s cnf 1 (s cnf 1)
487 (485+2)
s cnf 1 (s cnf 1 23916 188332)
c2_BMC_p1_k64.qdimacs.gz 800 (799+1) 609 (608+1)
s cnf 1 (s cnf 1)
800 (800+0) 8 (6+2)
s cnf 1 (s TRUE)
3 (3+0)
s cnf 1 (s cnf 1)
17 (17+0)
s cnf 1 (s cnf 1 8366 44842)
c2_BMC_p1_k8.qdimacs.gz 471 (471+1)
s cnf 1 (s cnf 1)
14 (14+0)
s cnf 1 (s cnf 1)
19 (19+0)
s cnf 1 (s cnf 1)
1 (0+0)
s cnf 1 (s TRUE)
0 (0+0)
s cnf 1 (s cnf 1)
1 (1+0)
s cnf 1 (s cnf 1 2878 14873)
c2_BMC_p2_k1024.qdimacs.gz 443 (441+2) 378 (377+2) 800 (800+0) 15 (13+2) 115 (115+1)
s cnf 0 (s cnf 0)
60 (58+2)
c2_BMC_p2_k128.qdimacs.gz 800 (799+1) 473 (471+2) 800 (800+0) 19 (14+4)
s cnf 0 (s FALSE)
2 (2+0)
s cnf 0 (s cnf 0)
23 (22+1)
s cnf 0 (s cnf 0 10602 65110)
c2_BMC_p2_k16.qdimacs.gz 800 (800+0) 47 (47+1)
s cnf 0 (s cnf 0)
800 (800+0) 2 (1+0)
s cnf 0 (s FALSE)
1 (1+0)
s cnf 0 (s cnf 0)
2 (2+0)
s cnf 0 (s cnf 0 6759 28913)
c2_BMC_p2_k2048.qdimacs.gz 632 (630+2) 574 (572+2) 800 (800+1) 15 (13+2) 40 (39+2)
s cnf 0 (s cnf 0)
103 (101+2)
c2_BMC_p2_k256.qdimacs.gz 800 (799+1) 800 (799+1) 800 (800+0) 52 (42+9)
s cnf 0 (s FALSE)
3 (3+0)
s cnf 0 (s cnf 0)
85 (83+1)
s cnf 0 (s cnf 0 15032 106300)
c2_BMC_p2_k32.qdimacs.gz 614 (614+1)
s cnf 0 (s cnf 0)
125 (124+1)
s cnf 0 (s cnf 0)
800 (800+0) 3 (2+1)
s cnf 0 (s FALSE)
1 (1+0)
s cnf 0 (s cnf 0)
6 (6+0)
s cnf 0 (s cnf 0 7295 34143)
c2_BMC_p2_k512.qdimacs.gz 800 (798+2) 800 (798+2) 800 (800+0) 98 (80+18)
s cnf 0 (s FALSE)
12 (12+0)
s cnf 0 (s cnf 0)
348 (346+2)
s cnf 0 (s cnf 0 23916 188332)
c2_BMC_p2_k64.qdimacs.gz 658 (658+1)
s cnf 0 (s cnf 0)
219 (218+1)
s cnf 0 (s cnf 0)
800 (800+0) 6 (3+2)
s cnf 0 (s FALSE)
2 (2+0)
s cnf 0 (s cnf 0)
11 (11+0)
s cnf 0 (s cnf 0 8362 44890)
c2_BMC_p2_k8.qdimacs.gz 74 (74+0)
s cnf 0 (s cnf 0)
13 (12+0)
s cnf 0 (s cnf 0)
17 (17+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s FALSE)
0 (0+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s cnf 0 2908 15054)
c3_BMC_p1_k1024.qdimacs.gz 116 (115+2) 112 (110+2) 163 (163+0)
s cnf 1 (s cnf 1)
475 (454+21)
s cnf 1 (s TRUE)
110 (109+0)
s cnf 1 (s cnf 1)
23 (21+2)
c3_BMC_p1_k128.qdimacs.gz 800 (799+1) 246 (245+1)
s cnf 1 (s cnf 1)
800 (800+0) 8 (6+2)
s cnf 1 (s TRUE)
3 (3+0)
s cnf 1 (s cnf 1)
5 (5+0)
s cnf 1 (s cnf 1 4771 29425)
c3_BMC_p1_k16.qdimacs.gz 800 (800+0) 12 (12+0)
s cnf 1 (s cnf 1)
370 (370+0)
s cnf 1 (s cnf 1)
1 (0+0)
s cnf 1 (s TRUE)
1 (1+0)
s cnf 1 (s cnf 1)
1 (1+0)
s cnf 1 (s cnf 1 2995 12831)
c3_BMC_p1_k2048.qdimacs.gz 316 (314+2) 274 (272+2) 452 (452+0)
s cnf 1 (s cnf 1)
19 (17+2) 322 (321+1)
s cnf 1 (s cnf 1)
28 (26+2)
c3_BMC_p1_k256.qdimacs.gz 800 (799+1) 800 (799+1) 38 (38+0)
s cnf 1 (s cnf 1)
30 (26+5)
s cnf 1 (s TRUE)
10 (9+0)
s cnf 1 (s cnf 1)
16 (15+1)
s cnf 1 (s cnf 1 6852 48290)
c3_BMC_p1_k32.qdimacs.gz 800 (799+1) 27 (27+0)
s cnf 1 (s cnf 1)
593 (593+0)
s cnf 1 (s cnf 1)
1 (1+0)
s cnf 1 (s TRUE)
1 (1+0)
s cnf 1 (s cnf 1)
1 (1+0)
s cnf 1 (s cnf 1 3239 15290)
c3_BMC_p1_k512.qdimacs.gz 800 (799+1) 800 (798+2) 758 (758+0)
s cnf 1 (s cnf 1)
124 (114+10)
s cnf 1 (s TRUE)
32 (32+0)
s cnf 1 (s cnf 1)
69 (68+1)
s cnf 1 (s cnf 1 10991 86037)
c3_BMC_p1_k64.qdimacs.gz 800 (799+1) 55 (54+1)
s cnf 1 (s cnf 1)
92 (91+0)
s cnf 1 (s cnf 1)
3 (2+1)
s cnf 1 (s TRUE)
2 (2+0)
s cnf 1 (s cnf 1)
3 (3+0)
s cnf 1 (s cnf 1 3760 20011)
c3_BMC_p1_k8.qdimacs.gz 477 (476+0)
s cnf 1 (s cnf 1)
7 (7+0)
s cnf 1 (s cnf 1)
19 (19+0)
s cnf 1 (s cnf 1)
0 (0+0)
s cnf 1 (s TRUE)
0 (0+0)
s cnf 1 (s cnf 1)
0 (0+0)
s cnf 1 (s cnf 1 1553 7719)
c4_BMC_p1_k1024.qdimacs.gz 800 (800+0) 58 (58+1)
s cnf 1 (s cnf 1)
65 (65+0)
s cnf 1 (s cnf 1)
2 (1+0)
s cnf 1 (s TRUE)
0 (0+0)
s cnf 1 (s cnf 1)
2 (2+0)
s cnf 1 (s cnf 1 1809 12440)
c4_BMC_p1_k128.qdimacs.gz 33 (33+0)
s cnf 1 (s cnf 1)
4 (4+0)
s cnf 1 (s cnf 1)
1 (1+0)
s cnf 1 (s cnf 1)
0 (0+0)
s cnf 1 (s TRUE)
0 (0+0)
s cnf 1 (s cnf 1)
0 (0+0)
s cnf 1 (s cnf 1 738 4095)
c4_BMC_p1_k2048.qdimacs.gz 800 (799+1) 275 (274+1)
s cnf 1 (s cnf 1)
800 (800+1) 4 (3+1)
s cnf 1 (s TRUE)
0 (0+0)
s cnf 1 (s cnf 1)
3 (3+0)
s cnf 1 (s cnf 1 3248 23528)
c4_BMC_p1_k256.qdimacs.gz 230 (229+0)
s cnf 1 (s cnf 1)
11 (10+0)
s cnf 1 (s cnf 1)
1 (1+0)
s cnf 1 (s cnf 1)
0 (0+0)
s cnf 1 (s TRUE)
0 (0+0)
s cnf 1 (s cnf 1)
0 (0+0)
s cnf 1 (s cnf 1 718 4084)
c4_BMC_p1_k32.qdimacs.gz 14 (14+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)
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 79 188)
c4_BMC_p1_k512.qdimacs.gz 800 (800+0) 22 (21+0)
s cnf 1 (s cnf 1)
12 (12+0)
s cnf 1 (s cnf 1)
1 (1+0)
s cnf 1 (s TRUE)
0 (0+0)
s cnf 1 (s cnf 1)
1 (1+0)
s cnf 1 (s cnf 1 1085 6879)
c4_BMC_p1_k64.qdimacs.gz 18 (18+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)
0 (0+0)
s cnf 1 (s TRUE)
0 (0+0)
s cnf 1 (s cnf 1)
0 (0+0)
s cnf 1 (s cnf 1 739 4627)
c4_BMC_p2_k1024.qdimacs.gz 35 (35+0)
s cnf 0 (s cnf 0)
57 (56+1)
s cnf 0 (s cnf 0)
39 (38+0)
s cnf 0 (s cnf 0)
1 (1+0)
s cnf 0 (s FALSE)
0 (0+0)
s cnf 0 (s cnf 0)
1 (1+0)
s cnf 0 (s cnf 0 1809 12440)
c4_BMC_p2_k128.qdimacs.gz 8 (8+0)
s cnf 0 (s cnf 0)
3 (3+0)
s cnf 0 (s cnf 0)
1 (1+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s FALSE)
0 (0+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s cnf 0 738 4095)
c4_BMC_p2_k2048.qdimacs.gz 81 (81+1)
s cnf 0 (s cnf 0)
341 (340+1)
s cnf 0 (s cnf 0)
800 (800+0) 2 (2+0)
s cnf 0 (s FALSE)
2 (2+0)
s cnf 0 (s cnf 0)
2 (2+0)
s cnf 0 (s cnf 0 3248 23528)
c4_BMC_p2_k256.qdimacs.gz 13 (13+0)
s cnf 0 (s cnf 0)
8 (8+0)
s cnf 0 (s cnf 0)
1 (1+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s FALSE)
0 (0+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s cnf 0 718 4084)
c4_BMC_p2_k512.qdimacs.gz 17 (16+0)
s cnf 0 (s cnf 0)
20 (20+0)
s cnf 0 (s cnf 0)
4 (4+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s FALSE)
0 (0+0)
s cnf 0 (s cnf 0)
1 (1+0)
s cnf 0 (s cnf 0 1085 6879)
c4_BMC_p2_k64.qdimacs.gz 10 (10+0)
s cnf 0 (s cnf 0)
2 (2+0)
s cnf 0 (s cnf 0)
1 (1+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s FALSE)
0 (0+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s cnf 0 739 4626)
c5_BMC_p1_k1024.qdimacs.gz 312 (310+2) 273 (271+2) 800 (800+0) 19 (17+2) 800 (799+1) 66 (64+2)
c5_BMC_p1_k128.qdimacs.gz 800 (799+1) 800 (798+2) 800 (800+0) 800 (790+10) 800 (798+2) 800 (799+1)
c5_BMC_p1_k16.qdimacs.gz 800 (799+1) 65 (64+1)
s cnf 1 (s cnf 1)
800 (800+0) 3 (2+1)
s cnf 1 (s TRUE)
8 (8+0)
s cnf 1 (s cnf 1)
5 (5+0)
s cnf 1 (s cnf 1 9410 45611)
c5_BMC_p1_k2048.qdimacs.gz 800 (798+2) 729 (727+2) 800 (800+0) 19 (17+2) 800 (798+2) 8 (6+2)
c5_BMC_p1_k256.qdimacs.gz 800 (797+3) 800 (798+2) 800 (800+0) 800 (780+21) 800 (798+2) 28 (27+2)
c5_BMC_p1_k32.qdimacs.gz 800 (799+1) 135 (133+1)
s cnf 1 (s cnf 1)
800 (800+0) 2 (2+0)
s cnf 1 (s TRUE)
11 (11+0)
s cnf 1 (s cnf 1)
8 (7+0)
s cnf 1 (s cnf 1 10283 58814)
c5_BMC_p1_k4.qdimacs.gz 118 (118+1)
s cnf 1 (s cnf 1)
13 (13+0)
s cnf 1 (s cnf 1)
2 (2+0)
s cnf 1 (s cnf 1)
0 (0+0)
s cnf 1 (s TRUE)
0 (0+0)
s cnf 1 (s cnf 1)
1 (1+0)
s cnf 1 (s cnf 1 1791 16367)
c5_BMC_p1_k512.qdimacs.gz 800 (798+2) 800 (798+2) 800 (800+0) 18 (16+2) 800 (798+2) 43 (41+2)
c5_BMC_p1_k64.qdimacs.gz 800 (799+1) 800 (798+2) 800 (800+0) 800 (795+5) 800 (799+1) 800 (799+1)
c5_BMC_p1_k8.qdimacs.gz 455 (454+1)
s cnf 1 (s cnf 1)
25 (24+1)
s cnf 1 (s cnf 1)
81 (81+0)
s cnf 1 (s cnf 1)
1 (0+0)
s cnf 1 (s TRUE)
0 (0+0)
s cnf 1 (s cnf 1)
2 (2+0)
s cnf 1 (s cnf 1 3908 24514)
c5_BMC_p2_k1024.qdimacs.gz 298 (296+2) 275 (274+2) 800 (800+0) 19 (17+2) 800 (798+2) 66 (64+2)
c5_BMC_p2_k128.qdimacs.gz 800 (799+1) 800 (798+2) 800 (800+0) 800 (790+10) 800 (798+2) 800 (799+1)
c5_BMC_p2_k16.qdimacs.gz 800 (799+1) 76 (75+1)
s cnf 0 (s cnf 0)
800 (800+0) 1 (1+0)
s cnf 0 (s FALSE)
7 (7+0)
s cnf 0 (s cnf 0)
4 (4+0)
s cnf 0 (s cnf 0 9410 45611)
c5_BMC_p2_k2048.qdimacs.gz 800 (798+2) 725 (723+2) 800 (800+0) 19 (17+2) 800 (798+2) 8 (6+2)
c5_BMC_p2_k256.qdimacs.gz 800 (798+2) 800 (798+2) 800 (800+0) 800 (778+22) 800 (798+2) 28 (26+2)
c5_BMC_p2_k32.qdimacs.gz 800 (799+1) 112 (111+1)
s cnf 0 (s cnf 0)
800 (800+0) 2 (2+0)
s cnf 0 (s FALSE)
9 (8+0)
s cnf 0 (s cnf 0)
6 (6+0)
s cnf 0 (s cnf 0 10283 58814)
c5_BMC_p2_k512.qdimacs.gz 800 (798+2) 800 (798+2) 800 (800+0) 18 (16+2) 800 (798+2) 43 (41+2)
c5_BMC_p2_k64.qdimacs.gz 800 (799+1) 800 (798+2) 0 (0+0) 800 (796+5) 800 (799+1) 800 (799+1)
c6_BMC_p1_k1024.qdimacs.gz 800 (799+1) 800 (799+2) 800 (800+0) 24 (21+3)
s cnf 1 (s TRUE)
0 (0+0)
s cnf 1 (s cnf 1)
23 (22+1)
s cnf 1 (s cnf 1 5131 39385)
c6_BMC_p1_k128.qdimacs.gz 800 (800+0) 41 (41+0)
s cnf 1 (s cnf 1)
93 (93+0)
s cnf 1 (s cnf 1)
1 (1+0)
s cnf 1 (s TRUE)
0 (0+0)
s cnf 1 (s cnf 1)
1 (1+0)
s cnf 1 (s cnf 1 1898 9063)
c6_BMC_p1_k16.qdimacs.gz 800 (800+0) 5 (5+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 980 5615)
c6_BMC_p1_k2048.qdimacs.gz 214 (212+1) 187 (186+1) 800 (800+0) 73 (67+6)
s cnf 1 (s TRUE)
0 (0+0)
s cnf 1 (s cnf 1)
77 (76+1)
s cnf 1 (s cnf 1 8873 73878)
c6_BMC_p1_k256.qdimacs.gz 800 (799+1) 178 (177+1)
s cnf 1 (s cnf 1)
800 (800+0) 2 (2+1)
s cnf 1 (s TRUE)
0 (0+0)
s cnf 1 (s cnf 1)
2 (2+0)
s cnf 1 (s cnf 1 2368 13385)
c6_BMC_p1_k32.qdimacs.gz 800 (800+0) 9 (9+0)
s cnf 1 (s cnf 1)
6 (6+0)
s cnf 1 (s cnf 1)
0 (0+0)
s cnf 1 (s TRUE)
0 (0+0)
s cnf 1 (s cnf 1)
0 (0+0)
s cnf 1 (s cnf 1 1694 7010)
c6_BMC_p1_k512.qdimacs.gz 800 (799+1) 800 (799+1) 686 (686+0)
s cnf 1 (s cnf 1)
7 (5+2)
s cnf 1 (s TRUE)
0 (0+0)
s cnf 1 (s cnf 1)
5 (4+0)
s cnf 1 (s cnf 1 3300 21927)
c6_BMC_p1_k64.qdimacs.gz 800 (800+0) 20 (20+0)
s cnf 1 (s cnf 1)
7 (7+0)
s cnf 1 (s cnf 1)
1 (0+0)
s cnf 1 (s TRUE)
0 (0+0)
s cnf 1 (s cnf 1)
1 (0+0)
s cnf 1 (s cnf 1 1672 6905)
c6_BMC_p1_k8.qdimacs.gz 15 (15+0)
s cnf 1 (s cnf 1)
3 (3+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 65 167)
c6_BMC_p2_k1024.qdimacs.gz 119 (118+1)
s cnf 0 (s cnf 0)
800 (798+2) 800 (800+0) 2 (1+0)
s cnf 0 (s FALSE)
0 (0+0)
s cnf 0 (s cnf 0)
5 (4+0)
s cnf 0 (s cnf 0 5131 39386)
c6_BMC_p2_k128.qdimacs.gz 24 (23+0)
s cnf 0 (s cnf 0)
26 (26+0)
s cnf 0 (s cnf 0)
157 (157+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s FALSE)
0 (0+0)
s cnf 0 (s cnf 0)
1 (1+0)
s cnf 0 (s cnf 0 1898 9064)
c6_BMC_p2_k2048.qdimacs.gz 210 (209+1) 191 (190+1) 800 (800+0) 3 (3+1)
s cnf 0 (s FALSE)
0 (0+0)
s cnf 0 (s cnf 0)
9 (8+1)
s cnf 0 (s cnf 0 8873 73879)
c6_BMC_p2_k256.qdimacs.gz 20 (20+0)
s cnf 0 (s cnf 0)
17 (16+0)
s cnf 0 (s cnf 0)
197 (197+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s FALSE)
0 (0+0)
s cnf 0 (s cnf 0)
1 (1+0)
s cnf 0 (s cnf 0 2368 13385)
c6_BMC_p2_k512.qdimacs.gz 45 (45+1)
s cnf 0 (s cnf 0)
570 (569+1)
s cnf 0 (s cnf 0)
395 (395+0)
s cnf 0 (s cnf 0)
1 (1+0)
s cnf 0 (s FALSE)
0 (0+0)
s cnf 0 (s cnf 0)
2 (2+0)
s cnf 0 (s cnf 0 3300 21930)
c6_BMC_p2_k64.qdimacs.gz 15 (15+0)
s cnf 0 (s cnf 0)
6 (6+0)
s cnf 0 (s cnf 0)
46 (46+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s FALSE)
0 (0+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s cnf 0 1671 6858)
TOTAL solved: 26
wins: 0
solved: 48
wins: 0
solved: 37
wins: 5
solved: 65
wins: 32
solved: 73
wins: 65
solved: 64
wins: 20
BMC_gq.ts BMC_gqc.ts BMC_nq72.ts BMC_quantor.ts BMC_rareqsuuh3pb.ts BMC_znenofex.ts