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/miplib3/normalized-mps-v2-20-10-p0548.opb
MD5SUM10547c6c0f11ab5df74fcaff6ba6d160
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.09
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 4542

Launcher Data

LAUNCH ON wulflinc21 THE 2005-09-19 18:06:10 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2998 boxname=wulflinc21 idbench=654 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  10547c6c0f11ab5df74fcaff6ba6d160  /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-p0548.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-p0548.opb
IDLAUNCH: 2998
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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.161
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:        889752 kB
Buffers:         33384 kB
Cached:          84056 kB
SwapCached:        812 kB
Active:          62516 kB
Inactive:        57568 kB
HighTotal:      131008 kB
HighFree:        46564 kB
LowTotal:       903652 kB
LowFree:        843188 kB
SwapTotal:     2097892 kB
SwapFree:      2096456 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5708 kB
Slab:            19024 kB
Committed_AS:    64352 kB
PageTables:        340 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-19 18:26:20 (client local time) WITH STATUS 0 IN 1209.89 SECONDS
stats: 2998 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/4763/stat): 4763 (minisat+_script) R 4762 4763 20602 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1729193824 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/4763/statm): 174 3 169 147 0 27 0
[pid=4763] 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=4764
New process pid=4765
New process pid=4766
execve syscall for /bin/sed executable
One traced child (pid=4765) 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=4766) exited with status: 0
One traced child (pid=4764) exited with status: 0
New process pid=4767
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-p0548.opb

[startup+10.003 s]
Raw data (loadavg): 0.93 0.95 0.88 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 1420 0 0 0 979 7 0 0 25 0 1 0 1729193829 6131712 1362 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4767/statm): 1497 1362 145 145 0 1352 0
[pid=4767] vsize: 5988
Current children cumulated CPU time (s) 9.87
Current children cumulated vsize (Kb) 8112

[startup+20.0046 s]
Raw data (loadavg): 0.94 0.96 0.88 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 1574 0 0 0 1976 8 0 0 25 0 1 0 1729193829 6754304 1516 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 1649 1516 145 145 0 1504 0
[pid=4767] vsize: 6596
Current children cumulated CPU time (s) 19.85
Current children cumulated vsize (Kb) 8720

[startup+30.0053 s]
Raw data (loadavg): 0.95 0.96 0.88 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 1770 0 0 0 2972 11 0 0 25 0 1 0 1729193829 7561216 1712 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 1846 1712 145 145 0 1701 0
[pid=4767] vsize: 7384
Current children cumulated CPU time (s) 29.84
Current children cumulated vsize (Kb) 9508

[startup+40.005 s]
Raw data (loadavg): 0.95 0.96 0.88 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 2013 0 0 0 3968 13 0 0 25 0 1 0 1729193829 8556544 1955 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 2089 1955 145 145 0 1944 0
[pid=4767] vsize: 8356
Current children cumulated CPU time (s) 39.82
Current children cumulated vsize (Kb) 10480

[startup+50.0056 s]
Raw data (loadavg): 0.96 0.96 0.88 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 2201 0 0 0 4964 14 0 0 25 0 1 0 1729193829 9326592 2143 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 2277 2143 145 145 0 2132 0
[pid=4767] vsize: 9108
Current children cumulated CPU time (s) 49.79
Current children cumulated vsize (Kb) 11232

[startup+60.0053 s]
Raw data (loadavg): 0.97 0.96 0.88 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 2240 0 0 0 5963 15 0 0 25 0 1 0 1729193829 9523200 2182 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 2325 2182 145 145 0 2180 0
[pid=4767] vsize: 9300
Current children cumulated CPU time (s) 59.79
Current children cumulated vsize (Kb) 11424

[startup+70.006 s]
Raw data (loadavg): 0.97 0.96 0.89 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 2252 0 0 0 6963 15 0 0 25 0 1 0 1729193829 9572352 2194 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 2337 2194 145 145 0 2192 0
[pid=4767] vsize: 9348
Current children cumulated CPU time (s) 69.79
Current children cumulated vsize (Kb) 11472

[startup+80.0067 s]
Raw data (loadavg): 0.98 0.96 0.89 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 2280 0 0 0 7963 15 0 0 25 0 1 0 1729193829 9719808 2222 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 2373 2222 145 145 0 2228 0
[pid=4767] vsize: 9492
Current children cumulated CPU time (s) 79.79
Current children cumulated vsize (Kb) 11616

[startup+90.0064 s]
Raw data (loadavg): 0.98 0.96 0.89 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 2285 0 0 0 8963 15 0 0 25 0 1 0 1729193829 9736192 2227 4294967295 134512640 135094434 3221224432 3221223024 134551454 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 2377 2227 145 145 0 2232 0
[pid=4767] vsize: 9508
Current children cumulated CPU time (s) 89.79
Current children cumulated vsize (Kb) 11632

[startup+100.007 s]
Raw data (loadavg): 0.98 0.96 0.89 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 2303 0 0 0 9963 15 0 0 25 0 1 0 1729193829 9818112 2245 4294967295 134512640 135094434 3221224432 3221223120 134554687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4767/statm): 2397 2245 145 145 0 2252 0
[pid=4767] vsize: 9588
Current children cumulated CPU time (s) 99.79
Current children cumulated vsize (Kb) 11712

[startup+110.008 s]
Raw data (loadavg): 0.98 0.96 0.89 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 2326 0 0 0 10963 15 0 0 25 0 1 0 1729193829 9895936 2268 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 2416 2268 145 145 0 2271 0
[pid=4767] vsize: 9664
Current children cumulated CPU time (s) 109.79
Current children cumulated vsize (Kb) 11788

[startup+120.008 s]
Raw data (loadavg): 0.99 0.97 0.89 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 2366 0 0 0 11962 16 0 0 25 0 1 0 1729193829 10063872 2308 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 2457 2308 145 145 0 2312 0
[pid=4767] vsize: 9828
Current children cumulated CPU time (s) 119.79
Current children cumulated vsize (Kb) 11952

[startup+130.009 s]
Raw data (loadavg): 0.99 0.97 0.89 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 2410 0 0 0 12961 16 0 0 25 0 1 0 1729193829 10244096 2352 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 2501 2352 145 145 0 2356 0
[pid=4767] vsize: 10004
Current children cumulated CPU time (s) 129.78
Current children cumulated vsize (Kb) 12128

[startup+140.009 s]
Raw data (loadavg): 0.99 0.97 0.89 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 2538 0 0 0 13959 18 0 0 25 0 1 0 1729193829 10780672 2480 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 2632 2480 145 145 0 2487 0
[pid=4767] 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.89 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 2552 0 0 0 14958 19 0 0 25 0 1 0 1729193829 10838016 2494 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 2646 2494 145 145 0 2501 0
[pid=4767] vsize: 10584
Current children cumulated CPU time (s) 149.78
Current children cumulated vsize (Kb) 12708

[startup+160.012 s]
Raw data (loadavg): 0.99 0.97 0.89 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 2731 0 0 0 15955 20 0 0 25 0 1 0 1729193829 11608064 2673 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 2834 2673 145 145 0 2689 0
[pid=4767] vsize: 11336
Current children cumulated CPU time (s) 159.76
Current children cumulated vsize (Kb) 13460

[startup+170.013 s]
Raw data (loadavg): 0.99 0.97 0.90 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 2741 0 0 0 16955 21 0 0 25 0 1 0 1729193829 11673600 2683 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 2850 2683 145 145 0 2705 0
[pid=4767] vsize: 11400
Current children cumulated CPU time (s) 169.77
Current children cumulated vsize (Kb) 13524

[startup+180.013 s]
Raw data (loadavg): 0.99 0.97 0.90 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 2853 0 0 0 17954 21 0 0 25 0 1 0 1729193829 12259328 2795 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 2993 2795 145 145 0 2848 0
[pid=4767] vsize: 11972
Current children cumulated CPU time (s) 179.76
Current children cumulated vsize (Kb) 14096

[startup+190.014 s]
Raw data (loadavg): 0.99 0.97 0.90 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 2870 0 0 0 18954 21 0 0 25 0 1 0 1729193829 12341248 2812 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3013 2812 145 145 0 2868 0
[pid=4767] vsize: 12052
Current children cumulated CPU time (s) 189.76
Current children cumulated vsize (Kb) 14176

[startup+200.015 s]
Raw data (loadavg): 0.99 0.97 0.90 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 2877 0 0 0 19953 22 0 0 25 0 1 0 1729193829 12374016 2819 4294967295 134512640 135094434 3221224432 3221223024 134551469 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3021 2819 145 145 0 2876 0
[pid=4767] 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.90 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 2883 0 0 0 20953 22 0 0 25 0 1 0 1729193829 12406784 2825 4294967295 134512640 135094434 3221224432 3221223040 134785094 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3029 2825 145 145 0 2884 0
[pid=4767] vsize: 12116
Current children cumulated CPU time (s) 209.76
Current children cumulated vsize (Kb) 14240

[startup+220.016 s]
Raw data (loadavg): 0.99 0.97 0.90 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 2894 0 0 0 21953 22 0 0 25 0 1 0 1729193829 12472320 2836 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3045 2836 145 145 0 2900 0
[pid=4767] 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.90 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 2919 0 0 0 22953 23 0 0 25 0 1 0 1729193829 12591104 2861 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3074 2861 145 145 0 2929 0
[pid=4767] vsize: 12296
Current children cumulated CPU time (s) 229.77
Current children cumulated vsize (Kb) 14420

[startup+240.017 s]
Raw data (loadavg): 0.99 0.97 0.90 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 2923 0 0 0 23953 23 0 0 25 0 1 0 1729193829 12599296 2865 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3076 2865 145 145 0 2931 0
[pid=4767] vsize: 12304
Current children cumulated CPU time (s) 239.77
Current children cumulated vsize (Kb) 14428

[startup+250.017 s]
Raw data (loadavg): 0.99 0.97 0.90 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 2948 0 0 0 24953 23 0 0 25 0 1 0 1729193829 12730368 2890 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3108 2890 145 145 0 2963 0
[pid=4767] vsize: 12432
Current children cumulated CPU time (s) 249.77
Current children cumulated vsize (Kb) 14556

[startup+260.018 s]
Raw data (loadavg): 0.99 0.97 0.90 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 2966 0 0 0 25953 23 0 0 25 0 1 0 1729193829 12804096 2908 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3126 2908 145 145 0 2981 0
[pid=4767] 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.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 2981 0 0 0 26953 24 0 0 25 0 1 0 1729193829 12886016 2923 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3146 2923 145 145 0 3001 0
[pid=4767] vsize: 12584
Current children cumulated CPU time (s) 269.78
Current children cumulated vsize (Kb) 14708

[startup+280.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 2995 0 0 0 27953 24 0 0 25 0 1 0 1729193829 12951552 2937 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3162 2937 145 145 0 3017 0
[pid=4767] vsize: 12648
Current children cumulated CPU time (s) 279.78
Current children cumulated vsize (Kb) 14772

[startup+290.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 2995 0 0 0 28953 24 0 0 25 0 1 0 1729193829 12951552 2937 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3162 2937 145 145 0 3017 0
[pid=4767] vsize: 12648
Current children cumulated CPU time (s) 289.78
Current children cumulated vsize (Kb) 14772

[startup+300.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 2995 0 0 0 29953 24 0 0 25 0 1 0 1729193829 12951552 2937 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3162 2937 145 145 0 3017 0
[pid=4767] vsize: 12648
Current children cumulated CPU time (s) 299.78
Current children cumulated vsize (Kb) 14772

[startup+310.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3016 0 0 0 30952 24 0 0 25 0 1 0 1729193829 13049856 2958 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4767/statm): 3186 2958 145 145 0 3041 0
[pid=4767] vsize: 12744
Current children cumulated CPU time (s) 309.77
Current children cumulated vsize (Kb) 14868

[startup+320.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3032 0 0 0 31952 25 0 0 25 0 1 0 1729193829 13115392 2974 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4767/statm): 3202 2974 145 145 0 3057 0
[pid=4767] 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.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3051 0 0 0 32951 25 0 0 25 0 1 0 1729193829 13197312 2993 4294967295 134512640 135094434 3221224432 3221223024 134557044 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4767/statm): 3222 2993 145 145 0 3077 0
[pid=4767] vsize: 12888
Current children cumulated CPU time (s) 329.77
Current children cumulated vsize (Kb) 15012

[startup+340.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3051 0 0 0 33951 25 0 0 25 0 1 0 1729193829 13197312 2993 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4767/statm): 3222 2993 145 145 0 3077 0
[pid=4767] vsize: 12888
Current children cumulated CPU time (s) 339.77
Current children cumulated vsize (Kb) 15012

[startup+350.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3060 0 0 0 34951 25 0 0 25 0 1 0 1729193829 13262848 3002 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4767/statm): 3238 3002 145 145 0 3093 0
[pid=4767] vsize: 12952
Current children cumulated CPU time (s) 349.77
Current children cumulated vsize (Kb) 15076

[startup+360.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3070 0 0 0 35951 25 0 0 25 0 1 0 1729193829 13328384 3012 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4767/statm): 3254 3012 145 145 0 3109 0
[pid=4767] vsize: 13016
Current children cumulated CPU time (s) 359.77
Current children cumulated vsize (Kb) 15140

[startup+370.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3070 0 0 0 36951 25 0 0 25 0 1 0 1729193829 13328384 3012 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4767/statm): 3254 3012 145 145 0 3109 0
[pid=4767] vsize: 13016
Current children cumulated CPU time (s) 369.77
Current children cumulated vsize (Kb) 15140

[startup+380.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3070 0 0 0 37951 26 0 0 25 0 1 0 1729193829 13328384 3012 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4767/statm): 3254 3012 145 145 0 3109 0
[pid=4767] vsize: 13016
Current children cumulated CPU time (s) 379.78
Current children cumulated vsize (Kb) 15140

[startup+390.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3070 0 0 0 38951 26 0 0 25 0 1 0 1729193829 13328384 3012 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4767/statm): 3254 3012 145 145 0 3109 0
[pid=4767] vsize: 13016
Current children cumulated CPU time (s) 389.78
Current children cumulated vsize (Kb) 15140

[startup+400.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3072 0 0 0 39951 26 0 0 25 0 1 0 1729193829 13328384 3014 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4767/statm): 3254 3014 145 145 0 3109 0
[pid=4767] vsize: 13016
Current children cumulated CPU time (s) 399.78
Current children cumulated vsize (Kb) 15140

[startup+410.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3072 0 0 0 40951 26 0 0 25 0 1 0 1729193829 13328384 3014 4294967295 134512640 135094434 3221224432 3221223088 134557914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4767/statm): 3254 3014 145 145 0 3109 0
[pid=4767] vsize: 13016
Current children cumulated CPU time (s) 409.78
Current children cumulated vsize (Kb) 15140

[startup+420.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3136 0 0 0 41950 27 0 0 25 0 1 0 1729193829 13590528 3078 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4767/statm): 3318 3078 145 145 0 3173 0
[pid=4767] vsize: 13272
Current children cumulated CPU time (s) 419.78
Current children cumulated vsize (Kb) 15396

[startup+430.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3149 0 0 0 42950 27 0 0 25 0 1 0 1729193829 13672448 3091 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3338 3091 145 145 0 3193 0
[pid=4767] vsize: 13352
Current children cumulated CPU time (s) 429.78
Current children cumulated vsize (Kb) 15476

[startup+440.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3167 0 0 0 43950 27 0 0 25 0 1 0 1729193829 13733888 3109 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3353 3109 145 145 0 3208 0
[pid=4767] vsize: 13412
Current children cumulated CPU time (s) 439.78
Current children cumulated vsize (Kb) 15536

[startup+450.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3180 0 0 0 44950 27 0 0 25 0 1 0 1729193829 13799424 3122 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3369 3122 145 145 0 3224 0
[pid=4767] vsize: 13476
Current children cumulated CPU time (s) 449.78
Current children cumulated vsize (Kb) 15600

[startup+460.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3185 0 0 0 45951 27 0 0 25 0 1 0 1729193829 13815808 3127 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3373 3127 145 145 0 3228 0
[pid=4767] vsize: 13492
Current children cumulated CPU time (s) 459.79
Current children cumulated vsize (Kb) 15616

[startup+470.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3202 0 0 0 46950 27 0 0 25 0 1 0 1729193829 13914112 3144 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3397 3144 145 145 0 3252 0
[pid=4767] vsize: 13588
Current children cumulated CPU time (s) 469.78
Current children cumulated vsize (Kb) 15712

[startup+480.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3212 0 0 0 47950 27 0 0 25 0 1 0 1729193829 13979648 3154 4294967295 134512640 135094434 3221224432 3221223024 134557227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3413 3154 145 145 0 3268 0
[pid=4767] vsize: 13652
Current children cumulated CPU time (s) 479.78
Current children cumulated vsize (Kb) 15776

[startup+490.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3213 0 0 0 48950 28 0 0 25 0 1 0 1729193829 13979648 3155 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3413 3155 145 145 0 3268 0
[pid=4767] vsize: 13652
Current children cumulated CPU time (s) 489.79
Current children cumulated vsize (Kb) 15776

[startup+500.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3236 0 0 0 49951 28 0 0 25 0 1 0 1729193829 14077952 3178 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3437 3178 145 145 0 3292 0
[pid=4767] vsize: 13748
Current children cumulated CPU time (s) 499.8
Current children cumulated vsize (Kb) 15872

[startup+510.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3239 0 0 0 50950 28 0 0 25 0 1 0 1729193829 14143488 3181 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3453 3181 145 145 0 3308 0
[pid=4767] vsize: 13812
Current children cumulated CPU time (s) 509.79
Current children cumulated vsize (Kb) 15936

[startup+520.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3243 0 0 0 51951 28 0 0 25 0 1 0 1729193829 14143488 3185 4294967295 134512640 135094434 3221224432 3221223088 134558289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3453 3185 145 145 0 3308 0
[pid=4767] 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.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3258 0 0 0 52951 28 0 0 25 0 1 0 1729193829 14192640 3200 4294967295 134512640 135094434 3221224432 3221223104 134555232 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3465 3200 145 145 0 3320 0
[pid=4767] vsize: 13860
Current children cumulated CPU time (s) 529.8
Current children cumulated vsize (Kb) 15984

[startup+540.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3311 0 0 0 53950 28 0 0 25 0 1 0 1729193829 14401536 3253 4294967295 134512640 135094434 3221224432 3221223088 134558011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3516 3253 145 145 0 3371 0
[pid=4767] vsize: 14064
Current children cumulated CPU time (s) 539.79
Current children cumulated vsize (Kb) 16188

[startup+550.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3327 0 0 0 54950 29 0 0 25 0 1 0 1729193829 14467072 3269 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3532 3269 145 145 0 3387 0
[pid=4767] vsize: 14128
Current children cumulated CPU time (s) 549.8
Current children cumulated vsize (Kb) 16252

[startup+560.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3341 0 0 0 55950 29 0 0 25 0 1 0 1729193829 14548992 3283 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3552 3283 145 145 0 3407 0
[pid=4767] vsize: 14208
Current children cumulated CPU time (s) 559.8
Current children cumulated vsize (Kb) 16332

[startup+570.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3428 0 0 0 56949 29 0 0 25 0 1 0 1729193829 14913536 3370 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3641 3370 145 145 0 3496 0
[pid=4767] vsize: 14564
Current children cumulated CPU time (s) 569.79
Current children cumulated vsize (Kb) 16688

[startup+580.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3435 0 0 0 57950 29 0 0 25 0 1 0 1729193829 14946304 3377 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3649 3377 145 145 0 3504 0
[pid=4767] vsize: 14596
Current children cumulated CPU time (s) 579.8
Current children cumulated vsize (Kb) 16720

[startup+590.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3440 0 0 0 58950 29 0 0 25 0 1 0 1729193829 14962688 3382 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3653 3382 145 145 0 3508 0
[pid=4767] vsize: 14612
Current children cumulated CPU time (s) 589.8
Current children cumulated vsize (Kb) 16736

[startup+600.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3474 0 0 0 59949 30 0 0 25 0 1 0 1729193829 15097856 3416 4294967295 134512640 135094434 3221224432 3221223024 134551428 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3686 3416 145 145 0 3541 0
[pid=4767] vsize: 14744
Current children cumulated CPU time (s) 599.8
Current children cumulated vsize (Kb) 16868

[startup+610.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3474 0 0 0 60949 30 0 0 25 0 1 0 1729193829 15097856 3416 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3686 3416 145 145 0 3541 0
[pid=4767] vsize: 14744
Current children cumulated CPU time (s) 609.8
Current children cumulated vsize (Kb) 16868

[startup+620.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3474 0 0 0 61950 30 0 0 25 0 1 0 1729193829 15097856 3416 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3686 3416 145 145 0 3541 0
[pid=4767] vsize: 14744
Current children cumulated CPU time (s) 619.81
Current children cumulated vsize (Kb) 16868

[startup+630.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3504 0 0 0 62949 30 0 0 25 0 1 0 1729193829 15261696 3446 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3726 3446 145 145 0 3581 0
[pid=4767] vsize: 14904
Current children cumulated CPU time (s) 629.8
Current children cumulated vsize (Kb) 17028

[startup+640.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3505 0 0 0 63949 30 0 0 25 0 1 0 1729193829 15261696 3447 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3726 3447 145 145 0 3581 0
[pid=4767] vsize: 14904
Current children cumulated CPU time (s) 639.8
Current children cumulated vsize (Kb) 17028

[startup+650.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3505 0 0 0 64950 30 0 0 25 0 1 0 1729193829 15261696 3447 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3726 3447 145 145 0 3581 0
[pid=4767] vsize: 14904
Current children cumulated CPU time (s) 649.81
Current children cumulated vsize (Kb) 17028

[startup+660.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3516 0 0 0 65950 31 0 0 25 0 1 0 1729193829 15360000 3458 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3750 3458 145 145 0 3605 0
[pid=4767] vsize: 15000
Current children cumulated CPU time (s) 659.82
Current children cumulated vsize (Kb) 17124

[startup+670.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3517 0 0 0 66950 31 0 0 25 0 1 0 1729193829 15360000 3459 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3750 3459 145 145 0 3605 0
[pid=4767] vsize: 15000
Current children cumulated CPU time (s) 669.82
Current children cumulated vsize (Kb) 17124

[startup+680.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3524 0 0 0 67950 31 0 0 25 0 1 0 1729193829 15360000 3466 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3750 3466 145 145 0 3605 0
[pid=4767] vsize: 15000
Current children cumulated CPU time (s) 679.82
Current children cumulated vsize (Kb) 17124

[startup+690.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3527 0 0 0 68950 31 0 0 25 0 1 0 1729193829 15425536 3469 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3766 3469 145 145 0 3621 0
[pid=4767] vsize: 15064
Current children cumulated CPU time (s) 689.82
Current children cumulated vsize (Kb) 17188

[startup+700.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3560 0 0 0 69950 31 0 0 25 0 1 0 1729193829 15536128 3502 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3793 3502 145 145 0 3648 0
[pid=4767] vsize: 15172
Current children cumulated CPU time (s) 699.82
Current children cumulated vsize (Kb) 17296

[startup+710.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3566 0 0 0 70949 32 0 0 25 0 1 0 1729193829 15552512 3508 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3797 3508 145 145 0 3652 0
[pid=4767] vsize: 15188
Current children cumulated CPU time (s) 709.82
Current children cumulated vsize (Kb) 17312

[startup+720.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3574 0 0 0 71949 32 0 0 25 0 1 0 1729193829 15585280 3516 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3805 3516 145 145 0 3660 0
[pid=4767] vsize: 15220
Current children cumulated CPU time (s) 719.82
Current children cumulated vsize (Kb) 17344

[startup+730.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3604 0 0 0 72950 32 0 0 25 0 1 0 1729193829 15781888 3546 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3853 3546 145 145 0 3708 0
[pid=4767] vsize: 15412
Current children cumulated CPU time (s) 729.83
Current children cumulated vsize (Kb) 17536

[startup+740.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3636 0 0 0 73948 33 0 0 25 0 1 0 1729193829 15921152 3578 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3887 3578 145 145 0 3742 0
[pid=4767] vsize: 15548
Current children cumulated CPU time (s) 739.82
Current children cumulated vsize (Kb) 17672

[startup+750.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3640 0 0 0 74948 34 0 0 25 0 1 0 1729193829 15937536 3582 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3891 3582 145 145 0 3746 0
[pid=4767] vsize: 15564
Current children cumulated CPU time (s) 749.83
Current children cumulated vsize (Kb) 17688

[startup+760.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3660 0 0 0 75948 34 0 0 25 0 1 0 1729193829 16052224 3602 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3919 3602 145 145 0 3774 0
[pid=4767] vsize: 15676
Current children cumulated CPU time (s) 759.83
Current children cumulated vsize (Kb) 17800

[startup+770.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3663 0 0 0 76947 35 0 0 25 0 1 0 1729193829 16052224 3605 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3919 3605 145 145 0 3774 0
[pid=4767] 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.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3667 0 0 0 77947 35 0 0 25 0 1 0 1729193829 16068608 3609 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3923 3609 145 145 0 3778 0
[pid=4767] vsize: 15692
Current children cumulated CPU time (s) 779.83
Current children cumulated vsize (Kb) 17816

[startup+790.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3672 0 0 0 78947 35 0 0 25 0 1 0 1729193829 16101376 3614 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3931 3614 145 145 0 3786 0
[pid=4767] vsize: 15724
Current children cumulated CPU time (s) 789.83
Current children cumulated vsize (Kb) 17848

[startup+800.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3672 0 0 0 79947 35 0 0 25 0 1 0 1729193829 16101376 3614 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3931 3614 145 145 0 3786 0
[pid=4767] vsize: 15724
Current children cumulated CPU time (s) 799.83
Current children cumulated vsize (Kb) 17848

[startup+810.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3677 0 0 0 80947 36 0 0 25 0 1 0 1729193829 16134144 3619 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3939 3619 145 145 0 3794 0
[pid=4767] vsize: 15756
Current children cumulated CPU time (s) 809.84
Current children cumulated vsize (Kb) 17880

[startup+820.05 s]
Raw data (loadavg): 1.07 0.99 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3677 0 0 0 81947 36 0 0 25 0 1 0 1729193829 16134144 3619 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3939 3619 145 145 0 3794 0
[pid=4767] vsize: 15756
Current children cumulated CPU time (s) 819.84
Current children cumulated vsize (Kb) 17880

[startup+830.051 s]
Raw data (loadavg): 1.06 0.99 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3678 0 0 0 82947 36 0 0 25 0 1 0 1729193829 16134144 3620 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3939 3620 145 145 0 3794 0
[pid=4767] vsize: 15756
Current children cumulated CPU time (s) 829.84
Current children cumulated vsize (Kb) 17880

[startup+840.05 s]
Raw data (loadavg): 1.05 0.99 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3678 0 0 0 83947 36 0 0 25 0 1 0 1729193829 16134144 3620 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 3939 3620 145 145 0 3794 0
[pid=4767] vsize: 15756
Current children cumulated CPU time (s) 839.84
Current children cumulated vsize (Kb) 17880

[startup+850.051 s]
Raw data (loadavg): 1.04 0.99 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3876 0 0 0 84944 37 0 0 25 0 1 0 1729193829 16941056 3818 4294967295 134512640 135094434 3221224432 3221223024 134557334 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 4136 3818 145 145 0 3991 0
[pid=4767] vsize: 16544
Current children cumulated CPU time (s) 849.82
Current children cumulated vsize (Kb) 18668

[startup+860.051 s]
Raw data (loadavg): 1.04 0.99 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3888 0 0 0 85944 38 0 0 25 0 1 0 1729193829 17039360 3830 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 4160 3830 145 145 0 4015 0
[pid=4767] vsize: 16640
Current children cumulated CPU time (s) 859.83
Current children cumulated vsize (Kb) 18764

[startup+870.051 s]
Raw data (loadavg): 1.03 0.99 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3891 0 0 0 86944 38 0 0 25 0 1 0 1729193829 17039360 3833 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 4160 3833 145 145 0 4015 0
[pid=4767] vsize: 16640
Current children cumulated CPU time (s) 869.83
Current children cumulated vsize (Kb) 18764

[startup+880.052 s]
Raw data (loadavg): 1.03 0.99 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 3900 0 0 0 87944 38 0 0 25 0 1 0 1729193829 17039360 3842 4294967295 134512640 135094434 3221224432 3221222992 134550337 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 4160 3842 145 145 0 4015 0
[pid=4767] vsize: 16640
Current children cumulated CPU time (s) 879.83
Current children cumulated vsize (Kb) 18764

[startup+890.052 s]
Raw data (loadavg): 1.02 0.99 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 4086 0 0 0 88941 39 0 0 25 0 1 0 1729193829 17809408 4028 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 4348 4028 145 145 0 4203 0
[pid=4767] vsize: 17392
Current children cumulated CPU time (s) 889.81
Current children cumulated vsize (Kb) 19516

[startup+900.052 s]
Raw data (loadavg): 1.02 0.99 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 4124 0 0 0 89941 39 0 0 25 0 1 0 1729193829 18010112 4066 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 4397 4066 145 145 0 4252 0
[pid=4767] vsize: 17588
Current children cumulated CPU time (s) 899.81
Current children cumulated vsize (Kb) 19712

[startup+910.052 s]
Raw data (loadavg): 1.01 0.99 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 4128 0 0 0 90941 40 0 0 25 0 1 0 1729193829 18059264 4070 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 4409 4070 145 145 0 4264 0
[pid=4767] vsize: 17636
Current children cumulated CPU time (s) 909.82
Current children cumulated vsize (Kb) 19760

[startup+920.053 s]
Raw data (loadavg): 1.01 0.99 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 4137 0 0 0 91941 40 0 0 25 0 1 0 1729193829 18075648 4079 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 4413 4079 145 145 0 4268 0
[pid=4767] vsize: 17652
Current children cumulated CPU time (s) 919.82
Current children cumulated vsize (Kb) 19776

[startup+930.053 s]
Raw data (loadavg): 1.01 0.99 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 4138 0 0 0 92941 40 0 0 25 0 1 0 1729193829 18075648 4080 4294967295 134512640 135094434 3221224432 3221223024 134557319 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 4413 4080 145 145 0 4268 0
[pid=4767] vsize: 17652
Current children cumulated CPU time (s) 929.82
Current children cumulated vsize (Kb) 19776

[startup+940.053 s]
Raw data (loadavg): 1.01 0.99 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 4140 0 0 0 93941 40 0 0 25 0 1 0 1729193829 18075648 4082 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 4413 4082 145 145 0 4268 0
[pid=4767] vsize: 17652
Current children cumulated CPU time (s) 939.82
Current children cumulated vsize (Kb) 19776

[startup+950.054 s]
Raw data (loadavg): 1.01 0.99 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 4140 0 0 0 94941 40 0 0 25 0 1 0 1729193829 18075648 4082 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 4413 4082 145 145 0 4268 0
[pid=4767] vsize: 17652
Current children cumulated CPU time (s) 949.82
Current children cumulated vsize (Kb) 19776

[startup+960.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 4145 0 0 0 95941 40 0 0 25 0 1 0 1729193829 18092032 4087 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 4417 4087 145 145 0 4272 0
[pid=4767] vsize: 17668
Current children cumulated CPU time (s) 959.82
Current children cumulated vsize (Kb) 19792

[startup+970.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 4159 0 0 0 96941 41 0 0 25 0 1 0 1729193829 18173952 4101 4294967295 134512640 135094434 3221224432 3221223104 134556410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 4437 4101 145 145 0 4292 0
[pid=4767] vsize: 17748
Current children cumulated CPU time (s) 969.83
Current children cumulated vsize (Kb) 19872

[startup+980.056 s]
Raw data (loadavg): 1.00 0.99 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 4159 0 0 0 97942 41 0 0 25 0 1 0 1729193829 18173952 4101 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 4437 4101 145 145 0 4292 0
[pid=4767] vsize: 17748
Current children cumulated CPU time (s) 979.84
Current children cumulated vsize (Kb) 19872

[startup+990.057 s]
Raw data (loadavg): 1.00 0.99 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 4159 0 0 0 98942 41 0 0 25 0 1 0 1729193829 18173952 4101 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 4437 4101 145 145 0 4292 0
[pid=4767] vsize: 17748
Current children cumulated CPU time (s) 989.84
Current children cumulated vsize (Kb) 19872

[startup+1000.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 4166 0 0 0 99942 41 0 0 25 0 1 0 1729193829 18206720 4108 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 4445 4108 145 145 0 4300 0
[pid=4767] vsize: 17780
Current children cumulated CPU time (s) 999.84
Current children cumulated vsize (Kb) 19904

[startup+1010.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 4178 0 0 0 100942 41 0 0 25 0 1 0 1729193829 18272256 4120 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 4461 4120 145 145 0 4316 0
[pid=4767] vsize: 17844
Current children cumulated CPU time (s) 1009.84
Current children cumulated vsize (Kb) 19968

[startup+1020.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 4178 0 0 0 101942 41 0 0 25 0 1 0 1729193829 18272256 4120 4294967295 134512640 135094434 3221224432 3221223088 134558033 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 4461 4120 145 145 0 4316 0
[pid=4767] vsize: 17844
Current children cumulated CPU time (s) 1019.84
Current children cumulated vsize (Kb) 19968

[startup+1030.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 4183 0 0 0 102942 41 0 0 25 0 1 0 1729193829 18305024 4125 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 4469 4125 145 145 0 4324 0
[pid=4767] vsize: 17876
Current children cumulated CPU time (s) 1029.84
Current children cumulated vsize (Kb) 20000

[startup+1040.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 4188 0 0 0 103942 41 0 0 25 0 1 0 1729193829 18337792 4130 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 4477 4130 145 145 0 4332 0
[pid=4767] vsize: 17908
Current children cumulated CPU time (s) 1039.84
Current children cumulated vsize (Kb) 20032

[startup+1050.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 4197 0 0 0 104942 41 0 0 25 0 1 0 1729193829 18403328 4139 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 4493 4139 145 145 0 4348 0
[pid=4767] vsize: 17972
Current children cumulated CPU time (s) 1049.84
Current children cumulated vsize (Kb) 20096

[startup+1060.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 4200 0 0 0 105942 41 0 0 25 0 1 0 1729193829 18403328 4142 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 4493 4142 145 145 0 4348 0
[pid=4767] vsize: 17972
Current children cumulated CPU time (s) 1059.84
Current children cumulated vsize (Kb) 20096

[startup+1070.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 4200 0 0 0 106943 41 0 0 25 0 1 0 1729193829 18403328 4142 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 4493 4142 145 145 0 4348 0
[pid=4767] vsize: 17972
Current children cumulated CPU time (s) 1069.85
Current children cumulated vsize (Kb) 20096

[startup+1080.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 4200 0 0 0 107943 42 0 0 25 0 1 0 1729193829 18403328 4142 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 4493 4142 145 145 0 4348 0
[pid=4767] vsize: 17972
Current children cumulated CPU time (s) 1079.86
Current children cumulated vsize (Kb) 20096

[startup+1090.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 4200 0 0 0 108943 42 0 0 25 0 1 0 1729193829 18403328 4142 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 4493 4142 145 145 0 4348 0
[pid=4767] vsize: 17972
Current children cumulated CPU time (s) 1089.86
Current children cumulated vsize (Kb) 20096

[startup+1100.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 4200 0 0 0 109943 42 0 0 25 0 1 0 1729193829 18403328 4142 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 4493 4142 145 145 0 4348 0
[pid=4767] vsize: 17972
Current children cumulated CPU time (s) 1099.86
Current children cumulated vsize (Kb) 20096

[startup+1110.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 4203 0 0 0 110943 42 0 0 25 0 1 0 1729193829 18403328 4145 4294967295 134512640 135094434 3221224432 3221223088 134557823 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 4493 4145 145 145 0 4348 0
[pid=4767] vsize: 17972
Current children cumulated CPU time (s) 1109.86
Current children cumulated vsize (Kb) 20096

[startup+1120.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 4203 0 0 0 111943 42 0 0 25 0 1 0 1729193829 18403328 4145 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 4493 4145 145 145 0 4348 0
[pid=4767] vsize: 17972
Current children cumulated CPU time (s) 1119.86
Current children cumulated vsize (Kb) 20096

[startup+1130.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 4203 0 0 0 112944 42 0 0 25 0 1 0 1729193829 18403328 4145 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 4493 4145 145 145 0 4348 0
[pid=4767] vsize: 17972
Current children cumulated CPU time (s) 1129.87
Current children cumulated vsize (Kb) 20096

[startup+1140.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 4203 0 0 0 113944 42 0 0 25 0 1 0 1729193829 18403328 4145 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 4493 4145 145 145 0 4348 0
[pid=4767] vsize: 17972
Current children cumulated CPU time (s) 1139.87
Current children cumulated vsize (Kb) 20096

[startup+1150.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 4203 0 0 0 114944 42 0 0 25 0 1 0 1729193829 18403328 4145 4294967295 134512640 135094434 3221224432 3221223104 134556533 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 4493 4145 145 145 0 4348 0
[pid=4767] vsize: 17972
Current children cumulated CPU time (s) 1149.87
Current children cumulated vsize (Kb) 20096

[startup+1160.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 4203 0 0 0 115944 43 0 0 25 0 1 0 1729193829 18403328 4145 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 4493 4145 145 145 0 4348 0
[pid=4767] vsize: 17972
Current children cumulated CPU time (s) 1159.88
Current children cumulated vsize (Kb) 20096

[startup+1170.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 4203 0 0 0 116944 43 0 0 25 0 1 0 1729193829 18403328 4145 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 4493 4145 145 145 0 4348 0
[pid=4767] vsize: 17972
Current children cumulated CPU time (s) 1169.88
Current children cumulated vsize (Kb) 20096

[startup+1180.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 4203 0 0 0 117944 43 0 0 25 0 1 0 1729193829 18403328 4145 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 4493 4145 145 145 0 4348 0
[pid=4767] vsize: 17972
Current children cumulated CPU time (s) 1179.88
Current children cumulated vsize (Kb) 20096

[startup+1190.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 4254 0 0 0 118943 43 0 0 25 0 1 0 1729193829 18620416 4196 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 4546 4196 145 145 0 4401 0
[pid=4767] vsize: 18184
Current children cumulated CPU time (s) 1189.87
Current children cumulated vsize (Kb) 20308

[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 4254 0 0 0 119944 43 0 0 25 0 1 0 1729193829 18620416 4196 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 4546 4196 145 145 0 4401 0
[pid=4767] vsize: 18184
Current children cumulated CPU time (s) 1199.88
Current children cumulated vsize (Kb) 20308

[startup+1210.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 4259 0 0 0 120944 43 0 0 25 0 1 0 1729193829 18653184 4201 4294967295 134512640 135094434 3221224432 3221223024 134557227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 4554 4201 145 145 0 4409 0
[pid=4767] vsize: 18216
Current children cumulated CPU time (s) 1209.88
Current children cumulated vsize (Kb) 20340



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/58 4767
Raw data (/proc/4763/stat): 4763 (minisat+_script) S 4762 4763 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1729193824 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4763/statm): 531 226 485 147 0 384 0
[pid=4763] vsize: 2124
Raw data (/proc/4767/stat): 4767 (minisat+_64-bit) R 4763 4763 20602 0 -1 0 4259 0 0 0 120944 43 0 0 25 0 1 0 1729193829 18653184 4201 4294967295 134512640 135094434 3221224432 3221223024 134556757 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4767/statm): 4554 4201 145 145 0 4409 0
[pid=4767] vsize: 18216
Current children cumulated CPU time (s) 1209.88
Current children cumulated vsize (Kb) 20340

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

Child status: 0
Real time (s): 1210.08
CPU time (s): 1209.89
CPU user time (s): 1209.44
CPU system time (s): 0.447931
CPU usage (%): 99.9841
Max. virtual memory (cumulated for all children) (Kb): 20340

Verifier Data

ERROR: no interpretation found !