Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
  1. LAUNCHER DATA
    These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. WATCHER DATA
    This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
    Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
    When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
  4. VERIFIER DATA
    The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.

General information on the benchmark

Namenormalized-opb/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-p0201.opb
MD5SUM8c361d02d5162bb0b133ab6ed38f9294
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 1523
Optimality of the best value was proved NO
Number of terms in the objective function 201
Biggest coefficient in the objective function 1920
Number of bits for the biggest coefficient in the objective function 11
Sum of the numbers in the objective function 19980
Number of bits of the sum of numbers in the objective function 15
Biggest number in a constraint 1920
Number of bits of the biggest number in a constraint 11
Biggest sum of numbers in a constraint 19980
Number of bits of the biggest sum of numbers15
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1.02184
Number of variables201
Total number of constraints334
Number of constraints which are clauses20
Number of constraints which are cardinality constraints (but not clauses)227
Number of constraints which are nor clauses,nor cardinality constraints87
Minimum length of a constraint1
Maximum length of a constraint67

Trace number 21123

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc4 THE 2005-04-21 22:53:09 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13715 boxname=wulflinc4 idbench=1055 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  8c361d02d5162bb0b133ab6ed38f9294  /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-p0201.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-p0201.opb /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-p0201.opb
IDLAUNCH: 13715
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        590144 kB
Buffers:         31944 kB
Cached:         391468 kB
SwapCached:        364 kB
Active:         103456 kB
Inactive:       322472 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        589892 kB
SwapTotal:     2097136 kB
SwapFree:      2096356 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6404 kB
Slab:            13000 kB
Committed_AS:    71788 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 23:13:11 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 13715 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 133 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################
c   -- Clauses(.)/Splits(s): sssss
c ---[ 137]---> BDD-cost:    3
c ---[ 136]---> BDD-cost:    3
c ---[ 135]---> BDD-cost:    3
c ---[ 133]---> BDD-cost:   15
c ---[ 131]---> BDD-cost:   15
c ---[ 129]---> BDD-cost:   15
c ---[ 127]---> BDD-cost:   15
c ---[ 125]---> BDD-cost:   15
c ---[ 123]---> BDD-cost:   15
c ---[ 121]---> BDD-cost:   15
c ---[ 119]---> BDD-cost:   15
c ---[ 117]---> BDD-cost:   15
c ---[ 115]---> BDD-cost:   15
c ---[ 113]---> BDD-cost:   15
c ---[ 111]---> BDD-cost:   15
c ---[ 109]---> BDD-cost:   15
c ---[ 107]---> BDD-cost:   15
c ---[ 105]---> BDD-cost:   15
c ---[ 103]---> BDD-cost:   15
c ---[ 101]---> BDD-cost:   15
c ---[  99]---> BDD-cost:   15
c ---[  97]---> BDD-cost:   15
c ---[  95]---> BDD-cost:   15
c ---[  89]---> BDD-cost:   39
c ---[  88]---> BDD-cost:   42
c ---[  87]---> BDD-cost:   42
c ---[  86]---> BDD-cost:   54
c ---[  85]---> BDD-cost:   73
c ---[  84]---> BDD-cost:   73
c ---[  83]---> BDD-cost:   98
c ---[  82]---> BDD-cost:   85
c ---[  81]---> BDD-cost:   85
c ---[  80]---> BDD-cost:  160
c ---[  79]---> BDD-cost:  107
c ---[  78]---> BDD-cost:  107
c ---[  77]---> BDD-cost:  201
c ---[  76]---> BDD-cost:  128
c ---[  75]---> BDD-cost:  128
c ---[  74]---> BDD-cost:  241
c ---[  73]---> BDD-cost:  150
c ---[  72]---> BDD-cost:  150
c ---[  71]---> BDD-cost:  281
c ---[  70]---> BDD-cost:  172
c ---[  69]---> BDD-cost:  172
c ---[  68]---> BDD-cost:  321
c ---[  67]---> BDD-cost:  194
c ---[  66]---> BDD-cost:  194
c ---[  65]---> BDD-cost:  361
c ---[  64]---> BDD-cost:    3
c ---[  63]---> BDD-cost:    3
c ---[  62]---> BDD-cost:    3
c ---[  61]---> BDD-cost:    3
c ---[  60]---> BDD-cost:    3
c ---[  59]---> BDD-cost:    3
c ---[  58]---> BDD-cost:    9
c ---[  57]---> BDD-cost:   11
c ---[  56]---> BDD-cost:   11
c ---[  55]---> BDD-cost:    9
c ---[  54]---> BDD-cost:   11
c ---[  53]---> BDD-cost:   11
c ---[  52]---> BDD-cost:    9
c ---[  51]---> BDD-cost:   11
c ---[  50]---> BDD-cost:   11
c ---[  49]---> BDD-cost:    9
c ---[  48]---> BDD-cost:   11
c ---[  47]---> BDD-cost:   11
c ---[  46]---> BDD-cost:    9
c ---[  45]---> BDD-cost:   11
c ---[  44]---> BDD-cost:   11
c ---[  43]---> BDD-cost:    9
c ---[  42]---> BDD-cost:   11
c ---[  41]---> BDD-cost:   11
c ---[  40]---> BDD-cost:    9
c ---[  39]---> BDD-cost:   11
c ---[  38]---> BDD-cost:   11
c ---[  37]---> BDD-cost:    9
c ---[  36]---> BDD-cost:   11
c ---[  35]---> BDD-cost:   11
c ---[  34]---> BDD-cost:    9
c ---[  33]---> BDD-cost:   11
c ---[  32]---> BDD-cost:   11
c ---[  31]---> BDD-cost:    9
c ---[  30]---> BDD-cost:   11
c ---[  29]---> BDD-cost:   11
c ---[  28]---> BDD-cost:    9
c ---[  27]---> BDD-cost:   11
c ---[  26]---> BDD-cost:   11
c ---[  25]---> BDD-cost:    9
c ---[  24]---> BDD-cost:   11
c ---[  23]---> BDD-cost:   11
c ---[  22]---> BDD-cost:    9
c ---[  21]---> BDD-cost:   11
c ---[  20]---> BDD-cost:   11
c ---[  19]---> BDD-cost:    9
c ---[  18]---> BDD-cost:   11
c ---[  17]---> BDD-cost:   11
c ---[  16]---> BDD-cost:    9
c ---[  15]---> BDD-cost:   11
c ---[  14]---> BDD-cost:   11
c ---[  13]---> BDD-cost:    9
c ---[  12]---> BDD-cost:   11
c ---[  11]---> BDD-cost:   11
c ---[  10]---> BDD-cost:    9
c ---[   9]---> BDD-cost:   11
c ---[   8]---> BDD-cost:   11
c ---[   7]---> BDD-cost:    9
c ---[   6]---> BDD-cost:   11
c ---[   5]---> BDD-cost:   11
c ---[   4]---> BDD-cost:    1
c ---[   3]---> BDD-cost:    1
c ---[   2]---> BDD-cost:    1
c ---[   1]---> BDD-cost:    1
c ---[   0]---> BDD-cost:    1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   23540    68455 |    7846       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 2734
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:21097     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         7 |   78351   196805 |   26117       3       60    20.0 |  0.000 % |
c ==============================================================================
c Found solution: 2329
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       106 |   77002   193861 |   25667      84     1079    12.8 |  0.000 % |
c ==============================================================================
c Found solution: 2304
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       118 |   77013   193888 |   25671      96     1193    12.4 |  0.000 % |
c |       218 |   76399   192474 |   28238     185     3409    18.4 |  4.161 % |
c |       368 |   75394   190171 |   31061     323     4790    14.8 |  5.253 % |
c |       594 |   71969   182251 |   34168     514     8965    17.4 |  9.788 % |
c ==============================================================================
c Found solution: 2283
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       822 |   71047   180141 |   23682     720    13788    19.1 |  9.788 % |
c |       922 |   70655   179234 |   26050     817    14502    17.8 | 11.766 % |
c |      1072 |   70585   179073 |   28655     965    17039    17.7 | 11.866 % |
c |      1300 |   70578   179052 |   31520    1190    21713    18.2 | 11.871 % |
c ==============================================================================
c Found solution: 2225
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1454 |   70707   179370 |   23569    1344    24163    18.0 | 11.871 % |
c ==============================================================================
c Found solution: 2191
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1457 |   70723   179410 |   23574    1347    24215    18.0 | 11.871 % |
c |      1557 |   70723   179410 |   25931    1447    26069    18.0 | 11.918 % |
c |      1707 |   70609   179152 |   28524    1574    27094    17.2 | 12.052 % |
c |      1932 |   70609   179152 |   31376    1799    30446    16.9 | 12.053 % |
c |      2270 |   70196   178201 |   34514    2121    32259    15.2 | 12.597 % |
c ==============================================================================
c Found solution: 2179
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2277 |   70204   178221 |   23401    2128    32301    15.2 | 12.597 % |
c |      2377 |   69756   177173 |   25741    2223    34819    15.7 | 13.223 % |
c |      2527 |   68491   174206 |   28315    2347    38087    16.2 | 14.893 % |
c ==============================================================================
c Found solution: 2173
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2595 |   67333   171523 |   22444    2401    38686    16.1 | 14.893 % |
c |      2697 |   66571   169748 |   24688    2488    39496    15.9 | 17.501 % |
c ==============================================================================
c Found solution: 2028
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2811 |   66573   169763 |   22191    2601    41964    16.1 | 17.501 % |
c |      2912 |   66338   169218 |   24410    2687    43291    16.1 | 18.031 % |
c ==============================================================================
c Found solution: 1924
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2988 |   65410   167073 |   21803    2746    43707    15.9 | 18.031 % |
c |      3089 |   63386   162376 |   23983    2799    47959    17.1 | 21.953 % |
c |      3239 |   63386   162376 |   26381    2949    62040    21.0 | 21.953 % |
c |      3464 |   63386   162376 |   29019    3174    74050    23.3 | 21.953 % |
c |      3803 |   61775   158616 |   31921    3446    76816    22.3 | 24.199 % |
c |      4309 |   61422   157788 |   35113    3935   116814    29.7 | 24.657 % |
c ==============================================================================
c Found solution: 1921
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4647 |   61453   157868 |   20484    4273   137525    32.2 | 24.657 % |
c |      4750 |   61453   157868 |   22532    4376   140697    32.2 | 24.650 % |
c |      4901 |   61453   157868 |   24785    4527   145200    32.1 | 24.650 % |
c |      5127 |   61453   157868 |   27264    4753   151738    31.9 | 24.650 % |
c |      5465 |   61349   157629 |   29990    5053   154257    30.5 | 24.780 % |
c |      5971 |   61349   157629 |   32989    5559   167280    30.1 | 24.780 % |
c ==============================================================================
c Found solution: 1907
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6178 |   61445   157865 |   20481    5766   175207    30.4 | 24.780 % |
c |      6278 |   61232   157240 |   22529    5852   177409    30.3 | 24.977 % |
c ==============================================================================
c Found solution: 1891
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6404 |   61201   157162 |   20400    5976   181572    30.4 | 24.977 % |
c |      6506 |   61194   157141 |   22440    6076   186499    30.7 | 25.023 % |
c |      6656 |   61174   157085 |   24684    6223   189898    30.5 | 25.040 % |
c |      6881 |   60935   156508 |   27152    6427   193656    30.1 | 25.385 % |
c |      7220 |   60725   156017 |   29867    6650   200513    30.2 | 25.635 % |
c ==============================================================================
c Found solution: 1889
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7349 |   60733   156037 |   20244    6779   203446    30.0 | 25.635 % |
c |      7450 |   60733   156037 |   22268    6880   205758    29.9 | 25.635 % |
c |      7601 |   60728   156022 |   24495    7030   208603    29.7 | 25.640 % |
c |      7827 |   60728   156022 |   26944    7256   213972    29.5 | 25.640 % |
c |      8165 |   60551   155604 |   29639    7565   221473    29.3 | 25.877 % |
c |      8671 |   60156   154619 |   32603    8053   252963    31.4 | 26.338 % |
c |      9430 |   60004   154263 |   35863    8790   286402    32.6 | 26.540 % |
c |     10571 |   59190   152376 |   39449    9881   315307    31.9 | 27.643 % |
c |     12280 |   59107   152160 |   43394   11583   357293    30.8 | 27.729 % |
c ==============================================================================
c Found solution: 1882
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12915 |   58997   151868 |   19665   12200   370350    30.4 | 27.729 % |
c |     13015 |   58997   151868 |   21631   12300   372395    30.3 | 27.856 % |
c |     13167 |   58958   151778 |   23794   12440   374194    30.1 | 27.912 % |
c |     13392 |   58831   151484 |   26174   12656   375759    29.7 | 28.076 % |
c ==============================================================================
c Found solution: 1879
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13486 |   58087   149754 |   19362   12598   375795    29.8 | 28.076 % |
c |     13588 |   58087   149754 |   21298   12700   377802    29.7 | 29.115 % |
c |     13741 |   58087   149754 |   23428   12853   387259    30.1 | 29.115 % |
c |     13966 |   58087   149754 |   25770   13078   393630    30.1 | 29.115 % |
c |     14306 |   58087   149754 |   28347   13418   400516    29.8 | 29.115 % |
c |     14812 |   58087   149754 |   31182   13924   439892    31.6 | 29.115 % |
c |     15571 |   57870   149241 |   34300   14673   454378    31.0 | 29.399 % |
c |     16710 |   57870   149241 |   37731   15812   474459    30.0 | 29.399 % |
c |     18418 |   57134   147529 |   41504   17423   574127    33.0 | 30.441 % |
c |     20981 |   57134   147529 |   45654   19986   723332    36.2 | 30.441 % |
c ==============================================================================
c Found solution: 1857
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21095 |   57151   147572 |   19050   20100   728049    36.2 | 30.441 % |
c |     21195 |   57130   147525 |   20955   20195   730320    36.2 | 30.465 % |
c |     21346 |   57130   147525 |   23050   20346   734030    36.1 | 30.465 % |
c ==============================================================================
c Found solution: 1851
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21570 |   57125   147513 |   19041   20563   743827    36.2 | 30.465 % |
c ==============================================================================
c Found solution: 1847
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21634 |   57128   147520 |   19042   20627   745630    36.1 | 30.465 % |
c |     21737 |   57128   147520 |   20946   20730   751945    36.3 | 30.471 % |
c |     21888 |   57045   147328 |   23040   20877   755676    36.2 | 30.574 % |
c |     22114 |   57045   147328 |   25344   21103   766990    36.3 | 30.574 % |
c |     22453 |   57020   147272 |   27879   21438   786878    36.7 | 30.604 % |
c |     22959 |   57020   147272 |   30667   21944   826660    37.7 | 30.604 % |
c ==============================================================================
c Found solution: 1845
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23563 |   56971   147158 |   18990   22547   891231    39.5 | 30.604 % |
c |     23666 |   56971   147158 |   20889   22650   893152    39.4 | 30.675 % |
c |     23817 |   56971   147158 |   22977   22801   895145    39.3 | 30.675 % |
c |     24042 |   56971   147158 |   25275   23026   906809    39.4 | 30.675 % |
c |     24379 |   56971   147158 |   27803   23363   937813    40.1 | 30.675 % |
c |     24887 |   56669   146466 |   30583   23864   973509    40.8 | 31.071 % |
c ==============================================================================
c Found solution: 1827
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25018 |   56676   146483 |   18892   23995   978086    40.8 | 31.071 % |
c |     25118 |   56676   146483 |   20781   24095   981131    40.7 | 31.071 % |
c |     25269 |   56676   146483 |   22859   24246   989880    40.8 | 31.071 % |
c |     25495 |   56676   146483 |   25145   24472  1001050    40.9 | 31.071 % |
c |     25832 |   56313   145647 |   27659   24774  1023643    41.3 | 31.575 % |
c ==============================================================================
c Found solution: 1819
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25914 |   56316   145654 |   18772   24856  1031106    41.5 | 31.575 % |
c |     26016 |   56316   145654 |   20649   24958  1032870    41.4 | 31.576 % |
c |     26169 |   56316   145654 |   22714   25111  1046447    41.7 | 31.576 % |
c |     26394 |   56316   145654 |   24985   25336  1064844    42.0 | 31.576 % |
c |     26731 |   56292   145598 |   27484   25672  1075820    41.9 | 31.602 % |
c |     27238 |   56233   145459 |   30232   26178  1098939    42.0 | 31.680 % |
c |     27999 |   56159   145237 |   33255   26934  1182332    43.9 | 31.736 % |
c |     29141 |   56159   145237 |   36581   28076  1252716    44.6 | 31.736 % |
c |     30849 |   56150   145214 |   40239   29782  1351975    45.4 | 31.744 % |
c ==============================================================================
c Found solution: 1789
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33214 |   56187   145307 |   18729   32147  1526468    47.5 | 31.744 % |
c |     33314 |   56187   145307 |   20601   16174   791453    48.9 | 31.735 % |
c |     33465 |   56187   145307 |   22662   16325   795339    48.7 | 31.735 % |
c |     33690 |   56187   145307 |   24928   16550   811934    49.1 | 31.735 % |
c |     34027 |   56187   145307 |   27421   16887   823519    48.8 | 31.735 % |
c ==============================================================================
c Found solution: 1779
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34130 |   56203   145347 |   18734   16990   827111    48.7 | 31.735 % |
c |     34232 |   56203   145347 |   20607   17092   838120    49.0 | 31.733 % |
c |     34383 |   56203   145347 |   22668   17243   842134    48.8 | 31.733 % |
c ==============================================================================
c Found solution: 1778
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34597 |   56213   145371 |   18737   17457   872147    50.0 | 31.733 % |
c |     34697 |   56205   145353 |   20610   17555   873761    49.8 | 31.740 % |
c |     34847 |   56163   145256 |   22671   17697   875346    49.5 | 31.796 % |
c |     35074 |   55614   143980 |   24938   17713   880296    49.7 | 32.527 % |
c |     35411 |   55614   143980 |   27432   18050   891405    49.4 | 32.527 % |
c |     35920 |   55614   143980 |   30176   18559   929733    50.1 | 32.527 % |
c |     36681 |   55614   143980 |   33193   19320   983705    50.9 | 32.527 % |
c |     37820 |   55614   143980 |   36513   20459  1065761    52.1 | 32.527 % |
c ==============================================================================
c Found solution: 1771
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     39153 |   55618   143990 |   18539   21792  1168350    53.6 | 32.527 % |
c |     39254 |   55618   143990 |   20392   21893  1171941    53.5 | 32.528 % |
c |     39409 |   55618   143990 |   22432   22048  1182758    53.6 | 32.528 % |
c |     39634 |   55618   143990 |   24675   22273  1190256    53.4 | 32.528 % |
c |     39971 |   55618   143990 |   27142   22610  1198970    53.0 | 32.528 % |
c |     40478 |   55618   143990 |   29857   23117  1241336    53.7 | 32.528 % |
c |     41238 |   55443   143587 |   32842   23871  1300327    54.5 | 32.760 % |
c |     42377 |   55436   143566 |   36127   25007  1332385    53.3 | 32.765 % |
c |     44085 |   55436   143566 |   39739   26715  1385367    51.9 | 32.765 % |
c |     46647 |   55427   143543 |   43713   29276  1512944    51.7 | 32.773 % |
c ==============================================================================
c Found solution: 1761
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     48332 |   55435   143563 |   18478   30961  1620159    52.3 | 32.773 % |
c |     48432 |   55435   143563 |   20325   15581   569217    36.5 | 32.773 % |
c |     48583 |   55435   143563 |   22358   15732   576354    36.6 | 32.773 % |
c |     48809 |   55435   143563 |   24594   15958   586916    36.8 | 32.773 % |
c ==============================================================================
c Found solution: 1751
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     49011 |   55440   143576 |   18480   16160   598362    37.0 | 32.773 % |
c |     49113 |   55440   143576 |   20328   16262   600587    36.9 | 32.775 % |
c |     49263 |   55440   143576 |   22360   16412   615724    37.5 | 32.775 % |
c |     49489 |   55433   143555 |   24596   16636   623173    37.5 | 32.779 % |
c |     49828 |   55433   143555 |   27056   16975   630918    37.2 | 32.779 % |
c |     50335 |   55433   143555 |   29762   17482   641582    36.7 | 32.779 % |
c |     51094 |   55424   143532 |   32738   18238   662543    36.3 | 32.788 % |
c |     52233 |   55290   143205 |   36012   19369   727221    37.5 | 32.951 % |
c |     53942 |   55283   143184 |   39613   21074   777289    36.9 | 32.955 % |
c ==============================================================================
c Found solution: 1730
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     55465 |   55305   143238 |   18435   22597   906318    40.1 | 32.955 % |
c |     55565 |   55073   142698 |   20278   22684   907310    40.0 | 33.250 % |
c |     55716 |   54831   142145 |   22306   22812   916789    40.2 | 33.556 % |
c |     55941 |   54831   142145 |   24536   23037   931838    40.4 | 33.555 % |
c |     56279 |   54686   141799 |   26990   23355   940703    40.3 | 33.749 % |
c |     56786 |   54679   141778 |   29689   23860   965722    40.5 | 33.753 % |
c |     57547 |   54679   141778 |   32658   24621   993342    40.3 | 33.753 % |
c |     58686 |   54584   141534 |   35924   25756  1053248    40.9 | 33.869 % |
c |     60394 |   54584   141534 |   39517   27464  1209356    44.0 | 33.869 % |
c |     62956 |   54579   141519 |   43468   30024  1362239    45.4 | 33.873 % |
c ==============================================================================
c Found solution: 1709
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     63218 |   54585   141533 |   18195   30286  1374583    45.4 | 33.873 % |
c |     63318 |   54585   141533 |   20014   15243   636385    41.7 | 33.873 % |
c |     63468 |   54585   141533 |   22015   15393   643684    41.8 | 33.873 % |
c |     63693 |   54585   141533 |   24217   15618   663543    42.5 | 33.873 % |
c |     64033 |   54585   141533 |   26639   15958   689700    43.2 | 33.873 % |
c |     64540 |   54569   141485 |   29303   16462   710848    43.2 | 33.886 % |
c |     65299 |   54556   141448 |   32233   17219   746818    43.4 | 33.899 % |
c |     66438 |   54556   141448 |   35456   18358   860808    46.9 | 33.899 % |
c |     68149 |   54556   141448 |   39002   20069   969043    48.3 | 33.899 % |
c ==============================================================================
c Found solution: 1708
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     69591 |   54563   141465 |   18187   21511  1057309    49.2 | 33.899 % |
c |     69692 |   54483   141280 |   20005   21601  1058935    49.0 | 34.011 % |
c |     69842 |   54483   141280 |   22006   21751  1067573    49.1 | 34.010 % |
c |     70069 |   54483   141280 |   24206   21978  1078942    49.1 | 34.010 % |
c |     70407 |   54483   141280 |   26627   22316  1102923    49.4 | 34.010 % |
c |     70914 |   54474   141257 |   29290   22820  1129045    49.5 | 34.019 % |
c |     71677 |   54192   140581 |   32219   23569  1181684    50.1 | 34.380 % |
c |     72817 |   54170   140523 |   35441   24706  1248961    50.6 | 34.401 % |
c ==============================================================================
c Found solution: 1704
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     73953 |   54176   140537 |   18058   25842  1331297    51.5 | 34.401 % |
c |     74054 |   54176   140537 |   19863   25943  1334005    51.4 | 34.401 % |
c |     74205 |   54168   140515 |   21850   26093  1343025    51.5 | 34.410 % |
c |     74431 |   54168   140515 |   24035   26319  1348240    51.2 | 34.410 % |
c |     74769 |   54168   140515 |   26438   26657  1359724    51.0 | 34.410 % |
c |     75275 |   53782   139616 |   29082   27138  1367750    50.4 | 34.929 % |
c |     76034 |   53666   139350 |   31990   27883  1422181    51.0 | 35.080 % |
c |     77175 |   53666   139350 |   35189   29024  1499346    51.7 | 35.080 % |
c |     78883 |   53661   139335 |   38708   30729  1570989    51.1 | 35.084 % |
c ==============================================================================
c Found solution: 1701
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     79115 |   53667   139349 |   17889   30961  1595829    51.5 | 35.084 % |
c |     79216 |   53667   139349 |   19677   15582   557033    35.7 | 35.084 % |
c |     79372 |   53667   139349 |   21645   15738   564117    35.8 | 35.084 % |
c |     79597 |   53667   139349 |   23810   15963   575906    36.1 | 35.084 % |
c |     79934 |   53667   139349 |   26191   16300   596618    36.6 | 35.084 % |
c |     80440 |   53667   139349 |   28810   16806   637980    38.0 | 35.084 % |
c ==============================================================================
c Found solution: 1681
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     80786 |   53694   139418 |   17898   17152   669439    39.0 | 35.084 % |
c |     80886 |   53694   139418 |   19687   17252   674169    39.1 | 35.074 % |
c |     81036 |   53694   139418 |   21656   17402   682240    39.2 | 35.074 % |
c |     81261 |   53694   139418 |   23822   17627   692778    39.3 | 35.074 % |
c |     81598 |   53694   139418 |   26204   17964   707014    39.4 | 35.074 % |
c |     82105 |   53694   139418 |   28824   18471   734735    39.8 | 35.074 % |
c |     82864 |   53694   139418 |   31707   19230   761208    39.6 | 35.074 % |
c |     84004 |   53694   139418 |   34878   20370   807262    39.6 | 35.074 % |
c |     85713 |   53636   139247 |   38365   22064   869533    39.4 | 35.122 % |
c |     88275 |   53636   139247 |   42202   24626  1028052    41.7 | 35.122 % |
c |     92123 |   53636   139247 |   46422   28474  1285993    45.2 | 35.122 % |
c |     97889 |   53636   139247 |   51065   34240  1645858    48.1 | 35.122 % |
c ==============================================================================
c Found solution: 1679
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    101348 |   53649   139280 |   17883   37699  1869282    49.6 | 35.122 % |
c |    101449 |   53649   139280 |   19671   17648   788473    44.7 | 35.120 % |
c |    101599 |   53649   139280 |   21638   17798   798338    44.9 | 35.120 % |
c |    101824 |   53464   138850 |   23802   18006   806059    44.8 | 35.373 % |
c |    102161 |   53464   138850 |   26182   18343   820610    44.7 | 35.373 % |
c |    102669 |   53464   138850 |   28800   18851   828169    43.9 | 35.373 % |
c |    103428 |   53433   138779 |   31680   19608   854709    43.6 | 35.416 % |
c |    104567 |   53433   138779 |   34848   20747   909381    43.8 | 35.416 % |
c |    106275 |   53433   138779 |   38333   22455   981995    43.7 | 35.416 % |
c |    108839 |   53409   138709 |   42167   25013  1091899    43.7 | 35.438 % |
c ==============================================================================
c Found solution: 1675
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    111459 |   53417   138729 |   17805   27633  1215412    44.0 | 35.438 % |
c |    111560 |   53417   138729 |   19585   13918   416627    29.9 | 35.437 % |
c |    111710 |   53417   138729 |   21544   14068   423829    30.1 | 35.437 % |
c |    111936 |   53417   138729 |   23698   14294   431416    30.2 | 35.437 % |
c |    112275 |   53417   138729 |   26068   14633   450898    30.8 | 35.437 % |
c |    112781 |   53417   138729 |   28675   15139   481538    31.8 | 35.437 % |
c |    113541 |   53417   138729 |   31542   15899   529961    33.3 | 35.437 % |
c |    114680 |   53417   138729 |   34696   17038   592837    34.8 | 35.437 % |
c |    116388 |   53291   138436 |   38166   18722   655572    35.0 | 35.617 % |
c |    118952 |   53142   138090 |   41983   21251   834890    39.3 | 35.819 % |
c |    122797 |   53142   138090 |   46181   25096  1015052    40.4 | 35.819 % |
c |    128563 |   53142   138090 |   50799   30862  1260163    40.8 | 35.819 % |
c |    137214 |   53132   138063 |   55879   39507  1747123    44.2 | 35.828 % |
c ==============================================================================
c Found solution: 1674
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    144513 |   53076   137933 |   17692   46804  2162886    46.2 | 35.828 % |
c |    144614 |   53076   137933 |   19461   19538   755239    38.7 | 35.913 % |
c |    144765 |   53076   137933 |   21407   19689   759014    38.6 | 35.913 % |
c |    144990 |   53076   137933 |   23548   19914   771862    38.8 | 35.913 % |
c |    145329 |   53076   137933 |   25902   20253   790174    39.0 | 35.913 % |
c |    145837 |   53076   137933 |   28493   20761   816689    39.3 | 35.913 % |
c |    146597 |   53076   137933 |   31342   21521   854194    39.7 | 35.913 % |
c |    147736 |   53076   137933 |   34476   22660   909307    40.1 | 35.913 % |
c |    149444 |   53076   137933 |   37924   24368   977408    40.1 | 35.913 % |
c ==============================================================================
c Found solution: 1673
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    150144 |   53079   137938 |   17693   25067  1018697    40.6 | 35.913 % |
c |    150244 |   53079   137938 |   19462   25167  1023272    40.7 | 35.917 % |
c |    150394 |   53079   137938 |   21408   25317  1027428    40.6 | 35.917 % |
c |    150619 |   52948   137633 |   23549   25530  1035370    40.6 | 36.102 % |
c |    150956 |   52811   137306 |   25904   25842  1047899    40.6 | 36.269 % |
c |    151464 |   52811   137306 |   28494   26350  1070170    40.6 | 36.269 % |
c |    152224 |   52811   137306 |   31344   27110  1094861    40.4 | 36.269 % |
c |    153363 |   52811   137306 |   34478   28249  1140635    40.4 | 36.269 % |
c |    155071 |   52811   137306 |   37926   29957  1211321    40.4 | 36.269 % |
c |    157633 |   52742   137146 |   41719   32516  1353392    41.6 | 36.368 % |
c |    161477 |   52691   137025 |   45891   36347  1573604    43.3 | 36.432 % |
c ==============================================================================
c Found solution: 1671
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    165192 |   52695   137035 |   17565   40062  1768654    44.1 | 36.432 % |
c |    165292 |   52695   137035 |   19321   19125   689106    36.0 | 36.433 % |
c |    165442 |   52695   137035 |   21253   19275   695771    36.1 | 36.433 % |
c |    165670 |   52695   137035 |   23379   19503   711946    36.5 | 36.433 % |
c |    166008 |   52695   137035 |   25716   19841   725279    36.6 | 36.433 % |
c |    166514 |   52695   137035 |   28288   20347   746787    36.7 | 36.433 % |
c ==============================================================================
c Found solution: 1668
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    166994 |   52699   137045 |   17566   20827   770393    37.0 | 36.433 % |
c |    167095 |   52699   137045 |   19322   20928   777479    37.2 | 36.434 % |
c |    167247 |   52699   137045 |   21254   21080   791718    37.6 | 36.434 % |
c |    167474 |   52699   137045 |   23380   21307   799949    37.5 | 36.434 % |
c |    167811 |   52699   137045 |   25718   21644   815385    37.7 | 36.434 % |
c |    168317 |   52699   137045 |   28290   22150   847982    38.3 | 36.434 % |
c |    169078 |   52699   137045 |   31119   22911   877800    38.3 | 36.434 % |
c |    170218 |   52699   137045 |   34231   24051   927360    38.6 | 36.434 % |
c |    171926 |   52699   137045 |   37654   25759  1026430    39.8 | 36.434 % |
c |    174491 |   52699   137045 |   41419   28324  1168146    41.2 | 36.434 % |
c ==============================================================================
c Found solution: 1659
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    175110 |   52703   137055 |   17567   28943  1215179    42.0 | 36.434 % |
c |    175212 |   52652   136935 |   19323   14572   480982    33.0 | 36.517 % |
c |    175362 |   52652   136935 |   21256   14722   490944    33.3 | 36.517 % |
c |    175588 |   52649   136929 |   23381   14946   505311    33.8 | 36.521 % |
c |    175928 |   52649   136929 |   25719   15286   524060    34.3 | 36.521 % |
c |    176435 |   52649   136929 |   28291   15793   549075    34.8 | 36.521 % |
c |    177194 |   52649   136929 |   31121   16552   587540    35.5 | 36.521 % |
c |    178334 |   52649   136929 |   34233   17692   646778    36.6 | 36.521 % |
c ==============================================================================
c Found solution: 1651
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    179859 |   52653   136939 |   17551   19217   741511    38.6 | 36.521 % |
c |    179959 |   52653   136939 |   19306   19317   746063    38.6 | 36.522 % |
c |    180109 |   52653   136939 |   21236   19467   753313    38.7 | 36.522 % |
c |    180334 |   52653   136939 |   23360   19692   762998    38.7 | 36.522 % |
c |    180672 |   52653   136939 |   25696   20030   780628    39.0 | 36.522 % |
c |    181179 |   52653   136939 |   28266   20537   810883    39.5 | 36.522 % |
c |    181938 |   52653   136939 |   31092   21296   849267    39.9 | 36.522 % |
c |    183077 |   52653   136939 |   34201   22435   899688    40.1 | 36.522 % |
c |    184786 |   52643   136916 |   37622   24139   992629    41.1 | 36.535 % |
c |    187348 |   52639   136906 |   41384   26700  1120688    42.0 | 36.539 % |
c ==============================================================================
c Found solution: 1648
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    188862 |   52646   136923 |   17548   28214  1228249    43.5 | 36.539 % |
c |    188962 |   52646   136923 |   19302   14207   469546    33.1 | 36.539 % |
c |    189112 |   52646   136923 |   21233   14357   474223    33.0 | 36.539 % |
c |    189339 |   52646   136923 |   23356   14584   483674    33.2 | 36.539 % |
c |    189676 |   52646   136923 |   25692   14921   500108    33.5 | 36.539 % |
c |    190182 |   52646   136923 |   28261   15427   522460    33.9 | 36.539 % |
c |    190943 |   52646   136923 |   31087   16188   557553    34.4 | 36.539 % |
c |    192082 |   52646   136923 |   34196   17327   599942    34.6 | 36.539 % |
c |    193792 |   52646   136923 |   37615   19037   717191    37.7 | 36.539 % |
c |    196354 |   52632   136885 |   41377   21594   806921    37.4 | 36.552 % |
c |    200198 |   52080   135597 |   45514   25416  1020646    40.2 | 37.324 % |
c |    205964 |   52080   135597 |   50066   31182  1315835    42.2 | 37.324 % |
c |    214613 |   52067   135564 |   55073   39828  1789558    44.9 | 37.337 % |
c |    227587 |   52067   135564 |   60580   52802  2635487    49.9 | 37.337 % |
c ==============================================================================
c Found solution: 1639
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    239337 |   52047   135506 |   17349   64547  3435785    53.2 | 37.337 % |
c |    239438 |   52047   135506 |   19083   21363   926240    43.4 | 37.359 % |
c |    239590 |   52047   135506 |   20992   21515   932551    43.3 | 37.359 % |
c |    239815 |   52047   135506 |   23091   21740   941576    43.3 | 37.359 % |
c |    240154 |   52047   135506 |   25400   22079   952174    43.1 | 37.359 % |
c |    240661 |   52047   135506 |   27940   22586   977468    43.3 | 37.359 % |
c |    241421 |   52047   135506 |   30734   23346  1027014    44.0 | 37.359 % |
c |    242565 |   52047   135506 |   33808   24490  1076721    44.0 | 37.359 % |
c |    244273 |   52047   135506 |   37189   26198  1169764    44.7 | 37.359 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.95 0.90 2/54 19046
Raw data (stat): 19046 (runsolver) R 19045 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 490603909 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0014 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 19046
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 2436 0 0 0 992 6 0 0 25 0 1 0 490603909 12017664 2362 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2934 2362 603 41 0 2893 0
vsize: 11736
[startup+20.0023 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 19046
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 2539 0 0 0 1992 7 0 0 25 0 1 0 490603909 12447744 2465 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3039 2465 603 41 0 2998 0
vsize: 12156
[startup+30.0026 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 19046
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 2630 0 0 0 2991 7 0 0 25 0 1 0 490603909 12877824 2556 4294967295 134512640 134672761 3221224544 3221223648 134560212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3144 2556 603 41 0 3103 0
vsize: 12576
[startup+40.004 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 19046
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 2736 0 0 0 3990 9 0 0 25 0 1 0 490603909 13312000 2662 4294967295 134512640 134672761 3221224544 3221223680 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3250 2662 603 41 0 3209 0
vsize: 13000
[startup+50.0048 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 19046
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 2831 0 0 0 4989 10 0 0 25 0 1 0 490603909 13647872 2757 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3332 2757 603 41 0 3291 0
vsize: 13328
[startup+60.0053 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 19046
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 2926 0 0 0 5989 10 0 0 25 0 1 0 490603909 14049280 2852 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3430 2852 603 41 0 3389 0
vsize: 13720
[startup+70.0065 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 19046
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 3070 0 0 0 6988 11 0 0 25 0 1 0 490603909 14729216 2996 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3596 2996 603 41 0 3555 0
vsize: 14384
[startup+80.0074 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 19046
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 3236 0 0 0 7987 12 0 0 25 0 1 0 490603909 15392768 3162 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3758 3162 603 41 0 3717 0
vsize: 15032
[startup+90.0079 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 19046
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 3436 0 0 0 8987 12 0 0 25 0 1 0 490603909 16158720 3362 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3945 3362 603 41 0 3904 0
vsize: 15780
[startup+100.008 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 19046
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 3570 0 0 0 9986 13 0 0 25 0 1 0 490603909 16687104 3496 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4074 3496 603 41 0 4033 0
vsize: 16296
[startup+110.01 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 19046
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 3726 0 0 0 10985 14 0 0 25 0 1 0 490603909 17350656 3652 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4236 3652 603 41 0 4195 0
vsize: 16944
[startup+120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19046
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 3851 0 0 0 11984 15 0 0 25 0 1 0 490603909 17879040 3777 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4365 3777 603 41 0 4324 0
vsize: 17460
[startup+130.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19046
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 3982 0 0 0 12984 16 0 0 25 0 1 0 490603909 18407424 3908 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4494 3908 603 41 0 4453 0
vsize: 17976
[startup+140.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19046
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4158 0 0 0 13983 17 0 0 25 0 1 0 490603909 19070976 4084 4294967295 134512640 134672761 3221224544 3221223844 134556646 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4656 4084 603 41 0 4615 0
vsize: 18624
[startup+150.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19046
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4158 0 0 0 14983 17 0 0 25 0 1 0 490603909 19070976 4084 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4656 4084 603 41 0 4615 0
vsize: 18624
[startup+160.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19046
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4158 0 0 0 15983 17 0 0 25 0 1 0 490603909 19070976 4084 4294967295 134512640 134672761 3221224544 3221223680 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4656 4084 603 41 0 4615 0
vsize: 18624
[startup+170.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19046
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4158 0 0 0 16983 18 0 0 25 0 1 0 490603909 19070976 4084 4294967295 134512640 134672761 3221224544 3221223648 134560379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4656 4084 603 41 0 4615 0
vsize: 18624
[startup+180.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19046
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4158 0 0 0 17983 18 0 0 25 0 1 0 490603909 19070976 4084 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4656 4084 603 41 0 4615 0
vsize: 18624
[startup+190.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19046
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4158 0 0 0 18982 19 0 0 25 0 1 0 490603909 19070976 4084 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4656 4084 603 41 0 4615 0
vsize: 18624
[startup+200.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19046
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4158 0 0 0 19982 19 0 0 25 0 1 0 490603909 19070976 4084 4294967295 134512640 134672761 3221224544 3221223696 134541817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4656 4084 603 41 0 4615 0
vsize: 18624
[startup+210.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19046
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4276 0 0 0 20981 20 0 0 25 0 1 0 490603909 19595264 4202 4294967295 134512640 134672761 3221224544 3221223680 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4784 4202 603 41 0 4743 0
vsize: 19136
[startup+220.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19046
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4321 0 0 0 21981 20 0 0 25 0 1 0 490603909 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+230.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19046
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4321 0 0 0 22981 20 0 0 25 0 1 0 490603909 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+240.016 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 19046
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4321 0 0 0 23981 20 0 0 25 0 1 0 490603909 19755008 4247 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+250.016 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 19046
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4321 0 0 0 24981 20 0 0 25 0 1 0 490603909 19755008 4247 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+260.016 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 19046
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4321 0 0 0 25981 21 0 0 25 0 1 0 490603909 19755008 4247 4294967295 134512640 134672761 3221224544 3221223680 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+270.016 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 19046
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4321 0 0 0 26980 21 0 0 25 0 1 0 490603909 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+280.017 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 19046
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4321 0 0 0 27980 22 0 0 25 0 1 0 490603909 19755008 4247 4294967295 134512640 134672761 3221224544 3221223648 134559887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+290.017 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 19046
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4321 0 0 0 28979 22 0 0 25 0 1 0 490603909 19755008 4247 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+300.018 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 19046
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4321 0 0 0 29979 22 0 0 25 0 1 0 490603909 19755008 4247 4294967295 134512640 134672761 3221224544 3221223680 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+310.018 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 19046
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4321 0 0 0 30979 23 0 0 25 0 1 0 490603909 19755008 4247 4294967295 134512640 134672761 3221224544 3221223648 134560361 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+320.019 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 19046
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4321 0 0 0 31979 23 0 0 25 0 1 0 490603909 19755008 4247 4294967295 134512640 134672761 3221224544 3221223680 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+330.019 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 19046
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4321 0 0 0 32979 24 0 0 25 0 1 0 490603909 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+340.021 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 19046
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4321 0 0 0 33978 24 0 0 25 0 1 0 490603909 19755008 4247 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+350.022 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 19046
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4321 0 0 0 34978 24 0 0 25 0 1 0 490603909 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+360.022 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 19046
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4396 0 0 0 35978 25 0 0 25 0 1 0 490603909 20062208 4322 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4898 4322 603 41 0 4857 0
vsize: 19592
[startup+370.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19046
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4396 0 0 0 36977 25 0 0 25 0 1 0 490603909 20062208 4322 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4898 4322 603 41 0 4857 0
vsize: 19592
[startup+380.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19046
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4396 0 0 0 37977 25 0 0 25 0 1 0 490603909 20062208 4322 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4898 4322 603 41 0 4857 0
vsize: 19592
[startup+390.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19046
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4396 0 0 0 38977 26 0 0 25 0 1 0 490603909 20062208 4322 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4898 4322 603 41 0 4857 0
vsize: 19592
[startup+400.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19046
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4396 0 0 0 39977 26 0 0 25 0 1 0 490603909 20062208 4322 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4898 4322 603 41 0 4857 0
vsize: 19592
[startup+410.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19046
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4396 0 0 0 40976 27 0 0 25 0 1 0 490603909 20062208 4322 4294967295 134512640 134672761 3221224544 3221223648 134560191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4898 4322 603 41 0 4857 0
vsize: 19592
[startup+420.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19099
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4396 0 0 0 41973 30 0 0 25 0 1 0 490603909 20062208 4322 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4898 4322 603 41 0 4857 0
vsize: 19592
[startup+430.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19099
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4396 0 0 0 42973 30 0 0 25 0 1 0 490603909 20062208 4322 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4898 4322 603 41 0 4857 0
vsize: 19592
[startup+440.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19099
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4429 0 0 0 43973 30 0 0 25 0 1 0 490603909 20324352 4355 4294967295 134512640 134672761 3221224544 3221223648 134560276 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4962 4355 603 41 0 4921 0
vsize: 19848
[startup+450.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19099
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4516 0 0 0 44973 30 0 0 25 0 1 0 490603909 20717568 4442 4294967295 134512640 134672761 3221224544 3221223648 134560070 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5058 4442 603 41 0 5017 0
vsize: 20232
[startup+460.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19099
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4648 0 0 0 45972 31 0 0 25 0 1 0 490603909 21250048 4574 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5188 4574 603 41 0 5147 0
vsize: 20752
[startup+470.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19099
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4753 0 0 0 46972 31 0 0 25 0 1 0 490603909 21635072 4679 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5282 4679 603 41 0 5241 0
vsize: 21128
[startup+480.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19099
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4753 0 0 0 47973 31 0 0 25 0 1 0 490603909 21635072 4679 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5282 4679 603 41 0 5241 0
vsize: 21128
[startup+490.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19101
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4753 0 0 0 48973 31 0 0 25 0 1 0 490603909 21635072 4679 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5282 4679 603 41 0 5241 0
vsize: 21128
[startup+500.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19101
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4753 0 0 0 49973 31 0 0 25 0 1 0 490603909 21635072 4679 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5282 4679 603 41 0 5241 0
vsize: 21128
[startup+510.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19101
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4753 0 0 0 50973 31 0 0 25 0 1 0 490603909 21635072 4679 4294967295 134512640 134672761 3221224544 3221223648 134554673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5282 4679 603 41 0 5241 0
vsize: 21128
[startup+520.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19101
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4753 0 0 0 51973 31 0 0 25 0 1 0 490603909 21630976 4679 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5281 4679 603 41 0 5240 0
vsize: 21124
[startup+530.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19101
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4753 0 0 0 52973 31 0 0 25 0 1 0 490603909 21630976 4679 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5281 4679 603 41 0 5240 0
vsize: 21124
[startup+540.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19101
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4753 0 0 0 53974 31 0 0 25 0 1 0 490603909 21630976 4679 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5281 4679 603 41 0 5240 0
vsize: 21124
[startup+550.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19101
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4753 0 0 0 54974 31 0 0 25 0 1 0 490603909 21630976 4679 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5281 4679 603 41 0 5240 0
vsize: 21124
[startup+560.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19101
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4753 0 0 0 55974 31 0 0 25 0 1 0 490603909 21630976 4679 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5281 4679 603 41 0 5240 0
vsize: 21124
[startup+570.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19101
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4753 0 0 0 56974 31 0 0 25 0 1 0 490603909 21630976 4679 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5281 4679 603 41 0 5240 0
vsize: 21124
[startup+580.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19101
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4753 0 0 0 57975 31 0 0 25 0 1 0 490603909 21630976 4679 4294967295 134512640 134672761 3221224544 3221223680 134560683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5281 4679 603 41 0 5240 0
vsize: 21124
[startup+590.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19101
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4753 0 0 0 58975 31 0 0 25 0 1 0 490603909 21630976 4679 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5281 4679 603 41 0 5240 0
vsize: 21124
[startup+600.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19101
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4753 0 0 0 59975 31 0 0 25 0 1 0 490603909 21630976 4679 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5281 4679 603 41 0 5240 0
vsize: 21124
[startup+610.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19101
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4753 0 0 0 60976 31 0 0 25 0 1 0 490603909 21630976 4679 4294967295 134512640 134672761 3221224544 3221223728 134559170 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5281 4679 603 41 0 5240 0
vsize: 21124
[startup+620.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19101
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4753 0 0 0 61976 31 0 0 25 0 1 0 490603909 21630976 4679 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5281 4679 603 41 0 5240 0
vsize: 21124
[startup+630.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19101
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4754 0 0 0 62976 31 0 0 25 0 1 0 490603909 21630976 4680 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5281 4680 603 41 0 5240 0
vsize: 21124
[startup+640.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19101
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4756 0 0 0 63976 31 0 0 25 0 1 0 490603909 21630976 4682 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5281 4682 603 41 0 5240 0
vsize: 21124
[startup+650.044 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19101
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4828 0 0 0 64976 31 0 0 25 0 1 0 490603909 21901312 4754 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5347 4754 603 41 0 5306 0
vsize: 21388
[startup+660.044 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19101
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 4941 0 0 0 65976 32 0 0 25 0 1 0 490603909 22429696 4867 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5476 4867 603 41 0 5435 0
vsize: 21904
[startup+670.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19101
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5063 0 0 0 66976 32 0 0 25 0 1 0 490603909 22953984 4989 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5604 4989 603 41 0 5563 0
vsize: 22416
[startup+680.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19101
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5196 0 0 0 67976 32 0 0 25 0 1 0 490603909 23425024 5122 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5719 5122 603 41 0 5678 0
vsize: 22876
[startup+690.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19101
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5196 0 0 0 68977 32 0 0 25 0 1 0 490603909 23425024 5122 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5719 5122 603 41 0 5678 0
vsize: 22876
[startup+700.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19101
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5196 0 0 0 69977 32 0 0 25 0 1 0 490603909 23425024 5122 4294967295 134512640 134672761 3221224544 3221223680 134560703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5719 5122 603 41 0 5678 0
vsize: 22876
[startup+710.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19101
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5196 0 0 0 70977 32 0 0 25 0 1 0 490603909 23425024 5122 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5719 5122 603 41 0 5678 0
vsize: 22876
[startup+720.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19101
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5196 0 0 0 71977 32 0 0 25 0 1 0 490603909 23425024 5122 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5719 5122 603 41 0 5678 0
vsize: 22876
[startup+730.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19101
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5196 0 0 0 72977 32 0 0 25 0 1 0 490603909 23425024 5122 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5719 5122 603 41 0 5678 0
vsize: 22876
[startup+740.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19101
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5196 0 0 0 73977 32 0 0 25 0 1 0 490603909 23425024 5122 4294967295 134512640 134672761 3221224544 3221223744 134557913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5719 5122 603 41 0 5678 0
vsize: 22876
[startup+750.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19101
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5196 0 0 0 74977 32 0 0 25 0 1 0 490603909 23425024 5122 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5719 5122 603 41 0 5678 0
vsize: 22876
[startup+760.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19101
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5196 0 0 0 75978 32 0 0 25 0 1 0 490603909 23425024 5122 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5719 5122 603 41 0 5678 0
vsize: 22876
[startup+770.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19101
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5196 0 0 0 76978 32 0 0 25 0 1 0 490603909 23425024 5122 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5719 5122 603 41 0 5678 0
vsize: 22876
[startup+780.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19101
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5212 0 0 0 77978 32 0 0 25 0 1 0 490603909 23523328 5138 4294967295 134512640 134672761 3221224544 3221223648 134554671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+790.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19103
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5212 0 0 0 78978 33 0 0 25 0 1 0 490603909 23523328 5138 4294967295 134512640 134672761 3221224544 3221223744 134557811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+800.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19103
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5212 0 0 0 79978 33 0 0 25 0 1 0 490603909 23523328 5138 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+810.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19103
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5212 0 0 0 80978 33 0 0 25 0 1 0 490603909 23523328 5138 4294967295 134512640 134672761 3221224544 3221223648 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+820.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19103
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5212 0 0 0 81978 33 0 0 25 0 1 0 490603909 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+830.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19103
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5212 0 0 0 82978 33 0 0 25 0 1 0 490603909 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+840.051 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19103
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5212 0 0 0 83979 33 0 0 25 0 1 0 490603909 23523328 5138 4294967295 134512640 134672761 3221224544 3221223680 134565039 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+850.052 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19103
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5212 0 0 0 84979 33 0 0 25 0 1 0 490603909 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+860.052 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19103
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5212 0 0 0 85979 33 0 0 25 0 1 0 490603909 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+870.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19103
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5212 0 0 0 86979 33 0 0 25 0 1 0 490603909 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+880.052 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19103
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5212 0 0 0 87980 33 0 0 25 0 1 0 490603909 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+890.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19103
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5212 0 0 0 88980 33 0 0 25 0 1 0 490603909 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+900.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19103
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5212 0 0 0 89980 33 0 0 25 0 1 0 490603909 23523328 5138 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+910.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19103
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5212 0 0 0 90980 33 0 0 25 0 1 0 490603909 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+920.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19103
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5212 0 0 0 91980 33 0 0 25 0 1 0 490603909 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+930.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19103
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5212 0 0 0 92980 33 0 0 25 0 1 0 490603909 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+940.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19103
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5212 0 0 0 93981 33 0 0 25 0 1 0 490603909 23523328 5138 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+950.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19103
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5212 0 0 0 94981 33 0 0 25 0 1 0 490603909 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+960.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19103
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5212 0 0 0 95981 33 0 0 25 0 1 0 490603909 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+970.056 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19103
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5212 0 0 0 96981 33 0 0 25 0 1 0 490603909 23523328 5138 4294967295 134512640 134672761 3221224544 3221223708 134565024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+980.056 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19103
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5212 0 0 0 97981 33 0 0 25 0 1 0 490603909 23523328 5138 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+990.057 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19103
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5212 0 0 0 98981 33 0 0 25 0 1 0 490603909 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+1000.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19103
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5212 0 0 0 99982 33 0 0 25 0 1 0 490603909 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+1010.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19103
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5212 0 0 0 100982 33 0 0 25 0 1 0 490603909 23523328 5138 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+1020.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19103
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5212 0 0 0 101982 33 0 0 25 0 1 0 490603909 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+1030.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19103
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5212 0 0 0 102982 33 0 0 25 0 1 0 490603909 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+1040.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19103
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5212 0 0 0 103982 33 0 0 25 0 1 0 490603909 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134561256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+1050.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19103
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5313 0 0 0 104982 33 0 0 25 0 1 0 490603909 23916544 5239 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5839 5239 603 41 0 5798 0
vsize: 23356
[startup+1060.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19103
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5439 0 0 0 105982 34 0 0 25 0 1 0 490603909 24449024 5365 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5969 5365 603 41 0 5928 0
vsize: 23876
[startup+1070.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19103
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5553 0 0 0 106982 34 0 0 25 0 1 0 490603909 25014272 5479 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6107 5479 603 41 0 6066 0
vsize: 24428
[startup+1080.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19103
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5654 0 0 0 107982 34 0 0 25 0 1 0 490603909 25407488 5580 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6203 5580 603 41 0 6162 0
vsize: 24812
[startup+1090.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19103
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5789 0 0 0 108982 34 0 0 25 0 1 0 490603909 25935872 5715 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6332 5715 603 41 0 6291 0
vsize: 25328
[startup+1100.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19103
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 5917 0 0 0 109981 35 0 0 25 0 1 0 490603909 26501120 5843 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6470 5843 603 41 0 6429 0
vsize: 25880
[startup+1110.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19103
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 6033 0 0 0 110981 36 0 0 25 0 1 0 490603909 26898432 5959 4294967295 134512640 134672761 3221224544 3221223712 134561234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6567 5959 603 41 0 6526 0
vsize: 26268
[startup+1120.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19103
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 6155 0 0 0 111981 36 0 0 25 0 1 0 490603909 27435008 6081 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6698 6081 603 41 0 6657 0
vsize: 26792
[startup+1130.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19103
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 6286 0 0 0 112981 37 0 0 25 0 1 0 490603909 27967488 6212 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6828 6212 603 41 0 6787 0
vsize: 27312
[startup+1140.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19103
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 6415 0 0 0 113980 37 0 0 25 0 1 0 490603909 28504064 6341 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6959 6341 603 41 0 6918 0
vsize: 27836
[startup+1150.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19103
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 6551 0 0 0 114981 37 0 0 25 0 1 0 490603909 29040640 6477 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7090 6477 603 41 0 7049 0
vsize: 28360
[startup+1160.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19103
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 6659 0 0 0 115981 37 0 0 25 0 1 0 490603909 29466624 6585 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7194 6585 603 41 0 7153 0
vsize: 28776
[startup+1170.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19103
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 6718 0 0 0 116981 38 0 0 25 0 1 0 490603909 29679616 6644 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7246 6644 603 41 0 7205 0
vsize: 28984
[startup+1180.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19103
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 6718 0 0 0 117981 38 0 0 25 0 1 0 490603909 29679616 6644 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7246 6644 603 41 0 7205 0
vsize: 28984
[startup+1190.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19103
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 6718 0 0 0 118981 38 0 0 25 0 1 0 490603909 29679616 6644 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7246 6644 603 41 0 7205 0
vsize: 28984
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19103
Raw data (stat): 19046 (minisat+) R 19045 5897 5896 0 -1 0 6718 0 0 0 119981 38 0 0 25 0 1 0 490603909 29679616 6644 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7246 6644 603 41 0 7205 0
vsize: 28984
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 19103
Raw data (stat): 19046 (minisat+) Z 19045 5897 5896 0 -1 12 6721 0 0 0 119981 39 0 0 25 0 1 0 490603909 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.08
CPU time (s): 1200.21
CPU user time (s): 1199.82
CPU system time (s): 0.395939
CPU usage (%): 100.011
Max. virtual memory (Kb): 28984
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####