c Parsing PB file...
c Converting 6440 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #
c   -- Clauses(.)/Splits(s): ......................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[   0]---> Adder-cost: 574   maxlim: 271   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   10379    26933 |    3459       0        0     nan |  0.000 % |
c |       101 |   10211    26359 |    3804      64      153     2.4 |  4.697 % |
c |       251 |   10043    25785 |    4185     186     1005     5.4 |  7.102 % |
c |       476 |    9799    24949 |    4603     369     2787     7.6 | 11.226 % |
c |       814 |    9373    23479 |    5064     613     4790     7.8 | 19.244 % |
c |      1321 |    9293    23201 |    5570    1090    15304    14.0 | 20.733 % |
c |      2080 |    9215    22933 |    6127    1806    35150    19.5 | 22.222 % |
c |      3222 |    9126    22628 |    6740    2917    60518    20.7 | 24.055 % |
c |      4932 |    9100    22538 |    7414    4585   115728    25.2 | 24.513 % |
c |      7494 |    9092    22512 |    8156    7146   169507    23.7 | 24.628 % |
c |     11340 |    9092    22512 |    8971    6672   145974    21.9 | 24.629 % |
c |     17106 |    9092    22512 |    9868    7726   168191    21.8 | 24.628 % |
c |     25757 |    9081    22473 |   10855    6183   145240    23.5 | 24.857 % |
c |     38732 |    9081    22473 |   11941    7906   204705    25.9 | 24.857 % |
c |     58194 |    9081    22473 |   13135    8839   217376    24.6 | 24.857 % |
c |     87386 |    9081    22473 |   14449   11001   274781    25.0 | 24.857 % |
c |    131175 |    9081    22473 |   15894   10193   298230    29.3 | 24.857 % |
c |    196861 |    9081    22473 |   17483   10778   265251    24.6 | 24.857 % |
c |    295387 |    9081    22473 |   19231   10984   258193    23.5 | 24.857 % |
c |    443176 |    9081    22473 |   21154   11609   290315    25.0 | 24.857 % |
c |    664861 |    9081    22473 |   23270   17774   564061    31.7 | 24.857 % |
c |    997386 |    9081    22473 |   25597   18934   558582    29.5 | 24.857 % |
c |   1496174 |    9081    22473 |   28157   24017   724004    30.1 | 24.857 % |
c |   2244356 |    9081    22473 |   30972   15414   382930    24.8 | 24.857 % |
c |   3366631 |    9081    22473 |   34070   24020   634557    26.4 | 24.857 % |
c |   5050042 |    9081    22473 |   37477   24953   681924    27.3 | 24.857 % |
c |   7575159 |    9081    22473 |   41224   31399   900094    28.7 | 24.857 % |
c |  11362835 |    9081    22473 |   45347   27239   725747    26.6 | 24.857 % |
c |  17044347 |    9081    22473 |   49882   37711  1101445    29.2 | 24.857 % |
c |  25566617 |    9081    22473 |   54870   21484   534144    24.9 | 24.857 % |
c |  38350020 |    9072    22442 |   60357   20843   539821    25.9 | 24.971 % |
c |  57525126 |    9072    22442 |   66393   21613   542407    25.1 | 24.971 % |
c |  86287786 |    9072    22442 |   73032   23324   731399    31.4 | 24.972 % |
c | 129431774 |    9072    22442 |   80335   25837   833112    32.2 | 24.971 % |
c | 194147756 |    9072    22442 |   88369   39174  1134004    28.9 | 24.971 % |
c | 291221729 |    9063    22411 |   97206   62683  1958042    31.2 | 25.201 % |
c | 436832689 |    9063    22411 |  106926   57556  1760953    30.6 | 25.201 % |
c 
c *** TERMINATED ***
s UNKNOWN