Some explanations

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

General information on the benchmark

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

Trace number 4539

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        861928 kB
Buffers:         37328 kB
Cached:         106108 kB
SwapCached:        792 kB
Active:          85372 kB
Inactive:        60680 kB
HighTotal:      131008 kB
HighFree:        21756 kB
LowTotal:       903652 kB
LowFree:        840172 kB
SwapTotal:     2097136 kB
SwapFree:      2095868 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5696 kB
Slab:            21104 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-19 18:26:01 (client local time) WITH STATUS 0 IN 1209.04 SECONDS
stats: 2994 7 1209.04 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/22514/stat): 22514 (minisat+_script) R 22513 22514 5299 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1851932766 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/22514/statm): 174 3 169 147 0 27 0
[pid=22514] 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=22515
New process pid=22516
New process pid=22517
execve syscall for /bin/sed executable
One traced child (pid=22516) 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=22517) exited with status: 0
One traced child (pid=22515) exited with status: 0
New process pid=22518
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-nw04.opb

[startup+10.003 s]
Raw data (loadavg): 0.88 0.94 0.87 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 26703 0 0 0 824 102 0 0 25 0 1 0 1851932771 69652480 6699 4294967295 134512640 135094434 3221224432 3221218848 134589807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22518/statm): 17005 6699 145 145 0 16860 0
[pid=22518] vsize: 68020
Current children cumulated CPU time (s) 9.28
Current children cumulated vsize (Kb) 70144

[startup+20.0046 s]
Raw data (loadavg): 0.89 0.94 0.87 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 32924 0 0 0 1786 123 0 0 25 0 1 0 1851932771 84213760 8554 4294967295 134512640 135094434 3221224432 3220559472 134596866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22518/statm): 20560 8554 145 145 0 20415 0
[pid=22518] vsize: 82240
Current children cumulated CPU time (s) 19.11
Current children cumulated vsize (Kb) 84364

[startup+30.0053 s]
Raw data (loadavg): 0.91 0.94 0.87 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 32924 0 0 0 2786 123 0 0 25 0 1 0 1851932771 84213760 8554 4294967295 134512640 135094434 3221224432 3220978880 134597091 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22518/statm): 20560 8554 145 145 0 20415 0
[pid=22518] vsize: 82240
Current children cumulated CPU time (s) 29.11
Current children cumulated vsize (Kb) 84364

[startup+40.0059 s]
Raw data (loadavg): 0.92 0.94 0.87 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 33254 0 0 0 3785 124 0 0 25 0 1 0 1851932771 85565440 8884 4294967295 134512640 135094434 3221224432 3220192512 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22518/statm): 20890 8884 145 145 0 20745 0
[pid=22518] vsize: 83560
Current children cumulated CPU time (s) 39.11
Current children cumulated vsize (Kb) 85684

[startup+50.0065 s]
Raw data (loadavg): 0.93 0.95 0.87 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 33280 0 0 0 4784 125 0 0 25 0 1 0 1851932771 85671936 8910 4294967295 134512640 135094434 3221224432 3220890000 134597084 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22518/statm): 20916 8910 145 145 0 20771 0
[pid=22518] vsize: 83664
Current children cumulated CPU time (s) 49.11
Current children cumulated vsize (Kb) 85788

[startup+60.0061 s]
Raw data (loadavg): 0.94 0.95 0.87 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 33999 0 0 0 5783 127 0 0 25 0 1 0 1851932771 89976832 9629 4294967295 134512640 135094434 3221224432 3218905248 134597094 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22518/statm): 21967 9629 145 145 0 21822 0
[pid=22518] vsize: 87868
Current children cumulated CPU time (s) 59.12
Current children cumulated vsize (Kb) 89992

[startup+70.0068 s]
Raw data (loadavg): 0.95 0.95 0.88 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 34037 0 0 0 6783 127 0 0 25 0 1 0 1851932771 89976832 9667 4294967295 134512640 135094434 3221224432 3221188144 134597017 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22518/statm): 21967 9667 145 145 0 21822 0
[pid=22518] vsize: 87868
Current children cumulated CPU time (s) 69.12
Current children cumulated vsize (Kb) 89992

[startup+80.0074 s]
Raw data (loadavg): 0.96 0.95 0.88 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 34038 0 0 0 7783 127 0 0 25 0 1 0 1851932771 89976832 9668 4294967295 134512640 135094434 3221224432 3217982480 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22518/statm): 21967 9668 145 145 0 21822 0
[pid=22518] vsize: 87868
Current children cumulated CPU time (s) 79.12
Current children cumulated vsize (Kb) 89992

[startup+90.008 s]
Raw data (loadavg): 0.96 0.95 0.88 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 34785 0 0 0 8781 129 0 0 25 0 1 0 1851932771 91324416 10085 4294967295 134512640 135094434 3221224432 3220393504 134596860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22518/statm): 22296 10085 145 145 0 22151 0
[pid=22518] vsize: 89184
Current children cumulated CPU time (s) 89.12
Current children cumulated vsize (Kb) 91308

[startup+100.009 s]
Raw data (loadavg): 0.97 0.95 0.88 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 34870 0 0 0 9780 130 0 0 25 0 1 0 1851932771 91324416 10170 4294967295 134512640 135094434 3221224432 3220313600 134597046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22518/statm): 22296 10170 145 145 0 22151 0
[pid=22518] vsize: 89184
Current children cumulated CPU time (s) 99.12
Current children cumulated vsize (Kb) 91308

[startup+110.009 s]
Raw data (loadavg): 0.97 0.95 0.88 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 34932 0 0 0 10780 131 0 0 25 0 1 0 1851932771 91324416 10232 4294967295 134512640 135094434 3221224432 3220070016 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22518/statm): 22296 10232 145 145 0 22151 0
[pid=22518] vsize: 89184
Current children cumulated CPU time (s) 109.13
Current children cumulated vsize (Kb) 91308

[startup+120.01 s]
Raw data (loadavg): 0.98 0.95 0.88 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 35039 0 0 0 11779 132 0 0 25 0 1 0 1851932771 94605312 10339 4294967295 134512640 135094434 3221224432 3219929744 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22518/statm): 23097 10339 145 145 0 22952 0
[pid=22518] vsize: 92388
Current children cumulated CPU time (s) 119.13
Current children cumulated vsize (Kb) 94512

[startup+130.01 s]
Raw data (loadavg): 0.98 0.95 0.88 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 35060 0 0 0 12779 132 0 0 25 0 1 0 1851932771 94605312 10360 4294967295 134512640 135094434 3221224432 3219506464 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22518/statm): 23097 10360 145 145 0 22952 0
[pid=22518] vsize: 92388
Current children cumulated CPU time (s) 129.13
Current children cumulated vsize (Kb) 94512

[startup+140.01 s]
Raw data (loadavg): 0.98 0.95 0.88 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 35426 0 0 0 13777 134 0 0 25 0 1 0 1851932771 95125504 10569 4294967295 134512640 135094434 3221224432 3220206768 134597084 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22518/statm): 23224 10569 145 145 0 23079 0
[pid=22518] vsize: 92896
Current children cumulated CPU time (s) 139.13
Current children cumulated vsize (Kb) 95020

[startup+150.011 s]
Raw data (loadavg): 0.98 0.95 0.88 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 35453 0 0 0 14777 134 0 0 25 0 1 0 1851932771 95166464 10596 4294967295 134512640 135094434 3221224432 3219502416 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22518/statm): 23234 10596 145 145 0 23089 0
[pid=22518] vsize: 92936
Current children cumulated CPU time (s) 149.13
Current children cumulated vsize (Kb) 95060

[startup+160.01 s]
Raw data (loadavg): 0.99 0.96 0.88 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 36308 0 0 0 15773 137 0 0 25 0 1 0 1851932771 97603584 11270 4294967295 134512640 135094434 3221224432 3217906800 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22518/statm): 23829 11270 145 145 0 23684 0
[pid=22518] vsize: 95316
Current children cumulated CPU time (s) 159.12
Current children cumulated vsize (Kb) 97440

[startup+170.012 s]
Raw data (loadavg): 0.99 0.96 0.89 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 37720 0 0 0 16768 142 0 0 25 0 1 0 1851932771 100405248 11984 4294967295 134512640 135094434 3221224432 3219685984 134597026 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22518/statm): 24513 11984 145 145 0 24368 0
[pid=22518] vsize: 98052
Current children cumulated CPU time (s) 169.12
Current children cumulated vsize (Kb) 100176

[startup+180.013 s]
Raw data (loadavg): 0.99 0.96 0.89 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 37868 0 0 0 17766 144 0 0 25 0 1 0 1851932771 100777984 12090 4294967295 134512640 135094434 3221224432 3220575840 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22518/statm): 24604 12090 145 145 0 24459 0
[pid=22518] vsize: 98416
Current children cumulated CPU time (s) 179.12
Current children cumulated vsize (Kb) 100540

[startup+190.015 s]
Raw data (loadavg): 0.99 0.96 0.89 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 37915 0 0 0 18765 144 0 0 25 0 1 0 1851932771 100925440 12137 4294967295 134512640 135094434 3221224432 3220892112 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22518/statm): 24640 12137 145 145 0 24495 0
[pid=22518] vsize: 98560
Current children cumulated CPU time (s) 189.11
Current children cumulated vsize (Kb) 100684

[startup+200.016 s]
Raw data (loadavg): 0.99 0.96 0.89 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 37915 0 0 0 19765 145 0 0 25 0 1 0 1851932771 100925440 12137 4294967295 134512640 135094434 3221224432 3219341552 134596852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22518/statm): 24640 12137 145 145 0 24495 0
[pid=22518] vsize: 98560
Current children cumulated CPU time (s) 199.12
Current children cumulated vsize (Kb) 100684

[startup+210.016 s]
Raw data (loadavg): 0.99 0.96 0.89 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 37915 0 0 0 20765 145 0 0 25 0 1 0 1851932771 100925440 12137 4294967295 134512640 135094434 3221224432 3218391504 134596919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22518/statm): 24640 12137 145 145 0 24495 0
[pid=22518] vsize: 98560
Current children cumulated CPU time (s) 209.12
Current children cumulated vsize (Kb) 100684

[startup+220.016 s]
Raw data (loadavg): 0.99 0.96 0.89 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 38004 0 0 0 21763 146 0 0 25 0 1 0 1851932771 101208064 12226 4294967295 134512640 135094434 3221224432 3217467328 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22518/statm): 24709 12226 145 145 0 24564 0
[pid=22518] vsize: 98836
Current children cumulated CPU time (s) 219.11
Current children cumulated vsize (Kb) 100960

[startup+230.017 s]
Raw data (loadavg): 0.99 0.96 0.89 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 38403 0 0 0 22760 148 0 0 25 0 1 0 1851932771 102285312 12542 4294967295 134512640 135094434 3221224432 3220665248 134597012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22518/statm): 24972 12542 145 145 0 24827 0
[pid=22518] vsize: 99888
Current children cumulated CPU time (s) 229.1
Current children cumulated vsize (Kb) 102012

[startup+240.017 s]
Raw data (loadavg): 0.99 0.96 0.89 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 38620 0 0 0 23758 149 0 0 25 0 1 0 1851932771 101908480 12504 4294967295 134512640 135094434 3221224432 3219438704 134597017 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22518/statm): 24880 12504 145 145 0 24735 0
[pid=22518] vsize: 99520
Current children cumulated CPU time (s) 239.09
Current children cumulated vsize (Kb) 101644

[startup+250.018 s]
Raw data (loadavg): 0.99 0.96 0.89 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 38724 0 0 0 24758 150 0 0 25 0 1 0 1851932771 102076416 12566 4294967295 134512640 135094434 3221224432 3220697984 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22518/statm): 24921 12566 145 145 0 24776 0
[pid=22518] vsize: 99684
Current children cumulated CPU time (s) 249.1
Current children cumulated vsize (Kb) 101808

[startup+260.019 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 38733 0 0 0 25758 150 0 0 25 0 1 0 1851932771 102076416 12575 4294967295 134512640 135094434 3221224432 3220247952 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22518/statm): 24921 12575 145 145 0 24776 0
[pid=22518] vsize: 99684
Current children cumulated CPU time (s) 259.1
Current children cumulated vsize (Kb) 101808

[startup+270.019 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 38733 0 0 0 26758 150 0 0 25 0 1 0 1851932771 102076416 12575 4294967295 134512640 135094434 3221224432 3219075616 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22518/statm): 24921 12575 145 145 0 24776 0
[pid=22518] vsize: 99684
Current children cumulated CPU time (s) 269.1
Current children cumulated vsize (Kb) 101808

[startup+280.02 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) T 22514 22514 5299 0 -1 0 38903 0 0 0 27755 152 0 0 25 0 1 0 1851932771 102584320 12745 4294967295 134512640 135094434 3221224432 3219553212 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/22518/statm): 25045 12745 145 145 0 24900 0
[pid=22518] vsize: 100180
Current children cumulated CPU time (s) 279.09
Current children cumulated vsize (Kb) 102304

[startup+290.022 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 39303 0 0 0 28754 153 0 0 25 0 1 0 1851932771 102793216 12854 4294967295 134512640 135094434 3221224432 3219223104 134597020 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 25096 12854 145 145 0 24951 0
[pid=22518] vsize: 100384
Current children cumulated CPU time (s) 289.09
Current children cumulated vsize (Kb) 102508

[startup+300.022 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 39374 0 0 0 29754 153 0 0 25 0 1 0 1851932771 102801408 12885 4294967295 134512640 135094434 3221224432 3221003696 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 25098 12885 145 145 0 24953 0
[pid=22518] vsize: 100392
Current children cumulated CPU time (s) 299.09
Current children cumulated vsize (Kb) 102516

[startup+310.023 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 39461 0 0 0 30754 153 0 0 25 0 1 0 1851932771 102969344 12930 4294967295 134512640 135094434 3221224432 3220133024 134596919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 25139 12930 145 145 0 24994 0
[pid=22518] vsize: 100556
Current children cumulated CPU time (s) 309.09
Current children cumulated vsize (Kb) 102680

[startup+320.023 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 39654 0 0 0 31752 154 0 0 25 0 1 0 1851932771 103546880 13123 4294967295 134512640 135094434 3221224432 3220510016 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 25280 13123 145 145 0 25135 0
[pid=22518] vsize: 101120
Current children cumulated CPU time (s) 319.08
Current children cumulated vsize (Kb) 103244

[startup+330.024 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 40052 0 0 0 32751 155 0 0 25 0 1 0 1851932771 103542784 13181 4294967295 134512640 135094434 3221224432 3219453312 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 25279 13181 145 145 0 25134 0
[pid=22518] vsize: 101116
Current children cumulated CPU time (s) 329.08
Current children cumulated vsize (Kb) 103240

[startup+340.025 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 40167 0 0 0 33751 155 0 0 25 0 1 0 1851932771 103759872 13254 4294967295 134512640 135094434 3221224432 3220620544 134597094 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 25332 13254 145 145 0 25187 0
[pid=22518] vsize: 101328
Current children cumulated CPU time (s) 339.08
Current children cumulated vsize (Kb) 103452

[startup+350.025 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 40210 0 0 0 34751 155 0 0 25 0 1 0 1851932771 103895040 13297 4294967295 134512640 135094434 3221224432 3220184416 134596860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 25365 13297 145 145 0 25220 0
[pid=22518] vsize: 101460
Current children cumulated CPU time (s) 349.08
Current children cumulated vsize (Kb) 103584

[startup+360.026 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 40210 0 0 0 35751 155 0 0 25 0 1 0 1851932771 103895040 13297 4294967295 134512640 135094434 3221224432 3219318672 134596857 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 25365 13297 145 145 0 25220 0
[pid=22518] vsize: 101460
Current children cumulated CPU time (s) 359.08
Current children cumulated vsize (Kb) 103584

[startup+370.026 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 40210 0 0 0 36752 155 0 0 25 0 1 0 1851932771 103895040 13297 4294967295 134512640 135094434 3221224432 3217204208 134596875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 25365 13297 145 145 0 25220 0
[pid=22518] vsize: 101460
Current children cumulated CPU time (s) 369.09
Current children cumulated vsize (Kb) 103584

[startup+380.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 40680 0 0 0 37748 157 0 0 25 0 1 0 1851932771 111489024 13684 4294967295 134512640 135094434 3221224432 3220783168 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 27219 13684 145 145 0 27074 0
[pid=22518] vsize: 108876
Current children cumulated CPU time (s) 379.07
Current children cumulated vsize (Kb) 111000

[startup+390.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 40897 0 0 0 38748 158 0 0 25 0 1 0 1851932771 111083520 13642 4294967295 134512640 135094434 3221224432 3219429200 134597037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 27120 13642 145 145 0 26975 0
[pid=22518] vsize: 108480
Current children cumulated CPU time (s) 389.08
Current children cumulated vsize (Kb) 110604

[startup+400.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 40999 0 0 0 39748 158 0 0 25 0 1 0 1851932771 111251456 13702 4294967295 134512640 135094434 3221224432 3220581472 134597094 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 27161 13702 145 145 0 27016 0
[pid=22518] vsize: 108644
Current children cumulated CPU time (s) 399.08
Current children cumulated vsize (Kb) 110768

[startup+410.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 41016 0 0 0 40748 158 0 0 25 0 1 0 1851932771 111280128 13719 4294967295 134512640 135094434 3221224432 3220154496 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 27168 13719 145 145 0 27023 0
[pid=22518] vsize: 108672
Current children cumulated CPU time (s) 409.08
Current children cumulated vsize (Kb) 110796

[startup+420.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 41016 0 0 0 41748 158 0 0 25 0 1 0 1851932771 111280128 13719 4294967295 134512640 135094434 3221224432 3219347536 134596888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 27168 13719 145 145 0 27023 0
[pid=22518] vsize: 108672
Current children cumulated CPU time (s) 419.08
Current children cumulated vsize (Kb) 110796

[startup+430.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 41016 0 0 0 42749 158 0 0 25 0 1 0 1851932771 111280128 13719 4294967295 134512640 135094434 3221224432 3217416816 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 27168 13719 145 145 0 27023 0
[pid=22518] vsize: 108672
Current children cumulated CPU time (s) 429.09
Current children cumulated vsize (Kb) 110796

[startup+440.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 41442 0 0 0 43746 160 0 0 25 0 1 0 1851932771 112439296 14062 4294967295 134512640 135094434 3221224432 3220074240 134597020 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 27451 14062 145 145 0 27306 0
[pid=22518] vsize: 109804
Current children cumulated CPU time (s) 439.08
Current children cumulated vsize (Kb) 111928

[startup+450.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 41696 0 0 0 44745 160 0 0 25 0 1 0 1851932771 112197632 14056 4294967295 134512640 135094434 3221224432 3218464368 134597053 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22518/statm): 27392 14056 145 145 0 27247 0
[pid=22518] vsize: 109568
Current children cumulated CPU time (s) 449.07
Current children cumulated vsize (Kb) 111692

[startup+460.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 41722 0 0 0 45745 160 0 0 25 0 1 0 1851932771 112197632 14082 4294967295 134512640 135094434 3221224432 3220055584 134597094 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 27392 14082 145 145 0 27247 0
[pid=22518] vsize: 109568
Current children cumulated CPU time (s) 459.07
Current children cumulated vsize (Kb) 111692

[startup+470.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 41820 0 0 0 46745 160 0 0 25 0 1 0 1851932771 112365568 14138 4294967295 134512640 135094434 3221224432 3220935936 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 27433 14138 145 145 0 27288 0
[pid=22518] vsize: 109732
Current children cumulated CPU time (s) 469.07
Current children cumulated vsize (Kb) 111856

[startup+480.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 41828 0 0 0 47745 160 0 0 25 0 1 0 1851932771 112377856 14146 4294967295 134512640 135094434 3221224432 3219772576 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 27436 14146 145 145 0 27291 0
[pid=22518] vsize: 109744
Current children cumulated CPU time (s) 479.07
Current children cumulated vsize (Kb) 111868

[startup+490.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 41828 0 0 0 48746 160 0 0 25 0 1 0 1851932771 112377856 14146 4294967295 134512640 135094434 3221224432 3218815664 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 27436 14146 145 145 0 27291 0
[pid=22518] vsize: 109744
Current children cumulated CPU time (s) 489.08
Current children cumulated vsize (Kb) 111868

[startup+500.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 41828 0 0 0 49746 161 0 0 25 0 1 0 1851932771 112377856 14146 4294967295 134512640 135094434 3221224432 3216523968 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 27436 14146 145 145 0 27291 0
[pid=22518] vsize: 109744
Current children cumulated CPU time (s) 499.09
Current children cumulated vsize (Kb) 111868

[startup+510.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 42309 0 0 0 50744 162 0 0 25 0 1 0 1851932771 113713152 14544 4294967295 134512640 135094434 3221224432 3220788272 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 27762 14544 145 145 0 27617 0
[pid=22518] vsize: 111048
Current children cumulated CPU time (s) 509.08
Current children cumulated vsize (Kb) 113172

[startup+520.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 42525 0 0 0 51743 163 0 0 25 0 1 0 1851932771 113307648 14499 4294967295 134512640 135094434 3221224432 3219109408 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 27663 14499 145 145 0 27518 0
[pid=22518] vsize: 110652
Current children cumulated CPU time (s) 519.08
Current children cumulated vsize (Kb) 112776

[startup+530.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 42627 0 0 0 52743 163 0 0 25 0 1 0 1851932771 113475584 14559 4294967295 134512640 135094434 3221224432 3220252176 134597040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 27704 14559 145 145 0 27559 0
[pid=22518] vsize: 110816
Current children cumulated CPU time (s) 529.08
Current children cumulated vsize (Kb) 112940

[startup+540.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 42640 0 0 0 53743 163 0 0 25 0 1 0 1851932771 113475584 14572 4294967295 134512640 135094434 3221224432 3221013024 134597040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 27704 14572 145 145 0 27559 0
[pid=22518] vsize: 110816
Current children cumulated CPU time (s) 539.08
Current children cumulated vsize (Kb) 112940

[startup+550.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 42653 0 0 0 54743 163 0 0 25 0 1 0 1851932771 113516544 14585 4294967295 134512640 135094434 3221224432 3219602736 134596860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 27714 14585 145 145 0 27569 0
[pid=22518] vsize: 110856
Current children cumulated CPU time (s) 549.08
Current children cumulated vsize (Kb) 112980

[startup+560.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 42653 0 0 0 55743 163 0 0 25 0 1 0 1851932771 113516544 14585 4294967295 134512640 135094434 3221224432 3218745440 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 27714 14585 145 145 0 27569 0
[pid=22518] vsize: 110856
Current children cumulated CPU time (s) 559.08
Current children cumulated vsize (Kb) 112980

[startup+570.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 42653 0 0 0 56743 163 0 0 25 0 1 0 1851932771 113516544 14585 4294967295 134512640 135094434 3221224432 3216770544 134596912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 27714 14585 145 145 0 27569 0
[pid=22518] vsize: 110856
Current children cumulated CPU time (s) 569.08
Current children cumulated vsize (Kb) 112980

[startup+580.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 45727 0 0 0 57734 171 0 0 25 0 1 0 1851932771 120115200 16258 4294967295 134512640 135094434 3221224432 3220034288 134597026 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 29325 16258 145 145 0 29180 0
[pid=22518] vsize: 117300
Current children cumulated CPU time (s) 579.07
Current children cumulated vsize (Kb) 119424

[startup+590.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 45983 0 0 0 58733 172 0 0 25 0 1 0 1851932771 120029184 16291 4294967295 134512640 135094434 3221224432 3217708448 134597091 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 29304 16291 145 145 0 29159 0
[pid=22518] vsize: 117216
Current children cumulated CPU time (s) 589.07
Current children cumulated vsize (Kb) 119340

[startup+600.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 46056 0 0 0 59733 172 0 0 25 0 1 0 1851932771 120037376 16324 4294967295 134512640 135094434 3221224432 3219542720 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 29306 16324 145 145 0 29161 0
[pid=22518] vsize: 117224
Current children cumulated CPU time (s) 599.07
Current children cumulated vsize (Kb) 119348

[startup+610.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 46154 0 0 0 60733 172 0 0 25 0 1 0 1851932771 120205312 16380 4294967295 134512640 135094434 3221224432 3220474464 134597017 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 29347 16380 145 145 0 29202 0
[pid=22518] vsize: 117388
Current children cumulated CPU time (s) 609.07
Current children cumulated vsize (Kb) 119512

[startup+620.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 46185 0 0 0 61733 172 0 0 25 0 1 0 1851932771 120283136 16411 4294967295 134512640 135094434 3221224432 3221149248 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 29366 16411 145 145 0 29221 0
[pid=22518] vsize: 117464
Current children cumulated CPU time (s) 619.07
Current children cumulated vsize (Kb) 119588

[startup+630.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 46191 0 0 0 62733 172 0 0 25 0 1 0 1851932771 120303616 16417 4294967295 134512640 135094434 3221224432 3219293504 134596921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 29371 16417 145 145 0 29226 0
[pid=22518] vsize: 117484
Current children cumulated CPU time (s) 629.07
Current children cumulated vsize (Kb) 119608

[startup+640.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 46191 0 0 0 63733 172 0 0 25 0 1 0 1851932771 120303616 16417 4294967295 134512640 135094434 3221224432 3218446416 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 29371 16417 145 145 0 29226 0
[pid=22518] vsize: 117484
Current children cumulated CPU time (s) 639.07
Current children cumulated vsize (Kb) 119608

[startup+650.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 46191 0 0 0 64733 172 0 0 25 0 1 0 1851932771 120303616 16417 4294967295 134512640 135094434 3221224432 3216613552 134596872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 29371 16417 145 145 0 29226 0
[pid=22518] vsize: 117484
Current children cumulated CPU time (s) 649.07
Current children cumulated vsize (Kb) 119608

[startup+660.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 46632 0 0 0 65730 174 0 0 25 0 1 0 1851932771 121511936 16775 4294967295 134512640 135094434 3221224432 3219875536 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 29666 16775 145 145 0 29521 0
[pid=22518] vsize: 118664
Current children cumulated CPU time (s) 659.06
Current children cumulated vsize (Kb) 120788

[startup+670.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 47137 0 0 0 66728 175 0 0 25 0 1 0 1851932771 122429440 17045 4294967295 134512640 135094434 3221224432 3216362400 134597053 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 29890 17045 145 145 0 29745 0
[pid=22518] vsize: 119560
Current children cumulated CPU time (s) 669.05
Current children cumulated vsize (Kb) 121684

[startup+680.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 47212 0 0 0 67728 175 0 0 25 0 1 0 1851932771 122433536 17079 4294967295 134512640 135094434 3221224432 3218375312 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 29891 17079 145 145 0 29746 0
[pid=22518] vsize: 119564
Current children cumulated CPU time (s) 679.05
Current children cumulated vsize (Kb) 121688

[startup+690.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 47311 0 0 0 68728 175 0 0 25 0 1 0 1851932771 122601472 17136 4294967295 134512640 135094434 3221224432 3219309168 134597026 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 29932 17136 145 145 0 29787 0
[pid=22518] vsize: 119728
Current children cumulated CPU time (s) 689.05
Current children cumulated vsize (Kb) 121852

[startup+700.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 47322 0 0 0 69728 175 0 0 25 0 1 0 1851932771 122601472 17147 4294967295 134512640 135094434 3221224432 3219985008 134597020 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 29932 17147 145 145 0 29787 0
[pid=22518] vsize: 119728
Current children cumulated CPU time (s) 699.05
Current children cumulated vsize (Kb) 121852

[startup+710.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 47356 0 0 0 70728 175 0 0 25 0 1 0 1851932771 122703872 17181 4294967295 134512640 135094434 3221224432 3220542048 134597094 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 29957 17181 145 145 0 29812 0
[pid=22518] vsize: 119828
Current children cumulated CPU time (s) 709.05
Current children cumulated vsize (Kb) 121952

[startup+720.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 47391 0 0 0 71728 176 0 0 25 0 1 0 1851932771 122814464 17216 4294967295 134512640 135094434 3221224432 3221028512 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22518/statm): 29984 17216 145 145 0 29839 0
[pid=22518] vsize: 119936
Current children cumulated CPU time (s) 719.06
Current children cumulated vsize (Kb) 122060

[startup+730.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 47406 0 0 0 72727 176 0 0 25 0 1 0 1851932771 122859520 17231 4294967295 134512640 135094434 3221224432 3218637552 134596919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22518/statm): 29995 17231 145 145 0 29850 0
[pid=22518] vsize: 119980
Current children cumulated CPU time (s) 729.05
Current children cumulated vsize (Kb) 122104

[startup+740.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 47406 0 0 0 73725 177 0 0 25 0 1 0 1851932771 122859520 17231 4294967295 134512640 135094434 3221224432 3218167632 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 29995 17231 145 145 0 29850 0
[pid=22518] vsize: 119980
Current children cumulated CPU time (s) 739.04
Current children cumulated vsize (Kb) 122104

[startup+750.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 47406 0 0 0 74725 177 0 0 25 0 1 0 1851932771 122859520 17231 4294967295 134512640 135094434 3221224432 3217606016 134596860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 29995 17231 145 145 0 29850 0
[pid=22518] vsize: 119980
Current children cumulated CPU time (s) 749.04
Current children cumulated vsize (Kb) 122104

[startup+760.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 47406 0 0 0 75725 177 0 0 25 0 1 0 1851932771 122859520 17231 4294967295 134512640 135094434 3221224432 3216899200 134596860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 29995 17231 145 145 0 29850 0
[pid=22518] vsize: 119980
Current children cumulated CPU time (s) 759.04
Current children cumulated vsize (Kb) 122104

[startup+770.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 47406 0 0 0 76725 177 0 0 25 0 1 0 1851932771 122859520 17231 4294967295 134512640 135094434 3221224432 3215571280 134596869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 29995 17231 145 145 0 29850 0
[pid=22518] vsize: 119980
Current children cumulated CPU time (s) 769.04
Current children cumulated vsize (Kb) 122104

[startup+780.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 47812 0 0 0 77722 180 0 0 25 0 1 0 1851932771 123957248 17554 4294967295 134512640 135094434 3221224432 3218263552 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22518/statm): 30263 17554 145 145 0 30118 0
[pid=22518] vsize: 121052
Current children cumulated CPU time (s) 779.04
Current children cumulated vsize (Kb) 123176

[startup+790.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 47944 0 0 0 78720 180 0 0 25 0 1 0 1851932771 124375040 17686 4294967295 134512640 135094434 3221224432 3220096944 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 30365 17686 145 145 0 30220 0
[pid=22518] vsize: 121460
Current children cumulated CPU time (s) 789.02
Current children cumulated vsize (Kb) 123584

[startup+800.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 48024 0 0 0 79719 181 0 0 25 0 1 0 1851932771 124628992 17766 4294967295 134512640 135094434 3221224432 3221186032 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 30427 17766 145 145 0 30282 0
[pid=22518] vsize: 121708
Current children cumulated CPU time (s) 799.02
Current children cumulated vsize (Kb) 123832

[startup+810.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 48295 0 0 0 80718 182 0 0 25 0 1 0 1851932771 124379136 17759 4294967295 134512640 135094434 3221224432 3217921232 134597020 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 30366 17759 145 145 0 30221 0
[pid=22518] vsize: 121464
Current children cumulated CPU time (s) 809.02
Current children cumulated vsize (Kb) 123588

[startup+820.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 48395 0 0 0 81718 182 0 0 25 0 1 0 1851932771 124547072 17817 4294967295 134512640 135094434 3221224432 3218955408 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 30407 17817 145 145 0 30262 0
[pid=22518] vsize: 121628
Current children cumulated CPU time (s) 819.02
Current children cumulated vsize (Kb) 123752

[startup+830.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 48407 0 0 0 82718 182 0 0 25 0 1 0 1851932771 124547072 17829 4294967295 134512640 135094434 3221224432 3219664864 134597023 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 30407 17829 145 145 0 30262 0
[pid=22518] vsize: 121628
Current children cumulated CPU time (s) 829.02
Current children cumulated vsize (Kb) 123752

[startup+840.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 48417 0 0 0 83719 182 0 0 25 0 1 0 1851932771 124547072 17839 4294967295 134512640 135094434 3221224432 3220244784 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 30407 17839 145 145 0 30262 0
[pid=22518] vsize: 121628
Current children cumulated CPU time (s) 839.03
Current children cumulated vsize (Kb) 123752

[startup+850.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 48425 0 0 0 84719 182 0 0 25 0 1 0 1851932771 124547072 17847 4294967295 134512640 135094434 3221224432 3220743744 134597017 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 30407 17847 145 145 0 30262 0
[pid=22518] vsize: 121628
Current children cumulated CPU time (s) 849.03
Current children cumulated vsize (Kb) 123752

[startup+860.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 48443 0 0 0 85719 182 0 0 25 0 1 0 1851932771 124592128 17865 4294967295 134512640 135094434 3221224432 3221183040 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 30418 17865 145 145 0 30273 0
[pid=22518] vsize: 121672
Current children cumulated CPU time (s) 859.03
Current children cumulated vsize (Kb) 123796

[startup+870.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 48447 0 0 0 86719 182 0 0 25 0 1 0 1851932771 124604416 17869 4294967295 134512640 135094434 3221224432 3218279920 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 30421 17869 145 145 0 30276 0
[pid=22518] vsize: 121684
Current children cumulated CPU time (s) 869.03
Current children cumulated vsize (Kb) 123808

[startup+880.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 48447 0 0 0 87719 182 0 0 25 0 1 0 1851932771 124604416 17869 4294967295 134512640 135094434 3221224432 3217815456 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 30421 17869 145 145 0 30276 0
[pid=22518] vsize: 121684
Current children cumulated CPU time (s) 879.03
Current children cumulated vsize (Kb) 123808

[startup+890.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 48447 0 0 0 88720 182 0 0 25 0 1 0 1851932771 124604416 17869 4294967295 134512640 135094434 3221224432 3217276896 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 30421 17869 145 145 0 30276 0
[pid=22518] vsize: 121684
Current children cumulated CPU time (s) 889.04
Current children cumulated vsize (Kb) 123808

[startup+900.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 48447 0 0 0 89720 182 0 0 25 0 1 0 1851932771 124604416 17869 4294967295 134512640 135094434 3221224432 3216611616 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22518/statm): 30421 17869 145 145 0 30276 0
[pid=22518] vsize: 121684
Current children cumulated CPU time (s) 899.04
Current children cumulated vsize (Kb) 123808

[startup+910.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 48447 0 0 0 90719 183 0 0 25 0 1 0 1851932771 124604416 17869 4294967295 134512640 135094434 3221224432 3215396160 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 30421 17869 145 145 0 30276 0
[pid=22518] vsize: 121684
Current children cumulated CPU time (s) 909.04
Current children cumulated vsize (Kb) 123808

[startup+920.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 48821 0 0 0 91715 185 0 0 25 0 1 0 1851932771 125599744 18160 4294967295 134512640 135094434 3221224432 3217592288 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 30664 18160 145 145 0 30519 0
[pid=22518] vsize: 122656
Current children cumulated CPU time (s) 919.02
Current children cumulated vsize (Kb) 124780

[startup+930.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 48966 0 0 0 92714 185 0 0 25 0 1 0 1851932771 126058496 18305 4294967295 134512640 135094434 3221224432 3219563840 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 30776 18305 145 145 0 30631 0
[pid=22518] vsize: 123104
Current children cumulated CPU time (s) 929.01
Current children cumulated vsize (Kb) 125228

[startup+940.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 49049 0 0 0 93713 186 0 0 25 0 1 0 1851932771 126320640 18388 4294967295 134512640 135094434 3221224432 3220720512 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 30840 18388 145 145 0 30695 0
[pid=22518] vsize: 123360
Current children cumulated CPU time (s) 939.01
Current children cumulated vsize (Kb) 125484

[startup+950.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 49276 0 0 0 94713 186 0 0 25 0 1 0 1851932771 125931520 18340 4294967295 134512640 135094434 3221224432 3217258592 134597094 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 30745 18340 145 145 0 30600 0
[pid=22518] vsize: 122980
Current children cumulated CPU time (s) 949.01
Current children cumulated vsize (Kb) 125104

[startup+960.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 49383 0 0 0 95713 186 0 0 25 0 1 0 1851932771 126099456 18405 4294967295 134512640 135094434 3221224432 3218710592 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 30786 18405 145 145 0 30641 0
[pid=22518] vsize: 123144
Current children cumulated CPU time (s) 959.01
Current children cumulated vsize (Kb) 125268

[startup+970.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 49396 0 0 0 96713 186 0 0 25 0 1 0 1851932771 126099456 18418 4294967295 134512640 135094434 3221224432 3219522480 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 30786 18418 145 145 0 30641 0
[pid=22518] vsize: 123144
Current children cumulated CPU time (s) 969.01
Current children cumulated vsize (Kb) 125268

[startup+980.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 49407 0 0 0 97713 187 0 0 25 0 1 0 1851932771 126099456 18429 4294967295 134512640 135094434 3221224432 3220155728 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 30786 18429 145 145 0 30641 0
[pid=22518] vsize: 123144
Current children cumulated CPU time (s) 979.02
Current children cumulated vsize (Kb) 125268

[startup+990.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 49416 0 0 0 98713 187 0 0 25 0 1 0 1851932771 126099456 18438 4294967295 134512640 135094434 3221224432 3220686896 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 30786 18438 145 145 0 30641 0
[pid=22518] vsize: 123144
Current children cumulated CPU time (s) 989.02
Current children cumulated vsize (Kb) 125268

[startup+1000.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 49423 0 0 0 99713 187 0 0 25 0 1 0 1851932771 126099456 18445 4294967295 134512640 135094434 3221224432 3221147840 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 30786 18445 145 145 0 30641 0
[pid=22518] vsize: 123144
Current children cumulated CPU time (s) 999.02
Current children cumulated vsize (Kb) 125268

[startup+1010.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 49425 0 0 0 100713 187 0 0 25 0 1 0 1851932771 126099456 18447 4294967295 134512640 135094434 3221224432 3218524560 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 30786 18447 145 145 0 30641 0
[pid=22518] vsize: 123144
Current children cumulated CPU time (s) 1009.02
Current children cumulated vsize (Kb) 125268

[startup+1020.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 49425 0 0 0 101714 187 0 0 25 0 1 0 1851932771 126099456 18447 4294967295 134512640 135094434 3221224432 3218048128 134596919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 30786 18447 145 145 0 30641 0
[pid=22518] vsize: 123144
Current children cumulated CPU time (s) 1019.03
Current children cumulated vsize (Kb) 125268

[startup+1030.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 49425 0 0 0 102714 187 0 0 25 0 1 0 1851932771 126099456 18447 4294967295 134512640 135094434 3221224432 3217486688 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 30786 18447 145 145 0 30641 0
[pid=22518] vsize: 123144
Current children cumulated CPU time (s) 1029.03
Current children cumulated vsize (Kb) 125268

[startup+1040.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 49425 0 0 0 103714 187 0 0 25 0 1 0 1851932771 126099456 18447 4294967295 134512640 135094434 3221224432 3216728304 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 30786 18447 145 145 0 30641 0
[pid=22518] vsize: 123144
Current children cumulated CPU time (s) 1039.03
Current children cumulated vsize (Kb) 125268

[startup+1050.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 49425 0 0 0 104714 187 0 0 25 0 1 0 1851932771 126099456 18447 4294967295 134512640 135094434 3221224432 3215468848 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 30786 18447 145 145 0 30641 0
[pid=22518] vsize: 123144
Current children cumulated CPU time (s) 1049.03
Current children cumulated vsize (Kb) 125268

[startup+1060.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 49830 0 0 0 105712 188 0 0 25 0 1 0 1851932771 127184896 18769 4294967295 134512640 135094434 3221224432 3218427760 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 31051 18769 145 145 0 30906 0
[pid=22518] vsize: 124204
Current children cumulated CPU time (s) 1059.02
Current children cumulated vsize (Kb) 126328

[startup+1070.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 49955 0 0 0 106710 189 0 0 25 0 1 0 1851932771 127578112 18894 4294967295 134512640 135094434 3221224432 3220136720 134597040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 31147 18894 145 145 0 31002 0
[pid=22518] vsize: 124588
Current children cumulated CPU time (s) 1069.01
Current children cumulated vsize (Kb) 126712

[startup+1080.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 50031 0 0 0 107709 189 0 0 25 0 1 0 1851932771 127819776 18970 4294967295 134512640 135094434 3221224432 3221194128 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 31206 18970 145 145 0 31061 0
[pid=22518] vsize: 124824
Current children cumulated CPU time (s) 1079
Current children cumulated vsize (Kb) 126948

[startup+1090.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 50240 0 0 0 108709 190 0 0 25 0 1 0 1851932771 127324160 18903 4294967295 134512640 135094434 3221224432 3218162880 134597091 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 31085 18903 145 145 0 30940 0
[pid=22518] vsize: 124340
Current children cumulated CPU time (s) 1089.01
Current children cumulated vsize (Kb) 126464

[startup+1100.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 50340 0 0 0 109708 190 0 0 25 0 1 0 1851932771 127492096 18961 4294967295 134512640 135094434 3221224432 3219138800 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 31126 18961 145 145 0 30981 0
[pid=22518] vsize: 124504
Current children cumulated CPU time (s) 1099
Current children cumulated vsize (Kb) 126628

[startup+1110.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 50351 0 0 0 110709 190 0 0 25 0 1 0 1851932771 127492096 18972 4294967295 134512640 135094434 3221224432 3219831008 134597023 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 31126 18972 145 145 0 30981 0
[pid=22518] vsize: 124504
Current children cumulated CPU time (s) 1109.01
Current children cumulated vsize (Kb) 126628

[startup+1120.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 50361 0 0 0 111709 191 0 0 25 0 1 0 1851932771 127492096 18982 4294967295 134512640 135094434 3221224432 3220400544 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 31126 18982 145 145 0 30981 0
[pid=22518] vsize: 124504
Current children cumulated CPU time (s) 1119.02
Current children cumulated vsize (Kb) 126628

[startup+1130.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 50369 0 0 0 112709 191 0 0 25 0 1 0 1851932771 127492096 18990 4294967295 134512640 135094434 3221224432 3220896336 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 31126 18990 145 145 0 30981 0
[pid=22518] vsize: 124504
Current children cumulated CPU time (s) 1129.02
Current children cumulated vsize (Kb) 126628

[startup+1140.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 50374 0 0 0 113709 191 0 0 25 0 1 0 1851932771 127492096 18995 4294967295 134512640 135094434 3221224432 3219242112 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 31126 18995 145 145 0 30981 0
[pid=22518] vsize: 124504
Current children cumulated CPU time (s) 1139.02
Current children cumulated vsize (Kb) 126628

[startup+1150.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 50374 0 0 0 114709 191 0 0 25 0 1 0 1851932771 127492096 18995 4294967295 134512640 135094434 3221224432 3218307024 134596885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 31126 18995 145 145 0 30981 0
[pid=22518] vsize: 124504
Current children cumulated CPU time (s) 1149.02
Current children cumulated vsize (Kb) 126628

[startup+1160.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 50374 0 0 0 115710 191 0 0 25 0 1 0 1851932771 127492096 18995 4294967295 134512640 135094434 3221224432 3217784128 134596852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 31126 18995 145 145 0 30981 0
[pid=22518] vsize: 124504
Current children cumulated CPU time (s) 1159.03
Current children cumulated vsize (Kb) 126628

[startup+1170.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 50374 0 0 0 116710 191 0 0 25 0 1 0 1851932771 127492096 18995 4294967295 134512640 135094434 3221224432 3217161968 134596863 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 31126 18995 145 145 0 30981 0
[pid=22518] vsize: 124504
Current children cumulated CPU time (s) 1169.03
Current children cumulated vsize (Kb) 126628

[startup+1180.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 50374 0 0 0 117710 191 0 0 25 0 1 0 1851932771 127492096 18995 4294967295 134512640 135094434 3221224432 3216024128 134596860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 31126 18995 145 145 0 30981 0
[pid=22518] vsize: 124504
Current children cumulated CPU time (s) 1179.03
Current children cumulated vsize (Kb) 126628

[startup+1190.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 50374 0 0 0 118710 191 0 0 25 0 1 0 1851932771 127492096 18995 4294967295 134512640 135094434 3221224432 3215049088 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 31126 18995 145 145 0 30981 0
[pid=22518] vsize: 124504
Current children cumulated CPU time (s) 1189.03
Current children cumulated vsize (Kb) 126628

[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 50849 0 0 0 119708 192 0 0 25 0 1 0 1851932771 128806912 19387 4294967295 134512640 135094434 3221224432 3219205856 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 31447 19387 145 145 0 31302 0
[pid=22518] vsize: 125788
Current children cumulated CPU time (s) 1199.02
Current children cumulated vsize (Kb) 127912

[startup+1210.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 50951 0 0 0 120707 192 0 0 25 0 1 0 1851932771 129130496 19489 4294967295 134512640 135094434 3221224432 3220594496 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 31526 19489 145 145 0 31381 0
[pid=22518] vsize: 126104
Current children cumulated CPU time (s) 1209.01
Current children cumulated vsize (Kb) 128228



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22518
Raw data (/proc/22514/stat): 22514 (minisat+_script) S 22513 22514 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851932766 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22514/statm): 531 226 485 147 0 384 0
[pid=22514] vsize: 2124
Raw data (/proc/22518/stat): 22518 (minisat+_64-bit) R 22514 22514 5299 0 -1 0 50951 0 0 0 120707 192 0 0 25 0 1 0 1851932771 129130496 19489 4294967295 134512640 135094434 3221224432 3220594496 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22518/statm): 31526 19489 145 145 0 31381 0
[pid=22518] vsize: 126104
Current children cumulated CPU time (s) 1209.01
Current children cumulated vsize (Kb) 128228

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

Child status: 0
Real time (s): 1210.12
CPU time (s): 1209.04
CPU user time (s): 1207.07
CPU system time (s): 1.9627
CPU usage (%): 99.9104
Max. virtual memory (cumulated for all children) (Kb): 128228



Verifier Data




ERROR: no interpretation found !