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

Namesubmitted/een/normalized-nw04.opb
MD5SUMc4c13764e2ea959929790d6ef6d0273c
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 0
Optimality of the best value was proved YES
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 42031
Number of bits of the biggest number in a constraint 16
Biggest sum of numbers in a constraint 120189580
Number of bits of the biggest sum of numbers27
Best result obtained on this benchmarkOPTIMUM FOUND
Best CPU time to get the best result obtained on this benchmark19.3551
Number of variables87482
Total number of constraints72
Number of constraints which are clauses36
Number of constraints which are cardinality constraints (but not clauses)36
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint599
Maximum length of a constraint42032

Trace number 2267

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        901540 kB
Buffers:         35608 kB
Cached:          72452 kB
SwapCached:        740 kB
Active:          82204 kB
Inactive:        28472 kB
HighTotal:      131008 kB
HighFree:        56420 kB
LowTotal:       903652 kB
LowFree:        845120 kB
SwapTotal:     2097136 kB
SwapFree:      2095892 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5716 kB
Slab:            16800 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 18:45:18 (client local time) WITH STATUS 0 IN 1209.14 SECONDS
stats: 2621 7 1209.14 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/25982/stat): 25982 (minisat+_script) R 25981 25982 15400 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1785192852 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/25982/statm): 174 3 169 147 0 27 0
[pid=25982] 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=25983
New process pid=25984
New process pid=25985
execve syscall for /bin/sed executable
One traced child (pid=25984) 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=25985) exited with status: 0
One traced child (pid=25983) exited with status: 0
New process pid=25986
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc7/normalized-nw04.opb

[startup+10.0041 s]
Raw data (loadavg): 0.94 0.96 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 31519 0 0 0 821 107 0 0 25 0 1 0 1785192857 74985472 7078 4294967295 134512640 135094434 3221224448 3221217792 134591262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 18307 7078 145 145 0 18162 0
[pid=25986] vsize: 73228
Current children cumulated CPU time (s) 9.28
Current children cumulated vsize (Kb) 75352

[startup+20.0047 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 36241 0 0 0 1789 125 0 0 25 0 1 0 1785192857 84508672 8630 4294967295 134512640 135094434 3221224448 3221088368 134597091 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 20632 8630 145 145 0 20487 0
[pid=25986] vsize: 82528
Current children cumulated CPU time (s) 19.14
Current children cumulated vsize (Kb) 84652

[startup+30.0054 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 36317 0 0 0 2789 125 0 0 25 0 1 0 1785192857 84819968 8706 4294967295 134512640 135094434 3221224448 3220989808 134597091 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 20708 8706 145 145 0 20563 0
[pid=25986] vsize: 82832
Current children cumulated CPU time (s) 29.14
Current children cumulated vsize (Kb) 84956

[startup+40.007 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 36822 0 0 0 3788 127 0 0 25 0 1 0 1785192857 88375296 9211 4294967295 134512640 135094434 3221224448 3220640096 134597020 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 21576 9211 145 145 0 21431 0
[pid=25986] vsize: 86304
Current children cumulated CPU time (s) 39.15
Current children cumulated vsize (Kb) 88428

[startup+50.0076 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 36906 0 0 0 4787 127 0 0 25 0 1 0 1785192857 88412160 9295 4294967295 134512640 135094434 3221224448 3220913600 134596888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 21585 9295 145 145 0 21440 0
[pid=25986] vsize: 86340
Current children cumulated CPU time (s) 49.14
Current children cumulated vsize (Kb) 88464

[startup+60.0083 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 37632 0 0 0 5786 129 0 0 25 0 1 0 1785192857 91115520 10021 4294967295 134512640 135094434 3221224448 3219345440 134596860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 22245 10021 145 145 0 22100 0
[pid=25986] vsize: 88980
Current children cumulated CPU time (s) 59.15
Current children cumulated vsize (Kb) 91104

[startup+70.0089 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 37760 0 0 0 6786 129 0 0 25 0 1 0 1785192857 91152384 10149 4294967295 134512640 135094434 3221224448 3220335904 134597200 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 22254 10149 145 145 0 22109 0
[pid=25986] vsize: 89016
Current children cumulated CPU time (s) 69.15
Current children cumulated vsize (Kb) 91140

[startup+80.0096 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 37859 0 0 0 7786 129 0 0 25 0 1 0 1785192857 91217920 10248 4294967295 134512640 135094434 3221224448 3221222304 134597023 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 22270 10248 145 145 0 22125 0
[pid=25986] vsize: 89080
Current children cumulated CPU time (s) 79.15
Current children cumulated vsize (Kb) 91204

[startup+90.0102 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 38113 0 0 0 8785 130 0 0 25 0 1 0 1785192857 95088640 10502 4294967295 134512640 135094434 3221224448 3220931728 134597032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 23215 10502 145 145 0 23070 0
[pid=25986] vsize: 92860
Current children cumulated CPU time (s) 89.15
Current children cumulated vsize (Kb) 94984

[startup+100.011 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 38161 0 0 0 9785 131 0 0 25 0 1 0 1785192857 95088640 10550 4294967295 134512640 135094434 3221224448 3221000368 134597020 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 23215 10550 145 145 0 23070 0
[pid=25986] vsize: 92860
Current children cumulated CPU time (s) 99.16
Current children cumulated vsize (Kb) 94984

[startup+110.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 38229 0 0 0 10785 131 0 0 25 0 1 0 1785192857 95154176 10618 4294967295 134512640 135094434 3221224448 3219811312 134596866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 23231 10618 145 145 0 23086 0
[pid=25986] vsize: 92924
Current children cumulated CPU time (s) 109.16
Current children cumulated vsize (Kb) 95048

[startup+120.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 39934 0 0 0 11780 136 0 0 25 0 1 0 1785192857 98467840 11506 4294967295 134512640 135094434 3221224448 3220042048 134597012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 24040 11506 145 145 0 23895 0
[pid=25986] vsize: 96160
Current children cumulated CPU time (s) 119.16
Current children cumulated vsize (Kb) 98284

[startup+130.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 39965 0 0 0 12780 136 0 0 25 0 1 0 1785192857 98512896 11537 4294967295 134512640 135094434 3221224448 3219586208 134596852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 24051 11537 145 145 0 23906 0
[pid=25986] vsize: 96204
Current children cumulated CPU time (s) 129.16
Current children cumulated vsize (Kb) 98328

[startup+140.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 40421 0 0 0 13778 137 0 0 25 0 1 0 1785192857 99393536 11831 4294967295 134512640 135094434 3221224448 3219671040 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 24266 11831 145 145 0 24121 0
[pid=25986] vsize: 97064
Current children cumulated CPU time (s) 139.15
Current children cumulated vsize (Kb) 99188

[startup+150.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 40500 0 0 0 14777 137 0 0 25 0 1 0 1785192857 99446784 11870 4294967295 134512640 135094434 3221224448 3219615072 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 24279 11870 145 145 0 24134 0
[pid=25986] vsize: 97116
Current children cumulated CPU time (s) 149.14
Current children cumulated vsize (Kb) 99240

[startup+160.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 41031 0 0 0 15774 140 0 0 25 0 1 0 1785192857 100671488 12233 4294967295 134512640 135094434 3221224448 3217987072 134596997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 24578 12233 145 145 0 24433 0
[pid=25986] vsize: 98312
Current children cumulated CPU time (s) 159.14
Current children cumulated vsize (Kb) 100436

[startup+170.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 41139 0 0 0 16774 140 0 0 25 0 1 0 1785192857 100765696 12300 4294967295 134512640 135094434 3221224448 3220649600 134597026 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 24601 12300 145 145 0 24456 0
[pid=25986] vsize: 98404
Current children cumulated CPU time (s) 169.14
Current children cumulated vsize (Kb) 100528

[startup+180.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 41264 0 0 0 17773 140 0 0 25 0 1 0 1785192857 101064704 12383 4294967295 134512640 135094434 3221224448 3220573392 134596860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 24674 12383 145 145 0 24529 0
[pid=25986] vsize: 98696
Current children cumulated CPU time (s) 179.13
Current children cumulated vsize (Kb) 100820

[startup+190.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 41338 0 0 0 18773 141 0 0 25 0 1 0 1785192857 101298176 12457 4294967295 134512640 135094434 3221224448 3218416160 134597046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 24731 12457 145 145 0 24586 0
[pid=25986] vsize: 98924
Current children cumulated CPU time (s) 189.14
Current children cumulated vsize (Kb) 101048

[startup+200.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 42032 0 0 0 19769 143 0 0 25 0 1 0 1785192857 102395904 12813 4294967295 134512640 135094434 3221224448 3219258848 134597094 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 24999 12813 145 145 0 24854 0
[pid=25986] vsize: 99996
Current children cumulated CPU time (s) 199.12
Current children cumulated vsize (Kb) 102120

[startup+210.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 42146 0 0 0 20769 143 0 0 25 0 1 0 1785192857 102592512 12885 4294967295 134512640 135094434 3221224448 3220727040 134597020 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 25047 12885 145 145 0 24902 0
[pid=25986] vsize: 100188
Current children cumulated CPU time (s) 209.12
Current children cumulated vsize (Kb) 102312

[startup+220.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 42182 0 0 0 21769 143 0 0 25 0 1 0 1785192857 102707200 12921 4294967295 134512640 135094434 3221224448 3220148704 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 25075 12921 145 145 0 24930 0
[pid=25986] vsize: 100300
Current children cumulated CPU time (s) 219.12
Current children cumulated vsize (Kb) 102424

[startup+230.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 42182 0 0 0 22769 143 0 0 25 0 1 0 1785192857 102707200 12921 4294967295 134512640 135094434 3221224448 3218816736 134596888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 25075 12921 145 145 0 24930 0
[pid=25986] vsize: 100300
Current children cumulated CPU time (s) 229.12
Current children cumulated vsize (Kb) 102424

[startup+240.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 42612 0 0 0 23766 145 0 0 25 0 1 0 1785192857 103878656 13268 4294967295 134512640 135094434 3221224448 3220413408 134597091 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 25361 13268 145 145 0 25216 0
[pid=25986] vsize: 101444
Current children cumulated CPU time (s) 239.11
Current children cumulated vsize (Kb) 103568

[startup+250.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 42896 0 0 0 24765 146 0 0 25 0 1 0 1785192857 103747584 13295 4294967295 134512640 135094434 3221224448 3219344912 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 25329 13295 145 145 0 25184 0
[pid=25986] vsize: 101316
Current children cumulated CPU time (s) 249.11
Current children cumulated vsize (Kb) 103440

[startup+260.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 42999 0 0 0 25764 147 0 0 25 0 1 0 1785192857 103915520 13356 4294967295 134512640 135094434 3221224448 3220573216 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 25370 13356 145 145 0 25225 0
[pid=25986] vsize: 101480
Current children cumulated CPU time (s) 259.11
Current children cumulated vsize (Kb) 103604

[startup+270.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 43021 0 0 0 26764 147 0 0 25 0 1 0 1785192857 103960576 13378 4294967295 134512640 135094434 3221224448 3220218576 134596857 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 25381 13378 145 145 0 25236 0
[pid=25986] vsize: 101524
Current children cumulated CPU time (s) 269.11
Current children cumulated vsize (Kb) 103648

[startup+280.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 43021 0 0 0 27764 147 0 0 25 0 1 0 1785192857 103960576 13378 4294967295 134512640 135094434 3221224448 3219361984 134596919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 25381 13378 145 145 0 25236 0
[pid=25986] vsize: 101524
Current children cumulated CPU time (s) 279.11
Current children cumulated vsize (Kb) 103648

[startup+290.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 43021 0 0 0 28765 147 0 0 25 0 1 0 1785192857 103960576 13378 4294967295 134512640 135094434 3221224448 3217191552 134596875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 25381 13378 145 145 0 25236 0
[pid=25986] vsize: 101524
Current children cumulated CPU time (s) 289.12
Current children cumulated vsize (Kb) 103648

[startup+300.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 43508 0 0 0 29762 149 0 0 25 0 1 0 1785192857 111603712 13782 4294967295 134512640 135094434 3221224448 3220998256 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 27247 13782 145 145 0 27102 0
[pid=25986] vsize: 108988
Current children cumulated CPU time (s) 299.11
Current children cumulated vsize (Kb) 111112

[startup+310.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 43738 0 0 0 30761 149 0 0 25 0 1 0 1785192857 111255552 13754 4294967295 134512640 135094434 3221224448 3219692864 134597084 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 27162 13754 145 145 0 27017 0
[pid=25986] vsize: 108648
Current children cumulated CPU time (s) 309.1
Current children cumulated vsize (Kb) 110772

[startup+320.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 43839 0 0 0 31761 149 0 0 25 0 1 0 1785192857 111423488 13813 4294967295 134512640 135094434 3221224448 3220819440 134597046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 27203 13813 145 145 0 27058 0
[pid=25986] vsize: 108812
Current children cumulated CPU time (s) 319.1
Current children cumulated vsize (Kb) 110936

[startup+330.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 43851 0 0 0 32762 149 0 0 25 0 1 0 1785192857 111443968 13825 4294967295 134512640 135094434 3221224448 3219872912 134596866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 27208 13825 145 145 0 27063 0
[pid=25986] vsize: 108832
Current children cumulated CPU time (s) 329.11
Current children cumulated vsize (Kb) 110956

[startup+340.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 43851 0 0 0 33762 149 0 0 25 0 1 0 1785192857 111443968 13825 4294967295 134512640 135094434 3221224448 3218804240 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 27208 13825 145 145 0 27063 0
[pid=25986] vsize: 108832
Current children cumulated CPU time (s) 339.11
Current children cumulated vsize (Kb) 110956

[startup+350.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 43991 0 0 0 34761 150 0 0 25 0 1 0 1785192857 111886336 13965 4294967295 134512640 135094434 3221224448 3218412464 134597020 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 27316 13965 145 145 0 27171 0
[pid=25986] vsize: 109264
Current children cumulated CPU time (s) 349.11
Current children cumulated vsize (Kb) 111388

[startup+360.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 44484 0 0 0 35758 151 0 0 25 0 1 0 1785192857 112402432 14156 4294967295 134512640 135094434 3221224448 3217561328 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 27442 14156 145 145 0 27297 0
[pid=25986] vsize: 109768
Current children cumulated CPU time (s) 359.09
Current children cumulated vsize (Kb) 111892

[startup+370.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 44565 0 0 0 36758 151 0 0 25 0 1 0 1785192857 112406528 14196 4294967295 134512640 135094434 3221224448 3219879600 134597037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 27443 14196 145 145 0 27298 0
[pid=25986] vsize: 109772
Current children cumulated CPU time (s) 369.09
Current children cumulated vsize (Kb) 111896

[startup+380.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 44664 0 0 0 37758 151 0 0 25 0 1 0 1785192857 112574464 14253 4294967295 134512640 135094434 3221224448 3220847424 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 27484 14253 145 145 0 27339 0
[pid=25986] vsize: 109936
Current children cumulated CPU time (s) 379.09
Current children cumulated vsize (Kb) 112060

[startup+390.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 44674 0 0 0 38758 151 0 0 25 0 1 0 1785192857 112590848 14263 4294967295 134512640 135094434 3221224448 3219864288 134596919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 27488 14263 145 145 0 27343 0
[pid=25986] vsize: 109952
Current children cumulated CPU time (s) 389.09
Current children cumulated vsize (Kb) 112076

[startup+400.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 44674 0 0 0 39759 151 0 0 25 0 1 0 1785192857 112590848 14263 4294967295 134512640 135094434 3221224448 3218924976 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 27488 14263 145 145 0 27343 0
[pid=25986] vsize: 109952
Current children cumulated CPU time (s) 399.1
Current children cumulated vsize (Kb) 112076

[startup+410.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 44674 0 0 0 40759 151 0 0 25 0 1 0 1785192857 112590848 14263 4294967295 134512640 135094434 3221224448 3216706144 134596875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 27488 14263 145 145 0 27343 0
[pid=25986] vsize: 109952
Current children cumulated CPU time (s) 409.1
Current children cumulated vsize (Kb) 112076

[startup+420.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 45155 0 0 0 41755 153 0 0 25 0 1 0 1785192857 113926144 14661 4294967295 134512640 135094434 3221224448 3220776848 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 27814 14661 145 145 0 27669 0
[pid=25986] vsize: 111256
Current children cumulated CPU time (s) 419.08
Current children cumulated vsize (Kb) 113380

[startup+430.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 45411 0 0 0 42755 154 0 0 25 0 1 0 1785192857 113680384 14657 4294967295 134512640 135094434 3221224448 3219194960 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 27754 14657 145 145 0 27609 0
[pid=25986] vsize: 111016
Current children cumulated CPU time (s) 429.09
Current children cumulated vsize (Kb) 113140

[startup+440.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 48150 0 0 0 43748 161 0 0 25 0 1 0 1785192857 119250944 16036 4294967295 134512640 135094434 3221224448 3220338256 134597017 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 29114 16036 145 145 0 28969 0
[pid=25986] vsize: 116456
Current children cumulated CPU time (s) 439.09
Current children cumulated vsize (Kb) 118580

[startup+450.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 48164 0 0 0 44748 161 0 0 25 0 1 0 1785192857 119255040 16050 4294967295 134512640 135094434 3221224448 3221091008 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 29115 16050 145 145 0 28970 0
[pid=25986] vsize: 116460
Current children cumulated CPU time (s) 449.09
Current children cumulated vsize (Kb) 118584

[startup+460.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 48174 0 0 0 45748 161 0 0 25 0 1 0 1785192857 119287808 16060 4294967295 134512640 135094434 3221224448 3219509120 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 29123 16060 145 145 0 28978 0
[pid=25986] vsize: 116492
Current children cumulated CPU time (s) 459.09
Current children cumulated vsize (Kb) 118616

[startup+470.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 48174 0 0 0 46748 162 0 0 25 0 1 0 1785192857 119287808 16060 4294967295 134512640 135094434 3221224448 3218515424 134596919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 29123 16060 145 145 0 28978 0
[pid=25986] vsize: 116492
Current children cumulated CPU time (s) 469.1
Current children cumulated vsize (Kb) 118616

[startup+480.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 48310 0 0 0 47746 163 0 0 25 0 1 0 1785192857 119717888 16196 4294967295 134512640 135094434 3221224448 3218166240 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 29228 16196 145 145 0 29083 0
[pid=25986] vsize: 116912
Current children cumulated CPU time (s) 479.09
Current children cumulated vsize (Kb) 119036

[startup+490.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 48754 0 0 0 48742 165 0 0 25 0 1 0 1785192857 120082432 16336 4294967295 134512640 135094434 3221224448 3217040816 134594932 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 29317 16336 145 145 0 29172 0
[pid=25986] vsize: 117268
Current children cumulated CPU time (s) 489.07
Current children cumulated vsize (Kb) 119392

[startup+500.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 48905 0 0 0 49742 166 0 0 25 0 1 0 1785192857 120315904 16447 4294967295 134512640 135094434 3221224448 3219482544 134597012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 29374 16447 145 145 0 29229 0
[pid=25986] vsize: 117496
Current children cumulated CPU time (s) 499.08
Current children cumulated vsize (Kb) 119620

[startup+510.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 49006 0 0 0 50742 166 0 0 25 0 1 0 1785192857 120483840 16506 4294967295 134512640 135094434 3221224448 3220541888 134597020 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 29415 16506 145 145 0 29270 0
[pid=25986] vsize: 117660
Current children cumulated CPU time (s) 509.08
Current children cumulated vsize (Kb) 119784

[startup+520.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 49020 0 0 0 51742 166 0 0 25 0 1 0 1785192857 120496128 16520 4294967295 134512640 135094434 3221224448 3220678992 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 29418 16520 145 145 0 29273 0
[pid=25986] vsize: 117672
Current children cumulated CPU time (s) 519.08
Current children cumulated vsize (Kb) 119796

[startup+530.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 49020 0 0 0 52742 166 0 0 25 0 1 0 1785192857 120496128 16520 4294967295 134512640 135094434 3221224448 3219298624 134596866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 29418 16520 145 145 0 29273 0
[pid=25986] vsize: 117672
Current children cumulated CPU time (s) 529.08
Current children cumulated vsize (Kb) 119796

[startup+540.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 49020 0 0 0 53743 166 0 0 25 0 1 0 1785192857 120496128 16520 4294967295 134512640 135094434 3221224448 3218209184 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 29418 16520 145 145 0 29273 0
[pid=25986] vsize: 117672
Current children cumulated CPU time (s) 539.09
Current children cumulated vsize (Kb) 119796

[startup+550.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 49385 0 0 0 54740 168 0 0 25 0 1 0 1785192857 121462784 16802 4294967295 134512640 135094434 3221224448 3218968800 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 29654 16802 145 145 0 29509 0
[pid=25986] vsize: 118616
Current children cumulated CPU time (s) 549.08
Current children cumulated vsize (Kb) 120740

[startup+560.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 49678 0 0 0 55738 169 0 0 25 0 1 0 1785192857 121540608 16872 4294967295 134512640 135094434 3221224448 3216894288 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 29673 16872 145 145 0 29528 0
[pid=25986] vsize: 118692
Current children cumulated CPU time (s) 559.07
Current children cumulated vsize (Kb) 120816

[startup+570.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 49782 0 0 0 56738 170 0 0 25 0 1 0 1785192857 121630720 16935 4294967295 134512640 135094434 3221224448 3219365856 134597043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 29695 16935 145 145 0 29550 0
[pid=25986] vsize: 118780
Current children cumulated CPU time (s) 569.08
Current children cumulated vsize (Kb) 120904

[startup+580.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 49881 0 0 0 57737 170 0 0 25 0 1 0 1785192857 121798656 16992 4294967295 134512640 135094434 3221224448 3220365536 134597094 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 29736 16992 145 145 0 29591 0
[pid=25986] vsize: 118944
Current children cumulated CPU time (s) 579.07
Current children cumulated vsize (Kb) 121068

[startup+590.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 49893 0 0 0 58738 170 0 0 25 0 1 0 1785192857 121798656 17004 4294967295 134512640 135094434 3221224448 3221047184 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 29736 17004 145 145 0 29591 0
[pid=25986] vsize: 118944
Current children cumulated CPU time (s) 589.08
Current children cumulated vsize (Kb) 121068

[startup+600.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 49905 0 0 0 59738 170 0 0 25 0 1 0 1785192857 121835520 17016 4294967295 134512640 135094434 3221224448 3219433616 134596852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 29745 17016 145 145 0 29600 0
[pid=25986] vsize: 118980
Current children cumulated CPU time (s) 599.08
Current children cumulated vsize (Kb) 121104

[startup+610.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 49905 0 0 0 60738 171 0 0 25 0 1 0 1785192857 121835520 17016 4294967295 134512640 135094434 3221224448 3218654640 134596882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 29745 17016 145 145 0 29600 0
[pid=25986] vsize: 118980
Current children cumulated CPU time (s) 609.09
Current children cumulated vsize (Kb) 121104

[startup+620.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 49905 0 0 0 61738 171 0 0 25 0 1 0 1785192857 121835520 17016 4294967295 134512640 135094434 3221224448 3216815264 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 29745 17016 145 145 0 29600 0
[pid=25986] vsize: 118980
Current children cumulated CPU time (s) 619.09
Current children cumulated vsize (Kb) 121104

[startup+630.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 50364 0 0 0 62734 172 0 0 25 0 1 0 1785192857 123101184 17392 4294967295 134512640 135094434 3221224448 3220106816 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 30054 17392 145 145 0 29909 0
[pid=25986] vsize: 120216
Current children cumulated CPU time (s) 629.06
Current children cumulated vsize (Kb) 122340

[startup+640.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 50899 0 0 0 63732 174 0 0 25 0 1 0 1785192857 123949056 17652 4294967295 134512640 135094434 3221224448 3217051280 134597094 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 30261 17652 145 145 0 30116 0
[pid=25986] vsize: 121044
Current children cumulated CPU time (s) 639.06
Current children cumulated vsize (Kb) 123168

[startup+650.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 51010 0 0 0 64732 175 0 0 25 0 1 0 1785192857 124116992 17721 4294967295 134512640 135094434 3221224448 3218718704 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 30302 17721 145 145 0 30157 0
[pid=25986] vsize: 121208
Current children cumulated CPU time (s) 649.07
Current children cumulated vsize (Kb) 123332

[startup+660.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 51025 0 0 0 65732 175 0 0 25 0 1 0 1785192857 124116992 17736 4294967295 134512640 135094434 3221224448 3219620704 134597026 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 30302 17736 145 145 0 30157 0
[pid=25986] vsize: 121208
Current children cumulated CPU time (s) 659.07
Current children cumulated vsize (Kb) 123332

[startup+670.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 51043 0 0 0 66732 175 0 0 25 0 1 0 1785192857 124149760 17754 4294967295 134512640 135094434 3221224448 3220259408 134597094 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 30310 17754 145 145 0 30165 0
[pid=25986] vsize: 121240
Current children cumulated CPU time (s) 669.07
Current children cumulated vsize (Kb) 123364

[startup+680.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 51082 0 0 0 67732 175 0 0 25 0 1 0 1785192857 124272640 17793 4294967295 134512640 135094434 3221224448 3220783712 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 30340 17793 145 145 0 30195 0
[pid=25986] vsize: 121360
Current children cumulated CPU time (s) 679.07
Current children cumulated vsize (Kb) 123484

[startup+690.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 51113 0 0 0 68731 176 0 0 25 0 1 0 1785192857 124370944 17824 4294967295 134512640 135094434 3221224448 3220382608 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 30364 17824 145 145 0 30219 0
[pid=25986] vsize: 121456
Current children cumulated CPU time (s) 689.07
Current children cumulated vsize (Kb) 123580

[startup+700.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 51113 0 0 0 69732 176 0 0 25 0 1 0 1785192857 124370944 17824 4294967295 134512640 135094434 3221224448 3218430768 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 30364 17824 145 145 0 30219 0
[pid=25986] vsize: 121456
Current children cumulated CPU time (s) 699.08
Current children cumulated vsize (Kb) 123580

[startup+710.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 51113 0 0 0 70732 176 0 0 25 0 1 0 1785192857 124370944 17824 4294967295 134512640 135094434 3221224448 3217923360 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 30364 17824 145 145 0 30219 0
[pid=25986] vsize: 121456
Current children cumulated CPU time (s) 709.08
Current children cumulated vsize (Kb) 123580

[startup+720.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 51113 0 0 0 71732 176 0 0 25 0 1 0 1785192857 124370944 17824 4294967295 134512640 135094434 3221224448 3217311232 134596852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 30364 17824 145 145 0 30219 0
[pid=25986] vsize: 121456
Current children cumulated CPU time (s) 719.08
Current children cumulated vsize (Kb) 123580

[startup+730.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 51113 0 0 0 72732 176 0 0 25 0 1 0 1785192857 124370944 17824 4294967295 134512640 135094434 3221224448 3216168288 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 30364 17824 145 145 0 30219 0
[pid=25986] vsize: 121456
Current children cumulated CPU time (s) 729.08
Current children cumulated vsize (Kb) 123580

[startup+740.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 51113 0 0 0 73733 176 0 0 25 0 1 0 1785192857 124370944 17824 4294967295 134512640 135094434 3221224448 3215104368 134596852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 30364 17824 145 145 0 30219 0
[pid=25986] vsize: 121456
Current children cumulated CPU time (s) 739.09
Current children cumulated vsize (Kb) 123580

[startup+750.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 51588 0 0 0 74730 178 0 0 25 0 1 0 1785192857 125685760 18216 4294967295 134512640 135094434 3221224448 3219225760 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 30685 18216 145 145 0 30540 0
[pid=25986] vsize: 122740
Current children cumulated CPU time (s) 749.08
Current children cumulated vsize (Kb) 124864

[startup+760.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 51688 0 0 0 75729 178 0 0 25 0 1 0 1785192857 126001152 18316 4294967295 134512640 135094434 3221224448 3220598736 134597029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 30762 18316 145 145 0 30617 0
[pid=25986] vsize: 123048
Current children cumulated CPU time (s) 759.07
Current children cumulated vsize (Kb) 125172

[startup+770.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 51926 0 0 0 76728 179 0 0 25 0 1 0 1785192857 125661184 18279 4294967295 134512640 135094434 3221224448 3217126784 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 30679 18279 145 145 0 30534 0
[pid=25986] vsize: 122716
Current children cumulated CPU time (s) 769.07
Current children cumulated vsize (Kb) 124840

[startup+780.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 52035 0 0 0 77728 179 0 0 25 0 1 0 1785192857 125829120 18346 4294967295 134512640 135094434 3221224448 3218700752 134597020 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 30720 18346 145 145 0 30575 0
[pid=25986] vsize: 122880
Current children cumulated CPU time (s) 779.07
Current children cumulated vsize (Kb) 125004

[startup+790.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 52049 0 0 0 78729 179 0 0 25 0 1 0 1785192857 125829120 18360 4294967295 134512640 135094434 3221224448 3219536752 134597094 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 30720 18360 145 145 0 30575 0
[pid=25986] vsize: 122880
Current children cumulated CPU time (s) 789.08
Current children cumulated vsize (Kb) 125004

[startup+800.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 52060 0 0 0 79729 179 0 0 25 0 1 0 1785192857 125829120 18371 4294967295 134512640 135094434 3221224448 3220172112 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 30720 18371 145 145 0 30575 0
[pid=25986] vsize: 122880
Current children cumulated CPU time (s) 799.08
Current children cumulated vsize (Kb) 125004

[startup+810.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 52069 0 0 0 80729 179 0 0 25 0 1 0 1785192857 125829120 18380 4294967295 134512640 135094434 3221224448 3220701872 134597094 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 30720 18380 145 145 0 30575 0
[pid=25986] vsize: 122880
Current children cumulated CPU time (s) 809.08
Current children cumulated vsize (Kb) 125004

[startup+820.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 52076 0 0 0 81729 179 0 0 25 0 1 0 1785192857 125829120 18387 4294967295 134512640 135094434 3221224448 3221170560 134597037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 30720 18387 145 145 0 30575 0
[pid=25986] vsize: 122880
Current children cumulated CPU time (s) 819.08
Current children cumulated vsize (Kb) 125004

[startup+830.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 52078 0 0 0 82730 179 0 0 25 0 1 0 1785192857 125833216 18389 4294967295 134512640 135094434 3221224448 3218504336 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 30721 18389 145 145 0 30576 0
[pid=25986] vsize: 122884
Current children cumulated CPU time (s) 829.09
Current children cumulated vsize (Kb) 125008

[startup+840.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 52078 0 0 0 83730 179 0 0 25 0 1 0 1785192857 125833216 18389 4294967295 134512640 135094434 3221224448 3218011536 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 30721 18389 145 145 0 30576 0
[pid=25986] vsize: 122884
Current children cumulated CPU time (s) 839.09
Current children cumulated vsize (Kb) 125008

[startup+850.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 52078 0 0 0 84730 179 0 0 25 0 1 0 1785192857 125833216 18389 4294967295 134512640 135094434 3221224448 3217427392 134596875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 30721 18389 145 145 0 30576 0
[pid=25986] vsize: 122884
Current children cumulated CPU time (s) 849.09
Current children cumulated vsize (Kb) 125008

[startup+860.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 52078 0 0 0 85730 179 0 0 25 0 1 0 1785192857 125833216 18389 4294967295 134512640 135094434 3221224448 3216538944 134596919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 30721 18389 145 145 0 30576 0
[pid=25986] vsize: 122884
Current children cumulated CPU time (s) 859.09
Current children cumulated vsize (Kb) 125008

[startup+870.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 52078 0 0 0 86730 179 0 0 25 0 1 0 1785192857 125833216 18389 4294967295 134512640 135094434 3221224448 3215370128 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 30721 18389 145 145 0 30576 0
[pid=25986] vsize: 122884
Current children cumulated CPU time (s) 869.09
Current children cumulated vsize (Kb) 125008

[startup+880.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 52509 0 0 0 87728 181 0 0 25 0 1 0 1785192857 127008768 18737 4294967295 134512640 135094434 3221224448 3218625952 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 31008 18737 145 145 0 30863 0
[pid=25986] vsize: 124032
Current children cumulated CPU time (s) 879.09
Current children cumulated vsize (Kb) 126156

[startup+890.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 52626 0 0 0 88727 181 0 0 25 0 1 0 1785192857 127377408 18854 4294967295 134512640 135094434 3221224448 3220213120 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 31098 18854 145 145 0 30953 0
[pid=25986] vsize: 124392
Current children cumulated CPU time (s) 889.08
Current children cumulated vsize (Kb) 126516

[startup+900.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 52804 0 0 0 89726 182 0 0 25 0 1 0 1785192857 127021056 18797 4294967295 134512640 135094434 3221224448 3215775984 134597053 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 31011 18797 145 145 0 30866 0
[pid=25986] vsize: 124044
Current children cumulated CPU time (s) 899.08
Current children cumulated vsize (Kb) 126168

[startup+910.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 52908 0 0 0 90725 182 0 0 25 0 1 0 1785192857 127111168 18861 4294967295 134512640 135094434 3221224448 3218308624 134597012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 31033 18861 145 145 0 30888 0
[pid=25986] vsize: 124132
Current children cumulated CPU time (s) 909.07
Current children cumulated vsize (Kb) 126256

[startup+920.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 53008 0 0 0 91726 182 0 0 25 0 1 0 1785192857 127279104 18919 4294967295 134512640 135094434 3221224448 3219285072 134597094 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 31074 18919 145 145 0 30929 0
[pid=25986] vsize: 124296
Current children cumulated CPU time (s) 919.08
Current children cumulated vsize (Kb) 126420

[startup+930.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 53019 0 0 0 92726 182 0 0 25 0 1 0 1785192857 127279104 18930 4294967295 134512640 135094434 3221224448 3219969712 134597094 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 31074 18930 145 145 0 30929 0
[pid=25986] vsize: 124296
Current children cumulated CPU time (s) 929.08
Current children cumulated vsize (Kb) 126420

[startup+940.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 53028 0 0 0 93726 182 0 0 25 0 1 0 1785192857 127279104 18939 4294967295 134512640 135094434 3221224448 3220527456 134597094 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 31074 18939 145 145 0 30929 0
[pid=25986] vsize: 124296
Current children cumulated CPU time (s) 939.08
Current children cumulated vsize (Kb) 126420

[startup+950.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 53036 0 0 0 94726 182 0 0 25 0 1 0 1785192857 127279104 18947 4294967295 134512640 135094434 3221224448 3221013216 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 31074 18947 145 145 0 30929 0
[pid=25986] vsize: 124296
Current children cumulated CPU time (s) 949.08
Current children cumulated vsize (Kb) 126420

[startup+960.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 53040 0 0 0 95727 182 0 0 25 0 1 0 1785192857 127279104 18951 4294967295 134512640 135094434 3221224448 3218654032 134595058 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 31074 18951 145 145 0 30929 0
[pid=25986] vsize: 124296
Current children cumulated CPU time (s) 959.09
Current children cumulated vsize (Kb) 126420

[startup+970.069 s]
Raw data (loadavg): 1.15 1.00 0.92 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 53040 0 0 0 96727 182 0 0 25 0 1 0 1785192857 127279104 18951 4294967295 134512640 135094434 3221224448 3218183488 134596919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 31074 18951 145 145 0 30929 0
[pid=25986] vsize: 124296
Current children cumulated CPU time (s) 969.09
Current children cumulated vsize (Kb) 126420

[startup+980.07 s]
Raw data (loadavg): 1.12 1.00 0.92 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 53040 0 0 0 97727 182 0 0 25 0 1 0 1785192857 127279104 18951 4294967295 134512640 135094434 3221224448 3217629968 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 31074 18951 145 145 0 30929 0
[pid=25986] vsize: 124296
Current children cumulated CPU time (s) 979.09
Current children cumulated vsize (Kb) 126420

[startup+990.07 s]
Raw data (loadavg): 1.10 1.00 0.92 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 53040 0 0 0 98727 182 0 0 25 0 1 0 1785192857 127279104 18951 4294967295 134512640 135094434 3221224448 3216946736 134596875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 31074 18951 145 145 0 30929 0
[pid=25986] vsize: 124296
Current children cumulated CPU time (s) 989.09
Current children cumulated vsize (Kb) 126420

[startup+1000.07 s]
Raw data (loadavg): 1.09 1.00 0.92 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 53040 0 0 0 99728 182 0 0 25 0 1 0 1785192857 127279104 18951 4294967295 134512640 135094434 3221224448 3215695904 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 31074 18951 145 145 0 30929 0
[pid=25986] vsize: 124296
Current children cumulated CPU time (s) 999.1
Current children cumulated vsize (Kb) 126420

[startup+1010.07 s]
Raw data (loadavg): 1.07 1.00 0.92 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 53395 0 0 0 100726 183 0 0 25 0 1 0 1785192857 128217088 19223 4294967295 134512640 135094434 3221224448 3217559920 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 31303 19223 145 145 0 31158 0
[pid=25986] vsize: 125212
Current children cumulated CPU time (s) 1009.09
Current children cumulated vsize (Kb) 127336

[startup+1020.07 s]
Raw data (loadavg): 1.06 1.00 0.92 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 53562 0 0 0 101725 184 0 0 25 0 1 0 1785192857 128745472 19390 4294967295 134512640 135094434 3221224448 3219840176 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 31432 19390 145 145 0 31287 0
[pid=25986] vsize: 125728
Current children cumulated CPU time (s) 1019.09
Current children cumulated vsize (Kb) 127852

[startup+1030.07 s]
Raw data (loadavg): 1.05 1.00 0.92 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 53648 0 0 0 102724 184 0 0 25 0 1 0 1785192857 129015808 19476 4294967295 134512640 135094434 3221224448 3221015504 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 31498 19476 145 145 0 31353 0
[pid=25986] vsize: 125992
Current children cumulated CPU time (s) 1029.08
Current children cumulated vsize (Kb) 128116

[startup+1040.07 s]
Raw data (loadavg): 1.04 1.00 0.92 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 53864 0 0 0 103723 185 0 0 25 0 1 0 1785192857 141144064 19417 4294967295 134512640 135094434 3221224448 3217887280 134597094 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 34459 19417 145 145 0 34314 0
[pid=25986] vsize: 137836
Current children cumulated CPU time (s) 1039.08
Current children cumulated vsize (Kb) 139960

[startup+1050.07 s]
Raw data (loadavg): 1.04 1.00 0.92 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 53966 0 0 0 104723 185 0 0 25 0 1 0 1785192857 141312000 19477 4294967295 134512640 135094434 3221224448 3219023008 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 34500 19477 145 145 0 34355 0
[pid=25986] vsize: 138000
Current children cumulated CPU time (s) 1049.08
Current children cumulated vsize (Kb) 140124

[startup+1060.07 s]
Raw data (loadavg): 1.03 1.00 0.92 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 53978 0 0 0 105723 185 0 0 25 0 1 0 1785192857 141312000 19489 4294967295 134512640 135094434 3221224448 3219775760 134597094 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 34500 19489 145 145 0 34355 0
[pid=25986] vsize: 138000
Current children cumulated CPU time (s) 1059.08
Current children cumulated vsize (Kb) 140124

[startup+1070.08 s]
Raw data (loadavg): 1.03 1.00 0.92 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 53988 0 0 0 106722 186 0 0 25 0 1 0 1785192857 141312000 19499 4294967295 134512640 135094434 3221224448 3220373104 134597017 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 34500 19499 145 145 0 34355 0
[pid=25986] vsize: 138000
Current children cumulated CPU time (s) 1069.08
Current children cumulated vsize (Kb) 140124

[startup+1080.08 s]
Raw data (loadavg): 1.02 1.00 0.92 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 53997 0 0 0 107722 187 0 0 25 0 1 0 1785192857 141312000 19508 4294967295 134512640 135094434 3221224448 3220875760 134597053 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 34500 19508 145 145 0 34355 0
[pid=25986] vsize: 138000
Current children cumulated CPU time (s) 1079.09
Current children cumulated vsize (Kb) 140124

[startup+1090.08 s]
Raw data (loadavg): 1.02 1.00 0.92 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 54002 0 0 0 108722 187 0 0 25 0 1 0 1785192857 141312000 19513 4294967295 134512640 135094434 3221224448 3219385568 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 34500 19513 145 145 0 34355 0
[pid=25986] vsize: 138000
Current children cumulated CPU time (s) 1089.09
Current children cumulated vsize (Kb) 140124

[startup+1100.08 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 54002 0 0 0 109723 187 0 0 25 0 1 0 1785192857 141312000 19513 4294967295 134512640 135094434 3221224448 3218316720 134596860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 34500 19513 145 145 0 34355 0
[pid=25986] vsize: 138000
Current children cumulated CPU time (s) 1099.1
Current children cumulated vsize (Kb) 140124

[startup+1110.08 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 54002 0 0 0 110723 187 0 0 25 0 1 0 1785192857 141312000 19513 4294967295 134512640 135094434 3221224448 3217795056 134596860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 34500 19513 145 145 0 34355 0
[pid=25986] vsize: 138000
Current children cumulated CPU time (s) 1109.1
Current children cumulated vsize (Kb) 140124

[startup+1120.08 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 54002 0 0 0 111723 187 0 0 25 0 1 0 1785192857 141312000 19513 4294967295 134512640 135094434 3221224448 3217152128 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 34500 19513 145 145 0 34355 0
[pid=25986] vsize: 138000
Current children cumulated CPU time (s) 1119.1
Current children cumulated vsize (Kb) 140124

[startup+1130.08 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 54002 0 0 0 112723 187 0 0 25 0 1 0 1785192857 141312000 19513 4294967295 134512640 135094434 3221224448 3215866448 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 34500 19513 145 145 0 34355 0
[pid=25986] vsize: 138000
Current children cumulated CPU time (s) 1129.1
Current children cumulated vsize (Kb) 140124

[startup+1140.08 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 54297 0 0 0 113722 188 0 0 25 0 1 0 1785192857 142057472 19725 4294967295 134512640 135094434 3221224448 3216719520 134597029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 34682 19725 145 145 0 34537 0
[pid=25986] vsize: 138728
Current children cumulated CPU time (s) 1139.1
Current children cumulated vsize (Kb) 140852

[startup+1150.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 54495 0 0 0 114719 189 0 0 25 0 1 0 1785192857 142684160 19923 4294967295 134512640 135094434 3221224448 3219452448 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 34835 19923 145 145 0 34690 0
[pid=25986] vsize: 139340
Current children cumulated CPU time (s) 1149.08
Current children cumulated vsize (Kb) 141464

[startup+1160.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 54588 0 0 0 115719 189 0 0 25 0 1 0 1785192857 142979072 20016 4294967295 134512640 135094434 3221224448 3220727392 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 34907 20016 145 145 0 34762 0
[pid=25986] vsize: 139628
Current children cumulated CPU time (s) 1159.08
Current children cumulated vsize (Kb) 141752

[startup+1170.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 54879 0 0 0 116718 190 0 0 25 0 1 0 1785192857 142823424 20028 4294967295 134512640 135094434 3221224448 3217172720 134597017 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 34869 20028 145 145 0 34724 0
[pid=25986] vsize: 139476
Current children cumulated CPU time (s) 1169.08
Current children cumulated vsize (Kb) 141600

[startup+1180.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 54985 0 0 0 117718 191 0 0 25 0 1 0 1785192857 142991360 20092 4294967295 134512640 135094434 3221224448 3218559776 134597094 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 34910 20092 145 145 0 34765 0
[pid=25986] vsize: 139640
Current children cumulated CPU time (s) 1179.09
Current children cumulated vsize (Kb) 141764

[startup+1190.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 54998 0 0 0 118718 191 0 0 25 0 1 0 1785192857 142991360 20105 4294967295 134512640 135094434 3221224448 3219367440 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 34910 20105 145 145 0 34765 0
[pid=25986] vsize: 139640
Current children cumulated CPU time (s) 1189.09
Current children cumulated vsize (Kb) 141764

[startup+1200.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 55008 0 0 0 119718 191 0 0 25 0 1 0 1785192857 142991360 20115 4294967295 134512640 135094434 3221224448 3219981504 134597014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 34910 20115 145 145 0 34765 0
[pid=25986] vsize: 139640
Current children cumulated CPU time (s) 1199.09
Current children cumulated vsize (Kb) 141764

[startup+1210.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 55017 0 0 0 120719 191 0 0 25 0 1 0 1785192857 142991360 20124 4294967295 134512640 135094434 3221224448 3220500000 134597029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 34910 20124 145 145 0 34765 0
[pid=25986] vsize: 139640
Current children cumulated CPU time (s) 1209.1
Current children cumulated vsize (Kb) 141764



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 25986
Raw data (/proc/25982/stat): 25982 (minisat+_script) S 25981 25982 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785192852 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25982/statm): 531 226 485 147 0 384 0
[pid=25982] vsize: 2124
Raw data (/proc/25986/stat): 25986 (minisat+_64-bit) R 25982 25982 15400 0 -1 0 55017 0 0 0 120719 191 0 0 25 0 1 0 1785192857 142991360 20124 4294967295 134512640 135094434 3221224448 3220500000 134597094 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25986/statm): 34910 20124 145 145 0 34765 0
[pid=25986] vsize: 139640
Current children cumulated CPU time (s) 1209.1
Current children cumulated vsize (Kb) 141764

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

Child status: 0
Real time (s): 1210.13
CPU time (s): 1209.14
CPU user time (s): 1207.19
CPU system time (s): 1.9517
CPU usage (%): 99.9186
Max. virtual memory (cumulated for all children) (Kb): 141764



Verifier Data




ERROR: no interpretation found !