Some explanations

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

General information on the benchmark

Namemps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-modszk1.opb
MD5SUM4c80436c6cab58e82888f1a9aa37d4f5
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 29700
Biggest coefficient in the objective function 197378980184064000
Number of bits for the biggest coefficient in the objective function 58
Sum of the numbers in the objective function -3892337408572559116
Number of bits of the sum of numbers in the objective function 64
Biggest number in a constraint 197378980184064000
Number of bits of the biggest number in a constraint 58
Biggest sum of numbers in a constraint -3892337408572559116
Number of bits of the biggest sum of numbers64
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables48602
Total number of constraints686
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints686
Minimum length of a constraint30
Maximum length of a constraint600

Trace number 2662

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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:        900300 kB
Buffers:         34860 kB
Cached:          71772 kB
SwapCached:        536 kB
Active:          70048 kB
Inactive:        39124 kB
HighTotal:      131008 kB
HighFree:        57232 kB
LowTotal:       903652 kB
LowFree:        843068 kB
SwapTotal:     2097892 kB
SwapFree:      2096832 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5864 kB
Slab:            19528 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 20:49:44 (client local time) WITH STATUS 0 IN 1209.6 SECONDS
stats: 2788 7 1209.6 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 1624] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...

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/2189/stat): 2189 (minisat+_script) R 2188 2189 21452 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1844143807 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/2189/statm): 174 3 169 147 0 27 0
[pid=2189] 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=2190
New process pid=2191
New process pid=2192
execve syscall for /bin/sed executable
One traced child (pid=2191) 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=2192) exited with status: 0
One traced child (pid=2190) exited with status: 0
New process pid=2193
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-20-10-modszk1.opb
One traced child (pid=2193) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=2194
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-20-10-modszk1.opb

[startup+10.0038 s]
Raw data (loadavg): 0.93 0.96 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 4258 0 3 0 928 23 0 0 25 0 1 0 1844143814 18567168 4122 4294967295 134512640 135167914 3221224448 3221222884 134608523 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2194/statm): 4533 4122 162 162 0 4371 0
[pid=2194] vsize: 18132
Current children cumulated CPU time (s) 9.53
Current children cumulated vsize (Kb) 20260

[startup+20.0045 s]
Raw data (loadavg): 0.94 0.96 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 1888 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221216688 134843036 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 19.31
Current children cumulated vsize (Kb) 33288

[startup+30.0052 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 2889 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221218112 134694351 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 29.32
Current children cumulated vsize (Kb) 33288

[startup+40.0059 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 3889 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219328 134849110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 39.32
Current children cumulated vsize (Kb) 33288

[startup+50.0066 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 4889 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221218556 134845876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 49.32
Current children cumulated vsize (Kb) 33288

[startup+60.0073 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 5889 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219180 134694480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 59.32
Current children cumulated vsize (Kb) 33288

[startup+70.008 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 6889 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221218992 134849113 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 69.32
Current children cumulated vsize (Kb) 33288

[startup+80.0097 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 7890 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219056 134844672 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 79.33
Current children cumulated vsize (Kb) 33288

[startup+90.0104 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 8890 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221220048 134843001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 89.33
Current children cumulated vsize (Kb) 33288

[startup+100.01 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 9890 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221218972 134722542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 99.33
Current children cumulated vsize (Kb) 33288

[startup+110.013 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 10891 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221217776 134629248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 109.34
Current children cumulated vsize (Kb) 33288

[startup+120.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 11891 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221218996 134696564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 119.34
Current children cumulated vsize (Kb) 33288

[startup+130.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 12891 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221218076 134843033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 129.34
Current children cumulated vsize (Kb) 33288

[startup+140.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 13891 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219792 134843107 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 139.34
Current children cumulated vsize (Kb) 33288

[startup+150.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 14892 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221220144 134844728 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 149.35
Current children cumulated vsize (Kb) 33288

[startup+160.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 15892 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221218924 134845876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 159.35
Current children cumulated vsize (Kb) 33288

[startup+170.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 16892 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219852 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 169.35
Current children cumulated vsize (Kb) 33288

[startup+180.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 17892 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219344 134693582 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 179.35
Current children cumulated vsize (Kb) 33288

[startup+190.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 18893 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219308 134844632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 189.36
Current children cumulated vsize (Kb) 33288

[startup+200.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 19893 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221218960 134843123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 199.36
Current children cumulated vsize (Kb) 33288

[startup+210.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 20893 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221218832 134630818 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 209.36
Current children cumulated vsize (Kb) 33288

[startup+220.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 21893 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221218992 134849066 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 219.36
Current children cumulated vsize (Kb) 33288

[startup+230.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 22894 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221218824 134849057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 229.37
Current children cumulated vsize (Kb) 33288

[startup+240.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 23894 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221218824 134694366 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 239.37
Current children cumulated vsize (Kb) 33288

[startup+250.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 24894 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219696 134849092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 249.37
Current children cumulated vsize (Kb) 33288

[startup+260.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 25894 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219500 134722512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 259.37
Current children cumulated vsize (Kb) 33288

[startup+270.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 26894 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219344 134849068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 269.37
Current children cumulated vsize (Kb) 33288

[startup+280.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 27895 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219328 134849122 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 279.38
Current children cumulated vsize (Kb) 33288

[startup+290.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 28895 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221218076 134845882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 289.38
Current children cumulated vsize (Kb) 33288

[startup+300.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 29895 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221220508 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 299.38
Current children cumulated vsize (Kb) 33288

[startup+310.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 30895 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221218296 134693776 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 309.38
Current children cumulated vsize (Kb) 33288

[startup+320.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 31896 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221220060 134842996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 319.39
Current children cumulated vsize (Kb) 33288

[startup+330.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 32896 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219872 134849187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 329.39
Current children cumulated vsize (Kb) 33288

[startup+340.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 33896 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221218240 134718497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 339.39
Current children cumulated vsize (Kb) 33288

[startup+350.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 34896 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219292 134845882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 349.39
Current children cumulated vsize (Kb) 33288

[startup+360.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 35896 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219792 134696745 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 359.39
Current children cumulated vsize (Kb) 33288

[startup+370.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 36897 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221218288 134693582 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 369.4
Current children cumulated vsize (Kb) 33288

[startup+380.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 37897 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221218440 134845939 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 379.4
Current children cumulated vsize (Kb) 33288

[startup+390.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 38897 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221217692 134723285 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 389.4
Current children cumulated vsize (Kb) 33288

[startup+400.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 39897 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219696 134693563 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 399.4
Current children cumulated vsize (Kb) 33288

[startup+410.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 40898 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221218256 134843123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 409.41
Current children cumulated vsize (Kb) 33288

[startup+420.031 s]
Raw data (loadavg): 0.99 0.97 0.91 3/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 41898 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219100 134723240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 419.41
Current children cumulated vsize (Kb) 33288

[startup+430.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 42898 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221220360 134842997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 429.41
Current children cumulated vsize (Kb) 33288

[startup+440.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 43898 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219376 134630843 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 439.41
Current children cumulated vsize (Kb) 33288

[startup+450.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 44899 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221220320 134696304 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 449.42
Current children cumulated vsize (Kb) 33288

[startup+460.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 45899 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221218964 134843117 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 459.42
Current children cumulated vsize (Kb) 33288

[startup+470.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 46899 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219636 134723216 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 469.42
Current children cumulated vsize (Kb) 33288

[startup+480.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 47899 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219952 134845927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 479.42
Current children cumulated vsize (Kb) 33288

[startup+490.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 48900 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221220208 134843064 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 489.43
Current children cumulated vsize (Kb) 33288

[startup+500.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 49900 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219184 134629275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 499.43
Current children cumulated vsize (Kb) 33288

[startup+510.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 50900 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221218912 134844708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 509.43
Current children cumulated vsize (Kb) 33288

[startup+520.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 51900 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221218768 134695319 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 519.43
Current children cumulated vsize (Kb) 33288

[startup+530.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 52901 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219952 134844637 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 529.44
Current children cumulated vsize (Kb) 33288

[startup+540.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 53901 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221217336 134693615 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 539.44
Current children cumulated vsize (Kb) 33288

[startup+550.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 54901 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219352 134522321 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 549.44
Current children cumulated vsize (Kb) 33288

[startup+560.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 55901 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219216 134845895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 559.44
Current children cumulated vsize (Kb) 33288

[startup+570.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 56902 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221220064 134630870 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 569.45
Current children cumulated vsize (Kb) 33288

[startup+580.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 57902 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219200 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 579.45
Current children cumulated vsize (Kb) 33288

[startup+590.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 58902 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219856 134843036 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 589.45
Current children cumulated vsize (Kb) 33288

[startup+600.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 59902 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221220224 134693582 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 599.45
Current children cumulated vsize (Kb) 33288

[startup+610.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 60903 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221218928 134843081 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 609.46
Current children cumulated vsize (Kb) 33288

[startup+620.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 61903 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219508 134849060 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 619.46
Current children cumulated vsize (Kb) 33288

[startup+630.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 62903 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221220208 134849153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 629.46
Current children cumulated vsize (Kb) 33288

[startup+640.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 63903 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221220736 134694386 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 639.46
Current children cumulated vsize (Kb) 33288

[startup+650.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 64903 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219888 134629340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 649.46
Current children cumulated vsize (Kb) 33288

[startup+660.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 65904 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221221024 134844725 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 659.47
Current children cumulated vsize (Kb) 33288

[startup+670.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 66904 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221220912 134694532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 669.47
Current children cumulated vsize (Kb) 33288

[startup+680.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 67904 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221220064 134629172 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 679.47
Current children cumulated vsize (Kb) 33288

[startup+690.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 68904 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221218400 134723229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 689.47
Current children cumulated vsize (Kb) 33288

[startup+700.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 69903 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221220384 134843400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 699.46
Current children cumulated vsize (Kb) 33288

[startup+710.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 70903 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219824 134722532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 709.46
Current children cumulated vsize (Kb) 33288

[startup+720.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 71903 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221218736 134844706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 719.46
Current children cumulated vsize (Kb) 33288

[startup+730.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 72904 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219440 134844668 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 729.47
Current children cumulated vsize (Kb) 33288

[startup+740.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 73904 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219568 134844723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 739.47
Current children cumulated vsize (Kb) 33288

[startup+750.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 74904 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221218924 134723236 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 749.47
Current children cumulated vsize (Kb) 33288

[startup+760.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 75904 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221220224 134849068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 759.47
Current children cumulated vsize (Kb) 33288

[startup+770.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 76905 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221220028 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 769.48
Current children cumulated vsize (Kb) 33288

[startup+780.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 77905 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219872 134693582 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 779.48
Current children cumulated vsize (Kb) 33288

[startup+790.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 78905 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221220320 134843406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 789.48
Current children cumulated vsize (Kb) 33288

[startup+800.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 79905 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221221072 134843123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 799.48
Current children cumulated vsize (Kb) 33288

[startup+810.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 80906 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221220432 134845911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 809.49
Current children cumulated vsize (Kb) 33288

[startup+820.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 81906 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219104 134843426 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 819.49
Current children cumulated vsize (Kb) 33288

[startup+830.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 82906 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219680 134843139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 829.49
Current children cumulated vsize (Kb) 33288

[startup+840.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 83906 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221220960 134629402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 839.49
Current children cumulated vsize (Kb) 33288

[startup+850.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 84907 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221220928 134522325 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 849.5
Current children cumulated vsize (Kb) 33288

[startup+860.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 85907 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219616 134843130 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 859.5
Current children cumulated vsize (Kb) 33288

[startup+870.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 86907 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221220400 134849096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 869.5
Current children cumulated vsize (Kb) 33288

[startup+880.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 87908 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219628 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 879.51
Current children cumulated vsize (Kb) 33288

[startup+890.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 88908 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221218736 134844731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 889.51
Current children cumulated vsize (Kb) 33288

[startup+900.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 89908 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221221264 134694517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 899.51
Current children cumulated vsize (Kb) 33288

[startup+910.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 90908 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221218740 134849147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 909.51
Current children cumulated vsize (Kb) 33288

[startup+920.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 91908 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219312 134722539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 919.51
Current children cumulated vsize (Kb) 33288

[startup+930.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 92909 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221218544 134845888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 929.52
Current children cumulated vsize (Kb) 33288

[startup+940.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 93909 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219488 134522839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 939.52
Current children cumulated vsize (Kb) 33288

[startup+950.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 94909 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219156 134849086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 949.52
Current children cumulated vsize (Kb) 33288

[startup+960.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 95909 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219520 134522197 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 959.52
Current children cumulated vsize (Kb) 33288

[startup+970.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 96910 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219324 134845876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 969.53
Current children cumulated vsize (Kb) 33288

[startup+980.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 97910 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219968 134696766 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 979.53
Current children cumulated vsize (Kb) 33288

[startup+990.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 98910 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221217868 134723260 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 989.53
Current children cumulated vsize (Kb) 33288

[startup+1000.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 99910 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221222096 134723229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 999.53
Current children cumulated vsize (Kb) 33288

[startup+1010.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 100911 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221218896 134843123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 1009.54
Current children cumulated vsize (Kb) 33288

[startup+1020.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 101911 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219836 134693552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 1019.54
Current children cumulated vsize (Kb) 33288

[startup+1030.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 102911 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221220688 134843107 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 1029.54
Current children cumulated vsize (Kb) 33288

[startup+1040.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 103911 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221220496 134845927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 1039.54
Current children cumulated vsize (Kb) 33288

[startup+1050.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 104912 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221220880 134693561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 1049.55
Current children cumulated vsize (Kb) 33288

[startup+1060.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 105912 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221220716 134845882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 1059.55
Current children cumulated vsize (Kb) 33288

[startup+1070.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 106912 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219696 134849143 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 1069.55
Current children cumulated vsize (Kb) 33288

[startup+1080.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 107912 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219456 134843001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 1079.55
Current children cumulated vsize (Kb) 33288

[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 108913 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219776 134843123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 1089.56
Current children cumulated vsize (Kb) 33288

[startup+1100.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 109913 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219356 134843033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 1099.56
Current children cumulated vsize (Kb) 33288

[startup+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 110913 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221220656 134843118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 1109.56
Current children cumulated vsize (Kb) 33288

[startup+1120.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 111913 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219328 134843404 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 1119.56
Current children cumulated vsize (Kb) 33288

[startup+1130.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 112914 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221221376 134844706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 1129.57
Current children cumulated vsize (Kb) 33288

[startup+1140.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 113914 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221220496 134843036 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 1139.57
Current children cumulated vsize (Kb) 33288

[startup+1150.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 114914 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221220576 134693570 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 1149.57
Current children cumulated vsize (Kb) 33288

[startup+1160.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 115914 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219792 134696389 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 1159.57
Current children cumulated vsize (Kb) 33288

[startup+1170.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 116915 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221220368 134522492 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 1169.58
Current children cumulated vsize (Kb) 33288

[startup+1180.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 117915 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219728 134844708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 1179.58
Current children cumulated vsize (Kb) 33288

[startup+1190.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 118915 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219844 134843117 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 1189.58
Current children cumulated vsize (Kb) 33288

[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 119915 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221218828 134849088 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 1199.58
Current children cumulated vsize (Kb) 33288

[startup+1210.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 120916 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219644 134723210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 1209.59
Current children cumulated vsize (Kb) 33288



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2194
Raw data (/proc/2189/stat): 2189 (minisat+_script) S 2188 2189 21452 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844143807 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2189/statm): 532 234 485 147 0 385 0
[pid=2189] vsize: 2128
Raw data (/proc/2194/stat): 2194 (minisat+_bignum) R 2189 2189 21452 0 -1 0 9048 0 3 0 120916 41 0 0 25 0 1 0 1844143814 31907840 7390 4294967295 134512640 135167914 3221224448 3221219616 134844691 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2194/statm): 7790 7390 162 162 0 7628 0
[pid=2194] vsize: 31160
Current children cumulated CPU time (s) 1209.59
Current children cumulated vsize (Kb) 33288

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

Child status: 0
Real time (s): 1210.1
CPU time (s): 1209.6
CPU user time (s): 1209.16
CPU system time (s): 0.433934
CPU usage (%): 99.9581
Max. virtual memory (cumulated for all children) (Kb): 33288

Verifier Data

ERROR: no interpretation found !