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/9905/stat): 9905 (minisat+_script) R 9904 9905 31778 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1784073609 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/9905/statm): 174 3 169 147 0 27 0
[pid=9905] 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=9906
New process pid=9907
New process pid=9908
execve syscall for /bin/sed executable
One traced child (pid=9907) 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=9908) exited with status: 0
One traced child (pid=9906) exited with status: 0
New process pid=9909
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc15/normalized-ii8b2.opb

[startup+10.004 s]
Raw data (loadavg): 0.93 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 4231 0 0 0 964 16 0 0 25 0 1 0 1784073614 17829888 4033 4294967295 134512640 135094434 3221224448 3221223088 134558264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 4353 4033 145 145 0 4208 0
[pid=9909] vsize: 17412
Current children cumulated CPU time (s) 9.81
Current children cumulated vsize (Kb) 19536

[startup+20.0048 s]
Raw data (loadavg): 0.94 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) T 9905 9905 31778 0 -1 0 4489 0 0 0 1960 17 0 0 25 0 1 0 1784073614 19943424 4291 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/9909/statm): 4869 4291 145 145 0 4724 0
[pid=9909] vsize: 19476
Current children cumulated CPU time (s) 19.78
Current children cumulated vsize (Kb) 21600

[startup+30.0067 s]
Raw data (loadavg): 0.95 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 4676 0 0 0 2957 19 0 0 25 0 1 0 1784073614 20692992 4478 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 5052 4478 145 145 0 4907 0
[pid=9909] vsize: 20208
Current children cumulated CPU time (s) 29.77
Current children cumulated vsize (Kb) 22332

[startup+40.0075 s]
Raw data (loadavg): 0.96 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 4929 0 0 0 3953 21 0 0 25 0 1 0 1784073614 21749760 4731 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 5310 4731 145 145 0 5165 0
[pid=9909] vsize: 21240
Current children cumulated CPU time (s) 39.75
Current children cumulated vsize (Kb) 23364

[startup+50.0093 s]
Raw data (loadavg): 0.96 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 5131 0 0 0 4948 23 0 0 25 0 1 0 1784073614 22564864 4933 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 5509 4933 145 145 0 5364 0
[pid=9909] vsize: 22036
Current children cumulated CPU time (s) 49.72
Current children cumulated vsize (Kb) 24160

[startup+60.0101 s]
Raw data (loadavg): 0.97 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 5300 0 0 0 5946 24 0 0 25 0 1 0 1784073614 23306240 5102 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 5690 5102 145 145 0 5545 0
[pid=9909] vsize: 22760
Current children cumulated CPU time (s) 59.71
Current children cumulated vsize (Kb) 24884

[startup+70.0109 s]
Raw data (loadavg): 0.97 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 5436 0 0 0 6944 25 0 0 25 0 1 0 1784073614 23875584 5238 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 5829 5238 145 145 0 5684 0
[pid=9909] vsize: 23316
Current children cumulated CPU time (s) 69.7
Current children cumulated vsize (Kb) 25440

[startup+80.0127 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 5576 0 0 0 7942 26 0 0 25 0 1 0 1784073614 24264704 5335 4294967295 134512640 135094434 3221224448 3221223072 134557694 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 5924 5335 145 145 0 5779 0
[pid=9909] vsize: 23696
Current children cumulated CPU time (s) 79.69
Current children cumulated vsize (Kb) 25820

[startup+90.0136 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 5692 0 0 0 8941 27 0 0 25 0 1 0 1784073614 24731648 5451 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 6038 5451 145 145 0 5893 0
[pid=9909] vsize: 24152
Current children cumulated CPU time (s) 89.69
Current children cumulated vsize (Kb) 26276

[startup+100.014 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 5881 0 0 0 9938 29 0 0 25 0 1 0 1784073614 25497600 5640 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 6225 5640 145 145 0 6080 0
[pid=9909] vsize: 24900
Current children cumulated CPU time (s) 99.68
Current children cumulated vsize (Kb) 27024

[startup+110.016 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 6041 0 0 0 10935 29 0 0 25 0 1 0 1784073614 26144768 5800 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 6383 5800 145 145 0 6238 0
[pid=9909] vsize: 25532
Current children cumulated CPU time (s) 109.65
Current children cumulated vsize (Kb) 27656

[startup+120.017 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 6193 0 0 0 11932 31 0 0 25 0 1 0 1784073614 26750976 5952 4294967295 134512640 135094434 3221224448 3221223072 134562131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 6531 5952 145 145 0 6386 0
[pid=9909] vsize: 26124
Current children cumulated CPU time (s) 119.64
Current children cumulated vsize (Kb) 28248

[startup+130.018 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 6377 0 0 0 12929 33 0 0 25 0 1 0 1784073614 27496448 6136 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 6713 6136 145 145 0 6568 0
[pid=9909] vsize: 26852
Current children cumulated CPU time (s) 129.63
Current children cumulated vsize (Kb) 28976

[startup+140.019 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 6556 0 0 0 13927 34 0 0 25 0 1 0 1784073614 28352512 6315 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 6922 6315 145 145 0 6777 0
[pid=9909] vsize: 27688
Current children cumulated CPU time (s) 139.62
Current children cumulated vsize (Kb) 29812

[startup+150.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 6745 0 0 0 14924 35 0 0 25 0 1 0 1784073614 29122560 6504 4294967295 134512640 135094434 3221224448 3221223072 134557604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 7110 6504 145 145 0 6965 0
[pid=9909] vsize: 28440
Current children cumulated CPU time (s) 149.6
Current children cumulated vsize (Kb) 30564

[startup+160.021 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 6876 0 0 0 15922 36 0 0 25 0 1 0 1784073614 29650944 6635 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 7239 6635 145 145 0 7094 0
[pid=9909] vsize: 28956
Current children cumulated CPU time (s) 159.59
Current children cumulated vsize (Kb) 31080

[startup+170.022 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 7037 0 0 0 16919 37 0 0 25 0 1 0 1784073614 30302208 6796 4294967295 134512640 135094434 3221224448 3221223040 134557423 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 7398 6796 145 145 0 7253 0
[pid=9909] vsize: 29592
Current children cumulated CPU time (s) 169.57
Current children cumulated vsize (Kb) 31716

[startup+180.023 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 7194 0 0 0 17917 38 0 0 25 0 1 0 1784073614 30945280 6953 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 7555 6953 145 145 0 7410 0
[pid=9909] vsize: 30220
Current children cumulated CPU time (s) 179.56
Current children cumulated vsize (Kb) 32344

[startup+190.024 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 7370 0 0 0 18914 40 0 0 25 0 1 0 1784073614 31657984 7129 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 7729 7129 145 145 0 7584 0
[pid=9909] vsize: 30916
Current children cumulated CPU time (s) 189.55
Current children cumulated vsize (Kb) 33040

[startup+200.025 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 7566 0 0 0 19911 41 0 0 25 0 1 0 1784073614 32456704 7325 4294967295 134512640 135094434 3221224448 3221223040 134556793 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 7924 7325 145 145 0 7779 0
[pid=9909] vsize: 31696
Current children cumulated CPU time (s) 199.53
Current children cumulated vsize (Kb) 33820

[startup+210.025 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 7708 0 0 0 20909 42 0 0 25 0 1 0 1784073614 33030144 7467 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 8064 7467 145 145 0 7919 0
[pid=9909] vsize: 32256
Current children cumulated CPU time (s) 209.52
Current children cumulated vsize (Kb) 34380

[startup+220.026 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 7852 0 0 0 21907 43 0 0 25 0 1 0 1784073614 33615872 7611 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 8207 7611 145 145 0 8062 0
[pid=9909] vsize: 32828
Current children cumulated CPU time (s) 219.51
Current children cumulated vsize (Kb) 34952

[startup+230.028 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 8008 0 0 0 22905 44 0 0 25 0 1 0 1784073614 34242560 7767 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 8360 7767 145 145 0 8215 0
[pid=9909] vsize: 33440
Current children cumulated CPU time (s) 229.5
Current children cumulated vsize (Kb) 35564

[startup+240.029 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 8153 0 0 0 23903 45 0 0 25 0 1 0 1784073614 34832384 7912 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 8504 7912 145 145 0 8359 0
[pid=9909] vsize: 34016
Current children cumulated CPU time (s) 239.49
Current children cumulated vsize (Kb) 36140

[startup+250.031 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 8312 0 0 0 24901 45 0 0 25 0 1 0 1784073614 35475456 8071 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 8661 8071 145 145 0 8516 0
[pid=9909] vsize: 34644
Current children cumulated CPU time (s) 249.47
Current children cumulated vsize (Kb) 36768

[startup+260.032 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 8482 0 0 0 25898 46 0 0 25 0 1 0 1784073614 36171776 8241 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 8831 8241 145 145 0 8686 0
[pid=9909] vsize: 35324
Current children cumulated CPU time (s) 259.45
Current children cumulated vsize (Kb) 37448

[startup+270.032 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 8646 0 0 0 26895 48 0 0 25 0 1 0 1784073614 36843520 8405 4294967295 134512640 135094434 3221224448 3221223040 134557369 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 8995 8405 145 145 0 8850 0
[pid=9909] vsize: 35980
Current children cumulated CPU time (s) 269.44
Current children cumulated vsize (Kb) 38104

[startup+280.033 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 8784 0 0 0 27893 49 0 0 25 0 1 0 1784073614 37400576 8543 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 9131 8543 145 145 0 8986 0
[pid=9909] vsize: 36524
Current children cumulated CPU time (s) 279.43
Current children cumulated vsize (Kb) 38648

[startup+290.035 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 8931 0 0 0 28892 49 0 0 25 0 1 0 1784073614 37998592 8690 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 9277 8690 145 145 0 9132 0
[pid=9909] vsize: 37108
Current children cumulated CPU time (s) 289.42
Current children cumulated vsize (Kb) 39232

[startup+300.036 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 9030 0 0 0 29891 50 0 0 25 0 1 0 1784073614 38227968 8746 4294967295 134512640 135094434 3221224448 3221223040 134556817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 9333 8746 145 145 0 9188 0
[pid=9909] vsize: 37332
Current children cumulated CPU time (s) 299.42
Current children cumulated vsize (Kb) 39456

[startup+310.037 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 9030 0 0 0 30890 50 0 0 25 0 1 0 1784073614 38227968 8746 4294967295 134512640 135094434 3221224448 3221223040 134557004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 9333 8746 145 145 0 9188 0
[pid=9909] vsize: 37332
Current children cumulated CPU time (s) 309.41
Current children cumulated vsize (Kb) 39456

[startup+320.037 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 9030 0 0 0 31891 50 0 0 25 0 1 0 1784073614 38227968 8746 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 9333 8746 145 145 0 9188 0
[pid=9909] vsize: 37332
Current children cumulated CPU time (s) 319.42
Current children cumulated vsize (Kb) 39456

[startup+330.038 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 9030 0 0 0 32891 50 0 0 25 0 1 0 1784073614 38227968 8746 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 9333 8746 145 145 0 9188 0
[pid=9909] vsize: 37332
Current children cumulated CPU time (s) 329.42
Current children cumulated vsize (Kb) 39456

[startup+340.039 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 9030 0 0 0 33891 50 0 0 25 0 1 0 1784073614 38227968 8746 4294967295 134512640 135094434 3221224448 3221223072 134557726 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 9333 8746 145 145 0 9188 0
[pid=9909] vsize: 37332
Current children cumulated CPU time (s) 339.42
Current children cumulated vsize (Kb) 39456

[startup+350.041 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 9030 0 0 0 34891 50 0 0 25 0 1 0 1784073614 38227968 8746 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 9333 8746 145 145 0 9188 0
[pid=9909] vsize: 37332
Current children cumulated CPU time (s) 349.42
Current children cumulated vsize (Kb) 39456

[startup+360.042 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 9030 0 0 0 35892 50 0 0 25 0 1 0 1784073614 38227968 8746 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 9333 8746 145 145 0 9188 0
[pid=9909] vsize: 37332
Current children cumulated CPU time (s) 359.43
Current children cumulated vsize (Kb) 39456

[startup+370.043 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 9030 0 0 0 36892 50 0 0 25 0 1 0 1784073614 38227968 8746 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 9333 8746 145 145 0 9188 0
[pid=9909] vsize: 37332
Current children cumulated CPU time (s) 369.43
Current children cumulated vsize (Kb) 39456

[startup+380.043 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 9030 0 0 0 37892 50 0 0 25 0 1 0 1784073614 38227968 8746 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 9333 8746 145 145 0 9188 0
[pid=9909] vsize: 37332
Current children cumulated CPU time (s) 379.43
Current children cumulated vsize (Kb) 39456

[startup+390.044 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 9030 0 0 0 38892 50 0 0 25 0 1 0 1784073614 38227968 8746 4294967295 134512640 135094434 3221224448 3221223104 134557882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 9333 8746 145 145 0 9188 0
[pid=9909] vsize: 37332
Current children cumulated CPU time (s) 389.43
Current children cumulated vsize (Kb) 39456

[startup+400.045 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 9030 0 0 0 39893 50 0 0 25 0 1 0 1784073614 38227968 8746 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 9333 8746 145 145 0 9188 0
[pid=9909] vsize: 37332
Current children cumulated CPU time (s) 399.44
Current children cumulated vsize (Kb) 39456

[startup+410.046 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 9030 0 0 0 40893 50 0 0 25 0 1 0 1784073614 38227968 8746 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 9333 8746 145 145 0 9188 0
[pid=9909] vsize: 37332
Current children cumulated CPU time (s) 409.44
Current children cumulated vsize (Kb) 39456

[startup+420.047 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 9030 0 0 0 41893 50 0 0 25 0 1 0 1784073614 38227968 8746 4294967295 134512640 135094434 3221224448 3221223040 134557363 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 9333 8746 145 145 0 9188 0
[pid=9909] vsize: 37332
Current children cumulated CPU time (s) 419.44
Current children cumulated vsize (Kb) 39456

[startup+430.048 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 9030 0 0 0 42894 50 0 0 25 0 1 0 1784073614 38227968 8746 4294967295 134512640 135094434 3221224448 3221223104 134558022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 9333 8746 145 145 0 9188 0
[pid=9909] vsize: 37332
Current children cumulated CPU time (s) 429.45
Current children cumulated vsize (Kb) 39456

[startup+440.049 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 9030 0 0 0 43894 50 0 0 25 0 1 0 1784073614 38227968 8746 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 9333 8746 145 145 0 9188 0
[pid=9909] vsize: 37332
Current children cumulated CPU time (s) 439.45
Current children cumulated vsize (Kb) 39456

[startup+450.051 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 9030 0 0 0 44894 50 0 0 25 0 1 0 1784073614 38227968 8746 4294967295 134512640 135094434 3221224448 3221223040 134557398 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 9333 8746 145 145 0 9188 0
[pid=9909] vsize: 37332
Current children cumulated CPU time (s) 449.45
Current children cumulated vsize (Kb) 39456

[startup+460.052 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 9030 0 0 0 45894 50 0 0 25 0 1 0 1784073614 38227968 8746 4294967295 134512640 135094434 3221224448 3221223040 134556933 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 9333 8746 145 145 0 9188 0
[pid=9909] vsize: 37332
Current children cumulated CPU time (s) 459.45
Current children cumulated vsize (Kb) 39456

[startup+470.053 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 9030 0 0 0 46895 50 0 0 25 0 1 0 1784073614 38227968 8746 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 9333 8746 145 145 0 9188 0
[pid=9909] vsize: 37332
Current children cumulated CPU time (s) 469.46
Current children cumulated vsize (Kb) 39456

[startup+480.054 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 9031 0 0 0 47895 50 0 0 25 0 1 0 1784073614 38227968 8747 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 9333 8747 145 145 0 9188 0
[pid=9909] vsize: 37332
Current children cumulated CPU time (s) 479.46
Current children cumulated vsize (Kb) 39456

[startup+490.054 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 9031 0 0 0 48895 50 0 0 25 0 1 0 1784073614 38227968 8747 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 9333 8747 145 145 0 9188 0
[pid=9909] vsize: 37332
Current children cumulated CPU time (s) 489.46
Current children cumulated vsize (Kb) 39456

[startup+500.056 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 9031 0 0 0 49896 50 0 0 25 0 1 0 1784073614 38227968 8747 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 9333 8747 145 145 0 9188 0
[pid=9909] vsize: 37332
Current children cumulated CPU time (s) 499.47
Current children cumulated vsize (Kb) 39456

[startup+510.057 s]
Raw data (loadavg): 1.15 1.02 1.01 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 9031 0 0 0 50896 50 0 0 25 0 1 0 1784073614 38227968 8747 4294967295 134512640 135094434 3221224448 3221223040 134556851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 9333 8747 145 145 0 9188 0
[pid=9909] vsize: 37332
Current children cumulated CPU time (s) 509.47
Current children cumulated vsize (Kb) 39456

[startup+520.058 s]
Raw data (loadavg): 1.12 1.02 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 9031 0 0 0 51896 50 0 0 25 0 1 0 1784073614 38227968 8747 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 9333 8747 145 145 0 9188 0
[pid=9909] vsize: 37332
Current children cumulated CPU time (s) 519.47
Current children cumulated vsize (Kb) 39456

[startup+530.06 s]
Raw data (loadavg): 1.10 1.01 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 9031 0 0 0 52896 50 0 0 25 0 1 0 1784073614 38227968 8747 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 9333 8747 145 145 0 9188 0
[pid=9909] vsize: 37332
Current children cumulated CPU time (s) 529.47
Current children cumulated vsize (Kb) 39456

[startup+540.061 s]
Raw data (loadavg): 1.09 1.01 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 9054 0 0 0 53896 50 0 0 25 0 1 0 1784073614 38322176 8770 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 9356 8770 145 145 0 9211 0
[pid=9909] vsize: 37424
Current children cumulated CPU time (s) 539.47
Current children cumulated vsize (Kb) 39548

[startup+550.062 s]
Raw data (loadavg): 1.07 1.01 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 9167 0 0 0 54894 52 0 0 25 0 1 0 1784073614 38780928 8883 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 9468 8883 145 145 0 9323 0
[pid=9909] vsize: 37872
Current children cumulated CPU time (s) 549.47
Current children cumulated vsize (Kb) 39996

[startup+560.063 s]
Raw data (loadavg): 1.06 1.01 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 9260 0 0 0 55893 53 0 0 25 0 1 0 1784073614 39157760 8976 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 9560 8976 145 145 0 9415 0
[pid=9909] vsize: 38240
Current children cumulated CPU time (s) 559.47
Current children cumulated vsize (Kb) 40364

[startup+570.064 s]
Raw data (loadavg): 1.05 1.01 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 9352 0 0 0 56892 53 0 0 25 0 1 0 1784073614 39534592 9068 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 9652 9068 145 145 0 9507 0
[pid=9909] vsize: 38608
Current children cumulated CPU time (s) 569.46
Current children cumulated vsize (Kb) 40732

[startup+580.065 s]
Raw data (loadavg): 1.04 1.01 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 9458 0 0 0 57890 54 0 0 25 0 1 0 1784073614 39976960 9174 4294967295 134512640 135094434 3221224448 3221223080 134557561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 9760 9174 145 145 0 9615 0
[pid=9909] vsize: 39040
Current children cumulated CPU time (s) 579.45
Current children cumulated vsize (Kb) 41164

[startup+590.066 s]
Raw data (loadavg): 1.04 1.01 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 9559 0 0 0 58889 54 0 0 25 0 1 0 1784073614 40398848 9275 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 9863 9275 145 145 0 9718 0
[pid=9909] vsize: 39452
Current children cumulated CPU time (s) 589.44
Current children cumulated vsize (Kb) 41576

[startup+600.066 s]
Raw data (loadavg): 1.03 1.01 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 9639 0 0 0 59888 55 0 0 25 0 1 0 1784073614 40722432 9355 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 9942 9355 145 145 0 9797 0
[pid=9909] vsize: 39768
Current children cumulated CPU time (s) 599.44
Current children cumulated vsize (Kb) 41892

[startup+610.067 s]
Raw data (loadavg): 1.03 1.01 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 9718 0 0 0 60887 55 0 0 25 0 1 0 1784073614 41041920 9434 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 10020 9434 145 145 0 9875 0
[pid=9909] vsize: 40080
Current children cumulated CPU time (s) 609.43
Current children cumulated vsize (Kb) 42204

[startup+620.068 s]
Raw data (loadavg): 1.02 1.01 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 9812 0 0 0 61885 55 0 0 25 0 1 0 1784073614 41422848 9528 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 10113 9528 145 145 0 9968 0
[pid=9909] vsize: 40452
Current children cumulated CPU time (s) 619.41
Current children cumulated vsize (Kb) 42576

[startup+630.069 s]
Raw data (loadavg): 1.02 1.00 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 9921 0 0 0 62883 56 0 0 25 0 1 0 1784073614 42123264 9637 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 10284 9637 145 145 0 10139 0
[pid=9909] vsize: 41136
Current children cumulated CPU time (s) 629.4
Current children cumulated vsize (Kb) 43260

[startup+640.07 s]
Raw data (loadavg): 1.01 1.00 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 10029 0 0 0 63882 57 0 0 25 0 1 0 1784073614 42561536 9745 4294967295 134512640 135094434 3221224448 3221223104 134557914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 10391 9745 145 145 0 10246 0
[pid=9909] vsize: 41564
Current children cumulated CPU time (s) 639.4
Current children cumulated vsize (Kb) 43688

[startup+650.072 s]
Raw data (loadavg): 1.01 1.00 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 10118 0 0 0 64881 58 0 0 25 0 1 0 1784073614 42921984 9834 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 10479 9834 145 145 0 10334 0
[pid=9909] vsize: 41916
Current children cumulated CPU time (s) 649.4
Current children cumulated vsize (Kb) 44040

[startup+660.072 s]
Raw data (loadavg): 1.16 1.04 1.01 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 10210 0 0 0 65879 59 0 0 25 0 1 0 1784073614 43319296 9926 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 10576 9926 145 145 0 10431 0
[pid=9909] vsize: 42304
Current children cumulated CPU time (s) 659.39
Current children cumulated vsize (Kb) 44428

[startup+670.073 s]
Raw data (loadavg): 1.14 1.03 1.01 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 10312 0 0 0 66878 59 0 0 25 0 1 0 1784073614 43732992 10028 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 10677 10028 145 145 0 10532 0
[pid=9909] vsize: 42708
Current children cumulated CPU time (s) 669.38
Current children cumulated vsize (Kb) 44832

[startup+680.074 s]
Raw data (loadavg): 1.12 1.03 1.01 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 10426 0 0 0 67875 60 0 0 25 0 1 0 1784073614 44220416 10142 4294967295 134512640 135094434 3221224448 3221223040 134557020 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 10796 10142 145 145 0 10651 0
[pid=9909] vsize: 43184
Current children cumulated CPU time (s) 679.36
Current children cumulated vsize (Kb) 45308

[startup+690.075 s]
Raw data (loadavg): 1.10 1.03 1.01 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 10533 0 0 0 68874 61 0 0 25 0 1 0 1784073614 44650496 10249 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 10901 10249 145 145 0 10756 0
[pid=9909] vsize: 43604
Current children cumulated CPU time (s) 689.36
Current children cumulated vsize (Kb) 45728

[startup+700.076 s]
Raw data (loadavg): 1.08 1.03 1.01 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 10627 0 0 0 69873 62 0 0 25 0 1 0 1784073614 45035520 10343 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 10995 10343 145 145 0 10850 0
[pid=9909] vsize: 43980
Current children cumulated CPU time (s) 699.36
Current children cumulated vsize (Kb) 46104

[startup+710.076 s]
Raw data (loadavg): 1.07 1.03 1.01 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 10747 0 0 0 70871 62 0 0 25 0 1 0 1784073614 45531136 10463 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 11116 10463 145 145 0 10971 0
[pid=9909] vsize: 44464
Current children cumulated CPU time (s) 709.34
Current children cumulated vsize (Kb) 46588

[startup+720.077 s]
Raw data (loadavg): 1.06 1.03 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 10830 0 0 0 71869 63 0 0 25 0 1 0 1784073614 45871104 10546 4294967295 134512640 135094434 3221224448 3221223104 134557893 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9909/statm): 11199 10546 145 145 0 11054 0
[pid=9909] vsize: 44796
Current children cumulated CPU time (s) 719.33
Current children cumulated vsize (Kb) 46920

[startup+730.079 s]
Raw data (loadavg): 1.05 1.03 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 10937 0 0 0 72867 64 0 0 25 0 1 0 1784073614 46350336 10653 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9909/statm): 11316 10653 145 145 0 11171 0
[pid=9909] vsize: 45264
Current children cumulated CPU time (s) 729.32
Current children cumulated vsize (Kb) 47388

[startup+740.08 s]
Raw data (loadavg): 1.04 1.02 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 11012 0 0 0 73865 65 0 0 25 0 1 0 1784073614 46637056 10728 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 11386 10728 145 145 0 11241 0
[pid=9909] vsize: 45544
Current children cumulated CPU time (s) 739.31
Current children cumulated vsize (Kb) 47668

[startup+750.082 s]
Raw data (loadavg): 1.03 1.02 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 11133 0 0 0 74864 65 0 0 25 0 1 0 1784073614 47116288 10849 4294967295 134512640 135094434 3221224448 3221223040 134557227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9909/statm): 11503 10849 145 145 0 11358 0
[pid=9909] vsize: 46012
Current children cumulated CPU time (s) 749.3
Current children cumulated vsize (Kb) 48136

[startup+760.083 s]
Raw data (loadavg): 1.03 1.02 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 11238 0 0 0 75861 67 0 0 25 0 1 0 1784073614 47550464 10954 4294967295 134512640 135094434 3221224448 3221223040 134556851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 11609 10954 145 145 0 11464 0
[pid=9909] vsize: 46436
Current children cumulated CPU time (s) 759.29
Current children cumulated vsize (Kb) 48560

[startup+770.083 s]
Raw data (loadavg): 1.02 1.02 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 11329 0 0 0 76860 67 0 0 25 0 1 0 1784073614 47919104 11045 4294967295 134512640 135094434 3221224448 3221223040 134556906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 11699 11045 145 145 0 11554 0
[pid=9909] vsize: 46796
Current children cumulated CPU time (s) 769.28
Current children cumulated vsize (Kb) 48920

[startup+780.085 s]
Raw data (loadavg): 1.02 1.02 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 11427 0 0 0 77859 67 0 0 25 0 1 0 1784073614 48316416 11143 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 11796 11143 145 145 0 11651 0
[pid=9909] vsize: 47184
Current children cumulated CPU time (s) 779.27
Current children cumulated vsize (Kb) 49308

[startup+790.086 s]
Raw data (loadavg): 1.02 1.02 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 11523 0 0 0 78857 68 0 0 25 0 1 0 1784073614 48701440 11239 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 11890 11239 145 145 0 11745 0
[pid=9909] vsize: 47560
Current children cumulated CPU time (s) 789.26
Current children cumulated vsize (Kb) 49684

[startup+800.087 s]
Raw data (loadavg): 1.01 1.02 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 11620 0 0 0 79856 69 0 0 25 0 1 0 1784073614 49090560 11336 4294967295 134512640 135094434 3221224448 3221223136 134554667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 11985 11336 145 145 0 11840 0
[pid=9909] vsize: 47940
Current children cumulated CPU time (s) 799.26
Current children cumulated vsize (Kb) 50064

[startup+810.088 s]
Raw data (loadavg): 1.01 1.02 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 11727 0 0 0 80854 70 0 0 25 0 1 0 1784073614 49520640 11443 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 12090 11443 145 145 0 11945 0
[pid=9909] vsize: 48360
Current children cumulated CPU time (s) 809.25
Current children cumulated vsize (Kb) 50484

[startup+820.088 s]
Raw data (loadavg): 1.01 1.02 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 11806 0 0 0 81853 70 0 0 25 0 1 0 1784073614 49844224 11522 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 12169 11522 145 145 0 12024 0
[pid=9909] vsize: 48676
Current children cumulated CPU time (s) 819.24
Current children cumulated vsize (Kb) 50800

[startup+830.089 s]
Raw data (loadavg): 1.01 1.02 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 11890 0 0 0 82853 71 0 0 25 0 1 0 1784073614 50184192 11606 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 12252 11606 145 145 0 12107 0
[pid=9909] vsize: 49008
Current children cumulated CPU time (s) 829.25
Current children cumulated vsize (Kb) 51132

[startup+840.09 s]
Raw data (loadavg): 1.00 1.01 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 11983 0 0 0 83851 72 0 0 25 0 1 0 1784073614 50565120 11699 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 12345 11699 145 145 0 12200 0
[pid=9909] vsize: 49380
Current children cumulated CPU time (s) 839.24
Current children cumulated vsize (Kb) 51504

[startup+850.091 s]
Raw data (loadavg): 1.00 1.01 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 12058 0 0 0 84850 72 0 0 25 0 1 0 1784073614 50868224 11774 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 12419 11774 145 145 0 12274 0
[pid=9909] vsize: 49676
Current children cumulated CPU time (s) 849.23
Current children cumulated vsize (Kb) 51800

[startup+860.092 s]
Raw data (loadavg): 1.00 1.01 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 12146 0 0 0 85850 72 0 0 25 0 1 0 1784073614 51224576 11862 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 12506 11862 145 145 0 12361 0
[pid=9909] vsize: 50024
Current children cumulated CPU time (s) 859.23
Current children cumulated vsize (Kb) 52148

[startup+870.093 s]
Raw data (loadavg): 1.00 1.01 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 12225 0 0 0 86849 72 0 0 25 0 1 0 1784073614 51556352 11941 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 12587 11941 145 145 0 12442 0
[pid=9909] vsize: 50348
Current children cumulated CPU time (s) 869.22
Current children cumulated vsize (Kb) 52472

[startup+880.094 s]
Raw data (loadavg): 1.00 1.01 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 12343 0 0 0 87847 73 0 0 25 0 1 0 1784073614 52031488 12059 4294967295 134512640 135094434 3221224448 3221223040 134556826 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 12703 12059 145 145 0 12558 0
[pid=9909] vsize: 50812
Current children cumulated CPU time (s) 879.21
Current children cumulated vsize (Kb) 52936

[startup+890.095 s]
Raw data (loadavg): 1.00 1.01 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 12434 0 0 0 88845 74 0 0 25 0 1 0 1784073614 52408320 12150 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 12795 12150 145 145 0 12650 0
[pid=9909] vsize: 51180
Current children cumulated CPU time (s) 889.2
Current children cumulated vsize (Kb) 53304

[startup+900.096 s]
Raw data (loadavg): 1.00 1.01 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 12510 0 0 0 89845 75 0 0 25 0 1 0 1784073614 52711424 12226 4294967295 134512640 135094434 3221224448 3221223040 134556773 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 12869 12226 145 145 0 12724 0
[pid=9909] vsize: 51476
Current children cumulated CPU time (s) 899.21
Current children cumulated vsize (Kb) 53600

[startup+910.097 s]
Raw data (loadavg): 1.00 1.01 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 12583 0 0 0 90844 75 0 0 25 0 1 0 1784073614 53014528 12299 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 12943 12299 145 145 0 12798 0
[pid=9909] vsize: 51772
Current children cumulated CPU time (s) 909.2
Current children cumulated vsize (Kb) 53896

[startup+920.097 s]
Raw data (loadavg): 1.00 1.01 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 12690 0 0 0 91842 76 0 0 25 0 1 0 1784073614 53444608 12406 4294967295 134512640 135094434 3221224448 3221223040 134557175 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 13048 12406 145 145 0 12903 0
[pid=9909] vsize: 52192
Current children cumulated CPU time (s) 919.19
Current children cumulated vsize (Kb) 54316

[startup+930.097 s]
Raw data (loadavg): 1.00 1.01 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 12768 0 0 0 92841 77 0 0 25 0 1 0 1784073614 53755904 12484 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 13124 12484 145 145 0 12979 0
[pid=9909] vsize: 52496
Current children cumulated CPU time (s) 929.19
Current children cumulated vsize (Kb) 54620

[startup+940.098 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 12833 0 0 0 93839 77 0 0 25 0 1 0 1784073614 54022144 12549 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 13189 12549 145 145 0 13044 0
[pid=9909] vsize: 52756
Current children cumulated CPU time (s) 939.17
Current children cumulated vsize (Kb) 54880

[startup+950.099 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 12914 0 0 0 94838 77 0 0 25 0 1 0 1784073614 54403072 12630 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 13282 12630 145 145 0 13137 0
[pid=9909] vsize: 53128
Current children cumulated CPU time (s) 949.16
Current children cumulated vsize (Kb) 55252

[startup+960.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 12992 0 0 0 95837 78 0 0 25 0 1 0 1784073614 54697984 12708 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 13354 12708 145 145 0 13209 0
[pid=9909] vsize: 53416
Current children cumulated CPU time (s) 959.16
Current children cumulated vsize (Kb) 55540

[startup+970.101 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 13103 0 0 0 96836 79 0 0 25 0 1 0 1784073614 55144448 12819 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 13463 12819 145 145 0 13318 0
[pid=9909] vsize: 53852
Current children cumulated CPU time (s) 969.16
Current children cumulated vsize (Kb) 55976

[startup+980.102 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 13213 0 0 0 97834 80 0 0 25 0 1 0 1784073614 55586816 12929 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 13571 12929 145 145 0 13426 0
[pid=9909] vsize: 54284
Current children cumulated CPU time (s) 979.15
Current children cumulated vsize (Kb) 56408

[startup+990.102 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 13324 0 0 0 98831 81 0 0 25 0 1 0 1784073614 56029184 13040 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9909/statm): 13679 13040 145 145 0 13534 0
[pid=9909] vsize: 54716
Current children cumulated CPU time (s) 989.13
Current children cumulated vsize (Kb) 56840

[startup+1000.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 13420 0 0 0 99828 82 0 0 25 0 1 0 1784073614 56438784 13136 4294967295 134512640 135094434 3221224448 3221223120 134555413 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 13779 13136 145 145 0 13634 0
[pid=9909] vsize: 55116
Current children cumulated CPU time (s) 999.11
Current children cumulated vsize (Kb) 57240

[startup+1010.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 13516 0 0 0 100827 83 0 0 25 0 1 0 1784073614 56823808 13232 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9909/statm): 13873 13232 145 145 0 13728 0
[pid=9909] vsize: 55492
Current children cumulated CPU time (s) 1009.11
Current children cumulated vsize (Kb) 57616

[startup+1020.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 13608 0 0 0 101825 84 0 0 25 0 1 0 1784073614 57184256 13324 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9909/statm): 13961 13324 145 145 0 13816 0
[pid=9909] vsize: 55844
Current children cumulated CPU time (s) 1019.1
Current children cumulated vsize (Kb) 57968

[startup+1030.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 13698 0 0 0 102822 85 0 0 25 0 1 0 1784073614 57548800 13414 4294967295 134512640 135094434 3221224448 3221223040 134556802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9909/statm): 14050 13414 145 145 0 13905 0
[pid=9909] vsize: 56200
Current children cumulated CPU time (s) 1029.08
Current children cumulated vsize (Kb) 58324

[startup+1040.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 13799 0 0 0 103820 86 0 0 25 0 1 0 1784073614 57954304 13515 4294967295 134512640 135094434 3221224448 3221223040 134557339 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9909/statm): 14149 13515 145 145 0 14004 0
[pid=9909] vsize: 56596
Current children cumulated CPU time (s) 1039.07
Current children cumulated vsize (Kb) 58720

[startup+1050.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 13896 0 0 0 104818 87 0 0 25 0 1 0 1784073614 58347520 13612 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9909/statm): 14245 13612 145 145 0 14100 0
[pid=9909] vsize: 56980
Current children cumulated CPU time (s) 1049.06
Current children cumulated vsize (Kb) 59104

[startup+1060.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 13970 0 0 0 105817 88 0 0 25 0 1 0 1784073614 58650624 13686 4294967295 134512640 135094434 3221224448 3221223040 134551454 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9909/statm): 14319 13686 145 145 0 14174 0
[pid=9909] vsize: 57276
Current children cumulated CPU time (s) 1059.06
Current children cumulated vsize (Kb) 59400

[startup+1070.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 13970 0 0 0 106816 89 0 0 25 0 1 0 1784073614 58650624 13686 4294967295 134512640 135094434 3221224448 3221223080 134557561 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9909/statm): 14319 13686 145 145 0 14174 0
[pid=9909] vsize: 57276
Current children cumulated CPU time (s) 1069.06
Current children cumulated vsize (Kb) 59400

[startup+1080.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 13970 0 0 0 107816 89 0 0 25 0 1 0 1784073614 58650624 13686 4294967295 134512640 135094434 3221224448 3221223104 134558022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9909/statm): 14319 13686 145 145 0 14174 0
[pid=9909] vsize: 57276
Current children cumulated CPU time (s) 1079.06
Current children cumulated vsize (Kb) 59400

[startup+1090.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 13970 0 0 0 108816 89 0 0 25 0 1 0 1784073614 58650624 13686 4294967295 134512640 135094434 3221224448 3221223040 134557208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9909/statm): 14319 13686 145 145 0 14174 0
[pid=9909] vsize: 57276
Current children cumulated CPU time (s) 1089.06
Current children cumulated vsize (Kb) 59400

[startup+1100.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 13970 0 0 0 109815 90 0 0 25 0 1 0 1784073614 58650624 13686 4294967295 134512640 135094434 3221224448 3221223040 134557157 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9909/statm): 14319 13686 145 145 0 14174 0
[pid=9909] vsize: 57276
Current children cumulated CPU time (s) 1099.06
Current children cumulated vsize (Kb) 59400

[startup+1110.12 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 13970 0 0 0 110815 90 0 0 25 0 1 0 1784073614 58650624 13686 4294967295 134512640 135094434 3221224448 3221223040 134557175 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9909/statm): 14319 13686 145 145 0 14174 0
[pid=9909] vsize: 57276
Current children cumulated CPU time (s) 1109.06
Current children cumulated vsize (Kb) 59400

[startup+1120.12 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 13970 0 0 0 111815 91 0 0 25 0 1 0 1784073614 58650624 13686 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9909/statm): 14319 13686 145 145 0 14174 0
[pid=9909] vsize: 57276
Current children cumulated CPU time (s) 1119.07
Current children cumulated vsize (Kb) 59400

[startup+1130.12 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 13970 0 0 0 112814 91 0 0 25 0 1 0 1784073614 58650624 13686 4294967295 134512640 135094434 3221224448 3221223040 134556880 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9909/statm): 14319 13686 145 145 0 14174 0
[pid=9909] vsize: 57276
Current children cumulated CPU time (s) 1129.06
Current children cumulated vsize (Kb) 59400

[startup+1140.12 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 13970 0 0 0 113814 92 0 0 25 0 1 0 1784073614 58650624 13686 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9909/statm): 14319 13686 145 145 0 14174 0
[pid=9909] vsize: 57276
Current children cumulated CPU time (s) 1139.07
Current children cumulated vsize (Kb) 59400

[startup+1150.12 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 13970 0 0 0 114814 92 0 0 25 0 1 0 1784073614 58650624 13686 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9909/statm): 14319 13686 145 145 0 14174 0
[pid=9909] vsize: 57276
Current children cumulated CPU time (s) 1149.07
Current children cumulated vsize (Kb) 59400

[startup+1160.12 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 13970 0 0 0 115813 93 0 0 25 0 1 0 1784073614 58650624 13686 4294967295 134512640 135094434 3221224448 3221223104 134558029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9909/statm): 14319 13686 145 145 0 14174 0
[pid=9909] vsize: 57276
Current children cumulated CPU time (s) 1159.07
Current children cumulated vsize (Kb) 59400

[startup+1170.12 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 13970 0 0 0 116813 93 0 0 25 0 1 0 1784073614 58650624 13686 4294967295 134512640 135094434 3221224448 3221223104 134557872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9909/statm): 14319 13686 145 145 0 14174 0
[pid=9909] vsize: 57276
Current children cumulated CPU time (s) 1169.07
Current children cumulated vsize (Kb) 59400

[startup+1180.12 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 13970 0 0 0 117813 93 0 0 25 0 1 0 1784073614 58650624 13686 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9909/statm): 14319 13686 145 145 0 14174 0
[pid=9909] vsize: 57276
Current children cumulated CPU time (s) 1179.07
Current children cumulated vsize (Kb) 59400

[startup+1190.12 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 13970 0 0 0 118812 94 0 0 25 0 1 0 1784073614 58650624 13686 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9909/statm): 14319 13686 145 145 0 14174 0
[pid=9909] vsize: 57276
Current children cumulated CPU time (s) 1189.07
Current children cumulated vsize (Kb) 59400

[startup+1200.12 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 13970 0 0 0 119811 95 0 0 25 0 1 0 1784073614 58650624 13686 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9909/statm): 14319 13686 145 145 0 14174 0
[pid=9909] vsize: 57276
Current children cumulated CPU time (s) 1199.07
Current children cumulated vsize (Kb) 59400

[startup+1210.13 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 13970 0 0 0 120811 95 0 0 25 0 1 0 1784073614 58650624 13686 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9909/statm): 14319 13686 145 145 0 14174 0
[pid=9909] vsize: 57276
Current children cumulated CPU time (s) 1209.07
Current children cumulated vsize (Kb) 59400



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.13 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9909
Raw data (/proc/9905/stat): 9905 (minisat+_script) S 9904 9905 31778 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1784073609 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9905/statm): 531 226 485 147 0 384 0
[pid=9905] vsize: 2124
Raw data (/proc/9909/stat): 9909 (minisat+_64-bit) R 9905 9905 31778 0 -1 0 13970 0 0 0 120811 95 0 0 25 0 1 0 1784073614 58650624 13686 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9909/statm): 14319 13686 145 145 0 14174 0
[pid=9909] vsize: 57276
Current children cumulated CPU time (s) 1209.07
Current children cumulated vsize (Kb) 59400

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

Child status: 10
Real time (s): 1210.16
CPU time (s): 1209.1
CPU user time (s): 1208.12
CPU system time (s): 0.978851
CPU usage (%): 99.9123
Max. virtual memory (cumulated for all children) (Kb): 59400