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/16029/stat): 16029 (minisat+_script) R 16028 16029 16528 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1854740105 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/16029/statm): 174 3 169 147 0 27 0
[pid=16029] 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=16030
New process pid=16031
New process pid=16032
execve syscall for /bin/sed executable
One traced child (pid=16031) 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=16032) exited with status: 0
One traced child (pid=16030) exited with status: 0
New process pid=16033
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-biella1.opb
One traced child (pid=16033) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=16034
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-biella1.opb

[startup+10.0039 s]
Raw data (loadavg): 0.94 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 4354 0 0 0 941 23 0 0 25 0 1 0 1854740119 17813504 3868 4294967295 134512640 135167914 3221224448 3221222384 134845911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16034/statm): 4349 3868 162 162 0 4187 0
[pid=16034] vsize: 17396
Current children cumulated CPU time (s) 9.7
Current children cumulated vsize (Kb) 19524

[startup+20.0056 s]
Raw data (loadavg): 0.95 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 6903 0 0 0 1916 36 0 0 25 0 1 0 1854740119 24416256 5437 4294967295 134512640 135167914 3221224448 3221221808 134693582 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16034/statm): 5961 5437 162 162 0 5799 0
[pid=16034] vsize: 23844
Current children cumulated CPU time (s) 19.58
Current children cumulated vsize (Kb) 25972

[startup+30.0063 s]
Raw data (loadavg): 0.95 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 7710 0 0 0 2911 39 0 0 25 0 1 0 1854740119 28884992 6244 4294967295 134512640 135167914 3221224448 3221223004 134845882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16034/statm): 7052 6244 162 162 0 6890 0
[pid=16034] vsize: 28208
Current children cumulated CPU time (s) 29.56
Current children cumulated vsize (Kb) 30336

[startup+40.007 s]
Raw data (loadavg): 0.96 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 8889 0 0 0 3905 43 0 0 25 0 1 0 1854740119 31592448 7093 4294967295 134512640 135167914 3221224448 3221222856 134722513 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 7713 7093 162 162 0 7551 0
[pid=16034] vsize: 30852
Current children cumulated CPU time (s) 39.54
Current children cumulated vsize (Kb) 32980

[startup+50.0077 s]
Raw data (loadavg): 0.97 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 9884 0 0 0 4895 47 0 0 25 0 1 0 1854740119 37429248 8088 4294967295 134512640 135167914 3221224448 3221221056 134693563 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 9138 8088 162 162 0 8976 0
[pid=16034] vsize: 36552
Current children cumulated CPU time (s) 49.48
Current children cumulated vsize (Kb) 38680

[startup+60.0084 s]
Raw data (loadavg): 0.97 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 11835 0 0 0 5888 51 0 0 25 0 1 0 1854740119 41762816 9380 4294967295 134512640 135167914 3221224448 3221221048 134723211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16034/statm): 10196 9380 162 162 0 10034 0
[pid=16034] vsize: 40784
Current children cumulated CPU time (s) 59.45
Current children cumulated vsize (Kb) 42912

[startup+70.01 s]
Raw data (loadavg): 0.97 0.98 0.99 1/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) T 16029 16029 16528 0 -1 0 12900 0 0 0 6879 56 0 0 25 0 1 0 1854740119 50802688 10445 4294967295 134512640 135167914 3221224448 3221219388 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/16034/statm): 12403 10445 162 162 0 12241 0
[pid=16034] vsize: 49612
Current children cumulated CPU time (s) 69.41
Current children cumulated vsize (Kb) 51740

[startup+80.0107 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 13788 0 0 0 7870 61 0 0 25 0 1 0 1854740119 53108736 11333 4294967295 134512640 135167914 3221224448 3221221536 134845911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 12966 11333 162 162 0 12804 0
[pid=16034] vsize: 51864
Current children cumulated CPU time (s) 79.37
Current children cumulated vsize (Kb) 53992

[startup+90.0104 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) T 16029 16029 16528 0 -1 0 20299 0 0 0 8834 84 0 0 25 0 1 0 1854740119 72339456 16273 4294967295 134512640 135167914 3221224448 3215682252 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/16034/statm): 17661 16273 162 162 0 17499 0
[pid=16034] vsize: 70644
Current children cumulated CPU time (s) 89.24
Current children cumulated vsize (Kb) 72772

[startup+100.011 s]
Raw data (loadavg): 0.98 0.98 0.99 1/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) T 16029 16029 16528 0 -1 0 27075 0 0 0 9773 113 0 0 25 0 1 0 1854740119 94298112 22471 4294967295 134512640 135167914 3221224448 3216053820 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/16034/statm): 23022 22471 162 162 0 22860 0
[pid=16034] vsize: 92088
Current children cumulated CPU time (s) 98.92
Current children cumulated vsize (Kb) 94216

[startup+110.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) T 16029 16029 16528 0 -1 0 33298 0 0 0 10717 141 0 0 25 0 1 0 1854740119 127258624 28035 4294967295 134512640 135167914 3221224448 3216175676 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/16034/statm): 31069 28035 162 162 0 30907 0
[pid=16034] vsize: 124276
Current children cumulated CPU time (s) 108.64
Current children cumulated vsize (Kb) 126404

[startup+120.013 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 45734 0 0 0 11653 179 0 0 25 0 1 0 1854740119 159379456 36516 4294967295 134512640 135167914 3221224448 3216010516 134849147 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16034/statm): 38911 36516 162 162 0 38749 0
[pid=16034] vsize: 155644
Current children cumulated CPU time (s) 118.38
Current children cumulated vsize (Kb) 157772

[startup+130.014 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 12613 196 0 0 25 0 1 0 1854740119 174440448 40522 4294967295 134512640 135167914 3221224448 3221223184 134849099 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 42588 40522 162 162 0 42426 0
[pid=16034] vsize: 170352
Current children cumulated CPU time (s) 128.15
Current children cumulated vsize (Kb) 172480

[startup+140.014 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 13613 196 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214512 134849148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 138.15
Current children cumulated vsize (Kb) 161932

[startup+150.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 14613 196 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214496 134845927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 148.15
Current children cumulated vsize (Kb) 161932

[startup+160.014 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 15613 196 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214400 134849102 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 158.15
Current children cumulated vsize (Kb) 161932

[startup+170.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 16613 196 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214592 134694351 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 168.15
Current children cumulated vsize (Kb) 161932

[startup+180.016 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 17613 197 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214928 134843160 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 178.16
Current children cumulated vsize (Kb) 161932

[startup+190.016 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 18613 197 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215200 134845930 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 188.16
Current children cumulated vsize (Kb) 161932

[startup+200.017 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 19614 197 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214528 134696194 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 198.17
Current children cumulated vsize (Kb) 161932

[startup+210.017 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 20614 197 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214576 134694517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 208.17
Current children cumulated vsize (Kb) 161932

[startup+220.017 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 21614 197 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214768 134849187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 218.17
Current children cumulated vsize (Kb) 161932

[startup+230.018 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 22614 197 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214992 134844697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 228.17
Current children cumulated vsize (Kb) 161932

[startup+240.018 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 23614 197 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215040 134844736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 238.17
Current children cumulated vsize (Kb) 161932

[startup+250.018 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 24615 197 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215104 134843010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 248.18
Current children cumulated vsize (Kb) 161932

[startup+260.019 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 25615 197 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215280 134849179 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 258.18
Current children cumulated vsize (Kb) 161932

[startup+270.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 26615 197 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215040 134845895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 268.18
Current children cumulated vsize (Kb) 161932

[startup+280.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 27615 197 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215104 134849187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 278.18
Current children cumulated vsize (Kb) 161932

[startup+290.021 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 28614 199 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214768 134693582 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 288.19
Current children cumulated vsize (Kb) 161932

[startup+300.022 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 29614 199 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214672 134845927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 298.19
Current children cumulated vsize (Kb) 161932

[startup+310.022 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 30614 199 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214956 134522320 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 308.19
Current children cumulated vsize (Kb) 161932

[startup+320.023 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 31613 200 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215488 134629290 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 318.19
Current children cumulated vsize (Kb) 161932

[startup+330.024 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 32613 200 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214884 134843000 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 328.19
Current children cumulated vsize (Kb) 161932

[startup+340.024 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 33613 200 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215152 134844647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 338.19
Current children cumulated vsize (Kb) 161932

[startup+350.024 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 34613 201 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214760 134722513 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 348.2
Current children cumulated vsize (Kb) 161932

[startup+360.025 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 35613 201 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214496 134845903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 358.2
Current children cumulated vsize (Kb) 161932

[startup+370.026 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 36613 201 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214736 134522338 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 368.2
Current children cumulated vsize (Kb) 161932

[startup+380.026 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 37614 201 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214576 134694428 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 378.21
Current children cumulated vsize (Kb) 161932

[startup+390.026 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 38614 201 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214800 134630866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 388.21
Current children cumulated vsize (Kb) 161932

[startup+400.027 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 39614 201 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215424 134849179 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 398.21
Current children cumulated vsize (Kb) 161932

[startup+410.027 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 40614 201 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214576 134694517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 408.21
Current children cumulated vsize (Kb) 161932

[startup+420.028 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 41614 201 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215112 134722513 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 418.21
Current children cumulated vsize (Kb) 161932

[startup+430.029 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 42614 202 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214944 134693570 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 428.22
Current children cumulated vsize (Kb) 161932

[startup+440.028 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 43614 202 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215312 134630912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 438.22
Current children cumulated vsize (Kb) 161932

[startup+450.029 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 44614 202 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215052 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 448.22
Current children cumulated vsize (Kb) 161932

[startup+460.03 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 45615 202 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215312 134629153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 458.23
Current children cumulated vsize (Kb) 161932

[startup+470.031 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 46615 202 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214784 134629373 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 468.23
Current children cumulated vsize (Kb) 161932

[startup+480.032 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 47615 202 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214700 134843002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 478.23
Current children cumulated vsize (Kb) 161932

[startup+490.032 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 48615 202 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214576 134849102 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 488.23
Current children cumulated vsize (Kb) 161932

[startup+500.033 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 49615 202 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215292 134722512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 498.23
Current children cumulated vsize (Kb) 161932

[startup+510.032 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 50615 202 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214816 134845280 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 508.23
Current children cumulated vsize (Kb) 161932

[startup+520.033 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 51615 203 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215004 134844638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 518.24
Current children cumulated vsize (Kb) 161932

[startup+530.034 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 52616 203 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214900 134845880 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 528.25
Current children cumulated vsize (Kb) 161932

[startup+540.034 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 53616 203 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215020 134844638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 538.25
Current children cumulated vsize (Kb) 161932

[startup+550.035 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 54616 203 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214544 134720503 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 548.25
Current children cumulated vsize (Kb) 161932

[startup+560.036 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 55616 203 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215224 134693662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 558.25
Current children cumulated vsize (Kb) 161932

[startup+570.036 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 56616 203 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214960 134628798 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 568.25
Current children cumulated vsize (Kb) 161932

[startup+580.037 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 57616 203 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215120 134849179 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 578.25
Current children cumulated vsize (Kb) 161932

[startup+590.038 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 58616 203 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215084 134844632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 588.25
Current children cumulated vsize (Kb) 161932

[startup+600.038 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 59617 203 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215392 134843107 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 598.26
Current children cumulated vsize (Kb) 161932

[startup+610.039 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 60617 203 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214844 134844675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 608.26
Current children cumulated vsize (Kb) 161932

[startup+620.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 61617 203 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215552 134845888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 618.26
Current children cumulated vsize (Kb) 161932

[startup+630.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 62617 203 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214752 134694524 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 628.26
Current children cumulated vsize (Kb) 161932

[startup+640.041 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 63617 203 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214876 134723267 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 638.26
Current children cumulated vsize (Kb) 161932

[startup+650.042 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 64618 203 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214420 134843000 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 648.27
Current children cumulated vsize (Kb) 161932

[startup+660.043 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 65618 203 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214952 134693553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 658.27
Current children cumulated vsize (Kb) 161932

[startup+670.043 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 66618 203 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214768 134849061 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 668.27
Current children cumulated vsize (Kb) 161932

[startup+680.044 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 67618 203 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215040 134845933 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 678.27
Current children cumulated vsize (Kb) 161932

[startup+690.044 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 68618 203 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214592 134849193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 688.27
Current children cumulated vsize (Kb) 161932

[startup+700.044 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 69618 204 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214400 134694545 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 698.28
Current children cumulated vsize (Kb) 161932

[startup+710.045 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 70619 204 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215136 134629096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 708.29
Current children cumulated vsize (Kb) 161932

[startup+720.046 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 71619 204 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214864 134844676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 718.29
Current children cumulated vsize (Kb) 161932

[startup+730.046 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 72619 204 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214768 134849187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 728.29
Current children cumulated vsize (Kb) 161932

[startup+740.046 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 73619 204 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215768 134849057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 738.29
Current children cumulated vsize (Kb) 161932

[startup+750.047 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 74619 204 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214848 134845903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 748.29
Current children cumulated vsize (Kb) 161932

[startup+760.047 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 75620 204 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214700 134723236 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 758.3
Current children cumulated vsize (Kb) 161932

[startup+770.049 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 76620 204 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214548 134845938 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 768.3
Current children cumulated vsize (Kb) 161932

[startup+780.05 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 77620 204 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214960 134629069 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 778.3
Current children cumulated vsize (Kb) 161932

[startup+790.049 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 78620 204 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214604 134849088 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 788.3
Current children cumulated vsize (Kb) 161932

[startup+800.05 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 79620 204 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215452 134722512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 798.3
Current children cumulated vsize (Kb) 161932

[startup+810.051 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 80621 204 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214956 134843033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 808.31
Current children cumulated vsize (Kb) 161932

[startup+820.052 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 81621 204 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214592 134849163 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 818.31
Current children cumulated vsize (Kb) 161932

[startup+830.053 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 82621 204 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215696 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 828.31
Current children cumulated vsize (Kb) 161932

[startup+840.053 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 83621 204 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215040 134844668 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 838.31
Current children cumulated vsize (Kb) 161932

[startup+850.053 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 84622 204 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215104 134849092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 848.32
Current children cumulated vsize (Kb) 161932

[startup+860.054 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 85621 205 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215468 134849056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 858.32
Current children cumulated vsize (Kb) 161932

[startup+870.055 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 86622 205 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214896 134720495 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 868.33
Current children cumulated vsize (Kb) 161932

[startup+880.056 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 87622 205 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215216 134845933 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 878.33
Current children cumulated vsize (Kb) 161932

[startup+890.056 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 88621 206 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215344 134844676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 888.33
Current children cumulated vsize (Kb) 161932

[startup+900.057 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 89620 206 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215104 134849153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 898.32
Current children cumulated vsize (Kb) 161932

[startup+910.058 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 90620 207 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214608 134628763 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 908.33
Current children cumulated vsize (Kb) 161932

[startup+920.058 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 91620 207 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215080 134844633 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 918.33
Current children cumulated vsize (Kb) 161932

[startup+930.059 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 92620 208 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215024 134845921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 928.34
Current children cumulated vsize (Kb) 161932

[startup+940.059 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 93620 208 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214752 134849108 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 938.34
Current children cumulated vsize (Kb) 161932

[startup+950.059 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 94620 208 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215760 134843001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 948.34
Current children cumulated vsize (Kb) 161932

[startup+960.06 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 95620 208 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215184 134844637 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 958.34
Current children cumulated vsize (Kb) 161932

[startup+970.061 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 96620 208 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215056 134843402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 968.34
Current children cumulated vsize (Kb) 161932

[startup+980.061 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 97620 208 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215344 134844703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 978.34
Current children cumulated vsize (Kb) 161932

[startup+990.062 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 98621 208 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215408 134696578 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 988.35
Current children cumulated vsize (Kb) 161932

[startup+1000.06 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 99621 209 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221216324 134845880 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 998.36
Current children cumulated vsize (Kb) 161932

[startup+1010.06 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 100621 209 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215600 134843001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 1008.36
Current children cumulated vsize (Kb) 161932

[startup+1020.06 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 101621 209 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215480 134693815 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 1018.36
Current children cumulated vsize (Kb) 161932

[startup+1030.06 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 102621 209 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215184 134844672 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 1028.36
Current children cumulated vsize (Kb) 161932

[startup+1040.06 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 103621 209 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215504 134844715 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 1038.36
Current children cumulated vsize (Kb) 161932

[startup+1050.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 104621 209 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215760 134843402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 1048.36
Current children cumulated vsize (Kb) 161932

[startup+1060.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 105622 209 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215120 134849196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 1058.37
Current children cumulated vsize (Kb) 161932

[startup+1070.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 106621 210 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215648 134849110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 1068.37
Current children cumulated vsize (Kb) 161932

[startup+1080.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 107621 210 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221216124 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 1078.37
Current children cumulated vsize (Kb) 161932

[startup+1090.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 108622 210 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215760 134849153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 1088.38
Current children cumulated vsize (Kb) 161932

[startup+1100.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 109622 210 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215436 134844632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 1098.38
Current children cumulated vsize (Kb) 161932

[startup+1110.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 110622 210 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215456 134849196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 1108.38
Current children cumulated vsize (Kb) 161932

[startup+1120.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 111622 210 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215644 134722512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 1118.38
Current children cumulated vsize (Kb) 161932

[startup+1130.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 112622 210 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221214944 134849066 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 1128.38
Current children cumulated vsize (Kb) 161932

[startup+1140.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 113622 210 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215620 134849147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 1138.38
Current children cumulated vsize (Kb) 161932

[startup+1150.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 114622 210 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215552 134718501 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 1148.38
Current children cumulated vsize (Kb) 161932

[startup+1160.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 115623 210 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215328 134628744 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 1158.39
Current children cumulated vsize (Kb) 161932

[startup+1170.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 116622 210 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215136 134629270 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 1168.38
Current children cumulated vsize (Kb) 161932

[startup+1180.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 117623 210 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215772 134842996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 1178.39
Current children cumulated vsize (Kb) 161932

[startup+1190.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 118623 210 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215152 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 1188.39
Current children cumulated vsize (Kb) 161932

[startup+1200.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 119623 210 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221215824 134849143 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 1198.39
Current children cumulated vsize (Kb) 161932

[startup+1210.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 120623 210 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221217152 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 1208.39
Current children cumulated vsize (Kb) 161932



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16034
Raw data (/proc/16029/stat): 16029 (minisat+_script) S 16028 16029 16528 0 -1 0 314 553 0 0 0 0 4 2 18 0 1 0 1854740105 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16029/statm): 532 234 485 147 0 385 0
[pid=16029] vsize: 2128
Raw data (/proc/16034/stat): 16034 (minisat+_bignum) R 16029 16029 16528 0 -1 0 49740 0 0 0 120624 210 0 0 25 0 1 0 1854740119 163639296 37885 4294967295 134512640 135167914 3221224448 3221217152 134845921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16034/statm): 39951 37885 162 162 0 39789 0
[pid=16034] vsize: 159804
Current children cumulated CPU time (s) 1208.4
Current children cumulated vsize (Kb) 161932

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

Child status: 0
Real time (s): 1210.15
CPU time (s): 1208.42
CPU user time (s): 1206.24
CPU system time (s): 2.18067
CPU usage (%): 99.8575
Max. virtual memory (cumulated for all children) (Kb): 172480