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/miplib2003/normalized-mps-v2-13-7-nw04.opb
MD5SUM5a18ff1f45b144b201f1f80233dc9b6b
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 30407
Optimality of the best value was proved NO
Number of terms in the objective function 87482
Biggest coefficient in the objective function 5220
Number of bits for the biggest coefficient in the objective function 13
Sum of the numbers in the objective function 120189580
Number of bits of the sum of numbers in the objective function 27
Biggest number in a constraint 5220
Number of bits of the biggest number in a constraint 13
Biggest sum of numbers in a constraint 120189580
Number of bits of the biggest sum of numbers27
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1190.09
Number of variables87482
Total number of constraints87518
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)87518
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint42032

Trace number 6150

Launcher Data

LAUNCH ON wulflinc2 THE 2005-09-20 03:50:20 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3315 boxname=wulflinc2 idbench=971 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  5a18ff1f45b144b201f1f80233dc9b6b  /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-nw04.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-nw04.opb
IDLAUNCH: 3315
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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	: 2
cpu MHz		: 451.191
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        898868 kB
Buffers:         10200 kB
Cached:         100384 kB
SwapCached:       1004 kB
Active:          33064 kB
Inactive:        80172 kB
HighTotal:      131008 kB
HighFree:        29092 kB
LowTotal:       903652 kB
LowFree:        869776 kB
SwapTotal:     2097136 kB
SwapFree:      2095552 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           5600 kB
Slab:            16860 kB
Committed_AS:    72492 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 04:10:23 (client local time) WITH STATUS 0 IN 1201.22 SECONDS
stats: 3315 7 1201.22 0

Solver Data



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/8169/stat): 8169 (minisat+_script) R 8168 8169 6872 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1797214136 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/8169/statm): 174 3 169 147 0 27 0
[pid=8169] 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=8170
New process pid=8171
New process pid=8172
execve syscall for /bin/sed executable
One traced child (pid=8171) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=8172) exited with status: 0
One traced child (pid=8170) exited with status: 0
New process pid=8173
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-nw04.opb

[startup+10.0032 s]
Raw data (loadavg): 0.96 0.97 0.91 2/57 8175
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 26753 0 0 0 821 104 0 0 25 0 1 0 1797214141 68460544 6197 4294967295 134512640 135094434 3221224448 3221223296 134587787 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8173/statm): 16714 6201 145 145 0 16569 0
[pid=8173] vsize: 66856
Current children cumulated CPU time (s) 9.26
Current children cumulated vsize (Kb) 68980

[startup+20.0039 s]
Raw data (loadavg): 1.04 0.99 0.91 2/57 8175
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 32924 0 0 0 1783 125 0 0 25 0 1 0 1797214141 84213760 8554 4294967295 134512640 135094434 3221224448 3220432592 134596912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8173/statm): 20560 8554 145 145 0 20415 0
[pid=8173] vsize: 82240
Current children cumulated CPU time (s) 19.09
Current children cumulated vsize (Kb) 84364

[startup+30.0046 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 8175
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 32924 0 0 0 2783 125 0 0 25 0 1 0 1797214141 84213760 8554 4294967295 134512640 135094434 3221224448 3221004064 134597037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8173/statm): 20560 8554 145 145 0 20415 0
[pid=8173] vsize: 82240
Current children cumulated CPU time (s) 29.09
Current children cumulated vsize (Kb) 84364

[startup+40.0053 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 8175
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 33254 0 0 0 3782 127 0 0 25 0 1 0 1797214141 85565440 8884 4294967295 134512640 135094434 3221224448 3220450544 134597017 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8173/statm): 20890 8884 145 145 0 20745 0
[pid=8173] vsize: 83560
Current children cumulated CPU time (s) 39.1
Current children cumulated vsize (Kb) 85684

[startup+50.006 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 8175
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 33280 0 0 0 4781 127 0 0 25 0 1 0 1797214141 85671936 8910 4294967295 134512640 135094434 3221224448 3220143424 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8173/statm): 20916 8910 145 145 0 20771 0
[pid=8173] vsize: 83664
Current children cumulated CPU time (s) 49.09
Current children cumulated vsize (Kb) 85788

[startup+60.0067 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 8175
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 34017 0 0 0 5780 129 0 0 25 0 1 0 1797214141 89976832 9647 4294967295 134512640 135094434 3221224448 3219936624 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8173/statm): 21967 9647 145 145 0 21822 0
[pid=8173] vsize: 87868
Current children cumulated CPU time (s) 59.1
Current children cumulated vsize (Kb) 89992

[startup+70.0074 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 8175
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 34038 0 0 0 6780 129 0 0 25 0 1 0 1797214141 89976832 9668 4294967295 134512640 135094434 3221224448 3219517216 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8173/statm): 21967 9668 145 145 0 21822 0
[pid=8173] vsize: 87868
Current children cumulated CPU time (s) 69.1
Current children cumulated vsize (Kb) 89992

[startup+80.0081 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 8175
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 34750 0 0 0 7778 131 0 0 25 0 1 0 1797214141 91324416 10050 4294967295 134512640 135094434 3221224448 3221148560 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8173/statm): 22296 10050 145 145 0 22151 0
[pid=8173] vsize: 89184
Current children cumulated CPU time (s) 79.1
Current children cumulated vsize (Kb) 91308

[startup+90.0078 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 8175
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 34845 0 0 0 8778 132 0 0 25 0 1 0 1797214141 91324416 10145 4294967295 134512640 135094434 3221224448 3220844256 134597091 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8173/statm): 22296 10145 145 145 0 22151 0
[pid=8173] vsize: 89184
Current children cumulated CPU time (s) 89.11
Current children cumulated vsize (Kb) 91308

[startup+100.008 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 8175
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 34920 0 0 0 9778 132 0 0 25 0 1 0 1797214141 91324416 10220 4294967295 134512640 135094434 3221224448 3220495600 134597053 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8173/statm): 22296 10220 145 145 0 22151 0
[pid=8173] vsize: 89184
Current children cumulated CPU time (s) 99.11
Current children cumulated vsize (Kb) 91308

[startup+110.009 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 8175
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 34946 0 0 0 10778 132 0 0 25 0 1 0 1797214141 91324416 10246 4294967295 134512640 135094434 3221224448 3219225472 134519159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8173/statm): 22296 10246 145 145 0 22151 0
[pid=8173] vsize: 89184
Current children cumulated CPU time (s) 109.11
Current children cumulated vsize (Kb) 91308

[startup+120.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8175
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 35059 0 0 0 11777 133 0 0 25 0 1 0 1797214141 94605312 10359 4294967295 134512640 135094434 3221224448 3221131664 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 23097 10359 145 145 0 22952 0
[pid=8173] vsize: 92388
Current children cumulated CPU time (s) 119.11
Current children cumulated vsize (Kb) 94512

[startup+130.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8175
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 35245 0 0 0 12776 134 0 0 25 0 1 0 1797214141 95195136 10545 4294967295 134512640 135094434 3221224448 3220794976 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 23241 10545 145 145 0 23096 0
[pid=8173] vsize: 92964
Current children cumulated CPU time (s) 129.11
Current children cumulated vsize (Kb) 95088

[startup+140.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8175
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 35453 0 0 0 13775 134 0 0 25 0 1 0 1797214141 95166464 10596 4294967295 134512640 135094434 3221224448 3220376448 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 23234 10596 145 145 0 23089 0
[pid=8173] vsize: 92936
Current children cumulated CPU time (s) 139.1
Current children cumulated vsize (Kb) 95060

[startup+150.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8175
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 35719 0 0 0 14774 135 0 0 25 0 1 0 1797214141 95911936 10820 4294967295 134512640 135094434 3221224448 3220663152 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 23416 10820 145 145 0 23271 0
[pid=8173] vsize: 93664
Current children cumulated CPU time (s) 149.1
Current children cumulated vsize (Kb) 95788

[startup+160.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8175
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 37689 0 0 0 15769 139 0 0 25 0 1 0 1797214141 100315136 11953 4294967295 134512640 135094434 3221224448 3219143392 134597094 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 24491 11953 145 145 0 24346 0
[pid=8173] vsize: 97964
Current children cumulated CPU time (s) 159.09
Current children cumulated vsize (Kb) 100088

[startup+170.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8175
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 37842 0 0 0 16768 139 0 0 25 0 1 0 1797214141 100696064 12064 4294967295 134512640 135094434 3221224448 3220231424 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 24584 12064 145 145 0 24439 0
[pid=8173] vsize: 98336
Current children cumulated CPU time (s) 169.08
Current children cumulated vsize (Kb) 100460

[startup+180.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8175
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 37896 0 0 0 17768 139 0 0 25 0 1 0 1797214141 100868096 12118 4294967295 134512640 135094434 3221224448 3220977312 134597091 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 24626 12118 145 145 0 24481 0
[pid=8173] vsize: 98504
Current children cumulated CPU time (s) 179.08
Current children cumulated vsize (Kb) 100628

[startup+190.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8175
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 37915 0 0 0 18768 139 0 0 25 0 1 0 1797214141 100925440 12137 4294967295 134512640 135094434 3221224448 3219597120 134596919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 24640 12137 145 145 0 24495 0
[pid=8173] vsize: 98560
Current children cumulated CPU time (s) 189.08
Current children cumulated vsize (Kb) 100684

[startup+200.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8175
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 37915 0 0 0 19769 139 0 0 25 0 1 0 1797214141 100925440 12137 4294967295 134512640 135094434 3221224448 3218746160 134596919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 24640 12137 145 145 0 24495 0
[pid=8173] vsize: 98560
Current children cumulated CPU time (s) 199.09
Current children cumulated vsize (Kb) 100684

[startup+210.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8175
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 37915 0 0 0 20769 139 0 0 25 0 1 0 1797214141 100925440 12137 4294967295 134512640 135094434 3221224448 3216725328 134596852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 24640 12137 145 145 0 24495 0
[pid=8173] vsize: 98560
Current children cumulated CPU time (s) 209.09
Current children cumulated vsize (Kb) 100684

[startup+220.015 s]
Raw data (loadavg): 1.00 0.99 0.91 1/57 8175
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) T 8169 8169 6872 0 -1 0 38367 0 0 0 21766 141 0 0 25 0 1 0 1797214141 102170624 12506 4294967295 134512640 135094434 3221224448 3220186828 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/8173/statm): 24944 12506 145 145 0 24799 0
[pid=8173] vsize: 99776
Current children cumulated CPU time (s) 219.08
Current children cumulated vsize (Kb) 101900

[startup+230.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8175
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 38609 0 0 0 22765 142 0 0 25 0 1 0 1797214141 101908480 12493 4294967295 134512640 135094434 3221224448 3218809696 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 24880 12493 145 145 0 24735 0
[pid=8173] vsize: 99520
Current children cumulated CPU time (s) 229.08
Current children cumulated vsize (Kb) 101644

[startup+240.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8175
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 38635 0 0 0 23765 142 0 0 25 0 1 0 1797214141 101908480 12519 4294967295 134512640 135094434 3221224448 3220336320 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 24880 12519 145 145 0 24735 0
[pid=8173] vsize: 99520
Current children cumulated CPU time (s) 239.08
Current children cumulated vsize (Kb) 101644

[startup+250.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8175
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 38732 0 0 0 24765 142 0 0 25 0 1 0 1797214141 102076416 12574 4294967295 134512640 135094434 3221224448 3221197488 134597012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 24921 12574 145 145 0 24776 0
[pid=8173] vsize: 99684
Current children cumulated CPU time (s) 249.08
Current children cumulated vsize (Kb) 101808

[startup+260.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8175
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 38733 0 0 0 25765 142 0 0 25 0 1 0 1797214141 102076416 12575 4294967295 134512640 135094434 3221224448 3219689872 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 24921 12575 145 145 0 24776 0
[pid=8173] vsize: 99684
Current children cumulated CPU time (s) 259.08
Current children cumulated vsize (Kb) 101808

[startup+270.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8175
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 38733 0 0 0 26766 142 0 0 25 0 1 0 1797214141 102076416 12575 4294967295 134512640 135094434 3221224448 3217572768 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 24921 12575 145 145 0 24776 0
[pid=8173] vsize: 99684
Current children cumulated CPU time (s) 269.09
Current children cumulated vsize (Kb) 101808

[startup+280.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8175
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 39156 0 0 0 27763 143 0 0 25 0 1 0 1797214141 103198720 12915 4294967295 134512640 135094434 3221224448 3220755904 134597012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 25195 12915 145 145 0 25050 0
[pid=8173] vsize: 100780
Current children cumulated CPU time (s) 279.07
Current children cumulated vsize (Kb) 102904

[startup+290.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 39361 0 0 0 28763 143 0 0 25 0 1 0 1797214141 102801408 12872 4294967295 134512640 135094434 3221224448 3220227024 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 25098 12872 145 145 0 24953 0
[pid=8173] vsize: 100392
Current children cumulated CPU time (s) 289.07
Current children cumulated vsize (Kb) 102516

[startup+300.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 39461 0 0 0 29763 144 0 0 25 0 1 0 1797214141 102969344 12930 4294967295 134512640 135094434 3221224448 3220916944 134596885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 25139 12930 145 145 0 24994 0
[pid=8173] vsize: 100556
Current children cumulated CPU time (s) 299.08
Current children cumulated vsize (Kb) 102680

[startup+310.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 39461 0 0 0 30763 144 0 0 25 0 1 0 1797214141 102969344 12930 4294967295 134512640 135094434 3221224448 3219315168 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 25139 12930 145 145 0 24994 0
[pid=8173] vsize: 100556
Current children cumulated CPU time (s) 309.08
Current children cumulated vsize (Kb) 102680

[startup+320.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 39869 0 0 0 31760 146 0 0 25 0 1 0 1797214141 104042496 13255 4294967295 134512640 135094434 3221224448 3221201888 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 25401 13255 145 145 0 25256 0
[pid=8173] vsize: 101604
Current children cumulated CPU time (s) 319.07
Current children cumulated vsize (Kb) 103728

[startup+330.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 40057 0 0 0 32760 146 0 0 25 0 1 0 1797214141 103542784 13186 4294967295 134512640 135094434 3221224448 3219747776 134597012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 25279 13186 145 145 0 25134 0
[pid=8173] vsize: 101116
Current children cumulated CPU time (s) 329.07
Current children cumulated vsize (Kb) 103240

[startup+340.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 40175 0 0 0 33760 146 0 0 25 0 1 0 1797214141 103784448 13262 4294967295 134512640 135094434 3221224448 3220748512 134597037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 25338 13262 145 145 0 25193 0
[pid=8173] vsize: 101352
Current children cumulated CPU time (s) 339.07
Current children cumulated vsize (Kb) 103476

[startup+350.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 40210 0 0 0 34760 146 0 0 25 0 1 0 1797214141 103895040 13297 4294967295 134512640 135094434 3221224448 3220055248 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 25365 13297 145 145 0 25220 0
[pid=8173] vsize: 101460
Current children cumulated CPU time (s) 349.07
Current children cumulated vsize (Kb) 103584

[startup+360.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 40210 0 0 0 35760 146 0 0 25 0 1 0 1797214141 103895040 13297 4294967295 134512640 135094434 3221224448 3219114000 134596882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 25365 13297 145 145 0 25220 0
[pid=8173] vsize: 101460
Current children cumulated CPU time (s) 359.07
Current children cumulated vsize (Kb) 103584

[startup+370.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 40235 0 0 0 36761 146 0 0 25 0 1 0 1797214141 103976960 13322 4294967295 134512640 135094434 3221224448 3216931952 134597084 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 25385 13322 145 145 0 25240 0
[pid=8173] vsize: 101540
Current children cumulated CPU time (s) 369.08
Current children cumulated vsize (Kb) 103664

[startup+380.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 40707 0 0 0 37757 148 0 0 25 0 1 0 1797214141 111575040 13711 4294967295 134512640 135094434 3221224448 3221151376 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 27240 13711 145 145 0 27095 0
[pid=8173] vsize: 108960
Current children cumulated CPU time (s) 379.06
Current children cumulated vsize (Kb) 111084

[startup+390.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 40899 0 0 0 38756 149 0 0 25 0 1 0 1797214141 111083520 13644 4294967295 134512640 135094434 3221224448 3219580928 134597020 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 27120 13644 145 145 0 26975 0
[pid=8173] vsize: 108480
Current children cumulated CPU time (s) 389.06
Current children cumulated vsize (Kb) 110604

[startup+400.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 41000 0 0 0 39756 149 0 0 25 0 1 0 1797214141 111251456 13703 4294967295 134512640 135094434 3221224448 3220640448 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 27161 13703 145 145 0 27016 0
[pid=8173] vsize: 108644
Current children cumulated CPU time (s) 399.06
Current children cumulated vsize (Kb) 110768

[startup+410.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 41016 0 0 0 40756 150 0 0 25 0 1 0 1797214141 111280128 13719 4294967295 134512640 135094434 3221224448 3220074432 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 27168 13719 145 145 0 27023 0
[pid=8173] vsize: 108672
Current children cumulated CPU time (s) 409.07
Current children cumulated vsize (Kb) 110796

[startup+420.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 41016 0 0 0 41757 150 0 0 25 0 1 0 1797214141 111280128 13719 4294967295 134512640 135094434 3221224448 3219225936 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 27168 13719 145 145 0 27023 0
[pid=8173] vsize: 108672
Current children cumulated CPU time (s) 419.08
Current children cumulated vsize (Kb) 110796

[startup+430.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 41016 0 0 0 42757 150 0 0 25 0 1 0 1797214141 111280128 13719 4294967295 134512640 135094434 3221224448 3217172016 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 27168 13719 145 145 0 27023 0
[pid=8173] vsize: 108672
Current children cumulated CPU time (s) 429.08
Current children cumulated vsize (Kb) 110796

[startup+440.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 41468 0 0 0 43753 151 0 0 25 0 1 0 1797214141 112521216 14088 4294967295 134512640 135094434 3221224448 3220430480 134597023 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 27471 14088 145 145 0 27326 0
[pid=8173] vsize: 109884
Current children cumulated CPU time (s) 439.05
Current children cumulated vsize (Kb) 112008

[startup+450.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 41703 0 0 0 44752 152 0 0 25 0 1 0 1797214141 112197632 14063 4294967295 134512640 135094434 3221224448 3218906848 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 27392 14063 145 145 0 27247 0
[pid=8173] vsize: 109568
Current children cumulated CPU time (s) 449.05
Current children cumulated vsize (Kb) 111692

[startup+460.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 41809 0 0 0 45752 152 0 0 25 0 1 0 1797214141 112365568 14127 4294967295 134512640 135094434 3221224448 3220274016 134597023 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 27433 14127 145 145 0 27288 0
[pid=8173] vsize: 109732
Current children cumulated CPU time (s) 459.05
Current children cumulated vsize (Kb) 111856

[startup+470.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 41822 0 0 0 46752 152 0 0 25 0 1 0 1797214141 112365568 14140 4294967295 134512640 135094434 3221224448 3221068656 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 27433 14140 145 145 0 27288 0
[pid=8173] vsize: 109732
Current children cumulated CPU time (s) 469.05
Current children cumulated vsize (Kb) 111856

[startup+480.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 41828 0 0 0 47752 152 0 0 25 0 1 0 1797214141 112377856 14146 4294967295 134512640 135094434 3221224448 3219636016 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 27436 14146 145 145 0 27291 0
[pid=8173] vsize: 109744
Current children cumulated CPU time (s) 479.05
Current children cumulated vsize (Kb) 111868

[startup+490.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 41828 0 0 0 48753 153 0 0 25 0 1 0 1797214141 112377856 14146 4294967295 134512640 135094434 3221224448 3218540240 134596919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 27436 14146 145 145 0 27291 0
[pid=8173] vsize: 109744
Current children cumulated CPU time (s) 489.07
Current children cumulated vsize (Kb) 111868

[startup+500.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 42013 0 0 0 49752 153 0 0 25 0 1 0 1797214141 112963584 14331 4294967295 134512640 135094434 3221224448 3218985520 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 27579 14331 145 145 0 27434 0
[pid=8173] vsize: 110316
Current children cumulated CPU time (s) 499.06
Current children cumulated vsize (Kb) 112440

[startup+510.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 42452 0 0 0 50750 154 0 0 25 0 1 0 1797214141 113303552 14467 4294967295 134512640 135094434 3221224448 3217259664 134597094 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 27662 14467 145 145 0 27517 0
[pid=8173] vsize: 110648
Current children cumulated CPU time (s) 509.05
Current children cumulated vsize (Kb) 112772

[startup+520.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 42532 0 0 0 51749 155 0 0 25 0 1 0 1797214141 113307648 14506 4294967295 134512640 135094434 3221224448 3219558752 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 27663 14506 145 145 0 27518 0
[pid=8173] vsize: 110652
Current children cumulated CPU time (s) 519.05
Current children cumulated vsize (Kb) 112776

[startup+530.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 42632 0 0 0 52750 155 0 0 25 0 1 0 1797214141 113475584 14564 4294967295 134512640 135094434 3221224448 3220566880 134597020 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 27704 14564 145 145 0 27559 0
[pid=8173] vsize: 110816
Current children cumulated CPU time (s) 529.06
Current children cumulated vsize (Kb) 112940

[startup+540.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 42653 0 0 0 53750 155 0 0 25 0 1 0 1797214141 113516544 14585 4294967295 134512640 135094434 3221224448 3220138144 134596860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 27714 14585 145 145 0 27569 0
[pid=8173] vsize: 110856
Current children cumulated CPU time (s) 539.06
Current children cumulated vsize (Kb) 112980

[startup+550.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 42653 0 0 0 54750 155 0 0 25 0 1 0 1797214141 113516544 14585 4294967295 134512640 135094434 3221224448 3219275568 134596919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 27714 14585 145 145 0 27569 0
[pid=8173] vsize: 110856
Current children cumulated CPU time (s) 549.06
Current children cumulated vsize (Kb) 112980

[startup+560.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 42653 0 0 0 55750 155 0 0 25 0 1 0 1797214141 113516544 14585 4294967295 134512640 135094434 3221224448 3218213760 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 27714 14585 145 145 0 27569 0
[pid=8173] vsize: 110856
Current children cumulated CPU time (s) 559.06
Current children cumulated vsize (Kb) 112980

[startup+570.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) T 8169 8169 6872 0 -1 0 45467 0 0 0 56743 162 0 0 25 0 1 0 1797214141 119476224 16081 4294967295 134512640 135094434 3221224448 3218718284 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/8173/statm): 29169 16081 145 145 0 29024 0
[pid=8173] vsize: 116676
Current children cumulated CPU time (s) 569.06
Current children cumulated vsize (Kb) 118800

[startup+580.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 45800 0 0 0 57741 163 0 0 25 0 1 0 1797214141 120344576 16331 4294967295 134512640 135094434 3221224448 3221026064 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 29381 16331 145 145 0 29236 0
[pid=8173] vsize: 117524
Current children cumulated CPU time (s) 579.05
Current children cumulated vsize (Kb) 119648

[startup+590.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 46048 0 0 0 58740 164 0 0 25 0 1 0 1797214141 120037376 16316 4294967295 134512640 135094434 3221224448 3219052400 134597012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 29306 16316 145 145 0 29161 0
[pid=8173] vsize: 117224
Current children cumulated CPU time (s) 589.05
Current children cumulated vsize (Kb) 119348

[startup+600.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 46149 0 0 0 59740 164 0 0 25 0 1 0 1797214141 120205312 16375 4294967295 134512640 135094434 3221224448 3220128288 134597094 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 29347 16375 145 145 0 29202 0
[pid=8173] vsize: 117388
Current children cumulated CPU time (s) 599.05
Current children cumulated vsize (Kb) 119512

[startup+610.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 46166 0 0 0 60740 164 0 0 25 0 1 0 1797214141 120225792 16392 4294967295 134512640 135094434 3221224448 3220879984 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 29352 16392 145 145 0 29207 0
[pid=8173] vsize: 117408
Current children cumulated CPU time (s) 609.05
Current children cumulated vsize (Kb) 119532

[startup+620.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 46191 0 0 0 61740 164 0 0 25 0 1 0 1797214141 120303616 16417 4294967295 134512640 135094434 3221224448 3219582688 134596852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 29371 16417 145 145 0 29226 0
[pid=8173] vsize: 117484
Current children cumulated CPU time (s) 619.05
Current children cumulated vsize (Kb) 119608

[startup+630.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 46191 0 0 0 62741 164 0 0 25 0 1 0 1797214141 120303616 16417 4294967295 134512640 135094434 3221224448 3218828880 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 29371 16417 145 145 0 29226 0
[pid=8173] vsize: 117484
Current children cumulated CPU time (s) 629.06
Current children cumulated vsize (Kb) 119608

[startup+640.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 46191 0 0 0 63741 164 0 0 25 0 1 0 1797214141 120303616 16417 4294967295 134512640 135094434 3221224448 3217311232 134596912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 29371 16417 145 145 0 29226 0
[pid=8173] vsize: 117484
Current children cumulated CPU time (s) 639.06
Current children cumulated vsize (Kb) 119608

[startup+650.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 46574 0 0 0 64738 166 0 0 25 0 1 0 1797214141 121327616 16717 4294967295 134512640 135094434 3221224448 3219070880 134597026 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 29621 16717 145 145 0 29476 0
[pid=8173] vsize: 118484
Current children cumulated CPU time (s) 649.05
Current children cumulated vsize (Kb) 120608

[startup+660.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 46720 0 0 0 65737 167 0 0 25 0 1 0 1797214141 121790464 16863 4294967295 134512640 135094434 3221224448 3221072352 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 29734 16863 145 145 0 29589 0
[pid=8173] vsize: 118936
Current children cumulated CPU time (s) 659.05
Current children cumulated vsize (Kb) 121060

[startup+670.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 47207 0 0 0 66735 169 0 0 25 0 1 0 1797214141 122433536 17074 4294967295 134512640 135094434 3221224448 3218082816 134597017 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 29891 17074 145 145 0 29746 0
[pid=8173] vsize: 119564
Current children cumulated CPU time (s) 669.05
Current children cumulated vsize (Kb) 121688

[startup+680.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 47308 0 0 0 67735 169 0 0 25 0 1 0 1797214141 122601472 17133 4294967295 134512640 135094434 3221224448 3219131600 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 29932 17133 145 145 0 29787 0
[pid=8173] vsize: 119728
Current children cumulated CPU time (s) 679.05
Current children cumulated vsize (Kb) 121852

[startup+690.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 47320 0 0 0 68736 169 0 0 25 0 1 0 1797214141 122601472 17145 4294967295 134512640 135094434 3221224448 3219856016 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 29932 17145 145 145 0 29787 0
[pid=8173] vsize: 119728
Current children cumulated CPU time (s) 689.06
Current children cumulated vsize (Kb) 121852

[startup+700.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 47349 0 0 0 69735 169 0 0 25 0 1 0 1797214141 122679296 17174 4294967295 134512640 135094434 3221224448 3220436992 134597094 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 29951 17174 145 145 0 29806 0
[pid=8173] vsize: 119804
Current children cumulated CPU time (s) 699.05
Current children cumulated vsize (Kb) 121928

[startup+710.051 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 47385 0 0 0 70735 169 0 0 25 0 1 0 1797214141 122793984 17210 4294967295 134512640 135094434 3221224448 3220937536 134597020 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 29979 17210 145 145 0 29834 0
[pid=8173] vsize: 119916
Current children cumulated CPU time (s) 709.05
Current children cumulated vsize (Kb) 122040

[startup+720.051 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 47406 0 0 0 71735 169 0 0 25 0 1 0 1797214141 122859520 17231 4294967295 134512640 135094434 3221224448 3218960176 134596872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 29995 17231 145 145 0 29850 0
[pid=8173] vsize: 119980
Current children cumulated CPU time (s) 719.05
Current children cumulated vsize (Kb) 122104

[startup+730.052 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 47406 0 0 0 72735 169 0 0 25 0 1 0 1797214141 122859520 17231 4294967295 134512640 135094434 3221224448 3218257408 134596863 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 29995 17231 145 145 0 29850 0
[pid=8173] vsize: 119980
Current children cumulated CPU time (s) 729.05
Current children cumulated vsize (Kb) 122104

[startup+740.052 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 47406 0 0 0 73744 169 0 0 25 0 1 0 1797214141 122859520 17231 4294967295 134512640 135094434 3221224448 3217720256 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 29995 17231 145 145 0 29850 0
[pid=8173] vsize: 119980
Current children cumulated CPU time (s) 739.14
Current children cumulated vsize (Kb) 122104

[startup+750.139 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 47406 0 0 0 74745 169 0 0 25 0 1 0 1797214141 122859520 17231 4294967295 134512640 135094434 3221224448 3217073984 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 29995 17231 145 145 0 29850 0
[pid=8173] vsize: 119980
Current children cumulated CPU time (s) 749.15
Current children cumulated vsize (Kb) 122104

[startup+760.146 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 47406 0 0 0 75745 169 0 0 25 0 1 0 1797214141 122859520 17231 4294967295 134512640 135094434 3221224448 3215786368 134596866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 29995 17231 145 145 0 29850 0
[pid=8173] vsize: 119980
Current children cumulated CPU time (s) 759.15
Current children cumulated vsize (Kb) 122104

[startup+770.146 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 47736 0 0 0 76744 170 0 0 25 0 1 0 1797214141 123719680 17478 4294967295 134512640 135094434 3221224448 3217237488 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 30205 17478 145 145 0 30060 0
[pid=8173] vsize: 120820
Current children cumulated CPU time (s) 769.15
Current children cumulated vsize (Kb) 122944

[startup+780.147 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 47914 0 0 0 77741 172 0 0 25 0 1 0 1797214141 124280832 17656 4294967295 134512640 135094434 3221224448 3219671920 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 30342 17656 145 145 0 30197 0
[pid=8173] vsize: 121368
Current children cumulated CPU time (s) 779.14
Current children cumulated vsize (Kb) 123492

[startup+790.148 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 48003 0 0 0 78740 172 0 0 25 0 1 0 1797214141 124563456 17745 4294967295 134512640 135094434 3221224448 3220891952 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 30411 17745 145 145 0 30266 0
[pid=8173] vsize: 121644
Current children cumulated CPU time (s) 789.13
Current children cumulated vsize (Kb) 123768

[startup+800.148 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 48288 0 0 0 79740 173 0 0 25 0 1 0 1797214141 124379136 17752 4294967295 134512640 135094434 3221224448 3217500608 134597017 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 30366 17752 145 145 0 30221 0
[pid=8173] vsize: 121464
Current children cumulated CPU time (s) 799.14
Current children cumulated vsize (Kb) 123588

[startup+810.149 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 48392 0 0 0 80740 173 0 0 25 0 1 0 1797214141 124547072 17814 4294967295 134512640 135094434 3221224448 3218756896 134597096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 30407 17814 145 145 0 30262 0
[pid=8173] vsize: 121628
Current children cumulated CPU time (s) 809.14
Current children cumulated vsize (Kb) 123752

[startup+820.15 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 48405 0 0 0 81740 173 0 0 25 0 1 0 1797214141 124547072 17827 4294967295 134512640 135094434 3221224448 3219508064 134597012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 30407 17827 145 145 0 30262 0
[pid=8173] vsize: 121628
Current children cumulated CPU time (s) 819.14
Current children cumulated vsize (Kb) 123752

[startup+830.151 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 48415 0 0 0 82740 173 0 0 25 0 1 0 1797214141 124547072 17837 4294967295 134512640 135094434 3221224448 3220114816 134519658 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 30407 17837 145 145 0 30262 0
[pid=8173] vsize: 121628
Current children cumulated CPU time (s) 829.14
Current children cumulated vsize (Kb) 123752

[startup+840.153 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 48423 0 0 0 83741 173 0 0 25 0 1 0 1797214141 124547072 17845 4294967295 134512640 135094434 3221224448 3220631648 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 30407 17845 145 145 0 30262 0
[pid=8173] vsize: 121628
Current children cumulated CPU time (s) 839.15
Current children cumulated vsize (Kb) 123752

[startup+850.155 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 48437 0 0 0 84741 173 0 0 25 0 1 0 1797214141 124571648 17859 4294967295 134512640 135094434 3221224448 3221086080 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 30413 17859 145 145 0 30268 0
[pid=8173] vsize: 121652
Current children cumulated CPU time (s) 849.15
Current children cumulated vsize (Kb) 123776

[startup+860.156 s]
Raw data (loadavg): 1.24 1.04 0.93 4/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 48447 0 0 0 85943 173 0 0 25 0 1 0 1797214141 124604416 17869 4294967295 134512640 135094434 3221224448 3218333968 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 30421 17869 145 145 0 30276 0
[pid=8173] vsize: 121684
Current children cumulated CPU time (s) 861.17
Current children cumulated vsize (Kb) 123808

[startup+872.173 s]
Raw data (loadavg): 1.20 1.04 0.93 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 48447 0 0 0 86943 174 0 0 25 0 1 0 1797214141 124604416 17869 4294967295 134512640 135094434 3221224448 3217875312 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 30421 17869 145 145 0 30276 0
[pid=8173] vsize: 121684
Current children cumulated CPU time (s) 871.18
Current children cumulated vsize (Kb) 123808

[startup+882.173 s]
Raw data (loadavg): 1.17 1.03 0.93 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 48447 0 0 0 87943 174 0 0 25 0 1 0 1797214141 124604416 17869 4294967295 134512640 135094434 3221224448 3217345728 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 30421 17869 145 145 0 30276 0
[pid=8173] vsize: 121684
Current children cumulated CPU time (s) 881.18
Current children cumulated vsize (Kb) 123808

[startup+892.174 s]
Raw data (loadavg): 1.14 1.03 0.93 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 48447 0 0 0 88943 174 0 0 25 0 1 0 1797214141 124604416 17869 4294967295 134512640 135094434 3221224448 3216698048 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 30421 17869 145 145 0 30276 0
[pid=8173] vsize: 121684
Current children cumulated CPU time (s) 891.18
Current children cumulated vsize (Kb) 123808

[startup+902.175 s]
Raw data (loadavg): 1.12 1.03 0.93 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 48447 0 0 0 89944 174 0 0 25 0 1 0 1797214141 124604416 17869 4294967295 134512640 135094434 3221224448 3215528176 134596860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 30421 17869 145 145 0 30276 0
[pid=8173] vsize: 121684
Current children cumulated CPU time (s) 901.19
Current children cumulated vsize (Kb) 123808

[startup+912.175 s]
Raw data (loadavg): 1.10 1.03 0.93 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 48744 0 0 0 90942 175 0 0 25 0 1 0 1797214141 125358080 18083 4294967295 134512640 135094434 3221224448 3216538064 134597043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 30605 18083 145 145 0 30460 0
[pid=8173] vsize: 122420
Current children cumulated CPU time (s) 911.18
Current children cumulated vsize (Kb) 124544

[startup+922.176 s]
Raw data (loadavg): 1.09 1.03 0.93 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 48947 0 0 0 91941 175 0 0 25 0 1 0 1797214141 125997056 18286 4294967295 134512640 135094434 3221224448 3219313584 134597091 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 30761 18286 145 145 0 30616 0
[pid=8173] vsize: 123044
Current children cumulated CPU time (s) 921.17
Current children cumulated vsize (Kb) 125168

[startup+932.177 s]
Raw data (loadavg): 1.07 1.03 0.93 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 49040 0 0 0 92940 176 0 0 25 0 1 0 1797214141 126291968 18379 4294967295 134512640 135094434 3221224448 3220588528 134597017 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 30833 18379 145 145 0 30688 0
[pid=8173] vsize: 123332
Current children cumulated CPU time (s) 931.17
Current children cumulated vsize (Kb) 125456

[startup+942.178 s]
Raw data (loadavg): 1.06 1.03 0.93 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 49272 0 0 0 93939 177 0 0 25 0 1 0 1797214141 125931520 18336 4294967295 134512640 135094434 3221224448 3217051808 134597043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 30745 18336 145 145 0 30600 0
[pid=8173] vsize: 122980
Current children cumulated CPU time (s) 941.17
Current children cumulated vsize (Kb) 125104

[startup+952.178 s]
Raw data (loadavg): 1.05 1.02 0.93 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 49382 0 0 0 94939 177 0 0 25 0 1 0 1797214141 126099456 18404 4294967295 134512640 135094434 3221224448 3218690896 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 30786 18404 145 145 0 30641 0
[pid=8173] vsize: 123144
Current children cumulated CPU time (s) 951.17
Current children cumulated vsize (Kb) 125268

[startup+962.179 s]
Raw data (loadavg): 1.04 1.02 0.93 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 49397 0 0 0 95939 177 0 0 25 0 1 0 1797214141 126099456 18419 4294967295 134512640 135094434 3221224448 3219546256 134597026 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 30786 18419 145 145 0 30641 0
[pid=8173] vsize: 123144
Current children cumulated CPU time (s) 961.17
Current children cumulated vsize (Kb) 125268

[startup+972.18 s]
Raw data (loadavg): 1.04 1.02 0.93 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 49407 0 0 0 96939 177 0 0 25 0 1 0 1797214141 126099456 18429 4294967295 134512640 135094434 3221224448 3220186192 134597043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 30786 18429 145 145 0 30641 0
[pid=8173] vsize: 123144
Current children cumulated CPU time (s) 971.17
Current children cumulated vsize (Kb) 125268

[startup+982.18 s]
Raw data (loadavg): 1.03 1.02 0.93 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 49416 0 0 0 97939 177 0 0 25 0 1 0 1797214141 126099456 18438 4294967295 134512640 135094434 3221224448 3220723344 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 30786 18438 145 145 0 30641 0
[pid=8173] vsize: 123144
Current children cumulated CPU time (s) 981.17
Current children cumulated vsize (Kb) 125268

[startup+992.181 s]
Raw data (loadavg): 1.02 1.02 0.93 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 49424 0 0 0 98940 177 0 0 25 0 1 0 1797214141 126099456 18446 4294967295 134512640 135094434 3221224448 3221197136 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 30786 18446 145 145 0 30641 0
[pid=8173] vsize: 123144
Current children cumulated CPU time (s) 991.18
Current children cumulated vsize (Kb) 125268

[startup+1002.18 s]
Raw data (loadavg): 1.02 1.02 0.93 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 49425 0 0 0 99940 177 0 0 25 0 1 0 1797214141 126099456 18447 4294967295 134512640 135094434 3221224448 3218446608 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 30786 18447 145 145 0 30641 0
[pid=8173] vsize: 123144
Current children cumulated CPU time (s) 1001.18
Current children cumulated vsize (Kb) 125268

[startup+1012.18 s]
Raw data (loadavg): 1.02 1.02 0.93 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 49425 0 0 0 100940 177 0 0 25 0 1 0 1797214141 126099456 18447 4294967295 134512640 135094434 3221224448 3217939728 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 30786 18447 145 145 0 30641 0
[pid=8173] vsize: 123144
Current children cumulated CPU time (s) 1011.18
Current children cumulated vsize (Kb) 125268

[startup+1022.18 s]
Raw data (loadavg): 1.01 1.02 0.93 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 49425 0 0 0 101940 177 0 0 25 0 1 0 1797214141 126099456 18447 4294967295 134512640 135094434 3221224448 3217331824 134596860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 30786 18447 145 145 0 30641 0
[pid=8173] vsize: 123144
Current children cumulated CPU time (s) 1021.18
Current children cumulated vsize (Kb) 125268

[startup+1032.18 s]
Raw data (loadavg): 1.01 1.02 0.93 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 49425 0 0 0 102941 177 0 0 25 0 1 0 1797214141 126099456 18447 4294967295 134512640 135094434 3221224448 3216242912 134596852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 30786 18447 145 145 0 30641 0
[pid=8173] vsize: 123144
Current children cumulated CPU time (s) 1031.19
Current children cumulated vsize (Kb) 125268

[startup+1042.18 s]
Raw data (loadavg): 1.01 1.02 0.93 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 49425 0 0 0 103941 177 0 0 25 0 1 0 1797214141 126099456 18447 4294967295 134512640 135094434 3221224448 3215098912 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 30786 18447 145 145 0 30641 0
[pid=8173] vsize: 123144
Current children cumulated CPU time (s) 1041.19
Current children cumulated vsize (Kb) 125268

[startup+1052.19 s]
Raw data (loadavg): 1.01 1.01 0.93 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 49886 0 0 0 104938 179 0 0 25 0 1 0 1797214141 127361024 18825 4294967295 134512640 135094434 3221224448 3219188800 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 31094 18825 145 145 0 30949 0
[pid=8173] vsize: 124376
Current children cumulated CPU time (s) 1051.18
Current children cumulated vsize (Kb) 126500

[startup+1062.19 s]
Raw data (loadavg): 1.01 1.01 0.93 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 49987 0 0 0 105937 179 0 0 25 0 1 0 1797214141 127680512 18926 4294967295 134512640 135094434 3221224448 3220582016 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 31172 18926 145 145 0 31027 0
[pid=8173] vsize: 124688
Current children cumulated CPU time (s) 1061.17
Current children cumulated vsize (Kb) 126812

[startup+1072.19 s]
Raw data (loadavg): 1.00 1.01 0.93 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 50222 0 0 0 106936 180 0 0 25 0 1 0 1797214141 127324160 18885 4294967295 134512640 135094434 3221224448 3217060960 134597020 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 31085 18885 145 145 0 30940 0
[pid=8173] vsize: 124340
Current children cumulated CPU time (s) 1071.17
Current children cumulated vsize (Kb) 126464

[startup+1082.19 s]
Raw data (loadavg): 1.00 1.01 0.93 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 50248 0 0 0 107936 180 0 0 25 0 1 0 1797214141 127324160 18911 4294967295 134512640 135094434 3221224448 3218621552 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 31085 18911 145 145 0 30940 0
[pid=8173] vsize: 124340
Current children cumulated CPU time (s) 1081.17
Current children cumulated vsize (Kb) 126464

[startup+1092.19 s]
Raw data (loadavg): 1.00 1.01 0.93 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 50345 0 0 0 108936 181 0 0 25 0 1 0 1797214141 127492096 18966 4294967295 134512640 135094434 3221224448 3219477440 134597017 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 31126 18966 145 145 0 30981 0
[pid=8173] vsize: 124504
Current children cumulated CPU time (s) 1091.18
Current children cumulated vsize (Kb) 126628

[startup+1102.19 s]
Raw data (loadavg): 1.00 1.01 0.93 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 50356 0 0 0 109936 181 0 0 25 0 1 0 1797214141 127492096 18977 4294967295 134512640 135094434 3221224448 3220126880 134597043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 31126 18977 145 145 0 30981 0
[pid=8173] vsize: 124504
Current children cumulated CPU time (s) 1101.18
Current children cumulated vsize (Kb) 126628

[startup+1112.19 s]
Raw data (loadavg): 1.00 1.01 0.93 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 50365 0 0 0 110937 181 0 0 25 0 1 0 1797214141 127492096 18986 4294967295 134512640 135094434 3221224448 3220661392 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 31126 18986 145 145 0 30981 0
[pid=8173] vsize: 124504
Current children cumulated CPU time (s) 1111.19
Current children cumulated vsize (Kb) 126628

[startup+1122.19 s]
Raw data (loadavg): 1.00 1.01 0.93 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 50373 0 0 0 111937 181 0 0 25 0 1 0 1797214141 127492096 18994 4294967295 134512640 135094434 3221224448 3221131312 134597026 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 31126 18994 145 145 0 30981 0
[pid=8173] vsize: 124504
Current children cumulated CPU time (s) 1121.19
Current children cumulated vsize (Kb) 126628

[startup+1132.19 s]
Raw data (loadavg): 1.00 1.01 0.93 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 50374 0 0 0 112937 181 0 0 25 0 1 0 1797214141 127492096 18995 4294967295 134512640 135094434 3221224448 3218528448 134596919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 31126 18995 145 145 0 30981 0
[pid=8173] vsize: 124504
Current children cumulated CPU time (s) 1131.19
Current children cumulated vsize (Kb) 126628

[startup+1142.19 s]
Raw data (loadavg): 1.00 1.01 0.93 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 50374 0 0 0 113937 181 0 0 25 0 1 0 1797214141 127492096 18995 4294967295 134512640 135094434 3221224448 3218037936 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 31126 18995 145 145 0 30981 0
[pid=8173] vsize: 124504
Current children cumulated CPU time (s) 1141.19
Current children cumulated vsize (Kb) 126628

[startup+1152.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 50374 0 0 0 114938 181 0 0 25 0 1 0 1797214141 127492096 18995 4294967295 134512640 135094434 3221224448 3217459776 134596866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 31126 18995 145 145 0 30981 0
[pid=8173] vsize: 124504
Current children cumulated CPU time (s) 1151.2
Current children cumulated vsize (Kb) 126628

[startup+1162.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 50374 0 0 0 115938 181 0 0 25 0 1 0 1797214141 127492096 18995 4294967295 134512640 135094434 3221224448 3216601424 134596863 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 31126 18995 145 145 0 30981 0
[pid=8173] vsize: 124504
Current children cumulated CPU time (s) 1161.2
Current children cumulated vsize (Kb) 126628

[startup+1172.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 50374 0 0 0 116938 181 0 0 25 0 1 0 1797214141 127492096 18995 4294967295 134512640 135094434 3221224448 3215331408 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 31126 18995 145 145 0 30981 0
[pid=8173] vsize: 124504
Current children cumulated CPU time (s) 1171.2
Current children cumulated vsize (Kb) 126628

[startup+1182.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 50820 0 0 0 117936 183 0 0 25 0 1 0 1797214141 128716800 19358 4294967295 134512640 135094434 3221224448 3218802656 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 31425 19358 145 145 0 31280 0
[pid=8173] vsize: 125700
Current children cumulated CPU time (s) 1181.2
Current children cumulated vsize (Kb) 127824

[startup+1192.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 50938 0 0 0 118934 183 0 0 25 0 1 0 1797214141 129089536 19476 4294967295 134512640 135094434 3221224448 3220424496 134597043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 31516 19476 145 145 0 31371 0
[pid=8173] vsize: 126064
Current children cumulated CPU time (s) 1191.18
Current children cumulated vsize (Kb) 128188

[startup+1202.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 51135 0 0 0 119933 184 0 0 25 0 1 0 1797214141 141344768 19438 4294967295 134512640 135094434 3221224448 3216710192 134597084 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 34508 19438 145 145 0 34363 0
[pid=8173] vsize: 138032
Current children cumulated CPU time (s) 1201.18
Current children cumulated vsize (Kb) 140156



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1202.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 8177
Raw data (/proc/8169/stat): 8169 (minisat+_script) S 8168 8169 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797214136 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8169/statm): 531 226 485 147 0 384 0
[pid=8169] vsize: 2124
Raw data (/proc/8173/stat): 8173 (minisat+_64-bit) R 8169 8169 6872 0 -1 0 51135 0 0 0 119933 184 0 0 25 0 1 0 1797214141 141344768 19438 4294967295 134512640 135094434 3221224448 3216710544 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8173/statm): 34508 19438 145 145 0 34363 0
[pid=8173] vsize: 138032
Current children cumulated CPU time (s) 1201.18
Current children cumulated vsize (Kb) 140156

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

Child status: 0
Real time (s): 1202.24
CPU time (s): 1201.22
CPU user time (s): 1199.34
CPU system time (s): 1.88171
CPU usage (%): 99.9148
Max. virtual memory (cumulated for all children) (Kb): 140156



Verifier Data




ERROR: no interpretation found !