Some explanations

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

General information on the benchmark

Namemps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-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 benchmark1204.97
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 3925

Launcher Data

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        835288 kB
Buffers:         35240 kB
Cached:         137044 kB
SwapCached:        708 kB
Active:          83988 kB
Inactive:        90888 kB
HighTotal:      131008 kB
HighFree:        24836 kB
LowTotal:       903652 kB
LowFree:        810452 kB
SwapTotal:     2097136 kB
SwapFree:      2095936 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5740 kB
Slab:            18856 kB
Committed_AS:    64164 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-19 04:08:17 (client local time) WITH STATUS 0 IN 1209.1 SECONDS
stats: 2931 7 1209.1 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/11208/stat): 11208 (minisat+_script) R 11207 11208 1333 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1788566919 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/11208/statm): 174 3 169 147 0 27 0
[pid=11208] 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=11209
New process pid=11210
New process pid=11211
execve syscall for /bin/sed executable
One traced child (pid=11210) 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=11211) exited with status: 0
One traced child (pid=11209) exited with status: 0
New process pid=11212
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-20-10-nw04.opb

[startup+10.0041 s]
Raw data (loadavg): 0.94 0.96 0.91 1/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) T 11208 11208 1333 0 -1 0 27081 0 0 0 825 101 0 0 25 0 1 0 1788566925 69414912 6483 4294967295 134512640 135094434 3221224432 3221222716 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/11212/statm): 16947 6483 145 145 0 16802 0
[pid=11212] vsize: 67788
Current children cumulated CPU time (s) 9.26
Current children cumulated vsize (Kb) 69912

[startup+20.0048 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 32924 0 0 0 1791 120 0 0 25 0 1 0 1788566925 84213760 8554 4294967295 134512640 135094434 3221224432 3220524800 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 20560 8554 145 145 0 20415 0
[pid=11212] vsize: 82240
Current children cumulated CPU time (s) 19.11
Current children cumulated vsize (Kb) 84364

[startup+30.0064 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 32924 0 0 0 2791 121 0 0 25 0 1 0 1788566925 84213760 8554 4294967295 134512640 135094434 3221224432 3220928016 134597023 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 20560 8554 145 145 0 20415 0
[pid=11212] vsize: 82240
Current children cumulated CPU time (s) 29.12
Current children cumulated vsize (Kb) 84364

[startup+40.0071 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 33254 0 0 0 3790 121 0 0 25 0 1 0 1788566925 85565440 8884 4294967295 134512640 135094434 3221224432 3219638288 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 20890 8884 145 145 0 20745 0
[pid=11212] vsize: 83560
Current children cumulated CPU time (s) 39.11
Current children cumulated vsize (Kb) 85684

[startup+50.0078 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 33280 0 0 0 4790 122 0 0 25 0 1 0 1788566925 85671936 8910 4294967295 134512640 135094434 3221224432 3221177760 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 20916 8910 145 145 0 20771 0
[pid=11212] vsize: 83664
Current children cumulated CPU time (s) 49.12
Current children cumulated vsize (Kb) 85788

[startup+60.0084 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 34010 0 0 0 5788 124 0 0 25 0 1 0 1788566925 89976832 9640 4294967295 134512640 135094434 3221224432 3219546416 134597091 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 21967 9640 145 145 0 21822 0
[pid=11212] vsize: 87868
Current children cumulated CPU time (s) 59.12
Current children cumulated vsize (Kb) 89992

[startup+70.0091 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 34038 0 0 0 6788 124 0 0 25 0 1 0 1788566925 89976832 9668 4294967295 134512640 135094434 3221224432 3219748992 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 21967 9668 145 145 0 21822 0
[pid=11212] vsize: 87868
Current children cumulated CPU time (s) 69.12
Current children cumulated vsize (Kb) 89992

[startup+80.0107 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 34739 0 0 0 7786 126 0 0 25 0 1 0 1788566925 91324416 10039 4294967295 134512640 135094434 3221224432 3220507904 134597020 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 22296 10039 145 145 0 22151 0
[pid=11212] vsize: 89184
Current children cumulated CPU time (s) 79.12
Current children cumulated vsize (Kb) 91308

[startup+90.0114 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 34830 0 0 0 8786 126 0 0 25 0 1 0 1788566925 91324416 10130 4294967295 134512640 135094434 3221224432 3219899648 134597026 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 22296 10130 145 145 0 22151 0
[pid=11212] vsize: 89184
Current children cumulated CPU time (s) 89.12
Current children cumulated vsize (Kb) 91308

[startup+100.011 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 34914 0 0 0 9785 127 0 0 25 0 1 0 1788566925 91324416 10214 4294967295 134512640 135094434 3221224432 3220115952 134597020 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 22296 10214 145 145 0 22151 0
[pid=11212] vsize: 89184
Current children cumulated CPU time (s) 99.12
Current children cumulated vsize (Kb) 91308

[startup+110.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 34932 0 0 0 10785 127 0 0 25 0 1 0 1788566925 91324416 10232 4294967295 134512640 135094434 3221224432 3218867936 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 22296 10232 145 145 0 22151 0
[pid=11212] vsize: 89184
Current children cumulated CPU time (s) 109.12
Current children cumulated vsize (Kb) 91308

[startup+120.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 35055 0 0 0 11784 128 0 0 25 0 1 0 1788566925 94605312 10355 4294967295 134512640 135094434 3221224432 3220914640 134597037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 23097 10355 145 145 0 22952 0
[pid=11212] vsize: 92388
Current children cumulated CPU time (s) 119.12
Current children cumulated vsize (Kb) 94512

[startup+130.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 35192 0 0 0 12784 129 0 0 25 0 1 0 1788566925 95027200 10492 4294967295 134512640 135094434 3221224432 3220074064 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 23200 10492 145 145 0 23055 0
[pid=11212] vsize: 92800
Current children cumulated CPU time (s) 129.13
Current children cumulated vsize (Kb) 94924

[startup+140.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 35439 0 0 0 13783 129 0 0 25 0 1 0 1788566925 95125504 10582 4294967295 134512640 135094434 3221224432 3220972544 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 23224 10582 145 145 0 23079 0
[pid=11212] vsize: 92896
Current children cumulated CPU time (s) 139.12
Current children cumulated vsize (Kb) 95020

[startup+150.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 35453 0 0 0 14782 130 0 0 25 0 1 0 1788566925 95166464 10596 4294967295 134512640 135094434 3221224432 3218164640 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 23234 10596 145 145 0 23089 0
[pid=11212] vsize: 92936
Current children cumulated CPU time (s) 149.12
Current children cumulated vsize (Kb) 95060

[startup+160.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 37683 0 0 0 15776 135 0 0 25 0 1 0 1788566925 100315136 11947 4294967295 134512640 135094434 3221224432 3218787856 134597037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 24491 11947 145 145 0 24346 0
[pid=11212] vsize: 97964
Current children cumulated CPU time (s) 159.11
Current children cumulated vsize (Kb) 100088

[startup+170.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 37828 0 0 0 16776 136 0 0 25 0 1 0 1788566925 100651008 12050 4294967295 134512640 135094434 3221224432 3220027952 134597046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 24573 12050 145 145 0 24428 0
[pid=11212] vsize: 98292
Current children cumulated CPU time (s) 169.12
Current children cumulated vsize (Kb) 100416

[startup+180.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 37885 0 0 0 17775 136 0 0 25 0 1 0 1788566925 100831232 12107 4294967295 134512640 135094434 3221224432 3220816256 134597094 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 24617 12107 145 145 0 24472 0
[pid=11212] vsize: 98468
Current children cumulated CPU time (s) 179.11
Current children cumulated vsize (Kb) 100592

[startup+190.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 37915 0 0 0 18775 137 0 0 25 0 1 0 1788566925 100925440 12137 4294967295 134512640 135094434 3221224432 3219761136 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 24640 12137 145 145 0 24495 0
[pid=11212] vsize: 98560
Current children cumulated CPU time (s) 189.12
Current children cumulated vsize (Kb) 100684

[startup+200.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 37915 0 0 0 19774 137 0 0 25 0 1 0 1788566925 100925440 12137 4294967295 134512640 135094434 3221224432 3219000816 134596860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 24640 12137 145 145 0 24495 0
[pid=11212] vsize: 98560
Current children cumulated CPU time (s) 199.11
Current children cumulated vsize (Kb) 100684

[startup+210.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 37915 0 0 0 20774 137 0 0 25 0 1 0 1788566925 100925440 12137 4294967295 134512640 135094434 3221224432 3217323360 134596866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 24640 12137 145 145 0 24495 0
[pid=11212] vsize: 98560
Current children cumulated CPU time (s) 209.11
Current children cumulated vsize (Kb) 100684

[startup+220.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 38330 0 0 0 21771 139 0 0 25 0 1 0 1788566925 102051840 12469 4294967295 134512640 135094434 3221224432 3219657648 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 24915 12469 145 145 0 24770 0
[pid=11212] vsize: 99660
Current children cumulated CPU time (s) 219.1
Current children cumulated vsize (Kb) 101784

[startup+230.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 38556 0 0 0 22769 140 0 0 25 0 1 0 1788566925 101900288 12480 4294967295 134512640 135094434 3221224432 3218103744 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 24878 12480 145 145 0 24733 0
[pid=11212] vsize: 99512
Current children cumulated CPU time (s) 229.09
Current children cumulated vsize (Kb) 101636

[startup+240.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 38632 0 0 0 23769 141 0 0 25 0 1 0 1788566925 101908480 12516 4294967295 134512640 135094434 3221224432 3220145520 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 24880 12516 145 145 0 24735 0
[pid=11212] vsize: 99520
Current children cumulated CPU time (s) 239.1
Current children cumulated vsize (Kb) 101644

[startup+250.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 38731 0 0 0 24768 142 0 0 25 0 1 0 1788566925 102076416 12573 4294967295 134512640 135094434 3221224432 3221130240 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 24921 12573 145 145 0 24776 0
[pid=11212] vsize: 99684
Current children cumulated CPU time (s) 249.1
Current children cumulated vsize (Kb) 101808

[startup+260.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 38733 0 0 0 25768 142 0 0 25 0 1 0 1788566925 102076416 12575 4294967295 134512640 135094434 3221224432 3219662752 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 24921 12575 145 145 0 24776 0
[pid=11212] vsize: 99684
Current children cumulated CPU time (s) 259.1
Current children cumulated vsize (Kb) 101808

[startup+270.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 38733 0 0 0 26768 143 0 0 25 0 1 0 1788566925 102076416 12575 4294967295 134512640 135094434 3221224432 3217394288 134596869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 24921 12575 145 145 0 24776 0
[pid=11212] vsize: 99684
Current children cumulated CPU time (s) 269.11
Current children cumulated vsize (Kb) 101808

[startup+280.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 39165 0 0 0 27763 145 0 0 25 0 1 0 1788566925 103227392 12924 4294967295 134512640 135094434 3221224432 3220881728 134597020 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 25202 12924 145 145 0 25057 0
[pid=11212] vsize: 100808
Current children cumulated CPU time (s) 279.08
Current children cumulated vsize (Kb) 102932

[startup+290.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 39364 0 0 0 28762 146 0 0 25 0 1 0 1788566925 102801408 12875 4294967295 134512640 135094434 3221224432 3220378720 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 25098 12875 145 145 0 24953 0
[pid=11212] vsize: 100392
Current children cumulated CPU time (s) 289.08
Current children cumulated vsize (Kb) 102516

[startup+300.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 39461 0 0 0 29762 146 0 0 25 0 1 0 1788566925 102969344 12930 4294967295 134512640 135094434 3221224432 3220783696 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 25139 12930 145 145 0 24994 0
[pid=11212] vsize: 100556
Current children cumulated CPU time (s) 299.08
Current children cumulated vsize (Kb) 102680

[startup+310.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 39461 0 0 0 30762 146 0 0 25 0 1 0 1788566925 102969344 12930 4294967295 134512640 135094434 3221224432 3218029120 134596888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 25139 12930 145 145 0 24994 0
[pid=11212] vsize: 100556
Current children cumulated CPU time (s) 309.08
Current children cumulated vsize (Kb) 102680

[startup+320.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 39991 0 0 0 31759 148 0 0 25 0 1 0 1788566925 103534592 13160 4294967295 134512640 135094434 3221224432 3218320400 134597029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 25277 13160 145 145 0 25132 0
[pid=11212] vsize: 101108
Current children cumulated CPU time (s) 319.07
Current children cumulated vsize (Kb) 103232

[startup+330.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 40065 0 0 0 32759 149 0 0 25 0 1 0 1788566925 103542784 13194 4294967295 134512640 135094434 3221224432 3220196912 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 25279 13194 145 145 0 25134 0
[pid=11212] vsize: 101116
Current children cumulated CPU time (s) 329.08
Current children cumulated vsize (Kb) 103240

[startup+340.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 40200 0 0 0 33758 149 0 0 25 0 1 0 1788566925 103866368 13287 4294967295 134512640 135094434 3221224432 3221089760 134597053 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 25358 13287 145 145 0 25213 0
[pid=11212] vsize: 101432
Current children cumulated CPU time (s) 339.07
Current children cumulated vsize (Kb) 103556

[startup+350.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 40210 0 0 0 34758 150 0 0 25 0 1 0 1788566925 103895040 13297 4294967295 134512640 135094434 3221224432 3219675600 134596919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 25365 13297 145 145 0 25220 0
[pid=11212] vsize: 101460
Current children cumulated CPU time (s) 349.08
Current children cumulated vsize (Kb) 103584

[startup+360.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 40210 0 0 0 35758 150 0 0 25 0 1 0 1788566925 103895040 13297 4294967295 134512640 135094434 3221224432 3218099696 134596880 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 25365 13297 145 145 0 25220 0
[pid=11212] vsize: 101460
Current children cumulated CPU time (s) 359.08
Current children cumulated vsize (Kb) 103584

[startup+370.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 40630 0 0 0 36754 152 0 0 25 0 1 0 1788566925 105037824 13634 4294967295 134512640 135094434 3221224432 3220097472 134597037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 25644 13634 145 145 0 25499 0
[pid=11212] vsize: 102576
Current children cumulated CPU time (s) 369.06
Current children cumulated vsize (Kb) 104700

[startup+380.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 40885 0 0 0 37752 154 0 0 25 0 1 0 1788566925 111083520 13630 4294967295 134512640 135094434 3221224432 3218753712 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 27120 13630 145 145 0 26975 0
[pid=11212] vsize: 108480
Current children cumulated CPU time (s) 379.06
Current children cumulated vsize (Kb) 110604

[startup+390.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 40994 0 0 0 38751 154 0 0 25 0 1 0 1788566925 111251456 13697 4294967295 134512640 135094434 3221224432 3220298288 134597096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 27161 13697 145 145 0 27016 0
[pid=11212] vsize: 108644
Current children cumulated CPU time (s) 389.05
Current children cumulated vsize (Kb) 110768

[startup+400.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 41009 0 0 0 39751 154 0 0 25 0 1 0 1788566925 111255552 13712 4294967295 134512640 135094434 3221224432 3221131472 134597017 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 27162 13712 145 145 0 27017 0
[pid=11212] vsize: 108648
Current children cumulated CPU time (s) 399.05
Current children cumulated vsize (Kb) 110772

[startup+410.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 41016 0 0 0 40751 155 0 0 25 0 1 0 1788566925 111280128 13719 4294967295 134512640 135094434 3221224432 3219563488 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 27168 13719 145 145 0 27023 0
[pid=11212] vsize: 108672
Current children cumulated CPU time (s) 409.06
Current children cumulated vsize (Kb) 110796

[startup+420.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 41016 0 0 0 41751 155 0 0 25 0 1 0 1788566925 111280128 13719 4294967295 134512640 135094434 3221224432 3218237680 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 27168 13719 145 145 0 27023 0
[pid=11212] vsize: 108672
Current children cumulated CPU time (s) 419.06
Current children cumulated vsize (Kb) 110796

[startup+430.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 41406 0 0 0 42748 157 0 0 25 0 1 0 1788566925 112324608 14026 4294967295 134512640 135094434 3221224432 3219572464 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 27423 14026 145 145 0 27278 0
[pid=11212] vsize: 109692
Current children cumulated CPU time (s) 429.05
Current children cumulated vsize (Kb) 111816

[startup+440.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 41644 0 0 0 43747 157 0 0 25 0 1 0 1788566925 112193536 14045 4294967295 134512640 135094434 3221224432 3217874592 134597040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 27391 14045 145 145 0 27246 0
[pid=11212] vsize: 109564
Current children cumulated CPU time (s) 439.04
Current children cumulated vsize (Kb) 111688

[startup+450.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 41721 0 0 0 44747 158 0 0 25 0 1 0 1788566925 112197632 14081 4294967295 134512640 135094434 3221224432 3219957552 134597043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 27392 14081 145 145 0 27247 0
[pid=11212] vsize: 109568
Current children cumulated CPU time (s) 449.05
Current children cumulated vsize (Kb) 111692

[startup+460.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 41819 0 0 0 45746 159 0 0 25 0 1 0 1788566925 112365568 14137 4294967295 134512640 135094434 3221224432 3220880672 134597026 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 27433 14137 145 145 0 27288 0
[pid=11212] vsize: 109732
Current children cumulated CPU time (s) 459.05
Current children cumulated vsize (Kb) 111856

[startup+470.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 41828 0 0 0 46746 159 0 0 25 0 1 0 1788566925 112377856 14146 4294967295 134512640 135094434 3221224432 3219826960 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 27436 14146 145 145 0 27291 0
[pid=11212] vsize: 109744
Current children cumulated CPU time (s) 469.05
Current children cumulated vsize (Kb) 111868

[startup+480.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 41828 0 0 0 47746 159 0 0 25 0 1 0 1788566925 112377856 14146 4294967295 134512640 135094434 3221224432 3218853504 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 27436 14146 145 145 0 27291 0
[pid=11212] vsize: 109744
Current children cumulated CPU time (s) 479.05
Current children cumulated vsize (Kb) 111868

[startup+490.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 41933 0 0 0 48744 161 0 0 25 0 1 0 1788566925 112709632 14251 4294967295 134512640 135094434 3221224432 3217884096 134597026 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 27517 14251 145 145 0 27372 0
[pid=11212] vsize: 110068
Current children cumulated CPU time (s) 489.05
Current children cumulated vsize (Kb) 112192

[startup+500.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 42339 0 0 0 49742 162 0 0 25 0 1 0 1788566925 113807360 14574 4294967295 134512640 135094434 3221224432 3221187264 134596997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 27785 14574 145 145 0 27640 0
[pid=11212] vsize: 111140
Current children cumulated CPU time (s) 499.04
Current children cumulated vsize (Kb) 113264

[startup+510.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 42532 0 0 0 50741 163 0 0 25 0 1 0 1788566925 113307648 14506 4294967295 134512640 135094434 3221224432 3219501360 134597012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 27663 14506 145 145 0 27518 0
[pid=11212] vsize: 110652
Current children cumulated CPU time (s) 509.04
Current children cumulated vsize (Kb) 112776

[startup+520.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 42632 0 0 0 51741 163 0 0 25 0 1 0 1788566925 113475584 14564 4294967295 134512640 135094434 3221224432 3220544336 134597026 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 27704 14564 145 145 0 27559 0
[pid=11212] vsize: 110816
Current children cumulated CPU time (s) 519.04
Current children cumulated vsize (Kb) 112940

[startup+530.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 42653 0 0 0 52741 163 0 0 25 0 1 0 1788566925 113516544 14585 4294967295 134512640 135094434 3221224432 3220271712 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 27714 14585 145 145 0 27569 0
[pid=11212] vsize: 110856
Current children cumulated CPU time (s) 529.04
Current children cumulated vsize (Kb) 112980

[startup+540.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 42653 0 0 0 53741 164 0 0 25 0 1 0 1788566925 113516544 14585 4294967295 134512640 135094434 3221224432 3219274848 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 27714 14585 145 145 0 27569 0
[pid=11212] vsize: 110856
Current children cumulated CPU time (s) 539.05
Current children cumulated vsize (Kb) 112980

[startup+550.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 42653 0 0 0 54741 164 0 0 25 0 1 0 1788566925 113516544 14585 4294967295 134512640 135094434 3221224432 3218147216 134596852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 27714 14585 145 145 0 27569 0
[pid=11212] vsize: 110856
Current children cumulated CPU time (s) 549.05
Current children cumulated vsize (Kb) 112980

[startup+560.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 45651 0 0 0 55733 171 0 0 25 0 1 0 1788566925 119873536 16182 4294967295 134512640 135094434 3221224432 3218982688 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 29266 16182 145 145 0 29121 0
[pid=11212] vsize: 117064
Current children cumulated CPU time (s) 559.04
Current children cumulated vsize (Kb) 119188

[startup+570.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 45814 0 0 0 56731 172 0 0 25 0 1 0 1788566925 120389632 16345 4294967295 134512640 135094434 3221224432 3221216304 134597020 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 29392 16345 145 145 0 29247 0
[pid=11212] vsize: 117568
Current children cumulated CPU time (s) 569.03
Current children cumulated vsize (Kb) 119692

[startup+580.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 46052 0 0 0 57731 173 0 0 25 0 1 0 1788566925 120037376 16320 4294967295 134512640 135094434 3221224432 3219296672 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 29306 16320 145 145 0 29161 0
[pid=11212] vsize: 117224
Current children cumulated CPU time (s) 579.04
Current children cumulated vsize (Kb) 119348

[startup+590.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 46152 0 0 0 58730 173 0 0 25 0 1 0 1788566925 120205312 16378 4294967295 134512640 135094434 3221224432 3220345808 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 29347 16378 145 145 0 29202 0
[pid=11212] vsize: 117388
Current children cumulated CPU time (s) 589.03
Current children cumulated vsize (Kb) 119512

[startup+600.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 46178 0 0 0 59730 174 0 0 25 0 1 0 1788566925 120262656 16404 4294967295 134512640 135094434 3221224432 3221060720 134597040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 29361 16404 145 145 0 29216 0
[pid=11212] vsize: 117444
Current children cumulated CPU time (s) 599.04
Current children cumulated vsize (Kb) 119568

[startup+610.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 46191 0 0 0 60730 174 0 0 25 0 1 0 1788566925 120303616 16417 4294967295 134512640 135094434 3221224432 3219391360 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 29371 16417 145 145 0 29226 0
[pid=11212] vsize: 117484
Current children cumulated CPU time (s) 609.04
Current children cumulated vsize (Kb) 119608

[startup+620.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 46191 0 0 0 61730 174 0 0 25 0 1 0 1788566925 120303616 16417 4294967295 134512640 135094434 3221224432 3218544448 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 29371 16417 145 145 0 29226 0
[pid=11212] vsize: 117484
Current children cumulated CPU time (s) 619.04
Current children cumulated vsize (Kb) 119608

[startup+630.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 46191 0 0 0 62730 174 0 0 25 0 1 0 1788566925 120303616 16417 4294967295 134512640 135094434 3221224432 3216541392 134596912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 29371 16417 145 145 0 29226 0
[pid=11212] vsize: 117484
Current children cumulated CPU time (s) 629.04
Current children cumulated vsize (Kb) 119608

[startup+640.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 46654 0 0 0 63728 176 0 0 25 0 1 0 1788566925 121581568 16797 4294967295 134512640 135094434 3221224432 3220169280 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 29683 16797 145 145 0 29538 0
[pid=11212] vsize: 118732
Current children cumulated CPU time (s) 639.04
Current children cumulated vsize (Kb) 120856

[startup+650.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 47189 0 0 0 64725 178 0 0 25 0 1 0 1788566925 122433536 17056 4294967295 134512640 135094434 3221224432 3216949184 134597026 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 29891 17056 145 145 0 29746 0
[pid=11212] vsize: 119564
Current children cumulated CPU time (s) 649.03
Current children cumulated vsize (Kb) 121688

[startup+660.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 47216 0 0 0 65725 178 0 0 25 0 1 0 1788566925 122433536 17083 4294967295 134512640 135094434 3221224432 3218582640 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 29891 17083 145 145 0 29746 0
[pid=11212] vsize: 119564
Current children cumulated CPU time (s) 659.03
Current children cumulated vsize (Kb) 121688

[startup+670.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 47313 0 0 0 66725 179 0 0 25 0 1 0 1788566925 122601472 17138 4294967295 134512640 135094434 3221224432 3219445216 134597020 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 29932 17138 145 145 0 29787 0
[pid=11212] vsize: 119728
Current children cumulated CPU time (s) 669.04
Current children cumulated vsize (Kb) 121852

[startup+680.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 47324 0 0 0 67726 179 0 0 25 0 1 0 1788566925 122601472 17149 4294967295 134512640 135094434 3221224432 3220096592 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 29932 17149 145 145 0 29787 0
[pid=11212] vsize: 119728
Current children cumulated CPU time (s) 679.05
Current children cumulated vsize (Kb) 121852

[startup+690.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 47363 0 0 0 68725 179 0 0 25 0 1 0 1788566925 122724352 17188 4294967295 134512640 135094434 3221224432 3220642016 134597040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 29962 17188 145 145 0 29817 0
[pid=11212] vsize: 119848
Current children cumulated CPU time (s) 689.04
Current children cumulated vsize (Kb) 121972

[startup+700.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 47398 0 0 0 69725 179 0 0 25 0 1 0 1788566925 122834944 17223 4294967295 134512640 135094434 3221224432 3221119504 134597026 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 29989 17223 145 145 0 29844 0
[pid=11212] vsize: 119956
Current children cumulated CPU time (s) 699.04
Current children cumulated vsize (Kb) 122080

[startup+710.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 47406 0 0 0 70725 180 0 0 25 0 1 0 1788566925 122859520 17231 4294967295 134512640 135094434 3221224432 3218540048 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 29995 17231 145 145 0 29850 0
[pid=11212] vsize: 119980
Current children cumulated CPU time (s) 709.05
Current children cumulated vsize (Kb) 122104

[startup+720.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 47406 0 0 0 71725 180 0 0 25 0 1 0 1788566925 122859520 17231 4294967295 134512640 135094434 3221224432 3218048832 134596880 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 29995 17231 145 145 0 29850 0
[pid=11212] vsize: 119980
Current children cumulated CPU time (s) 719.05
Current children cumulated vsize (Kb) 122104

[startup+730.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 47406 0 0 0 72725 180 0 0 25 0 1 0 1788566925 122859520 17231 4294967295 134512640 135094434 3221224432 3217469440 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 29995 17231 145 145 0 29850 0
[pid=11212] vsize: 119980
Current children cumulated CPU time (s) 729.05
Current children cumulated vsize (Kb) 122104

[startup+740.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 47406 0 0 0 73725 180 0 0 25 0 1 0 1788566925 122859520 17231 4294967295 134512640 135094434 3221224432 3216618480 134596852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 29995 17231 145 145 0 29850 0
[pid=11212] vsize: 119980
Current children cumulated CPU time (s) 739.05
Current children cumulated vsize (Kb) 122104

[startup+750.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 47406 0 0 0 74725 181 0 0 25 0 1 0 1788566925 122859520 17231 4294967295 134512640 135094434 3221224432 3215399856 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 29995 17231 145 145 0 29850 0
[pid=11212] vsize: 119980
Current children cumulated CPU time (s) 749.06
Current children cumulated vsize (Kb) 122104

[startup+760.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 47844 0 0 0 75722 182 0 0 25 0 1 0 1788566925 124059648 17586 4294967295 134512640 135094434 3221224432 3218706368 134597084 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 30288 17586 145 145 0 30143 0
[pid=11212] vsize: 121152
Current children cumulated CPU time (s) 759.04
Current children cumulated vsize (Kb) 123276

[startup+770.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 47954 0 0 0 76720 183 0 0 25 0 1 0 1788566925 124407808 17696 4294967295 134512640 135094434 3221224432 3220225424 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 30373 17696 145 145 0 30228 0
[pid=11212] vsize: 121492
Current children cumulated CPU time (s) 769.03
Current children cumulated vsize (Kb) 123616

[startup+780.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 48189 0 0 0 77718 185 0 0 25 0 1 0 1788566925 124289024 17693 4294967295 134512640 135094434 3221224432 3215276656 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 30344 17693 145 145 0 30199 0
[pid=11212] vsize: 121376
Current children cumulated CPU time (s) 779.03
Current children cumulated vsize (Kb) 123500

[startup+790.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 48297 0 0 0 78718 185 0 0 25 0 1 0 1788566925 124379136 17761 4294967295 134512640 135094434 3221224432 3218058160 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 30366 17761 145 145 0 30221 0
[pid=11212] vsize: 121464
Current children cumulated CPU time (s) 789.03
Current children cumulated vsize (Kb) 123588

[startup+800.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 48397 0 0 0 79718 185 0 0 25 0 1 0 1788566925 124547072 17819 4294967295 134512640 135094434 3221224432 3219057312 134597094 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 30407 17819 145 145 0 30262 0
[pid=11212] vsize: 121628
Current children cumulated CPU time (s) 799.03
Current children cumulated vsize (Kb) 123752

[startup+810.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 48408 0 0 0 80718 186 0 0 25 0 1 0 1788566925 124547072 17830 4294967295 134512640 135094434 3221224432 3219737200 134597020 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 30407 17830 145 145 0 30262 0
[pid=11212] vsize: 121628
Current children cumulated CPU time (s) 809.04
Current children cumulated vsize (Kb) 123752

[startup+820.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 48418 0 0 0 81718 186 0 0 25 0 1 0 1788566925 124547072 17840 4294967295 134512640 135094434 3221224432 3220293008 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 30407 17840 145 145 0 30262 0
[pid=11212] vsize: 121628
Current children cumulated CPU time (s) 819.04
Current children cumulated vsize (Kb) 123752

[startup+830.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 48426 0 0 0 82718 186 0 0 25 0 1 0 1788566925 124547072 17848 4294967295 134512640 135094434 3221224432 3220777712 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 30407 17848 145 145 0 30262 0
[pid=11212] vsize: 121628
Current children cumulated CPU time (s) 829.04
Current children cumulated vsize (Kb) 123752

[startup+840.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 48446 0 0 0 83718 186 0 0 25 0 1 0 1788566925 124600320 17868 4294967295 134512640 135094434 3221224432 3221216304 134597094 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 30420 17868 145 145 0 30275 0
[pid=11212] vsize: 121680
Current children cumulated CPU time (s) 839.04
Current children cumulated vsize (Kb) 123804

[startup+850.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 48447 0 0 0 84718 186 0 0 25 0 1 0 1788566925 124604416 17869 4294967295 134512640 135094434 3221224432 3218260560 134596857 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 30421 17869 145 145 0 30276 0
[pid=11212] vsize: 121684
Current children cumulated CPU time (s) 849.04
Current children cumulated vsize (Kb) 123808

[startup+860.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 48447 0 0 0 85718 187 0 0 25 0 1 0 1788566925 124604416 17869 4294967295 134512640 135094434 3221224432 3217798208 134596875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 30421 17869 145 145 0 30276 0
[pid=11212] vsize: 121684
Current children cumulated CPU time (s) 859.05
Current children cumulated vsize (Kb) 123808

[startup+870.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 48447 0 0 0 86718 187 0 0 25 0 1 0 1788566925 124604416 17869 4294967295 134512640 135094434 3221224432 3217265632 134596919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 30421 17869 145 145 0 30276 0
[pid=11212] vsize: 121684
Current children cumulated CPU time (s) 869.05
Current children cumulated vsize (Kb) 123808

[startup+880.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 48447 0 0 0 87718 187 0 0 25 0 1 0 1788566925 124604416 17869 4294967295 134512640 135094434 3221224432 3216622176 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 30421 17869 145 145 0 30276 0
[pid=11212] vsize: 121684
Current children cumulated CPU time (s) 879.05
Current children cumulated vsize (Kb) 123808

[startup+890.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 48447 0 0 0 88718 187 0 0 25 0 1 0 1788566925 124604416 17869 4294967295 134512640 135094434 3221224432 3215413936 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 30421 17869 145 145 0 30276 0
[pid=11212] vsize: 121684
Current children cumulated CPU time (s) 889.05
Current children cumulated vsize (Kb) 123808

[startup+900.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 48804 0 0 0 89716 189 0 0 25 0 1 0 1788566925 125546496 18143 4294967295 134512640 135094434 3221224432 3217353632 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 30651 18143 145 145 0 30506 0
[pid=11212] vsize: 122604
Current children cumulated CPU time (s) 899.05
Current children cumulated vsize (Kb) 124728

[startup+910.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) T 11208 11208 1333 0 -1 0 48969 0 0 0 90714 190 0 0 25 0 1 0 1788566925 126066688 18308 4294967295 134512640 135094434 3221224432 3219623084 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/11212/statm): 30778 18308 145 145 0 30633 0
[pid=11212] vsize: 123112
Current children cumulated CPU time (s) 909.04
Current children cumulated vsize (Kb) 125236

[startup+920.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 49055 0 0 0 91713 191 0 0 25 0 1 0 1788566925 126341120 18394 4294967295 134512640 135094434 3221224432 3220807456 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 30845 18394 145 145 0 30700 0
[pid=11212] vsize: 123380
Current children cumulated CPU time (s) 919.04
Current children cumulated vsize (Kb) 125504

[startup+930.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 49280 0 0 0 92712 192 0 0 25 0 1 0 1788566925 125931520 18344 4294967295 134512640 135094434 3221224432 3217531040 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11212/statm): 30745 18344 145 145 0 30600 0
[pid=11212] vsize: 122980
Current children cumulated CPU time (s) 929.04
Current children cumulated vsize (Kb) 125104

[startup+940.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 49385 0 0 0 93712 192 0 0 25 0 1 0 1788566925 126099456 18407 4294967295 134512640 135094434 3221224432 3218816720 134597094 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11212/statm): 30786 18407 145 145 0 30641 0
[pid=11212] vsize: 123144
Current children cumulated CPU time (s) 939.04
Current children cumulated vsize (Kb) 125268

[startup+950.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 49397 0 0 0 94711 193 0 0 25 0 1 0 1788566925 126099456 18419 4294967295 134512640 135094434 3221224432 3219576688 134597026 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11212/statm): 30786 18419 145 145 0 30641 0
[pid=11212] vsize: 123144
Current children cumulated CPU time (s) 949.04
Current children cumulated vsize (Kb) 125268

[startup+960.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 49407 0 0 0 95711 193 0 0 25 0 1 0 1788566925 126099456 18429 4294967295 134512640 135094434 3221224432 3220180192 134597094 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11212/statm): 30786 18429 145 145 0 30641 0
[pid=11212] vsize: 123144
Current children cumulated CPU time (s) 959.04
Current children cumulated vsize (Kb) 125268

[startup+970.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 49416 0 0 0 96712 193 0 0 25 0 1 0 1788566925 126099456 18438 4294967295 134512640 135094434 3221224432 3220694288 134597020 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11212/statm): 30786 18438 145 145 0 30641 0
[pid=11212] vsize: 123144
Current children cumulated CPU time (s) 969.05
Current children cumulated vsize (Kb) 125268

[startup+980.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 49424 0 0 0 97712 193 0 0 25 0 1 0 1788566925 126099456 18446 4294967295 134512640 135094434 3221224432 3221154880 134597026 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11212/statm): 30786 18446 145 145 0 30641 0
[pid=11212] vsize: 123144
Current children cumulated CPU time (s) 979.05
Current children cumulated vsize (Kb) 125268

[startup+990.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 49425 0 0 0 98712 193 0 0 25 0 1 0 1788566925 126099456 18447 4294967295 134512640 135094434 3221224432 3218492000 134596857 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11212/statm): 30786 18447 145 145 0 30641 0
[pid=11212] vsize: 123144
Current children cumulated CPU time (s) 989.05
Current children cumulated vsize (Kb) 125268

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 49425 0 0 0 99712 194 0 0 25 0 1 0 1788566925 126099456 18447 4294967295 134512640 135094434 3221224432 3218005360 134596866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11212/statm): 30786 18447 145 145 0 30641 0
[pid=11212] vsize: 123144
Current children cumulated CPU time (s) 999.06
Current children cumulated vsize (Kb) 125268

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 49425 0 0 0 100712 194 0 0 25 0 1 0 1788566925 126099456 18447 4294967295 134512640 135094434 3221224432 3217426144 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11212/statm): 30786 18447 145 145 0 30641 0
[pid=11212] vsize: 123144
Current children cumulated CPU time (s) 1009.06
Current children cumulated vsize (Kb) 125268

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 49425 0 0 0 101712 194 0 0 25 0 1 0 1788566925 126099456 18447 4294967295 134512640 135094434 3221224432 3216499152 134596860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11212/statm): 30786 18447 145 145 0 30641 0
[pid=11212] vsize: 123144
Current children cumulated CPU time (s) 1019.06
Current children cumulated vsize (Kb) 125268

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 49425 0 0 0 102712 194 0 0 25 0 1 0 1788566925 126099456 18447 4294967295 134512640 135094434 3221224432 3215271552 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11212/statm): 30786 18447 145 145 0 30641 0
[pid=11212] vsize: 123144
Current children cumulated CPU time (s) 1029.06
Current children cumulated vsize (Kb) 125268

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 49864 0 0 0 103709 196 0 0 25 0 1 0 1788566925 127291392 18803 4294967295 134512640 135094434 3221224432 3218885360 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11212/statm): 31077 18803 145 145 0 30932 0
[pid=11212] vsize: 124308
Current children cumulated CPU time (s) 1039.05
Current children cumulated vsize (Kb) 126432

[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 49973 0 0 0 104707 197 0 0 25 0 1 0 1788566925 127635456 18912 4294967295 134512640 135094434 3221224432 3220377840 134597020 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11212/statm): 31161 18912 145 145 0 31016 0
[pid=11212] vsize: 124644
Current children cumulated CPU time (s) 1049.04
Current children cumulated vsize (Kb) 126768

[startup+1060.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 50170 0 0 0 105707 198 0 0 25 0 1 0 1788566925 127320064 18874 4294967295 134512640 135094434 3221224432 3216447936 134597094 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11212/statm): 31084 18874 145 145 0 30939 0
[pid=11212] vsize: 124336
Current children cumulated CPU time (s) 1059.05
Current children cumulated vsize (Kb) 126460

[startup+1070.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 50244 0 0 0 106707 198 0 0 25 0 1 0 1788566925 127324160 18907 4294967295 134512640 135094434 3221224432 3218371440 134597012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11212/statm): 31085 18907 145 145 0 30940 0
[pid=11212] vsize: 124340
Current children cumulated CPU time (s) 1069.05
Current children cumulated vsize (Kb) 126464

[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 50342 0 0 0 107707 198 0 0 25 0 1 0 1788566925 127492096 18963 4294967295 134512640 135094434 3221224432 3219301248 134597026 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11212/statm): 31126 18963 145 145 0 30981 0
[pid=11212] vsize: 124504
Current children cumulated CPU time (s) 1079.05
Current children cumulated vsize (Kb) 126628

[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 50353 0 0 0 108707 198 0 0 25 0 1 0 1788566925 127492096 18974 4294967295 134512640 135094434 3221224432 3219971984 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11212/statm): 31126 18974 145 145 0 30981 0
[pid=11212] vsize: 124504
Current children cumulated CPU time (s) 1089.05
Current children cumulated vsize (Kb) 126628

[startup+1100.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 50363 0 0 0 109707 198 0 0 25 0 1 0 1788566925 127492096 18984 4294967295 134512640 135094434 3221224432 3220528848 134597094 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11212/statm): 31126 18984 145 145 0 30981 0
[pid=11212] vsize: 124504
Current children cumulated CPU time (s) 1099.05
Current children cumulated vsize (Kb) 126628

[startup+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 50371 0 0 0 110707 198 0 0 25 0 1 0 1788566925 127492096 18992 4294967295 134512640 135094434 3221224432 3221019184 134597094 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11212/statm): 31126 18992 145 145 0 30981 0
[pid=11212] vsize: 124504
Current children cumulated CPU time (s) 1109.05
Current children cumulated vsize (Kb) 126628

[startup+1120.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 50374 0 0 0 111707 198 0 0 25 0 1 0 1788566925 127492096 18995 4294967295 134512640 135094434 3221224432 3218625056 134596866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11212/statm): 31126 18995 145 145 0 30981 0
[pid=11212] vsize: 124504
Current children cumulated CPU time (s) 1119.05
Current children cumulated vsize (Kb) 126628

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 50374 0 0 0 112708 198 0 0 25 0 1 0 1788566925 127492096 18995 4294967295 134512640 135094434 3221224432 3218151088 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11212/statm): 31126 18995 145 145 0 30981 0
[pid=11212] vsize: 124504
Current children cumulated CPU time (s) 1129.06
Current children cumulated vsize (Kb) 126628

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 50374 0 0 0 113708 198 0 0 25 0 1 0 1788566925 127492096 18995 4294967295 134512640 135094434 3221224432 3217603552 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11212/statm): 31126 18995 145 145 0 30981 0
[pid=11212] vsize: 124504
Current children cumulated CPU time (s) 1139.06
Current children cumulated vsize (Kb) 126628

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 50374 0 0 0 114708 199 0 0 25 0 1 0 1788566925 127492096 18995 4294967295 134512640 135094434 3221224432 3216928064 134596866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11212/statm): 31126 18995 145 145 0 30981 0
[pid=11212] vsize: 124504
Current children cumulated CPU time (s) 1149.07
Current children cumulated vsize (Kb) 126628

[startup+1160.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 50374 0 0 0 115708 199 0 0 25 0 1 0 1788566925 127492096 18995 4294967295 134512640 135094434 3221224432 3215622496 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11212/statm): 31126 18995 145 145 0 30981 0
[pid=11212] vsize: 124504
Current children cumulated CPU time (s) 1159.07
Current children cumulated vsize (Kb) 126628

[startup+1170.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 50765 0 0 0 116705 200 0 0 25 0 1 0 1788566925 128540672 19303 4294967295 134512640 135094434 3221224432 3218057632 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11212/statm): 31382 19303 145 145 0 31237 0
[pid=11212] vsize: 125528
Current children cumulated CPU time (s) 1169.05
Current children cumulated vsize (Kb) 127652

[startup+1180.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 50914 0 0 0 117705 201 0 0 25 0 1 0 1788566925 129011712 19452 4294967295 134512640 135094434 3221224432 3220087264 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11212/statm): 31497 19452 145 145 0 31352 0
[pid=11212] vsize: 125988
Current children cumulated CPU time (s) 1179.06
Current children cumulated vsize (Kb) 128112

[startup+1190.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 50994 0 0 0 118704 201 0 0 25 0 1 0 1788566925 129265664 19532 4294967295 134512640 135094434 3221224432 3221199232 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11212/statm): 31559 19532 145 145 0 31414 0
[pid=11212] vsize: 126236
Current children cumulated CPU time (s) 1189.05
Current children cumulated vsize (Kb) 128360

[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 51202 0 0 0 119703 202 0 0 25 0 1 0 1788566925 141348864 19464 4294967295 134512640 135094434 3221224432 3218204944 134597020 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11212/statm): 34509 19464 145 145 0 34364 0
[pid=11212] vsize: 138036
Current children cumulated CPU time (s) 1199.05
Current children cumulated vsize (Kb) 140160

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 51302 0 0 0 120703 202 0 0 25 0 1 0 1788566925 141516800 19522 4294967295 134512640 135094434 3221224432 3219219584 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11212/statm): 34550 19522 145 145 0 34405 0
[pid=11212] vsize: 138200
Current children cumulated CPU time (s) 1209.05
Current children cumulated vsize (Kb) 140324



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11212
Raw data (/proc/11208/stat): 11208 (minisat+_script) S 11207 11208 1333 0 -1 0 289 239 0 0 0 0 0 0 20 0 1 0 1788566919 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11208/statm): 531 226 485 147 0 384 0
[pid=11208] vsize: 2124
Raw data (/proc/11212/stat): 11212 (minisat+_64-bit) R 11208 11208 1333 0 -1 0 51302 0 0 0 120703 202 0 0 25 0 1 0 1788566925 141516800 19522 4294967295 134512640 135094434 3221224432 3219219584 134597026 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11212/statm): 34550 19522 145 145 0 34405 0
[pid=11212] vsize: 138200
Current children cumulated CPU time (s) 1209.05
Current children cumulated vsize (Kb) 140324

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

Child status: 0
Real time (s): 1210.14
CPU time (s): 1209.1
CPU user time (s): 1207.04
CPU system time (s): 2.06369
CPU usage (%): 99.9141
Max. virtual memory (cumulated for all children) (Kb): 140324



Verifier Data




ERROR: no interpretation found !