c Parsing PB file...
c Converting 5572 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #
c   -- Clauses(.)/Splits(s): ..................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[   0]---> Adder-cost: 524   maxlim: 245   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    9174    23982 |    3058       0        0     nan |  0.000 % |
c |       100 |    9021    23457 |    3363      63      211     3.3 |  4.392 % |
c |       252 |    8854    22884 |    3700     181      787     4.3 |  7.027 % |
c |       477 |    8494    21648 |    4070     339     1627     4.8 | 14.304 % |
c |       814 |    8318    21034 |    4477     633     8711    13.8 | 17.943 % |
c |      1322 |    8229    20727 |    4924    1121    15548    13.9 | 19.825 % |
c |      2084 |    8193    20605 |    5417    1872    38700    20.7 | 20.452 % |
c |      3226 |    8193    20605 |    5959    3014    74041    24.6 | 20.452 % |
c |      4937 |    8184    20574 |    6555    4708   127310    27.0 | 20.578 % |
c |      7501 |    8175    20543 |    7210    3796   108100    28.5 | 20.703 % |
c |     11346 |    8157    20481 |    7931    3831    97085    25.3 | 20.954 % |
c |     17112 |    8149    20455 |    8724    5436   121926    22.4 | 21.079 % |
c |     25761 |    8138    20416 |    9597    5015    86402    17.2 | 21.330 % |
c |     38735 |    8138    20416 |   10557    8058   220853    27.4 | 21.330 % |
c |     58197 |    8138    20416 |   11612    5718   124925    21.8 | 21.330 % |
c |     87391 |    8138    20416 |   12774   11079   273359    24.7 | 21.330 % |
c |    131182 |    8111    20325 |   14051    9093   237267    26.1 | 21.832 % |
c |    196866 |    8111    20325 |   15456   10081   258501    25.6 | 21.832 % |
c |    295392 |    8111    20325 |   17002   14022   317183    22.6 | 21.832 % |
c |    443181 |    8103    20299 |   18702   14663   339552    23.2 | 21.957 % |
c |    664864 |    8103    20299 |   20572   17681   456599    25.8 | 21.957 % |
c |    997389 |    8103    20299 |   22629   15896   354343    22.3 | 21.958 % |
c |   1496183 |    8103    20299 |   24892   21167   601450    28.4 | 21.957 % |
c |   2244365 |    8088    20256 |   27382   24963   753069    30.2 | 22.459 % |
c |   3366642 |    8088    20256 |   30120   23823   685911    28.8 | 22.460 % |
c |   5050054 |    8059    20157 |   33132   16847   429196    25.5 | 23.338 % |
c |   7575171 |    8059    20157 |   36445   21546   495417    23.0 | 23.338 % |
c |  11362846 |    8053    20137 |   40090   15600   326528    20.9 | 23.464 % |
c |  17044358 |    8053    20137 |   44099   39799  1167621    29.3 | 23.463 % |
c |  25566627 |    8053    20137 |   48509   18627   464284    24.9 | 23.464 % |
c |  38350030 |    8053    20137 |   53360   38752  1268279    32.7 | 23.464 % |
c |  57525135 |    8053    20137 |   58696   47378  1265249    26.7 | 23.463 % |
c |  86287793 |    8053    20137 |   64565   47325  1365966    28.9 | 23.464 % |
c | 129431781 |    8046    20114 |   71022   49703  1384167    27.8 | 23.589 % |
c | 194147766 |    8046    20114 |   78124   47443  1181817    24.9 | 23.589 % |
c 
c *** TERMINATED ***
s UNKNOWN