Some explanations

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

General information on the benchmark

Namenormalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-p0548.opb
MD5SUM6f47095f2d417d23ced995954e641689
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 14938
Optimality of the best value was proved NO
Number of terms in the objective function 416
Biggest coefficient in the objective function 11000
Number of bits for the biggest coefficient in the objective function 14
Sum of the numbers in the objective function 96797
Number of bits of the sum of numbers in the objective function 17
Biggest number in a constraint 11000
Number of bits of the biggest number in a constraint 14
Biggest sum of numbers in a constraint 96797
Number of bits of the biggest sum of numbers17
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1236.51
Number of variables548
Total number of constraints724
Number of constraints which are clauses40
Number of constraints which are cardinality constraints (but not clauses)550
Number of constraints which are nor clauses,nor cardinality constraints134
Minimum length of a constraint1
Maximum length of a constraint143

Trace number 22318 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc26 THE 2005-04-22 02:48:20 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12168 boxname=wulflinc26 idbench=936 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6f47095f2d417d23ced995954e641689  /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-p0548.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-p0548.opb /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-p0548.opb
IDLAUNCH: 12168
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
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	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        251168 kB
Buffers:         34448 kB
Cached:         721236 kB
SwapCached:         68 kB
Active:         205696 kB
Inactive:       552852 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        250916 kB
SwapTotal:     2097892 kB
SwapFree:      2097800 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6880 kB
Slab:            19244 kB
Committed_AS:    63724 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-22 03:08:22 (client local time) WITH STATUS 0 IN 1200.2 SECONDS
stats: 12168 7 1200.2 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 156 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ssss.s..ssss........................................
c ---[ 164]---> BDD-cost:   12
c ---[ 163]---> BDD-cost:   46
c ---[ 162]---> BDD-cost:   27
c ---[ 161]---> BDD-cost:    8
c ---[ 160]---> BDD-cost:   48
c ---[ 159]---> BDD-cost:    7
c ---[ 157]---> BDD-cost:   75
c ---[ 156]---> BDD-cost:   23
c ---[ 154]---> BDD-cost:   54
c ---[ 153]---> BDD-cost:    8
c ---[ 152]---> BDD-cost:  105
c ---[ 151]---> BDD-cost:  104
c ---[ 150]---> BDD-cost:  120
c ---[ 149]---> BDD-cost:   79
c ---[ 148]---> BDD-cost:   19
c ---[ 147]---> BDD-cost:  115
c ---[ 146]---> BDD-cost:  107
c ---[ 145]---> BDD-cost:   11
c ---[ 144]---> BDD-cost:   55
c ---[ 143]---> BDD-cost:   87
c ---[ 142]---> BDD-cost:   54
c ---[ 141]---> BDD-cost:  164
c ---[ 140]---> BDD-cost:  151
c ---[ 139]---> BDD-cost:   31
c ---[ 138]---> BDD-cost:   26
c ---[ 136]---> BDD-cost:   28
c ---[ 135]---> BDD-cost:   77
c ---[ 134]---> BDD-cost:  153
c ---[ 133]---> BDD-cost:  109
c ---[ 131]---> BDD-cost:  137
c ---[ 130]---> BDD-cost:    6
c ---[ 129]---> BDD-cost:   56
c ---[ 128]---> BDD-cost:   23
c ---[ 127]---> BDD-cost:    7
c ---[ 126]---> BDD-cost:   32
c ---[ 125]---> BDD-cost:   15
c ---[ 123]---> BDD-cost:   14
c ---[ 121]---> BDD-cost:   10
c ---[ 120]---> BDD-cost:   19
c ---[ 119]---> BDD-cost:   12
c ---[ 118]---> BDD-cost:    9
c ---[ 117]---> BDD-cost:   24
c ---[ 116]---> BDD-cost:   11
c ---[ 115]---> BDD-cost:    9
c ---[ 114]---> BDD-cost:   29
c ---[ 112]---> BDD-cost:    6
c ---[ 111]---> BDD-cost:   21
c ---[ 110]---> BDD-cost:   29
c ---[ 109]---> BDD-cost:   51
c ---[ 107]---> BDD-cost:    8
c ---[ 106]---> BDD-cost:   35
c ---[ 105]---> BDD-cost:   24
c ---[ 104]---> BDD-cost:   12
c ---[ 103]---> BDD-cost:   16
c ---[ 102]---> BDD-cost:   29
c ---[ 101]---> BDD-cost:   13
c ---[ 100]---> BDD-cost:   49
c ---[  99]---> BDD-cost:   60
c ---[  98]---> BDD-cost:    7
c ---[  97]---> BDD-cost:   12
c ---[  96]---> BDD-cost:    9
c ---[  95]---> BDD-cost:   16
c ---[  93]---> BDD-cost:   68
c ---[  92]---> BDD-cost:   78
c ---[  91]---> BDD-cost:   47
c ---[  90]---> BDD-cost:   13
c ---[  89]---> BDD-cost:   68
c ---[  88]---> BDD-cost:    8
c ---[  87]---> BDD-cost:   20
c ---[  86]---> BDD-cost:   18
c ---[  83]---> BDD-cost:   10
c ---[  81]---> BDD-cost:   12
c ---[  80]---> Adder-cost: 750   maxlim: 2650   bits: 13/12
c ---[  79]---> Sorter-cost: 1212     Base: 2 3 2 3
c ---[  78]---> Adder-cost: 171   maxlim: 103   bits: 8/7
c ---[  77]---> Adder-cost: 190   maxlim: 736   bits: 10/10
c ---[  76]---> BDD-cost:   37
c ---[  75]---> BDD-cost:    3
c ---[  73]---> BDD-cost:    3
c ---[  71]---> BDD-cost:    3
c ---[  69]---> BDD-cost:    3
c ---[  67]---> BDD-cost:    3
c ---[  61]---> BDD-cost:    3
c ---[  59]---> BDD-cost:    3
c ---[  57]---> BDD-cost:    3
c ---[  55]---> BDD-cost:    3
c ---[  53]---> BDD-cost:    3
c ---[  47]---> BDD-cost:    3
c ---[  41]---> BDD-cost:    3
c ---[  33]---> BDD-cost:    3
c ---[  31]---> BDD-cost:    3
c ---[  29]---> BDD-cost:    3
c ---[  27]---> BDD-cost:    3
c ---[  25]---> BDD-cost:    3
c ---[  23]---> BDD-cost:    3
c ---[  21]---> BDD-cost:    3
c ---[  19]---> BDD-cost:    3
c ---[  17]---> BDD-cost:    3
c ---[  15]---> BDD-cost:    3
c ---[  13]---> BDD-cost:   49
c ---[  12]---> BDD-cost:   49
c ---[  11]---> BDD-cost:   26
c ---[  10]---> BDD-cost:    5
c ---[   9]---> BDD-cost:    7
c ---[   8]---> BDD-cost:    9
c ---[   7]---> BDD-cost:   11
c ---[   6]---> BDD-cost:    5
c ---[   5]---> BDD-cost:   20
c ---[   4]---> BDD-cost:    4
c ---[   3]---> BDD-cost:    2
c ---[   2]---> BDD-cost:    9
c ---[   1]---> BDD-cost:    2
c ---[   0]---> BDD-cost:    2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   24239    72664 |    8079       0        0     nan |  0.000 % |
c |       100 |   24204    72543 |    8886      94      630     6.7 |  2.627 % |
c |       250 |   24204    72543 |    9775     244     1500     6.1 |  2.627 % |
c |       475 |   24168    72424 |   10753     463     3762     8.1 |  2.700 % |
c |       812 |   24147    72351 |   11828     793     6573     8.3 |  2.736 % |
c |      1318 |   24094    72172 |   13011    1287    11505     8.9 |  2.845 % |
c |      2077 |   24070    72093 |   14312    2044    36065    17.6 |  2.881 % |
c |      3216 |   24070    72093 |   15743    3183    66248    20.8 |  2.881 % |
c |      4924 |   24070    72093 |   17318    4891   129432    26.5 |  2.881 % |
c |      7486 |   24046    72024 |   19049    7452   225412    30.2 |  2.917 % |
c |     11330 |   24030    71968 |   20954   11293   381242    33.8 |  2.953 % |
c |     17096 |   24024    71948 |   23050   17058   532868    31.2 |  2.972 % |
c |     25746 |   24024    71948 |   25355   13467   596053    44.3 |  2.972 % |
c |     38720 |   24024    71948 |   27890   13378   350688    26.2 |  2.972 % |
c |     58184 |   24024    71948 |   30679   17530   691331    39.4 |  2.972 % |
c |     87376 |   24024    71948 |   33747   27765   906272    32.6 |  2.972 % |
c |    131165 |   24016    71928 |   37122   30146  1168742    38.8 |  3.008 % |
c |    196849 |   24016    71928 |   40835   26633   994072    37.3 |  3.008 % |
c |    295375 |   24016    71928 |   44918   22515   781186    34.7 |  3.008 % |
c |    443166 |   23998    71874 |   49410   21696   804926    37.1 |  3.080 % |
c |    664849 |   23994    71864 |   54351   37767  1328360    35.2 |  3.099 % |
#### 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.65 0.86 0.88 2/54 16014
Raw data (stat): 16014 (runsolver) R 16013 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 550246179 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.001 s]
Raw data (loadavg): 0.71 0.86 0.88 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 1816 0 0 0 995 3 0 0 25 0 1 0 550246179 9052160 1783 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2210 1783 603 41 0 2169 0
vsize: 8840
[startup+20.0017 s]
Raw data (loadavg): 0.75 0.87 0.88 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 2098 0 0 0 1994 5 0 0 25 0 1 0 550246179 10248192 2065 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2502 2065 603 41 0 2461 0
vsize: 10008
[startup+30.002 s]
Raw data (loadavg): 0.79 0.87 0.88 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 2183 0 0 0 2994 5 0 0 25 0 1 0 550246179 10514432 2150 4294967295 134512640 134672761 3221224544 3221223728 134558648 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2567 2150 603 41 0 2526 0
vsize: 10268
[startup+40.0031 s]
Raw data (loadavg): 0.82 0.87 0.88 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 2301 0 0 0 3993 6 0 0 25 0 1 0 550246179 11051008 2268 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2698 2268 603 41 0 2657 0
vsize: 10792
[startup+50.0038 s]
Raw data (loadavg): 0.85 0.88 0.88 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 2493 0 0 0 4993 6 0 0 25 0 1 0 550246179 11849728 2460 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2893 2460 603 41 0 2852 0
vsize: 11572
[startup+60.004 s]
Raw data (loadavg): 0.87 0.88 0.88 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 2503 0 0 0 5993 7 0 0 25 0 1 0 550246179 11849728 2470 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2893 2470 603 41 0 2852 0
vsize: 11572
[startup+70.0052 s]
Raw data (loadavg): 0.89 0.89 0.88 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 2521 0 0 0 6992 7 0 0 25 0 1 0 550246179 11997184 2488 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2929 2488 603 41 0 2888 0
vsize: 11716
[startup+80.0058 s]
Raw data (loadavg): 0.91 0.89 0.88 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 2613 0 0 0 7992 8 0 0 25 0 1 0 550246179 12529664 2580 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3059 2580 603 41 0 3018 0
vsize: 12236
[startup+90.0061 s]
Raw data (loadavg): 0.92 0.89 0.89 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 2640 0 0 0 8992 8 0 0 25 0 1 0 550246179 12664832 2607 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3092 2607 603 41 0 3051 0
vsize: 12368
[startup+100.006 s]
Raw data (loadavg): 0.93 0.89 0.89 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 2701 0 0 0 9991 9 0 0 25 0 1 0 550246179 12943360 2668 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3160 2668 603 41 0 3119 0
vsize: 12640
[startup+110.007 s]
Raw data (loadavg): 0.94 0.90 0.89 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 2850 0 0 0 10991 9 0 0 25 0 1 0 550246179 13484032 2817 4294967295 134512640 134672761 3221224544 3221223712 134561003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3292 2817 603 41 0 3251 0
vsize: 13168
[startup+120.007 s]
Raw data (loadavg): 0.95 0.90 0.89 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 3064 0 0 0 11990 10 0 0 25 0 1 0 550246179 14438400 3031 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3525 3031 603 41 0 3484 0
vsize: 14100
[startup+130.007 s]
Raw data (loadavg): 0.96 0.90 0.89 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 3064 0 0 0 12990 10 0 0 25 0 1 0 550246179 14438400 3031 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3525 3031 603 41 0 3484 0
vsize: 14100
[startup+140.008 s]
Raw data (loadavg): 0.96 0.91 0.89 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 3076 0 0 0 13990 10 0 0 25 0 1 0 550246179 14438400 3043 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3525 3043 603 41 0 3484 0
vsize: 14100
[startup+150.008 s]
Raw data (loadavg): 0.97 0.91 0.89 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 3076 0 0 0 14990 10 0 0 25 0 1 0 550246179 14438400 3043 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3525 3043 603 41 0 3484 0
vsize: 14100
[startup+160.009 s]
Raw data (loadavg): 0.97 0.91 0.89 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 3077 0 0 0 15990 11 0 0 25 0 1 0 550246179 14438400 3044 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3525 3044 603 41 0 3484 0
vsize: 14100
[startup+170.01 s]
Raw data (loadavg): 0.98 0.91 0.89 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 3083 0 0 0 16990 11 0 0 25 0 1 0 550246179 14438400 3050 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3525 3050 603 41 0 3484 0
vsize: 14100
[startup+180.01 s]
Raw data (loadavg): 0.98 0.92 0.89 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 3122 0 0 0 17990 11 0 0 25 0 1 0 550246179 14716928 3089 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3593 3089 603 41 0 3552 0
vsize: 14372
[startup+190.01 s]
Raw data (loadavg): 0.98 0.92 0.90 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 3146 0 0 0 18990 12 0 0 25 0 1 0 550246179 14716928 3113 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3593 3113 603 41 0 3552 0
vsize: 14372
[startup+200.009 s]
Raw data (loadavg): 0.98 0.92 0.90 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 3167 0 0 0 19990 12 0 0 25 0 1 0 550246179 14876672 3134 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3632 3134 603 41 0 3591 0
vsize: 14528
[startup+210.011 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 3268 0 0 0 20989 12 0 0 25 0 1 0 550246179 15273984 3235 4294967295 134512640 134672761 3221224544 3221223648 134554677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3729 3235 603 41 0 3688 0
vsize: 14916
[startup+220.011 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 3283 0 0 0 21989 12 0 0 25 0 1 0 550246179 15421440 3250 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3765 3250 603 41 0 3724 0
vsize: 15060
[startup+230.011 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 3288 0 0 0 22990 13 0 0 25 0 1 0 550246179 15421440 3255 4294967295 134512640 134672761 3221224544 3221223680 134560654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3765 3255 603 41 0 3724 0
vsize: 15060
[startup+240.011 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 3304 0 0 0 23990 13 0 0 25 0 1 0 550246179 15421440 3271 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3765 3271 603 41 0 3724 0
vsize: 15060
[startup+250.011 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 3312 0 0 0 24990 13 0 0 25 0 1 0 550246179 15585280 3279 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3805 3279 603 41 0 3764 0
vsize: 15220
[startup+260.012 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 3322 0 0 0 25990 13 0 0 25 0 1 0 550246179 15585280 3289 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3805 3289 603 41 0 3764 0
vsize: 15220
[startup+270.012 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 3338 0 0 0 26990 13 0 0 25 0 1 0 550246179 15749120 3305 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3845 3305 603 41 0 3804 0
vsize: 15380
[startup+280.011 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 3352 0 0 0 27990 13 0 0 25 0 1 0 550246179 15749120 3319 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3845 3319 603 41 0 3804 0
vsize: 15380
[startup+290.012 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 3366 0 0 0 28990 13 0 0 25 0 1 0 550246179 15912960 3333 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3885 3333 603 41 0 3844 0
vsize: 15540
[startup+300.012 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 3367 0 0 0 29990 13 0 0 25 0 1 0 550246179 15912960 3334 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3885 3334 603 41 0 3844 0
vsize: 15540
[startup+310.012 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 3367 0 0 0 30991 13 0 0 25 0 1 0 550246179 15912960 3334 4294967295 134512640 134672761 3221224544 3221223712 134561136 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3885 3334 603 41 0 3844 0
vsize: 15540
[startup+320.013 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 3368 0 0 0 31991 13 0 0 25 0 1 0 550246179 15912960 3335 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3885 3335 603 41 0 3844 0
vsize: 15540
[startup+330.013 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 3368 0 0 0 32991 13 0 0 25 0 1 0 550246179 15912960 3335 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3885 3335 603 41 0 3844 0
vsize: 15540
[startup+340.013 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 3382 0 0 0 33991 13 0 0 25 0 1 0 550246179 15912960 3349 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3885 3349 603 41 0 3844 0
vsize: 15540
[startup+350.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 3466 0 0 0 34990 14 0 0 25 0 1 0 550246179 16347136 3433 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3991 3433 603 41 0 3950 0
vsize: 15964
[startup+360.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 3618 0 0 0 35990 15 0 0 25 0 1 0 550246179 16883712 3585 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4122 3585 603 41 0 4081 0
vsize: 16488
[startup+370.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 3631 0 0 0 36990 15 0 0 25 0 1 0 550246179 17018880 3598 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4155 3598 603 41 0 4114 0
vsize: 16620
[startup+380.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 3644 0 0 0 37990 15 0 0 25 0 1 0 550246179 17018880 3611 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4155 3611 603 41 0 4114 0
vsize: 16620
[startup+390.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 3678 0 0 0 38990 15 0 0 25 0 1 0 550246179 17182720 3645 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4195 3645 603 41 0 4154 0
vsize: 16780
[startup+400.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 3698 0 0 0 39990 15 0 0 25 0 1 0 550246179 17346560 3665 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4235 3665 603 41 0 4194 0
vsize: 16940
[startup+410.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 3742 0 0 0 40990 15 0 0 25 0 1 0 550246179 17477632 3709 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4267 3709 603 41 0 4226 0
vsize: 17068
[startup+420.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 3742 0 0 0 41990 16 0 0 25 0 1 0 550246179 17477632 3709 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4267 3709 603 41 0 4226 0
vsize: 17068
[startup+430.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 3763 0 0 0 42990 16 0 0 25 0 1 0 550246179 17620992 3730 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4302 3730 603 41 0 4261 0
vsize: 17208
[startup+440.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 3806 0 0 0 43990 16 0 0 25 0 1 0 550246179 17752064 3773 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4334 3773 603 41 0 4293 0
vsize: 17336
[startup+450.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 3809 0 0 0 44990 16 0 0 25 0 1 0 550246179 17752064 3776 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4334 3776 603 41 0 4293 0
vsize: 17336
[startup+460.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 3825 0 0 0 45990 16 0 0 25 0 1 0 550246179 17899520 3792 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4370 3792 603 41 0 4329 0
vsize: 17480
[startup+470.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 3844 0 0 0 46991 16 0 0 25 0 1 0 550246179 17899520 3811 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4370 3811 603 41 0 4329 0
vsize: 17480
[startup+480.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4122 0 0 0 47990 17 0 0 25 0 1 0 550246179 19095552 4089 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4662 4089 603 41 0 4621 0
vsize: 18648
[startup+490.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4212 0 0 0 48989 18 0 0 25 0 1 0 550246179 19492864 4179 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4759 4179 603 41 0 4718 0
vsize: 19036
[startup+500.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4212 0 0 0 49990 18 0 0 25 0 1 0 550246179 19492864 4179 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4759 4179 603 41 0 4718 0
vsize: 19036
[startup+510.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4212 0 0 0 50990 18 0 0 25 0 1 0 550246179 19492864 4179 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4759 4179 603 41 0 4718 0
vsize: 19036
[startup+520.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4255 0 0 0 51990 18 0 0 25 0 1 0 550246179 19648512 4222 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4797 4222 603 41 0 4756 0
vsize: 19188
[startup+530.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4259 0 0 0 52990 18 0 0 25 0 1 0 550246179 19648512 4226 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4797 4226 603 41 0 4756 0
vsize: 19188
[startup+540.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4350 0 0 0 53990 18 0 0 25 0 1 0 550246179 20062208 4317 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4898 4317 603 41 0 4857 0
vsize: 19592
[startup+550.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4350 0 0 0 54989 19 0 0 25 0 1 0 550246179 20062208 4317 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4898 4317 603 41 0 4857 0
vsize: 19592
[startup+560.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4362 0 0 0 55988 19 0 0 25 0 1 0 550246179 20213760 4329 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4935 4329 603 41 0 4894 0
vsize: 19740
[startup+570.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4392 0 0 0 56988 19 0 0 25 0 1 0 550246179 20377600 4359 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4975 4359 603 41 0 4934 0
vsize: 19900
[startup+580.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4409 0 0 0 57988 20 0 0 25 0 1 0 550246179 20377600 4376 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4975 4376 603 41 0 4934 0
vsize: 19900
[startup+590.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4409 0 0 0 58988 20 0 0 25 0 1 0 550246179 20377600 4376 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4975 4376 603 41 0 4934 0
vsize: 19900
[startup+600.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4435 0 0 0 59988 20 0 0 25 0 1 0 550246179 20541440 4402 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5015 4402 603 41 0 4974 0
vsize: 20060
[startup+610.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4450 0 0 0 60987 21 0 0 25 0 1 0 550246179 20541440 4417 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5015 4417 603 41 0 4974 0
vsize: 20060
[startup+620.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4487 0 0 0 61987 21 0 0 25 0 1 0 550246179 20738048 4454 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5063 4454 603 41 0 5022 0
vsize: 20252
[startup+630.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4521 0 0 0 62987 22 0 0 25 0 1 0 550246179 20934656 4488 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5111 4488 603 41 0 5070 0
vsize: 20444
[startup+640.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4521 0 0 0 63987 22 0 0 25 0 1 0 550246179 20934656 4488 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5111 4488 603 41 0 5070 0
vsize: 20444
[startup+650.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4521 0 0 0 64986 22 0 0 25 0 1 0 550246179 20934656 4488 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5111 4488 603 41 0 5070 0
vsize: 20444
[startup+660.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4521 0 0 0 65986 22 0 0 25 0 1 0 550246179 20934656 4488 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5111 4488 603 41 0 5070 0
vsize: 20444
[startup+670.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4534 0 0 0 66986 23 0 0 25 0 1 0 550246179 20934656 4501 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5111 4501 603 41 0 5070 0
vsize: 20444
[startup+680.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4534 0 0 0 67986 23 0 0 25 0 1 0 550246179 20934656 4501 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5111 4501 603 41 0 5070 0
vsize: 20444
[startup+690.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4534 0 0 0 68986 23 0 0 25 0 1 0 550246179 20934656 4501 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5111 4501 603 41 0 5070 0
vsize: 20444
[startup+700.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16014
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4534 0 0 0 69986 24 0 0 25 0 1 0 550246179 20934656 4501 4294967295 134512640 134672761 3221224544 3221223712 134561148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5111 4501 603 41 0 5070 0
vsize: 20444
[startup+710.02 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 16067
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4628 0 0 0 70980 28 0 0 25 0 1 0 550246179 21352448 4595 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5213 4595 603 41 0 5172 0
vsize: 20852
[startup+720.021 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 16067
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4644 0 0 0 71981 28 0 0 25 0 1 0 550246179 21516288 4611 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5253 4611 603 41 0 5212 0
vsize: 21012
[startup+730.021 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 16067
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4677 0 0 0 72981 28 0 0 25 0 1 0 550246179 21680128 4644 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5293 4644 603 41 0 5252 0
vsize: 21172
[startup+740.021 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 16067
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4681 0 0 0 73981 28 0 0 25 0 1 0 550246179 21680128 4648 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5293 4648 603 41 0 5252 0
vsize: 21172
[startup+750.022 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 16067
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4702 0 0 0 74981 28 0 0 25 0 1 0 550246179 21872640 4669 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5340 4669 603 41 0 5299 0
vsize: 21360
[startup+760.021 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 16067
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4704 0 0 0 75981 28 0 0 25 0 1 0 550246179 21872640 4671 4294967295 134512640 134672761 3221224544 3221223648 134554671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5340 4671 603 41 0 5299 0
vsize: 21360
[startup+770.021 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 16069
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4704 0 0 0 76981 28 0 0 25 0 1 0 550246179 21872640 4671 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5340 4671 603 41 0 5299 0
vsize: 21360
[startup+780.021 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 16069
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4704 0 0 0 77981 28 0 0 25 0 1 0 550246179 21872640 4671 4294967295 134512640 134672761 3221224544 3221223712 134561115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5340 4671 603 41 0 5299 0
vsize: 21360
[startup+790.021 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 16069
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4711 0 0 0 78981 28 0 0 25 0 1 0 550246179 21872640 4678 4294967295 134512640 134672761 3221224544 3221223728 134559332 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5340 4678 603 41 0 5299 0
vsize: 21360
[startup+800.021 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 16069
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4712 0 0 0 79981 29 0 0 25 0 1 0 550246179 21872640 4679 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5340 4679 603 41 0 5299 0
vsize: 21360
[startup+810.021 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 16069
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4712 0 0 0 80982 29 0 0 25 0 1 0 550246179 21872640 4679 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5340 4679 603 41 0 5299 0
vsize: 21360
[startup+820.021 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 16069
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4723 0 0 0 81982 29 0 0 25 0 1 0 550246179 21872640 4690 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5340 4690 603 41 0 5299 0
vsize: 21360
[startup+830.021 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 16069
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4724 0 0 0 82982 29 0 0 25 0 1 0 550246179 21872640 4691 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5340 4691 603 41 0 5299 0
vsize: 21360
[startup+840.022 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 16069
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4725 0 0 0 83982 29 0 0 25 0 1 0 550246179 21872640 4692 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5340 4692 603 41 0 5299 0
vsize: 21360
[startup+850.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16069
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4735 0 0 0 84982 29 0 0 25 0 1 0 550246179 22036480 4702 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5380 4702 603 41 0 5339 0
vsize: 21520
[startup+860.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16069
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4736 0 0 0 85982 29 0 0 25 0 1 0 550246179 22036480 4703 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5380 4703 603 41 0 5339 0
vsize: 21520
[startup+870.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16069
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4738 0 0 0 86982 29 0 0 25 0 1 0 550246179 22036480 4705 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5380 4705 603 41 0 5339 0
vsize: 21520
[startup+880.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16069
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4909 0 0 0 87981 30 0 0 25 0 1 0 550246179 22704128 4876 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5543 4876 603 41 0 5502 0
vsize: 22172
[startup+890.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16069
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4909 0 0 0 88982 30 0 0 25 0 1 0 550246179 22704128 4876 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5543 4876 603 41 0 5502 0
vsize: 22172
[startup+900.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16069
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4909 0 0 0 89982 30 0 0 25 0 1 0 550246179 22704128 4876 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5543 4876 603 41 0 5502 0
vsize: 22172
[startup+910.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16069
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4909 0 0 0 90982 30 0 0 25 0 1 0 550246179 22704128 4876 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5543 4876 603 41 0 5502 0
vsize: 22172
[startup+920.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16069
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 4965 0 0 0 91982 30 0 0 25 0 1 0 550246179 22835200 4932 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5575 4932 603 41 0 5534 0
vsize: 22300
[startup+930.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16069
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 5290 0 0 0 92981 31 0 0 25 0 1 0 550246179 24174592 5257 4294967295 134512640 134672761 3221224544 3221223668 134556395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5902 5257 603 41 0 5861 0
vsize: 23608
[startup+940.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16069
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 5290 0 0 0 93981 31 0 0 25 0 1 0 550246179 24174592 5257 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5902 5257 603 41 0 5861 0
vsize: 23608
[startup+950.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16069
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 5290 0 0 0 94981 31 0 0 25 0 1 0 550246179 24174592 5257 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5902 5257 603 41 0 5861 0
vsize: 23608
[startup+960.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16069
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 5290 0 0 0 95981 31 0 0 25 0 1 0 550246179 24174592 5257 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5902 5257 603 41 0 5861 0
vsize: 23608
[startup+970.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16069
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 5290 0 0 0 96981 31 0 0 25 0 1 0 550246179 24174592 5257 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5902 5257 603 41 0 5861 0
vsize: 23608
[startup+980.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16069
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 5609 0 0 0 97980 33 0 0 25 0 1 0 550246179 25513984 5576 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6229 5576 603 41 0 6188 0
vsize: 24916
[startup+990.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16069
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 5897 0 0 0 98980 33 0 0 25 0 1 0 550246179 26730496 5864 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6526 5864 603 41 0 6485 0
vsize: 26104
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16069
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 5964 0 0 0 99980 34 0 0 25 0 1 0 550246179 27004928 5931 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6593 5931 603 41 0 6552 0
vsize: 26372
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16069
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 5970 0 0 0 100980 34 0 0 25 0 1 0 550246179 27004928 5937 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6593 5937 603 41 0 6552 0
vsize: 26372
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16069
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 5970 0 0 0 101980 34 0 0 25 0 1 0 550246179 27004928 5937 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6593 5937 603 41 0 6552 0
vsize: 26372
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16069
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 5981 0 0 0 102980 34 0 0 25 0 1 0 550246179 27148288 5948 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6628 5948 603 41 0 6587 0
vsize: 26512
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16071
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 5984 0 0 0 103980 34 0 0 25 0 1 0 550246179 27148288 5951 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6628 5951 603 41 0 6587 0
vsize: 26512
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16071
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 5991 0 0 0 104980 34 0 0 25 0 1 0 550246179 27148288 5958 4294967295 134512640 134672761 3221224544 3221223712 134561121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6628 5958 603 41 0 6587 0
vsize: 26512
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16071
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 5991 0 0 0 105980 34 0 0 25 0 1 0 550246179 27148288 5958 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6628 5958 603 41 0 6587 0
vsize: 26512
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16071
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 6000 0 0 0 106981 34 0 0 25 0 1 0 550246179 27148288 5967 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6628 5967 603 41 0 6587 0
vsize: 26512
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16071
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 6001 0 0 0 107981 34 0 0 25 0 1 0 550246179 27148288 5968 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6628 5968 603 41 0 6587 0
vsize: 26512
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16071
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 6001 0 0 0 108981 34 0 0 25 0 1 0 550246179 27148288 5968 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6628 5968 603 41 0 6587 0
vsize: 26512
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16071
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 6011 0 0 0 109981 34 0 0 25 0 1 0 550246179 27344896 5978 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 5978 603 41 0 6635 0
vsize: 26704
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16071
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 6012 0 0 0 110981 34 0 0 25 0 1 0 550246179 27344896 5979 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 5979 603 41 0 6635 0
vsize: 26704
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16071
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 6012 0 0 0 111981 34 0 0 25 0 1 0 550246179 27344896 5979 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 5979 603 41 0 6635 0
vsize: 26704
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16071
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 6012 0 0 0 112981 34 0 0 25 0 1 0 550246179 27344896 5979 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 5979 603 41 0 6635 0
vsize: 26704
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16071
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 6012 0 0 0 113981 35 0 0 25 0 1 0 550246179 27344896 5979 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 5979 603 41 0 6635 0
vsize: 26704
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16071
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 6012 0 0 0 114982 35 0 0 25 0 1 0 550246179 27344896 5979 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 5979 603 41 0 6635 0
vsize: 26704
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16071
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 6021 0 0 0 115982 35 0 0 25 0 1 0 550246179 27344896 5988 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 5988 603 41 0 6635 0
vsize: 26704
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16071
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 6022 0 0 0 116982 35 0 0 25 0 1 0 550246179 27344896 5989 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 5989 603 41 0 6635 0
vsize: 26704
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16071
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 6022 0 0 0 117982 35 0 0 25 0 1 0 550246179 27344896 5989 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 5989 603 41 0 6635 0
vsize: 26704
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16071
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 6023 0 0 0 118982 35 0 0 25 0 1 0 550246179 27344896 5990 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 5990 603 41 0 6635 0
vsize: 26704
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16071
Raw data (stat): 16014 (minisat+) R 16013 22612 22611 0 -1 0 6024 0 0 0 119982 35 0 0 25 0 1 0 550246179 27344896 5991 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 5991 603 41 0 6635 0
vsize: 26704
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 16071
Raw data (stat): 16014 (minisat+) Z 16013 22612 22611 0 -1 12 6026 0 0 0 119982 36 0 0 25 0 1 0 550246179 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: 0
Real time (s): 1200.04
CPU time (s): 1200.2
CPU user time (s): 1199.83
CPU system time (s): 0.366944
CPU usage (%): 100.013
Max. virtual memory (Kb): 26704
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####