c Parsing PB file...
c Converting 6984 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #
c   -- Clauses(.)/Splits(s): ......................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[   0]---> Adder-cost: 472   maxlim: 227   bits: 8/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   10235    25559 |    3411       0        0     nan |  0.000 % |
c |       100 |   10145    25253 |    3752      83      371     4.5 |  3.755 % |
c |       250 |    9983    24697 |    4127     203      932     4.6 |  6.398 % |
c |       475 |    9512    23080 |    4540     354     2777     7.8 | 16.968 % |
c |       812 |    9426    22784 |    4994     678     9382    13.8 | 18.359 % |
c |      1319 |    9270    22242 |    5493    1140    19841    17.4 | 22.114 % |
c |      2079 |    9235    22123 |    6042    1892    33422    17.7 | 22.949 % |
c |      3218 |    9226    22092 |    6647    3019    57995    19.2 | 23.088 % |
c |      4927 |    9177    21925 |    7311    4664    94782    20.3 | 24.062 % |
c |      7490 |    9177    21925 |    8042    7227   162076    22.4 | 24.061 % |
c |     11335 |    9168    21894 |    8847    6824   140413    20.6 | 24.200 % |
c |     17101 |    9168    21894 |    9731    7982   246781    30.9 | 24.200 % |
c |     25750 |    9135    21781 |   10705    6525   141456    21.7 | 24.757 % |
c |     38724 |    9135    21781 |   11775    8446   179292    21.2 | 24.757 % |
c |     58189 |    9135    21781 |   12953    9825   234217    23.8 | 24.757 % |
c |     87381 |    9126    21750 |   14248   12348   293282    23.8 | 24.896 % |
c |    131170 |    9126    21750 |   15673   12452   289707    23.3 | 24.896 % |
c |    196854 |    9126    21750 |   17240   14234   354779    24.9 | 24.896 % |
c |    295382 |    9126    21750 |   18964   15937   391251    24.5 | 24.896 % |
c |    443171 |    9120    21730 |   20861   18820   458905    24.4 | 25.035 % |
c |    664854 |    9102    21670 |   22947   17571   396082    22.5 | 25.452 % |
c |    997379 |    9102    21670 |   25242   11961   237382    19.8 | 25.454 % |
c |   1496170 |    9102    21670 |   27766   24189   575635    23.8 | 25.452 % |
c |   2244353 |    9102    21670 |   30543   27000   630212    23.3 | 25.452 % |
c |   3366630 |    9102    21670 |   33597   21368   458436    21.5 | 25.452 % |
c |   5050045 |    9091    21633 |   36957   21866   429139    19.6 | 25.869 % |
c |   7575162 |    9091    21633 |   40652   23324   521756    22.4 | 25.872 % |
c |  11362839 |    9091    21633 |   44718   40067   843214    21.0 | 25.870 % |
c |  17044351 |    9091    21633 |   49190   29237   672172    23.0 | 25.869 % |
c |  25566620 |    9091    21633 |   54109   38174   840492    22.0 | 25.870 % |
c |  38350024 |    8987    21265 |   59519   35855   877463    24.5 | 28.234 % |
c ==============================================================================
c UNSATISFIABLE
s UNSATISFIABLE
c _______________________________________________________________________________
c 
c restarts              : 31
c conflicts             : 39298920       (9699 /sec)
c decisions             : 49401499       (12192 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 4051.8 s
c _______________________________________________________________________________