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-forplan.opb
MD5SUMdfc6e74660e6079f7108351001d51bc8
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 9340
Biggest coefficient in the objective function 6454798974976000
Number of bits for the biggest coefficient in the objective function 53
Sum of the numbers in the objective function 1138676908426644728
Number of bits of the sum of numbers in the objective function 60
Biggest number in a constraint 6454798974976000
Number of bits of the biggest number in a constraint 53
Biggest sum of numbers in a constraint 1138676908426644728
Number of bits of the biggest sum of numbers60
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables12528
Total number of constraints155
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 constraints155
Minimum length of a constraint27
Maximum length of a constraint9090

Trace number 2638

Launcher Data

LAUNCH ON wulflinc2 THE 2005-09-18 20:17:43 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2776 boxname=wulflinc2 idbench=432 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  dfc6e74660e6079f7108351001d51bc8  /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-20-10-forplan.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-20-10-forplan.opb
IDLAUNCH: 2776
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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.191
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:        916772 kB
Buffers:         33880 kB
Cached:          59668 kB
SwapCached:       1040 kB
Active:          62024 kB
Inactive:        34152 kB
HighTotal:      131008 kB
HighFree:        67816 kB
LowTotal:       903652 kB
LowFree:        848956 kB
SwapTotal:     2097136 kB
SwapFree:      2095568 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5696 kB
Slab:            15800 kB
Committed_AS:    72360 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 20:37:54 (client local time) WITH STATUS 0 IN 1204.55 SECONDS
stats: 2776 7 1204.55 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 425] 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/16467/stat): 16467 (minisat+_script) R 16466 16467 6872 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1785856854 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/16467/statm): 174 3 169 147 0 27 0
[pid=16467] 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=16468
New process pid=16469
New process pid=16470
execve syscall for /bin/sed executable
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
One traced child (pid=16469) exited with status: 0
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=16470) exited with status: 0
One traced child (pid=16468) exited with status: 0
New process pid=16471
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-20-10-forplan.opb
One traced child (pid=16471) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=16472
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-20-10-forplan.opb

[startup+10.0037 s]
Raw data (loadavg): 1.01 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 4429 0 3 0 925 24 0 0 25 0 1 0 1785856861 10596352 2230 4294967295 134512640 135167914 3221224448 3221223200 134845911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 2587 2230 162 162 0 2425 0
[pid=16472] vsize: 10348
Current children cumulated CPU time (s) 9.5
Current children cumulated vsize (Kb) 12476

[startup+20.0044 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 5351 0 3 0 1911 30 0 0 25 0 1 0 1785856861 14082048 3099 4294967295 134512640 135167914 3221224448 3221223296 134594189 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 3438 3099 162 162 0 3276 0
[pid=16472] vsize: 13752
Current children cumulated CPU time (s) 19.42
Current children cumulated vsize (Kb) 15880

[startup+30.0061 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 5351 0 3 0 2911 30 0 0 25 0 1 0 1785856861 14082048 3099 4294967295 134512640 135167914 3221224448 3221223204 134697070 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 3438 3099 162 162 0 3276 0
[pid=16472] vsize: 13752
Current children cumulated CPU time (s) 29.42
Current children cumulated vsize (Kb) 15880

[startup+40.0068 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 5351 0 3 0 3911 30 0 0 25 0 1 0 1785856861 14082048 3099 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 3438 3099 162 162 0 3276 0
[pid=16472] vsize: 13752
Current children cumulated CPU time (s) 39.42
Current children cumulated vsize (Kb) 15880

[startup+50.0075 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 5351 0 3 0 4911 30 0 0 25 0 1 0 1785856861 14082048 3099 4294967295 134512640 135167914 3221224448 3221223204 134697189 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 3438 3099 162 162 0 3276 0
[pid=16472] vsize: 13752
Current children cumulated CPU time (s) 49.42
Current children cumulated vsize (Kb) 15880

[startup+60.0082 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 5351 0 3 0 5912 30 0 0 25 0 1 0 1785856861 14082048 3099 4294967295 134512640 135167914 3221224448 3221223216 134691415 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 3438 3099 162 162 0 3276 0
[pid=16472] vsize: 13752
Current children cumulated CPU time (s) 59.43
Current children cumulated vsize (Kb) 15880

[startup+70.0089 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 8241 0 3 0 6889 42 0 0 25 0 1 0 1785856861 24424448 5625 4294967295 134512640 135167914 3221224448 3220151664 134845911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 5963 5625 162 162 0 5801 0
[pid=16472] vsize: 23852
Current children cumulated CPU time (s) 69.32
Current children cumulated vsize (Kb) 25980

[startup+80.0096 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 12630 0 3 0 7857 58 0 0 25 0 1 0 1785856861 38350848 9025 4294967295 134512640 135167914 3221224448 3220152108 134844675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 9363 9025 162 162 0 9201 0
[pid=16472] vsize: 37452
Current children cumulated CPU time (s) 79.16
Current children cumulated vsize (Kb) 39580

[startup+90.0103 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 14474 0 3 0 8837 66 0 0 25 0 1 0 1785856861 45903872 10869 4294967295 134512640 135167914 3221224448 3220150656 134695191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 11207 10869 162 162 0 11045 0
[pid=16472] vsize: 44828
Current children cumulated CPU time (s) 89.04
Current children cumulated vsize (Kb) 46956

[startup+100.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 16057 0 3 0 9820 73 0 0 25 0 1 0 1785856861 52387840 12452 4294967295 134512640 135167914 3221224448 3220152412 134722231 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 12790 12452 162 162 0 12628 0
[pid=16472] vsize: 51160
Current children cumulated CPU time (s) 98.94
Current children cumulated vsize (Kb) 53288

[startup+110.011 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 19905 0 3 0 10800 87 0 0 25 0 1 0 1785856861 62750720 14982 4294967295 134512640 135167914 3221224448 3220157308 134694368 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 15320 14982 162 162 0 15158 0
[pid=16472] vsize: 61280
Current children cumulated CPU time (s) 108.88
Current children cumulated vsize (Kb) 63408

[startup+120.011 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 21225 0 3 0 11785 93 0 0 25 0 1 0 1785856861 68157440 16302 4294967295 134512640 135167914 3221224448 3220153728 134844637 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 16640 16302 162 162 0 16478 0
[pid=16472] vsize: 66560
Current children cumulated CPU time (s) 118.79
Current children cumulated vsize (Kb) 68688

[startup+130.012 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 22310 0 3 0 12771 98 0 0 25 0 1 0 1785856861 72601600 17387 4294967295 134512640 135167914 3221224448 3220153072 134849153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 17725 17387 162 162 0 17563 0
[pid=16472] vsize: 70900
Current children cumulated CPU time (s) 128.7
Current children cumulated vsize (Kb) 73028

[startup+140.013 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 23313 0 3 0 13759 103 0 0 25 0 1 0 1785856861 76709888 18390 4294967295 134512640 135167914 3221224448 3220155600 134623970 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 18728 18390 162 162 0 18566 0
[pid=16472] vsize: 74912
Current children cumulated CPU time (s) 138.63
Current children cumulated vsize (Kb) 77040

[startup+150.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 24376 0 3 0 14745 109 0 0 25 0 1 0 1785856861 81063936 19453 4294967295 134512640 135167914 3221224448 3220150272 134694528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 19791 19453 162 162 0 19629 0
[pid=16472] vsize: 79164
Current children cumulated CPU time (s) 148.55
Current children cumulated vsize (Kb) 81292

[startup+160.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 25284 0 3 0 15735 113 0 0 25 0 1 0 1785856861 84783104 20361 4294967295 134512640 135167914 3221224448 3220150400 134849110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 20699 20361 162 162 0 20537 0
[pid=16472] vsize: 82796
Current children cumulated CPU time (s) 158.49
Current children cumulated vsize (Kb) 84924

[startup+170.015 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 26156 0 3 0 16723 118 0 0 25 0 1 0 1785856861 88354816 21233 4294967295 134512640 135167914 3221224448 3220160608 134847370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 21571 21233 162 162 0 21409 0
[pid=16472] vsize: 86284
Current children cumulated CPU time (s) 168.42
Current children cumulated vsize (Kb) 88412

[startup+180.016 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 32126 0 3 0 17701 135 0 0 25 0 1 0 1785856861 102006784 24566 4294967295 134512640 135167914 3221224448 3220156912 134845927 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 24904 24566 162 162 0 24742 0
[pid=16472] vsize: 99616
Current children cumulated CPU time (s) 178.37
Current children cumulated vsize (Kb) 101744

[startup+190.016 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 33096 0 3 0 18689 140 0 0 25 0 1 0 1785856861 105979904 25536 4294967295 134512640 135167914 3221224448 3220157280 134844703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 25874 25536 162 162 0 25712 0
[pid=16472] vsize: 103496
Current children cumulated CPU time (s) 188.3
Current children cumulated vsize (Kb) 105624

[startup+200.016 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 33925 0 3 0 19678 145 0 0 25 0 1 0 1785856861 109375488 26365 4294967295 134512640 135167914 3221224448 3220162492 134722225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 26703 26365 162 162 0 26541 0
[pid=16472] vsize: 106812
Current children cumulated CPU time (s) 198.24
Current children cumulated vsize (Kb) 108940

[startup+210.017 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 34670 0 3 0 20669 148 0 0 25 0 1 0 1785856861 112431104 27110 4294967295 134512640 135167914 3221224448 3220159596 134722656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 27449 27110 162 162 0 27287 0
[pid=16472] vsize: 109796
Current children cumulated CPU time (s) 208.18
Current children cumulated vsize (Kb) 111924

[startup+220.017 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 35474 0 3 0 21658 153 0 0 25 0 1 0 1785856861 115724288 27914 4294967295 134512640 135167914 3221224448 3220166772 134849086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 28253 27914 162 162 0 28091 0
[pid=16472] vsize: 113012
Current children cumulated CPU time (s) 218.12
Current children cumulated vsize (Kb) 115140

[startup+230.018 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 36236 0 3 0 22648 157 0 0 25 0 1 0 1785856861 118841344 28676 4294967295 134512640 135167914 3221224448 3220164512 134849196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 29014 28676 162 162 0 28852 0
[pid=16472] vsize: 116056
Current children cumulated CPU time (s) 228.06
Current children cumulated vsize (Kb) 118184

[startup+240.019 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 37132 0 3 0 23635 163 0 0 25 0 1 0 1785856861 122511360 29572 4294967295 134512640 135167914 3221224448 3220154704 134623813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 29910 29572 162 162 0 29748 0
[pid=16472] vsize: 119640
Current children cumulated CPU time (s) 237.99
Current children cumulated vsize (Kb) 121768

[startup+250.019 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 37834 0 3 0 24626 167 0 0 25 0 1 0 1785856861 125386752 30274 4294967295 134512640 135167914 3221224448 3220150624 134694392 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 30612 30274 162 162 0 30450 0
[pid=16472] vsize: 122448
Current children cumulated CPU time (s) 247.94
Current children cumulated vsize (Kb) 124576

[startup+260.019 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 38581 0 3 0 25615 173 0 0 25 0 1 0 1785856861 128466944 31021 4294967295 134512640 135167914 3221224448 3220153792 134844689 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 31364 31021 162 162 0 31202 0
[pid=16472] vsize: 125456
Current children cumulated CPU time (s) 257.89
Current children cumulated vsize (Kb) 127584

[startup+270.019 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 39322 0 3 0 26607 177 0 0 25 0 1 0 1785856861 131497984 31762 4294967295 134512640 135167914 3221224448 3220158960 134624420 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 32104 31762 162 162 0 31942 0
[pid=16472] vsize: 128416
Current children cumulated CPU time (s) 267.85
Current children cumulated vsize (Kb) 130544

[startup+280.02 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 40115 0 3 0 27595 182 0 0 25 0 1 0 1785856861 134746112 32555 4294967295 134512640 135167914 3221224448 3220163216 134623803 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 32897 32555 162 162 0 32735 0
[pid=16472] vsize: 131588
Current children cumulated CPU time (s) 277.78
Current children cumulated vsize (Kb) 133716

[startup+290.02 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 40969 0 3 0 28586 186 0 0 25 0 1 0 1785856861 138244096 33409 4294967295 134512640 135167914 3221224448 3220160048 134849110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 33751 33409 162 162 0 33589 0
[pid=16472] vsize: 135004
Current children cumulated CPU time (s) 287.73
Current children cumulated vsize (Kb) 137132

[startup+300.02 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 41910 0 3 0 29573 191 0 0 25 0 1 0 1785856861 142094336 34350 4294967295 134512640 135167914 3221224448 3220155152 134624526 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 34691 34350 162 162 0 34529 0
[pid=16472] vsize: 138764
Current children cumulated CPU time (s) 297.65
Current children cumulated vsize (Kb) 140892

[startup+310.021 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 42531 0 3 0 30565 195 0 0 25 0 1 0 1785856861 144637952 34971 4294967295 134512640 135167914 3221224448 3220154176 134844706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 35312 34971 162 162 0 35150 0
[pid=16472] vsize: 141248
Current children cumulated CPU time (s) 307.61
Current children cumulated vsize (Kb) 143376

[startup+320.021 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 43084 0 3 0 31557 199 0 0 25 0 1 0 1785856861 146903040 35524 4294967295 134512640 135167914 3221224448 3220151264 134722521 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 35865 35524 162 162 0 35703 0
[pid=16472] vsize: 143460
Current children cumulated CPU time (s) 317.57
Current children cumulated vsize (Kb) 145588

[startup+330.023 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 43660 0 3 0 32549 201 0 0 25 0 1 0 1785856861 149258240 36100 4294967295 134512640 135167914 3221224448 3220156672 134722603 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 36440 36100 162 162 0 36278 0
[pid=16472] vsize: 145760
Current children cumulated CPU time (s) 327.51
Current children cumulated vsize (Kb) 147888

[startup+340.024 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 44244 0 3 0 33540 205 0 0 25 0 1 0 1785856861 151646208 36684 4294967295 134512640 135167914 3221224448 3220158832 134845901 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 37023 36684 162 162 0 36861 0
[pid=16472] vsize: 148092
Current children cumulated CPU time (s) 337.46
Current children cumulated vsize (Kb) 150220

[startup+350.024 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 44944 0 3 0 34530 210 0 0 25 0 1 0 1785856861 154509312 37384 4294967295 134512640 135167914 3221224448 3220168992 134694377 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 37722 37384 162 162 0 37560 0
[pid=16472] vsize: 150888
Current children cumulated CPU time (s) 347.41
Current children cumulated vsize (Kb) 153016

[startup+360.024 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 45570 0 3 0 35520 215 0 0 25 0 1 0 1785856861 157073408 38010 4294967295 134512640 135167914 3221224448 3220165504 134844703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 38348 38010 162 162 0 38186 0
[pid=16472] vsize: 153392
Current children cumulated CPU time (s) 357.36
Current children cumulated vsize (Kb) 155520

[startup+370.025 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 46213 0 3 0 36510 219 0 0 25 0 1 0 1785856861 159707136 38653 4294967295 134512640 135167914 3221224448 3220168128 134624005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 38991 38653 162 162 0 38829 0
[pid=16472] vsize: 155964
Current children cumulated CPU time (s) 367.3
Current children cumulated vsize (Kb) 158092

[startup+380.026 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 46885 0 3 0 37503 221 0 0 25 0 1 0 1785856861 162500608 39325 4294967295 134512640 135167914 3221224448 3220154592 134844725 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 39673 39325 162 162 0 39511 0
[pid=16472] vsize: 158692
Current children cumulated CPU time (s) 377.25
Current children cumulated vsize (Kb) 160820

[startup+390.026 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 47628 0 3 0 38494 223 0 0 25 0 1 0 1785856861 165543936 40068 4294967295 134512640 135167914 3221224448 3220168704 134843068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 40416 40068 162 162 0 40254 0
[pid=16472] vsize: 161664
Current children cumulated CPU time (s) 387.18
Current children cumulated vsize (Kb) 163792

[startup+400.027 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 58575 0 3 0 39466 249 0 0 25 0 1 0 1785856861 210374656 51015 4294967295 134512640 135167914 3221224448 3220150736 134625468 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 51361 51015 162 162 0 51199 0
[pid=16472] vsize: 205444
Current children cumulated CPU time (s) 397.16
Current children cumulated vsize (Kb) 207572

[startup+410.028 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 58988 0 3 0 40460 252 0 0 25 0 1 0 1785856861 190464000 46155 4294967295 134512640 135167914 3221224448 3220166528 134843139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 46500 46155 162 162 0 46338 0
[pid=16472] vsize: 186000
Current children cumulated CPU time (s) 407.13
Current children cumulated vsize (Kb) 188128

[startup+420.027 s]
Raw data (loadavg): 1.00 0.99 0.93 1/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) T 16467 16467 6872 0 -1 0 59492 0 3 0 41453 254 0 0 25 0 1 0 1785856861 192528384 46659 4294967295 134512640 135167914 3221224448 3220158876 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/16472/statm): 47004 46659 162 162 0 46842 0
[pid=16472] vsize: 188016
Current children cumulated CPU time (s) 417.08
Current children cumulated vsize (Kb) 190144

[startup+430.029 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 60024 0 3 0 42446 257 0 0 25 0 1 0 1785856861 194703360 47191 4294967295 134512640 135167914 3221224448 3220151964 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 47535 47191 162 162 0 47373 0
[pid=16472] vsize: 190140
Current children cumulated CPU time (s) 427.04
Current children cumulated vsize (Kb) 192268

[startup+440.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 60568 0 3 0 43440 260 0 0 25 0 1 0 1785856861 196927488 47735 4294967295 134512640 135167914 3221224448 3220157632 134695554 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 48078 47735 162 162 0 47916 0
[pid=16472] vsize: 192312
Current children cumulated CPU time (s) 437.01
Current children cumulated vsize (Kb) 194440

[startup+450.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 61071 0 3 0 44433 263 0 0 25 0 1 0 1785856861 198987776 48238 4294967295 134512640 135167914 3221224448 3220166296 134722513 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 48581 48238 162 162 0 48419 0
[pid=16472] vsize: 194324
Current children cumulated CPU time (s) 446.97
Current children cumulated vsize (Kb) 196452

[startup+460.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 61636 0 3 0 45426 267 0 0 25 0 1 0 1785856861 201297920 48803 4294967295 134512640 135167914 3221224448 3220162816 134844676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 49145 48803 162 162 0 48983 0
[pid=16472] vsize: 196580
Current children cumulated CPU time (s) 456.94
Current children cumulated vsize (Kb) 198708

[startup+470.031 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 62176 0 3 0 46419 270 0 0 25 0 1 0 1785856861 203505664 49343 4294967295 134512640 135167914 3221224448 3220156428 134845882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 49684 49343 162 162 0 49522 0
[pid=16472] vsize: 198736
Current children cumulated CPU time (s) 466.9
Current children cumulated vsize (Kb) 200864

[startup+480.032 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 62702 0 3 0 47412 273 0 0 25 0 1 0 1785856861 205660160 49869 4294967295 134512640 135167914 3221224448 3220158064 134624577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 50210 49869 162 162 0 50048 0
[pid=16472] vsize: 200840
Current children cumulated CPU time (s) 476.86
Current children cumulated vsize (Kb) 202968

[startup+490.032 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 63254 0 3 0 48403 277 0 0 25 0 1 0 1785856861 207921152 50421 4294967295 134512640 135167914 3221224448 3220173568 134844728 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 50762 50421 162 162 0 50600 0
[pid=16472] vsize: 203048
Current children cumulated CPU time (s) 486.81
Current children cumulated vsize (Kb) 205176

[startup+500.033 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 63845 0 3 0 49395 280 0 0 25 0 1 0 1785856861 210341888 51012 4294967295 134512640 135167914 3221224448 3220175296 134623781 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 51353 51012 162 162 0 51191 0
[pid=16472] vsize: 205412
Current children cumulated CPU time (s) 496.76
Current children cumulated vsize (Kb) 207540

[startup+510.034 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 64444 0 3 0 50388 284 0 0 25 0 1 0 1785856861 212791296 51611 4294967295 134512640 135167914 3221224448 3220164880 134843118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 51951 51611 162 162 0 51789 0
[pid=16472] vsize: 207804
Current children cumulated CPU time (s) 506.73
Current children cumulated vsize (Kb) 209932

[startup+520.033 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 64902 0 3 0 51381 286 0 0 25 0 1 0 1785856861 214659072 52069 4294967295 134512640 135167914 3221224448 3220170160 134623813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 52407 52069 162 162 0 52245 0
[pid=16472] vsize: 209628
Current children cumulated CPU time (s) 516.68
Current children cumulated vsize (Kb) 211756

[startup+530.034 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 65379 0 3 0 52374 289 0 0 25 0 1 0 1785856861 216702976 52546 4294967295 134512640 135167914 3221224448 3220163836 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 52906 52546 162 162 0 52744 0
[pid=16472] vsize: 211624
Current children cumulated CPU time (s) 526.64
Current children cumulated vsize (Kb) 213752

[startup+540.035 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 65837 0 3 0 53369 291 0 0 25 0 1 0 1785856861 218578944 53004 4294967295 134512640 135167914 3221224448 3220177056 134843113 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 53364 53004 162 162 0 53202 0
[pid=16472] vsize: 213456
Current children cumulated CPU time (s) 536.61
Current children cumulated vsize (Kb) 215584

[startup+550.036 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 66323 0 3 0 54364 294 0 0 25 0 1 0 1785856861 220565504 53490 4294967295 134512640 135167914 3221224448 3220170108 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 53849 53490 162 162 0 53687 0
[pid=16472] vsize: 215396
Current children cumulated CPU time (s) 546.59
Current children cumulated vsize (Kb) 217524

[startup+560.036 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 66776 0 3 0 55358 296 0 0 25 0 1 0 1785856861 222420992 53943 4294967295 134512640 135167914 3221224448 3220172064 134844694 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 54302 53943 162 162 0 54140 0
[pid=16472] vsize: 217208
Current children cumulated CPU time (s) 556.55
Current children cumulated vsize (Kb) 219336

[startup+570.037 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 67265 0 3 0 56350 299 0 0 25 0 1 0 1785856861 224419840 54432 4294967295 134512640 135167914 3221224448 3220168572 134693585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 54790 54432 162 162 0 54628 0
[pid=16472] vsize: 219160
Current children cumulated CPU time (s) 566.5
Current children cumulated vsize (Kb) 221288

[startup+580.038 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 67783 0 3 0 57341 302 0 0 25 0 1 0 1785856861 226537472 54950 4294967295 134512640 135167914 3221224448 3220150836 134843117 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 55307 54950 162 162 0 55145 0
[pid=16472] vsize: 221228
Current children cumulated CPU time (s) 576.44
Current children cumulated vsize (Kb) 223356

[startup+590.038 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 68234 0 3 0 58335 306 0 0 25 0 1 0 1785856861 228380672 55401 4294967295 134512640 135167914 3221224448 3220158240 134694419 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 55757 55401 162 162 0 55595 0
[pid=16472] vsize: 223028
Current children cumulated CPU time (s) 586.42
Current children cumulated vsize (Kb) 225156

[startup+600.039 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 68703 0 3 0 59328 309 0 0 25 0 1 0 1785856861 230301696 55870 4294967295 134512640 135167914 3221224448 3220159808 134694392 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 56226 55870 162 162 0 56064 0
[pid=16472] vsize: 224904
Current children cumulated CPU time (s) 596.38
Current children cumulated vsize (Kb) 227032

[startup+610.04 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 69169 0 3 0 60320 312 0 0 25 0 1 0 1785856861 232210432 56336 4294967295 134512640 135167914 3221224448 3220174560 134844647 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 56692 56336 162 162 0 56530 0
[pid=16472] vsize: 226768
Current children cumulated CPU time (s) 606.33
Current children cumulated vsize (Kb) 228896

[startup+620.039 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 69702 0 3 0 61313 314 0 0 25 0 1 0 1785856861 234389504 56869 4294967295 134512640 135167914 3221224448 3220161920 134844720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 57224 56869 162 162 0 57062 0
[pid=16472] vsize: 228896
Current children cumulated CPU time (s) 616.28
Current children cumulated vsize (Kb) 231024

[startup+630.04 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 70303 0 3 0 62306 318 0 0 25 0 1 0 1785856861 236847104 57470 4294967295 134512640 135167914 3221224448 3220164640 134847370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 57824 57470 162 162 0 57662 0
[pid=16472] vsize: 231296
Current children cumulated CPU time (s) 626.25
Current children cumulated vsize (Kb) 233424

[startup+640.041 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 70739 0 3 0 63301 319 0 0 25 0 1 0 1785856861 238628864 57906 4294967295 134512640 135167914 3221224448 3220174556 134843033 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 58259 57906 162 162 0 58097 0
[pid=16472] vsize: 233036
Current children cumulated CPU time (s) 636.21
Current children cumulated vsize (Kb) 235164

[startup+650.041 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 71168 0 3 0 64295 322 0 0 25 0 1 0 1785856861 240381952 58335 4294967295 134512640 135167914 3221224448 3220157792 134694444 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 58687 58335 162 162 0 58525 0
[pid=16472] vsize: 234748
Current children cumulated CPU time (s) 646.18
Current children cumulated vsize (Kb) 236876

[startup+660.041 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 71604 0 3 0 65288 325 0 0 25 0 1 0 1785856861 242163712 58771 4294967295 134512640 135167914 3221224448 3220156320 134844703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 59122 58771 162 162 0 58960 0
[pid=16472] vsize: 236488
Current children cumulated CPU time (s) 656.14
Current children cumulated vsize (Kb) 238616

[startup+670.042 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 71996 0 3 0 66282 327 0 0 25 0 1 0 1785856861 243769344 59163 4294967295 134512640 135167914 3221224448 3220156720 134623813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 59514 59163 162 162 0 59352 0
[pid=16472] vsize: 238056
Current children cumulated CPU time (s) 666.1
Current children cumulated vsize (Kb) 240184

[startup+680.043 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 72395 0 3 0 67277 329 0 0 25 0 1 0 1785856861 245403648 59562 4294967295 134512640 135167914 3221224448 3220169152 134843153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 59913 59562 162 162 0 59751 0
[pid=16472] vsize: 239652
Current children cumulated CPU time (s) 676.07
Current children cumulated vsize (Kb) 241780

[startup+690.043 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 72834 0 3 0 68271 332 0 0 25 0 1 0 1785856861 247201792 60001 4294967295 134512640 135167914 3221224448 3220170988 134845876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 60352 60001 162 162 0 60190 0
[pid=16472] vsize: 241408
Current children cumulated CPU time (s) 686.04
Current children cumulated vsize (Kb) 243536

[startup+700.044 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 73229 0 3 0 69266 334 0 0 25 0 1 0 1785856861 248815616 60396 4294967295 134512640 135167914 3221224448 3220159520 134845913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 60746 60396 162 162 0 60584 0
[pid=16472] vsize: 242984
Current children cumulated CPU time (s) 696.01
Current children cumulated vsize (Kb) 245112

[startup+710.045 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 73612 0 3 0 70260 337 0 0 23 0 1 0 1785856861 250384384 60779 4294967295 134512640 135167914 3221224448 3220176320 134843010 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 61129 60779 162 162 0 60967 0
[pid=16472] vsize: 244516
Current children cumulated CPU time (s) 705.98
Current children cumulated vsize (Kb) 246644

[startup+720.044 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 74026 0 3 0 71254 340 0 0 25 0 1 0 1785856861 252080128 61193 4294967295 134512640 135167914 3221224448 3220169884 134722512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 61543 61193 162 162 0 61381 0
[pid=16472] vsize: 246172
Current children cumulated CPU time (s) 715.95
Current children cumulated vsize (Kb) 248300

[startup+730.045 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 74456 0 3 0 72248 342 0 0 25 0 1 0 1785856861 253837312 61623 4294967295 134512640 135167914 3221224448 3220159804 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 61972 61623 162 162 0 61810 0
[pid=16472] vsize: 247888
Current children cumulated CPU time (s) 725.91
Current children cumulated vsize (Kb) 250016

[startup+740.046 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 74833 0 3 0 73243 344 0 0 25 0 1 0 1785856861 255381504 62000 4294967295 134512640 135167914 3221224448 3220154128 134845927 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 62349 62000 162 162 0 62187 0
[pid=16472] vsize: 249396
Current children cumulated CPU time (s) 735.88
Current children cumulated vsize (Kb) 251524

[startup+750.046 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 75214 0 3 0 74238 346 0 0 25 0 1 0 1785856861 256942080 62381 4294967295 134512640 135167914 3221224448 3220174512 134843123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 62730 62381 162 162 0 62568 0
[pid=16472] vsize: 250920
Current children cumulated CPU time (s) 745.85
Current children cumulated vsize (Kb) 253048

[startup+760.046 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 75621 0 3 0 75234 348 0 0 25 0 1 0 1785856861 258609152 62788 4294967295 134512640 135167914 3221224448 3220173472 134694439 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 63137 62788 162 162 0 62975 0
[pid=16472] vsize: 252548
Current children cumulated CPU time (s) 755.83
Current children cumulated vsize (Kb) 254676

[startup+770.047 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 76017 0 3 0 76228 349 0 0 25 0 1 0 1785856861 260231168 63184 4294967295 134512640 135167914 3221224448 3220174368 134843026 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 63533 63184 162 162 0 63371 0
[pid=16472] vsize: 254132
Current children cumulated CPU time (s) 765.78
Current children cumulated vsize (Kb) 256260

[startup+780.048 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 76527 0 3 0 77220 352 0 0 25 0 1 0 1785856861 262320128 63694 4294967295 134512640 135167914 3221224448 3220163552 134845927 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 64043 63694 162 162 0 63881 0
[pid=16472] vsize: 256172
Current children cumulated CPU time (s) 775.73
Current children cumulated vsize (Kb) 258300

[startup+790.048 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 76967 0 3 0 78215 355 0 0 25 0 1 0 1785856861 264114176 64134 4294967295 134512640 135167914 3221224448 3220160044 134843002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 64481 64134 162 162 0 64319 0
[pid=16472] vsize: 257924
Current children cumulated CPU time (s) 785.71
Current children cumulated vsize (Kb) 260052

[startup+800.049 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 77354 0 3 0 79207 357 0 0 25 0 1 0 1785856861 265699328 64521 4294967295 134512640 135167914 3221224448 3220163552 134843010 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 64868 64521 162 162 0 64706 0
[pid=16472] vsize: 259472
Current children cumulated CPU time (s) 795.65
Current children cumulated vsize (Kb) 261600

[startup+810.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 77744 0 3 0 80202 360 0 0 25 0 1 0 1785856861 267292672 64911 4294967295 134512640 135167914 3221224448 3220172960 134843406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 65257 64911 162 162 0 65095 0
[pid=16472] vsize: 261028
Current children cumulated CPU time (s) 805.63
Current children cumulated vsize (Kb) 263156

[startup+820.049 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 78150 0 3 0 81196 362 0 0 25 0 1 0 1785856861 268951552 65317 4294967295 134512640 135167914 3221224448 3220155552 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 65662 65317 162 162 0 65500 0
[pid=16472] vsize: 262648
Current children cumulated CPU time (s) 815.59
Current children cumulated vsize (Kb) 264776

[startup+830.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 78528 0 3 0 82189 365 0 0 25 0 1 0 1785856861 270495744 65695 4294967295 134512640 135167914 3221224448 3220164992 134845921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 66039 65695 162 162 0 65877 0
[pid=16472] vsize: 264156
Current children cumulated CPU time (s) 825.55
Current children cumulated vsize (Kb) 266284

[startup+840.051 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 78905 0 3 0 83183 368 0 0 25 0 1 0 1785856861 272039936 66072 4294967295 134512640 135167914 3221224448 3220162512 134849122 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 66416 66072 162 162 0 66254 0
[pid=16472] vsize: 265664
Current children cumulated CPU time (s) 835.52
Current children cumulated vsize (Kb) 267792

[startup+850.052 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 79273 0 3 0 84177 370 0 0 25 0 1 0 1785856861 273547264 66440 4294967295 134512640 135167914 3221224448 3220165232 134623813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 66784 66440 162 162 0 66622 0
[pid=16472] vsize: 267136
Current children cumulated CPU time (s) 845.48
Current children cumulated vsize (Kb) 269264

[startup+860.052 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 79643 0 3 0 85171 373 0 0 25 0 1 0 1785856861 275062784 66810 4294967295 134512640 135167914 3221224448 3220182648 134845877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 67154 66810 162 162 0 66992 0
[pid=16472] vsize: 268616
Current children cumulated CPU time (s) 855.45
Current children cumulated vsize (Kb) 270744

[startup+870.053 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 80006 0 3 0 86165 376 0 0 25 0 1 0 1785856861 276549632 67173 4294967295 134512640 135167914 3221224448 3220160480 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 67517 67173 162 162 0 67355 0
[pid=16472] vsize: 270068
Current children cumulated CPU time (s) 865.42
Current children cumulated vsize (Kb) 272196

[startup+880.054 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 80363 0 3 0 87160 378 0 0 25 0 1 0 1785856861 278011904 67530 4294967295 134512640 135167914 3221224448 3220176400 134849187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 67874 67530 162 162 0 67712 0
[pid=16472] vsize: 271496
Current children cumulated CPU time (s) 875.39
Current children cumulated vsize (Kb) 273624

[startup+890.054 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 80703 0 3 0 88154 381 0 0 25 0 1 0 1785856861 279404544 67870 4294967295 134512640 135167914 3221224448 3220165544 134844674 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 68214 67870 162 162 0 68052 0
[pid=16472] vsize: 272856
Current children cumulated CPU time (s) 885.36
Current children cumulated vsize (Kb) 274984

[startup+900.055 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 81101 0 3 0 89149 383 0 0 25 0 1 0 1785856861 281026560 68268 4294967295 134512640 135167914 3221224448 3220160032 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 68610 68268 162 162 0 68448 0
[pid=16472] vsize: 274440
Current children cumulated CPU time (s) 895.33
Current children cumulated vsize (Kb) 276568

[startup+910.056 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 81466 0 3 0 90143 386 0 0 25 0 1 0 1785856861 282521600 68633 4294967295 134512640 135167914 3221224448 3220176880 134623813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 68975 68633 162 162 0 68813 0
[pid=16472] vsize: 275900
Current children cumulated CPU time (s) 905.3
Current children cumulated vsize (Kb) 278028

[startup+920.057 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 81832 0 3 0 91138 387 0 0 25 0 1 0 1785856861 284020736 68999 4294967295 134512640 135167914 3221224448 3220175708 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 69341 68999 162 162 0 69179 0
[pid=16472] vsize: 277364
Current children cumulated CPU time (s) 915.26
Current children cumulated vsize (Kb) 279492

[startup+930.058 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 82187 0 3 0 92132 390 0 0 25 0 1 0 1785856861 285474816 69354 4294967295 134512640 135167914 3221224448 3220155152 134624640 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 69696 69354 162 162 0 69534 0
[pid=16472] vsize: 278784
Current children cumulated CPU time (s) 925.23
Current children cumulated vsize (Kb) 280912

[startup+940.059 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 82555 0 3 0 93126 393 0 0 25 0 1 0 1785856861 286978048 69722 4294967295 134512640 135167914 3221224448 3220167196 134722208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 70063 69722 162 162 0 69901 0
[pid=16472] vsize: 280252
Current children cumulated CPU time (s) 935.2
Current children cumulated vsize (Kb) 282380

[startup+950.059 s]
Raw data (loadavg): 1.00 0.99 0.93 1/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) T 16467 16467 6872 0 -1 0 82926 0 3 0 94121 395 0 0 25 0 1 0 1785856861 288497664 70093 4294967295 134512640 135167914 3221224448 3220157724 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/16472/statm): 70434 70093 162 162 0 70272 0
[pid=16472] vsize: 281736
Current children cumulated CPU time (s) 945.17
Current children cumulated vsize (Kb) 283864

[startup+960.059 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 83427 0 3 0 95114 398 0 0 25 0 1 0 1785856861 290545664 70594 4294967295 134512640 135167914 3221224448 3220171636 134843031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 70934 70594 162 162 0 70772 0
[pid=16472] vsize: 283736
Current children cumulated CPU time (s) 955.13
Current children cumulated vsize (Kb) 285864

[startup+970.06 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 83857 0 3 0 96109 400 0 0 25 0 1 0 1785856861 292302848 71024 4294967295 134512640 135167914 3221224448 3220169584 134845927 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 71363 71024 162 162 0 71201 0
[pid=16472] vsize: 285452
Current children cumulated CPU time (s) 965.1
Current children cumulated vsize (Kb) 287580

[startup+980.061 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 84248 0 3 0 97105 402 0 0 25 0 1 0 1785856861 293900288 71415 4294967295 134512640 135167914 3221224448 3220158684 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 71753 71415 162 162 0 71591 0
[pid=16472] vsize: 287012
Current children cumulated CPU time (s) 975.08
Current children cumulated vsize (Kb) 289140

[startup+990.061 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 84618 0 3 0 98099 405 0 0 25 0 1 0 1785856861 295415808 71785 4294967295 134512640 135167914 3221224448 3220177056 134694392 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 72123 71785 162 162 0 71961 0
[pid=16472] vsize: 288492
Current children cumulated CPU time (s) 985.05
Current children cumulated vsize (Kb) 290620

[startup+1000.06 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 84976 0 3 0 99094 406 0 0 25 0 1 0 1785856861 296882176 72143 4294967295 134512640 135167914 3221224448 3220172576 134694392 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 72481 72143 162 162 0 72319 0
[pid=16472] vsize: 289924
Current children cumulated CPU time (s) 995.01
Current children cumulated vsize (Kb) 292052

[startup+1010.06 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 85356 0 3 0 100089 408 0 0 25 0 1 0 1785856861 298631168 72523 4294967295 134512640 135167914 3221224448 3220158848 134843153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 72908 72523 162 162 0 72746 0
[pid=16472] vsize: 291632
Current children cumulated CPU time (s) 1004.98
Current children cumulated vsize (Kb) 293760

[startup+1020.06 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 85686 0 3 0 101085 410 0 0 25 0 1 0 1785856861 299982848 72853 4294967295 134512640 135167914 3221224448 3220162208 134844736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 73238 72853 162 162 0 73076 0
[pid=16472] vsize: 292952
Current children cumulated CPU time (s) 1014.96
Current children cumulated vsize (Kb) 295080

[startup+1030.06 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 86020 0 3 0 102081 411 0 0 25 0 1 0 1785856861 301350912 73187 4294967295 134512640 135167914 3221224448 3220166128 134623803 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 73572 73187 162 162 0 73410 0
[pid=16472] vsize: 294288
Current children cumulated CPU time (s) 1024.93
Current children cumulated vsize (Kb) 296416

[startup+1040.06 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 86346 0 3 0 103076 413 0 0 25 0 1 0 1785856861 302682112 73513 4294967295 134512640 135167914 3221224448 3220166400 134844723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 73897 73513 162 162 0 73735 0
[pid=16472] vsize: 295588
Current children cumulated CPU time (s) 1034.9
Current children cumulated vsize (Kb) 297716

[startup+1050.07 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 86723 0 3 0 104069 416 0 0 25 0 1 0 1785856861 304222208 73890 4294967295 134512640 135167914 3221224448 3220172816 134849179 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 74273 73890 162 162 0 74111 0
[pid=16472] vsize: 297092
Current children cumulated CPU time (s) 1044.86
Current children cumulated vsize (Kb) 299220

[startup+1060.07 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 87064 0 3 0 105064 419 0 0 25 0 1 0 1785856861 305618944 74231 4294967295 134512640 135167914 3221224448 3220161184 134624169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 74614 74231 162 162 0 74452 0
[pid=16472] vsize: 298456
Current children cumulated CPU time (s) 1054.84
Current children cumulated vsize (Kb) 300584

[startup+1070.07 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 87394 0 3 0 106059 422 0 0 25 0 1 0 1785856861 306970624 74561 4294967295 134512640 135167914 3221224448 3220164512 134849148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 74944 74561 162 162 0 74782 0
[pid=16472] vsize: 299776
Current children cumulated CPU time (s) 1064.82
Current children cumulated vsize (Kb) 301904

[startup+1080.07 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 87707 0 3 0 107052 425 0 0 25 0 1 0 1785856861 308252672 74874 4294967295 134512640 135167914 3221224448 3220166040 134843032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 75257 74874 162 162 0 75095 0
[pid=16472] vsize: 301028
Current children cumulated CPU time (s) 1074.78
Current children cumulated vsize (Kb) 303156

[startup+1090.07 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 88057 0 3 0 108047 427 0 0 25 0 1 0 1785856861 309686272 75224 4294967295 134512640 135167914 3221224448 3220167200 134694410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 75607 75224 162 162 0 75445 0
[pid=16472] vsize: 302428
Current children cumulated CPU time (s) 1084.75
Current children cumulated vsize (Kb) 304556

[startup+1100.07 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 88390 0 3 0 109043 429 0 0 25 0 1 0 1785856861 311050240 75557 4294967295 134512640 135167914 3221224448 3220165408 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 75940 75557 162 162 0 75778 0
[pid=16472] vsize: 303760
Current children cumulated CPU time (s) 1094.73
Current children cumulated vsize (Kb) 305888

[startup+1110.07 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 88778 0 3 0 110036 431 0 0 25 0 1 0 1785856861 312635392 75945 4294967295 134512640 135167914 3221224448 3220157344 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 76327 75945 162 162 0 76165 0
[pid=16472] vsize: 305308
Current children cumulated CPU time (s) 1104.68
Current children cumulated vsize (Kb) 307436

[startup+1120.07 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 89121 0 3 0 111031 433 0 0 25 0 1 0 1785856861 314040320 76288 4294967295 134512640 135167914 3221224448 3220169228 134722660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 76670 76288 162 162 0 76508 0
[pid=16472] vsize: 306680
Current children cumulated CPU time (s) 1114.65
Current children cumulated vsize (Kb) 308808

[startup+1130.07 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 89452 0 3 0 112025 435 0 0 25 0 1 0 1785856861 315396096 76619 4294967295 134512640 135167914 3221224448 3220153344 134624169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 77001 76619 162 162 0 76839 0
[pid=16472] vsize: 308004
Current children cumulated CPU time (s) 1124.61
Current children cumulated vsize (Kb) 310132

[startup+1140.07 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 89788 0 3 0 113020 439 0 0 25 0 1 0 1785856861 316772352 76955 4294967295 134512640 135167914 3221224448 3220173052 134849056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 77337 76955 162 162 0 77175 0
[pid=16472] vsize: 309348
Current children cumulated CPU time (s) 1134.6
Current children cumulated vsize (Kb) 311476

[startup+1150.07 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 90121 0 3 0 114014 441 0 0 25 0 1 0 1785856861 318136320 77288 4294967295 134512640 135167914 3221224448 3220162880 134845930 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 77670 77288 162 162 0 77508 0
[pid=16472] vsize: 310680
Current children cumulated CPU time (s) 1144.56
Current children cumulated vsize (Kb) 312808

[startup+1160.08 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 90475 0 3 0 115009 443 0 0 25 0 1 0 1785856861 319586304 77642 4294967295 134512640 135167914 3221224448 3220167904 134845732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 78024 77642 162 162 0 77862 0
[pid=16472] vsize: 312096
Current children cumulated CPU time (s) 1154.53
Current children cumulated vsize (Kb) 314224

[startup+1170.08 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 111620 0 3 0 115957 495 0 0 25 0 1 0 1785856861 362999808 88241 4294967295 134512640 135167914 3221224448 3220168144 134623919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 88623 88241 162 162 0 88461 0
[pid=16472] vsize: 354492
Current children cumulated CPU time (s) 1164.53
Current children cumulated vsize (Kb) 356620

[startup+1180.08 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 111943 0 3 0 116952 496 0 0 25 0 1 0 1785856861 364322816 88564 4294967295 134512640 135167914 3221224448 3220167744 134844697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 88946 88564 162 162 0 88784 0
[pid=16472] vsize: 355784
Current children cumulated CPU time (s) 1174.49
Current children cumulated vsize (Kb) 357912

[startup+1190.08 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 112405 0 3 0 117945 498 0 0 25 0 1 0 1785856861 366211072 89026 4294967295 134512640 135167914 3221224448 3220170256 134845888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 89407 89026 162 162 0 89245 0
[pid=16472] vsize: 357628
Current children cumulated CPU time (s) 1184.44
Current children cumulated vsize (Kb) 359756

[startup+1200.08 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 112762 0 3 0 118940 500 0 0 25 0 1 0 1785856861 367669248 89383 4294967295 134512640 135167914 3221224448 3220180896 134624005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16472/statm): 89763 89383 162 162 0 89601 0
[pid=16472] vsize: 359052
Current children cumulated CPU time (s) 1194.41
Current children cumulated vsize (Kb) 361180

[startup+1210.08 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 113094 0 3 0 119936 502 0 0 25 0 1 0 1785856861 369025024 89715 4294967295 134512640 135167914 3221224448 3220163408 134849179 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 90094 89715 162 162 0 89932 0
[pid=16472] vsize: 360376
Current children cumulated CPU time (s) 1204.39
Current children cumulated vsize (Kb) 362504



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.08 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 16472
Raw data (/proc/16467/stat): 16467 (minisat+_script) S 16466 16467 6872 0 -1 0 314 346 0 0 0 0 0 1 22 0 1 0 1785856854 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16467/statm): 532 234 485 147 0 385 0
[pid=16467] vsize: 2128
Raw data (/proc/16472/stat): 16472 (minisat+_bignum) R 16467 16467 6872 0 -1 0 113094 0 3 0 119936 502 0 0 25 0 1 0 1785856861 369025024 89715 4294967295 134512640 135167914 3221224448 3220163776 134844706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16472/statm): 90094 89715 162 162 0 89932 0
[pid=16472] vsize: 360376
Current children cumulated CPU time (s) 1204.39
Current children cumulated vsize (Kb) 362504

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

Child status: 0
Real time (s): 1210.25
CPU time (s): 1204.55
CPU user time (s): 1199.37
CPU system time (s): 5.18521
CPU usage (%): 99.5294
Max. virtual memory (cumulated for all children) (Kb): 362504

Verifier Data

ERROR: no interpretation found !