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/11632/stat): 11632 (minisat+_script) R 11631 11632 16528 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1851925819 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/11632/statm): 174 3 169 147 0 27 0
[pid=11632] 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=11633
New process pid=11634
New process pid=11635
execve syscall for /bin/sed executable
One traced child (pid=11634) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=11635) exited with status: 0
One traced child (pid=11633) exited with status: 0
New process pid=11636
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-misc06.opb
One traced child (pid=11636) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=11637
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-misc06.opb

[startup+10.0044 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 3832 0 3 0 862 20 0 0 25 0 1 0 1851925902 16482304 3670 4294967295 134512640 135167914 3221224448 3221223056 134845128 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 4024 3670 162 162 0 3862 0
[pid=11637] vsize: 16096
Current children cumulated CPU time (s) 9.51
Current children cumulated vsize (Kb) 18224

[startup+20.0051 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 6008 0 3 0 1836 31 0 0 25 0 1 0 1851925902 22720512 5203 4294967295 134512640 135167914 3221224448 3221223296 134596402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 5547 5203 162 162 0 5385 0
[pid=11637] vsize: 22188
Current children cumulated CPU time (s) 19.36
Current children cumulated vsize (Kb) 24316

[startup+30.0058 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 6015 0 3 0 2836 32 0 0 25 0 1 0 1851925902 21508096 4911 4294967295 134512640 135167914 3221224448 3221221904 134843113 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 5251 4911 162 162 0 5089 0
[pid=11637] vsize: 21004
Current children cumulated CPU time (s) 29.37
Current children cumulated vsize (Kb) 23132

[startup+40.0065 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 6027 0 3 0 3836 32 0 0 25 0 1 0 1851925902 21508096 4923 4294967295 134512640 135167914 3221224448 3221221840 134844644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 5251 4923 162 162 0 5089 0
[pid=11637] vsize: 21004
Current children cumulated CPU time (s) 39.37
Current children cumulated vsize (Kb) 23132

[startup+50.0072 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 6027 0 3 0 4835 32 0 0 25 0 1 0 1851925902 21508096 4923 4294967295 134512640 135167914 3221224448 3221220032 134849082 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 5251 4923 162 162 0 5089 0
[pid=11637] vsize: 21004
Current children cumulated CPU time (s) 49.36
Current children cumulated vsize (Kb) 23132

[startup+60.0089 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 6027 0 3 0 5836 32 0 0 25 0 1 0 1851925902 21508096 4923 4294967295 134512640 135167914 3221224448 3221221212 134723262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 5251 4923 162 162 0 5089 0
[pid=11637] vsize: 21004
Current children cumulated CPU time (s) 59.37
Current children cumulated vsize (Kb) 23132

[startup+70.0095 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 6027 0 3 0 6835 33 0 0 25 0 1 0 1851925902 21508096 4923 4294967295 134512640 135167914 3221224448 3221221728 134845918 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 5251 4923 162 162 0 5089 0
[pid=11637] vsize: 21004
Current children cumulated CPU time (s) 69.37
Current children cumulated vsize (Kb) 23132

[startup+80.0102 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 6027 0 3 0 7835 33 0 0 25 0 1 0 1851925902 21508096 4923 4294967295 134512640 135167914 3221224448 3221221612 134845876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 5251 4923 162 162 0 5089 0
[pid=11637] vsize: 21004
Current children cumulated CPU time (s) 79.37
Current children cumulated vsize (Kb) 23132

[startup+90.0109 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 6027 0 3 0 8835 33 0 0 25 0 1 0 1851925902 21508096 4923 4294967295 134512640 135167914 3221224448 3221221212 134723262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 5251 4923 162 162 0 5089 0
[pid=11637] vsize: 21004
Current children cumulated CPU time (s) 89.37
Current children cumulated vsize (Kb) 23132

[startup+100.012 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 6027 0 3 0 9835 34 0 0 25 0 1 0 1851925902 21508096 4923 4294967295 134512640 135167914 3221224448 3221222520 134694481 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 5251 4923 162 162 0 5089 0
[pid=11637] vsize: 21004
Current children cumulated CPU time (s) 99.38
Current children cumulated vsize (Kb) 23132

[startup+110.013 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 6027 0 3 0 10834 34 0 0 25 0 1 0 1851925902 21508096 4923 4294967295 134512640 135167914 3221224448 3221221568 134696197 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 5251 4923 162 162 0 5089 0
[pid=11637] vsize: 21004
Current children cumulated CPU time (s) 109.37
Current children cumulated vsize (Kb) 23132

[startup+120.014 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 6027 0 3 0 11834 34 0 0 25 0 1 0 1851925902 21508096 4923 4294967295 134512640 135167914 3221224448 3221220516 134843000 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 5251 4923 162 162 0 5089 0
[pid=11637] vsize: 21004
Current children cumulated CPU time (s) 119.37
Current children cumulated vsize (Kb) 23132

[startup+130.015 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 6130 0 3 0 12834 34 0 0 25 0 1 0 1851925902 22294528 5026 4294967295 134512640 135167914 3221224448 3221219648 134693582 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 5443 5026 162 162 0 5281 0
[pid=11637] vsize: 21772
Current children cumulated CPU time (s) 129.37
Current children cumulated vsize (Kb) 23900

[startup+140.015 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 6135 0 3 0 13834 35 0 0 25 0 1 0 1851925902 22294528 5031 4294967295 134512640 135167914 3221224448 3221219024 134629476 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 5443 5031 162 162 0 5281 0
[pid=11637] vsize: 21772
Current children cumulated CPU time (s) 139.38
Current children cumulated vsize (Kb) 23900

[startup+150.016 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 6321 0 3 0 14833 35 0 0 25 0 1 0 1851925902 22970368 5217 4294967295 134512640 135167914 3221224448 3221221552 134844644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 5608 5217 162 162 0 5446 0
[pid=11637] vsize: 22432
Current children cumulated CPU time (s) 149.37
Current children cumulated vsize (Kb) 24560

[startup+160.017 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 6342 0 3 0 15832 36 0 0 25 0 1 0 1851925902 22970368 5238 4294967295 134512640 135167914 3221224448 3221221792 134694489 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 5608 5238 162 162 0 5446 0
[pid=11637] vsize: 22432
Current children cumulated CPU time (s) 159.37
Current children cumulated vsize (Kb) 24560

[startup+170.018 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 6366 0 3 0 16832 36 0 0 25 0 1 0 1851925902 22970368 5262 4294967295 134512640 135167914 3221224448 3221220496 134845901 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 5608 5262 162 162 0 5446 0
[pid=11637] vsize: 22432
Current children cumulated CPU time (s) 169.37
Current children cumulated vsize (Kb) 24560

[startup+180.017 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 6390 0 3 0 17832 37 0 0 25 0 1 0 1851925902 23756800 5286 4294967295 134512640 135167914 3221224448 3221221460 134849086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 5800 5286 162 162 0 5638 0
[pid=11637] vsize: 23200
Current children cumulated CPU time (s) 179.38
Current children cumulated vsize (Kb) 25328

[startup+190.018 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 6432 0 3 0 18831 37 0 0 25 0 1 0 1851925902 23830528 5328 4294967295 134512640 135167914 3221224448 3221221648 134630835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 5818 5328 162 162 0 5656 0
[pid=11637] vsize: 23272
Current children cumulated CPU time (s) 189.37
Current children cumulated vsize (Kb) 25400

[startup+200.019 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 6498 0 3 0 19831 38 0 0 25 0 1 0 1851925902 24006656 5394 4294967295 134512640 135167914 3221224448 3221221128 134630742 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 5861 5394 162 162 0 5699 0
[pid=11637] vsize: 23444
Current children cumulated CPU time (s) 199.38
Current children cumulated vsize (Kb) 25572

[startup+210.019 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 6885 0 3 0 20830 39 0 0 25 0 1 0 1851925902 24821760 5616 4294967295 134512640 135167914 3221224448 3221219680 134849102 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 6060 5616 162 162 0 5898 0
[pid=11637] vsize: 24240
Current children cumulated CPU time (s) 209.38
Current children cumulated vsize (Kb) 26368

[startup+220.02 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 6992 0 3 0 21828 40 0 0 25 0 1 0 1851925902 25100288 5723 4294967295 134512640 135167914 3221224448 3221222596 134845938 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 6128 5723 162 162 0 5966 0
[pid=11637] vsize: 24512
Current children cumulated CPU time (s) 219.37
Current children cumulated vsize (Kb) 26640

[startup+230.021 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 7094 0 3 0 22827 41 0 0 25 0 1 0 1851925902 25366528 5825 4294967295 134512640 135167914 3221224448 3221222288 134844637 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 6193 5825 162 162 0 6031 0
[pid=11637] vsize: 24772
Current children cumulated CPU time (s) 229.37
Current children cumulated vsize (Kb) 26900

[startup+240.021 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 7209 0 3 0 23826 42 0 0 25 0 1 0 1851925902 27238400 5940 4294967295 134512640 135167914 3221224448 3221221488 134845921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 6650 5940 162 162 0 6488 0
[pid=11637] vsize: 26600
Current children cumulated CPU time (s) 239.37
Current children cumulated vsize (Kb) 28728

[startup+250.022 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 7348 0 3 0 24825 42 0 0 25 0 1 0 1851925902 27602944 6079 4294967295 134512640 135167914 3221224448 3221219264 134843123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 6739 6079 162 162 0 6577 0
[pid=11637] vsize: 26956
Current children cumulated CPU time (s) 249.36
Current children cumulated vsize (Kb) 29084

[startup+260.024 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 7481 0 3 0 25824 43 0 0 25 0 1 0 1851925902 27951104 6212 4294967295 134512640 135167914 3221224448 3221222148 134849060 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 6824 6212 162 162 0 6662 0
[pid=11637] vsize: 27296
Current children cumulated CPU time (s) 259.36
Current children cumulated vsize (Kb) 29424

[startup+270.025 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 8333 0 3 0 26820 46 0 0 25 0 1 0 1851925902 29798400 6734 4294967295 134512640 135167914 3221224448 3221221436 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 7275 6734 162 162 0 7113 0
[pid=11637] vsize: 29100
Current children cumulated CPU time (s) 269.35
Current children cumulated vsize (Kb) 31228

[startup+280.024 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 8446 0 3 0 27819 47 0 0 25 0 1 0 1851925902 30097408 6847 4294967295 134512640 135167914 3221224448 3221221552 134696738 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 7348 6847 162 162 0 7186 0
[pid=11637] vsize: 29392
Current children cumulated CPU time (s) 279.35
Current children cumulated vsize (Kb) 31520

[startup+290.026 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 8559 0 3 0 28818 47 0 0 25 0 1 0 1851925902 30392320 6960 4294967295 134512640 135167914 3221224448 3221221376 134845888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 7420 6960 162 162 0 7258 0
[pid=11637] vsize: 29680
Current children cumulated CPU time (s) 289.34
Current children cumulated vsize (Kb) 31808

[startup+300.027 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 8676 0 3 0 29817 48 0 0 25 0 1 0 1851925902 30703616 7077 4294967295 134512640 135167914 3221224448 3221221452 134722660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 7496 7077 162 162 0 7334 0
[pid=11637] vsize: 29984
Current children cumulated CPU time (s) 299.34
Current children cumulated vsize (Kb) 32112

[startup+310.027 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 8727 0 3 0 30817 48 0 0 25 0 1 0 1851925902 30838784 7128 4294967295 134512640 135167914 3221224448 3221221104 134694338 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 7529 7128 162 162 0 7367 0
[pid=11637] vsize: 30116
Current children cumulated CPU time (s) 309.34
Current children cumulated vsize (Kb) 32244

[startup+320.029 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 8746 0 3 0 31817 48 0 0 25 0 1 0 1851925902 30887936 7147 4294967295 134512640 135167914 3221224448 3221221760 134722532 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 7541 7147 162 162 0 7379 0
[pid=11637] vsize: 30164
Current children cumulated CPU time (s) 319.34
Current children cumulated vsize (Kb) 32292

[startup+330.029 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 8814 0 3 0 32817 49 0 0 25 0 1 0 1851925902 31059968 7215 4294967295 134512640 135167914 3221224448 3221221040 134696587 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 7583 7215 162 162 0 7421 0
[pid=11637] vsize: 30332
Current children cumulated CPU time (s) 329.35
Current children cumulated vsize (Kb) 32460

[startup+340.03 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 8934 0 3 0 33816 49 0 0 25 0 1 0 1851925902 34516992 7335 4294967295 134512640 135167914 3221224448 3221222256 134844641 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 8427 7335 162 162 0 8265 0
[pid=11637] vsize: 33708
Current children cumulated CPU time (s) 339.34
Current children cumulated vsize (Kb) 35836

[startup+350.03 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 9076 0 3 0 34815 50 0 0 25 0 1 0 1851925902 34885632 7477 4294967295 134512640 135167914 3221224448 3221221888 134845933 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 8517 7477 162 162 0 8355 0
[pid=11637] vsize: 34068
Current children cumulated CPU time (s) 349.34
Current children cumulated vsize (Kb) 36196

[startup+360.032 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 9259 0 3 0 35814 51 0 0 25 0 1 0 1851925902 35389440 7660 4294967295 134512640 135167914 3221224448 3221219168 134849082 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 8640 7660 162 162 0 8478 0
[pid=11637] vsize: 34560
Current children cumulated CPU time (s) 359.34
Current children cumulated vsize (Kb) 36688

[startup+370.033 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 9259 0 3 0 36814 51 0 0 25 0 1 0 1851925902 35389440 7660 4294967295 134512640 135167914 3221224448 3221219344 134849102 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 8640 7660 162 162 0 8478 0
[pid=11637] vsize: 34560
Current children cumulated CPU time (s) 369.34
Current children cumulated vsize (Kb) 36688

[startup+380.033 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 9259 0 3 0 37814 51 0 0 25 0 1 0 1851925902 35389440 7660 4294967295 134512640 135167914 3221224448 3221221412 134522496 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 8640 7660 162 162 0 8478 0
[pid=11637] vsize: 34560
Current children cumulated CPU time (s) 379.34
Current children cumulated vsize (Kb) 36688

[startup+390.034 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 9551 0 3 0 38811 53 0 0 25 0 1 0 1851925902 36323328 7910 4294967295 134512640 135167914 3221224448 3221221728 134849153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 8868 7910 162 162 0 8706 0
[pid=11637] vsize: 35472
Current children cumulated CPU time (s) 389.33
Current children cumulated vsize (Kb) 37600

[startup+400.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 9551 0 3 0 39810 53 0 0 25 0 1 0 1851925902 36323328 7910 4294967295 134512640 135167914 3221224448 3221222520 134843032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 8868 7910 162 162 0 8706 0
[pid=11637] vsize: 35472
Current children cumulated CPU time (s) 399.32
Current children cumulated vsize (Kb) 37600

[startup+410.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 9668 0 3 0 40810 54 0 0 25 0 1 0 1851925902 36499456 7985 4294967295 134512640 135167914 3221224448 3221221068 134844632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 8911 7985 162 162 0 8749 0
[pid=11637] vsize: 35644
Current children cumulated CPU time (s) 409.33
Current children cumulated vsize (Kb) 37772

[startup+420.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 9668 0 3 0 41809 54 0 0 25 0 1 0 1851925902 36499456 7985 4294967295 134512640 135167914 3221224448 3221221440 134849068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 8911 7985 162 162 0 8749 0
[pid=11637] vsize: 35644
Current children cumulated CPU time (s) 419.32
Current children cumulated vsize (Kb) 37772

[startup+430.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 9791 0 3 0 42808 55 0 0 25 0 1 0 1851925902 36696064 8066 4294967295 134512640 135167914 3221224448 3221218672 134844723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 8959 8066 162 162 0 8797 0
[pid=11637] vsize: 35836
Current children cumulated CPU time (s) 429.32
Current children cumulated vsize (Kb) 37964

[startup+440.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 9791 0 3 0 43808 55 0 0 25 0 1 0 1851925902 36696064 8066 4294967295 134512640 135167914 3221224448 3221221568 134849099 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 8959 8066 162 162 0 8797 0
[pid=11637] vsize: 35836
Current children cumulated CPU time (s) 439.32
Current children cumulated vsize (Kb) 37964

[startup+450.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 9791 0 3 0 44808 55 0 0 25 0 1 0 1851925902 36696064 8066 4294967295 134512640 135167914 3221224448 3221219352 134694481 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 8959 8066 162 162 0 8797 0
[pid=11637] vsize: 35836
Current children cumulated CPU time (s) 449.32
Current children cumulated vsize (Kb) 37964

[startup+460.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 11243 0 3 0 45805 58 0 0 25 0 1 0 1851925902 39632896 8817 4294967295 134512640 135167914 3221224448 3221220320 134843010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 9676 8817 162 162 0 9514 0
[pid=11637] vsize: 38704
Current children cumulated CPU time (s) 459.32
Current children cumulated vsize (Kb) 40832

[startup+470.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 11243 0 3 0 46805 59 0 0 25 0 1 0 1851925902 39632896 8817 4294967295 134512640 135167914 3221224448 3221220740 134849086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 9676 8817 162 162 0 9514 0
[pid=11637] vsize: 38704
Current children cumulated CPU time (s) 469.33
Current children cumulated vsize (Kb) 40832

[startup+480.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 11276 0 3 0 47805 59 0 0 25 0 1 0 1851925902 39632896 8850 4294967295 134512640 135167914 3221224448 3221218896 134845921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 9676 8850 162 162 0 9514 0
[pid=11637] vsize: 38704
Current children cumulated CPU time (s) 479.33
Current children cumulated vsize (Kb) 40832

[startup+490.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 11276 0 3 0 48805 59 0 0 25 0 1 0 1851925902 39632896 8850 4294967295 134512640 135167914 3221224448 3221219824 134844637 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 9676 8850 162 162 0 9514 0
[pid=11637] vsize: 38704
Current children cumulated CPU time (s) 489.33
Current children cumulated vsize (Kb) 40832

[startup+500.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 11456 0 3 0 49804 59 0 0 25 0 1 0 1851925902 40103936 8988 4294967295 134512640 135167914 3221224448 3221218560 134844706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 9791 8988 162 162 0 9629 0
[pid=11637] vsize: 39164
Current children cumulated CPU time (s) 499.32
Current children cumulated vsize (Kb) 41292

[startup+510.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 11456 0 3 0 50805 59 0 0 25 0 1 0 1851925902 40103936 8988 4294967295 134512640 135167914 3221224448 3221220576 134694345 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 9791 8988 162 162 0 9629 0
[pid=11637] vsize: 39164
Current children cumulated CPU time (s) 509.33
Current children cumulated vsize (Kb) 41292

[startup+520.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 11456 0 3 0 51805 59 0 0 25 0 1 0 1851925902 40103936 8988 4294967295 134512640 135167914 3221224448 3221218384 134844703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 9791 8988 162 162 0 9629 0
[pid=11637] vsize: 39164
Current children cumulated CPU time (s) 519.33
Current children cumulated vsize (Kb) 41292

[startup+530.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 11575 0 3 0 52804 60 0 0 25 0 1 0 1851925902 40284160 9065 4294967295 134512640 135167914 3221224448 3221220448 134844668 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 9835 9065 162 162 0 9673 0
[pid=11637] vsize: 39340
Current children cumulated CPU time (s) 529.33
Current children cumulated vsize (Kb) 41468

[startup+540.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 11575 0 3 0 53804 60 0 0 25 0 1 0 1851925902 40284160 9065 4294967295 134512640 135167914 3221224448 3221222520 134693553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 9835 9065 162 162 0 9673 0
[pid=11637] vsize: 39340
Current children cumulated CPU time (s) 539.33
Current children cumulated vsize (Kb) 41468

[startup+550.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 11707 0 3 0 54804 60 0 0 25 0 1 0 1851925902 40513536 9155 4294967295 134512640 135167914 3221224448 3221220080 134629448 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 9891 9155 162 162 0 9729 0
[pid=11637] vsize: 39564
Current children cumulated CPU time (s) 549.33
Current children cumulated vsize (Kb) 41692

[startup+560.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 11707 0 3 0 55804 60 0 0 25 0 1 0 1851925902 40513536 9155 4294967295 134512640 135167914 3221224448 3221221808 134694351 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 9891 9155 162 162 0 9729 0
[pid=11637] vsize: 39564
Current children cumulated CPU time (s) 559.33
Current children cumulated vsize (Kb) 41692

[startup+570.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 11707 0 3 0 56804 60 0 0 25 0 1 0 1851925902 40513536 9155 4294967295 134512640 135167914 3221224448 3221221128 134629277 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 9891 9155 162 162 0 9729 0
[pid=11637] vsize: 39564
Current children cumulated CPU time (s) 569.33
Current children cumulated vsize (Kb) 41692

[startup+580.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 11843 0 3 0 57803 61 0 0 25 0 1 0 1851925902 40755200 9249 4294967295 134512640 135167914 3221224448 3221218108 134722656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 9950 9249 162 162 0 9788 0
[pid=11637] vsize: 39800
Current children cumulated CPU time (s) 579.33
Current children cumulated vsize (Kb) 41928

[startup+590.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 11843 0 3 0 58804 61 0 0 25 0 1 0 1851925902 40755200 9249 4294967295 134512640 135167914 3221224448 3221220928 134843001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 9950 9249 162 162 0 9788 0
[pid=11637] vsize: 39800
Current children cumulated CPU time (s) 589.34
Current children cumulated vsize (Kb) 41928

[startup+600.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 11876 0 3 0 59804 61 0 0 25 0 1 0 1851925902 40755200 9282 4294967295 134512640 135167914 3221224448 3221219836 134845882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 9950 9282 162 162 0 9788 0
[pid=11637] vsize: 39800
Current children cumulated CPU time (s) 599.34
Current children cumulated vsize (Kb) 41928

[startup+610.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 11876 0 3 0 60804 61 0 0 25 0 1 0 1851925902 40755200 9282 4294967295 134512640 135167914 3221224448 3221221652 134629088 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 9950 9282 162 162 0 9788 0
[pid=11637] vsize: 39800
Current children cumulated CPU time (s) 609.34
Current children cumulated vsize (Kb) 41928

[startup+620.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 12046 0 3 0 61803 62 0 0 25 0 1 0 1851925902 41185280 9410 4294967295 134512640 135167914 3221224448 3221219708 134696176 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 10055 9410 162 162 0 9893 0
[pid=11637] vsize: 40220
Current children cumulated CPU time (s) 619.34
Current children cumulated vsize (Kb) 42348

[startup+630.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 12046 0 3 0 62803 62 0 0 25 0 1 0 1851925902 41185280 9410 4294967295 134512640 135167914 3221224448 3221221900 134844675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 10055 9410 162 162 0 9893 0
[pid=11637] vsize: 40220
Current children cumulated CPU time (s) 629.34
Current children cumulated vsize (Kb) 42348

[startup+640.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 12046 0 3 0 63803 62 0 0 25 0 1 0 1851925902 41185280 9410 4294967295 134512640 135167914 3221224448 3221222156 134722512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 10055 9410 162 162 0 9893 0
[pid=11637] vsize: 40220
Current children cumulated CPU time (s) 639.34
Current children cumulated vsize (Kb) 42348

[startup+650.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 12159 0 3 0 64802 63 0 0 25 0 1 0 1851925902 41345024 9481 4294967295 134512640 135167914 3221224448 3221219616 134845930 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 10094 9481 162 162 0 9932 0
[pid=11637] vsize: 40376
Current children cumulated CPU time (s) 649.34
Current children cumulated vsize (Kb) 42504

[startup+660.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 12159 0 3 0 65802 63 0 0 25 0 1 0 1851925902 41345024 9481 4294967295 134512640 135167914 3221224448 3221221292 134842996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 10094 9481 162 162 0 9932 0
[pid=11637] vsize: 40376
Current children cumulated CPU time (s) 659.34
Current children cumulated vsize (Kb) 42504

[startup+670.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 12266 0 3 0 66802 63 0 0 25 0 1 0 1851925902 41476096 9546 4294967295 134512640 135167914 3221224448 3221220332 134723246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 10126 9546 162 162 0 9964 0
[pid=11637] vsize: 40504
Current children cumulated CPU time (s) 669.34
Current children cumulated vsize (Kb) 42632

[startup+680.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 12266 0 3 0 67802 63 0 0 25 0 1 0 1851925902 41476096 9546 4294967295 134512640 135167914 3221224448 3221221648 134630853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 10126 9546 162 162 0 9964 0
[pid=11637] vsize: 40504
Current children cumulated CPU time (s) 679.34
Current children cumulated vsize (Kb) 42632

[startup+690.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 12400 0 3 0 68802 64 0 0 25 0 1 0 1851925902 41713664 9638 4294967295 134512640 135167914 3221224448 3221219200 134845921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 10184 9638 162 162 0 10022 0
[pid=11637] vsize: 40736
Current children cumulated CPU time (s) 689.35
Current children cumulated vsize (Kb) 42864

[startup+700.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 12400 0 3 0 69802 64 0 0 25 0 1 0 1851925902 41713664 9638 4294967295 134512640 135167914 3221224448 3221221460 134522324 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 10184 9638 162 162 0 10022 0
[pid=11637] vsize: 40736
Current children cumulated CPU time (s) 699.35
Current children cumulated vsize (Kb) 42864

[startup+710.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 12533 0 3 0 70802 64 0 0 25 0 1 0 1851925902 41947136 9729 4294967295 134512640 135167914 3221224448 3221219088 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 10241 9729 162 162 0 10079 0
[pid=11637] vsize: 40964
Current children cumulated CPU time (s) 709.35
Current children cumulated vsize (Kb) 43092

[startup+720.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 12533 0 3 0 71802 65 0 0 25 0 1 0 1851925902 41947136 9729 4294967295 134512640 135167914 3221224448 3221220096 134845906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 10241 9729 162 162 0 10079 0
[pid=11637] vsize: 40964
Current children cumulated CPU time (s) 719.36
Current children cumulated vsize (Kb) 43092

[startup+730.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 12533 0 3 0 72802 65 0 0 25 0 1 0 1851925902 41947136 9729 4294967295 134512640 135167914 3221224448 3221221792 134849110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 10241 9729 162 162 0 10079 0
[pid=11637] vsize: 40964
Current children cumulated CPU time (s) 729.36
Current children cumulated vsize (Kb) 43092

[startup+740.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 12685 0 3 0 73801 65 0 0 25 0 1 0 1851925902 42278912 9839 4294967295 134512640 135167914 3221224448 3221219288 134843032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 10322 9839 162 162 0 10160 0
[pid=11637] vsize: 41288
Current children cumulated CPU time (s) 739.35
Current children cumulated vsize (Kb) 43416

[startup+750.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 12685 0 3 0 74801 65 0 0 25 0 1 0 1851925902 42278912 9839 4294967295 134512640 135167914 3221224448 3221221052 134843002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 10322 9839 162 162 0 10160 0
[pid=11637] vsize: 41288
Current children cumulated CPU time (s) 749.35
Current children cumulated vsize (Kb) 43416

[startup+760.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 12814 0 3 0 75800 66 0 0 25 0 1 0 1851925902 42496000 9926 4294967295 134512640 135167914 3221224448 3221219888 134629049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 10375 9926 162 162 0 10213 0
[pid=11637] vsize: 41500
Current children cumulated CPU time (s) 759.35
Current children cumulated vsize (Kb) 43628

[startup+770.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 12814 0 3 0 76801 66 0 0 25 0 1 0 1851925902 42496000 9926 4294967295 134512640 135167914 3221224448 3221221612 134722512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 10375 9926 162 162 0 10213 0
[pid=11637] vsize: 41500
Current children cumulated CPU time (s) 769.36
Current children cumulated vsize (Kb) 43628

[startup+780.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 12814 0 3 0 77801 66 0 0 25 0 1 0 1851925902 42496000 9926 4294967295 134512640 135167914 3221224448 3221222076 134718176 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 10375 9926 162 162 0 10213 0
[pid=11637] vsize: 41500
Current children cumulated CPU time (s) 779.36
Current children cumulated vsize (Kb) 43628

[startup+790.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 12950 0 3 0 78801 66 0 0 25 0 1 0 1851925902 42737664 10020 4294967295 134512640 135167914 3221224448 3221221116 134843033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 10434 10020 162 162 0 10272 0
[pid=11637] vsize: 41736
Current children cumulated CPU time (s) 789.36
Current children cumulated vsize (Kb) 43864

[startup+800.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 12950 0 3 0 79801 66 0 0 25 0 1 0 1851925902 42737664 10020 4294967295 134512640 135167914 3221224448 3221220656 134843118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 10434 10020 162 162 0 10272 0
[pid=11637] vsize: 41736
Current children cumulated CPU time (s) 799.36
Current children cumulated vsize (Kb) 43864

[startup+810.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 13087 0 3 0 80800 67 0 0 25 0 1 0 1851925902 42983424 10115 4294967295 134512640 135167914 3221224448 3221220032 134843036 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 10494 10115 162 162 0 10332 0
[pid=11637] vsize: 41976
Current children cumulated CPU time (s) 809.36
Current children cumulated vsize (Kb) 44104

[startup+820.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 13087 0 3 0 81800 67 0 0 25 0 1 0 1851925902 42983424 10115 4294967295 134512640 135167914 3221224448 3221221968 134843130 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 10494 10115 162 162 0 10332 0
[pid=11637] vsize: 41976
Current children cumulated CPU time (s) 819.36
Current children cumulated vsize (Kb) 44104

[startup+830.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 13117 0 3 0 82800 67 0 0 25 0 1 0 1851925902 42983424 10145 4294967295 134512640 135167914 3221224448 3221147584 134845927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 10494 10145 162 162 0 10332 0
[pid=11637] vsize: 41976
Current children cumulated CPU time (s) 829.36
Current children cumulated vsize (Kb) 44104

[startup+840.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 13184 0 3 0 83799 69 0 0 25 0 1 0 1851925902 43065344 10170 4294967295 134512640 135167914 3221224448 3221221284 134849060 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 10514 10170 162 162 0 10352 0
[pid=11637] vsize: 42056
Current children cumulated CPU time (s) 839.37
Current children cumulated vsize (Kb) 44184

[startup+850.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 13184 0 3 0 84798 69 0 0 25 0 1 0 1851925902 43065344 10170 4294967295 134512640 135167914 3221224448 3221220764 134849088 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 10514 10170 162 162 0 10352 0
[pid=11637] vsize: 42056
Current children cumulated CPU time (s) 849.36
Current children cumulated vsize (Kb) 44184

[startup+860.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 13373 0 3 0 85797 70 0 0 25 0 1 0 1851925902 49713152 10285 4294967295 134512640 135167914 3221224448 3221220656 134845906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 12137 10285 162 162 0 11975 0
[pid=11637] vsize: 48548
Current children cumulated CPU time (s) 859.36
Current children cumulated vsize (Kb) 50676

[startup+870.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 13373 0 3 0 86797 70 0 0 25 0 1 0 1851925902 49713152 10285 4294967295 134512640 135167914 3221224448 3221222016 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 12137 10285 162 162 0 11975 0
[pid=11637] vsize: 48548
Current children cumulated CPU time (s) 869.36
Current children cumulated vsize (Kb) 50676

[startup+880.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 13487 0 3 0 87797 71 0 0 25 0 1 0 1851925902 49872896 10357 4294967295 134512640 135167914 3221224448 3221220048 134849102 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 12176 10357 162 162 0 12014 0
[pid=11637] vsize: 48704
Current children cumulated CPU time (s) 879.37
Current children cumulated vsize (Kb) 50832

[startup+890.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 13487 0 3 0 88797 71 0 0 25 0 1 0 1851925902 49872896 10357 4294967295 134512640 135167914 3221224448 3221221040 134696656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 12176 10357 162 162 0 12014 0
[pid=11637] vsize: 48704
Current children cumulated CPU time (s) 889.37
Current children cumulated vsize (Kb) 50832

[startup+900.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 13656 0 3 0 89796 72 0 0 25 0 1 0 1851925902 50110464 10450 4294967295 134512640 135167914 3221224448 3221219452 134723251 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 12234 10450 162 162 0 12072 0
[pid=11637] vsize: 48936
Current children cumulated CPU time (s) 899.37
Current children cumulated vsize (Kb) 51064

[startup+910.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 13656 0 3 0 90796 72 0 0 25 0 1 0 1851925902 50110464 10450 4294967295 134512640 135167914 3221224448 3221220672 134696733 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 12234 10450 162 162 0 12072 0
[pid=11637] vsize: 48936
Current children cumulated CPU time (s) 909.37
Current children cumulated vsize (Kb) 51064

[startup+920.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 13656 0 3 0 91796 72 0 0 25 0 1 0 1851925902 50110464 10450 4294967295 134512640 135167914 3221224448 3221219152 134849196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 12234 10450 162 162 0 12072 0
[pid=11637] vsize: 48936
Current children cumulated CPU time (s) 919.37
Current children cumulated vsize (Kb) 51064

[startup+930.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 13806 0 3 0 92796 73 0 0 25 0 1 0 1851925902 50413568 10558 4294967295 134512640 135167914 3221224448 3221220060 134693552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 12308 10558 162 162 0 12146 0
[pid=11637] vsize: 49232
Current children cumulated CPU time (s) 929.38
Current children cumulated vsize (Kb) 51360

[startup+940.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 13806 0 3 0 93796 73 0 0 25 0 1 0 1851925902 50413568 10558 4294967295 134512640 135167914 3221224448 3221219440 134696328 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 12308 10558 162 162 0 12146 0
[pid=11637] vsize: 49232
Current children cumulated CPU time (s) 939.38
Current children cumulated vsize (Kb) 51360

[startup+950.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 13850 0 3 0 94796 73 0 0 25 0 1 0 1851925902 50450432 10602 4294967295 134512640 135167914 3221224448 3221220576 134693582 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 12317 10602 162 162 0 12155 0
[pid=11637] vsize: 49268
Current children cumulated CPU time (s) 949.38
Current children cumulated vsize (Kb) 51396

[startup+960.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 13850 0 3 0 95796 73 0 0 25 0 1 0 1851925902 50450432 10602 4294967295 134512640 135167914 3221224448 3221220844 134718176 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 12317 10602 162 162 0 12155 0
[pid=11637] vsize: 49268
Current children cumulated CPU time (s) 959.38
Current children cumulated vsize (Kb) 51396

[startup+970.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 14049 0 3 0 96795 74 0 0 25 0 1 0 1851925902 50872320 10727 4294967295 134512640 135167914 3221224448 3221219264 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 12420 10727 162 162 0 12258 0
[pid=11637] vsize: 49680
Current children cumulated CPU time (s) 969.38
Current children cumulated vsize (Kb) 51808

[startup+980.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 14049 0 3 0 97795 74 0 0 25 0 1 0 1851925902 50872320 10727 4294967295 134512640 135167914 3221224448 3221220220 134722542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 12420 10727 162 162 0 12258 0
[pid=11637] vsize: 49680
Current children cumulated CPU time (s) 979.38
Current children cumulated vsize (Kb) 51808

[startup+990.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 14151 0 3 0 98795 74 0 0 25 0 1 0 1851925902 51159040 10829 4294967295 134512640 135167914 3221224448 3221151032 134844674 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 12490 10829 162 162 0 12328 0
[pid=11637] vsize: 49960
Current children cumulated CPU time (s) 989.38
Current children cumulated vsize (Kb) 52088

[startup+1000.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 14166 0 3 0 99795 74 0 0 25 0 1 0 1851925902 51048448 10802 4294967295 134512640 135167914 3221224448 3221220528 134849110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 12463 10802 162 162 0 12301 0
[pid=11637] vsize: 49852
Current children cumulated CPU time (s) 999.38
Current children cumulated vsize (Kb) 51980

[startup+1010.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 14166 0 3 0 100795 74 0 0 25 0 1 0 1851925902 51048448 10802 4294967295 134512640 135167914 3221224448 3221222784 134696665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 12463 10802 162 162 0 12301 0
[pid=11637] vsize: 49852
Current children cumulated CPU time (s) 1009.38
Current children cumulated vsize (Kb) 51980

[startup+1020.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 14277 0 3 0 101795 75 0 0 25 0 1 0 1851925902 51195904 10871 4294967295 134512640 135167914 3221224448 3221220320 134844682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 12499 10871 162 162 0 12337 0
[pid=11637] vsize: 49996
Current children cumulated CPU time (s) 1019.39
Current children cumulated vsize (Kb) 52124

[startup+1030.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 14277 0 3 0 102795 75 0 0 25 0 1 0 1851925902 51195904 10871 4294967295 134512640 135167914 3221224448 3221221792 134843139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 12499 10871 162 162 0 12337 0
[pid=11637] vsize: 49996
Current children cumulated CPU time (s) 1029.39
Current children cumulated vsize (Kb) 52124

[startup+1040.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 14411 0 3 0 103795 75 0 0 25 0 1 0 1851925902 51433472 10963 4294967295 134512640 135167914 3221224448 3221219364 134629088 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 12557 10963 162 162 0 12395 0
[pid=11637] vsize: 50228
Current children cumulated CPU time (s) 1039.39
Current children cumulated vsize (Kb) 52356

[startup+1050.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 14411 0 3 0 104795 75 0 0 25 0 1 0 1851925902 51433472 10963 4294967295 134512640 135167914 3221224448 3221221260 134845876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 12557 10963 162 162 0 12395 0
[pid=11637] vsize: 50228
Current children cumulated CPU time (s) 1049.39
Current children cumulated vsize (Kb) 52356

[startup+1060.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 14472 0 3 0 105795 76 0 0 25 0 1 0 1851925902 51548160 11024 4294967295 134512640 135167914 3221224448 3221218848 134844682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 12585 11024 162 162 0 12423 0
[pid=11637] vsize: 50340
Current children cumulated CPU time (s) 1059.4
Current children cumulated vsize (Kb) 52468

[startup+1070.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 14472 0 3 0 106795 76 0 0 25 0 1 0 1851925902 51548160 11024 4294967295 134512640 135167914 3221224448 3221219968 134844641 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 12585 11024 162 162 0 12423 0
[pid=11637] vsize: 50340
Current children cumulated CPU time (s) 1069.4
Current children cumulated vsize (Kb) 52468

[startup+1080.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 14619 0 3 0 107795 76 0 0 25 0 1 0 1851925902 51937280 11139 4294967295 134512640 135167914 3221224448 3221151232 134722610 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 12680 11139 162 162 0 12518 0
[pid=11637] vsize: 50720
Current children cumulated CPU time (s) 1079.4
Current children cumulated vsize (Kb) 52848

[startup+1090.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 14637 0 3 0 108795 77 0 0 25 0 1 0 1851925902 51834880 11115 4294967295 134512640 135167914 3221224448 3221221632 134849068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 12655 11115 162 162 0 12493 0
[pid=11637] vsize: 50620
Current children cumulated CPU time (s) 1089.41
Current children cumulated vsize (Kb) 52748

[startup+1100.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 14660 0 3 0 109795 77 0 0 25 0 1 0 1851925902 51834880 11138 4294967295 134512640 135167914 3221224448 3221148480 134844745 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 12655 11138 162 162 0 12493 0
[pid=11637] vsize: 50620
Current children cumulated CPU time (s) 1099.41
Current children cumulated vsize (Kb) 52748

[startup+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 14744 0 3 0 110795 77 0 0 25 0 1 0 1851925902 51974144 11180 4294967295 134512640 135167914 3221224448 3221221504 134844846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 12689 11180 162 162 0 12527 0
[pid=11637] vsize: 50756
Current children cumulated CPU time (s) 1109.41
Current children cumulated vsize (Kb) 52884

[startup+1120.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 14744 0 3 0 111795 77 0 0 25 0 1 0 1851925902 51974144 11180 4294967295 134512640 135167914 3221224448 3221221904 134844676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 12689 11180 162 162 0 12527 0
[pid=11637] vsize: 50756
Current children cumulated CPU time (s) 1119.41
Current children cumulated vsize (Kb) 52884

[startup+1130.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 14870 0 3 0 112794 78 0 0 25 0 1 0 1851925902 52187136 11264 4294967295 134512640 135167914 3221224448 3221219296 134695266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11637/statm): 12741 11264 162 162 0 12579 0
[pid=11637] vsize: 50964
Current children cumulated CPU time (s) 1129.41
Current children cumulated vsize (Kb) 53092

[startup+1140.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 14870 0 3 0 113793 78 0 0 25 0 1 0 1851925902 52187136 11264 4294967295 134512640 135167914 3221224448 3221220608 134844718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 12741 11264 162 162 0 12579 0
[pid=11637] vsize: 50964
Current children cumulated CPU time (s) 1139.4
Current children cumulated vsize (Kb) 53092

[startup+1150.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 15003 0 3 0 114792 79 0 0 25 0 1 0 1851925902 52424704 11355 4294967295 134512640 135167914 3221224448 3221220180 134843000 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 12799 11355 162 162 0 12637 0
[pid=11637] vsize: 51196
Current children cumulated CPU time (s) 1149.4
Current children cumulated vsize (Kb) 53324

[startup+1160.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 15003 0 3 0 115792 79 0 0 25 0 1 0 1851925902 52424704 11355 4294967295 134512640 135167914 3221224448 3221222144 134849148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 12799 11355 162 162 0 12637 0
[pid=11637] vsize: 51196
Current children cumulated CPU time (s) 1159.4
Current children cumulated vsize (Kb) 53324

[startup+1170.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 18508 0 3 0 116779 88 0 0 25 0 1 0 1851925902 60039168 13542 4294967295 134512640 135167914 3221224448 3221221648 134629236 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 14658 13542 162 162 0 14496 0
[pid=11637] vsize: 58632
Current children cumulated CPU time (s) 1169.36
Current children cumulated vsize (Kb) 60760

[startup+1180.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 19111 0 3 0 117775 90 0 0 25 0 1 0 1851925902 61603840 14145 4294967295 134512640 135167914 3221224448 3221222692 134849086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 15040 14145 162 162 0 14878 0
[pid=11637] vsize: 60160
Current children cumulated CPU time (s) 1179.34
Current children cumulated vsize (Kb) 62288

[startup+1190.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 20064 0 3 0 118768 93 0 0 25 0 1 0 1851925902 64069632 15098 4294967295 134512640 135167914 3221224448 3221223260 134693552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 15642 15098 162 162 0 15480 0
[pid=11637] vsize: 62568
Current children cumulated CPU time (s) 1189.3
Current children cumulated vsize (Kb) 64696

[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) T 11632 11632 16528 0 -1 0 24385 0 3 0 119731 109 0 0 25 0 1 0 1851925902 79065088 18759 4294967295 134512640 135167914 3221224448 3221049244 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/11637/statm): 19303 18759 162 162 0 19141 0
[pid=11637] vsize: 77212
Current children cumulated CPU time (s) 1199.09
Current children cumulated vsize (Kb) 79340

[startup+1210.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) R 11632 11632 16528 0 -1 0 28745 0 3 0 120693 127 0 0 25 0 1 0 1851925902 94224384 22460 4294967295 134512640 135167914 3221224448 3221053888 134694428 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11637/statm): 23004 22460 162 162 0 22842 0
[pid=11637] vsize: 92016
Current children cumulated CPU time (s) 1208.89
Current children cumulated vsize (Kb) 94144



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11637
Raw data (/proc/11632/stat): 11632 (minisat+_script) S 11631 11632 16528 0 -1 0 314 2311 0 0 0 1 58 10 17 0 1 0 1851925819 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11632/statm): 532 234 485 147 0 385 0
[pid=11632] vsize: 2128
Raw data (/proc/11637/stat): 11637 (minisat+_bignum) T 11632 11632 16528 0 -1 0 28745 0 3 0 120693 127 0 0 25 0 1 0 1851925902 94224384 22460 4294967295 134512640 135167914 3221224448 3221050092 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/11637/statm): 23004 22460 162 162 0 22842 0
[pid=11637] vsize: 92016
Current children cumulated CPU time (s) 1208.89
Current children cumulated vsize (Kb) 94144

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

Child status: 0
Real time (s): 1210.13
CPU time (s): 1208.26
CPU user time (s): 1206.94
CPU system time (s): 1.3168
CPU usage (%): 99.845
Max. virtual memory (cumulated for all children) (Kb): 94144