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/miplib/normalized-mps-v2-13-7-p0201.opb
MD5SUM	ffa3a55eb53181880328dd1b84f91e66
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.02184
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 19033

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc22 THE 2005-04-21 17:40:53 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17121 boxname=wulflinc22 idbench=1317 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ffa3a55eb53181880328dd1b84f91e66  /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-p0201.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-p0201.opb /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-p0201.opb
IDLAUNCH: 17121
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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.031
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:        347744 kB
Buffers:         30488 kB
Cached:         627800 kB
SwapCached:         20 kB
Active:         118420 kB
Inactive:       542556 kB
HighTotal:      131008 kB
HighFree:         7756 kB
LowTotal:       903652 kB
LowFree:        339988 kB
SwapTotal:     2097892 kB
SwapFree:      2097664 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6640 kB
Slab:            20252 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 18:00:55 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 17121 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 % |
c ==============================================================================
c [1mFound solution: 1639[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 |    239337 |   52047   135506 |   17349   64547  3435785    53.2 | 37.337 % |
c |    239438 |   52047   135506 |   19083   21363   926240    43.4 | 37.359 % |
c |    239590 |   52047   135506 |   20992   21515   932551    43.3 | 37.359 % |
c |    239815 |   52047   135506 |   23091   21740   941576    43.3 | 37.359 % |
c |    240154 |   52047   135506 |   25400   22079   952174    43.1 | 37.359 % |
c |    240661 |   52047   135506 |   27940   22586   977468    43.3 | 37.359 % |
c |    241421 |   52047   135506 |   30734   23346  1027014    44.0 | 37.359 % |
c |    242565 |   52047   135506 |   33808   24490  1076721    44.0 | 37.359 % |
c |    244273 |   52047   135506 |   37189   26198  1169764    44.7 | 37.359 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.93 0.98 0.93 2/54 5339
Raw data (stat): 5339 (runsolver) R 5338 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 546954394 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.0006 s]
Raw data (loadavg): 0.94 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 2436 0 0 0 993 5 0 0 25 0 1 0 546954394 12017664 2362 4294967295 134512640 134672761 3221224544 3221223692 134560631 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.95 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 2539 0 0 0 1992 6 0 0 25 0 1 0 546954394 12447744 2465 4294967295 134512640 134672761 3221224544 3221223712 134560830 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.0015 s]
Raw data (loadavg): 0.95 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 2620 0 0 0 2992 7 0 0 25 0 1 0 546954394 12877824 2546 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3144 2546 603 41 0 3103 0
vsize: 12576
[startup+40.0022 s]
Raw data (loadavg): 0.96 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 2733 0 0 0 3991 7 0 0 25 0 1 0 546954394 13312000 2659 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3250 2659 603 41 0 3209 0
vsize: 13000
[startup+50.0033 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 2831 0 0 0 4991 8 0 0 25 0 1 0 546954394 13647872 2757 4294967295 134512640 134672761 3221224544 3221223712 134561266 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.0026 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 2920 0 0 0 5990 9 0 0 25 0 1 0 546954394 14049280 2846 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3430 2846 603 41 0 3389 0
vsize: 13720
[startup+70.0034 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 3060 0 0 0 6990 9 0 0 25 0 1 0 546954394 14729216 2986 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3596 2986 603 41 0 3555 0
vsize: 14384
[startup+80.0045 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 3217 0 0 0 7989 10 0 0 25 0 1 0 546954394 15261696 3143 4294967295 134512640 134672761 3221224544 3221223636 1075346528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3726 3143 603 41 0 3685 0
vsize: 14904
[startup+90.0048 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 3390 0 0 0 8987 11 0 0 25 0 1 0 546954394 16027648 3316 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3913 3316 603 41 0 3872 0
vsize: 15652
[startup+100.004 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 3548 0 0 0 9987 12 0 0 25 0 1 0 546954394 16687104 3474 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4074 3474 603 41 0 4033 0
vsize: 16296
[startup+110.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 3704 0 0 0 10986 13 0 0 25 0 1 0 546954394 17219584 3630 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4204 3630 603 41 0 4163 0
vsize: 16816
[startup+120.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 3840 0 0 0 11985 14 0 0 25 0 1 0 546954394 17879040 3766 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4365 3766 603 41 0 4324 0
vsize: 17460
[startup+130.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 3956 0 0 0 12985 14 0 0 25 0 1 0 546954394 18272256 3882 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4461 3882 603 41 0 4420 0
vsize: 17844
[startup+140.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4119 0 0 0 13984 15 0 0 25 0 1 0 546954394 18939904 4045 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4624 4045 603 41 0 4583 0
vsize: 18496
[startup+150.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4158 0 0 0 14984 15 0 0 25 0 1 0 546954394 19070976 4084 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4656 4084 603 41 0 4615 0
vsize: 18624
[startup+160.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4158 0 0 0 15984 16 0 0 25 0 1 0 546954394 19070976 4084 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4656 4084 603 41 0 4615 0
vsize: 18624
[startup+170.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4158 0 0 0 16984 16 0 0 25 0 1 0 546954394 19070976 4084 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4656 4084 603 41 0 4615 0
vsize: 18624
[startup+180.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4158 0 0 0 17984 16 0 0 25 0 1 0 546954394 19070976 4084 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4656 4084 603 41 0 4615 0
vsize: 18624
[startup+190.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4158 0 0 0 18984 16 0 0 25 0 1 0 546954394 19070976 4084 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4656 4084 603 41 0 4615 0
vsize: 18624
[startup+200.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4158 0 0 0 19984 16 0 0 25 0 1 0 546954394 19070976 4084 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4656 4084 603 41 0 4615 0
vsize: 18624
[startup+210.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4266 0 0 0 20984 16 0 0 25 0 1 0 546954394 19595264 4192 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4784 4192 603 41 0 4743 0
vsize: 19136
[startup+220.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4321 0 0 0 21984 16 0 0 25 0 1 0 546954394 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+230.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4321 0 0 0 22984 16 0 0 25 0 1 0 546954394 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+240.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4321 0 0 0 23985 16 0 0 25 0 1 0 546954394 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+250.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4321 0 0 0 24985 16 0 0 25 0 1 0 546954394 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+260.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4321 0 0 0 25985 16 0 0 25 0 1 0 546954394 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+270.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4321 0 0 0 26985 16 0 0 25 0 1 0 546954394 19755008 4247 4294967295 134512640 134672761 3221224544 3221223680 134560716 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+280.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4321 0 0 0 27985 17 0 0 25 0 1 0 546954394 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+290.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4321 0 0 0 28985 17 0 0 25 0 1 0 546954394 19755008 4247 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+300.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4321 0 0 0 29985 17 0 0 25 0 1 0 546954394 19755008 4247 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+310.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4321 0 0 0 30986 17 0 0 25 0 1 0 546954394 19755008 4247 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+320.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4321 0 0 0 31986 17 0 0 25 0 1 0 546954394 19755008 4247 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+330.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4321 0 0 0 32986 17 0 0 25 0 1 0 546954394 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+340.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4321 0 0 0 33986 17 0 0 25 0 1 0 546954394 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+350.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4321 0 0 0 34986 17 0 0 25 0 1 0 546954394 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+360.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4396 0 0 0 35986 17 0 0 25 0 1 0 546954394 20062208 4322 4294967295 134512640 134672761 3221224544 3221223712 134561275 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4898 4322 603 41 0 4857 0
vsize: 19592
[startup+370.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4396 0 0 0 36986 17 0 0 25 0 1 0 546954394 20062208 4322 4294967295 134512640 134672761 3221224544 3221223712 134560996 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.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4396 0 0 0 37986 17 0 0 25 0 1 0 546954394 20062208 4322 4294967295 134512640 134672761 3221224544 3221223712 134560940 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.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4396 0 0 0 38987 17 0 0 25 0 1 0 546954394 20062208 4322 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4898 4322 603 41 0 4857 0
vsize: 19592
[startup+400.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4396 0 0 0 39987 17 0 0 25 0 1 0 546954394 20062208 4322 4294967295 134512640 134672761 3221224544 3221223648 134560318 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.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4396 0 0 0 40987 17 0 0 25 0 1 0 546954394 20062208 4322 4294967295 134512640 134672761 3221224544 3221223712 134560988 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.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4396 0 0 0 41987 17 0 0 25 0 1 0 546954394 20062208 4322 4294967295 134512640 134672761 3221224544 3221223712 134561261 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.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4396 0 0 0 42987 17 0 0 25 0 1 0 546954394 20062208 4322 4294967295 134512640 134672761 3221224544 3221223744 134557809 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.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4429 0 0 0 43987 17 0 0 25 0 1 0 546954394 20324352 4355 4294967295 134512640 134672761 3221224544 3221223728 134559332 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4962 4355 603 41 0 4921 0
vsize: 19848
[startup+450.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4521 0 0 0 44987 18 0 0 25 0 1 0 546954394 20717568 4447 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5058 4447 603 41 0 5017 0
vsize: 20232
[startup+460.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4650 0 0 0 45987 18 0 0 25 0 1 0 546954394 21250048 4576 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5188 4576 603 41 0 5147 0
vsize: 20752
[startup+470.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4753 0 0 0 46987 18 0 0 25 0 1 0 546954394 21635072 4679 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5282 4679 603 41 0 5241 0
vsize: 21128
[startup+480.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4753 0 0 0 47987 18 0 0 25 0 1 0 546954394 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+490.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4753 0 0 0 48987 18 0 0 25 0 1 0 546954394 21635072 4679 4294967295 134512640 134672761 3221224544 3221223680 134560729 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.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4753 0 0 0 49988 18 0 0 25 0 1 0 546954394 21635072 4679 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4753 0 0 0 50988 18 0 0 25 0 1 0 546954394 21635072 4679 4294967295 134512640 134672761 3221224544 3221223844 134556682 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.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4753 0 0 0 51988 18 0 0 25 0 1 0 546954394 21630976 4679 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5281 4679 603 41 0 5240 0
vsize: 21124
[startup+530.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4753 0 0 0 52988 18 0 0 25 0 1 0 546954394 21630976 4679 4294967295 134512640 134672761 3221224544 3221223680 134560566 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.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4753 0 0 0 53988 19 0 0 25 0 1 0 546954394 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.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4753 0 0 0 54988 19 0 0 25 0 1 0 546954394 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.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4753 0 0 0 55988 19 0 0 25 0 1 0 546954394 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+570.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4753 0 0 0 56989 19 0 0 25 0 1 0 546954394 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+580.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4753 0 0 0 57989 19 0 0 25 0 1 0 546954394 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+590.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4753 0 0 0 58989 19 0 0 25 0 1 0 546954394 21630976 4679 4294967295 134512640 134672761 3221224544 3221223728 134558899 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.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4753 0 0 0 59989 19 0 0 25 0 1 0 546954394 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+610.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4753 0 0 0 60989 19 0 0 25 0 1 0 546954394 21630976 4679 4294967295 134512640 134672761 3221224544 3221223712 134560929 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.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4753 0 0 0 61989 19 0 0 25 0 1 0 546954394 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+630.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4754 0 0 0 62989 19 0 0 25 0 1 0 546954394 21630976 4680 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5281 4680 603 41 0 5240 0
vsize: 21124
[startup+640.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4756 0 0 0 63989 19 0 0 25 0 1 0 546954394 21630976 4682 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5281 4682 603 41 0 5240 0
vsize: 21124
[startup+650.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4819 0 0 0 64989 19 0 0 25 0 1 0 546954394 21901312 4745 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5347 4745 603 41 0 5306 0
vsize: 21388
[startup+660.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4930 0 0 0 65989 19 0 0 25 0 1 0 546954394 22429696 4856 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5476 4856 603 41 0 5435 0
vsize: 21904
[startup+670.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5049 0 0 0 66989 20 0 0 25 0 1 0 546954394 22822912 4975 4294967295 134512640 134672761 3221224544 3221223680 134560634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5572 4975 603 41 0 5531 0
vsize: 22288
[startup+680.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5166 0 0 0 67989 20 0 0 25 0 1 0 546954394 23351296 5092 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5701 5092 603 41 0 5660 0
vsize: 22804
[startup+690.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5196 0 0 0 68989 20 0 0 25 0 1 0 546954394 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+700.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5196 0 0 0 69989 20 0 0 25 0 1 0 546954394 23425024 5122 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5719 5122 603 41 0 5678 0
vsize: 22876
[startup+710.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5196 0 0 0 70989 20 0 0 25 0 1 0 546954394 23425024 5122 4294967295 134512640 134672761 3221224544 3221223712 134560830 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.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5196 0 0 0 71989 20 0 0 25 0 1 0 546954394 23425024 5122 4294967295 134512640 134672761 3221224544 3221223712 134561151 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.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5196 0 0 0 72989 21 0 0 25 0 1 0 546954394 23425024 5122 4294967295 134512640 134672761 3221224544 3221223712 134560871 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.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5196 0 0 0 73989 21 0 0 25 0 1 0 546954394 23425024 5122 4294967295 134512640 134672761 3221224544 3221223680 134560579 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.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5196 0 0 0 74989 21 0 0 25 0 1 0 546954394 23425024 5122 4294967295 134512640 134672761 3221224544 3221223712 134561008 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.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5196 0 0 0 75989 21 0 0 25 0 1 0 546954394 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+770.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5196 0 0 0 76989 21 0 0 25 0 1 0 546954394 23425024 5122 4294967295 134512640 134672761 3221224544 3221223648 134560235 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.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5196 0 0 0 77989 21 0 0 25 0 1 0 546954394 23425024 5122 4294967295 134512640 134672761 3221224544 3221223712 134561382 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.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 78989 21 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+800.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 79989 22 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+810.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 80990 22 0 0 25 0 1 0 546954394 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+820.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 81990 22 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223648 134560034 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.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 82990 22 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223648 134560248 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.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 83990 22 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223648 134560246 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.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 84990 22 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560882 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.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 85990 22 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223648 134559883 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.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 86990 22 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223648 134560196 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.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 87990 22 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223648 134560196 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.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 88991 22 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560825 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.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 89990 22 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560970 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.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 90991 22 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134561385 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.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 91991 22 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134561229 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.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 92991 22 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560833 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.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 93991 22 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560999 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.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 94991 22 0 0 25 0 1 0 546954394 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+960.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 95991 22 0 0 25 0 1 0 546954394 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+970.014 s]
Raw data (loadavg): 1.07 1.00 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 96991 22 0 0 25 0 1 0 546954394 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.015 s]
Raw data (loadavg): 1.06 1.00 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 97992 22 0 0 25 0 1 0 546954394 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.014 s]
Raw data (loadavg): 1.05 1.00 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 98992 22 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134561005 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.01 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 99992 22 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223648 134560370 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.01 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 100992 22 0 0 25 0 1 0 546954394 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+1020.01 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 101992 23 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223648 134559851 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.01 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 102992 23 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223680 134560677 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.01 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 103992 23 0 0 25 0 1 0 546954394 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+1050.01 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5265 0 0 0 104992 23 0 0 25 0 1 0 546954394 23785472 5191 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5807 5191 603 41 0 5766 0
vsize: 23228
[startup+1060.01 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5391 0 0 0 105992 23 0 0 25 0 1 0 546954394 24313856 5317 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5936 5317 603 41 0 5895 0
vsize: 23744
[startup+1070.02 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5507 0 0 0 106992 24 0 0 25 0 1 0 546954394 24752128 5433 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6043 5433 603 41 0 6002 0
vsize: 24172
[startup+1080.02 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5621 0 0 0 107992 24 0 0 25 0 1 0 546954394 25276416 5547 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6171 5547 603 41 0 6130 0
vsize: 24684
[startup+1090.02 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5734 0 0 0 108991 25 0 0 25 0 1 0 546954394 25669632 5660 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6267 5660 603 41 0 6226 0
vsize: 25068
[startup+1100.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5880 0 0 0 109991 25 0 0 25 0 1 0 546954394 26365952 5806 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6437 5806 603 41 0 6396 0
vsize: 25748
[startup+1110.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5996 0 0 0 110991 25 0 0 25 0 1 0 546954394 26763264 5922 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6534 5922 603 41 0 6493 0
vsize: 26136
[startup+1120.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 6108 0 0 0 111991 26 0 0 25 0 1 0 546954394 27299840 6034 4294967295 134512640 134672761 3221224544 3221223700 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6665 6034 603 41 0 6624 0
vsize: 26660
[startup+1130.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 6236 0 0 0 112991 26 0 0 25 0 1 0 546954394 27832320 6162 4294967295 134512640 134672761 3221224544 3221223600 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6795 6162 603 41 0 6754 0
vsize: 27180
[startup+1140.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 5339
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 6360 0 0 0 113990 27 0 0 25 0 1 0 546954394 28233728 6286 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6893 6286 603 41 0 6852 0
vsize: 27572
[startup+1150.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 5340
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 6499 0 0 0 114990 27 0 0 25 0 1 0 546954394 28774400 6425 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7025 6425 603 41 0 6984 0
vsize: 28100
[startup+1160.02 s]
Raw data (loadavg): 1.07 1.02 0.94 2/54 5392
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 6613 0 0 0 115982 35 0 0 25 0 1 0 546954394 29306880 6539 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7155 6539 603 41 0 7114 0
vsize: 28620
[startup+1170.02 s]
Raw data (loadavg): 1.06 1.02 0.94 2/54 5392
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 6718 0 0 0 116982 35 0 0 25 0 1 0 546954394 29679616 6644 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7246 6644 603 41 0 7205 0
vsize: 28984
[startup+1180.02 s]
Raw data (loadavg): 1.05 1.01 0.94 2/54 5392
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 6718 0 0 0 117982 35 0 0 25 0 1 0 546954394 29679616 6644 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7246 6644 603 41 0 7205 0
vsize: 28984
[startup+1190.02 s]
Raw data (loadavg): 1.04 1.01 0.94 2/54 5392
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 6718 0 0 0 118982 35 0 0 25 0 1 0 546954394 29679616 6644 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7246 6644 603 41 0 7205 0
vsize: 28984
[startup+1200.02 s]
Raw data (loadavg): 1.04 1.01 0.94 2/54 5392
Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 6718 0 0 0 119983 35 0 0 25 0 1 0 546954394 29679616 6644 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7246 6644 603 41 0 7205 0
vsize: 28984
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 1.04 1.01 0.94 1/54 5392
Raw data (stat): 5339 (minisat+) Z 5338 26298 26297 0 -1 12 6721 0 0 0 119983 37 0 0 25 0 1 0 546954394 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.03
CPU time (s): 1200.2
CPU user time (s): 1199.83
CPU system time (s): 0.372943
CPU usage (%): 100.014
Max. virtual memory (Kb): 28984
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####