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).
    Note that some very long lines in this section may be truncated by your web browser !
  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

Namemps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-p0548.opb
MD5SUM6f47095f2d417d23ced995954e641689
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 18719
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 benchmark1195.07
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 6103

Launcher Data

LAUNCH ON wulflinc22 THE 2005-09-20 03:20:05 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3261 boxname=wulflinc22 idbench=917 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6f47095f2d417d23ced995954e641689  /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-p0548.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-p0548.opb
IDLAUNCH: 3261
/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:        899432 kB
Buffers:          5460 kB
Cached:         103196 kB
SwapCached:        484 kB
Active:          14912 kB
Inactive:        96204 kB
HighTotal:      131008 kB
HighFree:        24248 kB
LowTotal:       903652 kB
LowFree:        875184 kB
SwapTotal:     2097892 kB
SwapFree:      2096748 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5676 kB
Slab:            18364 kB
Committed_AS:    64132 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 03:40:15 (client local time) WITH STATUS 0 IN 1209.88 SECONDS
stats: 3261 7 1209.88 0

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 |   19073    57623 |    6357       0        0     nan |  0.000 % |
c |       100 |   19073    57623 |    6992     100      672     6.7 |  2.555 % |
c |       252 |   19057    57569 |    7691     247     1692     6.9 |  2.591 % |
c |       477 |   19057    57569 |    8461     472     5450    11.5 |  2.591 % |
c |       815 |   19057    57569 |    9307     810    10043    12.4 |  2.591 % |
c |      1321 |   19042    57516 |   10238    1311    18125    13.8 |  2.609 % |
c |      2080 |   19012    57412 |   11261    2062    40134    19.5 |  2.664 % |
c |      3220 |   19012    57412 |   12387    3202    69123    21.6 |  2.664 % |
c |      4929 |   18949    57203 |   13626    4904   116688    23.8 |  2.772 % |
c |      7491 |   18925    57134 |   14989    7465   185728    24.9 |  2.808 % |
c |     11337 |   18925    57134 |   16488   11311   347696    30.7 |  2.809 % |
c |     17104 |   18925    57134 |   18137    8643   242756    28.1 |  2.808 % |
c |     25753 |   18925    57134 |   19950   17292   503434    29.1 |  2.808 % |
c |     38727 |   18925    57134 |   21946   20110   621158    30.9 |  2.808 % |
c |     58188 |   18885    57000 |   24140   16745   543948    32.5 |  2.917 % |
c |     87380 |   18885    57000 |   26554   20873   764650    36.6 |  2.917 % |
c |    131169 |   18869    56944 |   29210   23294   693331    29.8 |  2.953 % |
c |    196854 |   18869    56944 |   32131   25433  1047150    41.2 |  2.953 % |
c |    295382 |   18869    56944 |   35344   17901   689696    38.5 |  2.954 % |
c |    443173 |   18869    56944 |   38878   17949   602270    33.6 |  2.953 % |
c |    664857 |   18869    56944 |   42766   27238  1062812    39.0 |  2.953 % |

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/15927/stat): 15927 (minisat+_script) R 15926 15927 21452 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1855248457 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/15927/statm): 174 3 169 147 0 27 0
[pid=15927] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libtermcap.so.2
open syscall for file tls/i686/libtermcap.so.2
open syscall for file tls/mmx/libtermcap.so.2
open syscall for file tls/libtermcap.so.2
open syscall for file i686/mmx/libtermcap.so.2
open syscall for file i686/libtermcap.so.2
open syscall for file mmx/libtermcap.so.2
open syscall for file libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/libtermcap.so.2
open syscall for file /etc/ld.so.cache
open syscall for file /lib/libtermcap.so.2
open syscall for file tls/i686/mmx/libdl.so.2
open syscall for file tls/i686/libdl.so.2
open syscall for file tls/mmx/libdl.so.2
open syscall for file tls/libdl.so.2
open syscall for file i686/mmx/libdl.so.2
open syscall for file i686/libdl.so.2
open syscall for file mmx/libdl.so.2
open syscall for file libdl.so.2
open syscall for file /oldhome/oroussel/lib/libdl.so.2
open syscall for file /lib/libdl.so.2
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /lib/tls/libc.so.6
open syscall for file /dev/tty
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
New process pid=15928
New process pid=15929
New process pid=15930
execve syscall for /bin/sed executable
One traced child (pid=15929) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=15930) exited with status: 0
One traced child (pid=15928) exited with status: 0
New process pid=15931
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-p0548.opb

[startup+10.003 s]
Raw data (loadavg): 0.93 0.95 0.90 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 1420 0 0 0 976 10 0 0 25 0 1 0 1855248462 6131712 1362 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15931/statm): 1497 1362 145 145 0 1352 0
[pid=15931] vsize: 5988
Current children cumulated CPU time (s) 9.87
Current children cumulated vsize (Kb) 8112

[startup+20.0051 s]
Raw data (loadavg): 0.94 0.96 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 1577 0 0 0 1973 12 0 0 25 0 1 0 1855248462 6770688 1519 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15931/statm): 1653 1519 145 145 0 1508 0
[pid=15931] vsize: 6612
Current children cumulated CPU time (s) 19.86
Current children cumulated vsize (Kb) 8736

[startup+30.007 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 1772 0 0 0 2969 13 0 0 25 0 1 0 1855248462 7569408 1714 4294967295 134512640 135094434 3221224432 3221223104 134555612 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15931/statm): 1848 1714 145 145 0 1703 0
[pid=15931] vsize: 7392
Current children cumulated CPU time (s) 29.83
Current children cumulated vsize (Kb) 9516

[startup+40.0072 s]
Raw data (loadavg): 1.04 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 2020 0 0 0 3964 16 0 0 25 0 1 0 1855248462 8585216 1962 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15931/statm): 2096 1962 145 145 0 1951 0
[pid=15931] vsize: 8384
Current children cumulated CPU time (s) 39.81
Current children cumulated vsize (Kb) 10508

[startup+50.0089 s]
Raw data (loadavg): 1.03 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 2201 0 0 0 4960 17 0 0 25 0 1 0 1855248462 9326592 2143 4294967295 134512640 135094434 3221224432 3221223104 134556493 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15931/statm): 2277 2143 145 145 0 2132 0
[pid=15931] vsize: 9108
Current children cumulated CPU time (s) 49.78
Current children cumulated vsize (Kb) 11232

[startup+60.0096 s]
Raw data (loadavg): 1.03 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 2240 0 0 0 5960 18 0 0 25 0 1 0 1855248462 9523200 2182 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15931/statm): 2325 2182 145 145 0 2180 0
[pid=15931] vsize: 9300
Current children cumulated CPU time (s) 59.79
Current children cumulated vsize (Kb) 11424

[startup+70.0113 s]
Raw data (loadavg): 1.02 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 2252 0 0 0 6959 19 0 0 25 0 1 0 1855248462 9572352 2194 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15931/statm): 2337 2194 145 145 0 2192 0
[pid=15931] vsize: 9348
Current children cumulated CPU time (s) 69.79
Current children cumulated vsize (Kb) 11472

[startup+80.013 s]
Raw data (loadavg): 1.02 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 2280 0 0 0 7958 19 0 0 25 0 1 0 1855248462 9719808 2222 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15931/statm): 2373 2222 145 145 0 2228 0
[pid=15931] vsize: 9492
Current children cumulated CPU time (s) 79.78
Current children cumulated vsize (Kb) 11616

[startup+90.0137 s]
Raw data (loadavg): 1.02 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 2285 0 0 0 8958 20 0 0 25 0 1 0 1855248462 9736192 2227 4294967295 134512640 135094434 3221224432 3221223024 134551428 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15931/statm): 2377 2227 145 145 0 2232 0
[pid=15931] vsize: 9508
Current children cumulated CPU time (s) 89.79
Current children cumulated vsize (Kb) 11632

[startup+100.014 s]
Raw data (loadavg): 1.01 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 2303 0 0 0 9957 20 0 0 25 0 1 0 1855248462 9818112 2245 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15931/statm): 2397 2245 145 145 0 2252 0
[pid=15931] vsize: 9588
Current children cumulated CPU time (s) 99.78
Current children cumulated vsize (Kb) 11712

[startup+110.015 s]
Raw data (loadavg): 1.01 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 2326 0 0 0 10957 21 0 0 25 0 1 0 1855248462 9895936 2268 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15931/statm): 2416 2268 145 145 0 2271 0
[pid=15931] vsize: 9664
Current children cumulated CPU time (s) 109.79
Current children cumulated vsize (Kb) 11788

[startup+120.017 s]
Raw data (loadavg): 1.01 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 2371 0 0 0 11955 22 0 0 25 0 1 0 1855248462 10084352 2313 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15931/statm): 2462 2313 145 145 0 2317 0
[pid=15931] vsize: 9848
Current children cumulated CPU time (s) 119.78
Current children cumulated vsize (Kb) 11972

[startup+130.018 s]
Raw data (loadavg): 1.01 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 2410 0 0 0 12954 22 0 0 25 0 1 0 1855248462 10244096 2352 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15931/statm): 2501 2352 145 145 0 2356 0
[pid=15931] vsize: 10004
Current children cumulated CPU time (s) 129.77
Current children cumulated vsize (Kb) 12128

[startup+140.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 2538 0 0 0 13951 24 0 0 25 0 1 0 1855248462 10780672 2480 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15931/statm): 2632 2480 145 145 0 2487 0
[pid=15931] vsize: 10528
Current children cumulated CPU time (s) 139.76
Current children cumulated vsize (Kb) 12652

[startup+150.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 2552 0 0 0 14951 24 0 0 25 0 1 0 1855248462 10838016 2494 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15931/statm): 2646 2494 145 145 0 2501 0
[pid=15931] vsize: 10584
Current children cumulated CPU time (s) 149.76
Current children cumulated vsize (Kb) 12708

[startup+160.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 2731 0 0 0 15947 26 0 0 25 0 1 0 1855248462 11608064 2673 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15931/statm): 2834 2673 145 145 0 2689 0
[pid=15931] vsize: 11336
Current children cumulated CPU time (s) 159.74
Current children cumulated vsize (Kb) 13460

[startup+170.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 2741 0 0 0 16947 26 0 0 25 0 1 0 1855248462 11673600 2683 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15931/statm): 2850 2683 145 145 0 2705 0
[pid=15931] vsize: 11400
Current children cumulated CPU time (s) 169.74
Current children cumulated vsize (Kb) 13524

[startup+180.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 2853 0 0 0 17945 27 0 0 25 0 1 0 1855248462 12259328 2795 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15931/statm): 2993 2795 145 145 0 2848 0
[pid=15931] vsize: 11972
Current children cumulated CPU time (s) 179.73
Current children cumulated vsize (Kb) 14096

[startup+190.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 2870 0 0 0 18944 28 0 0 25 0 1 0 1855248462 12341248 2812 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15931/statm): 3013 2812 145 145 0 2868 0
[pid=15931] vsize: 12052
Current children cumulated CPU time (s) 189.73
Current children cumulated vsize (Kb) 14176

[startup+200.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 2877 0 0 0 19944 28 0 0 25 0 1 0 1855248462 12374016 2819 4294967295 134512640 135094434 3221224432 3221223024 134551457 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3021 2819 145 145 0 2876 0
[pid=15931] vsize: 12084
Current children cumulated CPU time (s) 199.73
Current children cumulated vsize (Kb) 14208

[startup+210.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 2883 0 0 0 20944 28 0 0 25 0 1 0 1855248462 12406784 2825 4294967295 134512640 135094434 3221224432 3221223056 134557648 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3029 2825 145 145 0 2884 0
[pid=15931] vsize: 12116
Current children cumulated CPU time (s) 209.73
Current children cumulated vsize (Kb) 14240

[startup+220.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 2894 0 0 0 21944 28 0 0 25 0 1 0 1855248462 12472320 2836 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3045 2836 145 145 0 2900 0
[pid=15931] vsize: 12180
Current children cumulated CPU time (s) 219.73
Current children cumulated vsize (Kb) 14304

[startup+230.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 2919 0 0 0 22944 28 0 0 25 0 1 0 1855248462 12591104 2861 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3074 2861 145 145 0 2929 0
[pid=15931] vsize: 12296
Current children cumulated CPU time (s) 229.73
Current children cumulated vsize (Kb) 14420

[startup+240.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 2923 0 0 0 23945 28 0 0 25 0 1 0 1855248462 12599296 2865 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3076 2865 145 145 0 2931 0
[pid=15931] vsize: 12304
Current children cumulated CPU time (s) 239.74
Current children cumulated vsize (Kb) 14428

[startup+250.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 2948 0 0 0 24945 28 0 0 25 0 1 0 1855248462 12730368 2890 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3108 2890 145 145 0 2963 0
[pid=15931] vsize: 12432
Current children cumulated CPU time (s) 249.74
Current children cumulated vsize (Kb) 14556

[startup+260.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 2966 0 0 0 25945 28 0 0 25 0 1 0 1855248462 12804096 2908 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3126 2908 145 145 0 2981 0
[pid=15931] vsize: 12504
Current children cumulated CPU time (s) 259.74
Current children cumulated vsize (Kb) 14628

[startup+270.031 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 2981 0 0 0 26945 28 0 0 25 0 1 0 1855248462 12886016 2923 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3146 2923 145 145 0 3001 0
[pid=15931] vsize: 12584
Current children cumulated CPU time (s) 269.74
Current children cumulated vsize (Kb) 14708

[startup+280.031 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 2995 0 0 0 27945 28 0 0 25 0 1 0 1855248462 12951552 2937 4294967295 134512640 135094434 3221224432 3221223088 134557956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3162 2937 145 145 0 3017 0
[pid=15931] vsize: 12648
Current children cumulated CPU time (s) 279.74
Current children cumulated vsize (Kb) 14772

[startup+290.032 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 2995 0 0 0 28945 28 0 0 25 0 1 0 1855248462 12951552 2937 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3162 2937 145 145 0 3017 0
[pid=15931] vsize: 12648
Current children cumulated CPU time (s) 289.74
Current children cumulated vsize (Kb) 14772

[startup+300.034 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 2995 0 0 0 29945 28 0 0 25 0 1 0 1855248462 12951552 2937 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3162 2937 145 145 0 3017 0
[pid=15931] vsize: 12648
Current children cumulated CPU time (s) 299.74
Current children cumulated vsize (Kb) 14772

[startup+310.034 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3015 0 0 0 30945 29 0 0 25 0 1 0 1855248462 13049856 2957 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3186 2957 145 145 0 3041 0
[pid=15931] vsize: 12744
Current children cumulated CPU time (s) 309.75
Current children cumulated vsize (Kb) 14868

[startup+320.034 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3032 0 0 0 31945 29 0 0 25 0 1 0 1855248462 13115392 2974 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3202 2974 145 145 0 3057 0
[pid=15931] vsize: 12808
Current children cumulated CPU time (s) 319.75
Current children cumulated vsize (Kb) 14932

[startup+330.035 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3051 0 0 0 32945 29 0 0 25 0 1 0 1855248462 13197312 2993 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3222 2993 145 145 0 3077 0
[pid=15931] vsize: 12888
Current children cumulated CPU time (s) 329.75
Current children cumulated vsize (Kb) 15012

[startup+340.035 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3051 0 0 0 33945 29 0 0 25 0 1 0 1855248462 13197312 2993 4294967295 134512640 135094434 3221224432 3221223056 134557616 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3222 2993 145 145 0 3077 0
[pid=15931] vsize: 12888
Current children cumulated CPU time (s) 339.75
Current children cumulated vsize (Kb) 15012

[startup+350.035 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3060 0 0 0 34945 29 0 0 25 0 1 0 1855248462 13262848 3002 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3238 3002 145 145 0 3093 0
[pid=15931] vsize: 12952
Current children cumulated CPU time (s) 349.75
Current children cumulated vsize (Kb) 15076

[startup+360.036 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3070 0 0 0 35945 29 0 0 25 0 1 0 1855248462 13328384 3012 4294967295 134512640 135094434 3221224432 3221223056 134557669 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3254 3012 145 145 0 3109 0
[pid=15931] vsize: 13016
Current children cumulated CPU time (s) 359.75
Current children cumulated vsize (Kb) 15140

[startup+370.036 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3070 0 0 0 36945 29 0 0 25 0 1 0 1855248462 13328384 3012 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3254 3012 145 145 0 3109 0
[pid=15931] vsize: 13016
Current children cumulated CPU time (s) 369.75
Current children cumulated vsize (Kb) 15140

[startup+380.036 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3070 0 0 0 37946 29 0 0 25 0 1 0 1855248462 13328384 3012 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3254 3012 145 145 0 3109 0
[pid=15931] vsize: 13016
Current children cumulated CPU time (s) 379.76
Current children cumulated vsize (Kb) 15140

[startup+390.037 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3070 0 0 0 38946 29 0 0 25 0 1 0 1855248462 13328384 3012 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3254 3012 145 145 0 3109 0
[pid=15931] vsize: 13016
Current children cumulated CPU time (s) 389.76
Current children cumulated vsize (Kb) 15140

[startup+400.038 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3072 0 0 0 39946 29 0 0 25 0 1 0 1855248462 13328384 3014 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3254 3014 145 145 0 3109 0
[pid=15931] vsize: 13016
Current children cumulated CPU time (s) 399.76
Current children cumulated vsize (Kb) 15140

[startup+410.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3072 0 0 0 40946 29 0 0 25 0 1 0 1855248462 13328384 3014 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3254 3014 145 145 0 3109 0
[pid=15931] vsize: 13016
Current children cumulated CPU time (s) 409.76
Current children cumulated vsize (Kb) 15140

[startup+420.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3136 0 0 0 41946 30 0 0 25 0 1 0 1855248462 13590528 3078 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3318 3078 145 145 0 3173 0
[pid=15931] vsize: 13272
Current children cumulated CPU time (s) 419.77
Current children cumulated vsize (Kb) 15396

[startup+430.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3144 0 0 0 42946 30 0 0 25 0 1 0 1855248462 13639680 3086 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3330 3086 145 145 0 3185 0
[pid=15931] vsize: 13320
Current children cumulated CPU time (s) 429.77
Current children cumulated vsize (Kb) 15444

[startup+440.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3167 0 0 0 43946 30 0 0 25 0 1 0 1855248462 13733888 3109 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3353 3109 145 145 0 3208 0
[pid=15931] vsize: 13412
Current children cumulated CPU time (s) 439.77
Current children cumulated vsize (Kb) 15536

[startup+450.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3180 0 0 0 44946 30 0 0 25 0 1 0 1855248462 13799424 3122 4294967295 134512640 135094434 3221224432 3221223072 134562115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3369 3122 145 145 0 3224 0
[pid=15931] vsize: 13476
Current children cumulated CPU time (s) 449.77
Current children cumulated vsize (Kb) 15600

[startup+460.041 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3181 0 0 0 45947 30 0 0 25 0 1 0 1855248462 13799424 3123 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3369 3123 145 145 0 3224 0
[pid=15931] vsize: 13476
Current children cumulated CPU time (s) 459.78
Current children cumulated vsize (Kb) 15600

[startup+470.042 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3202 0 0 0 46947 30 0 0 25 0 1 0 1855248462 13914112 3144 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3397 3144 145 145 0 3252 0
[pid=15931] vsize: 13588
Current children cumulated CPU time (s) 469.78
Current children cumulated vsize (Kb) 15712

[startup+480.043 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3212 0 0 0 47947 30 0 0 25 0 1 0 1855248462 13979648 3154 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3413 3154 145 145 0 3268 0
[pid=15931] vsize: 13652
Current children cumulated CPU time (s) 479.78
Current children cumulated vsize (Kb) 15776

[startup+490.042 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3212 0 0 0 48947 30 0 0 25 0 1 0 1855248462 13979648 3154 4294967295 134512640 135094434 3221224432 3221223088 134557984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3413 3154 145 145 0 3268 0
[pid=15931] vsize: 13652
Current children cumulated CPU time (s) 489.78
Current children cumulated vsize (Kb) 15776

[startup+500.043 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3234 0 0 0 49947 30 0 0 25 0 1 0 1855248462 14077952 3176 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3437 3176 145 145 0 3292 0
[pid=15931] vsize: 13748
Current children cumulated CPU time (s) 499.78
Current children cumulated vsize (Kb) 15872

[startup+510.044 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3239 0 0 0 50947 30 0 0 25 0 1 0 1855248462 14143488 3181 4294967295 134512640 135094434 3221224432 3221223104 134556549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3453 3181 145 145 0 3308 0
[pid=15931] vsize: 13812
Current children cumulated CPU time (s) 509.78
Current children cumulated vsize (Kb) 15936

[startup+520.043 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3239 0 0 0 51947 30 0 0 25 0 1 0 1855248462 14143488 3181 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3453 3181 145 145 0 3308 0
[pid=15931] vsize: 13812
Current children cumulated CPU time (s) 519.78
Current children cumulated vsize (Kb) 15936

[startup+530.044 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3257 0 0 0 52947 30 0 0 25 0 1 0 1855248462 14192640 3199 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3465 3199 145 145 0 3320 0
[pid=15931] vsize: 13860
Current children cumulated CPU time (s) 529.78
Current children cumulated vsize (Kb) 15984

[startup+540.045 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3308 0 0 0 53946 31 0 0 25 0 1 0 1855248462 14389248 3250 4294967295 134512640 135094434 3221224432 3221223024 134557236 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3513 3250 145 145 0 3368 0
[pid=15931] vsize: 14052
Current children cumulated CPU time (s) 539.78
Current children cumulated vsize (Kb) 16176

[startup+550.046 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3326 0 0 0 54946 31 0 0 25 0 1 0 1855248462 14467072 3268 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3532 3268 145 145 0 3387 0
[pid=15931] vsize: 14128
Current children cumulated CPU time (s) 549.78
Current children cumulated vsize (Kb) 16252

[startup+560.046 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3338 0 0 0 55947 31 0 0 25 0 1 0 1855248462 14532608 3280 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3548 3280 145 145 0 3403 0
[pid=15931] vsize: 14192
Current children cumulated CPU time (s) 559.79
Current children cumulated vsize (Kb) 16316

[startup+570.047 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3418 0 0 0 56945 32 0 0 25 0 1 0 1855248462 14860288 3360 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3628 3360 145 145 0 3483 0
[pid=15931] vsize: 14512
Current children cumulated CPU time (s) 569.78
Current children cumulated vsize (Kb) 16636

[startup+580.048 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3429 0 0 0 57945 32 0 0 25 0 1 0 1855248462 14913536 3371 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3641 3371 145 145 0 3496 0
[pid=15931] vsize: 14564
Current children cumulated CPU time (s) 579.78
Current children cumulated vsize (Kb) 16688

[startup+590.047 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3440 0 0 0 58946 32 0 0 25 0 1 0 1855248462 14962688 3382 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3653 3382 145 145 0 3508 0
[pid=15931] vsize: 14612
Current children cumulated CPU time (s) 589.79
Current children cumulated vsize (Kb) 16736

[startup+600.049 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3444 0 0 0 59946 32 0 0 25 0 1 0 1855248462 14979072 3386 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3657 3386 145 145 0 3512 0
[pid=15931] vsize: 14628
Current children cumulated CPU time (s) 599.79
Current children cumulated vsize (Kb) 16752

[startup+610.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3474 0 0 0 60945 32 0 0 25 0 1 0 1855248462 15097856 3416 4294967295 134512640 135094434 3221224432 3221223024 134556765 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3686 3416 145 145 0 3541 0
[pid=15931] vsize: 14744
Current children cumulated CPU time (s) 609.78
Current children cumulated vsize (Kb) 16868

[startup+620.049 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3474 0 0 0 61945 32 0 0 25 0 1 0 1855248462 15097856 3416 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3686 3416 145 145 0 3541 0
[pid=15931] vsize: 14744
Current children cumulated CPU time (s) 619.78
Current children cumulated vsize (Kb) 16868

[startup+630.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3504 0 0 0 62945 32 0 0 25 0 1 0 1855248462 15261696 3446 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3726 3446 145 145 0 3581 0
[pid=15931] vsize: 14904
Current children cumulated CPU time (s) 629.78
Current children cumulated vsize (Kb) 17028

[startup+640.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3505 0 0 0 63945 32 0 0 25 0 1 0 1855248462 15261696 3447 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3726 3447 145 145 0 3581 0
[pid=15931] vsize: 14904
Current children cumulated CPU time (s) 639.78
Current children cumulated vsize (Kb) 17028

[startup+650.051 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3505 0 0 0 64946 32 0 0 25 0 1 0 1855248462 15261696 3447 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3726 3447 145 145 0 3581 0
[pid=15931] vsize: 14904
Current children cumulated CPU time (s) 649.79
Current children cumulated vsize (Kb) 17028

[startup+660.051 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3513 0 0 0 65946 32 0 0 25 0 1 0 1855248462 15294464 3455 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3734 3455 145 145 0 3589 0
[pid=15931] vsize: 14936
Current children cumulated CPU time (s) 659.79
Current children cumulated vsize (Kb) 17060

[startup+670.052 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3517 0 0 0 66946 32 0 0 25 0 1 0 1855248462 15360000 3459 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3750 3459 145 145 0 3605 0
[pid=15931] vsize: 15000
Current children cumulated CPU time (s) 669.79
Current children cumulated vsize (Kb) 17124

[startup+680.053 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3517 0 0 0 67946 32 0 0 25 0 1 0 1855248462 15360000 3459 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3750 3459 145 145 0 3605 0
[pid=15931] vsize: 15000
Current children cumulated CPU time (s) 679.79
Current children cumulated vsize (Kb) 17124

[startup+690.053 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3526 0 0 0 68947 32 0 0 25 0 1 0 1855248462 15425536 3468 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3766 3468 145 145 0 3621 0
[pid=15931] vsize: 15064
Current children cumulated CPU time (s) 689.8
Current children cumulated vsize (Kb) 17188

[startup+700.054 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3528 0 0 0 69947 32 0 0 25 0 1 0 1855248462 15425536 3470 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3766 3470 145 145 0 3621 0
[pid=15931] vsize: 15064
Current children cumulated CPU time (s) 699.8
Current children cumulated vsize (Kb) 17188

[startup+710.055 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3564 0 0 0 70947 32 0 0 25 0 1 0 1855248462 15552512 3506 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3797 3506 145 145 0 3652 0
[pid=15931] vsize: 15188
Current children cumulated CPU time (s) 709.8
Current children cumulated vsize (Kb) 17312

[startup+720.056 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3567 0 0 0 71947 32 0 0 25 0 1 0 1855248462 15552512 3509 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3797 3509 145 145 0 3652 0
[pid=15931] vsize: 15188
Current children cumulated CPU time (s) 719.8
Current children cumulated vsize (Kb) 17312

[startup+730.056 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3586 0 0 0 72947 32 0 0 25 0 1 0 1855248462 15650816 3528 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3821 3528 145 145 0 3676 0
[pid=15931] vsize: 15284
Current children cumulated CPU time (s) 729.8
Current children cumulated vsize (Kb) 17408

[startup+740.057 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3610 0 0 0 73947 33 0 0 25 0 1 0 1855248462 15818752 3552 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3862 3552 145 145 0 3717 0
[pid=15931] vsize: 15448
Current children cumulated CPU time (s) 739.81
Current children cumulated vsize (Kb) 17572

[startup+750.058 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3637 0 0 0 74947 33 0 0 25 0 1 0 1855248462 15921152 3579 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3887 3579 145 145 0 3742 0
[pid=15931] vsize: 15548
Current children cumulated CPU time (s) 749.81
Current children cumulated vsize (Kb) 17672

[startup+760.058 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3643 0 0 0 75947 33 0 0 25 0 1 0 1855248462 15953920 3585 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3895 3585 145 145 0 3750 0
[pid=15931] vsize: 15580
Current children cumulated CPU time (s) 759.81
Current children cumulated vsize (Kb) 17704

[startup+770.059 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3661 0 0 0 76947 33 0 0 25 0 1 0 1855248462 16052224 3603 4294967295 134512640 135094434 3221224432 3221223088 134558162 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3919 3603 145 145 0 3774 0
[pid=15931] vsize: 15676
Current children cumulated CPU time (s) 769.81
Current children cumulated vsize (Kb) 17800

[startup+780.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3664 0 0 0 77948 33 0 0 25 0 1 0 1855248462 16052224 3606 4294967295 134512640 135094434 3221224432 3221223024 134551454 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3919 3606 145 145 0 3774 0
[pid=15931] vsize: 15676
Current children cumulated CPU time (s) 779.82
Current children cumulated vsize (Kb) 17800

[startup+790.061 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3667 0 0 0 78948 33 0 0 25 0 1 0 1855248462 16068608 3609 4294967295 134512640 135094434 3221224432 3221223104 134556543 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3923 3609 145 145 0 3778 0
[pid=15931] vsize: 15692
Current children cumulated CPU time (s) 789.82
Current children cumulated vsize (Kb) 17816

[startup+800.061 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3672 0 0 0 79948 33 0 0 25 0 1 0 1855248462 16101376 3614 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3931 3614 145 145 0 3786 0
[pid=15931] vsize: 15724
Current children cumulated CPU time (s) 799.82
Current children cumulated vsize (Kb) 17848

[startup+810.062 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3677 0 0 0 80948 33 0 0 25 0 1 0 1855248462 16134144 3619 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3939 3619 145 145 0 3794 0
[pid=15931] vsize: 15756
Current children cumulated CPU time (s) 809.82
Current children cumulated vsize (Kb) 17880

[startup+820.063 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3677 0 0 0 81949 33 0 0 25 0 1 0 1855248462 16134144 3619 4294967295 134512640 135094434 3221224432 3221223024 134551434 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3939 3619 145 145 0 3794 0
[pid=15931] vsize: 15756
Current children cumulated CPU time (s) 819.83
Current children cumulated vsize (Kb) 17880

[startup+830.063 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3677 0 0 0 82949 33 0 0 25 0 1 0 1855248462 16134144 3619 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 3939 3619 145 145 0 3794 0
[pid=15931] vsize: 15756
Current children cumulated CPU time (s) 829.83
Current children cumulated vsize (Kb) 17880

[startup+840.064 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3678 0 0 0 83948 33 0 0 25 0 1 0 1855248462 16134144 3620 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15931/statm): 3939 3620 145 145 0 3794 0
[pid=15931] vsize: 15756
Current children cumulated CPU time (s) 839.82
Current children cumulated vsize (Kb) 17880

[startup+850.066 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3770 0 0 0 84947 33 0 0 25 0 1 0 1855248462 16510976 3712 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 4031 3712 145 145 0 3886 0
[pid=15931] vsize: 16124
Current children cumulated CPU time (s) 849.81
Current children cumulated vsize (Kb) 18248

[startup+860.067 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3876 0 0 0 85945 34 0 0 25 0 1 0 1855248462 16941056 3818 4294967295 134512640 135094434 3221224432 3221223104 134556490 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 4136 3818 145 145 0 3991 0
[pid=15931] vsize: 16544
Current children cumulated CPU time (s) 859.8
Current children cumulated vsize (Kb) 18668

[startup+870.066 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3889 0 0 0 86945 34 0 0 25 0 1 0 1855248462 17039360 3831 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 4160 3831 145 145 0 4015 0
[pid=15931] vsize: 16640
Current children cumulated CPU time (s) 869.8
Current children cumulated vsize (Kb) 18764

[startup+880.067 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3892 0 0 0 87946 34 0 0 25 0 1 0 1855248462 17039360 3834 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 4160 3834 145 145 0 4015 0
[pid=15931] vsize: 16640
Current children cumulated CPU time (s) 879.81
Current children cumulated vsize (Kb) 18764

[startup+890.068 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 3927 0 0 0 88946 35 0 0 25 0 1 0 1855248462 17149952 3869 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 4187 3869 145 145 0 4042 0
[pid=15931] vsize: 16748
Current children cumulated CPU time (s) 889.82
Current children cumulated vsize (Kb) 18872

[startup+900.069 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 4113 0 0 0 89943 36 0 0 25 0 1 0 1855248462 17944576 4055 4294967295 134512640 135094434 3221224432 3221223088 134558123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 4381 4055 145 145 0 4236 0
[pid=15931] vsize: 17524
Current children cumulated CPU time (s) 899.8
Current children cumulated vsize (Kb) 19648

[startup+910.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 4125 0 0 0 90943 36 0 0 25 0 1 0 1855248462 18010112 4067 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 4397 4067 145 145 0 4252 0
[pid=15931] vsize: 17588
Current children cumulated CPU time (s) 909.8
Current children cumulated vsize (Kb) 19712

[startup+920.071 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 4128 0 0 0 91943 36 0 0 25 0 1 0 1855248462 18059264 4070 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 4409 4070 145 145 0 4264 0
[pid=15931] vsize: 17636
Current children cumulated CPU time (s) 919.8
Current children cumulated vsize (Kb) 19760

[startup+930.072 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 4137 0 0 0 92943 36 0 0 25 0 1 0 1855248462 18075648 4079 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 4413 4079 145 145 0 4268 0
[pid=15931] vsize: 17652
Current children cumulated CPU time (s) 929.8
Current children cumulated vsize (Kb) 19776

[startup+940.072 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 4138 0 0 0 93944 36 0 0 25 0 1 0 1855248462 18075648 4080 4294967295 134512640 135094434 3221224432 3221223120 134554751 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 4413 4080 145 145 0 4268 0
[pid=15931] vsize: 17652
Current children cumulated CPU time (s) 939.81
Current children cumulated vsize (Kb) 19776

[startup+950.073 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 4140 0 0 0 94944 36 0 0 25 0 1 0 1855248462 18075648 4082 4294967295 134512640 135094434 3221224432 3221223088 134558176 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 4413 4082 145 145 0 4268 0
[pid=15931] vsize: 17652
Current children cumulated CPU time (s) 949.81
Current children cumulated vsize (Kb) 19776

[startup+960.074 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 4140 0 0 0 95944 36 0 0 25 0 1 0 1855248462 18075648 4082 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 4413 4082 145 145 0 4268 0
[pid=15931] vsize: 17652
Current children cumulated CPU time (s) 959.81
Current children cumulated vsize (Kb) 19776

[startup+970.073 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 4145 0 0 0 96944 36 0 0 25 0 1 0 1855248462 18092032 4087 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 4417 4087 145 145 0 4272 0
[pid=15931] vsize: 17668
Current children cumulated CPU time (s) 969.81
Current children cumulated vsize (Kb) 19792

[startup+980.074 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 4159 0 0 0 97944 37 0 0 25 0 1 0 1855248462 18173952 4101 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 4437 4101 145 145 0 4292 0
[pid=15931] vsize: 17748
Current children cumulated CPU time (s) 979.82
Current children cumulated vsize (Kb) 19872

[startup+990.075 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 4159 0 0 0 98944 37 0 0 25 0 1 0 1855248462 18173952 4101 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 4437 4101 145 145 0 4292 0
[pid=15931] vsize: 17748
Current children cumulated CPU time (s) 989.82
Current children cumulated vsize (Kb) 19872

[startup+1000.08 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 4160 0 0 0 99945 37 0 0 25 0 1 0 1855248462 18173952 4102 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 4437 4102 145 145 0 4292 0
[pid=15931] vsize: 17748
Current children cumulated CPU time (s) 999.83
Current children cumulated vsize (Kb) 19872

[startup+1010.08 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 4166 0 0 0 100945 37 0 0 25 0 1 0 1855248462 18206720 4108 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 4445 4108 145 145 0 4300 0
[pid=15931] vsize: 17780
Current children cumulated CPU time (s) 1009.83
Current children cumulated vsize (Kb) 19904

[startup+1020.08 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 4178 0 0 0 101945 37 0 0 25 0 1 0 1855248462 18272256 4120 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 4461 4120 145 145 0 4316 0
[pid=15931] vsize: 17844
Current children cumulated CPU time (s) 1019.83
Current children cumulated vsize (Kb) 19968

[startup+1030.08 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 4178 0 0 0 102945 37 0 0 25 0 1 0 1855248462 18272256 4120 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 4461 4120 145 145 0 4316 0
[pid=15931] vsize: 17844
Current children cumulated CPU time (s) 1029.83
Current children cumulated vsize (Kb) 19968

[startup+1040.08 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 4183 0 0 0 103945 37 0 0 25 0 1 0 1855248462 18305024 4125 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 4469 4125 145 145 0 4324 0
[pid=15931] vsize: 17876
Current children cumulated CPU time (s) 1039.83
Current children cumulated vsize (Kb) 20000

[startup+1050.08 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 4188 0 0 0 104946 37 0 0 25 0 1 0 1855248462 18337792 4130 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 4477 4130 145 145 0 4332 0
[pid=15931] vsize: 17908
Current children cumulated CPU time (s) 1049.84
Current children cumulated vsize (Kb) 20032

[startup+1060.08 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 4197 0 0 0 105946 37 0 0 25 0 1 0 1855248462 18403328 4139 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 4493 4139 145 145 0 4348 0
[pid=15931] vsize: 17972
Current children cumulated CPU time (s) 1059.84
Current children cumulated vsize (Kb) 20096

[startup+1070.08 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 4200 0 0 0 106946 37 0 0 25 0 1 0 1855248462 18403328 4142 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 4493 4142 145 145 0 4348 0
[pid=15931] vsize: 17972
Current children cumulated CPU time (s) 1069.84
Current children cumulated vsize (Kb) 20096

[startup+1080.08 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 4200 0 0 0 107946 37 0 0 25 0 1 0 1855248462 18403328 4142 4294967295 134512640 135094434 3221224432 3221223072 134562085 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 4493 4142 145 145 0 4348 0
[pid=15931] vsize: 17972
Current children cumulated CPU time (s) 1079.84
Current children cumulated vsize (Kb) 20096

[startup+1090.08 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 4200 0 0 0 108947 37 0 0 25 0 1 0 1855248462 18403328 4142 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 4493 4142 145 145 0 4348 0
[pid=15931] vsize: 17972
Current children cumulated CPU time (s) 1089.85
Current children cumulated vsize (Kb) 20096

[startup+1100.08 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 4200 0 0 0 109947 37 0 0 25 0 1 0 1855248462 18403328 4142 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 4493 4142 145 145 0 4348 0
[pid=15931] vsize: 17972
Current children cumulated CPU time (s) 1099.85
Current children cumulated vsize (Kb) 20096

[startup+1110.08 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 4200 0 0 0 110947 37 0 0 25 0 1 0 1855248462 18403328 4142 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 4493 4142 145 145 0 4348 0
[pid=15931] vsize: 17972
Current children cumulated CPU time (s) 1109.85
Current children cumulated vsize (Kb) 20096

[startup+1120.08 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 4203 0 0 0 111947 37 0 0 25 0 1 0 1855248462 18403328 4145 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 4493 4145 145 145 0 4348 0
[pid=15931] vsize: 17972
Current children cumulated CPU time (s) 1119.85
Current children cumulated vsize (Kb) 20096

[startup+1130.08 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 4203 0 0 0 112947 37 0 0 25 0 1 0 1855248462 18403328 4145 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 4493 4145 145 145 0 4348 0
[pid=15931] vsize: 17972
Current children cumulated CPU time (s) 1129.85
Current children cumulated vsize (Kb) 20096

[startup+1140.08 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 4203 0 0 0 113948 37 0 0 25 0 1 0 1855248462 18403328 4145 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 4493 4145 145 145 0 4348 0
[pid=15931] vsize: 17972
Current children cumulated CPU time (s) 1139.86
Current children cumulated vsize (Kb) 20096

[startup+1150.09 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 4203 0 0 0 114948 37 0 0 25 0 1 0 1855248462 18403328 4145 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 4493 4145 145 145 0 4348 0
[pid=15931] vsize: 17972
Current children cumulated CPU time (s) 1149.86
Current children cumulated vsize (Kb) 20096

[startup+1160.09 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 4203 0 0 0 115948 37 0 0 25 0 1 0 1855248462 18403328 4145 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 4493 4145 145 145 0 4348 0
[pid=15931] vsize: 17972
Current children cumulated CPU time (s) 1159.86
Current children cumulated vsize (Kb) 20096

[startup+1170.09 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 4203 0 0 0 116948 37 0 0 25 0 1 0 1855248462 18403328 4145 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 4493 4145 145 145 0 4348 0
[pid=15931] vsize: 17972
Current children cumulated CPU time (s) 1169.86
Current children cumulated vsize (Kb) 20096

[startup+1180.09 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 4203 0 0 0 117949 37 0 0 25 0 1 0 1855248462 18403328 4145 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 4493 4145 145 145 0 4348 0
[pid=15931] vsize: 17972
Current children cumulated CPU time (s) 1179.87
Current children cumulated vsize (Kb) 20096

[startup+1190.09 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 4203 0 0 0 118949 37 0 0 25 0 1 0 1855248462 18403328 4145 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 4493 4145 145 145 0 4348 0
[pid=15931] vsize: 17972
Current children cumulated CPU time (s) 1189.87
Current children cumulated vsize (Kb) 20096

[startup+1200.09 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 4254 0 0 0 119949 37 0 0 25 0 1 0 1855248462 18620416 4196 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 4546 4196 145 145 0 4401 0
[pid=15931] vsize: 18184
Current children cumulated CPU time (s) 1199.87
Current children cumulated vsize (Kb) 20308

[startup+1210.09 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 4254 0 0 0 120949 37 0 0 25 0 1 0 1855248462 18620416 4196 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 4546 4196 145 145 0 4401 0
[pid=15931] vsize: 18184
Current children cumulated CPU time (s) 1209.87
Current children cumulated vsize (Kb) 20308



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15931
Raw data (/proc/15927/stat): 15927 (minisat+_script) S 15926 15927 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855248457 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15927/statm): 531 226 485 147 0 384 0
[pid=15927] vsize: 2124
Raw data (/proc/15931/stat): 15931 (minisat+_64-bit) R 15927 15927 21452 0 -1 0 4254 0 0 0 120949 37 0 0 25 0 1 0 1855248462 18620416 4196 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15931/statm): 4546 4196 145 145 0 4401 0
[pid=15931] vsize: 18184
Current children cumulated CPU time (s) 1209.87
Current children cumulated vsize (Kb) 20308

Sending SIGTERM to -15927
Sleeping 2 seconds
One traced child (pid=15927) ended because it received signal 15 (SIGTERM)
One traced child (pid=15931) exited with status: 0
All traced children have exited ! Game is over.

Child status: 0
Real time (s): 1210.1
CPU time (s): 1209.88
CPU user time (s): 1209.5
CPU system time (s): 0.381941
CPU usage (%): 99.9813
Max. virtual memory (cumulated for all children) (Kb): 20308

Verifier Data

ERROR: no interpretation found !