Problem Scholl-Becker_gq.ts Scholl-Becker_gqc.ts Scholl-Becker_nq72.ts Scholl-Becker_quantor.ts Scholl-Becker_rareqsuuh3pb.ts Scholl-Becker_znenofex.ts
C432.blif_0.10_0.20_0_0_inp_exact.qdimacs.gz 54 (54+0)
s cnf 0 (s cnf 0)
800 (800+0) 26 (26+0)
s cnf 0 (s cnf 0)
424 (416+8)
s cnf 0 (s FALSE)
153 (146+7)
s cnf 0 (s cnf 0)
52 (51+2)
C432.blif_0.10_0.20_0_0_out_exact.qdimacs.gz 3 (3+0)
s cnf 0 (s cnf 0)
7 (7+0)
s cnf 0 (s cnf 0)
800 (800+0) 194 (187+6)
s cnf 0 (s FALSE)
1 (1+0)
s cnf 0 (s cnf 0)
354 (353+1)
s cnf 0 (s cnf 0 530 4736)
C432.blif_0.10_0.20_0_1_inp_exact.qdimacs.gz 0 (0+0)
s cnf 1 (s cnf 1)
0 (0+0)
s cnf 1 (s cnf 1)
2 (2+0)
s cnf 1 (s cnf 1)
53 (44+8)
s cnf 1 (s TRUE)
0 (0+0)
s cnf 1 (s cnf 1)
72 (71+2)
C432.blif_0.10_0.20_0_1_out_exact.qdimacs.gz 10 (9+0)
s cnf 0 (s cnf 0)
8 (8+0)
s cnf 0 (s cnf 0)
800 (800+0) 160 (154+5)
s cnf 0 (s FALSE)
1 (1+0)
s cnf 0 (s cnf 0)
465 (464+1)
s cnf 0 (s cnf 0 369 3209)
C432.blif_0.10_1.00_0_0_inp_exact.qdimacs.gz 0 (0+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s UNSATISFIABLE)
0 (0+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s cnf 0 171 1208)
C432.blif_0.10_1.00_0_0_out_exact.qdimacs.gz 0 (0+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s UNSATISFIABLE)
0 (0+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s cnf 0 168 1260)
C432.blif_0.10_1.00_0_1_inp_exact.qdimacs.gz 0 (0+0)
s cnf 1 (s cnf 1)
0 (0+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 170 1203)
C432.blif_0.10_1.00_0_1_out_exact.qdimacs.gz 0 (0+0)
s cnf 1 (s cnf 1)
0 (0+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 168 1240)
C499.blif_0.10_0.20_0_0_inp_exact.qdimacs.gz 48 (47+0)
s cnf 0 (s cnf 0)
800 (800+0) 800 (799+1) 800 (776+25) 800 (787+13) 23 (22+2)
C499.blif_0.10_0.20_0_0_out_exact.qdimacs.gz 800 (798+2) 800 (798+2) 800 (799+1) 48 (25+23) 800 (800+0) 21 (19+2)
C499.blif_0.10_0.20_0_1_inp_exact.qdimacs.gz 1 (1+0)
s cnf 1 (s cnf 1)
39 (39+0)
s cnf 1 (s cnf 1)
5 (5+0)
s cnf 1 (s cnf 1)
800 (774+26) 1 (1+0)
s cnf 1 (s cnf 1)
27 (26+2)
C499.blif_0.10_0.20_0_1_out_exact.qdimacs.gz 800 (798+2) 800 (798+2) 800 (799+1) 28 (17+11) 800 (800+0) 20 (18+2)
C499.blif_0.10_1.00_0_0_inp_exact.qdimacs.gz 0 (0+0)
s cnf 0 (s cnf 0)
1 (1+0)
s cnf 0 (s cnf 0)
22 (21+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s UNSATISFIABLE)
0 (0+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s cnf 0 270 2322)
C499.blif_0.10_1.00_0_0_out_exact.qdimacs.gz 800 (797+3) 1 (0+0)
s cnf 0 (s cnf 0)
800 (799+1) 0 (0+0)
s cnf 0 (s UNSATISFIABLE)
0 (0+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s cnf 0 241 2402)
C499.blif_0.10_1.00_0_1_inp_exact.qdimacs.gz 0 (0+0)
s cnf 1 (s cnf 1)
0 (0+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 274 2336)
C499.blif_0.10_1.00_0_1_out_exact.qdimacs.gz 0 (0+0)
s cnf 1 (s cnf 1)
0 (0+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 243 2480)
C5315.blif_0.10_0.20_0_0_inp_exact.qdimacs.gz 800 (797+3) 800 (799+1) 800 (799+2) 12 (11+2) 800 (793+7) 35 (33+2)
C5315.blif_0.10_0.20_0_0_out_exact.qdimacs.gz 800 (798+2) 800 (800+0) 800 (799+1) 12 (10+2) 800 (789+11) 135 (133+2)
C5315.blif_0.10_0.20_0_1_inp_exact.qdimacs.gz 4 (4+0)
s cnf 1 (s cnf 1)
10 (10+0)
s cnf 1 (s cnf 1)
800 (799+1) 13 (11+2) 800 (794+6) 37 (36+1)
C5315.blif_0.10_0.20_0_1_out_exact.qdimacs.gz 800 (798+2) 800 (800+0) 800 (798+2) 12 (10+2) 800 (790+10) 158 (156+2)
C5315.blif_0.10_1.00_0_0_inp_exact.qdimacs.gz 2 (2+0)
s cnf 0 (s cnf 0)
3 (3+0)
s cnf 0 (s cnf 0)
547 (546+1)
s cnf 0 (s cnf 0)
3 (3+0)
s cnf 0 (s FALSE)
5 (5+0)
s cnf 0 (s cnf 0)
6 (6+0)
s cnf 0 (s cnf 0 492 4070)
C5315.blif_0.10_1.00_0_0_out_exact.qdimacs.gz 2 (2+0)
s cnf 0 (s cnf 0)
3 (3+0)
s cnf 0 (s cnf 0)
800 (799+1) 5 (5+0)
s cnf 0 (s FALSE)
5 (5+0)
s cnf 0 (s cnf 0)
16 (16+0)
s cnf 0 (s cnf 0 559 4298)
C5315.blif_0.10_1.00_0_1_inp_exact.qdimacs.gz 2 (2+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 TRUE)
0 (0+0)
s cnf 1 (s cnf 1)
0 (0+0)
s cnf 1 (s cnf 1 501 4003)
C5315.blif_0.10_1.00_0_1_out_exact.qdimacs.gz 2 (2+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 TRUE)
0 (0+0)
s cnf 1 (s cnf 1)
0 (0+0)
s cnf 1 (s cnf 1 552 4231)
C6288.blif_0.10_0.20_0_0_inp_exact.qdimacs.gz 800 (799+1) 800 (800+0) 800 (799+1) 13 (12+2) 800 (795+5) 37 (36+2)
C6288.blif_0.10_0.20_0_0_out_exact.qdimacs.gz 800 (799+1) 800 (800+0) 800 (799+1) 11 (9+2) 702 (688+14) 230 (228+2)
C6288.blif_0.10_0.20_0_1_inp_exact.qdimacs.gz 800 (799+1) 800 (800+0) 800 (799+1) 13 (12+2) 800 (795+5) 30 (29+2)
C6288.blif_0.10_0.20_0_1_out_exact.qdimacs.gz 800 (799+1) 800 (799+1) 800 (799+1) 11 (9+2) 699 (684+15) 181 (179+2)
C6288.blif_0.10_1.00_0_0_inp_exact.qdimacs.gz 800 (799+1) 800 (799+1) 800 (799+1) 11 (9+2) 800 (800+0) 82 (80+2)
C6288.blif_0.10_1.00_0_0_out_exact.qdimacs.gz 800 (799+1) 800 (800+0) 800 (799+1) 11 (9+2) 800 (794+6) 84 (83+2)
C6288.blif_0.10_1.00_0_1_inp_exact.qdimacs.gz 4 (3+0)
s cnf 1 (s cnf 1)
6 (5+0)
s cnf 1 (s cnf 1)
800 (800+0) 11 (9+2) 5 (5+0)
s cnf 1 (s cnf 1)
84 (82+2)
C6288.blif_0.10_1.00_0_1_out_exact.qdimacs.gz 4 (3+0)
s cnf 1 (s cnf 1)
6 (5+0)
s cnf 1 (s cnf 1)
800 (799+1) 11 (9+2) 6 (6+0)
s cnf 1 (s cnf 1)
131 (129+2)
C880.blif_0.10_0.20_0_0_inp_exact.qdimacs.gz 479 (478+1)
s cnf 0 (s cnf 0)
800 (800+0) 800 (799+1) 13 (11+2) 800 (772+28) 254 (252+2)
C880.blif_0.10_0.20_0_0_out_exact.qdimacs.gz 14 (14+0)
s cnf 0 (s cnf 0)
91 (90+0)
s cnf 0 (s cnf 0)
800 (799+1) 12 (10+2) 800 (800+0) 26 (25+2)
C880.blif_0.10_0.20_0_1_inp_exact.qdimacs.gz 274 (273+1)
s cnf 0 (s cnf 0)
800 (800+0) 800 (799+1) 14 (13+2) 800 (775+25) 800 (799+1)
C880.blif_0.10_0.20_0_1_out_exact.qdimacs.gz 15 (15+0)
s cnf 0 (s cnf 0)
30 (30+0)
s cnf 0 (s cnf 0)
800 (799+1) 12 (10+2) 800 (800+0) 32 (30+2)
C880.blif_0.10_1.00_0_0_inp_exact.qdimacs.gz 4 (4+0)
s cnf 0 (s cnf 0)
80 (80+0)
s cnf 0 (s cnf 0)
800 (800+0) 800 (784+17) 197 (196+0)
s cnf 0 (s cnf 0)
24 (21+2)
C880.blif_0.10_1.00_0_0_out_exact.qdimacs.gz 1 (1+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s cnf 0)
800 (799+1) 800 (780+20) 800 (800+0) 22 (20+2)
C880.blif_0.10_1.00_0_1_inp_exact.qdimacs.gz 0 (0+0)
s cnf 1 (s cnf 1)
0 (0+0)
s cnf 1 (s cnf 1)
0 (0+0)
s cnf 1 (s cnf 1)
800 (782+18) 0 (0+0)
s cnf 1 (s cnf 1)
25 (21+4)
C880.blif_0.10_1.00_0_1_out_exact.qdimacs.gz 0 (0+0)
s cnf 1 (s cnf 1)
0 (0+0)
s cnf 1 (s cnf 1)
800 (799+1) 40 (21+19)
s cnf 1 (s TRUE)
0 (0+0)
s cnf 1 (s cnf 1)
25 (20+5)
comp.blif_0.10_0.20_0_0_inp_exact.qdimacs.gz 0 (0+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s UNSATISFIABLE)
0 (0+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s cnf 0 54 379)
comp.blif_0.10_0.20_0_0_out_exact.qdimacs.gz 0 (0+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s UNSATISFIABLE)
0 (0+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s cnf 0 28 358)
comp.blif_0.10_0.20_0_1_out_exact.qdimacs.gz 0 (0+0)
s cnf 1 (s cnf 1)
0 (0+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 964)
comp.blif_0.10_1.00_0_0_inp_exact.qdimacs.gz 0 (0+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s UNSATISFIABLE)
0 (0+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s cnf 0 94 562)
comp.blif_0.10_1.00_0_0_out_exact.qdimacs.gz 0 (0+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s UNSATISFIABLE)
0 (0+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s cnf 0 92 763)
comp.blif_0.10_1.00_0_1_out_exact.qdimacs.gz 0 (0+0)
s cnf 1 (s cnf 1)
0 (0+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 84 795)
term1.blif_0.10_0.20_0_0_inp_exact.qdimacs.gz 1 (1+0)
s cnf 0 (s cnf 0)
5 (5+0)
s cnf 0 (s cnf 0)
2 (2+0)
s cnf 0 (s cnf 0)
83 (74+9)
s cnf 0 (s FALSE)
324 (299+25)
s cnf 0 (s cnf 0)
14 (12+2)
term1.blif_0.10_0.20_0_0_out_exact.qdimacs.gz 1 (1+0)
s cnf 0 (s cnf 0)
1 (0+0)
s cnf 0 (s cnf 0)
23 (23+0)
s cnf 0 (s cnf 0)
403 (397+6)
s cnf 0 (s FALSE)
5 (5+0)
s cnf 0 (s cnf 0)
455 (454+1)
s cnf 0 (s cnf 0 145 2176)
term1.blif_0.10_0.20_0_1_inp_exact.qdimacs.gz 0 (0+0)
s cnf 1 (s cnf 1)
0 (0+0)
s cnf 1 (s cnf 1)
0 (0+0)
s cnf 1 (s cnf 1)
8 (4+4)
s cnf 1 (s TRUE)
0 (0+0)
s cnf 1 (s cnf 1)
15 (14+2)
term1.blif_0.10_0.20_0_1_out_exact.qdimacs.gz 0 (0+0)
s cnf 1 (s cnf 1)
0 (0+0)
s cnf 1 (s cnf 1)
0 (0+0)
s cnf 1 (s cnf 1)
7 (3+3)
s cnf 1 (s TRUE)
0 (0+0)
s cnf 1 (s cnf 1)
4 (3+0)
s cnf 1 (s cnf 1 138 2169)
term1.blif_0.10_1.00_0_0_inp_exact.qdimacs.gz 0 (0+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s UNSATISFIABLE)
0 (0+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s cnf 0 162 2344)
term1.blif_0.10_1.00_0_0_out_exact.qdimacs.gz 0 (0+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s UNSATISFIABLE)
0 (0+0)
s cnf 0 (s cnf 0)
0 (0+0)
s cnf 0 (s cnf 0 152 2526)
term1.blif_0.10_1.00_0_1_inp_exact.qdimacs.gz 0 (0+0)
s cnf 1 (s cnf 1)
0 (0+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 163 2332)
term1.blif_0.10_1.00_0_1_out_exact.qdimacs.gz 0 (0+0)
s cnf 1 (s cnf 1)
0 (0+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 153 2494)
z4ml.blif_0.10_1.00_0_1_out_exact.qdimacs.gz 0 (0+0)
s cnf 1 (s cnf 1)
0 (0+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 10 78)
TOTAL solved: 43
wins: 37
solved: 40
wins: 24
solved: 29
wins: 23
solved: 32
wins: 21
solved: 37
wins: 29
solved: 27
wins: 21
Scholl-Becker_gq.ts Scholl-Becker_gqc.ts Scholl-Becker_nq72.ts Scholl-Becker_quantor.ts Scholl-Becker_rareqsuuh3pb.ts Scholl-Becker_znenofex.ts