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/32641/stat): 32641 (minisat+_script) R 32640 32641 9102 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1854950015 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/32641/statm): 174 3 169 147 0 27 0
[pid=32641] 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=32642
New process pid=32643
New process pid=32644
execve syscall for /bin/sed executable
One traced child (pid=32643) 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=32644) exited with status: 0
One traced child (pid=32642) exited with status: 0
New process pid=32645
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-dfl001.opb
One traced child (pid=32645) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=32646
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-dfl001.opb

[startup+10.0042 s]
Raw data (loadavg): 1.01 0.98 0.95 1/58 32646
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) T 32641 32641 9102 0 -1 0 7361 0 0 0 920 36 0 0 25 0 1 0 1854950025 37302272 6745 4294967295 134512640 135167914 3221224448 3221223352 134865821 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/32646/statm): 9107 6745 162 162 0 8945 0
[pid=32646] vsize: 36428
Current children cumulated CPU time (s) 9.6
Current children cumulated vsize (Kb) 38556

[startup+20.0052 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32648
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 11409 0 0 0 1882 53 0 0 25 0 1 0 1854950025 50417664 10402 4294967295 134512640 135167914 3221224448 3221221648 134844676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32646/statm): 12309 10402 162 162 0 12147 0
[pid=32646] vsize: 49236
Current children cumulated CPU time (s) 19.39
Current children cumulated vsize (Kb) 51364

[startup+30.0071 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32648
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 14894 0 0 0 2843 70 0 0 25 0 1 0 1854950025 62672896 13752 4294967295 134512640 135167914 3221224448 3221221640 134843032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32646/statm): 15301 13752 162 162 0 15139 0
[pid=32646] vsize: 61204
Current children cumulated CPU time (s) 29.17
Current children cumulated vsize (Kb) 63332

[startup+40.008 s]
Raw data (loadavg): 1.00 0.98 0.95 1/58 32648
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) T 32641 32641 9102 0 -1 0 18240 0 0 0 3802 87 0 0 25 0 1 0 1854950025 75059200 17040 4294967295 134512640 135167914 3221224448 3221222556 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/32646/statm): 18325 17040 162 162 0 18163 0
[pid=32646] vsize: 73300
Current children cumulated CPU time (s) 38.93
Current children cumulated vsize (Kb) 75428

[startup+50.0099 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32648
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 21430 0 0 0 4766 104 0 0 25 0 1 0 1854950025 86630400 20097 4294967295 134512640 135167914 3221224448 3221222704 134843064 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32646/statm): 21150 20097 162 162 0 20988 0
[pid=32646] vsize: 84600
Current children cumulated CPU time (s) 48.74
Current children cumulated vsize (Kb) 86728

[startup+60.0109 s]
Raw data (loadavg): 1.00 0.98 0.95 1/58 32648
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) T 32641 32641 9102 0 -1 0 24468 0 0 0 5726 124 0 0 25 0 1 0 1854950025 98455552 23135 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/32646/statm): 24037 23135 162 162 0 23875 0
[pid=32646] vsize: 96148
Current children cumulated CPU time (s) 58.54
Current children cumulated vsize (Kb) 98276

[startup+70.0118 s]
Raw data (loadavg): 1.00 0.98 0.95 1/58 32648
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) T 32641 32641 9102 0 -1 0 27532 0 0 0 6684 144 0 0 25 0 1 0 1854950025 110579712 26199 4294967295 134512640 135167914 3221224448 3221222604 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/32646/statm): 26997 26199 162 162 0 26835 0
[pid=32646] vsize: 107988
Current children cumulated CPU time (s) 68.32
Current children cumulated vsize (Kb) 110116

[startup+80.0138 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32650
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 31743 0 0 0 7649 162 0 0 25 0 1 0 1854950025 127684608 30410 4294967295 134512640 135167914 3221224448 3221223264 134522189 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32646/statm): 31173 30410 162 162 0 31011 0
[pid=32646] vsize: 124692
Current children cumulated CPU time (s) 78.15
Current children cumulated vsize (Kb) 126820

[startup+90.0147 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32650
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 31745 0 0 0 8650 162 0 0 25 0 1 0 1854950025 127684608 30412 4294967295 134512640 135167914 3221224448 3221223216 134691307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32646/statm): 31173 30412 162 162 0 31011 0
[pid=32646] vsize: 124692
Current children cumulated CPU time (s) 88.16
Current children cumulated vsize (Kb) 126820

[startup+100.016 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32650
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 31788 0 0 0 9649 162 0 0 25 0 1 0 1854950025 121913344 29022 4294967295 134512640 135167914 3221224448 3221222864 134849187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32646/statm): 29764 29022 162 162 0 29602 0
[pid=32646] vsize: 119056
Current children cumulated CPU time (s) 98.15
Current children cumulated vsize (Kb) 121184

[startup+110.017 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32650
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 33005 0 0 0 10641 166 0 0 25 0 1 0 1854950025 126222336 30074 4294967295 134512640 135167914 3221224448 3221098592 134843160 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32646/statm): 30816 30074 162 162 0 30654 0
[pid=32646] vsize: 123264
Current children cumulated CPU time (s) 108.11
Current children cumulated vsize (Kb) 125392

[startup+120.017 s]
Raw data (loadavg): 1.00 0.98 0.95 1/58 32650
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) T 32641 32641 9102 0 -1 0 36308 0 0 0 11609 181 0 0 25 0 1 0 1854950025 138399744 33047 4294967295 134512640 135167914 3221224448 3221098524 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/32646/statm): 33789 33047 162 162 0 33627 0
[pid=32646] vsize: 135156
Current children cumulated CPU time (s) 117.94
Current children cumulated vsize (Kb) 137284

[startup+130.018 s]
Raw data (loadavg): 1.00 0.98 0.95 1/58 32650
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) T 32641 32641 9102 0 -1 0 40415 0 0 0 12574 198 0 0 25 0 1 0 1854950025 152522752 36495 4294967295 134512640 135167914 3221224448 3221107068 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/32646/statm): 37237 36495 162 162 0 37075 0
[pid=32646] vsize: 148948
Current children cumulated CPU time (s) 127.76
Current children cumulated vsize (Kb) 151076

[startup+140.019 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32652
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 45512 0 0 0 13541 215 0 0 25 0 1 0 1854950025 168001536 40274 4294967295 134512640 135167914 3221224448 3221094312 134845939 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32646/statm): 41016 40274 162 162 0 40854 0
[pid=32646] vsize: 164064
Current children cumulated CPU time (s) 137.6
Current children cumulated vsize (Kb) 166192

[startup+150.021 s]
Raw data (loadavg): 1.00 0.98 0.95 1/58 32652
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) T 32641 32641 9102 0 -1 0 48578 0 0 0 14509 230 0 0 25 0 1 0 1854950025 180559872 43340 4294967295 134512640 135167914 3221224448 3221113340 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/32646/statm): 44082 43340 162 162 0 43920 0
[pid=32646] vsize: 176328
Current children cumulated CPU time (s) 147.43
Current children cumulated vsize (Kb) 178456

[startup+160.022 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32652
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) T 32641 32641 9102 0 -1 0 51242 0 0 0 15477 243 0 0 25 0 1 0 1854950025 191471616 46004 4294967295 134512640 135167914 3221224448 3221095868 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/32646/statm): 46746 46004 162 162 0 46584 0
[pid=32646] vsize: 186984
Current children cumulated CPU time (s) 157.24
Current children cumulated vsize (Kb) 189112

[startup+170.022 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32652
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 58664 0 0 0 16440 266 0 0 25 0 1 0 1854950025 211070976 50789 4294967295 134512640 135167914 3221224448 3221141840 134693576 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32646/statm): 51531 50789 162 162 0 51369 0
[pid=32646] vsize: 206124
Current children cumulated CPU time (s) 167.1
Current children cumulated vsize (Kb) 208252

[startup+180.023 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32652
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 61465 0 0 0 17412 278 0 0 25 0 1 0 1854950025 222543872 53590 4294967295 134512640 135167914 3221224448 3221108832 134844700 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32646/statm): 54332 53590 162 162 0 54170 0
[pid=32646] vsize: 217328
Current children cumulated CPU time (s) 176.94
Current children cumulated vsize (Kb) 219456

[startup+190.024 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32652
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 64238 0 0 0 18383 291 0 0 25 0 1 0 1854950025 233902080 56363 4294967295 134512640 135167914 3221224448 3221117216 134844725 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32646/statm): 57105 56363 162 162 0 56943 0
[pid=32646] vsize: 228420
Current children cumulated CPU time (s) 186.78
Current children cumulated vsize (Kb) 230548

[startup+200.025 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32654
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 67822 0 0 0 19345 308 0 0 25 0 1 0 1854950025 248582144 59947 4294967295 134512640 135167914 3221224448 3221104912 134623813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32646/statm): 60689 59947 162 162 0 60527 0
[pid=32646] vsize: 242756
Current children cumulated CPU time (s) 196.57
Current children cumulated vsize (Kb) 244884

[startup+210.026 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32654
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 70569 0 0 0 20315 321 0 0 25 0 1 0 1854950025 259833856 62694 4294967295 134512640 135167914 3221224448 3221109312 134844691 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32646/statm): 63436 62694 162 162 0 63274 0
[pid=32646] vsize: 253744
Current children cumulated CPU time (s) 206.4
Current children cumulated vsize (Kb) 255872

[startup+220.027 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32654
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 81349 0 0 0 21269 351 0 0 25 0 1 0 1854950025 314449920 73474 4294967295 134512640 135167914 3221224448 3221113504 134625368 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32646/statm): 76770 73482 162 162 0 76608 0
[pid=32646] vsize: 307080
Current children cumulated CPU time (s) 216.24
Current children cumulated vsize (Kb) 309208

[startup+230.028 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32654
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 85729 0 0 0 22244 364 0 0 25 0 1 0 1854950025 300331008 72581 4294967295 134512640 135167914 3221224448 3221098912 134849068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32646/statm): 73323 72581 162 162 0 73161 0
[pid=32646] vsize: 293292
Current children cumulated CPU time (s) 226.12
Current children cumulated vsize (Kb) 295420

[startup+240.029 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32654
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 88503 0 0 0 23213 378 0 0 25 0 1 0 1854950025 311693312 75355 4294967295 134512640 135167914 3221224448 3221119728 134849153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32646/statm): 76097 75355 162 162 0 75935 0
[pid=32646] vsize: 304388
Current children cumulated CPU time (s) 235.95
Current children cumulated vsize (Kb) 306516

[startup+250.031 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32654
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 91339 0 0 0 24182 390 0 0 25 0 1 0 1854950025 323309568 78191 4294967295 134512640 135167914 3221224448 3221094776 134845877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32646/statm): 78933 78191 162 162 0 78771 0
[pid=32646] vsize: 315732
Current children cumulated CPU time (s) 245.76
Current children cumulated vsize (Kb) 317860

[startup+260.031 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32656
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 94147 0 0 0 25152 403 0 0 25 0 1 0 1854950025 334811136 80999 4294967295 134512640 135167914 3221224448 3221115328 134844706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32646/statm): 81741 80999 162 162 0 81579 0
[pid=32646] vsize: 326964
Current children cumulated CPU time (s) 255.59
Current children cumulated vsize (Kb) 329092

[startup+270.032 s]
Raw data (loadavg): 1.00 0.98 0.95 1/58 32656
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) T 32641 32641 9102 0 -1 0 97033 0 0 0 26118 418 0 0 25 0 1 0 1854950025 346632192 83885 4294967295 134512640 135167914 3221224448 3221096732 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/32646/statm): 84627 83885 162 162 0 84465 0
[pid=32646] vsize: 338508
Current children cumulated CPU time (s) 265.4
Current children cumulated vsize (Kb) 340636

[startup+280.033 s]
Raw data (loadavg): 1.00 0.98 0.95 1/58 32656
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) T 32641 32641 9102 0 -1 0 99921 0 0 0 27088 429 0 0 25 0 1 0 1854950025 358461440 86773 4294967295 134512640 135167914 3221224448 3221097404 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/32646/statm): 87515 86773 162 162 0 87353 0
[pid=32646] vsize: 350060
Current children cumulated CPU time (s) 275.21
Current children cumulated vsize (Kb) 352188

[startup+290.034 s]
Raw data (loadavg): 1.00 0.98 0.95 1/58 32656
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) T 32641 32641 9102 0 -1 0 102893 0 0 0 28057 443 0 0 25 0 1 0 1854950025 370634752 89745 4294967295 134512640 135167914 3221224448 3221089116 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/32646/statm): 90487 89745 162 162 0 90325 0
[pid=32646] vsize: 361948
Current children cumulated CPU time (s) 285.04
Current children cumulated vsize (Kb) 364076

[startup+300.035 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32656
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 106007 0 0 0 29023 456 0 0 25 0 1 0 1854950025 383389696 92859 4294967295 134512640 135167914 3221224448 3221117756 134693552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32646/statm): 93601 92859 162 162 0 93439 0
[pid=32646] vsize: 374404
Current children cumulated CPU time (s) 294.83
Current children cumulated vsize (Kb) 376532

[startup+310.036 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32656
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 109282 0 0 0 29986 471 0 0 25 0 1 0 1854950025 396804096 96134 4294967295 134512640 135167914 3221224448 3221090080 134694428 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32646/statm): 96876 96134 162 162 0 96714 0
[pid=32646] vsize: 387504
Current children cumulated CPU time (s) 304.61
Current children cumulated vsize (Kb) 389632

[startup+320.037 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32658
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 112205 0 0 0 30954 485 0 0 25 0 1 0 1854950025 408776704 99057 4294967295 134512640 135167914 3221224448 3221097488 134849108 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32646/statm): 99799 99057 162 162 0 99637 0
[pid=32646] vsize: 399196
Current children cumulated CPU time (s) 314.43
Current children cumulated vsize (Kb) 401324

[startup+330.038 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32658
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 114926 0 0 0 31924 498 0 0 25 0 1 0 1854950025 419921920 101778 4294967295 134512640 135167914 3221224448 3221095692 134849088 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32646/statm): 102520 101778 162 162 0 102358 0
[pid=32646] vsize: 410080
Current children cumulated CPU time (s) 324.26
Current children cumulated vsize (Kb) 412208

[startup+340.039 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32658
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 136787 0 0 0 32866 551 0 0 25 0 1 0 1854950025 509464576 123639 4294967295 134512640 135167914 3221224448 3221144592 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32646/statm): 124381 123639 162 162 0 124219 0
[pid=32646] vsize: 497524
Current children cumulated CPU time (s) 334.21
Current children cumulated vsize (Kb) 499652

[startup+350.04 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32658
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 139360 0 0 0 33833 566 0 0 25 0 1 0 1854950025 476807168 115666 4294967295 134512640 135167914 3221224448 3221098044 134849056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32646/statm): 116408 115666 162 162 0 116246 0
[pid=32646] vsize: 465632
Current children cumulated CPU time (s) 344.03
Current children cumulated vsize (Kb) 467760

[startup+360.041 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32658
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 142464 0 0 0 34799 579 0 0 25 0 1 0 1854950025 489521152 118770 4294967295 134512640 135167914 3221224448 3221088432 134620081 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32646/statm): 119512 118770 162 162 0 119350 0
[pid=32646] vsize: 478048
Current children cumulated CPU time (s) 353.82
Current children cumulated vsize (Kb) 480176

[startup+370.042 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32658
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 145292 0 0 0 35766 593 0 0 25 0 1 0 1854950025 501104640 121598 4294967295 134512640 135167914 3221224448 3221090528 134843139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32646/statm): 122340 121598 162 162 0 122178 0
[pid=32646] vsize: 489360
Current children cumulated CPU time (s) 363.63
Current children cumulated vsize (Kb) 491488

[startup+380.043 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32660
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 148125 0 0 0 36732 608 0 0 25 0 1 0 1854950025 512708608 124431 4294967295 134512640 135167914 3221224448 3221099872 134844720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32646/statm): 125173 124431 162 162 0 125011 0
[pid=32646] vsize: 500692
Current children cumulated CPU time (s) 373.44
Current children cumulated vsize (Kb) 502820

[startup+390.044 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32660
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 150927 0 0 0 37701 620 0 0 25 0 1 0 1854950025 524185600 127233 4294967295 134512640 135167914 3221224448 3221092688 134620562 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32646/statm): 127975 127233 162 162 0 127813 0
[pid=32646] vsize: 511900
Current children cumulated CPU time (s) 383.25
Current children cumulated vsize (Kb) 514028

[startup+400.045 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32660
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 153877 0 0 0 38667 633 0 0 25 0 1 0 1854950025 536268800 130183 4294967295 134512640 135167914 3221224448 3221135648 134843404 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32646/statm): 130925 130183 162 162 0 130763 0
[pid=32646] vsize: 523700
Current children cumulated CPU time (s) 393.04
Current children cumulated vsize (Kb) 525828

[startup+410.045 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32660
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 157120 0 0 0 39631 647 0 0 25 0 1 0 1854950025 549552128 133426 4294967295 134512640 135167914 3221224448 3221095008 134694392 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32646/statm): 134168 133426 162 162 0 134006 0
[pid=32646] vsize: 536672
Current children cumulated CPU time (s) 402.82
Current children cumulated vsize (Kb) 538800

[startup+420.045 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32660
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 160172 0 0 0 40598 662 0 0 25 0 1 0 1854950025 562053120 136478 4294967295 134512640 135167914 3221224448 3221095088 134522462 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32646/statm): 137220 136478 162 162 0 137058 0
[pid=32646] vsize: 548880
Current children cumulated CPU time (s) 412.64
Current children cumulated vsize (Kb) 551008

[startup+430.046 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32660
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) T 32641 32641 9102 0 -1 0 162928 0 0 0 41565 675 0 0 25 0 1 0 1854950025 573341696 139234 4294967295 134512640 135167914 3221224448 3221087500 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/32646/statm): 139976 139234 162 162 0 139814 0
[pid=32646] vsize: 559904
Current children cumulated CPU time (s) 422.44
Current children cumulated vsize (Kb) 562032

[startup+440.047 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32662
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 165791 0 0 0 42533 688 0 0 25 0 1 0 1854950025 585068544 142097 4294967295 134512640 135167914 3221224448 3221094624 134722527 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32646/statm): 142839 142097 162 162 0 142677 0
[pid=32646] vsize: 571356
Current children cumulated CPU time (s) 432.25
Current children cumulated vsize (Kb) 573484

[startup+450.048 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32662
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) T 32641 32641 9102 0 -1 0 168763 0 0 0 43502 702 0 0 25 0 1 0 1854950025 597241856 145069 4294967295 134512640 135167914 3221224448 3221097308 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/32646/statm): 145811 145069 162 162 0 145649 0
[pid=32646] vsize: 583244
Current children cumulated CPU time (s) 442.08
Current children cumulated vsize (Kb) 585372

[startup+460.049 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32662
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 171494 0 0 0 44471 714 0 0 25 0 1 0 1854950025 608428032 147800 4294967295 134512640 135167914 3221224448 3221098712 134843032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32646/statm): 148542 147800 162 162 0 148380 0
[pid=32646] vsize: 594168
Current children cumulated CPU time (s) 451.89
Current children cumulated vsize (Kb) 596296

[startup+470.049 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32662
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 174211 0 0 0 45438 726 0 0 25 0 1 0 1854950025 619556864 150517 4294967295 134512640 135167914 3221224448 3221117592 134842997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32646/statm): 151259 150517 162 162 0 151097 0
[pid=32646] vsize: 605036
Current children cumulated CPU time (s) 461.68
Current children cumulated vsize (Kb) 607164

[startup+480.05 s]
Raw data (loadavg): 1.00 0.98 0.95 1/58 32662
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) T 32641 32641 9102 0 -1 0 177441 0 0 0 46403 742 0 0 25 0 1 0 1854950025 632786944 153747 4294967295 134512640 135167914 3221224448 3221134764 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/32646/statm): 154489 153747 162 162 0 154327 0
[pid=32646] vsize: 617956
Current children cumulated CPU time (s) 471.49
Current children cumulated vsize (Kb) 620084

[startup+490.051 s]
Raw data (loadavg): 1.00 0.98 0.95 1/58 32662
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) T 32641 32641 9102 0 -1 0 180373 0 0 0 47372 755 0 0 25 0 1 0 1854950025 644796416 156679 4294967295 134512640 135167914 3221224448 3221086556 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/32646/statm): 157421 156679 162 162 0 157259 0
[pid=32646] vsize: 629684
Current children cumulated CPU time (s) 481.31
Current children cumulated vsize (Kb) 631812

[startup+500.053 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32664
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 183177 0 0 0 48342 767 0 0 25 0 1 0 1854950025 656281600 159483 4294967295 134512640 135167914 3221224448 3221105568 134844831 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32646/statm): 160225 159483 162 162 0 160063 0
[pid=32646] vsize: 640900
Current children cumulated CPU time (s) 491.13
Current children cumulated vsize (Kb) 643028

[startup+510.054 s]
Raw data (loadavg): 1.00 0.98 0.95 1/58 32664
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) T 32641 32641 9102 0 -1 0 186012 0 0 0 49312 778 0 0 25 0 1 0 1854950025 667893760 162318 4294967295 134512640 135167914 3221224448 3221116508 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/32646/statm): 163060 162318 162 162 0 162898 0
[pid=32646] vsize: 652240
Current children cumulated CPU time (s) 500.94
Current children cumulated vsize (Kb) 654368

[startup+520.055 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32664
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 188791 0 0 0 50285 790 0 0 25 0 1 0 1854950025 679276544 165097 4294967295 134512640 135167914 3221224448 3221097052 134694368 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32646/statm): 165839 165097 162 162 0 165677 0
[pid=32646] vsize: 663356
Current children cumulated CPU time (s) 510.79
Current children cumulated vsize (Kb) 665484

[startup+530.056 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32664
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 191519 0 0 0 51257 801 0 0 25 0 1 0 1854950025 690450432 167825 4294967295 134512640 135167914 3221224448 3221094656 134843402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32646/statm): 168567 167825 162 162 0 168405 0
[pid=32646] vsize: 674268
Current children cumulated CPU time (s) 520.62
Current children cumulated vsize (Kb) 676396

[startup+540.057 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32664
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) T 32641 32641 9102 0 -1 0 194372 0 0 0 52222 816 0 0 25 0 1 0 1854950025 702136320 170678 4294967295 134512640 135167914 3221224448 3221097308 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/32646/statm): 171420 170678 162 162 0 171258 0
[pid=32646] vsize: 685680
Current children cumulated CPU time (s) 530.42
Current children cumulated vsize (Kb) 687808

[startup+550.058 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32664
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 197165 0 0 0 53192 829 0 0 25 0 1 0 1854950025 713576448 173471 4294967295 134512640 135167914 3221224448 3221101968 134693582 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32646/statm): 174213 173471 162 162 0 174051 0
[pid=32646] vsize: 696852
Current children cumulated CPU time (s) 540.25
Current children cumulated vsize (Kb) 698980

[startup+560.059 s]
Raw data (loadavg): 1.00 0.98 0.95 1/58 32666
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) T 32641 32641 9102 0 -1 0 199899 0 0 0 54161 842 0 0 25 0 1 0 1854950025 724774912 176205 4294967295 134512640 135167914 3221224448 3221086716 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/32646/statm): 176947 176205 162 162 0 176785 0
[pid=32646] vsize: 707788
Current children cumulated CPU time (s) 550.07
Current children cumulated vsize (Kb) 709916

[startup+570.06 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32666
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 242568 0 0 0 55058 942 0 0 25 0 1 0 1854950025 899547136 218874 4294967295 134512640 135167914 3221224448 3221101152 134624993 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32646/statm): 219616 218874 162 162 0 219454 0
[pid=32646] vsize: 878464
Current children cumulated CPU time (s) 560.04
Current children cumulated vsize (Kb) 880592

[startup+580.061 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32666
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) T 32641 32641 9102 0 -1 0 243179 0 0 0 56048 949 0 0 25 0 1 0 1854950025 815661056 198394 4294967295 134512640 135167914 3221224448 3221103484 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/32646/statm): 199136 198394 162 162 0 198974 0
[pid=32646] vsize: 796544
Current children cumulated CPU time (s) 570.01
Current children cumulated vsize (Kb) 798672

[startup+590.062 s]
Raw data (loadavg): 1.00 0.98 0.95 1/58 32666
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) T 32641 32641 9102 0 -1 0 246070 0 0 0 57018 962 0 0 20 0 1 0 1854950025 827502592 201285 4294967295 134512640 135167914 3221224448 3221092924 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/32646/statm): 202027 201285 162 162 0 201865 0
[pid=32646] vsize: 808108
Current children cumulated CPU time (s) 579.84
Current children cumulated vsize (Kb) 810236

[startup+600.064 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32666
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 248799 0 0 0 57989 973 0 0 25 0 1 0 1854950025 838680576 204014 4294967295 134512640 135167914 3221224448 3221092640 134849082 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32646/statm): 204756 204014 162 162 0 204594 0
[pid=32646] vsize: 819024
Current children cumulated CPU time (s) 589.66
Current children cumulated vsize (Kb) 821152

[startup+610.065 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32666
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 252006 0 0 0 58953 988 0 0 25 0 1 0 1854950025 851816448 207221 4294967295 134512640 135167914 3221224448 3221102496 134844728 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32646/statm): 207963 207221 162 162 0 207801 0
[pid=32646] vsize: 831852
Current children cumulated CPU time (s) 599.45
Current children cumulated vsize (Kb) 833980

[startup+620.066 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32668
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 255220 0 0 0 59919 1002 0 0 25 0 1 0 1854950025 864980992 210435 4294967295 134512640 135167914 3221224448 3221092624 134849153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32646/statm): 211177 210435 162 162 0 211015 0
[pid=32646] vsize: 844708
Current children cumulated CPU time (s) 609.25
Current children cumulated vsize (Kb) 846836

[startup+630.067 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32668
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 257965 0 0 0 60891 1013 0 0 25 0 1 0 1854950025 876224512 213180 4294967295 134512640 135167914 3221224448 3221092032 134843026 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32646/statm): 213922 213180 162 162 0 213760 0
[pid=32646] vsize: 855688
Current children cumulated CPU time (s) 619.08
Current children cumulated vsize (Kb) 857816

[startup+640.068 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32668
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 260828 0 0 0 61856 1028 0 0 25 0 1 0 1854950025 887951360 216043 4294967295 134512640 135167914 3221224448 3221119628 134844675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32646/statm): 216785 216043 162 162 0 216623 0
[pid=32646] vsize: 867140
Current children cumulated CPU time (s) 628.88
Current children cumulated vsize (Kb) 869268

[startup+650.069 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32668
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 263767 0 0 0 62822 1040 0 0 25 0 1 0 1854950025 899989504 218982 4294967295 134512640 135167914 3221224448 3221121896 134846921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32646/statm): 219724 218982 162 162 0 219562 0
[pid=32646] vsize: 878896
Current children cumulated CPU time (s) 638.66
Current children cumulated vsize (Kb) 881024

[startup+660.07 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32668
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) T 32641 32641 9102 0 -1 0 266582 0 0 0 63791 1053 0 0 25 0 1 0 1854950025 911519744 221797 4294967295 134512640 135167914 3221224448 3221097884 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/32646/statm): 222539 221797 162 162 0 222377 0
[pid=32646] vsize: 890156
Current children cumulated CPU time (s) 648.48
Current children cumulated vsize (Kb) 892284

[startup+670.071 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32668
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) R 32641 32641 9102 0 -1 0 269456 0 22 0 64745 1064 0 0 21 0 1 0 1854950025 922611712 224476 4294967295 134512640 135167914 3221224448 3221111776 134849260 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32646/statm): 225247 224476 162 162 0 225085 0
[pid=32646] vsize: 900988
Current children cumulated CPU time (s) 658.13
Current children cumulated vsize (Kb) 903116

[startup+680.072 s]
Raw data (loadavg): 1.00 0.98 0.95 2/58 32670
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) T 32641 32641 9102 0 -1 0 272728 0 171 0 65538 1078 0 0 23 0 1 0 1854950025 932712448 226423 4294967295 134512640 135167914 3221224448 3221088572 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/32646/statm): 227713 226423 162 162 0 227551 0
[pid=32646] vsize: 910852
Current children cumulated CPU time (s) 666.2
Current children cumulated vsize (Kb) 912980



Mem limit exceeded: sending SIGTERM then SIGKILL

[startup+688.821 s]
Raw data (loadavg): 1.00 0.98 0.95 1/58 32670
Raw data (/proc/32641/stat): 32641 (minisat+_script) S 32640 32641 9102 0 -1 0 314 332 0 0 0 0 2 2 20 0 1 0 1854950015 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32641/statm): 532 234 485 147 0 385 0
[pid=32641] vsize: 2128
Raw data (/proc/32646/stat): 32646 (minisat+_bignum) T 32641 32641 9102 0 -1 0 274969 0 203 0 66341 1090 0 0 25 0 1 0 1854950025 941543424 224763 4294967295 134512640 135167914 3221224448 3221087548 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/32646/statm): 229869 224763 162 162 0 229707 0
[pid=32646] vsize: 919476
Current children cumulated CPU time (s) 674.35
Current children cumulated vsize (Kb) 921604

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

Child status: 0
Real time (s): 689.28
CPU time (s): 674.742
CPU user time (s): 663.41
CPU system time (s): 11.3323
CPU usage (%): 97.8909
Max. virtual memory (cumulated for all children) (Kb): 921604