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/9144/stat): 9144 (minisat+_script) R 9143 9144 15400 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1796516354 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/9144/statm): 174 3 169 147 0 27 0
[pid=9144] 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=9145
New process pid=9146
New process pid=9147
execve syscall for /bin/sed executable
One traced child (pid=9146) 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=9147) exited with status: 0
One traced child (pid=9145) exited with status: 0
New process pid=9148
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-bg512142.opb

[startup+10.0033 s]
Raw data (loadavg): 0.93 0.97 0.91 1/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) T 9144 9144 15400 0 -1 0 13444 0 0 0 886 61 0 0 23 0 1 0 1796516358 53444608 12019 4294967295 134512640 135094434 3221224432 3221205724 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/9148/statm): 13048 12019 145 145 0 12903 0
[pid=9148] vsize: 52192
Current children cumulated CPU time (s) 9.48
Current children cumulated vsize (Kb) 54316

[startup+20.004 s]
Raw data (loadavg): 0.94 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 34809 0 0 0 1699 150 0 0 25 0 1 0 1796516358 150925312 33384 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9148/statm): 36847 33384 145 145 0 36702 0
[pid=9148] vsize: 147388
Current children cumulated CPU time (s) 18.5
Current children cumulated vsize (Kb) 149512

[startup+30.0046 s]
Raw data (loadavg): 0.95 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 34809 0 0 0 2699 151 0 0 25 0 1 0 1796516358 150925312 33384 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9148/statm): 36847 33384 145 145 0 36702 0
[pid=9148] vsize: 147388
Current children cumulated CPU time (s) 28.51
Current children cumulated vsize (Kb) 149512

[startup+40.0052 s]
Raw data (loadavg): 0.95 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 34811 0 0 0 3699 151 0 0 25 0 1 0 1796516358 150933504 33386 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 36849 33386 145 145 0 36704 0
[pid=9148] vsize: 147396
Current children cumulated CPU time (s) 38.51
Current children cumulated vsize (Kb) 149520

[startup+50.0058 s]
Raw data (loadavg): 0.96 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 34830 0 0 0 4698 151 0 0 25 0 1 0 1796516358 151011328 33405 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 36868 33405 145 145 0 36723 0
[pid=9148] vsize: 147472
Current children cumulated CPU time (s) 48.5
Current children cumulated vsize (Kb) 149596

[startup+60.0055 s]
Raw data (loadavg): 0.97 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 34848 0 0 0 5698 152 0 0 25 0 1 0 1796516358 151085056 33423 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 36886 33423 145 145 0 36741 0
[pid=9148] vsize: 147544
Current children cumulated CPU time (s) 58.51
Current children cumulated vsize (Kb) 149668

[startup+70.0061 s]
Raw data (loadavg): 0.97 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 34864 0 0 0 6697 152 0 0 25 0 1 0 1796516358 151150592 33439 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9148/statm): 36902 33439 145 145 0 36757 0
[pid=9148] vsize: 147608
Current children cumulated CPU time (s) 68.5
Current children cumulated vsize (Kb) 149732

[startup+80.0068 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 34885 0 0 0 7696 153 0 0 25 0 1 0 1796516358 151236608 33460 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9148/statm): 36923 33460 145 145 0 36778 0
[pid=9148] vsize: 147692
Current children cumulated CPU time (s) 78.5
Current children cumulated vsize (Kb) 149816

[startup+90.0084 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 34894 0 0 0 8695 153 0 0 25 0 1 0 1796516358 151273472 33469 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 36932 33469 145 145 0 36787 0
[pid=9148] vsize: 147728
Current children cumulated CPU time (s) 88.49
Current children cumulated vsize (Kb) 149852

[startup+100.009 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 34937 0 0 0 9695 153 0 0 25 0 1 0 1796516358 151379968 33512 4294967295 134512640 135094434 3221224432 3221223136 134558968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 36958 33512 145 145 0 36813 0
[pid=9148] vsize: 147832
Current children cumulated CPU time (s) 98.49
Current children cumulated vsize (Kb) 149956

[startup+110.01 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 34951 0 0 0 10695 153 0 0 25 0 1 0 1796516358 151433216 33526 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 36971 33526 145 145 0 36826 0
[pid=9148] vsize: 147884
Current children cumulated CPU time (s) 108.49
Current children cumulated vsize (Kb) 150008

[startup+120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 34958 0 0 0 11695 153 0 0 25 0 1 0 1796516358 151461888 33533 4294967295 134512640 135094434 3221224432 3221223112 134553433 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 36978 33533 145 145 0 36833 0
[pid=9148] vsize: 147912
Current children cumulated CPU time (s) 118.49
Current children cumulated vsize (Kb) 150036

[startup+130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 34962 0 0 0 12694 153 0 0 25 0 1 0 1796516358 151478272 33537 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 36982 33537 145 145 0 36837 0
[pid=9148] vsize: 147928
Current children cumulated CPU time (s) 128.48
Current children cumulated vsize (Kb) 150052

[startup+140.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 34968 0 0 0 13695 153 0 0 25 0 1 0 1796516358 151498752 33543 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 36987 33543 145 145 0 36842 0
[pid=9148] vsize: 147948
Current children cumulated CPU time (s) 138.49
Current children cumulated vsize (Kb) 150072

[startup+150.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 34974 0 0 0 14695 154 0 0 25 0 1 0 1796516358 151523328 33549 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 36993 33549 145 145 0 36848 0
[pid=9148] vsize: 147972
Current children cumulated CPU time (s) 148.5
Current children cumulated vsize (Kb) 150096

[startup+160.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 34983 0 0 0 15695 154 0 0 25 0 1 0 1796516358 151560192 33558 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37002 33558 145 145 0 36857 0
[pid=9148] vsize: 148008
Current children cumulated CPU time (s) 158.5
Current children cumulated vsize (Kb) 150132

[startup+170.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 34990 0 0 0 16695 154 0 0 25 0 1 0 1796516358 151588864 33565 4294967295 134512640 135094434 3221224432 3221223116 134553526 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37009 33565 145 145 0 36864 0
[pid=9148] vsize: 148036
Current children cumulated CPU time (s) 168.5
Current children cumulated vsize (Kb) 150160

[startup+180.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 34994 0 0 0 17695 154 0 0 25 0 1 0 1796516358 151605248 33569 4294967295 134512640 135094434 3221224432 3221223092 134553450 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37013 33569 145 145 0 36868 0
[pid=9148] vsize: 148052
Current children cumulated CPU time (s) 178.5
Current children cumulated vsize (Kb) 150176

[startup+190.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35001 0 0 0 18695 154 0 0 25 0 1 0 1796516358 151633920 33576 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37020 33576 145 145 0 36875 0
[pid=9148] vsize: 148080
Current children cumulated CPU time (s) 188.5
Current children cumulated vsize (Kb) 150204

[startup+200.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35027 0 0 0 19695 154 0 0 25 0 1 0 1796516358 151670784 33602 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37029 33602 145 145 0 36884 0
[pid=9148] vsize: 148116
Current children cumulated CPU time (s) 198.5
Current children cumulated vsize (Kb) 150240

[startup+210.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35044 0 0 0 20695 154 0 0 25 0 1 0 1796516358 151744512 33619 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37047 33619 145 145 0 36902 0
[pid=9148] vsize: 148188
Current children cumulated CPU time (s) 208.5
Current children cumulated vsize (Kb) 150312

[startup+220.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35048 0 0 0 21695 154 0 0 25 0 1 0 1796516358 151760896 33623 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37051 33623 145 145 0 36906 0
[pid=9148] vsize: 148204
Current children cumulated CPU time (s) 218.5
Current children cumulated vsize (Kb) 150328

[startup+230.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35052 0 0 0 22695 154 0 0 25 0 1 0 1796516358 151777280 33627 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37055 33627 145 145 0 36910 0
[pid=9148] vsize: 148220
Current children cumulated CPU time (s) 228.5
Current children cumulated vsize (Kb) 150344

[startup+240.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35076 0 0 0 23695 155 0 0 25 0 1 0 1796516358 151871488 33651 4294967295 134512640 135094434 3221224432 3221223104 134553437 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37078 33651 145 145 0 36933 0
[pid=9148] vsize: 148312
Current children cumulated CPU time (s) 238.51
Current children cumulated vsize (Kb) 150436

[startup+250.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35082 0 0 0 24695 155 0 0 25 0 1 0 1796516358 151896064 33657 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37084 33657 145 145 0 36939 0
[pid=9148] vsize: 148336
Current children cumulated CPU time (s) 248.51
Current children cumulated vsize (Kb) 150460

[startup+260.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35117 0 0 0 25695 155 0 0 25 0 1 0 1796516358 151941120 33692 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37095 33692 145 145 0 36950 0
[pid=9148] vsize: 148380
Current children cumulated CPU time (s) 258.51
Current children cumulated vsize (Kb) 150504

[startup+270.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35125 0 0 0 26695 155 0 0 25 0 1 0 1796516358 151969792 33700 4294967295 134512640 135094434 3221224432 3221223092 134553489 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37102 33700 145 145 0 36957 0
[pid=9148] vsize: 148408
Current children cumulated CPU time (s) 268.51
Current children cumulated vsize (Kb) 150532

[startup+280.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35135 0 0 0 27695 155 0 0 25 0 1 0 1796516358 152010752 33710 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37112 33710 145 145 0 36967 0
[pid=9148] vsize: 148448
Current children cumulated CPU time (s) 278.51
Current children cumulated vsize (Kb) 150572

[startup+290.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35136 0 0 0 28695 155 0 0 25 0 1 0 1796516358 152014848 33711 4294967295 134512640 135094434 3221224432 3221223136 134559010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37113 33711 145 145 0 36968 0
[pid=9148] vsize: 148452
Current children cumulated CPU time (s) 288.51
Current children cumulated vsize (Kb) 150576

[startup+300.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35144 0 0 0 29695 155 0 0 25 0 1 0 1796516358 152043520 33719 4294967295 134512640 135094434 3221224432 3221223092 134553450 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37120 33719 145 145 0 36975 0
[pid=9148] vsize: 148480
Current children cumulated CPU time (s) 298.51
Current children cumulated vsize (Kb) 150604

[startup+310.016 s]
Raw data (loadavg): 0.99 0.97 0.91 3/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35182 0 0 0 30694 156 0 0 25 0 1 0 1796516358 152117248 33757 4294967295 134512640 135094434 3221224432 3221223092 134553494 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37138 33757 145 145 0 36993 0
[pid=9148] vsize: 148552
Current children cumulated CPU time (s) 308.51
Current children cumulated vsize (Kb) 150676

[startup+320.017 s]
Raw data (loadavg): 0.99 0.97 0.91 3/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35187 0 0 0 31694 156 0 0 25 0 1 0 1796516358 152137728 33762 4294967295 134512640 135094434 3221224432 3221223112 134553433 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37143 33762 145 145 0 36998 0
[pid=9148] vsize: 148572
Current children cumulated CPU time (s) 318.51
Current children cumulated vsize (Kb) 150696

[startup+330.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35190 0 0 0 32694 156 0 0 25 0 1 0 1796516358 152150016 33765 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37146 33765 145 145 0 37001 0
[pid=9148] vsize: 148584
Current children cumulated CPU time (s) 328.51
Current children cumulated vsize (Kb) 150708

[startup+340.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35200 0 0 0 33694 156 0 0 25 0 1 0 1796516358 152215552 33775 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37162 33775 145 145 0 37017 0
[pid=9148] vsize: 148648
Current children cumulated CPU time (s) 338.51
Current children cumulated vsize (Kb) 150772

[startup+350.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35203 0 0 0 34694 156 0 0 25 0 1 0 1796516358 152227840 33778 4294967295 134512640 135094434 3221224432 3221223092 134553454 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37165 33778 145 145 0 37020 0
[pid=9148] vsize: 148660
Current children cumulated CPU time (s) 348.51
Current children cumulated vsize (Kb) 150784

[startup+360.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35233 0 0 0 35694 157 0 0 25 0 1 0 1796516358 152285184 33808 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37179 33808 145 145 0 37034 0
[pid=9148] vsize: 148716
Current children cumulated CPU time (s) 358.52
Current children cumulated vsize (Kb) 150840

[startup+370.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35235 0 0 0 36694 157 0 0 25 0 1 0 1796516358 152293376 33810 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37181 33810 145 145 0 37036 0
[pid=9148] vsize: 148724
Current children cumulated CPU time (s) 368.52
Current children cumulated vsize (Kb) 150848

[startup+380.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35237 0 0 0 37694 157 0 0 25 0 1 0 1796516358 152301568 33812 4294967295 134512640 135094434 3221224432 3221223092 134553454 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9148/statm): 37183 33812 145 145 0 37038 0
[pid=9148] vsize: 148732
Current children cumulated CPU time (s) 378.52
Current children cumulated vsize (Kb) 150856

[startup+390.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35239 0 0 0 38694 157 0 0 25 0 1 0 1796516358 152305664 33814 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37184 33814 145 145 0 37039 0
[pid=9148] vsize: 148736
Current children cumulated CPU time (s) 388.52
Current children cumulated vsize (Kb) 150860

[startup+400.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35241 0 0 0 39694 157 0 0 25 0 1 0 1796516358 152313856 33816 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37186 33816 145 145 0 37041 0
[pid=9148] vsize: 148744
Current children cumulated CPU time (s) 398.52
Current children cumulated vsize (Kb) 150868

[startup+410.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35242 0 0 0 40694 157 0 0 25 0 1 0 1796516358 152317952 33817 4294967295 134512640 135094434 3221224432 3221223136 134559019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37187 33817 145 145 0 37042 0
[pid=9148] vsize: 148748
Current children cumulated CPU time (s) 408.52
Current children cumulated vsize (Kb) 150872

[startup+420.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35244 0 0 0 41694 157 0 0 25 0 1 0 1796516358 152326144 33819 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37189 33819 145 145 0 37044 0
[pid=9148] vsize: 148756
Current children cumulated CPU time (s) 418.52
Current children cumulated vsize (Kb) 150880

[startup+430.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35245 0 0 0 42694 157 0 0 25 0 1 0 1796516358 152330240 33820 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37190 33820 145 145 0 37045 0
[pid=9148] vsize: 148760
Current children cumulated CPU time (s) 428.52
Current children cumulated vsize (Kb) 150884

[startup+440.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35248 0 0 0 43694 157 0 0 25 0 1 0 1796516358 152338432 33823 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37192 33823 145 145 0 37047 0
[pid=9148] vsize: 148768
Current children cumulated CPU time (s) 438.52
Current children cumulated vsize (Kb) 150892

[startup+450.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35252 0 0 0 44694 157 0 0 25 0 1 0 1796516358 152354816 33827 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37196 33827 145 145 0 37051 0
[pid=9148] vsize: 148784
Current children cumulated CPU time (s) 448.52
Current children cumulated vsize (Kb) 150908

[startup+460.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35254 0 0 0 45695 157 0 0 25 0 1 0 1796516358 152363008 33829 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37198 33829 145 145 0 37053 0
[pid=9148] vsize: 148792
Current children cumulated CPU time (s) 458.53
Current children cumulated vsize (Kb) 150916

[startup+470.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35303 0 0 0 46695 157 0 0 25 0 1 0 1796516358 152432640 33878 4294967295 134512640 135094434 3221224432 3221223116 134553526 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37215 33878 145 145 0 37070 0
[pid=9148] vsize: 148860
Current children cumulated CPU time (s) 468.53
Current children cumulated vsize (Kb) 150984

[startup+480.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35309 0 0 0 47695 157 0 0 25 0 1 0 1796516358 152457216 33884 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37221 33884 145 145 0 37076 0
[pid=9148] vsize: 148884
Current children cumulated CPU time (s) 478.53
Current children cumulated vsize (Kb) 151008

[startup+490.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35316 0 0 0 48695 157 0 0 25 0 1 0 1796516358 152481792 33891 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37227 33891 145 145 0 37082 0
[pid=9148] vsize: 148908
Current children cumulated CPU time (s) 488.53
Current children cumulated vsize (Kb) 151032

[startup+500.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35319 0 0 0 49695 157 0 0 25 0 1 0 1796516358 152494080 33894 4294967295 134512640 135094434 3221224432 3221223136 134558968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37230 33894 145 145 0 37085 0
[pid=9148] vsize: 148920
Current children cumulated CPU time (s) 498.53
Current children cumulated vsize (Kb) 151044

[startup+510.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35326 0 0 0 50695 157 0 0 25 0 1 0 1796516358 152522752 33901 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37237 33901 145 145 0 37092 0
[pid=9148] vsize: 148948
Current children cumulated CPU time (s) 508.53
Current children cumulated vsize (Kb) 151072

[startup+520.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35334 0 0 0 51695 157 0 0 25 0 1 0 1796516358 152551424 33909 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37244 33909 145 145 0 37099 0
[pid=9148] vsize: 148976
Current children cumulated CPU time (s) 518.53
Current children cumulated vsize (Kb) 151100

[startup+530.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35341 0 0 0 52695 157 0 0 25 0 1 0 1796516358 152580096 33916 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37251 33916 145 145 0 37106 0
[pid=9148] vsize: 149004
Current children cumulated CPU time (s) 528.53
Current children cumulated vsize (Kb) 151128

[startup+540.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35352 0 0 0 53695 158 0 0 25 0 1 0 1796516358 152621056 33927 4294967295 134512640 135094434 3221224432 3221223112 134553433 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37261 33927 145 145 0 37116 0
[pid=9148] vsize: 149044
Current children cumulated CPU time (s) 538.54
Current children cumulated vsize (Kb) 151168

[startup+550.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35357 0 0 0 54695 158 0 0 25 0 1 0 1796516358 152641536 33932 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37266 33932 145 145 0 37121 0
[pid=9148] vsize: 149064
Current children cumulated CPU time (s) 548.54
Current children cumulated vsize (Kb) 151188

[startup+560.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35364 0 0 0 55695 158 0 0 25 0 1 0 1796516358 152670208 33939 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37273 33939 145 145 0 37128 0
[pid=9148] vsize: 149092
Current children cumulated CPU time (s) 558.54
Current children cumulated vsize (Kb) 151216

[startup+570.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35392 0 0 0 56695 158 0 0 25 0 1 0 1796516358 152846336 33967 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37316 33967 145 145 0 37171 0
[pid=9148] vsize: 149264
Current children cumulated CPU time (s) 568.54
Current children cumulated vsize (Kb) 151388

[startup+580.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35393 0 0 0 57695 158 0 0 25 0 1 0 1796516358 152846336 33968 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37316 33968 145 145 0 37171 0
[pid=9148] vsize: 149264
Current children cumulated CPU time (s) 578.54
Current children cumulated vsize (Kb) 151388

[startup+590.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35395 0 0 0 58695 158 0 0 25 0 1 0 1796516358 152850432 33970 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37317 33970 145 145 0 37172 0
[pid=9148] vsize: 149268
Current children cumulated CPU time (s) 588.54
Current children cumulated vsize (Kb) 151392

[startup+600.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35409 0 0 0 59696 158 0 0 25 0 1 0 1796516358 152903680 33984 4294967295 134512640 135094434 3221224432 3221223056 134557587 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37330 33984 145 145 0 37185 0
[pid=9148] vsize: 149320
Current children cumulated CPU time (s) 598.55
Current children cumulated vsize (Kb) 151444

[startup+610.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35416 0 0 0 60695 159 0 0 25 0 1 0 1796516358 152932352 33991 4294967295 134512640 135094434 3221224432 3221223104 134553523 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37337 33991 145 145 0 37192 0
[pid=9148] vsize: 149348
Current children cumulated CPU time (s) 608.55
Current children cumulated vsize (Kb) 151472

[startup+620.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35420 0 0 0 61694 160 0 0 25 0 1 0 1796516358 152948736 33995 4294967295 134512640 135094434 3221224432 3221223092 134553489 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9148/statm): 37341 33995 145 145 0 37196 0
[pid=9148] vsize: 149364
Current children cumulated CPU time (s) 618.55
Current children cumulated vsize (Kb) 151488

[startup+630.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35431 0 0 0 62693 160 0 0 25 0 1 0 1796516358 152989696 34006 4294967295 134512640 135094434 3221224432 3221223104 134553523 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37351 34006 145 145 0 37206 0
[pid=9148] vsize: 149404
Current children cumulated CPU time (s) 628.54
Current children cumulated vsize (Kb) 151528

[startup+640.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35435 0 0 0 63693 160 0 0 25 0 1 0 1796516358 153006080 34010 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37355 34010 145 145 0 37210 0
[pid=9148] vsize: 149420
Current children cumulated CPU time (s) 638.54
Current children cumulated vsize (Kb) 151544

[startup+650.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35453 0 0 0 64693 160 0 0 25 0 1 0 1796516358 153075712 34028 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37372 34028 145 145 0 37227 0
[pid=9148] vsize: 149488
Current children cumulated CPU time (s) 648.54
Current children cumulated vsize (Kb) 151612

[startup+660.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35458 0 0 0 65693 161 0 0 25 0 1 0 1796516358 153096192 34033 4294967295 134512640 135094434 3221224432 3221223088 134561717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37377 34033 145 145 0 37232 0
[pid=9148] vsize: 149508
Current children cumulated CPU time (s) 658.55
Current children cumulated vsize (Kb) 151632

[startup+670.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35485 0 0 0 66693 161 0 0 25 0 1 0 1796516358 153141248 34060 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37388 34060 145 145 0 37243 0
[pid=9148] vsize: 149552
Current children cumulated CPU time (s) 668.55
Current children cumulated vsize (Kb) 151676

[startup+680.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35487 0 0 0 67693 161 0 0 25 0 1 0 1796516358 153149440 34062 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37390 34062 145 145 0 37245 0
[pid=9148] vsize: 149560
Current children cumulated CPU time (s) 678.55
Current children cumulated vsize (Kb) 151684

[startup+690.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35506 0 0 0 68693 161 0 0 25 0 1 0 1796516358 153202688 34081 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37403 34081 145 145 0 37258 0
[pid=9148] vsize: 149612
Current children cumulated CPU time (s) 688.55
Current children cumulated vsize (Kb) 151736

[startup+700.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35508 0 0 0 69693 161 0 0 25 0 1 0 1796516358 153210880 34083 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37405 34083 145 145 0 37260 0
[pid=9148] vsize: 149620
Current children cumulated CPU time (s) 698.55
Current children cumulated vsize (Kb) 151744

[startup+710.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35516 0 0 0 70694 161 0 0 25 0 1 0 1796516358 153239552 34091 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37412 34091 145 145 0 37267 0
[pid=9148] vsize: 149648
Current children cumulated CPU time (s) 708.56
Current children cumulated vsize (Kb) 151772

[startup+720.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35530 0 0 0 71693 162 0 0 25 0 1 0 1796516358 153292800 34105 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9148/statm): 37425 34105 145 145 0 37280 0
[pid=9148] vsize: 149700
Current children cumulated CPU time (s) 718.56
Current children cumulated vsize (Kb) 151824

[startup+730.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35536 0 0 0 72692 162 0 0 25 0 1 0 1796516358 153317376 34111 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37431 34111 145 145 0 37286 0
[pid=9148] vsize: 149724
Current children cumulated CPU time (s) 728.55
Current children cumulated vsize (Kb) 151848

[startup+740.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35554 0 0 0 73692 162 0 0 25 0 1 0 1796516358 153387008 34129 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37448 34129 145 145 0 37303 0
[pid=9148] vsize: 149792
Current children cumulated CPU time (s) 738.55
Current children cumulated vsize (Kb) 151916

[startup+750.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35875 0 0 0 74688 164 0 0 25 0 1 0 1796516358 154677248 34450 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37763 34450 145 145 0 37618 0
[pid=9148] vsize: 151052
Current children cumulated CPU time (s) 748.53
Current children cumulated vsize (Kb) 153176

[startup+760.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35888 0 0 0 75688 164 0 0 25 0 1 0 1796516358 154726400 34463 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37775 34463 145 145 0 37630 0
[pid=9148] vsize: 151100
Current children cumulated CPU time (s) 758.53
Current children cumulated vsize (Kb) 153224

[startup+770.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35905 0 0 0 76688 164 0 0 25 0 1 0 1796516358 154796032 34480 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37792 34480 145 145 0 37647 0
[pid=9148] vsize: 151168
Current children cumulated CPU time (s) 768.53
Current children cumulated vsize (Kb) 153292

[startup+780.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35912 0 0 0 77688 164 0 0 25 0 1 0 1796516358 154824704 34487 4294967295 134512640 135094434 3221224432 3221223136 134558999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37799 34487 145 145 0 37654 0
[pid=9148] vsize: 151196
Current children cumulated CPU time (s) 778.53
Current children cumulated vsize (Kb) 153320

[startup+790.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35947 0 0 0 78688 164 0 0 25 0 1 0 1796516358 155095040 34522 4294967295 134512640 135094434 3221224432 3221223056 134557598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37865 34522 145 145 0 37720 0
[pid=9148] vsize: 151460
Current children cumulated CPU time (s) 788.53
Current children cumulated vsize (Kb) 153584

[startup+800.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35948 0 0 0 79688 165 0 0 25 0 1 0 1796516358 155095040 34523 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37865 34523 145 145 0 37720 0
[pid=9148] vsize: 151460
Current children cumulated CPU time (s) 798.54
Current children cumulated vsize (Kb) 153584

[startup+810.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35948 0 0 0 80688 165 0 0 25 0 1 0 1796516358 155095040 34523 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37865 34523 145 145 0 37720 0
[pid=9148] vsize: 151460
Current children cumulated CPU time (s) 808.54
Current children cumulated vsize (Kb) 153584

[startup+820.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35950 0 0 0 81689 165 0 0 25 0 1 0 1796516358 155099136 34525 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37866 34525 145 145 0 37721 0
[pid=9148] vsize: 151464
Current children cumulated CPU time (s) 818.55
Current children cumulated vsize (Kb) 153588

[startup+830.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35961 0 0 0 82689 165 0 0 25 0 1 0 1796516358 155144192 34536 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37877 34536 145 145 0 37732 0
[pid=9148] vsize: 151508
Current children cumulated CPU time (s) 828.55
Current children cumulated vsize (Kb) 153632

[startup+840.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35966 0 0 0 83689 165 0 0 25 0 1 0 1796516358 155160576 34541 4294967295 134512640 135094434 3221224432 3221223136 134559002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37881 34541 145 145 0 37736 0
[pid=9148] vsize: 151524
Current children cumulated CPU time (s) 838.55
Current children cumulated vsize (Kb) 153648

[startup+850.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 35973 0 0 0 84689 165 0 0 25 0 1 0 1796516358 155189248 34548 4294967295 134512640 135094434 3221224432 3221223044 134563089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37888 34548 145 145 0 37743 0
[pid=9148] vsize: 151552
Current children cumulated CPU time (s) 848.55
Current children cumulated vsize (Kb) 153676

[startup+860.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 36010 0 0 0 85689 165 0 0 25 0 1 0 1796516358 155336704 34585 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37924 34585 145 145 0 37779 0
[pid=9148] vsize: 151696
Current children cumulated CPU time (s) 858.55
Current children cumulated vsize (Kb) 153820

[startup+870.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 36023 0 0 0 86689 165 0 0 25 0 1 0 1796516358 155385856 34598 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37936 34598 145 145 0 37791 0
[pid=9148] vsize: 151744
Current children cumulated CPU time (s) 868.55
Current children cumulated vsize (Kb) 153868

[startup+880.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 36039 0 0 0 87689 165 0 0 25 0 1 0 1796516358 155447296 34614 4294967295 134512640 135094434 3221224432 3221223088 134557843 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 37951 34614 145 145 0 37806 0
[pid=9148] vsize: 151804
Current children cumulated CPU time (s) 878.55
Current children cumulated vsize (Kb) 153928

[startup+890.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 36090 0 0 0 88688 166 0 0 25 0 1 0 1796516358 155648000 34665 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 38000 34665 145 145 0 37855 0
[pid=9148] vsize: 152000
Current children cumulated CPU time (s) 888.55
Current children cumulated vsize (Kb) 154124

[startup+900.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 36111 0 0 0 89687 167 0 0 25 0 1 0 1796516358 155729920 34686 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 38020 34686 145 145 0 37875 0
[pid=9148] vsize: 152080
Current children cumulated CPU time (s) 898.55
Current children cumulated vsize (Kb) 154204

[startup+910.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 36128 0 0 0 90688 167 0 0 25 0 1 0 1796516358 155795456 34703 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 38036 34703 145 145 0 37891 0
[pid=9148] vsize: 152144
Current children cumulated CPU time (s) 908.56
Current children cumulated vsize (Kb) 154268

[startup+920.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 36157 0 0 0 91687 167 0 0 25 0 1 0 1796516358 155910144 34732 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 38064 34732 145 145 0 37919 0
[pid=9148] vsize: 152256
Current children cumulated CPU time (s) 918.55
Current children cumulated vsize (Kb) 154380

[startup+930.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 36166 0 0 0 92687 167 0 0 25 0 1 0 1796516358 155947008 34741 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 38073 34741 145 145 0 37928 0
[pid=9148] vsize: 152292
Current children cumulated CPU time (s) 928.55
Current children cumulated vsize (Kb) 154416

[startup+940.065 s]
Raw data (loadavg): 1.06 0.99 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 36277 0 0 0 93686 168 0 0 25 0 1 0 1796516358 156389376 34852 4294967295 134512640 135094434 3221224432 3221223100 134553438 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 38181 34852 145 145 0 38036 0
[pid=9148] vsize: 152724
Current children cumulated CPU time (s) 938.55
Current children cumulated vsize (Kb) 154848

[startup+950.066 s]
Raw data (loadavg): 1.05 0.99 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 36281 0 0 0 94686 168 0 0 25 0 1 0 1796516358 156405760 34856 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 38185 34856 145 145 0 38040 0
[pid=9148] vsize: 152740
Current children cumulated CPU time (s) 948.55
Current children cumulated vsize (Kb) 154864

[startup+960.067 s]
Raw data (loadavg): 1.04 0.99 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 36395 0 0 0 95685 168 0 0 25 0 1 0 1796516358 156856320 34970 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 38295 34970 145 145 0 38150 0
[pid=9148] vsize: 153180
Current children cumulated CPU time (s) 958.54
Current children cumulated vsize (Kb) 155304

[startup+970.067 s]
Raw data (loadavg): 1.04 0.99 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 36404 0 0 0 96685 169 0 0 25 0 1 0 1796516358 156893184 34979 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 38304 34979 145 145 0 38159 0
[pid=9148] vsize: 153216
Current children cumulated CPU time (s) 968.55
Current children cumulated vsize (Kb) 155340

[startup+980.068 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 36435 0 0 0 97684 169 0 0 25 0 1 0 1796516358 157016064 35010 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 38334 35010 145 145 0 38189 0
[pid=9148] vsize: 153336
Current children cumulated CPU time (s) 978.54
Current children cumulated vsize (Kb) 155460

[startup+990.069 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 36447 0 0 0 98685 169 0 0 25 0 1 0 1796516358 157061120 35022 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 38345 35022 145 145 0 38200 0
[pid=9148] vsize: 153380
Current children cumulated CPU time (s) 988.55
Current children cumulated vsize (Kb) 155504

[startup+1000.07 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 36450 0 0 0 99684 169 0 0 25 0 1 0 1796516358 157073408 35025 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9148/statm): 38348 35025 145 145 0 38203 0
[pid=9148] vsize: 153392
Current children cumulated CPU time (s) 998.54
Current children cumulated vsize (Kb) 155516

[startup+1010.07 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 36456 0 0 0 100683 169 0 0 25 0 1 0 1796516358 157093888 35031 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 38353 35031 145 145 0 38208 0
[pid=9148] vsize: 153412
Current children cumulated CPU time (s) 1008.53
Current children cumulated vsize (Kb) 155536

[startup+1020.07 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 36483 0 0 0 101683 170 0 0 25 0 1 0 1796516358 157200384 35058 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 38379 35058 145 145 0 38234 0
[pid=9148] vsize: 153516
Current children cumulated CPU time (s) 1018.54
Current children cumulated vsize (Kb) 155640

[startup+1030.07 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 36560 0 0 0 102681 171 0 0 25 0 1 0 1796516358 157507584 35135 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 38454 35135 145 145 0 38309 0
[pid=9148] vsize: 153816
Current children cumulated CPU time (s) 1028.53
Current children cumulated vsize (Kb) 155940

[startup+1040.07 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 36640 0 0 0 103680 172 0 0 25 0 1 0 1796516358 157831168 35215 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 38533 35215 145 145 0 38388 0
[pid=9148] vsize: 154132
Current children cumulated CPU time (s) 1038.53
Current children cumulated vsize (Kb) 156256

[startup+1050.07 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 36649 0 0 0 104680 172 0 0 25 0 1 0 1796516358 157863936 35224 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 38541 35224 145 145 0 38396 0
[pid=9148] vsize: 154164
Current children cumulated CPU time (s) 1048.53
Current children cumulated vsize (Kb) 156288

[startup+1060.07 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 36666 0 0 0 105680 172 0 0 25 0 1 0 1796516358 157933568 35241 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 38558 35241 145 145 0 38413 0
[pid=9148] vsize: 154232
Current children cumulated CPU time (s) 1058.53
Current children cumulated vsize (Kb) 156356

[startup+1070.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 36681 0 0 0 106680 172 0 0 25 0 1 0 1796516358 157990912 35256 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 38572 35256 145 145 0 38427 0
[pid=9148] vsize: 154288
Current children cumulated CPU time (s) 1068.53
Current children cumulated vsize (Kb) 156412

[startup+1080.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 36697 0 0 0 107680 172 0 0 25 0 1 0 1796516358 158052352 35272 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 38587 35272 145 145 0 38442 0
[pid=9148] vsize: 154348
Current children cumulated CPU time (s) 1078.53
Current children cumulated vsize (Kb) 156472

[startup+1090.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 36721 0 0 0 108680 172 0 0 25 0 1 0 1796516358 158146560 35296 4294967295 134512640 135094434 3221224432 3221223044 134563101 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 38610 35296 145 145 0 38465 0
[pid=9148] vsize: 154440
Current children cumulated CPU time (s) 1088.53
Current children cumulated vsize (Kb) 156564

[startup+1100.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 36741 0 0 0 109680 173 0 0 25 0 1 0 1796516358 158224384 35316 4294967295 134512640 135094434 3221224432 3221223044 134563061 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 38629 35316 145 145 0 38484 0
[pid=9148] vsize: 154516
Current children cumulated CPU time (s) 1098.54
Current children cumulated vsize (Kb) 156640

[startup+1110.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 36756 0 0 0 110680 173 0 0 25 0 1 0 1796516358 158281728 35331 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 38643 35331 145 145 0 38498 0
[pid=9148] vsize: 154572
Current children cumulated CPU time (s) 1108.54
Current children cumulated vsize (Kb) 156696

[startup+1120.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 36773 0 0 0 111680 173 0 0 25 0 1 0 1796516358 158609408 35348 4294967295 134512640 135094434 3221224432 3221223044 134563110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 38723 35348 145 145 0 38578 0
[pid=9148] vsize: 154892
Current children cumulated CPU time (s) 1118.54
Current children cumulated vsize (Kb) 157016

[startup+1130.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 36806 0 0 0 112679 173 0 0 25 0 1 0 1796516358 158740480 35381 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 38755 35381 145 145 0 38610 0
[pid=9148] vsize: 155020
Current children cumulated CPU time (s) 1128.53
Current children cumulated vsize (Kb) 157144

[startup+1140.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 36824 0 0 0 113679 173 0 0 25 0 1 0 1796516358 158810112 35399 4294967295 134512640 135094434 3221224432 3221223068 134557639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 38772 35399 145 145 0 38627 0
[pid=9148] vsize: 155088
Current children cumulated CPU time (s) 1138.53
Current children cumulated vsize (Kb) 157212

[startup+1150.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 36851 0 0 0 114679 174 0 0 25 0 1 0 1796516358 158916608 35426 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 38798 35426 145 145 0 38653 0
[pid=9148] vsize: 155192
Current children cumulated CPU time (s) 1148.54
Current children cumulated vsize (Kb) 157316

[startup+1160.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 36879 0 0 0 115678 174 0 0 25 0 1 0 1796516358 159027200 35454 4294967295 134512640 135094434 3221224432 3221223092 134553466 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 38825 35454 145 145 0 38680 0
[pid=9148] vsize: 155300
Current children cumulated CPU time (s) 1158.53
Current children cumulated vsize (Kb) 157424

[startup+1170.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 36891 0 0 0 116678 174 0 0 25 0 1 0 1796516358 159072256 35466 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 38836 35466 145 145 0 38691 0
[pid=9148] vsize: 155344
Current children cumulated CPU time (s) 1168.53
Current children cumulated vsize (Kb) 157468

[startup+1180.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 36909 0 0 0 117678 175 0 0 25 0 1 0 1796516358 159141888 35484 4294967295 134512640 135094434 3221224432 3221223136 134558970 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 38853 35484 145 145 0 38708 0
[pid=9148] vsize: 155412
Current children cumulated CPU time (s) 1178.54
Current children cumulated vsize (Kb) 157536

[startup+1190.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 37038 0 0 0 118676 175 0 0 25 0 1 0 1796516358 159662080 35613 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 38980 35613 145 145 0 38835 0
[pid=9148] vsize: 155920
Current children cumulated CPU time (s) 1188.52
Current children cumulated vsize (Kb) 158044

[startup+1200.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 37094 0 0 0 119676 176 0 0 25 0 1 0 1796516358 159883264 35669 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 39034 35669 145 145 0 38889 0
[pid=9148] vsize: 156136
Current children cumulated CPU time (s) 1198.53
Current children cumulated vsize (Kb) 158260

[startup+1210.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 37267 0 0 0 120673 177 0 0 25 0 1 0 1796516358 160571392 35842 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 39202 35842 145 145 0 39057 0
[pid=9148] vsize: 156808
Current children cumulated CPU time (s) 1208.51
Current children cumulated vsize (Kb) 158932



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9148
Raw data (/proc/9144/stat): 9144 (minisat+_script) S 9143 9144 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1796516354 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9144/statm): 531 226 485 147 0 384 0
[pid=9144] vsize: 2124
Raw data (/proc/9148/stat): 9148 (minisat+_64-bit) R 9144 9144 15400 0 -1 0 37267 0 0 0 120673 177 0 0 25 0 1 0 1796516358 160571392 35842 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9148/statm): 39202 35842 145 145 0 39057 0
[pid=9148] vsize: 156808
Current children cumulated CPU time (s) 1208.51
Current children cumulated vsize (Kb) 158932

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

Child status: 0
Real time (s): 1210.16
CPU time (s): 1208.58
CPU user time (s): 1206.73
CPU system time (s): 1.84672
CPU usage (%): 99.8693
Max. virtual memory (cumulated for all children) (Kb): 158932