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/31705/stat): 31705 (minisat+_script) R 31704 31705 9102 0 -1 0 19 0 0 0 0 0 0 0 18 0 1 0 1854520735 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/31705/statm): 174 3 169 147 0 27 0
[pid=31705] 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=31706
New process pid=31707
New process pid=31708
execve syscall for /bin/sed executable
One traced child (pid=31707) 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=31708) exited with status: 0
One traced child (pid=31706) exited with status: 0
New process pid=31709
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-20-10-fome11.opb
One traced child (pid=31709) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=31710
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-20-10-fome11.opb

[startup+10.6966 s]
Raw data (loadavg): 0.81 0.89 0.95 2/58 31710
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 11615 0 0 0 833 54 0 0 25 0 1 0 1854520857 64782336 10981 4294967295 134512640 135167914 3221224448 3221223268 134697173 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 15816 10981 162 162 0 15654 0
[pid=31710] vsize: 63264
Current children cumulated CPU time (s) 8.94
Current children cumulated vsize (Kb) 65392

[startup+20.6976 s]
Raw data (loadavg): 0.84 0.90 0.95 2/58 31710
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 20546 0 0 0 1757 94 0 0 25 0 1 0 1854520857 87232512 18438 4294967295 134512640 135167914 3221224448 3221222744 134846995 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 21297 18438 162 162 0 21135 0
[pid=31710] vsize: 85188
Current children cumulated CPU time (s) 18.58
Current children cumulated vsize (Kb) 87316

[startup+30.6985 s]
Raw data (loadavg): 0.87 0.90 0.95 2/58 31710
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 22327 0 0 0 2736 105 0 0 25 0 1 0 1854520857 92901376 20219 4294967295 134512640 135167914 3221224448 3221223024 134844975 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 22681 20219 162 162 0 22519 0
[pid=31710] vsize: 90724
Current children cumulated CPU time (s) 28.48
Current children cumulated vsize (Kb) 92852

[startup+40.7004 s]
Raw data (loadavg): 0.89 0.90 0.95 2/58 31710
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 24908 0 0 0 3706 119 0 0 25 0 1 0 1854520857 101957632 22800 4294967295 134512640 135167914 3221224448 3221222768 134843160 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 24892 22800 162 162 0 24730 0
[pid=31710] vsize: 99568
Current children cumulated CPU time (s) 38.32
Current children cumulated vsize (Kb) 101696

[startup+50.7014 s]
Raw data (loadavg): 0.90 0.91 0.95 2/58 31712
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 28253 0 0 0 4664 139 0 0 25 0 1 0 1854520857 113553408 26014 4294967295 134512640 135167914 3221224448 3221222784 134845913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 27723 26014 162 162 0 27561 0
[pid=31710] vsize: 110892
Current children cumulated CPU time (s) 48.1
Current children cumulated vsize (Kb) 113020

[startup+60.7023 s]
Raw data (loadavg): 0.92 0.91 0.95 2/58 31712
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 31920 0 0 0 5619 159 0 0 25 0 1 0 1854520857 124801024 28978 4294967295 134512640 135167914 3221224448 3221222232 134843032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 30469 28978 162 162 0 30307 0
[pid=31710] vsize: 121876
Current children cumulated CPU time (s) 57.85
Current children cumulated vsize (Kb) 124004

[startup+70.7032 s]
Raw data (loadavg): 0.93 0.91 0.95 2/58 31712
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 35038 0 0 0 6579 176 0 0 25 0 1 0 1854520857 136577024 32096 4294967295 134512640 135167914 3221224448 3221220060 134844638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 33344 32096 162 162 0 33182 0
[pid=31710] vsize: 133376
Current children cumulated CPU time (s) 67.62
Current children cumulated vsize (Kb) 135504

[startup+80.7041 s]
Raw data (loadavg): 0.94 0.91 0.95 2/58 31712
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 37899 0 0 0 7544 192 0 0 25 0 1 0 1854520857 147238912 34915 4294967295 134512640 135167914 3221224448 3221222720 134610320 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31710/statm): 35947 34915 162 162 0 35785 0
[pid=31710] vsize: 143788
Current children cumulated CPU time (s) 77.43
Current children cumulated vsize (Kb) 145916

[startup+90.7051 s]
Raw data (loadavg): 0.95 0.92 0.95 2/58 31712
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 40813 0 0 0 8503 212 0 0 25 0 1 0 1854520857 195678208 37829 4294967295 134512640 135167914 3221224448 3221223360 134572232 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 47773 37829 162 162 0 47611 0
[pid=31710] vsize: 191092
Current children cumulated CPU time (s) 87.22
Current children cumulated vsize (Kb) 193220

[startup+100.706 s]
Raw data (loadavg): 0.96 0.92 0.95 2/58 31712
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 43616 0 0 0 9466 229 0 0 25 0 1 0 1854520857 206544896 40632 4294967295 134512640 135167914 3221224448 3221222544 134844733 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 50426 40632 162 162 0 50264 0
[pid=31710] vsize: 201704
Current children cumulated CPU time (s) 97.02
Current children cumulated vsize (Kb) 203832

[startup+110.709 s]
Raw data (loadavg): 0.96 0.92 0.95 2/58 31714
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 46437 0 0 0 10430 245 0 0 25 0 1 0 1854520857 217608192 43453 4294967295 134512640 135167914 3221224448 3221222764 134722512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31710/statm): 53127 43453 162 162 0 52965 0
[pid=31710] vsize: 212508
Current children cumulated CPU time (s) 106.82
Current children cumulated vsize (Kb) 214636

[startup+120.71 s]
Raw data (loadavg): 0.97 0.92 0.95 2/58 31714
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 49250 0 0 0 11389 263 0 0 25 0 1 0 1854520857 228093952 46080 4294967295 134512640 135167914 3221224448 3221222080 134610758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 55687 46080 162 162 0 55525 0
[pid=31710] vsize: 222748
Current children cumulated CPU time (s) 116.59
Current children cumulated vsize (Kb) 224876

[startup+130.71 s]
Raw data (loadavg): 0.97 0.92 0.95 2/58 31714
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 52615 0 0 0 12348 280 0 0 25 0 1 0 1854520857 239382528 49176 4294967295 134512640 135167914 3221224448 3221223200 134844725 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 58443 49176 162 162 0 58281 0
[pid=31710] vsize: 233772
Current children cumulated CPU time (s) 126.35
Current children cumulated vsize (Kb) 235900

[startup+140.711 s]
Raw data (loadavg): 0.98 0.93 0.95 2/58 31714
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 55895 0 0 0 13312 297 0 0 25 0 1 0 1854520857 250753024 52393 4294967295 134512640 135167914 3221224448 3221221248 134845924 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 61219 52393 162 162 0 61057 0
[pid=31710] vsize: 244876
Current children cumulated CPU time (s) 136.16
Current children cumulated vsize (Kb) 247004

[startup+150.712 s]
Raw data (loadavg): 0.98 0.93 0.95 2/58 31714
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 59228 0 0 0 14275 313 0 0 25 0 1 0 1854520857 262406144 55643 4294967295 134512640 135167914 3221224448 3221221308 134845940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 64064 55643 162 162 0 63902 0
[pid=31710] vsize: 256256
Current children cumulated CPU time (s) 145.95
Current children cumulated vsize (Kb) 258384

[startup+160.713 s]
Raw data (loadavg): 0.98 0.93 0.95 2/58 31714
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 62557 0 0 0 15236 331 0 0 25 0 1 0 1854520857 273956864 58841 4294967295 134512640 135167914 3221224448 3221223152 134722532 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 66884 58841 162 162 0 66722 0
[pid=31710] vsize: 267536
Current children cumulated CPU time (s) 155.74
Current children cumulated vsize (Kb) 269664

[startup+170.714 s]
Raw data (loadavg): 0.98 0.93 0.95 2/58 31716
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 66220 0 0 0 16193 349 0 0 25 0 1 0 1854520857 285257728 61801 4294967295 134512640 135167914 3221224448 3221221456 134843130 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 69643 61801 162 162 0 69481 0
[pid=31710] vsize: 278572
Current children cumulated CPU time (s) 165.49
Current children cumulated vsize (Kb) 280700

[startup+180.713 s]
Raw data (loadavg): 0.99 0.93 0.95 2/58 31716
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 71700 0 0 0 17152 371 0 0 25 0 1 0 1854520857 301359104 65963 4294967295 134512640 135167914 3221224448 3221223200 134844718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 73574 65963 162 162 0 73412 0
[pid=31710] vsize: 294296
Current children cumulated CPU time (s) 175.3
Current children cumulated vsize (Kb) 296424

[startup+190.715 s]
Raw data (loadavg): 0.99 0.93 0.95 2/58 31716
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 74706 0 0 0 18116 388 0 0 25 0 1 0 1854520857 312504320 68891 4294967295 134512640 135167914 3221224448 3221221344 134516622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 76295 68891 162 162 0 76133 0
[pid=31710] vsize: 305180
Current children cumulated CPU time (s) 185.11
Current children cumulated vsize (Kb) 307308

[startup+200.716 s]
Raw data (loadavg): 0.99 0.94 0.95 2/58 31716
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 77649 0 0 0 19077 407 0 0 25 0 1 0 1854520857 323444736 71749 4294967295 134512640 135167914 3221224448 3221223248 134849153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 78966 71749 162 162 0 78804 0
[pid=31710] vsize: 315864
Current children cumulated CPU time (s) 194.91
Current children cumulated vsize (Kb) 317992

[startup+210.717 s]
Raw data (loadavg): 0.99 0.94 0.95 2/58 31716
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 80472 0 0 0 20039 425 0 0 25 0 1 0 1854520857 334426112 74572 4294967295 134512640 135167914 3221224448 3221222060 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 81647 74572 162 162 0 81485 0
[pid=31710] vsize: 326588
Current children cumulated CPU time (s) 204.71
Current children cumulated vsize (Kb) 328716

[startup+220.718 s]
Raw data (loadavg): 0.99 0.94 0.95 2/58 31716
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 83305 0 0 0 20999 443 0 0 25 0 1 0 1854520857 345501696 77405 4294967295 134512640 135167914 3221224448 3221222808 134693626 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 84351 77405 162 162 0 84189 0
[pid=31710] vsize: 337404
Current children cumulated CPU time (s) 214.49
Current children cumulated vsize (Kb) 339532

[startup+230.718 s]
Raw data (loadavg): 0.99 0.94 0.95 2/58 31718
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 86125 0 0 0 21956 463 0 0 25 0 1 0 1854520857 356020224 80040 4294967295 134512640 135167914 3221224448 3221222748 134849253 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 86919 80040 162 162 0 86757 0
[pid=31710] vsize: 347676
Current children cumulated CPU time (s) 224.26
Current children cumulated vsize (Kb) 349804

[startup+240.719 s]
Raw data (loadavg): 0.99 0.94 0.95 2/58 31718
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 97227 0 0 0 22877 502 0 0 25 0 1 0 1854520857 401424384 91142 4294967295 134512640 135167914 3221224448 3221223192 134693709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 98004 91142 162 162 0 97842 0
[pid=31710] vsize: 392016
Current children cumulated CPU time (s) 233.86
Current children cumulated vsize (Kb) 394144

[startup+250.72 s]
Raw data (loadavg): 0.99 0.94 0.95 2/58 31718
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 97230 0 0 0 23877 503 0 0 25 0 1 0 1854520857 401428480 91145 4294967295 134512640 135167914 3221224448 3221223216 134691382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 98005 91145 162 162 0 97843 0
[pid=31710] vsize: 392020
Current children cumulated CPU time (s) 243.87
Current children cumulated vsize (Kb) 394148

[startup+260.722 s]
Raw data (loadavg): 0.99 0.95 0.95 2/58 31718
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 97231 0 0 0 24876 503 0 0 25 0 1 0 1854520857 401428480 91146 4294967295 134512640 135167914 3221224448 3221223212 134697191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 98005 91146 162 162 0 97843 0
[pid=31710] vsize: 392020
Current children cumulated CPU time (s) 253.86
Current children cumulated vsize (Kb) 394148

[startup+270.723 s]
Raw data (loadavg): 0.99 0.95 0.95 2/58 31718
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 97232 0 0 0 25876 503 0 0 25 0 1 0 1854520857 401428480 91147 4294967295 134512640 135167914 3221224448 3221223216 134691231 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 98005 91147 162 162 0 97843 0
[pid=31710] vsize: 392020
Current children cumulated CPU time (s) 263.86
Current children cumulated vsize (Kb) 394148

[startup+280.724 s]
Raw data (loadavg): 0.99 0.95 0.95 2/58 31718
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 97236 0 0 0 26876 504 0 0 25 0 1 0 1854520857 401432576 91151 4294967295 134512640 135167914 3221224448 3221223204 134697187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 98006 91151 162 162 0 97844 0
[pid=31710] vsize: 392024
Current children cumulated CPU time (s) 273.87
Current children cumulated vsize (Kb) 394152

[startup+290.725 s]
Raw data (loadavg): 0.99 0.95 0.95 2/58 31720
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 97238 0 0 0 27875 504 0 0 25 0 1 0 1854520857 401432576 91153 4294967295 134512640 135167914 3221224448 3221223204 134697076 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 98006 91153 162 162 0 97844 0
[pid=31710] vsize: 392024
Current children cumulated CPU time (s) 283.86
Current children cumulated vsize (Kb) 394152

[startup+300.726 s]
Raw data (loadavg): 0.99 0.95 0.95 2/58 31720
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 97241 0 0 0 28875 505 0 0 25 0 1 0 1854520857 401436672 91156 4294967295 134512640 135167914 3221224448 3221223212 134697040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 98007 91156 162 162 0 97845 0
[pid=31710] vsize: 392028
Current children cumulated CPU time (s) 293.87
Current children cumulated vsize (Kb) 394156

[startup+310.728 s]
Raw data (loadavg): 0.99 0.95 0.95 2/58 31720
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 97242 0 0 0 29874 505 0 0 25 0 1 0 1854520857 401436672 91157 4294967295 134512640 135167914 3221224448 3221223216 134691366 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 98007 91157 162 162 0 97845 0
[pid=31710] vsize: 392028
Current children cumulated CPU time (s) 303.86
Current children cumulated vsize (Kb) 394156

[startup+320.729 s]
Raw data (loadavg): 0.99 0.95 0.95 2/58 31720
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 97245 0 0 0 30874 505 0 0 25 0 1 0 1854520857 401436672 91160 4294967295 134512640 135167914 3221224448 3221223256 134722657 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 98007 91160 162 162 0 97845 0
[pid=31710] vsize: 392028
Current children cumulated CPU time (s) 313.86
Current children cumulated vsize (Kb) 394156

[startup+330.729 s]
Raw data (loadavg): 0.99 0.95 0.95 2/58 31720
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 97251 0 0 0 31873 506 0 0 25 0 1 0 1854520857 401440768 91166 4294967295 134512640 135167914 3221224448 3221223216 134691307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 98008 91166 162 162 0 97846 0
[pid=31710] vsize: 392032
Current children cumulated CPU time (s) 323.86
Current children cumulated vsize (Kb) 394160

[startup+340.73 s]
Raw data (loadavg): 0.99 0.95 0.95 2/58 31720
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 97266 0 0 0 32873 506 0 0 25 0 1 0 1854520857 401453056 91181 4294967295 134512640 135167914 3221224448 3221223296 134594194 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 98011 91181 162 162 0 97849 0
[pid=31710] vsize: 392044
Current children cumulated CPU time (s) 333.86
Current children cumulated vsize (Kb) 394172

[startup+350.731 s]
Raw data (loadavg): 0.99 0.95 0.95 2/58 31722
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 97284 0 0 0 33871 508 0 0 25 0 1 0 1854520857 383873024 86901 4294967295 134512640 135167914 3221224448 3221223132 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 93719 86901 162 162 0 93557 0
[pid=31710] vsize: 374876
Current children cumulated CPU time (s) 343.86
Current children cumulated vsize (Kb) 377004

[startup+360.733 s]
Raw data (loadavg): 0.99 0.95 0.95 2/58 31722
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 97329 0 0 0 34870 508 0 0 25 0 1 0 1854520857 383995904 86946 4294967295 134512640 135167914 3221224448 3221222608 134845901 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 93749 86946 162 162 0 93587 0
[pid=31710] vsize: 374996
Current children cumulated CPU time (s) 353.85
Current children cumulated vsize (Kb) 377124

[startup+370.735 s]
Raw data (loadavg): 0.99 0.96 0.95 2/58 31722
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 97340 0 0 0 35871 508 0 0 25 0 1 0 1854520857 384040960 86957 4294967295 134512640 135167914 3221224448 3221060348 134693600 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31710/statm): 93760 86957 162 162 0 93598 0
[pid=31710] vsize: 375040
Current children cumulated CPU time (s) 363.86
Current children cumulated vsize (Kb) 377168

[startup+380.735 s]
Raw data (loadavg): 0.99 0.96 0.95 2/58 31722
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 97340 0 0 0 36871 508 0 0 25 0 1 0 1854520857 384040960 86957 4294967295 134512640 135167914 3221224448 3221058464 134844708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31710/statm): 93760 86957 162 162 0 93598 0
[pid=31710] vsize: 375040
Current children cumulated CPU time (s) 373.86
Current children cumulated vsize (Kb) 377168

[startup+390.736 s]
Raw data (loadavg): 0.99 0.96 0.95 2/58 31722
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 99336 0 0 0 37861 514 0 0 25 0 1 0 1854520857 392216576 88953 4294967295 134512640 135167914 3221224448 3221064928 134845219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31710/statm): 95756 88953 162 162 0 95594 0
[pid=31710] vsize: 383024
Current children cumulated CPU time (s) 383.82
Current children cumulated vsize (Kb) 385152

[startup+400.737 s]
Raw data (loadavg): 0.99 0.96 0.95 2/58 31722
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 101495 0 0 0 38838 525 0 0 25 0 1 0 1854520857 401059840 91112 4294967295 134512640 135167914 3221224448 3221074560 134845090 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31710/statm): 97915 91112 162 162 0 97753 0
[pid=31710] vsize: 391660
Current children cumulated CPU time (s) 393.7
Current children cumulated vsize (Kb) 393788

[startup+410.738 s]
Raw data (loadavg): 0.99 0.96 0.95 2/58 31724
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 106381 0 0 0 39808 541 0 0 25 0 1 0 1854520857 415674368 94680 4294967295 134512640 135167914 3221224448 3221062880 134620948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 101483 94680 162 162 0 101321 0
[pid=31710] vsize: 405932
Current children cumulated CPU time (s) 403.56
Current children cumulated vsize (Kb) 408060

[startup+420.739 s]
Raw data (loadavg): 0.99 0.96 0.95 1/58 31724
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) T 31705 31705 9102 0 -1 0 109043 0 0 0 40776 555 0 0 25 0 1 0 1854520857 426577920 97342 4294967295 134512640 135167914 3221224448 3221077148 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/31710/statm): 104145 97342 162 162 0 103983 0
[pid=31710] vsize: 416580
Current children cumulated CPU time (s) 413.38
Current children cumulated vsize (Kb) 418708

[startup+430.74 s]
Raw data (loadavg): 0.99 0.96 0.95 2/58 31724
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 111362 0 0 0 41745 567 0 0 25 0 1 0 1854520857 436076544 99661 4294967295 134512640 135167914 3221224448 3221077872 134694345 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 106464 99661 162 162 0 106302 0
[pid=31710] vsize: 425856
Current children cumulated CPU time (s) 423.19
Current children cumulated vsize (Kb) 427984

[startup+440.741 s]
Raw data (loadavg): 0.99 0.96 0.95 2/58 31724
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 113706 0 0 0 42718 578 0 0 25 0 1 0 1854520857 445677568 102005 4294967295 134512640 135167914 3221224448 3221059968 134620936 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 108808 102005 162 162 0 108646 0
[pid=31710] vsize: 435232
Current children cumulated CPU time (s) 433.03
Current children cumulated vsize (Kb) 437360

[startup+450.742 s]
Raw data (loadavg): 0.99 0.96 0.95 2/58 31724
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 120796 0 0 0 43683 599 0 0 25 0 1 0 1854520857 463917056 106458 4294967295 134512640 135167914 3221224448 3221076576 134845930 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31710/statm): 113261 106458 162 162 0 113099 0
[pid=31710] vsize: 453044
Current children cumulated CPU time (s) 442.89
Current children cumulated vsize (Kb) 455172

[startup+460.743 s]
Raw data (loadavg): 0.99 0.96 0.95 2/58 31724
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 123223 0 0 0 44657 610 0 0 25 0 1 0 1854520857 473858048 108885 4294967295 134512640 135167914 3221224448 3221069952 134845927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31710/statm): 115688 108885 162 162 0 115526 0
[pid=31710] vsize: 462752
Current children cumulated CPU time (s) 452.74
Current children cumulated vsize (Kb) 464880

[startup+470.743 s]
Raw data (loadavg): 0.99 0.97 0.95 2/58 31726
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 125588 0 0 0 45631 620 0 0 25 0 1 0 1854520857 483545088 111250 4294967295 134512640 135167914 3221224448 3221069680 134844700 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 118053 111250 162 162 0 117891 0
[pid=31710] vsize: 472212
Current children cumulated CPU time (s) 462.58
Current children cumulated vsize (Kb) 474340

[startup+480.743 s]
Raw data (loadavg): 0.99 0.97 0.95 2/58 31726
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 128524 0 0 0 46596 633 0 0 25 0 1 0 1854520857 495570944 114186 4294967295 134512640 135167914 3221224448 3221055456 134694439 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31710/statm): 120989 114186 162 162 0 120827 0
[pid=31710] vsize: 483956
Current children cumulated CPU time (s) 472.36
Current children cumulated vsize (Kb) 486084

[startup+490.744 s]
Raw data (loadavg): 0.99 0.97 0.95 1/58 31726
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) T 31705 31705 9102 0 -1 0 130822 0 0 0 47570 644 0 0 25 0 1 0 1854520857 504983552 116484 4294967295 134512640 135167914 3221224448 3221063164 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/31710/statm): 123287 116484 162 162 0 123125 0
[pid=31710] vsize: 493148
Current children cumulated CPU time (s) 482.21
Current children cumulated vsize (Kb) 495276

[startup+500.745 s]
Raw data (loadavg): 0.99 0.97 0.95 2/58 31726
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 133194 0 0 0 48540 656 0 0 25 0 1 0 1854520857 514699264 118856 4294967295 134512640 135167914 3221224448 3221058928 134844963 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31710/statm): 125659 118856 162 162 0 125497 0
[pid=31710] vsize: 502636
Current children cumulated CPU time (s) 492.03
Current children cumulated vsize (Kb) 504764

[startup+510.746 s]
Raw data (loadavg): 0.99 0.97 0.95 2/58 31726
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 135405 0 0 0 49516 667 0 0 25 0 1 0 1854520857 523755520 121067 4294967295 134512640 135167914 3221224448 3221064520 134844633 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31710/statm): 127870 121067 162 162 0 127708 0
[pid=31710] vsize: 511480
Current children cumulated CPU time (s) 501.9
Current children cumulated vsize (Kb) 513608

[startup+520.747 s]
Raw data (loadavg): 0.99 0.97 0.95 2/58 31726
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 147228 0 0 0 50478 697 0 0 22 0 1 0 1854520857 550584320 127617 4294967295 134512640 135167914 3221224448 3221062440 134846971 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 134420 127617 162 162 0 134258 0
[pid=31710] vsize: 537680
Current children cumulated CPU time (s) 511.82
Current children cumulated vsize (Kb) 539808

[startup+530.747 s]
Raw data (loadavg): 0.99 0.97 0.95 2/58 31728
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 149698 0 0 0 51452 708 0 0 25 0 1 0 1854520857 560701440 130087 4294967295 134512640 135167914 3221224448 3221056800 134844694 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 136890 130087 162 162 0 136728 0
[pid=31710] vsize: 547560
Current children cumulated CPU time (s) 521.67
Current children cumulated vsize (Kb) 549688

[startup+540.748 s]
Raw data (loadavg): 0.99 0.97 0.95 2/58 31728
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 152019 0 0 0 52425 719 0 0 25 0 1 0 1854520857 570208256 132408 4294967295 134512640 135167914 3221224448 3221065192 134844633 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 139211 132408 162 162 0 139049 0
[pid=31710] vsize: 556844
Current children cumulated CPU time (s) 531.51
Current children cumulated vsize (Kb) 558972

[startup+550.749 s]
Raw data (loadavg): 0.99 0.97 0.95 2/58 31728
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 154626 0 0 0 53395 732 0 0 25 0 1 0 1854520857 580886528 135015 4294967295 134512640 135167914 3221224448 3221068304 134843030 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 141818 135015 162 162 0 141656 0
[pid=31710] vsize: 567272
Current children cumulated CPU time (s) 541.34
Current children cumulated vsize (Kb) 569400

[startup+560.75 s]
Raw data (loadavg): 0.99 0.97 0.95 2/58 31728
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 157061 0 0 0 54369 743 0 0 25 0 1 0 1854520857 590860288 137450 4294967295 134512640 135167914 3221224448 3221066368 134844703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 144253 137450 162 162 0 144091 0
[pid=31710] vsize: 577012
Current children cumulated CPU time (s) 551.19
Current children cumulated vsize (Kb) 579140

[startup+570.751 s]
Raw data (loadavg): 0.99 0.97 0.95 2/58 31728
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 159293 0 0 0 55346 754 0 0 25 0 1 0 1854520857 600002560 139682 4294967295 134512640 135167914 3221224448 3221098160 134843123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 146485 139682 162 162 0 146323 0
[pid=31710] vsize: 585940
Current children cumulated CPU time (s) 561.07
Current children cumulated vsize (Kb) 588068

[startup+580.752 s]
Raw data (loadavg): 0.99 0.97 0.95 2/58 31728
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) T 31705 31705 9102 0 -1 0 162298 0 0 0 56312 767 0 0 25 0 1 0 1854520857 612311040 142687 4294967295 134512640 135167914 3221224448 3221076828 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/31710/statm): 149490 142687 162 162 0 149328 0
[pid=31710] vsize: 597960
Current children cumulated CPU time (s) 570.86
Current children cumulated vsize (Kb) 600088

[startup+590.753 s]
Raw data (loadavg): 0.99 0.97 0.95 2/58 31730
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 165163 0 0 0 57279 781 0 0 25 0 1 0 1854520857 624046080 145552 4294967295 134512640 135167914 3221224448 3221077200 134695738 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 152355 145552 162 162 0 152193 0
[pid=31710] vsize: 609420
Current children cumulated CPU time (s) 580.67
Current children cumulated vsize (Kb) 611548

[startup+600.754 s]
Raw data (loadavg): 0.99 0.97 0.95 2/58 31730
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 168010 0 0 0 58245 796 0 0 25 0 1 0 1854520857 635707392 148399 4294967295 134512640 135167914 3221224448 3221068652 134844675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 155202 148399 162 162 0 155040 0
[pid=31710] vsize: 620808
Current children cumulated CPU time (s) 590.48
Current children cumulated vsize (Kb) 622936

[startup+610.755 s]
Raw data (loadavg): 0.99 0.97 0.95 2/58 31730
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 170326 0 0 0 59215 809 0 0 25 0 1 0 1854520857 645193728 150715 4294967295 134512640 135167914 3221224448 3221065344 134619242 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 157518 150715 162 162 0 157356 0
[pid=31710] vsize: 630072
Current children cumulated CPU time (s) 600.31
Current children cumulated vsize (Kb) 632200

[startup+620.756 s]
Raw data (loadavg): 0.99 0.97 0.95 2/58 31730
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 172785 0 0 0 60188 820 0 0 25 0 1 0 1854520857 655265792 153174 4294967295 134512640 135167914 3221224448 3221057184 134624777 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 159977 153174 162 162 0 159815 0
[pid=31710] vsize: 639908
Current children cumulated CPU time (s) 610.15
Current children cumulated vsize (Kb) 642036

[startup+630.756 s]
Raw data (loadavg): 0.99 0.97 0.95 2/58 31730
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 175214 0 0 0 61162 832 0 0 25 0 1 0 1854520857 665214976 155603 4294967295 134512640 135167914 3221224448 3221073924 134845938 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 162406 155603 162 162 0 162244 0
[pid=31710] vsize: 649624
Current children cumulated CPU time (s) 620.01
Current children cumulated vsize (Kb) 651752

[startup+640.757 s]
Raw data (loadavg): 0.99 0.97 0.95 2/58 31730
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 177549 0 0 0 62138 842 0 0 25 0 1 0 1854520857 674779136 157938 4294967295 134512640 135167914 3221224448 3221056456 134846926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 164741 157938 162 162 0 164579 0
[pid=31710] vsize: 658964
Current children cumulated CPU time (s) 629.87
Current children cumulated vsize (Kb) 661092

[startup+650.758 s]
Raw data (loadavg): 0.99 0.97 0.95 2/58 31732
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 192947 0 0 0 63080 882 0 0 25 0 1 0 1854520857 771502080 173336 4294967295 134512640 135167914 3221224448 3221085952 134625368 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 188355 173336 162 162 0 188193 0
[pid=31710] vsize: 753420
Current children cumulated CPU time (s) 639.69
Current children cumulated vsize (Kb) 755548

[startup+660.76 s]
Raw data (loadavg): 0.99 0.97 0.95 1/58 31732
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) T 31705 31705 9102 0 -1 0 201638 0 0 0 64054 906 0 0 25 0 1 0 1854520857 730251264 171481 4294967295 134512640 135167914 3221224448 3221065628 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/31710/statm): 178284 171481 162 162 0 178122 0
[pid=31710] vsize: 713136
Current children cumulated CPU time (s) 649.67
Current children cumulated vsize (Kb) 715264

[startup+670.761 s]
Raw data (loadavg): 0.99 0.97 0.95 2/58 31732
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 203987 0 0 0 65028 916 0 0 25 0 1 0 1854520857 739872768 173830 4294967295 134512640 135167914 3221224448 3221089276 134722225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31710/statm): 180633 173830 162 162 0 180471 0
[pid=31710] vsize: 722532
Current children cumulated CPU time (s) 659.51
Current children cumulated vsize (Kb) 724660

[startup+680.762 s]
Raw data (loadavg): 0.99 0.97 0.95 2/58 31732
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) T 31705 31705 9102 0 -1 0 206453 0 0 0 66001 927 0 0 25 0 1 0 1854520857 749973504 176296 4294967295 134512640 135167914 3221224448 3221058684 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/31710/statm): 183099 176296 162 162 0 182937 0
[pid=31710] vsize: 732396
Current children cumulated CPU time (s) 669.35
Current children cumulated vsize (Kb) 734524

[startup+690.763 s]
Raw data (loadavg): 0.99 0.97 0.95 2/58 31732
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 208753 0 0 0 66973 939 0 0 25 0 1 0 1854520857 759394304 178596 4294967295 134512640 135167914 3221224448 3221078792 134844633 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31710/statm): 185399 178596 162 162 0 185237 0
[pid=31710] vsize: 741596
Current children cumulated CPU time (s) 679.19
Current children cumulated vsize (Kb) 743724

[startup+700.764 s]
Raw data (loadavg): 0.99 0.97 0.95 2/58 31732
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 211218 0 0 0 67947 949 0 0 25 0 1 0 1854520857 769490944 181061 4294967295 134512640 135167914 3221224448 3221055692 134695542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31710/statm): 187864 181061 162 162 0 187702 0
[pid=31710] vsize: 751456
Current children cumulated CPU time (s) 689.03
Current children cumulated vsize (Kb) 753584

[startup+710.765 s]
Raw data (loadavg): 0.99 0.97 0.95 2/58 31734
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 213544 0 0 0 68922 959 0 0 25 0 1 0 1854520857 779018240 183387 4294967295 134512640 135167914 3221224448 3221054756 134845938 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31710/statm): 190190 183387 162 162 0 190028 0
[pid=31710] vsize: 760760
Current children cumulated CPU time (s) 698.88
Current children cumulated vsize (Kb) 762888

[startup+720.766 s]
Raw data (loadavg): 0.99 0.97 0.95 2/58 31734
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 215961 0 0 0 69893 971 0 0 25 0 1 0 1854520857 788918272 185804 4294967295 134512640 135167914 3221224448 3221078912 134624036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 192607 185804 162 162 0 192445 0
[pid=31710] vsize: 770428
Current children cumulated CPU time (s) 708.71
Current children cumulated vsize (Kb) 772556

[startup+730.767 s]
Raw data (loadavg): 0.99 0.97 0.95 2/58 31734
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 218549 0 0 0 70865 982 0 0 25 0 1 0 1854520857 799518720 188392 4294967295 134512640 135167914 3221224448 3221056368 134845927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31710/statm): 195195 188392 162 162 0 195033 0
[pid=31710] vsize: 780780
Current children cumulated CPU time (s) 718.54
Current children cumulated vsize (Kb) 782908

[startup+740.768 s]
Raw data (loadavg): 0.99 0.97 0.95 2/58 31734
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 220842 0 0 0 71839 995 0 0 25 0 1 0 1854520857 808910848 190685 4294967295 134512640 135167914 3221224448 3221077520 134845937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 197488 190685 162 162 0 197326 0
[pid=31710] vsize: 789952
Current children cumulated CPU time (s) 728.41
Current children cumulated vsize (Kb) 792080

[startup+750.769 s]
Raw data (loadavg): 0.99 0.97 0.95 2/58 31734
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 223365 0 0 0 72809 1009 0 0 25 0 1 0 1854520857 819245056 193208 4294967295 134512640 135167914 3221224448 3221057248 134845219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 200011 193208 162 162 0 199849 0
[pid=31710] vsize: 800044
Current children cumulated CPU time (s) 738.25
Current children cumulated vsize (Kb) 802172

[startup+760.769 s]
Raw data (loadavg): 0.99 0.97 0.95 2/58 31734
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 225773 0 0 0 73783 1018 0 0 25 0 1 0 1854520857 829108224 195616 4294967295 134512640 135167914 3221224448 3221076904 134693706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 202419 195616 162 162 0 202257 0
[pid=31710] vsize: 809676
Current children cumulated CPU time (s) 748.08
Current children cumulated vsize (Kb) 811804

[startup+770.77 s]
Raw data (loadavg): 0.99 0.97 0.95 2/58 31736
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) T 31705 31705 9102 0 -1 0 227994 0 0 0 74758 1029 0 0 25 0 1 0 1854520857 838205440 197837 4294967295 134512640 135167914 3221224448 3221088476 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/31710/statm): 204640 197837 162 162 0 204478 0
[pid=31710] vsize: 818560
Current children cumulated CPU time (s) 757.94
Current children cumulated vsize (Kb) 820688

[startup+780.77 s]
Raw data (loadavg): 1.07 0.99 0.95 2/58 31736
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 230863 0 0 0 75725 1043 0 0 25 0 1 0 1854520857 849956864 200706 4294967295 134512640 135167914 3221224448 3221064512 134849606 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 207509 200706 162 162 0 207347 0
[pid=31710] vsize: 830036
Current children cumulated CPU time (s) 767.75
Current children cumulated vsize (Kb) 832164

[startup+790.772 s]
Raw data (loadavg): 1.14 1.00 0.96 2/58 31736
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 233295 0 0 0 76696 1054 0 0 25 0 1 0 1854520857 859918336 203138 4294967295 134512640 135167914 3221224448 3221065952 134695660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31710/statm): 209941 203138 162 162 0 209779 0
[pid=31710] vsize: 839764
Current children cumulated CPU time (s) 777.57
Current children cumulated vsize (Kb) 841892

[startup+800.773 s]
Raw data (loadavg): 1.11 1.00 0.96 2/58 31736
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 235596 0 0 0 77672 1065 0 0 25 0 1 0 1854520857 869343232 205439 4294967295 134512640 135167914 3221224448 3221054784 134843113 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31710/statm): 212242 205439 162 162 0 212080 0
[pid=31710] vsize: 848968
Current children cumulated CPU time (s) 787.44
Current children cumulated vsize (Kb) 851096

[startup+810.774 s]
Raw data (loadavg): 1.10 1.00 0.96 2/58 31736
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 238030 0 0 0 78642 1078 0 0 25 0 1 0 1854520857 879312896 207873 4294967295 134512640 135167914 3221224448 3221067504 134623757 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31710/statm): 214676 207873 162 162 0 214514 0
[pid=31710] vsize: 858704
Current children cumulated CPU time (s) 797.27
Current children cumulated vsize (Kb) 860832

[startup+820.775 s]
Raw data (loadavg): 1.08 1.00 0.96 2/58 31736
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 240719 0 0 0 79611 1090 0 0 25 0 1 0 1854520857 890327040 210562 4294967295 134512640 135167914 3221224448 3221078248 134846924 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31710/statm): 217365 210562 162 162 0 217203 0
[pid=31710] vsize: 869460
Current children cumulated CPU time (s) 807.08
Current children cumulated vsize (Kb) 871588

[startup+830.775 s]
Raw data (loadavg): 1.07 1.00 0.96 2/58 31738
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 243038 0 6 0 80579 1103 0 0 25 0 1 0 1854520857 899764224 212546 4294967295 134512640 135167914 3221224448 3221058656 134844956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 219669 212546 162 162 0 219507 0
[pid=31710] vsize: 878676
Current children cumulated CPU time (s) 816.89
Current children cumulated vsize (Kb) 880804

[startup+840.776 s]
Raw data (loadavg): 1.06 1.00 0.96 2/58 31738
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 245384 0 33 0 81529 1115 0 0 25 0 1 0 1854520857 909172736 214604 4294967295 134512640 135167914 3221224448 3221068624 134623803 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 221966 214604 162 162 0 221804 0
[pid=31710] vsize: 887864
Current children cumulated CPU time (s) 826.51
Current children cumulated vsize (Kb) 889992

[startup+850.777 s]
Raw data (loadavg): 1.05 1.00 0.96 2/58 31738
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 247652 0 49 0 82487 1131 0 0 25 0 1 0 1854520857 918364160 216539 4294967295 134512640 135167914 3221224448 3221087540 134843117 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31710/statm): 224210 216539 162 162 0 224048 0
[pid=31710] vsize: 896840
Current children cumulated CPU time (s) 836.25
Current children cumulated vsize (Kb) 898968

[startup+860.779 s]
Raw data (loadavg): 1.04 1.00 0.96 2/58 31738
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 249980 0 88 0 83422 1144 0 0 25 0 1 0 1854520857 926883840 217658 4294967295 134512640 135167914 3221224448 3221098512 134619144 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 226290 217658 162 162 0 226128 0
[pid=31710] vsize: 905160
Current children cumulated CPU time (s) 845.73
Current children cumulated vsize (Kb) 907288

[startup+870.78 s]
Raw data (loadavg): 1.03 1.00 0.96 2/58 31738
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 234 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 252750 0 383 0 84050 1158 0 0 18 0 1 0 1854520857 933425152 218450 4294967295 134512640 135167914 3221224448 3221069520 134843113 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 227887 218450 162 162 0 227725 0
[pid=31710] vsize: 911548
Current children cumulated CPU time (s) 852.15
Current children cumulated vsize (Kb) 913676

[startup+880.78 s]
Raw data (loadavg): 1.10 1.02 0.96 2/58 31738
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 233 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 233 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) R 31705 31705 9102 0 -1 0 255749 0 519 0 84894 1171 0 0 25 0 1 0 1854520857 941445120 220044 4294967295 134512640 135167914 3221224448 3221073424 134845930 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31710/statm): 229845 220044 162 162 0 229683 0
[pid=31710] vsize: 919380
Current children cumulated CPU time (s) 860.72
Current children cumulated vsize (Kb) 921508



Mem limit exceeded: sending SIGTERM then SIGKILL

[startup+880.865 s]
Raw data (loadavg): 1.10 1.02 0.96 1/58 31738
Raw data (/proc/31705/stat): 31705 (minisat+_script) S 31704 31705 9102 0 -1 0 301 331 13 1 0 1 3 3 17 0 1 0 1854520735 2179072 233 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31705/statm): 532 233 485 147 0 385 0
[pid=31705] vsize: 2128
Raw data (/proc/31710/stat): 31710 (minisat+_bignum) T 31705 31705 9102 0 -1 0 255772 0 519 0 84902 1171 0 0 25 0 1 0 1854520857 941543424 220067 4294967295 134512640 135167914 3221224448 3221066940 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/31710/statm): 229869 220067 162 162 0 229707 0
[pid=31710] vsize: 919476
Current children cumulated CPU time (s) 860.8
Current children cumulated vsize (Kb) 921604

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

Child status: 0
Real time (s): 881.364
CPU time (s): 861.153
CPU user time (s): 849.024
CPU system time (s): 12.1292
CPU usage (%): 97.7068
Max. virtual memory (cumulated for all children) (Kb): 921604