| Problem | qesto | nbl_gqc | rareqs | depqbf |
|---|---|---|---|---|
| k_ph_p-10.qdimacs.gz (1) | 117 (117+0) s cnf 0 (s cnf 0) (bt:1) |
77 (76+0) s cnf 0 (s cnf 0) |
109 (109+0) s cnf 0 (s cnf 0) |
800 (800+0) |
| jnh213-00.qdimacs.gz (1) | 0 (0+0) s cnf 1 (s cnf 1) (bt:1) |
1 (1+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) |
| k_ph_p-11.qdimacs.gz (1) | 800 (800+0) (bt:0) |
415 (415+1) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (800+0) |
| k_ph_p-12.qdimacs.gz (1) | 800 (800+0) (bt:0) |
800 (799+1) | 800 (800+0) | 800 (800+0) |
| lights3_021_0_027.qdimacs.gz (1) | 0 (0+0) s cnf 0 (s cnf 0) (bt:1) |
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) |
| lights3_021_0_009.qdimacs.gz (1) | 0 (0+0) s cnf 1 (s cnf 1) (bt: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 cnf 1) |
| TOILET7.1.iv.13.qdimacs.gz (1) | 0 (0+0) s cnf 0 (s cnf 0) (bt:1) |
1 (1+0) s cnf 0 (s cnf 0) |
0 (0+0) s cnf 0 (s cnf 0) |
2 (2+0) s cnf 0 (s cnf 0) |
| TOILET7.1.iv.14.qdimacs.gz (1) | 0 (0+0) s cnf 1 (s cnf 1) (bt: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 cnf 1) |
| C432.blif_0.10_1.00_0_0_out_exact.qdimacs.gz (1) | 0 (0+0) s cnf 0 (s cnf 0) (bt:1) |
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) |
| k_ph_n-16.qdimacs.gz (1) | 0 (0+0) s cnf 1 (s cnf 1) (bt:1) |
110 (109+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) |
| k_ph_p-16.qdimacs.gz (1) | 800 (800+0) (bt:0) |
800 (799+1) | 800 (800+0) | 800 (800+0) |
| k_ph_n-17.qdimacs.gz (1) | 0 (0+0) s cnf 1 (s cnf 1) (bt:1) |
183 (182+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) |
| lights3_035_0_002.qdimacs.gz (1) | 0 (0+0) s cnf 0 (s cnf 0) (bt:1) |
1 (1+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) |
| C499.blif_0.10_0.20_0_1_out_exact.qdimacs.gz (3) | 800 (799+1) (bt:1087062) |
800 (798+2) | 800 (800+0) | 800 (800+0) |
| C499.blif_0.10_0.20_0_0_out_exact.qdimacs.gz (3) | 800 (799+1) (bt:1165670) |
800 (798+2) | 800 (800+0) | 800 (800+0) |
| C499.blif_0.10_0.20_0_0_inp_exact.qdimacs.gz (17) | 800 (799+1) (bt:777207) |
800 (800+0) | 800 (784+16) | 88 (88+0) s cnf 0 (s cnf 0) |
| emptyroom_e3_par--opt-10_.qdimacs.gz (3) | 0 (0+0) s cnf 1 (s cnf 1) (bt:64) |
2 (2+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
1 (1+0) s cnf 1 (s cnf 1) |
| C499.blif_0.10_1.00_0_0_out_exact.qdimacs.gz (1) | 0 (0+0) s cnf 0 (s cnf 0) (bt:1) |
0 (0+0) s cnf 0 (s cnf 0) |
0 (0+0) s cnf 0 (s cnf 0) |
2 (2+0) s cnf 0 (s cnf 0) |
| biu.mv.xl_ao.bb-b001-p010-MIF01-c10.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004.qdimacs.gz (7) | 0 (0+0) s cnf 1 (s cnf 1) (bt:17) |
1 (1+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) |
| lights3_035_0_027.qdimacs.gz (3) | 0 (0+0) s cnf 0 (s cnf 0) (bt:1) |
1 (1+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) |
| lights3_035_0_051.qdimacs.gz (5) | 0 (0+0) s cnf 0 (s cnf 0) (bt:1) |
1 (1+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) |
| emptyroom_e3_ser---19_.qdimacs.gz (3) | 800 (799+1) (bt:794653) |
318 (317+0) s cnf 0 (s cnf 0) |
23 (23+0) s cnf 0 (s cnf 0) |
800 (800+0) |
| uclid-pipe2.qdimacs.gz (4) | 800 (779+21) (bt:5177) |
800 (800+0) | 800 (799+1) | 800 (800+0) |
| uclid-pipe3a.qdimacs.gz (4) | 800 (800+0) (bt:19542) |
121 (121+0) s cnf 1 (s cnf 1) |
800 (795+5) | 800 (800+0) |
| biu.mv.xl_ao.bb-b001-p010-MIF05-c07.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004.qdimacs.gz (7) | 800 (797+3) (bt:731819) |
2 (2+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
800 (800+0) |
| lut4_AND_f1.qdimacs.gz (3) | 0 (0+0) s cnf 1 (s cnf 1) (bt:247) |
6 (6+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) |
| biu.mv.xl_ao.bb-b001-p010-OPF02-c08.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003.qdimacs.gz (5) | 0 (0+0) s cnf 1 (s cnf 1) (bt:20) |
1 (1+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) |
| incrementer-enc08-uniform-depth-9.qdimacs.gz (3) | 0 (0+0) s cnf 0 (s cnf 0) (bt:1) |
2 (2+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) |
| counter_32.qdimacs.gz (11) | 0 (0+0) s cnf 1 (s cnf 1) (bt:711) |
800 (799+1) | 36 (34+2) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| lights3_021_0_013.qdimacs.gz (21) | 0 (0+0) s cnf 0 (s cnf 0) (bt:1) |
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) |
| eijk.S1238.S-d3.qdimacs.gz (3) | 83 (83+0) s cnf 0 (s cnf 0) (bt:146134) |
0 (0+0) s cnf 0 (s cnf 0) |
1 (1+0) s cnf 0 (s cnf 0) |
434 (434+0) s cnf 0 (s cnf 0) |
| ev-pr-6x6-5-5-0-1-2-lg.qdimacs.gz (5) | 0 (0+0) s cnf 0 (s cnf 0) (bt:40) |
4 (4+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) |
| biu.mv.xl_ao.bb-b003-p020-MIF04-c05.blif-biu.inv.prop.bb-bmc.with-IOC.unfold-004.qdimacs.gz (7) | 18 (18+0) s cnf 0 (s cnf 0) (bt:11194) |
2 (2+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) |
| sortnetsort7.v.stepl.004.qdimacs.gz (3) | 3 (3+0) s cnf 0 (s cnf 0) (bt:3914) |
36 (36+0) s cnf 0 (s cnf 0) |
0 (0+0) s cnf 0 (s cnf 0) |
326 (326+0) s cnf 0 (s cnf 0) |
| s510_d3_s.qdimacs.gz (3) | 0 (0+0) s cnf 1 (s cnf 1) (bt:749) |
1 (1+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) |
| counter_e_8.qdimacs.gz (7) | 8 (7+0) s cnf 1 (s cnf 1) (bt:20321) |
800 (800+0) | 4 (4+0) s cnf 1 (s cnf 1) |
800 (800+0) |
| C880.blif_0.10_0.20_0_1_out_exact.qdimacs.gz (3) | 800 (799+1) (bt:1084976) |
28 (28+0) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (800+0) |
| C880.blif_0.10_0.20_0_0_out_exact.qdimacs.gz (3) | 800 (799+1) (bt:1081280) |
27 (27+0) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (800+0) |
| test4_quant_squaring4.qdimacs.gz (7) | 800 (799+1) (bt:172295) |
578 (575+2) | 800 (794+6) | 800 (800+0) |
| C432.blif_0.10_0.20_0_1_out_exact.qdimacs.gz (3) | 800 (799+1) (bt:834099) |
2 (2+0) s cnf 0 (s cnf 0) |
2 (2+0) s cnf 0 (s cnf 0) |
102 (102+0) s cnf 0 (s cnf 0) |
| test1_quant2.qdimacs.gz (3) | 800 (799+1) (bt:1153596) |
571 (569+2) | 800 (800+1) | 800 (800+0) |
| TOILET10.1.iv.20.qdimacs.gz (1) | 0 (0+0) s cnf 1 (s cnf 1) (bt:1) |
1 (1+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) |
| s13207_1_107.qdimacs.gz (3) | 625 (625+0) s cnf 1 (s cnf 1) (bt:788074) |
6 (6+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) |
| C880.blif_0.10_1.00_0_0_out_exact.qdimacs.gz (3) | 800 (799+1) (bt:1258427) |
0 (0+0) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (800+0) |
| incrementer-enc06-uniform-depth-7.qdimacs.gz (3) | 0 (0+0) s cnf 0 (s cnf 0) (bt:1) |
2 (2+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) |
| cube_c5_ser---14_.qdimacs.gz (3) | 27 (27+0) s cnf 0 (s cnf 0) (bt:4597) |
310 (310+0) s cnf 0 (s cnf 0) |
6 (6+0) s cnf 0 (s cnf 0) |
800 (800+0) |
| lut4_2_f2.qdimacs.gz (3) | 4 (4+0) s cnf 0 (s cnf 0) (bt:11381) |
17 (17+0) s cnf 0 (s cnf 0) |
0 (0+0) s cnf 0 (s cnf 0) |
41 (41+0) s cnf 0 (s cnf 0) |
| blocks_enc_2_b3_ser--opt-9_.qdimacs.gz (3) | 1 (1+0) s cnf 1 (s cnf 1) (bt:634) |
4 (3+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) |
| C880.blif_0.10_0.20_0_0_inp_exact.qdimacs.gz (17) | 800 (799+1) (bt:740066) |
800 (800+0) | 800 (770+30) | 800 (800+0) |
| ken.flash^14.C-d4.qdimacs.gz (3) | 800 (798+3) (bt:764836) |
112 (112+0) s cnf 0 (s cnf 0) |
800 (795+5) | 800 (800+0) |
| stmt31_276_328.qdimacs.gz (2) | 800 (798+2) (bt:801280) |
800 (800+0) | 800 (795+5) | 800 (800+0) |
| C432.blif_0.10_0.20_0_0_out_exact.qdimacs.gz (3) | 736 (736+1) s cnf 0 (s cnf 0) (bt:855066) |
4 (4+0) s cnf 0 (s cnf 0) |
1 (1+0) s cnf 0 (s cnf 0) |
174 (174+0) s cnf 0 (s cnf 0) |
| test3_quant_squaring4.qdimacs.gz (7) | 800 (799+1) (bt:286637) |
598 (595+2) | 800 (785+15) | 800 (800+0) |
| cube_c5_ser--opt-15_.qdimacs.gz (3) | 0 (0+0) s cnf 1 (s cnf 1) (bt:166) |
13 (13+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) |
| BLOCKS4iii.7.qdimacs.gz (3) | 0 (0+0) s cnf 1 (s cnf 1) (bt:754) |
492 (491+1) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
10 (10+0) s cnf 1 (s cnf 1) |
| test4_quant_squaring2.qdimacs.gz (3) | 800 (800+0) (bt:379866) |
768 (765+3) | 800 (800+1) | 277 (277+0) s cnf 0 (s cnf 0) |
| biu.mv.xl_ao.bb-b001-p005-IPF02-c02.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004.qdimacs.gz (7) | 0 (0+0) s cnf 0 (s cnf 0) (bt:1) |
1 (1+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) |
| C880.blif_0.10_0.20_0_1_inp_exact.qdimacs.gz (17) | 800 (799+1) (bt:795106) |
800 (800+0) | 800 (772+28) | 800 (800+0) |
| s3330_1_70.qdimacs.gz (3) | 17 (17+0) s cnf 1 (s cnf 1) (bt:9907) |
6 (6+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) |
| stmt41_286_385.qdimacs.gz (2) | 720 (719+2) s cnf 0 (s cnf 0) (bt:647786) |
800 (800+0) | 800 (796+4) | 800 (800+0) |
| ev-pr-8x8-5-7-0-1-2-lg.qdimacs.gz (5) | 0 (0+0) s cnf 0 (s cnf 0) (bt:115) |
16 (16+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) |
| biu.mv.xl_ao.bb-b003-p020-IPF01-c05.blif-biu.inv.prop.bb-bmc.conf01.01X-QBF.BB1-Zi.BB2-01X.BB3-01X.with-IOC.unfold-004.qdimacs.gz (9) | 0 (0+0) s cnf 0 (s cnf 0) (bt:1) |
1 (1+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) |
| biu.mv.xl_ao.bb-b001-p010-MIF05-c04.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004.qdimacs.gz (7) | 0 (0+0) s cnf 1 (s cnf 1) (bt:106) |
1 (1+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) |
| stmt47_340_389.qdimacs.gz (2) | 571 (569+2) s cnf 0 (s cnf 0) (bt:481814) |
800 (800+0) | 800 (797+3) | 800 (800+0) |
| test1_quant_squaring3.qdimacs.gz (5) | 800 (800+0) (bt:1362095) |
578 (576+2) | 800 (799+1) | 800 (800+0) |
| counter_r_8.qdimacs.gz (5) | 6 (6+0) s cnf 1 (s cnf 1) (bt:13454) |
800 (800+0) | 1 (1+0) s cnf 1 (s cnf 1) |
3 (3+0) s cnf 1 (s cnf 1) |
| test1_quant3.qdimacs.gz (3) | 800 (799+1) (bt:690228) |
503 (501+2) | 800 (799+1) | 800 (800+0) |
| biu.mv.xl_ao.bb-b001-p010-MIF03-c10.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-005.qdimacs.gz (9) | 0 (0+0) s cnf 1 (s cnf 1) (bt:147) |
99 (99+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) |
| s1269_d2_s.qdimacs.gz (3) | 0 (0+0) s cnf 1 (s cnf 1) (bt:317) |
1 (1+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) |
| s1196_d2_s.qdimacs.gz (3) | 0 (0+0) s cnf 1 (s cnf 1) (bt:645) |
1 (1+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) |
| C5315.blif_0.10_1.00_0_0_inp_exact.qdimacs.gz (3) | 19 (19+0) s cnf 0 (s cnf 0) (bt:9) |
2 (2+0) s cnf 0 (s cnf 0) |
6 (5+0) s cnf 0 (s cnf 0) |
20 (20+0) s cnf 0 (s cnf 0) |
| test4_quant4.qdimacs.gz (3) | 800 (800+0) (bt:141160) |
623 (620+3) | 800 (800+1) | 800 (800+0) |
| C880.blif_0.10_1.00_0_0_inp_exact.qdimacs.gz (3) | 718 (717+1) s cnf 0 (s cnf 0) (bt:712357) |
80 (80+0) s cnf 0 (s cnf 0) |
134 (134+0) s cnf 0 (s cnf 0) |
617 (617+0) s cnf 0 (s cnf 0) |
| test5_quant5.qdimacs.gz (3) | 2 (2+0) s cnf 1 (s cnf 1) (bt:1458) |
639 (636+3) | 174 (174+0) s cnf 1 (s cnf 1) |
22 (22+0) s cnf 1 (s cnf 1) |
| ev-pr-4x4-9-3-0-0-1-lg.qdimacs.gz (9) | 36 (36+0) s cnf 1 (s cnf 1) (bt:10269) |
2 (2+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
1 (1+0) s cnf 1 (s cnf 1) |
| C5315.blif_0.10_0.20_0_1_inp_exact.qdimacs.gz (29) | 441 (438+2) (bt:332645) |
6 (6+0) s cnf 1 (s cnf 1) |
800 (797+3) | 800 (800+0) |
| C5315.blif_0.10_0.20_0_0_inp_exact.qdimacs.gz (29) | 761 (755+6) (bt:445729) |
800 (799+1) | 800 (794+6) | 800 (800+0) |
| test1_quant_squaring2.qdimacs.gz (3) | 800 (799+1) (bt:852394) |
445 (443+2) | 800 (799+1) | 800 (800+0) |
| eijk.S382.S-f4.qdimacs.gz (3) | 800 (798+2) (bt:350643) |
1 (1+0) s cnf 1 (s cnf 1) |
800 (796+4) | 800 (800+0) |
| C5315.blif_0.10_1.00_0_0_out_exact.qdimacs.gz (3) | 800 (799+1) (bt:1094283) |
2 (2+0) s cnf 0 (s cnf 0) |
3 (3+0) s cnf 0 (s cnf 0) |
800 (800+0) |
| s641_d3_s.qdimacs.gz (3) | 1 (1+0) s cnf 1 (s cnf 1) (bt:1493) |
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) |
| C5315.blif_0.10_0.20_0_1_out_exact.qdimacs.gz (3) | 558 (552+6) (bt:343305) |
800 (800+0) | 800 (795+5) | 800 (800+0) |
| stmt47_290_340.qdimacs.gz (2) | 40 (40+0) s cnf 0 (s cnf 0) (bt:56186) |
800 (800+0) | 377 (375+2) s cnf 0 (s cnf 0) |
800 (800+0) |
| adder-12-unsat.qdimacs.gz (3) | 800 (800+0) (bt:725003) |
800 (800+0) | 800 (799+1) | 800 (800+0) |
| C5315.blif_0.10_0.20_0_0_out_exact.qdimacs.gz (3) | 444 (439+5) (bt:323993) |
800 (800+0) | 631 (625+6) | 800 (800+0) |
| sortnetsort8.v.stepl.008.qdimacs.gz (3) | 800 (800+0) (bt:557177) |
327 (326+1) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
800 (800+0) |
| b11_C_1_14.qdimacs.gz (3) | 19 (18+0) s cnf 1 (s cnf 1) (bt:8293) |
67 (67+1) s cnf 1 (s cnf 1) |
19 (19+0) s cnf 1 (s cnf 1) |
1 (1+0) s cnf 1 (s cnf 1) |
| biu.mv.xl_ao.bb-b003-p020-MIF02-c01.blif-biu.inv.prop.bb-bmc.with-IOC.unfold-005.qdimacs.gz (11) | 800 (798+2) (bt:257219) |
800 (800+0) | 0 (0+0) s cnf 0 (s cnf 0) |
4 (4+0) s cnf 0 (s cnf 0) |
| test3_quant2.qdimacs.gz (3) | 624 (624+0) s cnf 0 (s cnf 0) (bt:76671) |
800 (797+3) | 228 (228+0) s cnf 0 (s cnf 0) |
6 (6+0) s cnf 0 (s cnf 0) |
| test2_quant2.qdimacs.gz (3) | 800 (798+2) (bt:474388) |
450 (449+1) | 800 (796+4) | 800 (800+0) |
| stmt17_70_82.qdimacs.gz (2) | 800 (797+3) (bt:556354) |
173 (172+0) s cnf 1 (s cnf 1) |
800 (791+9) | 800 (800+0) |
| s713_d3_s.qdimacs.gz (3) | 1 (1+0) s cnf 1 (s cnf 1) (bt:1485) |
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) |
| k_branch_n-10.qdimacs.gz (15) | 4 (4+0) s cnf 1 (s cnf 1) (bt:914) |
800 (800+0) | 64 (61+3) s cnf 1 (s cnf 1) |
15 (15+0) s cnf 1 (s cnf 1) |
| vis.prodcell^24.E-f3.qdimacs.gz (3) | 800 (798+2) (bt:411337) |
5 (4+0) s cnf 1 (s cnf 1) |
800 (796+4) | 800 (800+0) |
| test2_quant_squaring2.qdimacs.gz (3) | 800 (798+2) (bt:505556) |
450 (448+1) | 800 (797+3) | 800 (800+0) |
| s5378_1_0.qdimacs.gz (3) | 800 (800+0) (bt:331059) |
141 (141+1) s cnf 1 (s cnf 1) |
4 (4+0) s cnf 1 (s cnf 1) |
7 (7+0) s cnf 1 (s cnf 1) |
| jnh205-90.qdimacs.gz (3) | 4 (4+0) s cnf 0 (s cnf 0) (bt:2920) |
1 (1+0) s cnf 0 (s cnf 0) |
0 (0+0) s cnf 0 (s cnf 0) |
1 (1+0) s cnf 0 (s cnf 0) |
| k_branch_p-10.qdimacs.gz (15) | 0 (0+0) s cnf 0 (s cnf 0) (bt:142) |
800 (800+1) | 1 (1+0) s cnf 0 (s cnf 0) |
0 (0+0) s cnf 0 (s cnf 0) |
| ii8a3-90.qdimacs.gz (3) | 2 (2+0) s cnf 0 (s cnf 0) (bt:1567) |
100 (99+1) s cnf 0 (s cnf 0) |
5 (5+0) s cnf 0 (s cnf 0) |
14 (14+0) s cnf 0 (s cnf 0) |
| cmu.dme1.B-f4.qdimacs.gz (3) | 546 (544+2) (bt:473086) |
2 (2+0) s cnf 1 (s cnf 1) |
769 (763+6) | 800 (800+0) |
| ii32c1-50.qdimacs.gz (3) | 0 (0+0) s cnf 1 (s cnf 1) (bt: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 cnf 1) |
| stmt17_74_78.qdimacs.gz (2) | 800 (797+3) (bt:595496) |
113 (113+0) s cnf 1 (s cnf 1) |
800 (793+8) | 800 (800+0) |
| BLOCKS4ii.7.2.qdimacs.gz (3) | 1 (1+0) s cnf 0 (s cnf 0) (bt:1461) |
5 (5+0) s cnf 0 (s cnf 0) |
0 (0+0) s cnf 0 (s cnf 0) |
5 (5+0) s cnf 0 (s cnf 0) |
| sortnetsort10.v.stepl.012.qdimacs.gz (3) | 800 (800+0) (bt:395422) |
800 (799+1) | 7 (7+0) s cnf 1 (s cnf 1) |
800 (800+0) |
| uclid-pipe3b.qdimacs.gz (6) | 800 (791+9) (bt:155516) |
2 (2+0) s cnf 0 (s cnf 0) |
800 (794+6) | 800 (800+0) |
| irst.dme4.B-d4.qdimacs.gz (3) | 0 (0+0) s cnf 1 (s cnf 1) (bt:120) |
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) |
| cube_c7_ser---23_.qdimacs.gz (3) | 800 (799+1) (bt:461144) |
800 (799+1) | 183 (183+0) s cnf 0 (s cnf 0) |
800 (800+0) |
| b17_C_1_163.qdimacs.gz (3) | 248 (247+1) s cnf 1 (s cnf 1) (bt:32769) |
414 (413+2) | 197 (194+3) s cnf 1 (s cnf 1) |
6 (6+0) s cnf 1 (s cnf 1) |
| s713_d4_s.qdimacs.gz (3) | 2 (2+0) s cnf 1 (s cnf 1) (bt:1373) |
3 (3+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) |
| emptyroom_e4_par---21_.qdimacs.gz (3) | 800 (799+1) (bt:735779) |
119 (119+0) s cnf 0 (s cnf 0) |
9 (9+0) s cnf 0 (s cnf 0) |
800 (800+0) |
| cube_c7_ser--opt-24_.qdimacs.gz (3) | 53 (53+0) s cnf 1 (s cnf 1) (bt:48417) |
211 (210+0) s cnf 1 (s cnf 1) |
1 (1+0) s cnf 1 (s cnf 1) |
14 (14+0) s cnf 1 (s cnf 1) |
| cmu.periodic.N-f4.qdimacs.gz (3) | 383 (377+7) (bt:120667) |
4 (3+0) s cnf 1 (s cnf 1) |
800 (793+7) | 800 (800+0) |
| stmt41_160_235.qdimacs.gz (2) | 340 (340+1) s cnf 0 (s cnf 0) (bt:312196) |
800 (800+0) | 800 (796+4) | 800 (800+0) |
| sortnetsort9.v.stepl.012.qdimacs.gz (3) | 800 (799+1) (bt:457887) |
800 (799+1) | 3 (3+0) s cnf 1 (s cnf 1) |
800 (800+0) |
| emptyroom_e4_par--opt-22_.qdimacs.gz (3) | 800 (799+1) (bt:793763) |
655 (654+1) s cnf 1 (s cnf 1) |
18 (18+0) s cnf 1 (s cnf 1) |
800 (800+0) |
| ethernet-fixpoint-3.qdimacs.gz (2) | 800 (798+2) (bt:453737) |
540 (538+1) | 800 (794+6) | 800 (800+0) |
| c6_BMC_p2_k64.qdimacs.gz (3) | 0 (0+0) s cnf 0 (s cnf 0) (bt:5) |
10 (10+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) |
| adder-14-unsat.qdimacs.gz (3) | 800 (800+0) (bt:498501) |
800 (800+0) | 800 (799+1) | 800 (800+0) |
| cache-coherence-2-fixpoint-5.qdimacs.gz (2) | 800 (796+4) (bt:301858) |
800 (798+2) | 800 (793+7) | 800 (800+0) |
| W4-Umbrella_tbm_21.tex.moduleQ3.6S.000001.qdimacs.gz (18) | 195 (194+1) s cnf 1 (s cnf 1) (bt:73379) |
800 (799+1) | 800 (791+9) | 231 (231+0) s cnf 1 (s cnf 1) |
| Core1108_tbm_02.tex.moduleQ3.2S.000098.qdimacs.gz (18) | 45 (45+0) s cnf 0 (s cnf 0) (bt:10901) |
800 (800+1) | 800 (787+13) | 18 (18+0) s cnf 0 (s cnf 0) |
| Core1108_tbm_03.tex.module.000034.qdimacs.gz (18) | 108 (108+1) s cnf 1 (s cnf 1) (bt:125495) |
800 (800+0) | 800 (787+13) | 83 (83+0) s cnf 1 (s cnf 1) |
| nusmv.tcas^2.B-f2.qdimacs.gz (3) | 703 (698+5) (bt:341997) |
3 (3+0) s cnf 1 (s cnf 1) |
800 (796+4) | 800 (800+0) |
| stmt17_82_86.qdimacs.gz (2) | 800 (797+3) (bt:483159) |
295 (295+0) s cnf 1 (s cnf 1) |
800 (794+6) | 800 (800+0) |
| Umbrella_tbm_05.tex.module.000011.qdimacs.gz (18) | 800 (795+5) (bt:411788) |
800 (800+0) | 800 (782+18) | 159 (159+0) s cnf 1 (s cnf 1) |
| Core1108_tbm_02.tex.moduleQ3.2S.000099.qdimacs.gz (18) | 44 (43+0) s cnf 0 (s cnf 0) (bt:13815) |
7 (7+0) s cnf 0 (s cnf 0) |
800 (785+15) | 17 (17+0) s cnf 0 (s cnf 0) |
| cube_c9_par---10_.qdimacs.gz (3) | 2 (2+0) s cnf 0 (s cnf 0) (bt:2594) |
10 (10+0) s cnf 0 (s cnf 0) |
0 (0+0) s cnf 0 (s cnf 0) |
3 (3+0) s cnf 0 (s cnf 0) |
| incrementer-enc02-uniform-depth-17.qdimacs.gz (3) | 0 (0+0) s cnf 0 (s cnf 0) (bt:1) |
4 (4+0) s cnf 0 (s cnf 0) |
0 (0+0) s cnf 0 (s cnf 0) |
800 (800+0) |
| s1196_1_5.qdimacs.gz (3) | 616 (615+2) (bt:75682) |
173 (173+1) s cnf 1 (s cnf 1) |
197 (195+2) | 134 (134+0) s cnf 1 (s cnf 1) |
| Core1108_tbm_21.tex.moduleQ3.2S.000027.qdimacs.gz (18) | 284 (282+1) s cnf 1 (s cnf 1) (bt:129907) |
800 (800+0) | 800 (784+16) | 104 (104+0) s cnf 1 (s cnf 1) |
| tlc02-uniform-depth-46.qdimacs.gz (1) | 0 (0+0) s cnf 0 (s cnf 0) (bt:1) |
7 (7+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) |
| incrementer-enc09-nonuniform-depth-10.qdimacs.gz (13) | 0 (0+0) s cnf 0 (s cnf 0) (bt:1) |
3 (3+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) |
| b22_C_2_12.qdimacs.gz (3) | 683 (681+2) (bt:198783) |
800 (799+1) | 348 (346+2) | 800 (800+0) |
| stmt19_83_91.qdimacs.gz (2) | 800 (798+2) (bt:425723) |
173 (173+0) s cnf 1 (s cnf 1) |
775 (768+7) | 800 (800+0) |
| adder-6-sat.qdimacs.gz (4) | 800 (797+3) (bt:38834) |
800 (800+0) | 800 (771+29) | 800 (800+0) |
| W4-Umbrella_tbm_05.tex.moduleQ3.8S.000001.qdimacs.gz (18) | 55 (55+0) s cnf 0 (s cnf 0) (bt:11617) |
29 (29+0) s cnf 0 (s cnf 0) |
800 (782+18) | 3 (3+0) s cnf 0 (s cnf 0) |
| W5-Umbrella_tbm_05.tex.moduleQ3.8S.000001.qdimacs.gz (18) | 800 (795+5) (bt:260024) |
800 (800+1) | 800 (786+14) | 222 (222+0) s cnf 1 (s cnf 1) |
| vis.prodcell^23.E-f4.qdimacs.gz (3) | 800 (797+3) (bt:487067) |
11 (10+1) s cnf 1 (s cnf 1) |
800 (796+4) | 800 (800+0) |
| b14_C_3_105.qdimacs.gz (3) | 800 (800+0) (bt:220498) |
251 (250+1) | 111 (110+1) | 800 (800+0) |
| s713_d5_s.qdimacs.gz (3) | 6 (6+0) s cnf 1 (s cnf 1) (bt:3423) |
4 (4+0) s cnf 1 (s cnf 1) |
2 (2+0) s cnf 1 (s cnf 1) |
32 (32+0) s cnf 1 (s cnf 1) |
| biu.mv.xl_ao.bb-b003-p020-IPF01-c05.blif-biu.inv.prop.bb-bmc.conf02.01X-QBF.BB1-01X.BB2-Zi.BB3-01X.with-IOC.unfold-007.qdimacs.gz (15) | 800 (799+1) (bt:153395) |
800 (800+1) | 0 (0+0) s cnf 0 (s cnf 0) |
1 (1+0) s cnf 0 (s cnf 0) |
| Umbrella_tbm_25.tex.module.000099.qdimacs.gz (18) | 23 (23+0) s cnf 0 (s cnf 0) (bt:5991) |
2 (2+0) s cnf 0 (s cnf 0) |
800 (792+8) | 1 (1+0) s cnf 0 (s cnf 0) |
| s05378_PR_2_50.qdimacs.gz (3) | 0 (0+0) s cnf 1 (s cnf 1) (bt:31) |
9 (8+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) |
| stmt27_149_224.qdimacs.gz (2) | 63 (63+0) s cnf 0 (s cnf 0) (bt:51101) |
308 (308+0) s cnf 0 (s cnf 0) |
800 (797+3) | 800 (800+0) |
| s298_d10_s.qdimacs.gz (3) | 5 (5+0) s cnf 1 (s cnf 1) (bt:2843) |
4 (4+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) |
| adder-16-unsat.qdimacs.gz (3) | 800 (800+0) (bt:340905) |
800 (800+1) | 680 (678+1) | 800 (800+0) |
| Core1108_tbm_21.tex.moduleQ3.2S.000024.qdimacs.gz (18) | 87 (86+0) s cnf 0 (s cnf 0) (bt:18001) |
271 (271+0) s cnf 0 (s cnf 0) |
800 (782+18) | 17 (17+0) s cnf 0 (s cnf 0) |
| stmt23_92_96.qdimacs.gz (2) | 800 (797+3) (bt:441917) |
332 (331+1) s cnf 1 (s cnf 1) |
800 (792+8) | 800 (800+0) |
| ev-pr-4x4-5-3-0-0-1-s.qdimacs.gz (5) | 800 (798+2) (bt:89297) |
204 (203+1) | 800 (798+2) | 800 (800+0) |
| W3-Umbrella_tbm_21.tex.moduleQ3.6S.000001.qdimacs.gz (18) | 4 (4+0) s cnf 0 (s cnf 0) (bt:809) |
4 (4+0) s cnf 0 (s cnf 0) |
800 (787+13) | 27 (27+0) s cnf 0 (s cnf 0) |
| connect_5x4_3_R.qdimacs.gz (19) | 41 (41+0) s cnf 0 (s cnf 0) (bt:4179) |
99 (99+1) s cnf 0 (s cnf 0) |
800 (732+68) | 11 (11+0) s cnf 0 (s cnf 0) |
| ii32c2-90.qdimacs.gz (3) | 1 (1+0) s cnf 1 (s cnf 1) (bt:501) |
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 cnf 1) |
| s09234_PR_9_20.qdimacs.gz (3) | 0 (0+0) s cnf 1 (s cnf 1) (bt:9) |
361 (359+1) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| Umbrella_tbm_05.tex.module.000025.qdimacs.gz (18) | 800 (795+5) (bt:383684) |
800 (800+0) | 800 (785+15) | 162 (161+0) s cnf 1 (s cnf 1) |
| W5-Umbrella_tbm_25.tex.moduleQ3.7S.000003.qdimacs.gz (18) | 397 (395+2) s cnf 1 (s cnf 1) (bt:102181) |
800 (799+1) | 800 (788+12) | 329 (329+0) s cnf 1 (s cnf 1) |
| TOILET16.1.iv.32.qdimacs.gz (1) | 2 (2+0) s cnf 1 (s cnf 1) (bt:1) |
13 (13+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) |
| s38584_3_238.qdimacs.gz (3) | 152 (151+1) (bt:13544) |
267 (265+1) | 280 (279+1) | 800 (800+0) |
| stmt17_94_98.qdimacs.gz (2) | 800 (798+3) (bt:395178) |
299 (299+1) s cnf 1 (s cnf 1) |
800 (792+8) | 800 (800+0) |
| nusmv.tcas-t^6.B-f3.qdimacs.gz (3) | 800 (797+3) (bt:283077) |
8 (7+0) s cnf 1 (s cnf 1) |
800 (795+5) | 800 (800+0) |
| k6_4_3.qdimacs.gz (3) | 800 (799+1) (bt:112798) |
800 (799+1) | 800 (798+3) | 800 (800+0) |
| C6288.blif_0.10_0.20_0_1_out_exact.qdimacs.gz (3) | 800 (795+5) (bt:384716) |
800 (800+0) | 458 (454+4) | 800 (800+0) |
| k_ph_p-17.qdimacs.gz (3) | 800 (800+0) (bt:3172) |
800 (799+1) | 800 (799+1) | 800 (800+0) |
| C6288.blif_0.10_0.20_0_0_out_exact.qdimacs.gz (3) | 800 (796+4) (bt:308936) |
800 (800+0) | 682 (676+6) | 800 (800+0) |
| C6288.blif_0.10_1.00_0_1_out_exact.qdimacs.gz (3) | 8 (8+0) s cnf 1 (s cnf 1) (bt:6145) |
3 (3+0) s cnf 1 (s cnf 1) |
6 (6+0) s cnf 1 (s cnf 1) |
800 (800+0) |
| ii8a4-00.qdimacs.gz (3) | 0 (0+0) s cnf 1 (s cnf 1) (bt:116) |
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 cnf 1) |
| C6288.blif_0.10_1.00_0_1_inp_exact.qdimacs.gz (3) | 6 (6+0) s cnf 1 (s cnf 1) (bt:4609) |
3 (3+0) s cnf 1 (s cnf 1) |
4 (4+0) s cnf 1 (s cnf 1) |
800 (800+0) |
| C6288.blif_0.10_1.00_0_0_inp_exact.qdimacs.gz (3) | 800 (800+0) (bt:64717) |
800 (799+1) | 800 (800+0) | 800 (800+0) |
| C6288.blif_0.10_0.20_0_1_inp_exact.qdimacs.gz (13) | 800 (796+4) (bt:357407) |
800 (800+0) | 800 (797+4) | 800 (800+0) |
| k_branch_p-13.qdimacs.gz (25) | 72 (72+0) s cnf 0 (s cnf 0) (bt:3057) |
800 (799+1) | 6 (6+0) s cnf 0 (s cnf 0) |
0 (0+0) s cnf 0 (s cnf 0) |
| s641_d6_s.qdimacs.gz (3) | 11 (11+0) s cnf 1 (s cnf 1) (bt:4322) |
7 (7+0) s cnf 1 (s cnf 1) |
5 (5+0) s cnf 1 (s cnf 1) |
6 (6+0) s cnf 1 (s cnf 1) |
| k_ph_n-18.qdimacs.gz (3) | 1 (1+0) s cnf 1 (s cnf 1) (bt:308) |
800 (799+1) | 10 (9+0) s cnf 1 (s cnf 1) |
2 (2+0) s cnf 1 (s cnf 1) |
| Umbrella_tbm_14.tex.moduleQ2.1S.000792.qdimacs.gz (12) | 2 (2+0) s cnf 0 (s cnf 0) (bt:166) |
800 (799+1) | 493 (485+8) s cnf 0 (s cnf 0) |
0 (0+0) s cnf 0 (s cnf 0) |
| s298_d13_s.qdimacs.gz (3) | 14 (14+0) s cnf 1 (s cnf 1) (bt:4256) |
8 (7+0) s cnf 1 (s cnf 1) |
9 (9+0) s cnf 1 (s cnf 1) |
134 (134+0) s cnf 1 (s cnf 1) |
| incrementer-enc03-uniform-depth-24.qdimacs.gz (3) | 0 (0+0) s cnf 0 (s cnf 0) (bt:1) |
6 (6+0) s cnf 0 (s cnf 0) |
0 (0+0) s cnf 0 (s cnf 0) |
800 (800+0) |
| nusmv.tcas^4.B-f3.qdimacs.gz (3) | 800 (796+4) (bt:228707) |
8 (7+0) s cnf 1 (s cnf 1) |
773 (768+5) | 800 (800+0) |
| W4-Umbrella_tbm_26.tex.moduleQ3.7S.000003.qdimacs.gz (18) | 14 (14+0) s cnf 0 (s cnf 0) (bt:2270) |
8 (7+0) s cnf 0 (s cnf 0) |
800 (774+26) | 7 (7+0) s cnf 0 (s cnf 0) |
| ev-pr-4x4-17-3-0-0-1-lg.qdimacs.gz (17) | 800 (800+1) (bt:33769) |
9 (9+0) s cnf 1 (s cnf 1) |
1 (0+0) s cnf 1 (s cnf 1) |
609 (609+0) s cnf 1 (s cnf 1) |
| s820_d6_s.qdimacs.gz (3) | 10 (10+0) s cnf 1 (s cnf 1) (bt:4090) |
7 (7+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) |
| k_ph_p-18.qdimacs.gz (3) | 800 (800+0) (bt:3820) |
800 (799+1) | 800 (799+1) | 800 (800+0) |
| emptyroom_e4_ser--opt-44_.qdimacs.gz (3) | 800 (799+1) (bt:471569) |
800 (799+1) | 125 (124+0) s cnf 1 (s cnf 1) |
800 (800+0) |
| s1196_d3_u.qdimacs.gz (3) | 34 (34+0) s cnf 0 (s cnf 0) (bt:11585) |
72 (72+0) s cnf 0 (s cnf 0) |
294 (271+22) | 800 (800+0) |
| Core1108_tbm_09.tex.moduleQ3.2S.000010.qdimacs.gz (18) | 29 (29+0) s cnf 0 (s cnf 0) (bt:1610) |
174 (174+0) s cnf 0 (s cnf 0) |
800 (780+20) | 14 (14+0) s cnf 0 (s cnf 0) |
| k_branch_n-14.qdimacs.gz (27) | 800 (799+1) (bt:11117) |
800 (799+1) | 800 (782+18) | 800 (800+0) |
| ev-pr-8x8-7-7-0-1-2-lg.qdimacs.gz (7) | 94 (94+0) s cnf 0 (s cnf 0) (bt:4790) |
78 (77+1) s cnf 0 (s cnf 0) |
10 (10+0) s cnf 0 (s cnf 0) |
3 (3+0) s cnf 0 (s cnf 0) |
| Umbrella_tbm_26.tex.moduleQ3.2S.000037.qdimacs.gz (18) | 109 (109+0) s cnf 0 (s cnf 0) (bt:13842) |
800 (799+1) | 800 (780+20) | 38 (38+0) s cnf 0 (s cnf 0) |
| s641_d7_u.qdimacs.gz (3) | 22 (22+0) s cnf 0 (s cnf 0) (bt:6454) |
22 (22+0) s cnf 0 (s cnf 0) |
53 (51+2) s cnf 0 (s cnf 0) |
298 (298+0) s cnf 0 (s cnf 0) |
| sortnetsort10.AE.stepl.008.qdimacs.gz (2) | 800 (800+1) (bt:140260) |
800 (799+1) | 800 (797+3) | 42 (42+0) s cnf 0 (s cnf 0) |
| k_ph_n-20.qdimacs.gz (3) | 10 (10+0) s cnf 1 (s cnf 1) (bt:1234) |
800 (799+1) | 7 (7+0) s cnf 1 (s cnf 1) |
4 (4+0) s cnf 1 (s cnf 1) |
| tlc03-nonuniform-depth-82.qdimacs.gz (142) | 2 (2+0) s cnf 0 (s cnf 0) (bt:4) |
5 (5+0) | 0 (0+0) s cnf 0 (s cnf 0) |
0 (0+0) s cnf 0 (s cnf 0) |
| Umbrella_tbm_26.tex.moduleQ3.2S.000020.qdimacs.gz (18) | 274 (273+1) s cnf 0 (s cnf 0) (bt:33144) |
72 (72+0) s cnf 0 (s cnf 0) |
800 (771+29) | 55 (55+0) s cnf 0 (s cnf 0) |
| s1196_d4_u.qdimacs.gz (3) | 28 (28+0) s cnf 0 (s cnf 0) (bt:7646) |
95 (94+0) s cnf 0 (s cnf 0) |
269 (245+24) | 800 (800+0) |
| c5_BMC_p1_k4.qdimacs.gz (3) | 0 (0+0) s cnf 1 (s cnf 1) (bt:91) |
10 (9+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) |
| connect_6x5_5_R.qdimacs.gz (29) | 800 (799+1) (bt:37804) |
228 (227+1) | 800 (727+73) | 800 (800+0) |
| k_branch_p-15.qdimacs.gz (29) | 527 (526+1) s cnf 0 (s cnf 0) (bt:9825) |
800 (799+1) | 48 (47+1) s cnf 0 (s cnf 0) |
800 (800+0) |
| tlc02-uniform-depth-84.qdimacs.gz (1) | 1 (1+0) s cnf 0 (s cnf 0) (bt:1) |
4 (4+0) | 1 (1+0) s cnf 0 (s cnf 0) |
2 (2+0) s cnf 0 (s cnf 0) |
| ev-pr-6x6-11-5-0-1-2-lg.qdimacs.gz (11) | 800 (800+0) (bt:20078) |
284 (283+1) | 800 (792+8) | 51 (50+0) s cnf 0 (s cnf 0) |
| s1196_d5_u.qdimacs.gz (3) | 41 (41+0) s cnf 0 (s cnf 0) (bt:8362) |
134 (133+0) s cnf 0 (s cnf 0) |
296 (250+46) | 800 (800+0) |
| s298_d16_s.qdimacs.gz (3) | 800 (799+1) (bt:129949) |
10 (10+0) s cnf 1 (s cnf 1) |
526 (524+2) s cnf 1 (s cnf 1) |
800 (800+0) |
| b21_C_3_206.qdimacs.gz (3) | 800 (800+0) (bt:69467) |
152 (150+1) | 164 (163+1) | 800 (800+0) |
| b04_C_2_20.qdimacs.gz (3) | 133 (132+1) (bt:7308) |
183 (182+1) | 209 (207+1) | 800 (800+0) |
| ev-pr-4x4-7-3-0-0-1-s.qdimacs.gz (7) | 800 (799+1) (bt:72598) |
156 (155+1) | 800 (798+2) | 800 (800+0) |
| s820_d8_s.qdimacs.gz (3) | 35 (35+0) s cnf 1 (s cnf 1) (bt:6209) |
13 (13+0) s cnf 1 (s cnf 1) |
20 (20+0) s cnf 1 (s cnf 1) |
447 (446+0) s cnf 1 (s cnf 1) |
| s386_d12_u.qdimacs.gz (3) | 31 (31+0) s cnf 0 (s cnf 0) (bt:5815) |
8 (8+0) s cnf 0 (s cnf 0) |
20 (20+0) s cnf 0 (s cnf 0) |
382 (382+0) s cnf 0 (s cnf 0) |
| k12_2_2.qdimacs.gz (3) | 800 (799+1) (bt:83007) |
800 (799+1) | 800 (799+1) | 800 (800+0) |
| sortnetsort10.AE.stepl.010.qdimacs.gz (2) | 800 (800+0) (bt:104136) |
800 (798+2) | 800 (798+2) | 36 (36+0) s cnf 0 (s cnf 0) |
| s820_d7_s.qdimacs.gz (3) | 71 (71+0) s cnf 1 (s cnf 1) (bt:13613) |
9 (9+0) s cnf 1 (s cnf 1) |
24 (24+0) s cnf 1 (s cnf 1) |
288 (288+0) s cnf 1 (s cnf 1) |
| s298_d22_u.qdimacs.gz (3) | 69 (69+0) s cnf 0 (s cnf 0) (bt:7977) |
28 (28+0) s cnf 0 (s cnf 0) |
58 (58+0) s cnf 0 (s cnf 0) |
800 (800+0) |
| s298_d21_u.qdimacs.gz (3) | 63 (63+0) s cnf 0 (s cnf 0) (bt:7730) |
27 (27+0) s cnf 0 (s cnf 0) |
57 (56+1) s cnf 0 (s cnf 0) |
800 (800+0) |
| s499_d15_s.qdimacs.gz (3) | 63 (63+0) s cnf 1 (s cnf 1) (bt:9331) |
11 (11+0) s cnf 1 (s cnf 1) |
39 (39+0) s cnf 1 (s cnf 1) |
800 (800+0) |
| k_ph_n-19.qdimacs.gz (3) | 9 (9+0) s cnf 1 (s cnf 1) (bt:1050) |
800 (799+1) | 49 (48+1) s cnf 1 (s cnf 1) |
9 (9+0) s cnf 1 (s cnf 1) |
| biu.mv.xl_ao.bb-b003-p020-IPF01-c05.blif-biu.inv.prop.bb-bmc.with-IOC.unfold-009.qdimacs.gz (19) | 800 (799+1) (bt:56463) |
800 (799+1) | 0 (0+0) s cnf 0 (s cnf 0) |
800 (800+0) |
| ev-pr-6x6-13-5-0-1-2-lg.qdimacs.gz (13) | 800 (800+0) (bt:16951) |
207 (206+1) | 800 (793+7) | 340 (340+0) s cnf 0 (s cnf 0) |
| s1196_d6_u.qdimacs.gz (3) | 106 (106+0) s cnf 0 (s cnf 0) (bt:13879) |
164 (163+0) s cnf 0 (s cnf 0) |
167 (152+15) | 800 (800+0) |
| k12_2_3.qdimacs.gz (3) | 800 (800+0) (bt:66677) |
800 (799+1) | 800 (798+2) | 800 (800+0) |
| ev-pr-8x8-9-7-0-1-2-lg.qdimacs.gz (9) | 708 (708+0) s cnf 0 (s cnf 0) (bt:15672) |
173 (171+1) | 55 (54+1) s cnf 0 (s cnf 0) |
31 (31+0) s cnf 0 (s cnf 0) |
| s1196_d7_u.qdimacs.gz (3) | 87 (87+0) s cnf 0 (s cnf 0) (bt:11325) |
179 (179+0) s cnf 0 (s cnf 0) |
208 (179+29) | 800 (800+0) |
| b20_PR_5_10.qdimacs.gz (3) | 170 (169+1) (bt:11636) |
26 (25+1) s cnf 1 (s cnf 1) |
129 (128+1) | 800 (800+0) |
| k_ph_n-21.qdimacs.gz (3) | 16 (16+0) s cnf 1 (s cnf 1) (bt:1438) |
800 (799+1) | 57 (56+1) s cnf 1 (s cnf 1) |
26 (26+0) s cnf 1 (s cnf 1) |
| tlc02-uniform-depth-119.qdimacs.gz (1) | 2 (1+0) s cnf 0 (s cnf 0) (bt:1) |
5 (5+0) | 2 (2+0) s cnf 0 (s cnf 0) |
7 (7+0) s cnf 0 (s cnf 0) |
| s298_d24_u.qdimacs.gz (3) | 800 (799+1) (bt:68257) |
33 (33+0) s cnf 0 (s cnf 0) |
800 (798+2) | 800 (800+0) |
| ev-pr-6x6-15-5-0-1-2-lg.qdimacs.gz (15) | 800 (800+0) (bt:8132) |
234 (233+1) | 800 (790+10) | 800 (800+0) |
| blocks_enc_2_b4_ser--opt-26_.qdimacs.gz (3) | 800 (799+1) (bt:54502) |
800 (799+1) | 800 (798+2) | 800 (800+0) |
| adder-10-sat.qdimacs.gz (4) | 800 (799+1) (bt:39652) |
800 (800+0) | 800 (762+38) | 800 (800+0) |
| ev-pr-4x4-11-3-0-0-1-s.qdimacs.gz (11) | 800 (800+1) (bt:21973) |
129 (128+1) | 800 (798+2) | 1 (1+0) s cnf 1 (s cnf 1) |
| ev-pr-8x8-11-7-0-1-2-lg.qdimacs.gz (11) | 800 (800+0) (bt:10428) |
207 (206+1) | 800 (796+4) | 263 (263+0) s cnf 0 (s cnf 0) |
| s1269_d8_s.qdimacs.gz (3) | 348 (348+0) s cnf 1 (s cnf 1) (bt:13145) |
29 (29+0) s cnf 1 (s cnf 1) |
296 (292+3) s cnf 1 (s cnf 1) |
800 (800+0) |
| k12_3_3.qdimacs.gz (3) | 800 (800+0) (bt:39564) |
800 (799+1) | 800 (798+2) | 800 (800+0) |
| c1_BMC_p1_k8.qdimacs.gz (3) | 227 (227+0) s cnf 1 (s cnf 1) (bt:12833) |
41 (40+1) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
20 (20+0) s cnf 1 (s cnf 1) |
| k_branch_n-20.qdimacs.gz (41) | 163 (162+1) (bt:2605) |
800 (799+1) | 800 (773+27) | 800 (800+0) |
| k12_4_2.qdimacs.gz (3) | 800 (800+0) (bt:36030) |
800 (799+1) | 800 (798+2) | 800 (800+0) |
| tlc02-uniform-depth-168.qdimacs.gz (1) | 4 (4+0) s cnf 0 (s cnf 0) (bt:1) |
7 (6+0) | 4 (4+0) s cnf 0 (s cnf 0) |
19 (19+0) s cnf 0 (s cnf 0) |
| adder-12-sat.qdimacs.gz (4) | 800 (799+1) (bt:47211) |
800 (800+0) | 512 (469+43) | 800 (800+0) |
| filesys_fastfat_allocsup.c.qdimacs.gz (3) | 800 (799+1) (bt:115511) |
382 (381+1) | 800 (799+1) | 800 (800+0) |
| cube_c11_ser--opt-42_.qdimacs.gz (3) | 800 (800+0) (bt:118864) |
800 (799+1) | 459 (458+1) s cnf 1 (s cnf 1) |
800 (800+0) |
| filesys_smbmrx_smbxchng.c.qdimacs.gz (3) | 800 (800+0) (bt:407365) |
355 (353+1) | 800 (797+3) | 800 (800+0) |
| filesys_fastfat_easup.c.qdimacs.gz (3) | 800 (799+1) (bt:116793) |
302 (301+1) | 800 (797+3) | 800 (800+0) |
| ev-pr-4x4-13-3-0-0-1-s.qdimacs.gz (13) | 800 (800+0) (bt:14151) |
165 (164+1) | 800 (798+2) | 0 (0+0) s cnf 1 (s cnf 1) |
| audio_ac97_wavepcistream3.cpp.qdimacs.gz (3) | 800 (799+1) (bt:113502) |
475 (474+1) | 153 (152+1) s cnf 0 (s cnf 0) |
800 (800+0) |
| k_branch_p-21.qdimacs.gz (43) | 131 (131+1) (bt:1849) |
800 (799+1) | 800 (670+130) | 800 (800+0) |
| k_branch_n-21.qdimacs.gz (43) | 248 (247+1) (bt:2665) |
800 (799+1) | 800 (786+14) | 800 (800+0) |
| connect_7x6_4_R.qdimacs.gz (43) | 800 (799+1) (bt:5132) |
167 (166+1) | 800 (747+53) | 800 (800+0) |
| s1269_d9_s.qdimacs.gz (3) | 800 (800+0) (bt:21060) |
416 (416+1) s cnf 1 (s cnf 1) |
597 (593+4) | 800 (800+0) |
| c6_BMC_p1_k1024.qdimacs.gz (3) | 26 (26+0) s cnf 1 (s cnf 1) (bt:5765) |
800 (798+2) | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| ev-pr-8x8-13-7-0-1-2-lg.qdimacs.gz (13) | 800 (800+0) (bt:13648) |
230 (228+1) | 800 (796+4) | 800 (800+0) |
| b22_PR_8_20.qdimacs.gz (3) | 160 (159+1) (bt:6612) |
12 (10+1) | 141 (140+1) | 800 (800+0) |
| ring_r6_ser--opt-17_.qdimacs.gz (3) | 242 (242+0) s cnf 1 (s cnf 1) (bt:4121) |
518 (516+2) | 244 (243+0) s cnf 1 (s cnf 1) |
800 (800+0) |
| s1269_d10_s.qdimacs.gz (3) | 800 (800+1) (bt:18943) |
800 (798+2) | 800 (799+1) | 800 (800+0) |
| ev-pr-6x6-5-5-0-1-2-s.qdimacs.gz (5) | 800 (799+1) (bt:13918) |
320 (318+2) | 550 (547+3) | 800 (800+0) |
| tlc02-nonuniform-depth-216.qdimacs.gz (1) | 9 (9+0) s cnf 0 (s cnf 0) (bt:1) |
8 (8+0) | 10 (9+0) s cnf 0 (s cnf 0) |
52 (52+0) s cnf 0 (s cnf 0) |
| s510_d26_s.qdimacs.gz (3) | 800 (800+1) (bt:30103) |
89 (89+1) s cnf 1 (s cnf 1) |
800 (799+1) | 800 (800+0) |
| ev-pr-4x4-15-3-0-0-1-s.qdimacs.gz (15) | 800 (800+0) (bt:9006) |
248 (247+1) | 800 (798+2) | 800 (800+0) |
| c3_BMC_p1_k256.qdimacs.gz (3) | 56 (56+0) s cnf 1 (s cnf 1) (bt:6372) |
800 (798+2) | 5 (5+0) s cnf 1 (s cnf 1) |
62 (62+0) s cnf 1 (s cnf 1) |
| ev-pr-4x4-17-3-0-0-1-s.qdimacs.gz (17) | 800 (800+0) (bt:6918) |
250 (249+2) | 800 (798+2) | 1 (1+0) s cnf 1 (s cnf 1) |
| s3330_d6_s.qdimacs.gz (3) | 800 (800+0) (bt:28170) |
173 (172+1) s cnf 1 (s cnf 1) |
800 (799+1) | 800 (800+0) |
| s510_d33_s.qdimacs.gz (3) | 800 (799+1) (bt:27556) |
148 (147+1) s cnf 1 (s cnf 1) |
800 (799+1) | 800 (800+0) |
| s1269_d13_u.qdimacs.gz (3) | 800 (800+1) (bt:16259) |
800 (799+1) | 800 (799+1) | 800 (800+0) |
| b20_C_3_2.qdimacs.gz (3) | 157 (156+1) (bt:1676) |
436 (434+2) | 800 (799+1) | 800 (800+0) |
| s1269_d15_u.qdimacs.gz (3) | 800 (800+1) (bt:15950) |
800 (799+1) | 800 (799+1) | 800 (800+0) |
| ev-pr-8x8-19-7-0-1-2-lg.qdimacs.gz (19) | 800 (800+0) (bt:4358) |
252 (250+2) | 800 (796+4) | 800 (800+0) |
| audio_ddksynth_voice.cpp.qdimacs.gz (3) | 800 (799+1) (bt:56449) |
507 (505+2) | 800 (798+2) | 800 (800+0) |
| ev-pr-6x6-7-5-0-1-2-s.qdimacs.gz (7) | 800 (799+1) (bt:17250) |
330 (328+2) | 650 (647+2) | 800 (800+0) |
| k14_3_3.qdimacs.gz (3) | 800 (800+0) (bt:23590) |
800 (797+3) | 800 (799+1) | 800 (800+0) |
| filesys_cdfs_namesup.c.qdimacs.gz (3) | 800 (799+1) (bt:37626) |
800 (798+2) | 800 (797+3) | 800 (800+0) |
| s3330_d10_u.qdimacs.gz (3) | 800 (800+0) (bt:16971) |
800 (799+1) | 800 (799+1) | 800 (800+0) |
| s3330_d11_u.qdimacs.gz (3) | 800 (800+1) (bt:15824) |
800 (799+1) | 800 (799+1) | 800 (800+0) |
| s3330_d13_u.qdimacs.gz (3) | 800 (799+1) (bt:12578) |
800 (799+1) | 800 (799+1) | 800 (800+0) |
| connect_9x8_3_R.qdimacs.gz (73) | 4 (3+1) | 471 (468+3) | 800 (786+14) | 800 (800+0) |
| s3330_d14_u.qdimacs.gz (3) | 800 (800+0) (bt:6725) |
800 (800+1) | 800 (799+1) | 800 (800+0) |
| ring_r7_ser---19_.qdimacs.gz (3) | 74 (74+0) s cnf 0 (s cnf 0) (bt:31) |
124 (121+2) | 3 (3+0) s cnf 0 (s cnf 0) |
800 (800+0) |
| c2_Debug_s5_f1_e1_v3.qdimacs.gz (5) | 800 (800+0) (bt:4565) |
89 (87+2) | 800 (798+2) | 800 (800+0) |
| ring_r7_ser--opt-20_.qdimacs.gz (3) | 800 (799+1) (bt:4973) |
121 (119+2) | 800 (800+0) | 177 (176+0) s cnf 1 (s cnf 1) |
| c4_Debug_s3_f1_e2_v3.qdimacs.gz (3) | 800 (799+1) (bt:3832) |
226 (223+3) | 800 (799+1) | 800 (800+0) |
| c4_Debug_s3_f1_e1_v3.qdimacs.gz (3) | 800 (799+1) (bt:4549) |
226 (223+3) | 800 (799+1) | 800 (800+0) |
| AR-fixpoint-2.qdimacs.gz (2) | 800 (799+1) (bt:4714) |
31 (30+1) | 348 (347+1) | 800 (800+0) |
| c4_Debug_s3_f2_e1_v3.qdimacs.gz (3) | 800 (799+1) (bt:4227) |
123 (121+2) | 800 (799+1) | 800 (800+0) |
| c3_Debug_s3_f2_e2_v2.qdimacs.gz (3) | 800 (799+1) | 320 (317+3) | 10 (9+2) | 800 (799+1) |
| TOTAL (276) | solved:133 wins:68 uniq:3 |
solved:137 wins:55 uniq:28 |
solved:128 wins:87 uniq:7 |
solved:129 wins:86 uniq:14 |
| qesto | nbl_gqc | rareqs | depqbf |