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

Launcher Data

LAUNCH ON wulflinc22 THE 2005-09-19 03:19:59 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2877 boxname=wulflinc22 idbench=533 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6f47095f2d417d23ced995954e641689  /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-20-10-p0548.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-20-10-p0548.opb
IDLAUNCH: 2877
/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:        891972 kB
Buffers:         35816 kB
Cached:          79452 kB
SwapCached:        536 kB
Active:          73936 kB
Inactive:        43956 kB
HighTotal:      131008 kB
HighFree:        49448 kB
LowTotal:       903652 kB
LowFree:        842524 kB
SwapTotal:     2097892 kB
SwapFree:      2096832 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5864 kB
Slab:            19132 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-19 03:40:09 (client local time) WITH STATUS 0 IN 1209.89 SECONDS
stats: 2877 7 1209.89 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/5648/stat): 5648 (minisat+_script) R 5647 5648 21452 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1846606690 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/5648/statm): 174 3 169 147 0 27 0
[pid=5648] 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=5649
New process pid=5650
New process pid=5651
execve syscall for /bin/sed executable
One traced child (pid=5650) 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=5651) exited with status: 0
One traced child (pid=5649) exited with status: 0
New process pid=5652
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-20-10-p0548.opb

[startup+10.0031 s]
Raw data (loadavg): 0.93 0.95 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 1420 0 0 0 979 7 0 0 25 0 1 0 1846606695 6131712 1362 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5652/statm): 1497 1362 145 145 0 1352 0
[pid=5652] vsize: 5988
Current children cumulated CPU time (s) 9.87
Current children cumulated vsize (Kb) 8112

[startup+20.0038 s]
Raw data (loadavg): 0.94 0.96 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 1577 0 0 0 1976 9 0 0 25 0 1 0 1846606695 6770688 1519 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5652/statm): 1653 1519 145 145 0 1508 0
[pid=5652] vsize: 6612
Current children cumulated CPU time (s) 19.86
Current children cumulated vsize (Kb) 8736

[startup+30.0046 s]
Raw data (loadavg): 0.95 0.96 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 1779 0 0 0 2973 11 0 0 25 0 1 0 1846606695 7598080 1721 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5652/statm): 1855 1721 145 145 0 1710 0
[pid=5652] vsize: 7420
Current children cumulated CPU time (s) 29.85
Current children cumulated vsize (Kb) 9544

[startup+40.0053 s]
Raw data (loadavg): 0.95 0.96 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 2023 0 0 0 3966 14 0 0 25 0 1 0 1846606695 8597504 1965 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 2099 1965 145 145 0 1954 0
[pid=5652] vsize: 8396
Current children cumulated CPU time (s) 39.81
Current children cumulated vsize (Kb) 10520

[startup+50.006 s]
Raw data (loadavg): 0.96 0.96 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 2201 0 0 0 4963 15 0 0 25 0 1 0 1846606695 9326592 2143 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 2277 2143 145 145 0 2132 0
[pid=5652] vsize: 9108
Current children cumulated CPU time (s) 49.79
Current children cumulated vsize (Kb) 11232

[startup+60.0067 s]
Raw data (loadavg): 0.97 0.96 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 2240 0 0 0 5963 15 0 0 25 0 1 0 1846606695 9523200 2182 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 2325 2182 145 145 0 2180 0
[pid=5652] vsize: 9300
Current children cumulated CPU time (s) 59.79
Current children cumulated vsize (Kb) 11424

[startup+70.0074 s]
Raw data (loadavg): 0.97 0.96 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 2252 0 0 0 6963 15 0 0 25 0 1 0 1846606695 9572352 2194 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 2337 2194 145 145 0 2192 0
[pid=5652] vsize: 9348
Current children cumulated CPU time (s) 69.79
Current children cumulated vsize (Kb) 11472

[startup+80.0081 s]
Raw data (loadavg): 0.98 0.96 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 2280 0 0 0 7963 15 0 0 25 0 1 0 1846606695 9719808 2222 4294967295 134512640 135094434 3221224432 3221223088 134558240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 2373 2222 145 145 0 2228 0
[pid=5652] vsize: 9492
Current children cumulated CPU time (s) 79.79
Current children cumulated vsize (Kb) 11616

[startup+90.0078 s]
Raw data (loadavg): 0.98 0.96 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 2285 0 0 0 8963 16 0 0 25 0 1 0 1846606695 9736192 2227 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 2377 2227 145 145 0 2232 0
[pid=5652] vsize: 9508
Current children cumulated CPU time (s) 89.8
Current children cumulated vsize (Kb) 11632

[startup+100.009 s]
Raw data (loadavg): 0.98 0.96 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 2299 0 0 0 9963 16 0 0 25 0 1 0 1846606695 9801728 2241 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 2393 2241 145 145 0 2248 0
[pid=5652] vsize: 9572
Current children cumulated CPU time (s) 99.8
Current children cumulated vsize (Kb) 11696

[startup+110.009 s]
Raw data (loadavg): 0.98 0.96 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 2326 0 0 0 10963 16 0 0 25 0 1 0 1846606695 9895936 2268 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 2416 2268 145 145 0 2271 0
[pid=5652] vsize: 9664
Current children cumulated CPU time (s) 109.8
Current children cumulated vsize (Kb) 11788

[startup+120.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 2348 0 0 0 11963 16 0 0 25 0 1 0 1846606695 9994240 2290 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 2440 2290 145 145 0 2295 0
[pid=5652] vsize: 9760
Current children cumulated CPU time (s) 119.8
Current children cumulated vsize (Kb) 11884

[startup+130.011 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 2410 0 0 0 12963 16 0 0 25 0 1 0 1846606695 10244096 2352 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 2501 2352 145 145 0 2356 0
[pid=5652] vsize: 10004
Current children cumulated CPU time (s) 129.8
Current children cumulated vsize (Kb) 12128

[startup+140.011 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 2538 0 0 0 13960 17 0 0 25 0 1 0 1846606695 10780672 2480 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 2632 2480 145 145 0 2487 0
[pid=5652] vsize: 10528
Current children cumulated CPU time (s) 139.78
Current children cumulated vsize (Kb) 12652

[startup+150.012 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 2550 0 0 0 14960 17 0 0 25 0 1 0 1846606695 10829824 2492 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 2644 2492 145 145 0 2499 0
[pid=5652] vsize: 10576
Current children cumulated CPU time (s) 149.78
Current children cumulated vsize (Kb) 12700

[startup+160.013 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 2724 0 0 0 15957 19 0 0 25 0 1 0 1846606695 11575296 2666 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 2826 2666 145 145 0 2681 0
[pid=5652] vsize: 11304
Current children cumulated CPU time (s) 159.77
Current children cumulated vsize (Kb) 13428

[startup+170.014 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 2740 0 0 0 16957 19 0 0 25 0 1 0 1846606695 11673600 2682 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 2850 2682 145 145 0 2705 0
[pid=5652] vsize: 11400
Current children cumulated CPU time (s) 169.77
Current children cumulated vsize (Kb) 13524

[startup+180.014 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 2853 0 0 0 17955 19 0 0 25 0 1 0 1846606695 12259328 2795 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 2993 2795 145 145 0 2848 0
[pid=5652] vsize: 11972
Current children cumulated CPU time (s) 179.75
Current children cumulated vsize (Kb) 14096

[startup+190.014 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 2857 0 0 0 18956 19 0 0 25 0 1 0 1846606695 12275712 2799 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 2997 2799 145 145 0 2852 0
[pid=5652] vsize: 11988
Current children cumulated CPU time (s) 189.76
Current children cumulated vsize (Kb) 14112

[startup+200.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 2877 0 0 0 19956 19 0 0 25 0 1 0 1846606695 12374016 2819 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3021 2819 145 145 0 2876 0
[pid=5652] vsize: 12084
Current children cumulated CPU time (s) 199.76
Current children cumulated vsize (Kb) 14208

[startup+210.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 2877 0 0 0 20956 19 0 0 25 0 1 0 1846606695 12374016 2819 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3021 2819 145 145 0 2876 0
[pid=5652] vsize: 12084
Current children cumulated CPU time (s) 209.76
Current children cumulated vsize (Kb) 14208

[startup+220.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 2894 0 0 0 21956 19 0 0 25 0 1 0 1846606695 12472320 2836 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3045 2836 145 145 0 2900 0
[pid=5652] vsize: 12180
Current children cumulated CPU time (s) 219.76
Current children cumulated vsize (Kb) 14304

[startup+230.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 2919 0 0 0 22956 19 0 0 25 0 1 0 1846606695 12591104 2861 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3074 2861 145 145 0 2929 0
[pid=5652] vsize: 12296
Current children cumulated CPU time (s) 229.76
Current children cumulated vsize (Kb) 14420

[startup+240.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 2921 0 0 0 23956 19 0 0 25 0 1 0 1846606695 12591104 2863 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3074 2863 145 145 0 2929 0
[pid=5652] vsize: 12296
Current children cumulated CPU time (s) 239.76
Current children cumulated vsize (Kb) 14420

[startup+250.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 2947 0 0 0 24956 20 0 0 25 0 1 0 1846606695 12730368 2889 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3108 2889 145 145 0 2963 0
[pid=5652] vsize: 12432
Current children cumulated CPU time (s) 249.77
Current children cumulated vsize (Kb) 14556

[startup+260.019 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 2966 0 0 0 25956 20 0 0 25 0 1 0 1846606695 12804096 2908 4294967295 134512640 135094434 3221224432 3221223060 134557564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3126 2908 145 145 0 2981 0
[pid=5652] vsize: 12504
Current children cumulated CPU time (s) 259.77
Current children cumulated vsize (Kb) 14628

[startup+270.019 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 2980 0 0 0 26956 20 0 0 25 0 1 0 1846606695 12886016 2922 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3146 2922 145 145 0 3001 0
[pid=5652] vsize: 12584
Current children cumulated CPU time (s) 269.77
Current children cumulated vsize (Kb) 14708

[startup+280.019 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 2995 0 0 0 27956 20 0 0 25 0 1 0 1846606695 12951552 2937 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3162 2937 145 145 0 3017 0
[pid=5652] vsize: 12648
Current children cumulated CPU time (s) 279.77
Current children cumulated vsize (Kb) 14772

[startup+290.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 2995 0 0 0 28956 20 0 0 25 0 1 0 1846606695 12951552 2937 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3162 2937 145 145 0 3017 0
[pid=5652] vsize: 12648
Current children cumulated CPU time (s) 289.77
Current children cumulated vsize (Kb) 14772

[startup+300.021 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 2995 0 0 0 29957 20 0 0 25 0 1 0 1846606695 12951552 2937 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3162 2937 145 145 0 3017 0
[pid=5652] vsize: 12648
Current children cumulated CPU time (s) 299.78
Current children cumulated vsize (Kb) 14772

[startup+310.022 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3015 0 0 0 30956 21 0 0 25 0 1 0 1846606695 13049856 2957 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5652/statm): 3186 2957 145 145 0 3041 0
[pid=5652] vsize: 12744
Current children cumulated CPU time (s) 309.78
Current children cumulated vsize (Kb) 14868

[startup+320.022 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3032 0 0 0 31956 21 0 0 25 0 1 0 1846606695 13115392 2974 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3202 2974 145 145 0 3057 0
[pid=5652] vsize: 12808
Current children cumulated CPU time (s) 319.78
Current children cumulated vsize (Kb) 14932

[startup+330.023 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3051 0 0 0 32956 21 0 0 25 0 1 0 1846606695 13197312 2993 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3222 2993 145 145 0 3077 0
[pid=5652] vsize: 12888
Current children cumulated CPU time (s) 329.78
Current children cumulated vsize (Kb) 15012

[startup+340.023 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3051 0 0 0 33956 21 0 0 25 0 1 0 1846606695 13197312 2993 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3222 2993 145 145 0 3077 0
[pid=5652] vsize: 12888
Current children cumulated CPU time (s) 339.78
Current children cumulated vsize (Kb) 15012

[startup+350.024 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3060 0 0 0 34956 21 0 0 25 0 1 0 1846606695 13262848 3002 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3238 3002 145 145 0 3093 0
[pid=5652] vsize: 12952
Current children cumulated CPU time (s) 349.78
Current children cumulated vsize (Kb) 15076

[startup+360.025 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3070 0 0 0 35956 21 0 0 25 0 1 0 1846606695 13328384 3012 4294967295 134512640 135094434 3221224432 3221223024 134551457 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3254 3012 145 145 0 3109 0
[pid=5652] vsize: 13016
Current children cumulated CPU time (s) 359.78
Current children cumulated vsize (Kb) 15140

[startup+370.025 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3070 0 0 0 36957 21 0 0 25 0 1 0 1846606695 13328384 3012 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3254 3012 145 145 0 3109 0
[pid=5652] vsize: 13016
Current children cumulated CPU time (s) 369.79
Current children cumulated vsize (Kb) 15140

[startup+380.026 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3070 0 0 0 37957 21 0 0 25 0 1 0 1846606695 13328384 3012 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3254 3012 145 145 0 3109 0
[pid=5652] vsize: 13016
Current children cumulated CPU time (s) 379.79
Current children cumulated vsize (Kb) 15140

[startup+390.026 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3070 0 0 0 38957 21 0 0 25 0 1 0 1846606695 13328384 3012 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3254 3012 145 145 0 3109 0
[pid=5652] vsize: 13016
Current children cumulated CPU time (s) 389.79
Current children cumulated vsize (Kb) 15140

[startup+400.027 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3072 0 0 0 39957 21 0 0 25 0 1 0 1846606695 13328384 3014 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3254 3014 145 145 0 3109 0
[pid=5652] vsize: 13016
Current children cumulated CPU time (s) 399.79
Current children cumulated vsize (Kb) 15140

[startup+410.028 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3072 0 0 0 40958 21 0 0 25 0 1 0 1846606695 13328384 3014 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3254 3014 145 145 0 3109 0
[pid=5652] vsize: 13016
Current children cumulated CPU time (s) 409.8
Current children cumulated vsize (Kb) 15140

[startup+420.028 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3136 0 0 0 41957 21 0 0 25 0 1 0 1846606695 13590528 3078 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3318 3078 145 145 0 3173 0
[pid=5652] vsize: 13272
Current children cumulated CPU time (s) 419.79
Current children cumulated vsize (Kb) 15396

[startup+430.029 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3139 0 0 0 42957 21 0 0 25 0 1 0 1846606695 13606912 3081 4294967295 134512640 135094434 3221224432 3221223104 134556242 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3322 3081 145 145 0 3177 0
[pid=5652] vsize: 13288
Current children cumulated CPU time (s) 429.79
Current children cumulated vsize (Kb) 15412

[startup+440.03 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3161 0 0 0 43957 21 0 0 25 0 1 0 1846606695 13717504 3103 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3349 3103 145 145 0 3204 0
[pid=5652] vsize: 13396
Current children cumulated CPU time (s) 439.79
Current children cumulated vsize (Kb) 15520

[startup+450.031 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3180 0 0 0 44957 22 0 0 25 0 1 0 1846606695 13799424 3122 4294967295 134512640 135094434 3221224432 3221223024 134551469 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3369 3122 145 145 0 3224 0
[pid=5652] vsize: 13476
Current children cumulated CPU time (s) 449.8
Current children cumulated vsize (Kb) 15600

[startup+460.031 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3180 0 0 0 45958 22 0 0 25 0 1 0 1846606695 13799424 3122 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3369 3122 145 145 0 3224 0
[pid=5652] vsize: 13476
Current children cumulated CPU time (s) 459.81
Current children cumulated vsize (Kb) 15600

[startup+470.032 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3201 0 0 0 46958 22 0 0 25 0 1 0 1846606695 13914112 3143 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3397 3143 145 145 0 3252 0
[pid=5652] vsize: 13588
Current children cumulated CPU time (s) 469.81
Current children cumulated vsize (Kb) 15712

[startup+480.033 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3212 0 0 0 47958 22 0 0 25 0 1 0 1846606695 13979648 3154 4294967295 134512640 135094434 3221224432 3221223024 134551463 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3413 3154 145 145 0 3268 0
[pid=5652] vsize: 13652
Current children cumulated CPU time (s) 479.81
Current children cumulated vsize (Kb) 15776

[startup+490.032 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3212 0 0 0 48958 22 0 0 25 0 1 0 1846606695 13979648 3154 4294967295 134512640 135094434 3221224432 3221223024 134551718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3413 3154 145 145 0 3268 0
[pid=5652] vsize: 13652
Current children cumulated CPU time (s) 489.81
Current children cumulated vsize (Kb) 15776

[startup+500.033 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3226 0 0 0 49958 22 0 0 25 0 1 0 1846606695 14045184 3168 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3429 3168 145 145 0 3284 0
[pid=5652] vsize: 13716
Current children cumulated CPU time (s) 499.81
Current children cumulated vsize (Kb) 15840

[startup+510.034 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3239 0 0 0 50958 22 0 0 25 0 1 0 1846606695 14143488 3181 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3453 3181 145 145 0 3308 0
[pid=5652] vsize: 13812
Current children cumulated CPU time (s) 509.81
Current children cumulated vsize (Kb) 15936

[startup+520.034 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3239 0 0 0 51957 22 0 0 25 0 1 0 1846606695 14143488 3181 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5652/statm): 3453 3181 145 145 0 3308 0
[pid=5652] vsize: 13812
Current children cumulated CPU time (s) 519.8
Current children cumulated vsize (Kb) 15936

[startup+530.034 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3257 0 0 0 52956 23 0 0 25 0 1 0 1846606695 14192640 3199 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3465 3199 145 145 0 3320 0
[pid=5652] vsize: 13860
Current children cumulated CPU time (s) 529.8
Current children cumulated vsize (Kb) 15984

[startup+540.035 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3308 0 0 0 53956 23 0 0 25 0 1 0 1846606695 14389248 3250 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3513 3250 145 145 0 3368 0
[pid=5652] vsize: 14052
Current children cumulated CPU time (s) 539.8
Current children cumulated vsize (Kb) 16176

[startup+550.036 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3311 0 0 0 54956 23 0 0 25 0 1 0 1846606695 14401536 3253 4294967295 134512640 135094434 3221224432 3221223024 134557191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3516 3253 145 145 0 3371 0
[pid=5652] vsize: 14064
Current children cumulated CPU time (s) 549.8
Current children cumulated vsize (Kb) 16188

[startup+560.036 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3331 0 0 0 55956 23 0 0 25 0 1 0 1846606695 14532608 3273 4294967295 134512640 135094434 3221224432 3221223088 134557896 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3548 3273 145 145 0 3403 0
[pid=5652] vsize: 14192
Current children cumulated CPU time (s) 559.8
Current children cumulated vsize (Kb) 16316

[startup+570.036 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3380 0 0 0 56955 24 0 0 25 0 1 0 1846606695 14704640 3322 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3590 3322 145 145 0 3445 0
[pid=5652] vsize: 14360
Current children cumulated CPU time (s) 569.8
Current children cumulated vsize (Kb) 16484

[startup+580.037 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3429 0 0 0 57955 24 0 0 25 0 1 0 1846606695 14913536 3371 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3641 3371 145 145 0 3496 0
[pid=5652] vsize: 14564
Current children cumulated CPU time (s) 579.8
Current children cumulated vsize (Kb) 16688

[startup+590.038 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3439 0 0 0 58955 24 0 0 25 0 1 0 1846606695 14962688 3381 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3653 3381 145 145 0 3508 0
[pid=5652] vsize: 14612
Current children cumulated CPU time (s) 589.8
Current children cumulated vsize (Kb) 16736

[startup+600.038 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3444 0 0 0 59955 24 0 0 25 0 1 0 1846606695 14979072 3386 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3657 3386 145 145 0 3512 0
[pid=5652] vsize: 14628
Current children cumulated CPU time (s) 599.8
Current children cumulated vsize (Kb) 16752

[startup+610.039 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3474 0 0 0 60955 24 0 0 25 0 1 0 1846606695 15097856 3416 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3686 3416 145 145 0 3541 0
[pid=5652] vsize: 14744
Current children cumulated CPU time (s) 609.8
Current children cumulated vsize (Kb) 16868

[startup+620.04 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3474 0 0 0 61955 24 0 0 25 0 1 0 1846606695 15097856 3416 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3686 3416 145 145 0 3541 0
[pid=5652] vsize: 14744
Current children cumulated CPU time (s) 619.8
Current children cumulated vsize (Kb) 16868

[startup+630.04 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3503 0 0 0 62955 24 0 0 25 0 1 0 1846606695 15261696 3445 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3726 3445 145 145 0 3581 0
[pid=5652] vsize: 14904
Current children cumulated CPU time (s) 629.8
Current children cumulated vsize (Kb) 17028

[startup+640.04 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3505 0 0 0 63955 24 0 0 25 0 1 0 1846606695 15261696 3447 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3726 3447 145 145 0 3581 0
[pid=5652] vsize: 14904
Current children cumulated CPU time (s) 639.8
Current children cumulated vsize (Kb) 17028

[startup+650.042 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3505 0 0 0 64956 24 0 0 25 0 1 0 1846606695 15261696 3447 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3726 3447 145 145 0 3581 0
[pid=5652] vsize: 14904
Current children cumulated CPU time (s) 649.81
Current children cumulated vsize (Kb) 17028

[startup+660.043 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3511 0 0 0 65956 24 0 0 25 0 1 0 1846606695 15294464 3453 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3734 3453 145 145 0 3589 0
[pid=5652] vsize: 14936
Current children cumulated CPU time (s) 659.81
Current children cumulated vsize (Kb) 17060

[startup+670.042 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3517 0 0 0 66956 24 0 0 25 0 1 0 1846606695 15360000 3459 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3750 3459 145 145 0 3605 0
[pid=5652] vsize: 15000
Current children cumulated CPU time (s) 669.81
Current children cumulated vsize (Kb) 17124

[startup+680.043 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3517 0 0 0 67956 24 0 0 25 0 1 0 1846606695 15360000 3459 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3750 3459 145 145 0 3605 0
[pid=5652] vsize: 15000
Current children cumulated CPU time (s) 679.81
Current children cumulated vsize (Kb) 17124

[startup+690.044 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3526 0 0 0 68957 24 0 0 25 0 1 0 1846606695 15425536 3468 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3766 3468 145 145 0 3621 0
[pid=5652] vsize: 15064
Current children cumulated CPU time (s) 689.82
Current children cumulated vsize (Kb) 17188

[startup+700.044 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3528 0 0 0 69957 24 0 0 25 0 1 0 1846606695 15425536 3470 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3766 3470 145 145 0 3621 0
[pid=5652] vsize: 15064
Current children cumulated CPU time (s) 699.82
Current children cumulated vsize (Kb) 17188

[startup+710.045 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3563 0 0 0 70957 24 0 0 25 0 1 0 1846606695 15552512 3505 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3797 3505 145 145 0 3652 0
[pid=5652] vsize: 15188
Current children cumulated CPU time (s) 709.82
Current children cumulated vsize (Kb) 17312

[startup+720.046 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3567 0 0 0 71957 24 0 0 25 0 1 0 1846606695 15552512 3509 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3797 3509 145 145 0 3652 0
[pid=5652] vsize: 15188
Current children cumulated CPU time (s) 719.82
Current children cumulated vsize (Kb) 17312

[startup+730.047 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3585 0 0 0 72957 25 0 0 25 0 1 0 1846606695 15650816 3527 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3821 3527 145 145 0 3676 0
[pid=5652] vsize: 15284
Current children cumulated CPU time (s) 729.83
Current children cumulated vsize (Kb) 17408

[startup+740.046 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3604 0 0 0 73957 25 0 0 25 0 1 0 1846606695 15781888 3546 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3853 3546 145 145 0 3708 0
[pid=5652] vsize: 15412
Current children cumulated CPU time (s) 739.83
Current children cumulated vsize (Kb) 17536

[startup+750.047 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3637 0 0 0 74957 25 0 0 25 0 1 0 1846606695 15921152 3579 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3887 3579 145 145 0 3742 0
[pid=5652] vsize: 15548
Current children cumulated CPU time (s) 749.83
Current children cumulated vsize (Kb) 17672

[startup+760.048 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3643 0 0 0 75957 25 0 0 25 0 1 0 1846606695 15953920 3585 4294967295 134512640 135094434 3221224432 3221223088 134557956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3895 3585 145 145 0 3750 0
[pid=5652] vsize: 15580
Current children cumulated CPU time (s) 759.83
Current children cumulated vsize (Kb) 17704

[startup+770.047 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3660 0 0 0 76957 25 0 0 25 0 1 0 1846606695 16052224 3602 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3919 3602 145 145 0 3774 0
[pid=5652] vsize: 15676
Current children cumulated CPU time (s) 769.83
Current children cumulated vsize (Kb) 17800

[startup+780.048 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3664 0 0 0 77957 25 0 0 25 0 1 0 1846606695 16052224 3606 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3919 3606 145 145 0 3774 0
[pid=5652] vsize: 15676
Current children cumulated CPU time (s) 779.83
Current children cumulated vsize (Kb) 17800

[startup+790.049 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3667 0 0 0 78957 25 0 0 25 0 1 0 1846606695 16068608 3609 4294967295 134512640 135094434 3221224432 3221223056 134557734 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3923 3609 145 145 0 3778 0
[pid=5652] vsize: 15692
Current children cumulated CPU time (s) 789.83
Current children cumulated vsize (Kb) 17816

[startup+800.05 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3672 0 0 0 79958 25 0 0 25 0 1 0 1846606695 16101376 3614 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3931 3614 145 145 0 3786 0
[pid=5652] vsize: 15724
Current children cumulated CPU time (s) 799.84
Current children cumulated vsize (Kb) 17848

[startup+810.05 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3677 0 0 0 80958 25 0 0 25 0 1 0 1846606695 16134144 3619 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3939 3619 145 145 0 3794 0
[pid=5652] vsize: 15756
Current children cumulated CPU time (s) 809.84
Current children cumulated vsize (Kb) 17880

[startup+820.051 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3677 0 0 0 81958 25 0 0 25 0 1 0 1846606695 16134144 3619 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3939 3619 145 145 0 3794 0
[pid=5652] vsize: 15756
Current children cumulated CPU time (s) 819.84
Current children cumulated vsize (Kb) 17880

[startup+830.052 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3677 0 0 0 82959 25 0 0 25 0 1 0 1846606695 16134144 3619 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3939 3619 145 145 0 3794 0
[pid=5652] vsize: 15756
Current children cumulated CPU time (s) 829.85
Current children cumulated vsize (Kb) 17880

[startup+840.052 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3678 0 0 0 83958 25 0 0 25 0 1 0 1846606695 16134144 3620 4294967295 134512640 135094434 3221224432 3221223056 134557655 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3939 3620 145 145 0 3794 0
[pid=5652] vsize: 15756
Current children cumulated CPU time (s) 839.84
Current children cumulated vsize (Kb) 17880

[startup+850.053 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3713 0 0 0 84958 25 0 0 25 0 1 0 1846606695 16281600 3655 4294967295 134512640 135094434 3221224432 3221223044 134563124 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 3975 3655 145 145 0 3830 0
[pid=5652] vsize: 15900
Current children cumulated CPU time (s) 849.84
Current children cumulated vsize (Kb) 18024

[startup+860.054 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3876 0 0 0 85955 27 0 0 25 0 1 0 1846606695 16941056 3818 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 4136 3818 145 145 0 3991 0
[pid=5652] vsize: 16544
Current children cumulated CPU time (s) 859.83
Current children cumulated vsize (Kb) 18668

[startup+870.054 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3889 0 0 0 86955 27 0 0 25 0 1 0 1846606695 17039360 3831 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 4160 3831 145 145 0 4015 0
[pid=5652] vsize: 16640
Current children cumulated CPU time (s) 869.83
Current children cumulated vsize (Kb) 18764

[startup+880.054 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3892 0 0 0 87956 27 0 0 25 0 1 0 1846606695 17039360 3834 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 4160 3834 145 145 0 4015 0
[pid=5652] vsize: 16640
Current children cumulated CPU time (s) 879.84
Current children cumulated vsize (Kb) 18764

[startup+890.055 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 3900 0 0 0 88956 27 0 0 25 0 1 0 1846606695 17039360 3842 4294967295 134512640 135094434 3221224432 3221223024 134551908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 4160 3842 145 145 0 4015 0
[pid=5652] vsize: 16640
Current children cumulated CPU time (s) 889.84
Current children cumulated vsize (Kb) 18764

[startup+900.056 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 4113 0 0 0 89952 29 0 0 25 0 1 0 1846606695 17944576 4055 4294967295 134512640 135094434 3221224432 3221223024 134551454 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 4381 4055 145 145 0 4236 0
[pid=5652] vsize: 17524
Current children cumulated CPU time (s) 899.82
Current children cumulated vsize (Kb) 19648

[startup+910.056 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 4125 0 0 0 90952 29 0 0 25 0 1 0 1846606695 18010112 4067 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 4397 4067 145 145 0 4252 0
[pid=5652] vsize: 17588
Current children cumulated CPU time (s) 909.82
Current children cumulated vsize (Kb) 19712

[startup+920.056 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 4128 0 0 0 91952 29 0 0 25 0 1 0 1846606695 18059264 4070 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 4409 4070 145 145 0 4264 0
[pid=5652] vsize: 17636
Current children cumulated CPU time (s) 919.82
Current children cumulated vsize (Kb) 19760

[startup+930.057 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 4137 0 0 0 92952 29 0 0 25 0 1 0 1846606695 18075648 4079 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 4413 4079 145 145 0 4268 0
[pid=5652] vsize: 17652
Current children cumulated CPU time (s) 929.82
Current children cumulated vsize (Kb) 19776

[startup+940.058 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 4138 0 0 0 93952 29 0 0 25 0 1 0 1846606695 18075648 4080 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 4413 4080 145 145 0 4268 0
[pid=5652] vsize: 17652
Current children cumulated CPU time (s) 939.82
Current children cumulated vsize (Kb) 19776

[startup+950.058 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 4140 0 0 0 94953 29 0 0 25 0 1 0 1846606695 18075648 4082 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 4413 4082 145 145 0 4268 0
[pid=5652] vsize: 17652
Current children cumulated CPU time (s) 949.83
Current children cumulated vsize (Kb) 19776

[startup+960.059 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 4140 0 0 0 95953 29 0 0 25 0 1 0 1846606695 18075648 4082 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 4413 4082 145 145 0 4268 0
[pid=5652] vsize: 17652
Current children cumulated CPU time (s) 959.83
Current children cumulated vsize (Kb) 19776

[startup+970.06 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 4145 0 0 0 96953 29 0 0 25 0 1 0 1846606695 18092032 4087 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 4417 4087 145 145 0 4272 0
[pid=5652] vsize: 17668
Current children cumulated CPU time (s) 969.83
Current children cumulated vsize (Kb) 19792

[startup+980.06 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 4159 0 0 0 97953 29 0 0 25 0 1 0 1846606695 18173952 4101 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 4437 4101 145 145 0 4292 0
[pid=5652] vsize: 17748
Current children cumulated CPU time (s) 979.83
Current children cumulated vsize (Kb) 19872

[startup+990.061 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 4159 0 0 0 98953 29 0 0 25 0 1 0 1846606695 18173952 4101 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 4437 4101 145 145 0 4292 0
[pid=5652] vsize: 17748
Current children cumulated CPU time (s) 989.83
Current children cumulated vsize (Kb) 19872

[startup+1000.06 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 4159 0 0 0 99954 29 0 0 25 0 1 0 1846606695 18173952 4101 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 4437 4101 145 145 0 4292 0
[pid=5652] vsize: 17748
Current children cumulated CPU time (s) 999.84
Current children cumulated vsize (Kb) 19872

[startup+1010.06 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 4166 0 0 0 100954 29 0 0 25 0 1 0 1846606695 18206720 4108 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 4445 4108 145 145 0 4300 0
[pid=5652] vsize: 17780
Current children cumulated CPU time (s) 1009.84
Current children cumulated vsize (Kb) 19904

[startup+1020.06 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 4178 0 0 0 101954 29 0 0 25 0 1 0 1846606695 18272256 4120 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 4461 4120 145 145 0 4316 0
[pid=5652] vsize: 17844
Current children cumulated CPU time (s) 1019.84
Current children cumulated vsize (Kb) 19968

[startup+1030.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 4178 0 0 0 102954 29 0 0 25 0 1 0 1846606695 18272256 4120 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 4461 4120 145 145 0 4316 0
[pid=5652] vsize: 17844
Current children cumulated CPU time (s) 1029.84
Current children cumulated vsize (Kb) 19968

[startup+1040.06 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 4183 0 0 0 103954 29 0 0 25 0 1 0 1846606695 18305024 4125 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 4469 4125 145 145 0 4324 0
[pid=5652] vsize: 17876
Current children cumulated CPU time (s) 1039.84
Current children cumulated vsize (Kb) 20000

[startup+1050.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 4188 0 0 0 104955 29 0 0 25 0 1 0 1846606695 18337792 4130 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 4477 4130 145 145 0 4332 0
[pid=5652] vsize: 17908
Current children cumulated CPU time (s) 1049.85
Current children cumulated vsize (Kb) 20032

[startup+1060.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 4197 0 0 0 105955 29 0 0 25 0 1 0 1846606695 18403328 4139 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 4493 4139 145 145 0 4348 0
[pid=5652] vsize: 17972
Current children cumulated CPU time (s) 1059.85
Current children cumulated vsize (Kb) 20096

[startup+1070.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 4200 0 0 0 106955 29 0 0 25 0 1 0 1846606695 18403328 4142 4294967295 134512640 135094434 3221224432 3221223024 134551434 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 4493 4142 145 145 0 4348 0
[pid=5652] vsize: 17972
Current children cumulated CPU time (s) 1069.85
Current children cumulated vsize (Kb) 20096

[startup+1080.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 4200 0 0 0 107955 29 0 0 25 0 1 0 1846606695 18403328 4142 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 4493 4142 145 145 0 4348 0
[pid=5652] vsize: 17972
Current children cumulated CPU time (s) 1079.85
Current children cumulated vsize (Kb) 20096

[startup+1090.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 4200 0 0 0 108955 29 0 0 25 0 1 0 1846606695 18403328 4142 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 4493 4142 145 145 0 4348 0
[pid=5652] vsize: 17972
Current children cumulated CPU time (s) 1089.85
Current children cumulated vsize (Kb) 20096

[startup+1100.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 4200 0 0 0 109956 29 0 0 25 0 1 0 1846606695 18403328 4142 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 4493 4142 145 145 0 4348 0
[pid=5652] vsize: 17972
Current children cumulated CPU time (s) 1099.86
Current children cumulated vsize (Kb) 20096

[startup+1110.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 4200 0 0 0 110956 29 0 0 25 0 1 0 1846606695 18403328 4142 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 4493 4142 145 145 0 4348 0
[pid=5652] vsize: 17972
Current children cumulated CPU time (s) 1109.86
Current children cumulated vsize (Kb) 20096

[startup+1120.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 4203 0 0 0 111956 29 0 0 25 0 1 0 1846606695 18403328 4145 4294967295 134512640 135094434 3221224432 3221223104 134556478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 4493 4145 145 145 0 4348 0
[pid=5652] vsize: 17972
Current children cumulated CPU time (s) 1119.86
Current children cumulated vsize (Kb) 20096

[startup+1130.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 4203 0 0 0 112956 29 0 0 25 0 1 0 1846606695 18403328 4145 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 4493 4145 145 145 0 4348 0
[pid=5652] vsize: 17972
Current children cumulated CPU time (s) 1129.86
Current children cumulated vsize (Kb) 20096

[startup+1140.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 4203 0 0 0 113957 29 0 0 25 0 1 0 1846606695 18403328 4145 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 4493 4145 145 145 0 4348 0
[pid=5652] vsize: 17972
Current children cumulated CPU time (s) 1139.87
Current children cumulated vsize (Kb) 20096

[startup+1150.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 4203 0 0 0 114957 29 0 0 25 0 1 0 1846606695 18403328 4145 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 4493 4145 145 145 0 4348 0
[pid=5652] vsize: 17972
Current children cumulated CPU time (s) 1149.87
Current children cumulated vsize (Kb) 20096

[startup+1160.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 4203 0 0 0 115957 29 0 0 25 0 1 0 1846606695 18403328 4145 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 4493 4145 145 145 0 4348 0
[pid=5652] vsize: 17972
Current children cumulated CPU time (s) 1159.87
Current children cumulated vsize (Kb) 20096

[startup+1170.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 4203 0 0 0 116957 29 0 0 25 0 1 0 1846606695 18403328 4145 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 4493 4145 145 145 0 4348 0
[pid=5652] vsize: 17972
Current children cumulated CPU time (s) 1169.87
Current children cumulated vsize (Kb) 20096

[startup+1180.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 4203 0 0 0 117958 29 0 0 25 0 1 0 1846606695 18403328 4145 4294967295 134512640 135094434 3221224432 3221223104 134556257 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 4493 4145 145 145 0 4348 0
[pid=5652] vsize: 17972
Current children cumulated CPU time (s) 1179.88
Current children cumulated vsize (Kb) 20096

[startup+1190.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 4203 0 0 0 118958 29 0 0 25 0 1 0 1846606695 18403328 4145 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 4493 4145 145 145 0 4348 0
[pid=5652] vsize: 17972
Current children cumulated CPU time (s) 1189.88
Current children cumulated vsize (Kb) 20096

[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 4254 0 0 0 119957 30 0 0 25 0 1 0 1846606695 18620416 4196 4294967295 134512640 135094434 3221224432 3221223024 134551434 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 4546 4196 145 145 0 4401 0
[pid=5652] vsize: 18184
Current children cumulated CPU time (s) 1199.88
Current children cumulated vsize (Kb) 20308

[startup+1210.08 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 4254 0 0 0 120957 30 0 0 25 0 1 0 1846606695 18620416 4196 4294967295 134512640 135094434 3221224432 3221223088 134557972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 4546 4196 145 145 0 4401 0
[pid=5652] vsize: 18184
Current children cumulated CPU time (s) 1209.88
Current children cumulated vsize (Kb) 20308



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.08 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5652
Raw data (/proc/5648/stat): 5648 (minisat+_script) S 5647 5648 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846606690 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5648/statm): 531 226 485 147 0 384 0
[pid=5648] vsize: 2124
Raw data (/proc/5652/stat): 5652 (minisat+_64-bit) R 5648 5648 21452 0 -1 0 4254 0 0 0 120957 30 0 0 25 0 1 0 1846606695 18620416 4196 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5652/statm): 4546 4196 145 145 0 4401 0
[pid=5652] vsize: 18184
Current children cumulated CPU time (s) 1209.88
Current children cumulated vsize (Kb) 20308

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

Child status: 0
Real time (s): 1210.09
CPU time (s): 1209.89
CPU user time (s): 1209.58
CPU system time (s): 0.309952
CPU usage (%): 99.9835
Max. virtual memory (cumulated for all children) (Kb): 20308

Verifier Data

ERROR: no interpretation found !