PB'05 competition: run trace

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:
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.
SOLVER DATA
This is the output of the solver (stdout and stderr).
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.
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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-p0201.opb
MD5SUM	8c361d02d5162bb0b133ab6ed38f9294
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
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 numbers	15
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02284
Number of variables	201
Total number of constraints	334
Number of constraints which are clauses	20
Number of constraints which are cardinality constraints (but not clauses)	227
Number of constraints which are nor clauses,nor cardinality constraints	87
Minimum length of a constraint	1
Maximum length of a constraint	67
Trace number 15021

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc23 THE 2005-04-21 02:37:33 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18707 boxname=wulflinc23 idbench=1439 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  8c361d02d5162bb0b133ab6ed38f9294  /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-p0201.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-p0201.opb /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-p0201.opb
IDLAUNCH: 18707
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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	: 3
cpu MHz		: 451.037
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:        757420 kB
Buffers:         12928 kB
Cached:         235432 kB
SwapCached:        520 kB
Active:          51860 kB
Inactive:       198584 kB
HighTotal:      131008 kB
HighFree:         3528 kB
LowTotal:       903652 kB
LowFree:        753892 kB
SwapTotal:     2097136 kB
SwapFree:      2095824 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5220 kB
Slab:            21160 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 02:57:36 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 18707 7 1200.2 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 [1mFound solution: 2734[0m
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 [1mFound solution: 2329[0m
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 [1mFound solution: 2304[0m
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 [1mFound solution: 2283[0m
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 [1mFound solution: 2225[0m
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 [1mFound solution: 2191[0m
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 [1mFound solution: 2179[0m
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 [1mFound solution: 2173[0m
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 [1mFound solution: 2028[0m
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 [1mFound solution: 1924[0m
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 [1mFound solution: 1921[0m
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 [1mFound solution: 1907[0m
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 [1mFound solution: 1891[0m
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 [1mFound solution: 1889[0m
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 [1mFound solution: 1882[0m
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 [1mFound solution: 1879[0m
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 [1mFound solution: 1857[0m
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 [1mFound solution: 1851[0m
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 [1mFound solution: 1847[0m
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 [1mFound solution: 1845[0m
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 [1mFound solution: 1827[0m
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 [1mFound solution: 1819[0m
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 [1mFound solution: 1789[0m
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 [1mFound solution: 1779[0m
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 [1mFound solution: 1778[0m
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 [1mFound solution: 1771[0m
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 [1mFound solution: 1761[0m
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 [1mFound solution: 1751[0m
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 [1mFound solution: 1730[0m
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 [1mFound solution: 1709[0m
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 [1mFound solution: 1708[0m
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 [1mFound solution: 1704[0m
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 [1mFound solution: 1701[0m
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 [1mFound solution: 1681[0m
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 [1mFound solution: 1679[0m
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 [1mFound solution: 1675[0m
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 [1mFound solution: 1674[0m
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 [1mFound solution: 1673[0m
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 [1mFound solution: 1671[0m
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 [1mFound solution: 1668[0m
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 [1mFound solution: 1659[0m
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 [1mFound solution: 1651[0m
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 [1mFound solution: 1648[0m
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 % |
#### 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.92 0.95 0.91 2/54 27283
Raw data (stat): 27283 (runsolver) R 27282 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 541534760 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 2436 0 0 0 992 6 0 0 25 0 1 0 541534760 12017664 2362 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2934 2362 603 41 0 2893 0
vsize: 11736
[startup+20.0012 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 2539 0 0 0 1991 7 0 0 25 0 1 0 541534760 12447744 2465 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3039 2465 603 41 0 2998 0
vsize: 12156
[startup+30.0012 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 2618 0 0 0 2990 8 0 0 25 0 1 0 541534760 12877824 2544 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3144 2544 603 41 0 3103 0
vsize: 12576
[startup+40.0015 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 2732 0 0 0 3990 9 0 0 25 0 1 0 541534760 13312000 2658 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3250 2658 603 41 0 3209 0
vsize: 13000
[startup+50.0021 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 2831 0 0 0 4989 10 0 0 25 0 1 0 541534760 13647872 2757 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3332 2757 603 41 0 3291 0
vsize: 13328
[startup+60.0032 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 2918 0 0 0 5989 10 0 0 25 0 1 0 541534760 14049280 2844 4294967295 134512640 134672761 3221224544 3221223680 134560619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3430 2844 603 41 0 3389 0
vsize: 13720
[startup+70.0034 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 3057 0 0 0 6988 11 0 0 25 0 1 0 541534760 14729216 2983 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3596 2983 603 41 0 3555 0
vsize: 14384
[startup+80.0216 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 3212 0 0 0 7989 12 0 0 25 0 1 0 541534760 15261696 3138 4294967295 134512640 134672761 3221224544 3221223712 134561220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3726 3138 603 41 0 3685 0
vsize: 14904
[startup+90.0221 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 3371 0 0 0 8988 13 0 0 25 0 1 0 541534760 15892480 3297 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3880 3297 603 41 0 3839 0
vsize: 15520
[startup+100.021 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 3540 0 0 0 9987 14 0 0 25 0 1 0 541534760 16556032 3466 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4042 3466 603 41 0 4001 0
vsize: 16168
[startup+110.022 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 3684 0 0 0 10987 14 0 0 25 0 1 0 541534760 17219584 3610 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4204 3610 603 41 0 4163 0
vsize: 16816
[startup+120.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 3827 0 0 0 11986 15 0 0 25 0 1 0 541534760 17747968 3753 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4333 3753 603 41 0 4292 0
vsize: 17332
[startup+130.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 3943 0 0 0 12985 16 0 0 25 0 1 0 541534760 18272256 3869 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4461 3869 603 41 0 4420 0
vsize: 17844
[startup+140.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4098 0 0 0 13984 17 0 0 25 0 1 0 541534760 18939904 4024 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4624 4024 603 41 0 4583 0
vsize: 18496
[startup+150.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4158 0 0 0 14984 18 0 0 25 0 1 0 541534760 19070976 4084 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4656 4084 603 41 0 4615 0
vsize: 18624
[startup+160.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4158 0 0 0 15984 18 0 0 25 0 1 0 541534760 19070976 4084 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4656 4084 603 41 0 4615 0
vsize: 18624
[startup+170.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4158 0 0 0 16984 18 0 0 25 0 1 0 541534760 19070976 4084 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4656 4084 603 41 0 4615 0
vsize: 18624
[startup+180.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4158 0 0 0 17983 19 0 0 25 0 1 0 541534760 19070976 4084 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4656 4084 603 41 0 4615 0
vsize: 18624
[startup+190.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4158 0 0 0 18983 19 0 0 25 0 1 0 541534760 19070976 4084 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4656 4084 603 41 0 4615 0
vsize: 18624
[startup+200.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4158 0 0 0 19983 19 0 0 25 0 1 0 541534760 19070976 4084 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4656 4084 603 41 0 4615 0
vsize: 18624
[startup+210.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4237 0 0 0 20982 20 0 0 25 0 1 0 541534760 19464192 4163 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4752 4163 603 41 0 4711 0
vsize: 19008
[startup+220.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4321 0 0 0 21982 21 0 0 25 0 1 0 541534760 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+230.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4321 0 0 0 22981 21 0 0 25 0 1 0 541534760 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+240.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4321 0 0 0 23981 21 0 0 25 0 1 0 541534760 19755008 4247 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+250.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4321 0 0 0 24981 21 0 0 25 0 1 0 541534760 19755008 4247 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+260.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4321 0 0 0 25981 21 0 0 25 0 1 0 541534760 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+270.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4321 0 0 0 26981 22 0 0 25 0 1 0 541534760 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+280.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4321 0 0 0 27981 22 0 0 25 0 1 0 541534760 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+290.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4321 0 0 0 28980 22 0 0 25 0 1 0 541534760 19755008 4247 4294967295 134512640 134672761 3221224544 3221223744 134557919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+300.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4321 0 0 0 29980 22 0 0 25 0 1 0 541534760 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+310.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4321 0 0 0 30980 23 0 0 25 0 1 0 541534760 19755008 4247 4294967295 134512640 134672761 3221224544 3221223648 134559998 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+320.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4321 0 0 0 31980 23 0 0 25 0 1 0 541534760 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+330.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4321 0 0 0 32980 23 0 0 25 0 1 0 541534760 19755008 4247 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+340.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4321 0 0 0 33979 24 0 0 25 0 1 0 541534760 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+350.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4321 0 0 0 34978 25 0 0 25 0 1 0 541534760 19755008 4247 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+360.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4339 0 0 0 35978 25 0 0 25 0 1 0 541534760 19886080 4265 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4855 4265 603 41 0 4814 0
vsize: 19420
[startup+370.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4396 0 0 0 36978 25 0 0 25 0 1 0 541534760 20062208 4322 4294967295 134512640 134672761 3221224544 3221223648 134560492 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4396 0 0 0 37978 25 0 0 25 0 1 0 541534760 20062208 4322 4294967295 134512640 134672761 3221224544 3221223712 134561391 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4396 0 0 0 38978 25 0 0 25 0 1 0 541534760 20062208 4322 4294967295 134512640 134672761 3221224544 3221223716 134556639 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4396 0 0 0 39978 25 0 0 25 0 1 0 541534760 20062208 4322 4294967295 134512640 134672761 3221224544 3221223704 134561240 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4396 0 0 0 40979 25 0 0 25 0 1 0 541534760 20062208 4322 4294967295 134512640 134672761 3221224544 3221223744 134557830 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4396 0 0 0 41979 25 0 0 25 0 1 0 541534760 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+430.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4396 0 0 0 42979 25 0 0 25 0 1 0 541534760 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+440.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4396 0 0 0 43979 25 0 0 25 0 1 0 541534760 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+450.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4429 0 0 0 44979 25 0 0 25 0 1 0 541534760 20324352 4355 4294967295 134512640 134672761 3221224544 3221223648 134560002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4962 4355 603 41 0 4921 0
vsize: 19848
[startup+460.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4510 0 0 0 45979 26 0 0 25 0 1 0 541534760 20717568 4436 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5058 4436 603 41 0 5017 0
vsize: 20232
[startup+470.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4636 0 0 0 46979 26 0 0 25 0 1 0 541534760 21250048 4562 4294967295 134512640 134672761 3221224544 3221223680 134560637 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5188 4562 603 41 0 5147 0
vsize: 20752
[startup+480.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4753 0 0 0 47979 26 0 0 25 0 1 0 541534760 21635072 4679 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5282 4679 603 41 0 5241 0
vsize: 21128
[startup+490.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4753 0 0 0 48979 26 0 0 25 0 1 0 541534760 21635072 4679 4294967295 134512640 134672761 3221224544 3221223712 134561018 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5282 4679 603 41 0 5241 0
vsize: 21128
[startup+500.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4753 0 0 0 49979 26 0 0 25 0 1 0 541534760 21635072 4679 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5282 4679 603 41 0 5241 0
vsize: 21128
[startup+510.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4753 0 0 0 50979 26 0 0 25 0 1 0 541534760 21635072 4679 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5282 4679 603 41 0 5241 0
vsize: 21128
[startup+520.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4753 0 0 0 51979 26 0 0 25 0 1 0 541534760 21635072 4679 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5282 4679 603 41 0 5241 0
vsize: 21128
[startup+530.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4753 0 0 0 52979 26 0 0 25 0 1 0 541534760 21630976 4679 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5281 4679 603 41 0 5240 0
vsize: 21124
[startup+540.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4753 0 0 0 53980 26 0 0 25 0 1 0 541534760 21630976 4679 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5281 4679 603 41 0 5240 0
vsize: 21124
[startup+550.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4753 0 0 0 54980 26 0 0 25 0 1 0 541534760 21630976 4679 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5281 4679 603 41 0 5240 0
vsize: 21124
[startup+560.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4753 0 0 0 55980 26 0 0 25 0 1 0 541534760 21630976 4679 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5281 4679 603 41 0 5240 0
vsize: 21124
[startup+570.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4753 0 0 0 56980 26 0 0 25 0 1 0 541534760 21630976 4679 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5281 4679 603 41 0 5240 0
vsize: 21124
[startup+580.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4753 0 0 0 57980 26 0 0 25 0 1 0 541534760 21630976 4679 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5281 4679 603 41 0 5240 0
vsize: 21124
[startup+590.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4753 0 0 0 58981 26 0 0 25 0 1 0 541534760 21630976 4679 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5281 4679 603 41 0 5240 0
vsize: 21124
[startup+600.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4753 0 0 0 59981 26 0 0 25 0 1 0 541534760 21630976 4679 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5281 4679 603 41 0 5240 0
vsize: 21124
[startup+610.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4753 0 0 0 60981 27 0 0 25 0 1 0 541534760 21630976 4679 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5281 4679 603 41 0 5240 0
vsize: 21124
[startup+620.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4753 0 0 0 61981 27 0 0 25 0 1 0 541534760 21630976 4679 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5281 4679 603 41 0 5240 0
vsize: 21124
[startup+630.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4753 0 0 0 62981 27 0 0 25 0 1 0 541534760 21630976 4679 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5281 4679 603 41 0 5240 0
vsize: 21124
[startup+640.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4753 0 0 0 63981 27 0 0 25 0 1 0 541534760 21630976 4679 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5281 4679 603 41 0 5240 0
vsize: 21124
[startup+650.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4754 0 0 0 64982 27 0 0 25 0 1 0 541534760 21630976 4680 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5281 4680 603 41 0 5240 0
vsize: 21124
[startup+660.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4756 0 0 0 65982 27 0 0 25 0 1 0 541534760 21630976 4682 4294967295 134512640 134672761 3221224544 3221223648 134560184 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5281 4682 603 41 0 5240 0
vsize: 21124
[startup+670.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4824 0 0 0 66982 27 0 0 25 0 1 0 541534760 21901312 4750 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5347 4750 603 41 0 5306 0
vsize: 21388
[startup+680.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 4934 0 0 0 67982 27 0 0 25 0 1 0 541534760 22429696 4860 4294967295 134512640 134672761 3221224544 3221223680 134560667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5476 4860 603 41 0 5435 0
vsize: 21904
[startup+690.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5051 0 0 0 68981 28 0 0 25 0 1 0 541534760 22822912 4977 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5572 4977 603 41 0 5531 0
vsize: 22288
[startup+700.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5163 0 0 0 69981 28 0 0 25 0 1 0 541534760 23351296 5089 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5701 5089 603 41 0 5660 0
vsize: 22804
[startup+710.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5196 0 0 0 70981 28 0 0 25 0 1 0 541534760 23425024 5122 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5719 5122 603 41 0 5678 0
vsize: 22876
[startup+720.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5196 0 0 0 71981 28 0 0 25 0 1 0 541534760 23425024 5122 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5719 5122 603 41 0 5678 0
vsize: 22876
[startup+730.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5196 0 0 0 72981 28 0 0 25 0 1 0 541534760 23425024 5122 4294967295 134512640 134672761 3221224544 3221223680 134560604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5719 5122 603 41 0 5678 0
vsize: 22876
[startup+740.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5196 0 0 0 73981 29 0 0 25 0 1 0 541534760 23425024 5122 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5719 5122 603 41 0 5678 0
vsize: 22876
[startup+750.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5196 0 0 0 74981 29 0 0 25 0 1 0 541534760 23425024 5122 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5719 5122 603 41 0 5678 0
vsize: 22876
[startup+760.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5196 0 0 0 75981 29 0 0 25 0 1 0 541534760 23425024 5122 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5719 5122 603 41 0 5678 0
vsize: 22876
[startup+770.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5196 0 0 0 76981 29 0 0 25 0 1 0 541534760 23425024 5122 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5719 5122 603 41 0 5678 0
vsize: 22876
[startup+780.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5196 0 0 0 77982 29 0 0 25 0 1 0 541534760 23425024 5122 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5719 5122 603 41 0 5678 0
vsize: 22876
[startup+790.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5196 0 0 0 78982 29 0 0 25 0 1 0 541534760 23425024 5122 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5719 5122 603 41 0 5678 0
vsize: 22876
[startup+800.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5196 0 0 0 79982 29 0 0 25 0 1 0 541534760 23425024 5122 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5719 5122 603 41 0 5678 0
vsize: 22876
[startup+810.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5212 0 0 0 80982 29 0 0 25 0 1 0 541534760 23523328 5138 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+820.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5212 0 0 0 81982 29 0 0 25 0 1 0 541534760 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+830.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5212 0 0 0 82982 29 0 0 25 0 1 0 541534760 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+840.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5212 0 0 0 83983 29 0 0 25 0 1 0 541534760 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+850.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5212 0 0 0 84983 29 0 0 25 0 1 0 541534760 23523328 5138 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+860.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5212 0 0 0 85983 29 0 0 25 0 1 0 541534760 23523328 5138 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+870.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5212 0 0 0 86983 29 0 0 25 0 1 0 541534760 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+880.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5212 0 0 0 87983 29 0 0 25 0 1 0 541534760 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+890.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5212 0 0 0 88983 29 0 0 25 0 1 0 541534760 23523328 5138 4294967295 134512640 134672761 3221224544 3221223648 134560150 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+900.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5212 0 0 0 89983 29 0 0 25 0 1 0 541534760 23523328 5138 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+910.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5212 0 0 0 90984 29 0 0 25 0 1 0 541534760 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+920.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5212 0 0 0 91984 29 0 0 25 0 1 0 541534760 23523328 5138 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+930.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5212 0 0 0 92984 29 0 0 25 0 1 0 541534760 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+940.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5212 0 0 0 93984 29 0 0 25 0 1 0 541534760 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+950.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5212 0 0 0 94984 29 0 0 25 0 1 0 541534760 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+960.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5212 0 0 0 95984 29 0 0 25 0 1 0 541534760 23523328 5138 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+970.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5212 0 0 0 96985 29 0 0 25 0 1 0 541534760 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+980.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5212 0 0 0 97985 29 0 0 25 0 1 0 541534760 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+990.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5212 0 0 0 98985 29 0 0 25 0 1 0 541534760 23523328 5138 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5212 0 0 0 99985 29 0 0 25 0 1 0 541534760 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5212 0 0 0 100985 29 0 0 25 0 1 0 541534760 23523328 5138 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5212 0 0 0 101985 30 0 0 25 0 1 0 541534760 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5212 0 0 0 102985 30 0 0 25 0 1 0 541534760 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5212 0 0 0 103985 30 0 0 25 0 1 0 541534760 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5212 0 0 0 104985 30 0 0 25 0 1 0 541534760 23523328 5138 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5212 0 0 0 105985 30 0 0 25 0 1 0 541534760 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5212 0 0 0 106986 30 0 0 25 0 1 0 541534760 23523328 5138 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5212 0 0 0 107986 30 0 0 25 0 1 0 541534760 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5320 0 0 0 108986 30 0 0 25 0 1 0 541534760 23916544 5246 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5839 5246 603 41 0 5798 0
vsize: 23356
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5439 0 0 0 109985 31 0 0 25 0 1 0 541534760 24449024 5365 4294967295 134512640 134672761 3221224544 3221223648 134560252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5969 5365 603 41 0 5928 0
vsize: 23876
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5547 0 0 0 110985 31 0 0 25 0 1 0 541534760 24883200 5473 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6075 5473 603 41 0 6034 0
vsize: 24300
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5646 0 0 0 111985 31 0 0 25 0 1 0 541534760 25276416 5572 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6171 5572 603 41 0 6130 0
vsize: 24684
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5771 0 0 0 112984 32 0 0 25 0 1 0 541534760 25800704 5697 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6299 5697 603 41 0 6258 0
vsize: 25196
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 5895 0 0 0 113984 32 0 0 25 0 1 0 541534760 26365952 5821 4294967295 134512640 134672761 3221224544 3221223712 134561121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6437 5821 603 41 0 6396 0
vsize: 25748
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 6012 0 0 0 114984 33 0 0 25 0 1 0 541534760 26898432 5938 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6567 5938 603 41 0 6526 0
vsize: 26268
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 6123 0 0 0 115984 33 0 0 25 0 1 0 541534760 27299840 6049 4294967295 134512640 134672761 3221224544 3221223680 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6665 6049 603 41 0 6624 0
vsize: 26660
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 6244 0 0 0 116983 34 0 0 25 0 1 0 541534760 27832320 6170 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6795 6170 603 41 0 6754 0
vsize: 27180
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 6363 0 0 0 117983 34 0 0 25 0 1 0 541534760 28233728 6289 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6893 6289 603 41 0 6852 0
vsize: 27572
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 6496 0 0 0 118983 35 0 0 25 0 1 0 541534760 28774400 6422 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7025 6422 603 41 0 6984 0
vsize: 28100
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27283
Raw data (stat): 27283 (minisat+) R 27282 3260 3259 0 -1 0 6610 0 0 0 119983 35 0 0 25 0 1 0 541534760 29306880 6536 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7155 6536 603 41 0 7114 0
vsize: 28620
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 27283
Raw data (stat): 27283 (minisat+) Z 27282 3260 3259 0 -1 12 6613 0 0 0 119983 36 0 0 25 0 1 0 541534760 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.04
CPU time (s): 1200.2
CPU user time (s): 1199.83
CPU system time (s): 0.368943
CPU usage (%): 100.013
Max. virtual memory (Kb): 28620
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####