Some explanations

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

General information on the benchmark

Namemps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-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 6224

Launcher Data

LAUNCH ON wulflinc31 THE 2005-09-20 04:33:41 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3382 boxname=wulflinc31 idbench=1038 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  10547c6c0f11ab5df74fcaff6ba6d160  /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-p0548.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-p0548.opb
IDLAUNCH: 3382
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        920136 kB
Buffers:          8888 kB
Cached:          77924 kB
SwapCached:       1180 kB
Active:          13892 kB
Inactive:        75712 kB
HighTotal:      131008 kB
HighFree:        50092 kB
LowTotal:       903652 kB
LowFree:        870044 kB
SwapTotal:     2097892 kB
SwapFree:      2096228 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5672 kB
Slab:            19144 kB
Committed_AS:    64376 kB
PageTables:        340 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 04:53:51 (client local time) WITH STATUS 0 IN 1209.84 SECONDS
stats: 3382 7 1209.84 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/1252/stat): 1252 (minisat+_script) R 1251 1252 9102 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1855649389 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/1252/statm): 174 3 169 147 0 27 0
[pid=1252] 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=1253
New process pid=1254
New process pid=1255
One traced child (pid=1254) exited with status: 0
execve syscall for /bin/sed executable
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=1255) exited with status: 0
One traced child (pid=1253) exited with status: 0
New process pid=1257
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-p0548.opb

[startup+10.0042 s]
Raw data (loadavg): 0.93 0.97 0.96 2/58 1257
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 1420 0 0 0 979 7 0 0 25 0 1 0 1855649394 6131712 1362 4294967295 134512640 135094434 3221224432 3221223104 134556540 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 1497 1362 145 145 0 1352 0
[pid=1257] vsize: 5988
Current children cumulated CPU time (s) 9.87
Current children cumulated vsize (Kb) 8112

[startup+20.0061 s]
Raw data (loadavg): 0.94 0.97 0.96 2/58 1257
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 1574 0 0 0 1975 9 0 0 25 0 1 0 1855649394 6754304 1516 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 1649 1516 145 145 0 1504 0
[pid=1257] vsize: 6596
Current children cumulated CPU time (s) 19.85
Current children cumulated vsize (Kb) 8720

[startup+30.0081 s]
Raw data (loadavg): 0.95 0.97 0.96 2/58 1257
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 1770 0 0 0 2972 11 0 0 25 0 1 0 1855649394 7561216 1712 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 1846 1712 145 145 0 1701 0
[pid=1257] vsize: 7384
Current children cumulated CPU time (s) 29.84
Current children cumulated vsize (Kb) 9508

[startup+40.009 s]
Raw data (loadavg): 0.96 0.97 0.96 2/58 1257
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 1950 0 0 0 3968 12 0 0 25 0 1 0 1855649394 8302592 1892 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 2027 1892 145 145 0 1882 0
[pid=1257] vsize: 8108
Current children cumulated CPU time (s) 39.81
Current children cumulated vsize (Kb) 10232

[startup+50.0109 s]
Raw data (loadavg): 0.96 0.97 0.96 2/58 1259
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 2136 0 0 0 4964 14 0 0 25 0 1 0 1855649394 9060352 2078 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 2212 2078 145 145 0 2067 0
[pid=1257] vsize: 8848
Current children cumulated CPU time (s) 49.79
Current children cumulated vsize (Kb) 10972

[startup+60.0119 s]
Raw data (loadavg): 0.97 0.97 0.96 2/58 1259
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 2240 0 0 0 5962 15 0 0 25 0 1 0 1855649394 9523200 2182 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 2325 2182 145 145 0 2180 0
[pid=1257] vsize: 9300
Current children cumulated CPU time (s) 59.78
Current children cumulated vsize (Kb) 11424

[startup+70.0138 s]
Raw data (loadavg): 0.97 0.97 0.96 2/58 1259
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 2241 0 0 0 6962 15 0 0 25 0 1 0 1855649394 9523200 2183 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 2325 2183 145 145 0 2180 0
[pid=1257] vsize: 9300
Current children cumulated CPU time (s) 69.78
Current children cumulated vsize (Kb) 11424

[startup+80.0157 s]
Raw data (loadavg): 0.98 0.97 0.96 2/58 1259
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 2278 0 0 0 7961 16 0 0 25 0 1 0 1855649394 9719808 2220 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 2373 2220 145 145 0 2228 0
[pid=1257] vsize: 9492
Current children cumulated CPU time (s) 79.78
Current children cumulated vsize (Kb) 11616

[startup+90.0166 s]
Raw data (loadavg): 0.98 0.97 0.96 2/58 1259
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 2283 0 0 0 8961 16 0 0 25 0 1 0 1855649394 9728000 2225 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 2375 2225 145 145 0 2230 0
[pid=1257] vsize: 9500
Current children cumulated CPU time (s) 89.78
Current children cumulated vsize (Kb) 11624

[startup+100.018 s]
Raw data (loadavg): 0.98 0.97 0.96 2/58 1259
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 2295 0 0 0 9962 16 0 0 25 0 1 0 1855649394 9785344 2237 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 2389 2237 145 145 0 2244 0
[pid=1257] vsize: 9556
Current children cumulated CPU time (s) 99.79
Current children cumulated vsize (Kb) 11680

[startup+110.019 s]
Raw data (loadavg): 0.98 0.97 0.96 2/58 1262
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 2326 0 0 0 10962 16 0 0 25 0 1 0 1855649394 9895936 2268 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 2416 2268 145 145 0 2271 0
[pid=1257] vsize: 9664
Current children cumulated CPU time (s) 109.79
Current children cumulated vsize (Kb) 11788

[startup+120.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1262
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 2339 0 0 0 11962 16 0 0 25 0 1 0 1855649394 9945088 2281 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 2428 2281 145 145 0 2283 0
[pid=1257] vsize: 9712
Current children cumulated CPU time (s) 119.79
Current children cumulated vsize (Kb) 11836

[startup+130.021 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1262
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 2409 0 0 0 12961 16 0 0 25 0 1 0 1855649394 10244096 2351 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 2501 2351 145 145 0 2356 0
[pid=1257] vsize: 10004
Current children cumulated CPU time (s) 129.78
Current children cumulated vsize (Kb) 12128

[startup+140.022 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1262
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 2538 0 0 0 13959 17 0 0 25 0 1 0 1855649394 10780672 2480 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 2632 2480 145 145 0 2487 0
[pid=1257] vsize: 10528
Current children cumulated CPU time (s) 139.77
Current children cumulated vsize (Kb) 12652

[startup+150.023 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1262
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 2546 0 0 0 14959 17 0 0 25 0 1 0 1855649394 10813440 2488 4294967295 134512640 135094434 3221224432 3221223104 134556166 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 2640 2488 145 145 0 2495 0
[pid=1257] vsize: 10560
Current children cumulated CPU time (s) 149.77
Current children cumulated vsize (Kb) 12684

[startup+160.024 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1262
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 2721 0 0 0 15957 19 0 0 25 0 1 0 1855649394 11558912 2663 4294967295 134512640 135094434 3221224432 3221223024 134551469 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 2822 2663 145 145 0 2677 0
[pid=1257] vsize: 11288
Current children cumulated CPU time (s) 159.77
Current children cumulated vsize (Kb) 13412

[startup+170.025 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1264
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 2734 0 0 0 16957 19 0 0 25 0 1 0 1855649394 11673600 2676 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 2850 2676 145 145 0 2705 0
[pid=1257] vsize: 11400
Current children cumulated CPU time (s) 169.77
Current children cumulated vsize (Kb) 13524

[startup+180.026 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1264
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 2787 0 0 0 17956 19 0 0 25 0 1 0 1855649394 11862016 2729 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 2896 2729 145 145 0 2751 0
[pid=1257] vsize: 11584
Current children cumulated CPU time (s) 179.76
Current children cumulated vsize (Kb) 13708

[startup+190.027 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1264
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 2854 0 0 0 18956 19 0 0 25 0 1 0 1855649394 12259328 2796 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 2993 2796 145 145 0 2848 0
[pid=1257] vsize: 11972
Current children cumulated CPU time (s) 189.76
Current children cumulated vsize (Kb) 14096

[startup+200.028 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1264
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 2877 0 0 0 19956 20 0 0 25 0 1 0 1855649394 12374016 2819 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 3021 2819 145 145 0 2876 0
[pid=1257] vsize: 12084
Current children cumulated CPU time (s) 199.77
Current children cumulated vsize (Kb) 14208

[startup+210.029 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1264
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 2877 0 0 0 20956 20 0 0 25 0 1 0 1855649394 12374016 2819 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 3021 2819 145 145 0 2876 0
[pid=1257] vsize: 12084
Current children cumulated CPU time (s) 209.77
Current children cumulated vsize (Kb) 14208

[startup+220.031 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1264
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 2888 0 0 0 21956 20 0 0 25 0 1 0 1855649394 12439552 2830 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 3037 2830 145 145 0 2892 0
[pid=1257] vsize: 12148
Current children cumulated CPU time (s) 219.77
Current children cumulated vsize (Kb) 14272

[startup+230.032 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1266
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 2914 0 0 0 22956 20 0 0 25 0 1 0 1855649394 12570624 2856 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 3069 2856 145 145 0 2924 0
[pid=1257] vsize: 12276
Current children cumulated CPU time (s) 229.77
Current children cumulated vsize (Kb) 14400

[startup+240.033 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1266
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 2921 0 0 0 23956 20 0 0 25 0 1 0 1855649394 12591104 2863 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 3074 2863 145 145 0 2929 0
[pid=1257] vsize: 12296
Current children cumulated CPU time (s) 239.77
Current children cumulated vsize (Kb) 14420

[startup+250.034 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1266
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 2940 0 0 0 24957 20 0 0 25 0 1 0 1855649394 12697600 2882 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 3100 2882 145 145 0 2955 0
[pid=1257] vsize: 12400
Current children cumulated CPU time (s) 249.78
Current children cumulated vsize (Kb) 14524

[startup+260.035 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1266
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 2965 0 0 0 25956 20 0 0 25 0 1 0 1855649394 12804096 2907 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3126 2907 145 145 0 2981 0
[pid=1257] vsize: 12504
Current children cumulated CPU time (s) 259.77
Current children cumulated vsize (Kb) 14628

[startup+270.036 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1266
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 2966 0 0 0 26956 21 0 0 25 0 1 0 1855649394 12804096 2908 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3126 2908 145 145 0 2981 0
[pid=1257] vsize: 12504
Current children cumulated CPU time (s) 269.78
Current children cumulated vsize (Kb) 14628

[startup+280.037 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1266
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 2981 0 0 0 27955 22 0 0 25 0 1 0 1855649394 12886016 2923 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3146 2923 145 145 0 3001 0
[pid=1257] vsize: 12584
Current children cumulated CPU time (s) 279.78
Current children cumulated vsize (Kb) 14708

[startup+290.038 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1268
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 2995 0 0 0 28954 23 0 0 25 0 1 0 1855649394 12951552 2937 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3162 2937 145 145 0 3017 0
[pid=1257] vsize: 12648
Current children cumulated CPU time (s) 289.78
Current children cumulated vsize (Kb) 14772

[startup+300.04 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1268
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 2995 0 0 0 29953 23 0 0 25 0 1 0 1855649394 12951552 2937 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3162 2937 145 145 0 3017 0
[pid=1257] vsize: 12648
Current children cumulated CPU time (s) 299.77
Current children cumulated vsize (Kb) 14772

[startup+310.041 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1268
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 2995 0 0 0 30953 24 0 0 25 0 1 0 1855649394 12951552 2937 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3162 2937 145 145 0 3017 0
[pid=1257] vsize: 12648
Current children cumulated CPU time (s) 309.78
Current children cumulated vsize (Kb) 14772

[startup+320.043 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1268
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3016 0 0 0 31952 25 0 0 25 0 1 0 1855649394 13049856 2958 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3186 2958 145 145 0 3041 0
[pid=1257] vsize: 12744
Current children cumulated CPU time (s) 319.78
Current children cumulated vsize (Kb) 14868

[startup+330.045 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1268
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3032 0 0 0 32952 25 0 0 25 0 1 0 1855649394 13115392 2974 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3202 2974 145 145 0 3057 0
[pid=1257] vsize: 12808
Current children cumulated CPU time (s) 329.78
Current children cumulated vsize (Kb) 14932

[startup+340.046 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1268
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3051 0 0 0 33951 26 0 0 25 0 1 0 1855649394 13197312 2993 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3222 2993 145 145 0 3077 0
[pid=1257] vsize: 12888
Current children cumulated CPU time (s) 339.78
Current children cumulated vsize (Kb) 15012

[startup+350.048 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1270
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3051 0 0 0 34951 26 0 0 25 0 1 0 1855649394 13197312 2993 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3222 2993 145 145 0 3077 0
[pid=1257] vsize: 12888
Current children cumulated CPU time (s) 349.78
Current children cumulated vsize (Kb) 15012

[startup+360.05 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1270
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3060 0 0 0 35950 27 0 0 25 0 1 0 1855649394 13262848 3002 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3238 3002 145 145 0 3093 0
[pid=1257] vsize: 12952
Current children cumulated CPU time (s) 359.78
Current children cumulated vsize (Kb) 15076

[startup+370.051 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1270
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3070 0 0 0 36950 27 0 0 25 0 1 0 1855649394 13328384 3012 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3254 3012 145 145 0 3109 0
[pid=1257] vsize: 13016
Current children cumulated CPU time (s) 369.78
Current children cumulated vsize (Kb) 15140

[startup+380.052 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1270
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3070 0 0 0 37949 28 0 0 25 0 1 0 1855649394 13328384 3012 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3254 3012 145 145 0 3109 0
[pid=1257] vsize: 13016
Current children cumulated CPU time (s) 379.78
Current children cumulated vsize (Kb) 15140

[startup+390.053 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1270
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3070 0 0 0 38949 29 0 0 25 0 1 0 1855649394 13328384 3012 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3254 3012 145 145 0 3109 0
[pid=1257] vsize: 13016
Current children cumulated CPU time (s) 389.79
Current children cumulated vsize (Kb) 15140

[startup+400.055 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1270
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3070 0 0 0 39948 29 0 0 25 0 1 0 1855649394 13328384 3012 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3254 3012 145 145 0 3109 0
[pid=1257] vsize: 13016
Current children cumulated CPU time (s) 399.78
Current children cumulated vsize (Kb) 15140

[startup+410.056 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1272
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3072 0 0 0 40947 30 0 0 25 0 1 0 1855649394 13328384 3014 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3254 3014 145 145 0 3109 0
[pid=1257] vsize: 13016
Current children cumulated CPU time (s) 409.78
Current children cumulated vsize (Kb) 15140

[startup+420.058 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1272
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3072 0 0 0 41947 31 0 0 25 0 1 0 1855649394 13328384 3014 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3254 3014 145 145 0 3109 0
[pid=1257] vsize: 13016
Current children cumulated CPU time (s) 419.79
Current children cumulated vsize (Kb) 15140

[startup+430.058 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1272
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3136 0 0 0 42945 32 0 0 25 0 1 0 1855649394 13590528 3078 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3318 3078 145 145 0 3173 0
[pid=1257] vsize: 13272
Current children cumulated CPU time (s) 429.78
Current children cumulated vsize (Kb) 15396

[startup+440.059 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1272
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3144 0 0 0 43944 32 0 0 25 0 1 0 1855649394 13639680 3086 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3330 3086 145 145 0 3185 0
[pid=1257] vsize: 13320
Current children cumulated CPU time (s) 439.77
Current children cumulated vsize (Kb) 15444

[startup+450.061 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1272
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3161 0 0 0 44944 33 0 0 25 0 1 0 1855649394 13717504 3103 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3349 3103 145 145 0 3204 0
[pid=1257] vsize: 13396
Current children cumulated CPU time (s) 449.78
Current children cumulated vsize (Kb) 15520

[startup+460.062 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1272
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3180 0 0 0 45944 33 0 0 25 0 1 0 1855649394 13799424 3122 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3369 3122 145 145 0 3224 0
[pid=1257] vsize: 13476
Current children cumulated CPU time (s) 459.78
Current children cumulated vsize (Kb) 15600

[startup+470.064 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1274
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3180 0 0 0 46942 34 0 0 25 0 1 0 1855649394 13799424 3122 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3369 3122 145 145 0 3224 0
[pid=1257] vsize: 13476
Current children cumulated CPU time (s) 469.77
Current children cumulated vsize (Kb) 15600

[startup+480.065 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1274
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3201 0 0 0 47942 35 0 0 25 0 1 0 1855649394 13914112 3143 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3397 3143 145 145 0 3252 0
[pid=1257] vsize: 13588
Current children cumulated CPU time (s) 479.78
Current children cumulated vsize (Kb) 15712

[startup+490.066 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1274
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3212 0 0 0 48941 35 0 0 25 0 1 0 1855649394 13979648 3154 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3413 3154 145 145 0 3268 0
[pid=1257] vsize: 13652
Current children cumulated CPU time (s) 489.77
Current children cumulated vsize (Kb) 15776

[startup+500.068 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1274
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3212 0 0 0 49941 36 0 0 25 0 1 0 1855649394 13979648 3154 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3413 3154 145 145 0 3268 0
[pid=1257] vsize: 13652
Current children cumulated CPU time (s) 499.78
Current children cumulated vsize (Kb) 15776

[startup+510.069 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1274
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3225 0 0 0 50940 36 0 0 25 0 1 0 1855649394 14045184 3167 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 3429 3167 145 145 0 3284 0
[pid=1257] vsize: 13716
Current children cumulated CPU time (s) 509.77
Current children cumulated vsize (Kb) 15840

[startup+520.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1274
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3239 0 0 0 51941 36 0 0 25 0 1 0 1855649394 14143488 3181 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 3453 3181 145 145 0 3308 0
[pid=1257] vsize: 13812
Current children cumulated CPU time (s) 519.78
Current children cumulated vsize (Kb) 15936

[startup+530.071 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1276
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3239 0 0 0 52940 36 0 0 25 0 1 0 1855649394 14143488 3181 4294967295 134512640 135094434 3221224432 3221223024 134557251 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3453 3181 145 145 0 3308 0
[pid=1257] vsize: 13812
Current children cumulated CPU time (s) 529.77
Current children cumulated vsize (Kb) 15936

[startup+540.072 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1276
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3250 0 0 0 53939 37 0 0 25 0 1 0 1855649394 14159872 3192 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3457 3192 145 145 0 3312 0
[pid=1257] vsize: 13828
Current children cumulated CPU time (s) 539.77
Current children cumulated vsize (Kb) 15952

[startup+550.074 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1276
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3263 0 0 0 54939 37 0 0 25 0 1 0 1855649394 14209024 3205 4294967295 134512640 135094434 3221224432 3221223096 134550365 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3469 3205 145 145 0 3324 0
[pid=1257] vsize: 13876
Current children cumulated CPU time (s) 549.77
Current children cumulated vsize (Kb) 16000

[startup+560.075 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1276
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3311 0 0 0 55938 38 0 0 25 0 1 0 1855649394 14401536 3253 4294967295 134512640 135094434 3221224432 3221223088 134558238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3516 3253 145 145 0 3371 0
[pid=1257] vsize: 14064
Current children cumulated CPU time (s) 559.77
Current children cumulated vsize (Kb) 16188

[startup+570.077 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1276
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3330 0 0 0 56938 39 0 0 25 0 1 0 1855649394 14532608 3272 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3548 3272 145 145 0 3403 0
[pid=1257] vsize: 14192
Current children cumulated CPU time (s) 569.78
Current children cumulated vsize (Kb) 16316

[startup+580.077 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1276
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3341 0 0 0 57937 39 0 0 25 0 1 0 1855649394 14548992 3283 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3552 3283 145 145 0 3407 0
[pid=1257] vsize: 14208
Current children cumulated CPU time (s) 579.77
Current children cumulated vsize (Kb) 16332

[startup+590.078 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1278
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3429 0 0 0 58935 40 0 0 25 0 1 0 1855649394 14913536 3371 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3641 3371 145 145 0 3496 0
[pid=1257] vsize: 14564
Current children cumulated CPU time (s) 589.76
Current children cumulated vsize (Kb) 16688

[startup+600.08 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1278
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3435 0 0 0 59934 41 0 0 25 0 1 0 1855649394 14946304 3377 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3649 3377 145 145 0 3504 0
[pid=1257] vsize: 14596
Current children cumulated CPU time (s) 599.76
Current children cumulated vsize (Kb) 16720

[startup+610.081 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1278
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3440 0 0 0 60934 41 0 0 25 0 1 0 1855649394 14962688 3382 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3653 3382 145 145 0 3508 0
[pid=1257] vsize: 14612
Current children cumulated CPU time (s) 609.76
Current children cumulated vsize (Kb) 16736

[startup+620.082 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1278
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3474 0 0 0 61933 42 0 0 25 0 1 0 1855649394 15097856 3416 4294967295 134512640 135094434 3221224432 3221223024 134551465 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3686 3416 145 145 0 3541 0
[pid=1257] vsize: 14744
Current children cumulated CPU time (s) 619.76
Current children cumulated vsize (Kb) 16868

[startup+630.084 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1278
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3474 0 0 0 62933 43 0 0 25 0 1 0 1855649394 15097856 3416 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3686 3416 145 145 0 3541 0
[pid=1257] vsize: 14744
Current children cumulated CPU time (s) 629.77
Current children cumulated vsize (Kb) 16868

[startup+640.085 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1278
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3474 0 0 0 63932 43 0 0 25 0 1 0 1855649394 15097856 3416 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3686 3416 145 145 0 3541 0
[pid=1257] vsize: 14744
Current children cumulated CPU time (s) 639.76
Current children cumulated vsize (Kb) 16868

[startup+650.086 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1280
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3504 0 0 0 64932 43 0 0 25 0 1 0 1855649394 15261696 3446 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3726 3446 145 145 0 3581 0
[pid=1257] vsize: 14904
Current children cumulated CPU time (s) 649.76
Current children cumulated vsize (Kb) 17028

[startup+660.087 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1280
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3505 0 0 0 65932 44 0 0 25 0 1 0 1855649394 15261696 3447 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3726 3447 145 145 0 3581 0
[pid=1257] vsize: 14904
Current children cumulated CPU time (s) 659.77
Current children cumulated vsize (Kb) 17028

[startup+670.089 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1280
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3505 0 0 0 66931 44 0 0 25 0 1 0 1855649394 15261696 3447 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3726 3447 145 145 0 3581 0
[pid=1257] vsize: 14904
Current children cumulated CPU time (s) 669.76
Current children cumulated vsize (Kb) 17028

[startup+680.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1280
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3515 0 0 0 67931 45 0 0 25 0 1 0 1855649394 15360000 3457 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3750 3457 145 145 0 3605 0
[pid=1257] vsize: 15000
Current children cumulated CPU time (s) 679.77
Current children cumulated vsize (Kb) 17124

[startup+690.091 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1280
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3517 0 0 0 68931 45 0 0 25 0 1 0 1855649394 15360000 3459 4294967295 134512640 135094434 3221224432 3221223024 134551454 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3750 3459 145 145 0 3605 0
[pid=1257] vsize: 15000
Current children cumulated CPU time (s) 689.77
Current children cumulated vsize (Kb) 17124

[startup+700.093 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1280
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3523 0 0 0 69930 46 0 0 25 0 1 0 1855649394 15360000 3465 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3750 3465 145 145 0 3605 0
[pid=1257] vsize: 15000
Current children cumulated CPU time (s) 699.77
Current children cumulated vsize (Kb) 17124

[startup+710.094 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1283
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3527 0 0 0 70929 47 0 0 25 0 1 0 1855649394 15425536 3469 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3766 3469 145 145 0 3621 0
[pid=1257] vsize: 15064
Current children cumulated CPU time (s) 709.77
Current children cumulated vsize (Kb) 17188

[startup+720.096 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1283
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3528 0 0 0 71929 47 0 0 25 0 1 0 1855649394 15425536 3470 4294967295 134512640 135094434 3221224432 3221223088 134557908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3766 3470 145 145 0 3621 0
[pid=1257] vsize: 15064
Current children cumulated CPU time (s) 719.77
Current children cumulated vsize (Kb) 17188

[startup+730.096 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1283
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3564 0 0 0 72928 48 0 0 25 0 1 0 1855649394 15552512 3506 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3797 3506 145 145 0 3652 0
[pid=1257] vsize: 15188
Current children cumulated CPU time (s) 729.77
Current children cumulated vsize (Kb) 17312

[startup+740.097 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1283
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3567 0 0 0 73928 48 0 0 25 0 1 0 1855649394 15552512 3509 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3797 3509 145 145 0 3652 0
[pid=1257] vsize: 15188
Current children cumulated CPU time (s) 739.77
Current children cumulated vsize (Kb) 17312

[startup+750.099 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1283
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3586 0 0 0 74927 49 0 0 25 0 1 0 1855649394 15650816 3528 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3821 3528 145 145 0 3676 0
[pid=1257] vsize: 15284
Current children cumulated CPU time (s) 749.77
Current children cumulated vsize (Kb) 17408

[startup+760.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1283
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3604 0 0 0 75927 49 0 0 25 0 1 0 1855649394 15781888 3546 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3853 3546 145 145 0 3708 0
[pid=1257] vsize: 15412
Current children cumulated CPU time (s) 759.77
Current children cumulated vsize (Kb) 17536

[startup+770.102 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1285
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3637 0 0 0 76925 51 0 0 25 0 1 0 1855649394 15921152 3579 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1257/statm): 3887 3579 145 145 0 3742 0
[pid=1257] vsize: 15548
Current children cumulated CPU time (s) 769.77
Current children cumulated vsize (Kb) 17672

[startup+780.103 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1285
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3643 0 0 0 77925 51 0 0 25 0 1 0 1855649394 15953920 3585 4294967295 134512640 135094434 3221224432 3221223104 134556288 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 3895 3585 145 145 0 3750 0
[pid=1257] vsize: 15580
Current children cumulated CPU time (s) 779.77
Current children cumulated vsize (Kb) 17704

[startup+790.104 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1285
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3660 0 0 0 78925 51 0 0 25 0 1 0 1855649394 16052224 3602 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 3919 3602 145 145 0 3774 0
[pid=1257] vsize: 15676
Current children cumulated CPU time (s) 789.77
Current children cumulated vsize (Kb) 17800

[startup+800.105 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1285
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3664 0 0 0 79926 51 0 0 25 0 1 0 1855649394 16052224 3606 4294967295 134512640 135094434 3221224432 3221223088 134558181 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 3919 3606 145 145 0 3774 0
[pid=1257] vsize: 15676
Current children cumulated CPU time (s) 799.78
Current children cumulated vsize (Kb) 17800

[startup+810.106 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1285
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3667 0 0 0 80926 51 0 0 25 0 1 0 1855649394 16068608 3609 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 3923 3609 145 145 0 3778 0
[pid=1257] vsize: 15692
Current children cumulated CPU time (s) 809.78
Current children cumulated vsize (Kb) 17816

[startup+820.108 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1285
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3672 0 0 0 81926 51 0 0 25 0 1 0 1855649394 16101376 3614 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 3931 3614 145 145 0 3786 0
[pid=1257] vsize: 15724
Current children cumulated CPU time (s) 819.78
Current children cumulated vsize (Kb) 17848

[startup+830.109 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1287
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3677 0 0 0 82926 51 0 0 25 0 1 0 1855649394 16134144 3619 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 3939 3619 145 145 0 3794 0
[pid=1257] vsize: 15756
Current children cumulated CPU time (s) 829.78
Current children cumulated vsize (Kb) 17880

[startup+840.112 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1287
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3677 0 0 0 83927 51 0 0 25 0 1 0 1855649394 16134144 3619 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 3939 3619 145 145 0 3794 0
[pid=1257] vsize: 15756
Current children cumulated CPU time (s) 839.79
Current children cumulated vsize (Kb) 17880

[startup+850.113 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1287
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3677 0 0 0 84927 51 0 0 25 0 1 0 1855649394 16134144 3619 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 3939 3619 145 145 0 3794 0
[pid=1257] vsize: 15756
Current children cumulated CPU time (s) 849.79
Current children cumulated vsize (Kb) 17880

[startup+860.114 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1287
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3678 0 0 0 85927 51 0 0 25 0 1 0 1855649394 16134144 3620 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 3939 3620 145 145 0 3794 0
[pid=1257] vsize: 15756
Current children cumulated CPU time (s) 859.79
Current children cumulated vsize (Kb) 17880

[startup+870.115 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1287
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3684 0 0 0 86927 51 0 0 25 0 1 0 1855649394 16183296 3626 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 3951 3626 145 145 0 3806 0
[pid=1257] vsize: 15804
Current children cumulated CPU time (s) 869.79
Current children cumulated vsize (Kb) 17928

[startup+880.116 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1287
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3876 0 0 0 87924 53 0 0 25 0 1 0 1855649394 16941056 3818 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 4136 3818 145 145 0 3991 0
[pid=1257] vsize: 16544
Current children cumulated CPU time (s) 879.78
Current children cumulated vsize (Kb) 18668

[startup+890.116 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1289
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3888 0 0 0 88924 53 0 0 25 0 1 0 1855649394 17039360 3830 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 4160 3830 145 145 0 4015 0
[pid=1257] vsize: 16640
Current children cumulated CPU time (s) 889.78
Current children cumulated vsize (Kb) 18764

[startup+900.117 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1289
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3891 0 0 0 89924 53 0 0 25 0 1 0 1855649394 17039360 3833 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 4160 3833 145 145 0 4015 0
[pid=1257] vsize: 16640
Current children cumulated CPU time (s) 899.78
Current children cumulated vsize (Kb) 18764

[startup+910.118 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1289
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 3899 0 0 0 90924 53 0 0 25 0 1 0 1855649394 17039360 3841 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 4160 3841 145 145 0 4015 0
[pid=1257] vsize: 16640
Current children cumulated CPU time (s) 909.78
Current children cumulated vsize (Kb) 18764

[startup+920.119 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1289
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 4067 0 0 0 91921 54 0 0 25 0 1 0 1855649394 17731584 4009 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 4329 4009 145 145 0 4184 0
[pid=1257] vsize: 17316
Current children cumulated CPU time (s) 919.76
Current children cumulated vsize (Kb) 19440

[startup+930.12 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1289
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 4121 0 0 0 92921 54 0 0 25 0 1 0 1855649394 17977344 4063 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 4389 4063 145 145 0 4244 0
[pid=1257] vsize: 17556
Current children cumulated CPU time (s) 929.76
Current children cumulated vsize (Kb) 19680

[startup+940.121 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1289
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 4128 0 0 0 93921 54 0 0 25 0 1 0 1855649394 18059264 4070 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 4409 4070 145 145 0 4264 0
[pid=1257] vsize: 17636
Current children cumulated CPU time (s) 939.76
Current children cumulated vsize (Kb) 19760

[startup+950.122 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1291
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 4137 0 0 0 94921 54 0 0 25 0 1 0 1855649394 18075648 4079 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 4413 4079 145 145 0 4268 0
[pid=1257] vsize: 17652
Current children cumulated CPU time (s) 949.76
Current children cumulated vsize (Kb) 19776

[startup+960.123 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1291
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 4138 0 0 0 95922 54 0 0 25 0 1 0 1855649394 18075648 4080 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 4413 4080 145 145 0 4268 0
[pid=1257] vsize: 17652
Current children cumulated CPU time (s) 959.77
Current children cumulated vsize (Kb) 19776

[startup+970.124 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1291
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 4140 0 0 0 96922 54 0 0 25 0 1 0 1855649394 18075648 4082 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 4413 4082 145 145 0 4268 0
[pid=1257] vsize: 17652
Current children cumulated CPU time (s) 969.77
Current children cumulated vsize (Kb) 19776

[startup+980.125 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1291
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 4140 0 0 0 97922 54 0 0 25 0 1 0 1855649394 18075648 4082 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 4413 4082 145 145 0 4268 0
[pid=1257] vsize: 17652
Current children cumulated CPU time (s) 979.77
Current children cumulated vsize (Kb) 19776

[startup+990.126 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1291
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 4145 0 0 0 98922 54 0 0 25 0 1 0 1855649394 18092032 4087 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 4417 4087 145 145 0 4272 0
[pid=1257] vsize: 17668
Current children cumulated CPU time (s) 989.77
Current children cumulated vsize (Kb) 19792

[startup+1000.13 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1291
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 4159 0 0 0 99922 54 0 0 25 0 1 0 1855649394 18173952 4101 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 4437 4101 145 145 0 4292 0
[pid=1257] vsize: 17748
Current children cumulated CPU time (s) 999.77
Current children cumulated vsize (Kb) 19872

[startup+1010.13 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1293
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 4159 0 0 0 100923 54 0 0 25 0 1 0 1855649394 18173952 4101 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 4437 4101 145 145 0 4292 0
[pid=1257] vsize: 17748
Current children cumulated CPU time (s) 1009.78
Current children cumulated vsize (Kb) 19872

[startup+1020.13 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1293
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 4159 0 0 0 101923 54 0 0 25 0 1 0 1855649394 18173952 4101 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 4437 4101 145 145 0 4292 0
[pid=1257] vsize: 17748
Current children cumulated CPU time (s) 1019.78
Current children cumulated vsize (Kb) 19872

[startup+1030.13 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1293
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 4165 0 0 0 102923 54 0 0 25 0 1 0 1855649394 18206720 4107 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 4445 4107 145 145 0 4300 0
[pid=1257] vsize: 17780
Current children cumulated CPU time (s) 1029.78
Current children cumulated vsize (Kb) 19904

[startup+1040.13 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1293
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 4172 0 0 0 103923 54 0 0 25 0 1 0 1855649394 18239488 4114 4294967295 134512640 135094434 3221224432 3221223104 134556434 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 4453 4114 145 145 0 4308 0
[pid=1257] vsize: 17812
Current children cumulated CPU time (s) 1039.78
Current children cumulated vsize (Kb) 19936

[startup+1050.13 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1293
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 4178 0 0 0 104924 54 0 0 25 0 1 0 1855649394 18272256 4120 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 4461 4120 145 145 0 4316 0
[pid=1257] vsize: 17844
Current children cumulated CPU time (s) 1049.79
Current children cumulated vsize (Kb) 19968

[startup+1060.13 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1293
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 4183 0 0 0 105924 54 0 0 25 0 1 0 1855649394 18305024 4125 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 4469 4125 145 145 0 4324 0
[pid=1257] vsize: 17876
Current children cumulated CPU time (s) 1059.79
Current children cumulated vsize (Kb) 20000

[startup+1070.13 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1295
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 4188 0 0 0 106924 54 0 0 25 0 1 0 1855649394 18337792 4130 4294967295 134512640 135094434 3221224432 3221223088 134558026 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 4477 4130 145 145 0 4332 0
[pid=1257] vsize: 17908
Current children cumulated CPU time (s) 1069.79
Current children cumulated vsize (Kb) 20032

[startup+1080.13 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1295
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 4188 0 0 0 107924 54 0 0 25 0 1 0 1855649394 18337792 4130 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 4477 4130 145 145 0 4332 0
[pid=1257] vsize: 17908
Current children cumulated CPU time (s) 1079.79
Current children cumulated vsize (Kb) 20032

[startup+1090.13 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1295
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 4198 0 0 0 108924 54 0 0 25 0 1 0 1855649394 18403328 4140 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 4493 4140 145 145 0 4348 0
[pid=1257] vsize: 17972
Current children cumulated CPU time (s) 1089.79
Current children cumulated vsize (Kb) 20096

[startup+1100.14 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1295
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 4200 0 0 0 109925 54 0 0 25 0 1 0 1855649394 18403328 4142 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 4493 4142 145 145 0 4348 0
[pid=1257] vsize: 17972
Current children cumulated CPU time (s) 1099.8
Current children cumulated vsize (Kb) 20096

[startup+1110.14 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1295
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 4200 0 0 0 110925 54 0 0 25 0 1 0 1855649394 18403328 4142 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 4493 4142 145 145 0 4348 0
[pid=1257] vsize: 17972
Current children cumulated CPU time (s) 1109.8
Current children cumulated vsize (Kb) 20096

[startup+1120.14 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1295
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 4200 0 0 0 111925 54 0 0 25 0 1 0 1855649394 18403328 4142 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 4493 4142 145 145 0 4348 0
[pid=1257] vsize: 17972
Current children cumulated CPU time (s) 1119.8
Current children cumulated vsize (Kb) 20096

[startup+1130.14 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1297
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 4200 0 0 0 112926 54 0 0 25 0 1 0 1855649394 18403328 4142 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 4493 4142 145 145 0 4348 0
[pid=1257] vsize: 17972
Current children cumulated CPU time (s) 1129.81
Current children cumulated vsize (Kb) 20096

[startup+1140.14 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1297
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 4203 0 0 0 113926 54 0 0 25 0 1 0 1855649394 18403328 4145 4294967295 134512640 135094434 3221224432 3221222176 134562864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 4493 4145 145 145 0 4348 0
[pid=1257] vsize: 17972
Current children cumulated CPU time (s) 1139.81
Current children cumulated vsize (Kb) 20096

[startup+1150.14 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1297
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 4203 0 0 0 114926 54 0 0 25 0 1 0 1855649394 18403328 4145 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 4493 4145 145 145 0 4348 0
[pid=1257] vsize: 17972
Current children cumulated CPU time (s) 1149.81
Current children cumulated vsize (Kb) 20096

[startup+1160.14 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1297
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 4203 0 0 0 115926 54 0 0 25 0 1 0 1855649394 18403328 4145 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 4493 4145 145 145 0 4348 0
[pid=1257] vsize: 17972
Current children cumulated CPU time (s) 1159.81
Current children cumulated vsize (Kb) 20096

[startup+1170.14 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1297
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 4203 0 0 0 116926 54 0 0 25 0 1 0 1855649394 18403328 4145 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 4493 4145 145 145 0 4348 0
[pid=1257] vsize: 17972
Current children cumulated CPU time (s) 1169.81
Current children cumulated vsize (Kb) 20096

[startup+1180.14 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1297
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 4203 0 0 0 117927 54 0 0 25 0 1 0 1855649394 18403328 4145 4294967295 134512640 135094434 3221224432 3221223024 134551469 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 4493 4145 145 145 0 4348 0
[pid=1257] vsize: 17972
Current children cumulated CPU time (s) 1179.82
Current children cumulated vsize (Kb) 20096

[startup+1190.14 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1299
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 4203 0 0 0 118927 54 0 0 25 0 1 0 1855649394 18403328 4145 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 4493 4145 145 145 0 4348 0
[pid=1257] vsize: 17972
Current children cumulated CPU time (s) 1189.82
Current children cumulated vsize (Kb) 20096

[startup+1200.15 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1299
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 4203 0 0 0 119927 54 0 0 25 0 1 0 1855649394 18403328 4145 4294967295 134512640 135094434 3221224432 3221223024 134557037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 4493 4145 145 145 0 4348 0
[pid=1257] vsize: 17972
Current children cumulated CPU time (s) 1199.82
Current children cumulated vsize (Kb) 20096

[startup+1210.15 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1299
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 4203 0 0 0 120927 54 0 0 25 0 1 0 1855649394 18403328 4145 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 4493 4145 145 145 0 4348 0
[pid=1257] vsize: 17972
Current children cumulated CPU time (s) 1209.82
Current children cumulated vsize (Kb) 20096



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.15 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1299
Raw data (/proc/1252/stat): 1252 (minisat+_script) S 1251 1252 9102 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855649389 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1252/statm): 531 226 485 147 0 384 0
[pid=1252] vsize: 2124
Raw data (/proc/1257/stat): 1257 (minisat+_64-bit) R 1252 1252 9102 0 -1 0 4203 0 0 0 120928 54 0 0 25 0 1 0 1855649394 18403328 4145 4294967295 134512640 135094434 3221224432 3221223088 134558141 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1257/statm): 4493 4145 145 145 0 4348 0
[pid=1257] vsize: 17972
Current children cumulated CPU time (s) 1209.83
Current children cumulated vsize (Kb) 20096

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

Child status: 0
Real time (s): 1210.16
CPU time (s): 1209.84
CPU user time (s): 1209.28
CPU system time (s): 0.553915
CPU usage (%): 99.9732
Max. virtual memory (cumulated for all children) (Kb): 20096

Verifier Data

ERROR: no interpretation found !