c Parsing PB file...
c Converting 13421 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #
c   -- Clauses(.)/Splits(s): ...........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[   0]---> Adder-cost: 800   maxlim: 385   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   18964    46617 |    6321       0        0     nan |  0.000 % |
c |       100 |   18769    45952 |    6953      69      205     3.0 |  3.957 % |
c |       251 |   18676    45633 |    7648     197      625     3.2 |  4.864 % |
c |       477 |   18374    44597 |    8413     369     1722     4.7 |  8.244 % |
c |       815 |   17550    41761 |    9254     557     2728     4.9 | 18.714 % |
c |      1321 |   17156    40405 |   10180     949     6652     7.0 | 23.908 % |
c |      2081 |   17001    39870 |   11198    1638    22207    13.6 | 26.051 % |
c |      3221 |   16968    39759 |   12317    2759    42825    15.5 | 26.463 % |
c |      4930 |   16934    39641 |   13549    4461    97948    22.0 | 26.958 % |
c |      7492 |   16915    39574 |   14904    7001   194802    27.8 | 27.288 % |
c |     11336 |   16886    39473 |   16395   10786   291669    27.0 | 27.618 % |
c |     17102 |   16857    39374 |   18034   16528   442015    26.7 | 28.030 % |
c |     25752 |   16857    39374 |   19838   15902   404136    25.4 | 28.030 % |
c |     38728 |   16857    39374 |   21821   18635   532456    28.6 | 28.030 % |
c |     58189 |   16845    39334 |   24003   15656   562323    35.9 | 28.195 % |
c |     87382 |   16845    39334 |   26404   20205   674596    33.4 | 28.195 % |
c |    131171 |   16833    39294 |   29044   23573   970361    41.2 | 28.360 % |
c |    196856 |   16833    39294 |   31949   15201   474739    31.2 | 28.360 % |
c |    295387 |   16833    39294 |   35144   32304   956072    29.6 | 28.360 % |
c |    443177 |   16833    39294 |   38658   35636  1386671    38.9 | 28.360 % |
c |    664860 |   16813    39224 |   42524   29616   909500    30.7 | 28.607 % |
c |    997386 |   16813    39224 |   46776   31190   901450    28.9 | 28.607 % |
c |   1496176 |   16813    39224 |   51454   45710  1720169    37.6 | 28.607 % |
c |   2244360 |   16813    39224 |   56600   20139   525491    26.1 | 28.607 % |
c |   3366636 |   16813    39224 |   62260   35983  1357023    37.7 | 28.607 % |
c |   5050049 |   16802    39185 |   68486   34131  1215874    35.6 | 28.772 % |
c |   7575165 |   16802    39185 |   75334   49129  1638345    33.3 | 28.772 % |
c |  11362840 |   16802    39185 |   82868   35377  1163597    32.9 | 28.772 % |
c |  17044352 |   16802    39185 |   91155   80817  2768486    34.3 | 28.772 % |
c |  25566621 |   16802    39185 |  100270   74440  2605875    35.0 | 28.772 % |
c |  38350024 |   16802    39185 |  110297   63103  2606270    41.3 | 28.772 % |
c |  57525129 |   16802    39185 |  121327   78469  2562868    32.7 | 28.772 % |
c |  86287788 |   16802    39185 |  133460  101024  3244087    32.1 | 28.772 % |
c | 129431776 |   16802    39185 |  146806   57404  2052704    35.8 | 28.772 % |
c 
c *** TERMINATED ***
s UNKNOWN