c Parsing PB file...
c Converting 5867 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #
c   -- Clauses(.)/Splits(s): .........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[   0]---> Adder-cost: 532   maxlim: 250   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    9530    24793 |    3176       0        0     nan |  0.000 % |
c |       100 |    9488    24659 |    3493      94      343     3.6 |  3.087 % |
c |       251 |    9393    24332 |    3842     227     1023     4.5 |  4.692 % |
c |       476 |    9348    24181 |    4227     444     3481     7.8 |  5.556 % |
c |       813 |    8965    22862 |    4649     701     5863     8.4 | 12.469 % |
c |      1319 |    8604    21621 |    5114    1127    11049     9.8 | 19.383 % |
c |      2079 |    8595    21590 |    5626    1869    35456    19.0 | 19.506 % |
c |      3219 |    8478    21185 |    6189    2970    54496    18.3 | 21.975 % |
c |      4931 |    8394    20895 |    6808    4659    88026    18.9 | 23.581 % |
c |      7493 |    8385    20864 |    7488    7210   154515    21.4 | 23.704 % |
c |     11337 |    8373    20824 |    8237    7164   167403    23.4 | 23.951 % |
c |     17103 |    8367    20804 |    9061    4335    99134    22.9 | 24.074 % |
c |     25753 |    8306    20593 |    9967    8210   196792    24.0 | 25.186 % |
c |     38727 |    8289    20534 |   10964    5718    99935    17.5 | 25.556 % |
c |     58189 |    8289    20534 |   12060    8140   202148    24.8 | 25.556 % |
c |     87383 |    8289    20534 |   13266    6351   128398    20.2 | 25.556 % |
c |    131173 |    8289    20534 |   14593    9360   220471    23.6 | 25.556 % |
c |    196859 |    8289    20534 |   16052    7821   181602    23.2 | 25.556 % |
c |    295385 |    8289    20534 |   17658   16156   492484    30.5 | 25.556 % |
c |    443174 |    8289    20534 |   19424   10968   282487    25.8 | 25.556 % |
c |    664858 |    8289    20534 |   21366   15094   451900    29.9 | 25.556 % |
c |    997384 |    8289    20534 |   23503   21666   777841    35.9 | 25.556 % |
c |   1496172 |    8289    20534 |   25853   19085   620943    32.5 | 25.556 % |
c |   2244357 |    8289    20534 |   28438   20258   538275    26.6 | 25.556 % |
c |   3366633 |    8289    20534 |   31282   19688   528927    26.9 | 25.556 % |
c |   5050044 |    8289    20534 |   34411   21803   538077    24.7 | 25.556 % |
c |   7575162 |    8289    20534 |   37852   25727   712352    27.7 | 25.556 % |
c |  11362838 |    8289    20534 |   41637   21291   698812    32.8 | 25.556 % |
c |  17044352 |    8289    20534 |   45801   23442   779143    33.2 | 25.556 % |
c |  25566621 |    8289    20534 |   50381   25047   739249    29.5 | 25.556 % |
c |  38350025 |    8289    20534 |   55419   44329  1337838    30.2 | 25.556 % |
c |  57525130 |    8289    20534 |   60961   42590  1254738    29.5 | 25.556 % |
c |  86287788 |    8289    20534 |   67057   46949  1293035    27.5 | 25.556 % |
c | 129431777 |    8289    20534 |   73763   44328  1496332    33.8 | 25.556 % |
c | 194147763 |    8289    20534 |   81139   32594   918532    28.2 | 25.556 % |
c | 291221736 |    8289    20534 |   89253   44168  1286388    29.1 | 25.556 % |
c | 436832697 |    8289    20534 |   98178   69716  2072598    29.7 | 25.556 % |
c | 655249137 |    8289    20534 |  107996   80700  1935581    24.0 | 25.556 % |
c 
c *** TERMINATED ***
s UNKNOWN