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-stair.opb
MD5SUMf2a6dc8d2697a7f5959c84e4079088c9
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableNO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 30
Biggest coefficient in the objective function 536870912
Number of bits for the biggest coefficient in the objective function 30
Sum of the numbers in the objective function 1073741823
Number of bits of the sum of numbers in the objective function 30
Biggest number in a constraint 528959045369856
Number of bits of the biggest number in a constraint 49
Biggest sum of numbers in a constraint 3702118998041541
Number of bits of the biggest sum of numbers52
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark204.283
Number of variables11454
Total number of constraints362
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 constraints362
Minimum length of a constraint13
Maximum length of a constraint810

Trace number 2675

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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:        912432 kB
Buffers:         34424 kB
Cached:          63804 kB
SwapCached:        780 kB
Active:          65052 kB
Inactive:        35892 kB
HighTotal:      131008 kB
HighFree:        63532 kB
LowTotal:       903652 kB
LowFree:        848900 kB
SwapTotal:     2097136 kB
SwapFree:      2095888 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5804 kB
Slab:            15652 kB
Committed_AS:    64300 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 20:58:06 (client local time) WITH STATUS 0 IN 1209.91 SECONDS
stats: 2823 7 1209.91 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 478] 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/13392/stat): 13392 (minisat+_script) R 13391 13392 824 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1785971103 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/13392/statm): 174 3 169 147 0 27 0
[pid=13392] 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=13393
New process pid=13394
New process pid=13395
execve syscall for /bin/sed executable
One traced child (pid=13394) 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=13395) exited with status: 0
One traced child (pid=13393) exited with status: 0
New process pid=13396
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-stair.opb
One traced child (pid=13396) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=13397
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-stair.opb

[startup+10.0035 s]
Raw data (loadavg): 0.93 0.96 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 945 14 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221218292 134522324 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0
[pid=13397] vsize: 10028
Current children cumulated CPU time (s) 9.61
Current children cumulated vsize (Kb) 12156

[startup+20.0043 s]
Raw data (loadavg): 0.94 0.96 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 1946 14 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221219340 134722656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0
[pid=13397] vsize: 10028
Current children cumulated CPU time (s) 19.62
Current children cumulated vsize (Kb) 12156

[startup+30.005 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 2946 14 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221219100 134723267 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0
[pid=13397] vsize: 10028
Current children cumulated CPU time (s) 29.62
Current children cumulated vsize (Kb) 12156

[startup+40.0058 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 3946 14 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221219440 134845895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0
[pid=13397] vsize: 10028
Current children cumulated CPU time (s) 39.62
Current children cumulated vsize (Kb) 12156

[startup+50.0065 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 4946 14 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221219216 134844715 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0
[pid=13397] vsize: 10028
Current children cumulated CPU time (s) 49.62
Current children cumulated vsize (Kb) 12156

[startup+60.0062 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 5946 14 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221219376 134628744 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0
[pid=13397] vsize: 10028
Current children cumulated CPU time (s) 59.62
Current children cumulated vsize (Kb) 12156

[startup+70.007 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 6946 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221220056 134843032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0
[pid=13397] vsize: 10028
Current children cumulated CPU time (s) 69.63
Current children cumulated vsize (Kb) 12156

[startup+80.0077 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 7947 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221219552 134629445 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0
[pid=13397] vsize: 10028
Current children cumulated CPU time (s) 79.64
Current children cumulated vsize (Kb) 12156

[startup+90.0085 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 8947 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221220048 134693582 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0
[pid=13397] vsize: 10028
Current children cumulated CPU time (s) 89.64
Current children cumulated vsize (Kb) 12156

[startup+100.009 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 9947 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221219680 134694517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0
[pid=13397] vsize: 10028
Current children cumulated CPU time (s) 99.64
Current children cumulated vsize (Kb) 12156

[startup+110.01 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 10947 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221220056 134693808 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0
[pid=13397] vsize: 10028
Current children cumulated CPU time (s) 109.64
Current children cumulated vsize (Kb) 12156

[startup+120.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 11947 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221220044 134722660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0
[pid=13397] vsize: 10028
Current children cumulated CPU time (s) 119.64
Current children cumulated vsize (Kb) 12156

[startup+130.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 12948 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221220308 134844636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0
[pid=13397] vsize: 10028
Current children cumulated CPU time (s) 129.65
Current children cumulated vsize (Kb) 12156

[startup+140.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 13948 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221220524 134722225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0
[pid=13397] vsize: 10028
Current children cumulated CPU time (s) 139.65
Current children cumulated vsize (Kb) 12156

[startup+150.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 14948 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221220904 134722513 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0
[pid=13397] vsize: 10028
Current children cumulated CPU time (s) 149.65
Current children cumulated vsize (Kb) 12156

[startup+160.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 15948 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221220588 134694551 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0
[pid=13397] vsize: 10028
Current children cumulated CPU time (s) 159.65
Current children cumulated vsize (Kb) 12156

[startup+170.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 16948 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221221376 134696366 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0
[pid=13397] vsize: 10028
Current children cumulated CPU time (s) 169.65
Current children cumulated vsize (Kb) 12156

[startup+180.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 17949 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221220672 134696726 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0
[pid=13397] vsize: 10028
Current children cumulated CPU time (s) 179.66
Current children cumulated vsize (Kb) 12156

[startup+190.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 18949 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221220832 134845930 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0
[pid=13397] vsize: 10028
Current children cumulated CPU time (s) 189.66
Current children cumulated vsize (Kb) 12156

[startup+200.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 19949 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221221128 134629047 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0
[pid=13397] vsize: 10028
Current children cumulated CPU time (s) 199.66
Current children cumulated vsize (Kb) 12156

[startup+210.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 20949 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221221392 134696578 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0
[pid=13397] vsize: 10028
Current children cumulated CPU time (s) 209.66
Current children cumulated vsize (Kb) 12156

[startup+220.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 21949 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221220864 134843402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0
[pid=13397] vsize: 10028
Current children cumulated CPU time (s) 219.66
Current children cumulated vsize (Kb) 12156

[startup+230.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 22951 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221221264 134694435 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0
[pid=13397] vsize: 10028
Current children cumulated CPU time (s) 229.68
Current children cumulated vsize (Kb) 12156

[startup+240.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 23951 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221221552 134843420 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0
[pid=13397] vsize: 10028
Current children cumulated CPU time (s) 239.68
Current children cumulated vsize (Kb) 12156

[startup+250.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 24951 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221221360 134845927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0
[pid=13397] vsize: 10028
Current children cumulated CPU time (s) 249.68
Current children cumulated vsize (Kb) 12156

[startup+260.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 25951 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221221216 134723225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0
[pid=13397] vsize: 10028
Current children cumulated CPU time (s) 259.68
Current children cumulated vsize (Kb) 12156

[startup+270.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 26952 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221221424 134722521 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0
[pid=13397] vsize: 10028
Current children cumulated CPU time (s) 269.69
Current children cumulated vsize (Kb) 12156

[startup+280.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 27952 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221221624 134722513 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0
[pid=13397] vsize: 10028
Current children cumulated CPU time (s) 279.69
Current children cumulated vsize (Kb) 12156

[startup+290.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 28952 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221221264 134849122 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0
[pid=13397] vsize: 10028
Current children cumulated CPU time (s) 289.69
Current children cumulated vsize (Kb) 12156

[startup+300.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 29952 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221221552 134845927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0
[pid=13397] vsize: 10028
Current children cumulated CPU time (s) 299.69
Current children cumulated vsize (Kb) 12156

[startup+310.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2418 0 3 0 30952 15 0 0 25 0 1 0 1785971109 10268672 2335 4294967295 134512640 135167914 3221224448 3221221392 134696233 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2507 2335 162 162 0 2345 0
[pid=13397] vsize: 10028
Current children cumulated CPU time (s) 309.69
Current children cumulated vsize (Kb) 12156

[startup+320.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2733 0 3 0 31951 17 0 0 25 0 1 0 1785971109 11358208 2608 4294967295 134512640 135167914 3221224448 3221218428 134842996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2773 2608 162 162 0 2611 0
[pid=13397] vsize: 11092
Current children cumulated CPU time (s) 319.7
Current children cumulated vsize (Kb) 13220

[startup+330.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2733 0 3 0 32951 17 0 0 25 0 1 0 1785971109 11358208 2608 4294967295 134512640 135167914 3221224448 3221218764 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2773 2608 162 162 0 2611 0
[pid=13397] vsize: 11092
Current children cumulated CPU time (s) 329.7
Current children cumulated vsize (Kb) 13220

[startup+340.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2733 0 3 0 33951 17 0 0 25 0 1 0 1785971109 11358208 2608 4294967295 134512640 135167914 3221224448 3221219460 134843031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2773 2608 162 162 0 2611 0
[pid=13397] vsize: 11092
Current children cumulated CPU time (s) 339.7
Current children cumulated vsize (Kb) 13220

[startup+350.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2733 0 3 0 34952 17 0 0 25 0 1 0 1785971109 11358208 2608 4294967295 134512640 135167914 3221224448 3221220016 134843118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2773 2608 162 162 0 2611 0
[pid=13397] vsize: 11092
Current children cumulated CPU time (s) 349.71
Current children cumulated vsize (Kb) 13220

[startup+360.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2733 0 3 0 35952 17 0 0 25 0 1 0 1785971109 11358208 2608 4294967295 134512640 135167914 3221224448 3221220320 134844653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2773 2608 162 162 0 2611 0
[pid=13397] vsize: 11092
Current children cumulated CPU time (s) 359.71
Current children cumulated vsize (Kb) 13220

[startup+370.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2733 0 3 0 36952 17 0 0 25 0 1 0 1785971109 11358208 2608 4294967295 134512640 135167914 3221224448 3221220736 134849082 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2773 2608 162 162 0 2611 0
[pid=13397] vsize: 11092
Current children cumulated CPU time (s) 369.71
Current children cumulated vsize (Kb) 13220

[startup+380.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2733 0 3 0 37952 17 0 0 25 0 1 0 1785971109 11358208 2608 4294967295 134512640 135167914 3221224448 3221221060 134845880 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2773 2608 162 162 0 2611 0
[pid=13397] vsize: 11092
Current children cumulated CPU time (s) 379.71
Current children cumulated vsize (Kb) 13220

[startup+390.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2733 0 3 0 38952 17 0 0 25 0 1 0 1785971109 11358208 2608 4294967295 134512640 135167914 3221224448 3221221184 134843123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2773 2608 162 162 0 2611 0
[pid=13397] vsize: 11092
Current children cumulated CPU time (s) 389.71
Current children cumulated vsize (Kb) 13220

[startup+400.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2733 0 3 0 39953 17 0 0 25 0 1 0 1785971109 11358208 2608 4294967295 134512640 135167914 3221224448 3221221424 134522468 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2773 2608 162 162 0 2611 0
[pid=13397] vsize: 11092
Current children cumulated CPU time (s) 399.72
Current children cumulated vsize (Kb) 13220

[startup+410.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2733 0 3 0 40953 17 0 0 25 0 1 0 1785971109 11358208 2608 4294967295 134512640 135167914 3221224448 3221221280 134849163 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2773 2608 162 162 0 2611 0
[pid=13397] vsize: 11092
Current children cumulated CPU time (s) 409.72
Current children cumulated vsize (Kb) 13220

[startup+420.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2733 0 3 0 41953 17 0 0 25 0 1 0 1785971109 11358208 2608 4294967295 134512640 135167914 3221224448 3221221640 134693826 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2773 2608 162 162 0 2611 0
[pid=13397] vsize: 11092
Current children cumulated CPU time (s) 419.72
Current children cumulated vsize (Kb) 13220

[startup+430.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2733 0 3 0 42953 17 0 0 25 0 1 0 1785971109 11358208 2608 4294967295 134512640 135167914 3221224448 3221222256 134844708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2773 2608 162 162 0 2611 0
[pid=13397] vsize: 11092
Current children cumulated CPU time (s) 429.72
Current children cumulated vsize (Kb) 13220

[startup+440.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2733 0 3 0 43954 17 0 0 25 0 1 0 1785971109 11358208 2608 4294967295 134512640 135167914 3221224448 3221222256 134696738 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2773 2608 162 162 0 2611 0
[pid=13397] vsize: 11092
Current children cumulated CPU time (s) 439.73
Current children cumulated vsize (Kb) 13220

[startup+450.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 44954 17 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221217148 134845876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 449.73
Current children cumulated vsize (Kb) 13232

[startup+460.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 45954 17 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221217944 134843032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 459.73
Current children cumulated vsize (Kb) 13232

[startup+470.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 46954 17 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221218652 134693552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 469.73
Current children cumulated vsize (Kb) 13232

[startup+480.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 47954 18 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221218192 134843118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 479.74
Current children cumulated vsize (Kb) 13232

[startup+490.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 48954 18 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221218824 134522321 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 489.74
Current children cumulated vsize (Kb) 13232

[startup+500.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 49954 18 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221218428 134844632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 499.74
Current children cumulated vsize (Kb) 13232

[startup+510.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 50954 18 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221219248 134845927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 509.74
Current children cumulated vsize (Kb) 13232

[startup+520.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 51954 19 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221219536 134630875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 519.75
Current children cumulated vsize (Kb) 13232

[startup+530.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 52954 19 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221219264 134844676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 529.75
Current children cumulated vsize (Kb) 13232

[startup+540.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 53954 19 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221220016 134843123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 539.75
Current children cumulated vsize (Kb) 13232

[startup+550.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 54954 19 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221219296 134718188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 549.75
Current children cumulated vsize (Kb) 13232

[startup+560.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 55954 19 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221219492 134843117 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 559.75
Current children cumulated vsize (Kb) 13232

[startup+570.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 56954 19 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221220048 134693582 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 569.75
Current children cumulated vsize (Kb) 13232

[startup+580.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 57955 19 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221219768 134844633 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 579.76
Current children cumulated vsize (Kb) 13232

[startup+590.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 58955 19 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221219520 134849102 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 589.76
Current children cumulated vsize (Kb) 13232

[startup+600.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 59955 19 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221219804 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 599.76
Current children cumulated vsize (Kb) 13232

[startup+610.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 60955 19 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221220184 134844633 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 609.76
Current children cumulated vsize (Kb) 13232

[startup+620.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 61956 19 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221219836 134844632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 619.77
Current children cumulated vsize (Kb) 13232

[startup+630.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 62956 19 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221220156 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 629.77
Current children cumulated vsize (Kb) 13232

[startup+640.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 63956 19 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221220400 134849096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 639.77
Current children cumulated vsize (Kb) 13232

[startup+650.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 64956 19 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221220512 134723288 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 649.77
Current children cumulated vsize (Kb) 13232

[startup+660.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 65956 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221220716 134842996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 659.78
Current children cumulated vsize (Kb) 13232

[startup+670.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 66956 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221220864 134843406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 669.78
Current children cumulated vsize (Kb) 13232

[startup+680.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 67957 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221220576 134849092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 679.79
Current children cumulated vsize (Kb) 13232

[startup+690.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 68957 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221221216 134843130 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 689.79
Current children cumulated vsize (Kb) 13232

[startup+700.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 69957 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221221200 134843036 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 699.79
Current children cumulated vsize (Kb) 13232

[startup+710.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 70957 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221221024 134844706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 709.79
Current children cumulated vsize (Kb) 13232

[startup+720.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 71957 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221220912 134843139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 719.79
Current children cumulated vsize (Kb) 13232

[startup+730.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 72958 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221220848 134696285 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 729.8
Current children cumulated vsize (Kb) 13232

[startup+740.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 73958 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221221104 134849082 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 739.8
Current children cumulated vsize (Kb) 13232

[startup+750.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 74958 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221220912 134694528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 749.8
Current children cumulated vsize (Kb) 13232

[startup+760.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 75958 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221221008 134845933 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 759.8
Current children cumulated vsize (Kb) 13232

[startup+770.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 76958 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221221464 134696561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 769.8
Current children cumulated vsize (Kb) 13232

[startup+780.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 77959 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221221104 134849066 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 779.81
Current children cumulated vsize (Kb) 13232

[startup+790.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 78959 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221221248 134845881 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 789.81
Current children cumulated vsize (Kb) 13232

[startup+800.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 79959 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221220840 134844633 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 799.81
Current children cumulated vsize (Kb) 13232

[startup+810.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 80959 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221221488 134844728 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 809.81
Current children cumulated vsize (Kb) 13232

[startup+820.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 81959 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221221036 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 819.81
Current children cumulated vsize (Kb) 13232

[startup+830.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 82960 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221221760 134695257 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 829.82
Current children cumulated vsize (Kb) 13232

[startup+840.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 83960 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221221840 134628639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 839.82
Current children cumulated vsize (Kb) 13232

[startup+850.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 84960 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221221920 134849092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 849.82
Current children cumulated vsize (Kb) 13232

[startup+860.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 85960 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221221564 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 859.82
Current children cumulated vsize (Kb) 13232

[startup+870.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2736 0 3 0 86961 20 0 0 25 0 1 0 1785971109 11370496 2611 4294967295 134512640 135167914 3221224448 3221222320 134843107 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2776 2611 162 162 0 2614 0
[pid=13397] vsize: 11104
Current children cumulated CPU time (s) 869.83
Current children cumulated vsize (Kb) 13232

[startup+880.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 87960 21 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221217152 134845918 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0
[pid=13397] vsize: 11668
Current children cumulated CPU time (s) 879.83
Current children cumulated vsize (Kb) 13796

[startup+890.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 88960 21 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221217584 134849110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0
[pid=13397] vsize: 11668
Current children cumulated CPU time (s) 889.83
Current children cumulated vsize (Kb) 13796

[startup+900.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 89960 21 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221217392 134849061 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0
[pid=13397] vsize: 11668
Current children cumulated CPU time (s) 899.83
Current children cumulated vsize (Kb) 13796

[startup+910.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 90960 21 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221217440 134844676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0
[pid=13397] vsize: 11668
Current children cumulated CPU time (s) 909.83
Current children cumulated vsize (Kb) 13796

[startup+920.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 91961 21 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221217792 134844647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0
[pid=13397] vsize: 11668
Current children cumulated CPU time (s) 919.84
Current children cumulated vsize (Kb) 13796

[startup+930.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 92961 21 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221218444 134845876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0
[pid=13397] vsize: 11668
Current children cumulated CPU time (s) 929.84
Current children cumulated vsize (Kb) 13796

[startup+940.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 93961 21 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221217856 134845903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0
[pid=13397] vsize: 11668
Current children cumulated CPU time (s) 939.84
Current children cumulated vsize (Kb) 13796

[startup+950.079 s]
Raw data (loadavg): 1.07 0.99 0.92 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 94961 21 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221218640 134693576 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0
[pid=13397] vsize: 11668
Current children cumulated CPU time (s) 949.84
Current children cumulated vsize (Kb) 13796

[startup+960.08 s]
Raw data (loadavg): 1.06 0.99 0.92 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 95962 21 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221218292 134522188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0
[pid=13397] vsize: 11668
Current children cumulated CPU time (s) 959.85
Current children cumulated vsize (Kb) 13796

[startup+970.081 s]
Raw data (loadavg): 1.05 0.99 0.92 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 96962 21 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221218652 134522320 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0
[pid=13397] vsize: 11668
Current children cumulated CPU time (s) 969.85
Current children cumulated vsize (Kb) 13796

[startup+980.082 s]
Raw data (loadavg): 1.04 0.99 0.92 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 97962 21 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221218436 134843117 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0
[pid=13397] vsize: 11668
Current children cumulated CPU time (s) 979.85
Current children cumulated vsize (Kb) 13796

[startup+990.083 s]
Raw data (loadavg): 1.04 0.99 0.92 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 98962 21 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221218280 134849057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0
[pid=13397] vsize: 11668
Current children cumulated CPU time (s) 989.85
Current children cumulated vsize (Kb) 13796

[startup+1000.08 s]
Raw data (loadavg): 1.03 0.99 0.92 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 99963 21 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221218448 134843400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0
[pid=13397] vsize: 11668
Current children cumulated CPU time (s) 999.86
Current children cumulated vsize (Kb) 13796

[startup+1010.08 s]
Raw data (loadavg): 1.03 0.99 0.92 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 100963 21 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221218976 134849187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0
[pid=13397] vsize: 11668
Current children cumulated CPU time (s) 1009.86
Current children cumulated vsize (Kb) 13796

[startup+1020.09 s]
Raw data (loadavg): 1.02 0.99 0.92 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 101963 21 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221219360 134629236 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0
[pid=13397] vsize: 11668
Current children cumulated CPU time (s) 1019.86
Current children cumulated vsize (Kb) 13796

[startup+1030.09 s]
Raw data (loadavg): 1.02 0.99 0.92 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 102963 21 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221219328 134843153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0
[pid=13397] vsize: 11668
Current children cumulated CPU time (s) 1029.86
Current children cumulated vsize (Kb) 13796

[startup+1040.09 s]
Raw data (loadavg): 1.01 0.99 0.92 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 103964 21 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221219148 134722542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0
[pid=13397] vsize: 11668
Current children cumulated CPU time (s) 1039.87
Current children cumulated vsize (Kb) 13796

[startup+1050.09 s]
Raw data (loadavg): 1.01 0.99 0.92 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 104964 21 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221218956 134845882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0
[pid=13397] vsize: 11668
Current children cumulated CPU time (s) 1049.87
Current children cumulated vsize (Kb) 13796

[startup+1060.09 s]
Raw data (loadavg): 1.01 0.99 0.92 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 105964 21 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221219296 134693582 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0
[pid=13397] vsize: 11668
Current children cumulated CPU time (s) 1059.87
Current children cumulated vsize (Kb) 13796

[startup+1070.09 s]
Raw data (loadavg): 1.01 0.99 0.92 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 106964 21 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221219040 134844718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0
[pid=13397] vsize: 11668
Current children cumulated CPU time (s) 1069.87
Current children cumulated vsize (Kb) 13796

[startup+1080.09 s]
Raw data (loadavg): 1.01 0.99 0.92 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 107964 22 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221218944 134844637 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0
[pid=13397] vsize: 11668
Current children cumulated CPU time (s) 1079.88
Current children cumulated vsize (Kb) 13796

[startup+1090.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 108964 22 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221219364 134629267 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0
[pid=13397] vsize: 11668
Current children cumulated CPU time (s) 1089.88
Current children cumulated vsize (Kb) 13796

[startup+1100.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 109964 22 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221219188 134629364 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0
[pid=13397] vsize: 11668
Current children cumulated CPU time (s) 1099.88
Current children cumulated vsize (Kb) 13796

[startup+1110.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 110964 23 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221219352 134522234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0
[pid=13397] vsize: 11668
Current children cumulated CPU time (s) 1109.89
Current children cumulated vsize (Kb) 13796

[startup+1120.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 111964 23 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221219708 134694368 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0
[pid=13397] vsize: 11668
Current children cumulated CPU time (s) 1119.89
Current children cumulated vsize (Kb) 13796

[startup+1130.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 112964 23 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221219456 134696608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0
[pid=13397] vsize: 11668
Current children cumulated CPU time (s) 1129.89
Current children cumulated vsize (Kb) 13796

[startup+1140.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 113964 23 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221220208 134694532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0
[pid=13397] vsize: 11668
Current children cumulated CPU time (s) 1139.89
Current children cumulated vsize (Kb) 13796

[startup+1150.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 114965 23 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221219872 134849108 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0
[pid=13397] vsize: 11668
Current children cumulated CPU time (s) 1149.9
Current children cumulated vsize (Kb) 13796

[startup+1160.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 115965 23 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221219716 134629088 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0
[pid=13397] vsize: 11668
Current children cumulated CPU time (s) 1159.9
Current children cumulated vsize (Kb) 13796

[startup+1170.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 116965 23 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221219664 134522338 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0
[pid=13397] vsize: 11668
Current children cumulated CPU time (s) 1169.9
Current children cumulated vsize (Kb) 13796

[startup+1180.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 117965 23 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221219932 134844638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0
[pid=13397] vsize: 11668
Current children cumulated CPU time (s) 1179.9
Current children cumulated vsize (Kb) 13796

[startup+1190.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 118965 23 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221219868 134722512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0
[pid=13397] vsize: 11668
Current children cumulated CPU time (s) 1189.9
Current children cumulated vsize (Kb) 13796

[startup+1200.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 119965 23 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221219644 134849056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0
[pid=13397] vsize: 11668
Current children cumulated CPU time (s) 1199.9
Current children cumulated vsize (Kb) 13796

[startup+1210.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 120966 23 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221219600 134845913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0
[pid=13397] vsize: 11668
Current children cumulated CPU time (s) 1209.91
Current children cumulated vsize (Kb) 13796



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 13397
Raw data (/proc/13392/stat): 13392 (minisat+_script) S 13391 13392 824 0 -1 0 314 340 0 0 0 1 0 1 22 0 1 0 1785971103 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13392/statm): 532 234 485 147 0 385 0
[pid=13392] vsize: 2128
Raw data (/proc/13397/stat): 13397 (minisat+_bignum) R 13392 13392 824 0 -1 0 2839 0 3 0 120966 23 0 0 25 0 1 0 1785971109 11948032 2682 4294967295 134512640 135167914 3221224448 3221219616 134696726 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13397/statm): 2917 2682 162 162 0 2755 0
[pid=13397] vsize: 11668
Current children cumulated CPU time (s) 1209.91
Current children cumulated vsize (Kb) 13796

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

Child status: 0
Real time (s): 1210.11
CPU time (s): 1209.91
CPU user time (s): 1209.66
CPU system time (s): 0.244962
CPU usage (%): 99.983
Max. virtual memory (cumulated for all children) (Kb): 13796

Verifier Data

ERROR: no interpretation found !