Some explanations

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

General information on the benchmark

Namemps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-boeing2.opb
MD5SUM86934ee38968c649e6d8e09bdd8d93c2
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 2145
Biggest coefficient in the objective function 39321600000
Number of bits for the biggest coefficient in the objective function 36
Sum of the numbers in the objective function 2483529923827
Number of bits of the sum of numbers in the objective function 42
Biggest number in a constraint 1280000000000
Number of bits of the biggest number in a constraint 41
Biggest sum of numbers in a constraint 17827473345180
Number of bits of the biggest sum of numbers45
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables2319
Total number of constraints213
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints213
Minimum length of a constraint9
Maximum length of a constraint1580

Trace number 6067

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        916592 kB
Buffers:           192 kB
Cached:          92768 kB
SwapCached:        744 kB
Active:          24872 kB
Inactive:        70720 kB
HighTotal:      131008 kB
HighFree:        34020 kB
LowTotal:       903652 kB
LowFree:        882572 kB
SwapTotal:     2097136 kB
SwapFree:      2095884 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5664 kB
Slab:            16600 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 03:22:11 (client local time) WITH STATUS 0 IN 1205.83 SECONDS
stats: 3216 7 1205.83 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/9821/stat): 9821 (minisat+_script) R 9820 9821 15400 0 -1 0 19 0 0 0 0 0 0 0 21 0 1 0 1796935858 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/9821/statm): 174 3 169 147 0 27 0
[pid=9821] 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=9822
New process pid=9823
New process pid=9824
execve syscall for /bin/sed executable
One traced child (pid=9823) 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=9824) exited with status: 0
One traced child (pid=9822) exited with status: 0
New process pid=9825
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-boeing2.opb

[startup+10.004 s]
Raw data (loadavg): 0.90 0.96 0.91 1/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) T 9821 9821 15400 0 -1 0 35408 0 0 0 801 116 0 0 17 0 1 0 1796935863 102096896 24804 4294967295 134512640 135094434 3221224432 3221209484 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/9825/statm): 24926 24804 145 145 0 24781 0
[pid=9825] vsize: 99704
Current children cumulated CPU time (s) 9.19
Current children cumulated vsize (Kb) 101828

[startup+20.0047 s]
Raw data (loadavg): 0.92 0.96 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 69644 0 0 0 1624 215 0 0 25 0 1 0 1796935863 242323456 59040 4294967295 134512640 135094434 3221224432 3221210176 134597410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9825/statm): 59161 59040 145 145 0 59016 0
[pid=9825] vsize: 236644
Current children cumulated CPU time (s) 18.41
Current children cumulated vsize (Kb) 238768

[startup+30.0083 s]
Raw data (loadavg): 0.93 0.96 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 78654 0 0 0 2529 258 0 0 25 0 1 0 1796935863 149630976 36413 4294967295 134512640 135094434 3221224432 3221219500 134676382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36531 36413 145 145 0 36386 0
[pid=9825] vsize: 146124
Current children cumulated CPU time (s) 27.89
Current children cumulated vsize (Kb) 148248

[startup+40.0089 s]
Raw data (loadavg): 0.94 0.96 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 78654 0 0 0 3530 258 0 0 25 0 1 0 1796935863 149630976 36413 4294967295 134512640 135094434 3221224432 3221220632 134676609 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36531 36413 145 145 0 36386 0
[pid=9825] vsize: 146124
Current children cumulated CPU time (s) 37.9
Current children cumulated vsize (Kb) 148248

[startup+50.0105 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 78654 0 0 0 4530 258 0 0 25 0 1 0 1796935863 149630976 36413 4294967295 134512640 135094434 3221224432 3221220048 134676522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36531 36413 145 145 0 36386 0
[pid=9825] vsize: 146124
Current children cumulated CPU time (s) 47.9
Current children cumulated vsize (Kb) 148248

[startup+60.0112 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 78654 0 0 0 5530 258 0 0 25 0 1 0 1796935863 149630976 36413 4294967295 134512640 135094434 3221224432 3221219872 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36531 36413 145 145 0 36386 0
[pid=9825] vsize: 146124
Current children cumulated CPU time (s) 57.9
Current children cumulated vsize (Kb) 148248

[startup+70.0118 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 78654 0 0 0 6530 258 0 0 25 0 1 0 1796935863 149630976 36413 4294967295 134512640 135094434 3221224432 3221221600 134676245 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36531 36413 145 145 0 36386 0
[pid=9825] vsize: 146124
Current children cumulated CPU time (s) 67.9
Current children cumulated vsize (Kb) 148248

[startup+80.0124 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 78654 0 0 0 7530 258 0 0 25 0 1 0 1796935863 149630976 36413 4294967295 134512640 135094434 3221224432 3221221456 134600314 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36531 36413 145 145 0 36386 0
[pid=9825] vsize: 146124
Current children cumulated CPU time (s) 77.9
Current children cumulated vsize (Kb) 148248

[startup+90.0131 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 78654 0 0 0 8531 258 0 0 25 0 1 0 1796935863 149630976 36413 4294967295 134512640 135094434 3221224432 3221221456 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36531 36413 145 145 0 36386 0
[pid=9825] vsize: 146124
Current children cumulated CPU time (s) 87.91
Current children cumulated vsize (Kb) 148248

[startup+100.014 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 78654 0 0 0 9531 258 0 0 25 0 1 0 1796935863 149630976 36413 4294967295 134512640 135094434 3221224432 3221220048 134600144 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36531 36413 145 145 0 36386 0
[pid=9825] vsize: 146124
Current children cumulated CPU time (s) 97.91
Current children cumulated vsize (Kb) 148248

[startup+110.014 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 78654 0 0 0 10531 258 0 0 25 0 1 0 1796935863 149630976 36413 4294967295 134512640 135094434 3221224432 3221220208 134600162 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36531 36413 145 145 0 36386 0
[pid=9825] vsize: 146124
Current children cumulated CPU time (s) 107.91
Current children cumulated vsize (Kb) 148248

[startup+120.015 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 78654 0 0 0 11531 258 0 0 25 0 1 0 1796935863 149630976 36413 4294967295 134512640 135094434 3221224432 3221219872 134677290 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36531 36413 145 145 0 36386 0
[pid=9825] vsize: 146124
Current children cumulated CPU time (s) 117.91
Current children cumulated vsize (Kb) 148248

[startup+130.016 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 78654 0 0 0 12532 258 0 0 25 0 1 0 1796935863 149630976 36413 4294967295 134512640 135094434 3221224432 3221221104 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36531 36413 145 145 0 36386 0
[pid=9825] vsize: 146124
Current children cumulated CPU time (s) 127.92
Current children cumulated vsize (Kb) 148248

[startup+140.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 78654 0 0 0 13532 258 0 0 25 0 1 0 1796935863 149630976 36413 4294967295 134512640 135094434 3221224432 3221221104 134677239 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36531 36413 145 145 0 36386 0
[pid=9825] vsize: 146124
Current children cumulated CPU time (s) 137.92
Current children cumulated vsize (Kb) 148248

[startup+150.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 89241 0 0 0 14509 281 0 0 25 0 1 0 1796935863 192901120 46917 4294967295 134512640 135094434 3221224432 3221186736 134596997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 47095 46917 145 145 0 46950 0
[pid=9825] vsize: 188380
Current children cumulated CPU time (s) 147.92
Current children cumulated vsize (Kb) 190504

[startup+160.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 110332 0 0 0 15462 329 0 0 25 0 1 0 1796935863 236093440 57462 4294967295 134512640 135094434 3221224432 3221186304 134594847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 57640 57462 145 145 0 57495 0
[pid=9825] vsize: 230560
Current children cumulated CPU time (s) 157.93
Current children cumulated vsize (Kb) 232684

[startup+170.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 120736 0 0 0 16359 369 0 0 25 0 1 0 1796935863 278708224 67866 4294967295 134512640 135094434 3221224432 3221186384 134596848 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9825/statm): 68044 67866 145 145 0 67899 0
[pid=9825] vsize: 272176
Current children cumulated CPU time (s) 167.3
Current children cumulated vsize (Kb) 274300

[startup+180.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 170480 0 0 0 17184 498 0 0 25 0 1 0 1796935863 482459648 117610 4294967295 134512640 135094434 3221224432 3221185536 134597447 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 117788 117610 145 145 0 117643 0
[pid=9825] vsize: 471152
Current children cumulated CPU time (s) 176.84
Current children cumulated vsize (Kb) 473276

[startup+190.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 18106 533 0 0 25 0 1 0 1796935863 424931328 103565 4294967295 134512640 135094434 3221224432 3221223232 134596735 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9825/statm): 103743 103565 145 145 0 103598 0
[pid=9825] vsize: 414972
Current children cumulated CPU time (s) 186.41
Current children cumulated vsize (Kb) 417096

[startup+200.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 19087 547 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221219344 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 196.36
Current children cumulated vsize (Kb) 148304

[startup+210.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 20087 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221219696 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 206.37
Current children cumulated vsize (Kb) 148304

[startup+220.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 21086 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221219872 134677351 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 216.36
Current children cumulated vsize (Kb) 148304

[startup+230.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 22087 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221220048 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 226.37
Current children cumulated vsize (Kb) 148304

[startup+240.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 23087 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221220392 134600722 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 236.37
Current children cumulated vsize (Kb) 148304

[startup+250.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 24087 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221220576 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 246.37
Current children cumulated vsize (Kb) 148304

[startup+260.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 25087 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221220752 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 256.37
Current children cumulated vsize (Kb) 148304

[startup+270.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 26088 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221220208 134600246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 266.38
Current children cumulated vsize (Kb) 148304

[startup+280.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 27088 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221220048 134677346 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 276.38
Current children cumulated vsize (Kb) 148304

[startup+290.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 28088 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221219872 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 286.38
Current children cumulated vsize (Kb) 148304

[startup+300.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 29088 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221220384 134600167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 296.38
Current children cumulated vsize (Kb) 148304

[startup+310.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 30089 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221220752 134600151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 306.39
Current children cumulated vsize (Kb) 148304

[startup+320.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 31089 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221219968 134676311 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 316.39
Current children cumulated vsize (Kb) 148304

[startup+330.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 32089 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221220576 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 326.39
Current children cumulated vsize (Kb) 148304

[startup+340.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 33089 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 336.39
Current children cumulated vsize (Kb) 148304

[startup+350.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 34090 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221220048 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 346.4
Current children cumulated vsize (Kb) 148304

[startup+360.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 35090 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221220576 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 356.4
Current children cumulated vsize (Kb) 148304

[startup+370.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 36090 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221220912 134600162 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 366.4
Current children cumulated vsize (Kb) 148304

[startup+380.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 37090 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221220576 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 376.4
Current children cumulated vsize (Kb) 148304

[startup+390.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 38091 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221220576 134676598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 386.41
Current children cumulated vsize (Kb) 148304

[startup+400.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 39091 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221220808 134676461 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 396.41
Current children cumulated vsize (Kb) 148304

[startup+410.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 40091 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221220752 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 406.41
Current children cumulated vsize (Kb) 148304

[startup+420.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 41091 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221220400 134601029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 416.41
Current children cumulated vsize (Kb) 148304

[startup+430.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 42092 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221220644 134677085 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 426.42
Current children cumulated vsize (Kb) 148304

[startup+440.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 43092 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221220752 134600228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 436.42
Current children cumulated vsize (Kb) 148304

[startup+450.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 44092 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221221984 134600301 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 446.42
Current children cumulated vsize (Kb) 148304

[startup+460.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 45092 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221220400 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 456.42
Current children cumulated vsize (Kb) 148304

[startup+470.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 46092 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221220908 134676240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 466.42
Current children cumulated vsize (Kb) 148304

[startup+480.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 47093 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221220576 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 476.43
Current children cumulated vsize (Kb) 148304

[startup+490.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 48093 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221221200 134677138 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 486.43
Current children cumulated vsize (Kb) 148304

[startup+500.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 49093 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221220576 134600314 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 496.43
Current children cumulated vsize (Kb) 148304

[startup+510.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 50093 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221220496 134677007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 506.43
Current children cumulated vsize (Kb) 148304

[startup+520.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 51094 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221221620 134600159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 516.44
Current children cumulated vsize (Kb) 148304

[startup+530.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 52094 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 526.44
Current children cumulated vsize (Kb) 148304

[startup+540.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 53094 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221221456 134600314 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 536.44
Current children cumulated vsize (Kb) 148304

[startup+550.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 54094 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221220848 134676311 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 546.44
Current children cumulated vsize (Kb) 148304

[startup+560.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 55095 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221220896 134518674 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 556.45
Current children cumulated vsize (Kb) 148304

[startup+570.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 56095 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221221280 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 566.45
Current children cumulated vsize (Kb) 148304

[startup+580.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 57095 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221221104 134676516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 576.45
Current children cumulated vsize (Kb) 148304

[startup+590.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 58095 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221221104 134676589 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 586.45
Current children cumulated vsize (Kb) 148304

[startup+600.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 59096 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 596.46
Current children cumulated vsize (Kb) 148304

[startup+610.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 60096 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221220752 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 606.46
Current children cumulated vsize (Kb) 148304

[startup+620.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 61096 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221221092 134600238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 616.46
Current children cumulated vsize (Kb) 148304

[startup+630.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 62096 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221221804 134600154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 626.46
Current children cumulated vsize (Kb) 148304

[startup+640.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 63097 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221220848 134677049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 636.47
Current children cumulated vsize (Kb) 148304

[startup+650.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 64097 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221221280 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 646.47
Current children cumulated vsize (Kb) 148304

[startup+660.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 65097 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221221604 134676380 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 656.47
Current children cumulated vsize (Kb) 148304

[startup+670.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 66097 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221221632 134677346 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 666.47
Current children cumulated vsize (Kb) 148304

[startup+680.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 67098 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221221104 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 676.48
Current children cumulated vsize (Kb) 148304

[startup+690.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 68098 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221221104 134599953 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 686.48
Current children cumulated vsize (Kb) 148304

[startup+700.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 69098 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221221632 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 696.48
Current children cumulated vsize (Kb) 148304

[startup+710.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 70098 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221220576 134600225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 706.48
Current children cumulated vsize (Kb) 148304

[startup+720.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 71099 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 716.49
Current children cumulated vsize (Kb) 148304

[startup+730.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 72099 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221220928 134676601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 726.49
Current children cumulated vsize (Kb) 148304

[startup+740.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 73099 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221220752 134600151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 736.49
Current children cumulated vsize (Kb) 148304

[startup+750.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 74099 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221221104 134677340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 746.49
Current children cumulated vsize (Kb) 148304

[startup+760.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 75099 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221221264 134600241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 756.49
Current children cumulated vsize (Kb) 148304

[startup+770.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 76100 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221221808 134676519 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 766.5
Current children cumulated vsize (Kb) 148304

[startup+780.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177526 0 0 0 77100 548 0 0 25 0 1 0 1796935863 149688320 36367 4294967295 134512640 135094434 3221224432 3221222240 134676328 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36545 36367 145 145 0 36400 0
[pid=9825] vsize: 146180
Current children cumulated CPU time (s) 776.5
Current children cumulated vsize (Kb) 148304

[startup+790.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177639 0 0 0 78100 548 0 0 25 0 1 0 1796935863 150474752 36480 4294967295 134512640 135094434 3221224432 3221220224 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36737 36480 145 145 0 36592 0
[pid=9825] vsize: 146948
Current children cumulated CPU time (s) 786.5
Current children cumulated vsize (Kb) 149072

[startup+800.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177639 0 0 0 79100 548 0 0 25 0 1 0 1796935863 150474752 36480 4294967295 134512640 135094434 3221224432 3221221552 134676251 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36737 36480 145 145 0 36592 0
[pid=9825] vsize: 146948
Current children cumulated CPU time (s) 796.5
Current children cumulated vsize (Kb) 149072

[startup+810.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177639 0 0 0 80100 548 0 0 25 0 1 0 1796935863 150474752 36480 4294967295 134512640 135094434 3221224432 3221221376 134677042 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36737 36480 145 145 0 36592 0
[pid=9825] vsize: 146948
Current children cumulated CPU time (s) 806.5
Current children cumulated vsize (Kb) 149072

[startup+820.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 177639 0 0 0 81100 548 0 0 25 0 1 0 1796935863 150474752 36480 4294967295 134512640 135094434 3221224432 3221191600 134597239 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36737 36480 145 145 0 36592 0
[pid=9825] vsize: 146948
Current children cumulated CPU time (s) 816.5
Current children cumulated vsize (Kb) 149072

[startup+830.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 188185 0 0 0 82077 572 0 0 25 0 1 0 1796935863 193671168 47026 4294967295 134512640 135094434 3221224432 3221191840 134596842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 47283 47026 145 145 0 47138 0
[pid=9825] vsize: 189132
Current children cumulated CPU time (s) 826.51
Current children cumulated vsize (Kb) 191256

[startup+840.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 209276 0 0 0 83030 619 0 0 25 0 1 0 1796935863 236863488 57571 4294967295 134512640 135094434 3221224432 3221195008 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 57828 57571 145 145 0 57683 0
[pid=9825] vsize: 231312
Current children cumulated CPU time (s) 836.51
Current children cumulated vsize (Kb) 233436

[startup+850.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 222469 0 0 0 83900 670 0 0 25 0 1 0 1796935863 290902016 70764 4294967295 134512640 135094434 3221224432 3221223232 134596743 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 71021 70764 145 145 0 70876 0
[pid=9825] vsize: 284084
Current children cumulated CPU time (s) 845.72
Current children cumulated vsize (Kb) 286208

[startup+860.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 222469 0 0 0 84891 677 0 0 25 0 1 0 1796935863 150523904 36492 4294967295 134512640 135094434 3221224432 3221221088 134600162 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36749 36492 145 145 0 36604 0
[pid=9825] vsize: 146996
Current children cumulated CPU time (s) 855.7
Current children cumulated vsize (Kb) 149120

[startup+870.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 222469 0 0 0 85891 677 0 0 25 0 1 0 1796935863 150523904 36492 4294967295 134512640 135094434 3221224432 3221220048 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36749 36492 145 145 0 36604 0
[pid=9825] vsize: 146996
Current children cumulated CPU time (s) 865.7
Current children cumulated vsize (Kb) 149120

[startup+880.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 222469 0 0 0 86891 677 0 0 25 0 1 0 1796935863 150523904 36492 4294967295 134512640 135094434 3221224432 3221219616 134677059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36749 36492 145 145 0 36604 0
[pid=9825] vsize: 146996
Current children cumulated CPU time (s) 875.7
Current children cumulated vsize (Kb) 149120

[startup+890.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 222469 0 0 0 87892 677 0 0 25 0 1 0 1796935863 150523904 36492 4294967295 134512640 135094434 3221224432 3221220224 134677239 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36749 36492 145 145 0 36604 0
[pid=9825] vsize: 146996
Current children cumulated CPU time (s) 885.71
Current children cumulated vsize (Kb) 149120

[startup+900.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 222469 0 0 0 88892 677 0 0 25 0 1 0 1796935863 150523904 36492 4294967295 134512640 135094434 3221224432 3221220024 134676989 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36749 36492 145 145 0 36604 0
[pid=9825] vsize: 146996
Current children cumulated CPU time (s) 895.71
Current children cumulated vsize (Kb) 149120

[startup+910.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 222469 0 0 0 89892 677 0 0 25 0 1 0 1796935863 150523904 36492 4294967295 134512640 135094434 3221224432 3221219872 134676480 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36749 36492 145 145 0 36604 0
[pid=9825] vsize: 146996
Current children cumulated CPU time (s) 905.71
Current children cumulated vsize (Kb) 149120

[startup+920.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 222469 0 0 0 90892 677 0 0 25 0 1 0 1796935863 150523904 36492 4294967295 134512640 135094434 3221224432 3221220812 134677228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36749 36492 145 145 0 36604 0
[pid=9825] vsize: 146996
Current children cumulated CPU time (s) 915.71
Current children cumulated vsize (Kb) 149120

[startup+930.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 222469 0 0 0 91893 677 0 0 25 0 1 0 1796935863 150523904 36492 4294967295 134512640 135094434 3221224432 3221220048 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36749 36492 145 145 0 36604 0
[pid=9825] vsize: 146996
Current children cumulated CPU time (s) 925.72
Current children cumulated vsize (Kb) 149120

[startup+940.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 222469 0 0 0 92893 677 0 0 25 0 1 0 1796935863 150523904 36492 4294967295 134512640 135094434 3221224432 3221219576 134677229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36749 36492 145 145 0 36604 0
[pid=9825] vsize: 146996
Current children cumulated CPU time (s) 935.72
Current children cumulated vsize (Kb) 149120

[startup+950.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 222469 0 0 0 93893 677 0 0 25 0 1 0 1796935863 150523904 36492 4294967295 134512640 135094434 3221224432 3221220224 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36749 36492 145 145 0 36604 0
[pid=9825] vsize: 146996
Current children cumulated CPU time (s) 945.72
Current children cumulated vsize (Kb) 149120

[startup+960.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 222469 0 0 0 94893 677 0 0 25 0 1 0 1796935863 150523904 36492 4294967295 134512640 135094434 3221224432 3221219968 134676376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36749 36492 145 145 0 36604 0
[pid=9825] vsize: 146996
Current children cumulated CPU time (s) 955.72
Current children cumulated vsize (Kb) 149120

[startup+970.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 222469 0 0 0 95894 677 0 0 25 0 1 0 1796935863 150523904 36492 4294967295 134512640 135094434 3221224432 3221219872 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36749 36492 145 145 0 36604 0
[pid=9825] vsize: 146996
Current children cumulated CPU time (s) 965.73
Current children cumulated vsize (Kb) 149120

[startup+980.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 222469 0 0 0 96894 677 0 0 25 0 1 0 1796935863 150523904 36492 4294967295 134512640 135094434 3221224432 3221220752 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36749 36492 145 145 0 36604 0
[pid=9825] vsize: 146996
Current children cumulated CPU time (s) 975.73
Current children cumulated vsize (Kb) 149120

[startup+990.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 222469 0 0 0 97894 677 0 0 25 0 1 0 1796935863 150523904 36492 4294967295 134512640 135094434 3221224432 3221220048 134677346 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36749 36492 145 145 0 36604 0
[pid=9825] vsize: 146996
Current children cumulated CPU time (s) 985.73
Current children cumulated vsize (Kb) 149120

[startup+1000.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 222469 0 0 0 98894 677 0 0 25 0 1 0 1796935863 150523904 36492 4294967295 134512640 135094434 3221224432 3221220752 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36749 36492 145 145 0 36604 0
[pid=9825] vsize: 146996
Current children cumulated CPU time (s) 995.73
Current children cumulated vsize (Kb) 149120

[startup+1010.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 222469 0 0 0 99895 677 0 0 25 0 1 0 1796935863 150523904 36492 4294967295 134512640 135094434 3221224432 3221220208 134600162 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36749 36492 145 145 0 36604 0
[pid=9825] vsize: 146996
Current children cumulated CPU time (s) 1005.74
Current children cumulated vsize (Kb) 149120

[startup+1020.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 222469 0 0 0 100895 677 0 0 25 0 1 0 1796935863 150523904 36492 4294967295 134512640 135094434 3221224432 3221220496 134677059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36749 36492 145 145 0 36604 0
[pid=9825] vsize: 146996
Current children cumulated CPU time (s) 1015.74
Current children cumulated vsize (Kb) 149120

[startup+1030.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 222469 0 0 0 101895 677 0 0 25 0 1 0 1796935863 150523904 36492 4294967295 134512640 135094434 3221224432 3221221080 134676989 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36749 36492 145 145 0 36604 0
[pid=9825] vsize: 146996
Current children cumulated CPU time (s) 1025.74
Current children cumulated vsize (Kb) 149120

[startup+1040.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 222469 0 0 0 102895 677 0 0 25 0 1 0 1796935863 150523904 36492 4294967295 134512640 135094434 3221224432 3221220400 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36749 36492 145 145 0 36604 0
[pid=9825] vsize: 146996
Current children cumulated CPU time (s) 1035.74
Current children cumulated vsize (Kb) 149120

[startup+1050.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 222469 0 0 0 103895 677 0 0 25 0 1 0 1796935863 150523904 36492 4294967295 134512640 135094434 3221224432 3221220224 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36749 36492 145 145 0 36604 0
[pid=9825] vsize: 146996
Current children cumulated CPU time (s) 1045.74
Current children cumulated vsize (Kb) 149120

[startup+1060.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 222469 0 0 0 104895 677 0 0 25 0 1 0 1796935863 150523904 36492 4294967295 134512640 135094434 3221224432 3221220224 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36749 36492 145 145 0 36604 0
[pid=9825] vsize: 146996
Current children cumulated CPU time (s) 1055.74
Current children cumulated vsize (Kb) 149120

[startup+1070.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 222469 0 0 0 105896 677 0 0 25 0 1 0 1796935863 150523904 36492 4294967295 134512640 135094434 3221224432 3221221168 134677091 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36749 36492 145 145 0 36604 0
[pid=9825] vsize: 146996
Current children cumulated CPU time (s) 1065.75
Current children cumulated vsize (Kb) 149120

[startup+1080.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 222469 0 0 0 106896 677 0 0 25 0 1 0 1796935863 150523904 36492 4294967295 134512640 135094434 3221224432 3221220224 134677248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36749 36492 145 145 0 36604 0
[pid=9825] vsize: 146996
Current children cumulated CPU time (s) 1075.75
Current children cumulated vsize (Kb) 149120

[startup+1090.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 222469 0 0 0 107896 677 0 0 25 0 1 0 1796935863 150523904 36492 4294967295 134512640 135094434 3221224432 3221220432 134781392 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36749 36492 145 145 0 36604 0
[pid=9825] vsize: 146996
Current children cumulated CPU time (s) 1085.75
Current children cumulated vsize (Kb) 149120

[startup+1100.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 222469 0 0 0 108896 677 0 0 25 0 1 0 1796935863 150523904 36492 4294967295 134512640 135094434 3221224432 3221220380 134676988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36749 36492 145 145 0 36604 0
[pid=9825] vsize: 146996
Current children cumulated CPU time (s) 1095.75
Current children cumulated vsize (Kb) 149120

[startup+1110.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 222469 0 0 0 109896 677 0 0 25 0 1 0 1796935863 150523904 36492 4294967295 134512640 135094434 3221224432 3221221104 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36749 36492 145 145 0 36604 0
[pid=9825] vsize: 146996
Current children cumulated CPU time (s) 1105.75
Current children cumulated vsize (Kb) 149120

[startup+1120.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 222469 0 0 0 110897 677 0 0 25 0 1 0 1796935863 150523904 36492 4294967295 134512640 135094434 3221224432 3221220928 134677313 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36749 36492 145 145 0 36604 0
[pid=9825] vsize: 146996
Current children cumulated CPU time (s) 1115.76
Current children cumulated vsize (Kb) 149120

[startup+1130.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 222469 0 0 0 111897 677 0 0 25 0 1 0 1796935863 150523904 36492 4294967295 134512640 135094434 3221224432 3221220048 134677300 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36749 36492 145 145 0 36604 0
[pid=9825] vsize: 146996
Current children cumulated CPU time (s) 1125.76
Current children cumulated vsize (Kb) 149120

[startup+1140.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 222469 0 0 0 112897 677 0 0 25 0 1 0 1796935863 150523904 36492 4294967295 134512640 135094434 3221224432 3221221104 134599953 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36749 36492 145 145 0 36604 0
[pid=9825] vsize: 146996
Current children cumulated CPU time (s) 1135.76
Current children cumulated vsize (Kb) 149120

[startup+1150.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 222469 0 0 0 113897 677 0 0 25 0 1 0 1796935863 150523904 36492 4294967295 134512640 135094434 3221224432 3221220640 134676336 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36749 36492 145 145 0 36604 0
[pid=9825] vsize: 146996
Current children cumulated CPU time (s) 1145.76
Current children cumulated vsize (Kb) 149120

[startup+1160.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 222469 0 0 0 114898 677 0 0 25 0 1 0 1796935863 150523904 36492 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36749 36492 145 145 0 36604 0
[pid=9825] vsize: 146996
Current children cumulated CPU time (s) 1155.77
Current children cumulated vsize (Kb) 149120

[startup+1170.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 222469 0 0 0 115898 677 0 0 25 0 1 0 1796935863 150523904 36492 4294967295 134512640 135094434 3221224432 3221221456 134600314 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36749 36492 145 145 0 36604 0
[pid=9825] vsize: 146996
Current children cumulated CPU time (s) 1165.77
Current children cumulated vsize (Kb) 149120

[startup+1180.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 222469 0 0 0 116898 677 0 0 25 0 1 0 1796935863 150523904 36492 4294967295 134512640 135094434 3221224432 3221220400 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36749 36492 145 145 0 36604 0
[pid=9825] vsize: 146996
Current children cumulated CPU time (s) 1175.77
Current children cumulated vsize (Kb) 149120

[startup+1190.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 222469 0 0 0 117898 677 0 0 25 0 1 0 1796935863 150523904 36492 4294967295 134512640 135094434 3221224432 3221220752 134676510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36749 36492 145 145 0 36604 0
[pid=9825] vsize: 146996
Current children cumulated CPU time (s) 1185.77
Current children cumulated vsize (Kb) 149120

[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 222469 0 0 0 118898 677 0 0 25 0 1 0 1796935863 150523904 36492 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36749 36492 145 145 0 36604 0
[pid=9825] vsize: 146996
Current children cumulated CPU time (s) 1195.77
Current children cumulated vsize (Kb) 149120

[startup+1210.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 222469 0 0 0 119899 677 0 0 25 0 1 0 1796935863 150523904 36492 4294967295 134512640 135094434 3221224432 3221220400 134677300 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36749 36492 145 145 0 36604 0
[pid=9825] vsize: 146996
Current children cumulated CPU time (s) 1205.78
Current children cumulated vsize (Kb) 149120



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9825
Raw data (/proc/9821/stat): 9821 (minisat+_script) S 9820 9821 15400 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796935858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9821/statm): 531 226 485 147 0 384 0
[pid=9821] vsize: 2124
Raw data (/proc/9825/stat): 9825 (minisat+_64-bit) R 9821 9821 15400 0 -1 0 222469 0 0 0 119899 677 0 0 25 0 1 0 1796935863 150523904 36492 4294967295 134512640 135094434 3221224432 3221220400 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9825/statm): 36749 36492 145 145 0 36604 0
[pid=9825] vsize: 146996
Current children cumulated CPU time (s) 1205.78
Current children cumulated vsize (Kb) 149120

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

Child status: 0
Real time (s): 1210.14
CPU time (s): 1205.83
CPU user time (s): 1198.99
CPU system time (s): 6.83996
CPU usage (%): 99.6442
Max. virtual memory (cumulated for all children) (Kb): 473276



Verifier Data




ERROR: no interpretation found !