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/26543/stat): 26543 (minisat+_script) R 26542 26543 4419 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1854885810 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/26543/statm): 174 3 169 147 0 27 0
[pid=26543] 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=26544
New process pid=26545
New process pid=26546
execve syscall for /bin/sed executable
One traced child (pid=26545) 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=26546) exited with status: 0
One traced child (pid=26544) exited with status: 0
New process pid=26547
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-tr12-30.opb

[startup+10.0032 s]
Raw data (loadavg): 0.96 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 14339 0 0 0 870 64 0 0 22 0 1 0 1854885815 63053824 13535 4294967295 134512640 135094434 3221224432 3221199760 134779244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26547/statm): 15394 13535 145 145 0 15249 0
[pid=26547] vsize: 61576
Current children cumulated CPU time (s) 9.34
Current children cumulated vsize (Kb) 63700

[startup+20.0039 s]
Raw data (loadavg): 0.97 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18488 0 0 0 1833 84 0 0 25 0 1 0 1854885815 78856192 17684 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26547/statm): 19252 17684 145 145 0 19107 0
[pid=26547] vsize: 77008
Current children cumulated CPU time (s) 19.17
Current children cumulated vsize (Kb) 79132

[startup+30.0055 s]
Raw data (loadavg): 0.97 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18488 0 0 0 2832 85 0 0 25 0 1 0 1854885815 78856192 17684 4294967295 134512640 135094434 3221224432 3221223092 134553501 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26547/statm): 19252 17684 145 145 0 19107 0
[pid=26547] vsize: 77008
Current children cumulated CPU time (s) 29.17
Current children cumulated vsize (Kb) 79132

[startup+40.0061 s]
Raw data (loadavg): 0.98 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18488 0 0 0 3832 85 0 0 25 0 1 0 1854885815 78856192 17684 4294967295 134512640 135094434 3221224432 3221223068 134557639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26547/statm): 19252 17684 145 145 0 19107 0
[pid=26547] vsize: 77008
Current children cumulated CPU time (s) 39.17
Current children cumulated vsize (Kb) 79132

[startup+50.0077 s]
Raw data (loadavg): 0.98 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18488 0 0 0 4831 86 0 0 25 0 1 0 1854885815 78856192 17684 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26547/statm): 19252 17684 145 145 0 19107 0
[pid=26547] vsize: 77008
Current children cumulated CPU time (s) 49.17
Current children cumulated vsize (Kb) 79132

[startup+60.0083 s]
Raw data (loadavg): 0.98 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18488 0 0 0 5831 86 0 0 25 0 1 0 1854885815 78856192 17684 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26547/statm): 19252 17684 145 145 0 19107 0
[pid=26547] vsize: 77008
Current children cumulated CPU time (s) 59.17
Current children cumulated vsize (Kb) 79132

[startup+70.0089 s]
Raw data (loadavg): 0.98 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18488 0 0 0 6830 87 0 0 25 0 1 0 1854885815 78856192 17684 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26547/statm): 19252 17684 145 145 0 19107 0
[pid=26547] vsize: 77008
Current children cumulated CPU time (s) 69.17
Current children cumulated vsize (Kb) 79132

[startup+80.0105 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18488 0 0 0 7830 88 0 0 25 0 1 0 1854885815 78856192 17684 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26547/statm): 19252 17684 145 145 0 19107 0
[pid=26547] vsize: 77008
Current children cumulated CPU time (s) 79.18
Current children cumulated vsize (Kb) 79132

[startup+90.0111 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18492 0 0 0 8829 88 0 0 25 0 1 0 1854885815 78856192 17688 4294967295 134512640 135094434 3221224432 3221223112 134553433 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26547/statm): 19252 17688 145 145 0 19107 0
[pid=26547] vsize: 77008
Current children cumulated CPU time (s) 89.17
Current children cumulated vsize (Kb) 79132

[startup+100.012 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18493 0 0 0 9829 88 0 0 25 0 1 0 1854885815 78856192 17689 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26547/statm): 19252 17689 145 145 0 19107 0
[pid=26547] vsize: 77008
Current children cumulated CPU time (s) 99.17
Current children cumulated vsize (Kb) 79132

[startup+110.012 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18500 0 0 0 10828 89 0 0 25 0 1 0 1854885815 78872576 17696 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26547/statm): 19256 17696 145 145 0 19111 0
[pid=26547] vsize: 77024
Current children cumulated CPU time (s) 109.17
Current children cumulated vsize (Kb) 79148

[startup+120.013 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18505 0 0 0 11827 90 0 0 25 0 1 0 1854885815 78893056 17701 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26547/statm): 19261 17701 145 145 0 19116 0
[pid=26547] vsize: 77044
Current children cumulated CPU time (s) 119.17
Current children cumulated vsize (Kb) 79168

[startup+130.013 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18526 0 0 0 12827 90 0 0 25 0 1 0 1854885815 78946304 17722 4294967295 134512640 135094434 3221224432 3221223112 134553433 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26547/statm): 19274 17722 145 145 0 19129 0
[pid=26547] vsize: 77096
Current children cumulated CPU time (s) 129.17
Current children cumulated vsize (Kb) 79220

[startup+140.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18529 0 0 0 13826 90 0 0 25 0 1 0 1854885815 78958592 17725 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26547/statm): 19277 17725 145 145 0 19132 0
[pid=26547] vsize: 77108
Current children cumulated CPU time (s) 139.16
Current children cumulated vsize (Kb) 79232

[startup+150.016 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18533 0 0 0 14826 91 0 0 25 0 1 0 1854885815 78979072 17729 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26547/statm): 19282 17729 145 145 0 19137 0
[pid=26547] vsize: 77128
Current children cumulated CPU time (s) 149.17
Current children cumulated vsize (Kb) 79252

[startup+160.016 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18536 0 0 0 15825 91 0 0 25 0 1 0 1854885815 78991360 17732 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26547/statm): 19285 17732 145 145 0 19140 0
[pid=26547] vsize: 77140
Current children cumulated CPU time (s) 159.16
Current children cumulated vsize (Kb) 79264

[startup+170.017 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18538 0 0 0 16825 92 0 0 25 0 1 0 1854885815 78999552 17734 4294967295 134512640 135094434 3221224432 3221223104 134553523 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26547/statm): 19287 17734 145 145 0 19142 0
[pid=26547] vsize: 77148
Current children cumulated CPU time (s) 169.17
Current children cumulated vsize (Kb) 79272

[startup+180.018 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18547 0 0 0 17824 92 0 0 25 0 1 0 1854885815 79015936 17743 4294967295 134512640 135094434 3221224432 3221223044 134563059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26547/statm): 19291 17743 145 145 0 19146 0
[pid=26547] vsize: 77164
Current children cumulated CPU time (s) 179.16
Current children cumulated vsize (Kb) 79288

[startup+190.019 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18550 0 0 0 18824 93 0 0 25 0 1 0 1854885815 79028224 17746 4294967295 134512640 135094434 3221224432 3221223092 134553450 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26547/statm): 19294 17746 145 145 0 19149 0
[pid=26547] vsize: 77176
Current children cumulated CPU time (s) 189.17
Current children cumulated vsize (Kb) 79300

[startup+200.02 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18551 0 0 0 19823 93 0 0 25 0 1 0 1854885815 79032320 17747 4294967295 134512640 135094434 3221224432 3221223092 134553487 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26547/statm): 19295 17747 145 145 0 19150 0
[pid=26547] vsize: 77180
Current children cumulated CPU time (s) 199.16
Current children cumulated vsize (Kb) 79304

[startup+210.02 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18553 0 0 0 20823 94 0 0 25 0 1 0 1854885815 79040512 17749 4294967295 134512640 135094434 3221224432 3221223112 134553433 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26547/statm): 19297 17749 145 145 0 19152 0
[pid=26547] vsize: 77188
Current children cumulated CPU time (s) 209.17
Current children cumulated vsize (Kb) 79312

[startup+220.021 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18553 0 0 0 21823 94 0 0 25 0 1 0 1854885815 79040512 17749 4294967295 134512640 135094434 3221224432 3221223136 134558968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26547/statm): 19297 17749 145 145 0 19152 0
[pid=26547] vsize: 77188
Current children cumulated CPU time (s) 219.17
Current children cumulated vsize (Kb) 79312

[startup+230.022 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18568 0 0 0 22822 95 0 0 25 0 1 0 1854885815 79073280 17764 4294967295 134512640 135094434 3221224432 3221223092 134553454 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26547/statm): 19305 17764 145 145 0 19160 0
[pid=26547] vsize: 77220
Current children cumulated CPU time (s) 229.17
Current children cumulated vsize (Kb) 79344

[startup+240.022 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18590 0 0 0 23821 96 0 0 25 0 1 0 1854885815 79130624 17786 4294967295 134512640 135094434 3221224432 3221223136 134559017 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26547/statm): 19319 17786 145 145 0 19174 0
[pid=26547] vsize: 77276
Current children cumulated CPU time (s) 239.17
Current children cumulated vsize (Kb) 79400

[startup+250.024 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18596 0 0 0 24821 96 0 0 25 0 1 0 1854885815 79163392 17792 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26547/statm): 19327 17792 145 145 0 19182 0
[pid=26547] vsize: 77308
Current children cumulated CPU time (s) 249.17
Current children cumulated vsize (Kb) 79432

[startup+260.024 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18599 0 0 0 25820 97 0 0 25 0 1 0 1854885815 79175680 17795 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26547/statm): 19330 17795 145 145 0 19185 0
[pid=26547] vsize: 77320
Current children cumulated CPU time (s) 259.17
Current children cumulated vsize (Kb) 79444

[startup+270.025 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18601 0 0 0 26819 97 0 0 25 0 1 0 1854885815 79183872 17797 4294967295 134512640 135094434 3221224432 3221223108 134553524 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26547/statm): 19332 17797 145 145 0 19187 0
[pid=26547] vsize: 77328
Current children cumulated CPU time (s) 269.16
Current children cumulated vsize (Kb) 79452

[startup+280.026 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18604 0 0 0 27819 97 0 0 25 0 1 0 1854885815 79196160 17800 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26547/statm): 19335 17800 145 145 0 19190 0
[pid=26547] vsize: 77340
Current children cumulated CPU time (s) 279.16
Current children cumulated vsize (Kb) 79464

[startup+290.026 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18608 0 0 0 28819 97 0 0 25 0 1 0 1854885815 79208448 17804 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26547/statm): 19338 17804 145 145 0 19193 0
[pid=26547] vsize: 77352
Current children cumulated CPU time (s) 289.16
Current children cumulated vsize (Kb) 79476

[startup+300.028 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18613 0 0 0 29818 98 0 0 25 0 1 0 1854885815 79220736 17809 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26547/statm): 19341 17809 145 145 0 19196 0
[pid=26547] vsize: 77364
Current children cumulated CPU time (s) 299.16
Current children cumulated vsize (Kb) 79488

[startup+310.028 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18613 0 0 0 30818 99 0 0 25 0 1 0 1854885815 79220736 17809 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26547/statm): 19341 17809 145 145 0 19196 0
[pid=26547] vsize: 77364
Current children cumulated CPU time (s) 309.17
Current children cumulated vsize (Kb) 79488

[startup+320.029 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18639 0 0 0 31817 100 0 0 25 0 1 0 1854885815 79273984 17835 4294967295 134512640 135094434 3221224432 3221223092 134553489 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26547/statm): 19354 17835 145 145 0 19209 0
[pid=26547] vsize: 77416
Current children cumulated CPU time (s) 319.17
Current children cumulated vsize (Kb) 79540

[startup+330.031 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18644 0 0 0 32817 100 0 0 25 0 1 0 1854885815 79294464 17840 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26547/statm): 19359 17840 145 145 0 19214 0
[pid=26547] vsize: 77436
Current children cumulated CPU time (s) 329.17
Current children cumulated vsize (Kb) 79560

[startup+340.031 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18648 0 0 0 33816 100 0 0 25 0 1 0 1854885815 79310848 17844 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26547/statm): 19363 17844 145 145 0 19218 0
[pid=26547] vsize: 77452
Current children cumulated CPU time (s) 339.16
Current children cumulated vsize (Kb) 79576

[startup+350.032 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18653 0 0 0 34816 100 0 0 25 0 1 0 1854885815 79327232 17849 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26547/statm): 19367 17849 145 145 0 19222 0
[pid=26547] vsize: 77468
Current children cumulated CPU time (s) 349.16
Current children cumulated vsize (Kb) 79592

[startup+360.033 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18656 0 0 0 35815 101 0 0 25 0 1 0 1854885815 79339520 17852 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19370 17852 145 145 0 19225 0
[pid=26547] vsize: 77480
Current children cumulated CPU time (s) 359.16
Current children cumulated vsize (Kb) 79604

[startup+370.034 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18657 0 0 0 36816 101 0 0 25 0 1 0 1854885815 79343616 17853 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19371 17853 145 145 0 19226 0
[pid=26547] vsize: 77484
Current children cumulated CPU time (s) 369.17
Current children cumulated vsize (Kb) 79608

[startup+380.035 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18661 0 0 0 37816 101 0 0 25 0 1 0 1854885815 79355904 17857 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19374 17857 145 145 0 19229 0
[pid=26547] vsize: 77496
Current children cumulated CPU time (s) 379.17
Current children cumulated vsize (Kb) 79620

[startup+390.035 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18663 0 0 0 38816 101 0 0 25 0 1 0 1854885815 79364096 17859 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19376 17859 145 145 0 19231 0
[pid=26547] vsize: 77504
Current children cumulated CPU time (s) 389.17
Current children cumulated vsize (Kb) 79628

[startup+400.037 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18672 0 0 0 39816 101 0 0 25 0 1 0 1854885815 79384576 17868 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19381 17868 145 145 0 19236 0
[pid=26547] vsize: 77524
Current children cumulated CPU time (s) 399.17
Current children cumulated vsize (Kb) 79648

[startup+410.037 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18676 0 0 0 40816 101 0 0 25 0 1 0 1854885815 79400960 17872 4294967295 134512640 135094434 3221224432 3221223136 134558999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19385 17872 145 145 0 19240 0
[pid=26547] vsize: 77540
Current children cumulated CPU time (s) 409.17
Current children cumulated vsize (Kb) 79664

[startup+420.038 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18687 0 0 0 41816 101 0 0 25 0 1 0 1854885815 79470592 17883 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19402 17883 145 145 0 19257 0
[pid=26547] vsize: 77608
Current children cumulated CPU time (s) 419.17
Current children cumulated vsize (Kb) 79732

[startup+430.04 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18687 0 0 0 42816 101 0 0 25 0 1 0 1854885815 79470592 17883 4294967295 134512640 135094434 3221224432 3221223044 134563061 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19402 17883 145 145 0 19257 0
[pid=26547] vsize: 77608
Current children cumulated CPU time (s) 429.17
Current children cumulated vsize (Kb) 79732

[startup+440.04 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18705 0 0 0 43816 101 0 0 25 0 1 0 1854885815 79503360 17901 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19410 17901 145 145 0 19265 0
[pid=26547] vsize: 77640
Current children cumulated CPU time (s) 439.17
Current children cumulated vsize (Kb) 79764

[startup+450.041 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18709 0 0 0 44817 101 0 0 25 0 1 0 1854885815 79515648 17905 4294967295 134512640 135094434 3221224432 3221223120 134558992 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19413 17905 145 145 0 19268 0
[pid=26547] vsize: 77652
Current children cumulated CPU time (s) 449.18
Current children cumulated vsize (Kb) 79776

[startup+460.041 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18712 0 0 0 45817 102 0 0 25 0 1 0 1854885815 79527936 17908 4294967295 134512640 135094434 3221224432 3221223136 134559019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19416 17908 145 145 0 19271 0
[pid=26547] vsize: 77664
Current children cumulated CPU time (s) 459.19
Current children cumulated vsize (Kb) 79788

[startup+470.042 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18720 0 0 0 46817 102 0 0 25 0 1 0 1854885815 79556608 17916 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19423 17916 145 145 0 19278 0
[pid=26547] vsize: 77692
Current children cumulated CPU time (s) 469.19
Current children cumulated vsize (Kb) 79816

[startup+480.043 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18728 0 0 0 47817 102 0 0 25 0 1 0 1854885815 79581184 17924 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19429 17924 145 145 0 19284 0
[pid=26547] vsize: 77716
Current children cumulated CPU time (s) 479.19
Current children cumulated vsize (Kb) 79840

[startup+490.043 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18732 0 0 0 48817 102 0 0 25 0 1 0 1854885815 79589376 17928 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19431 17928 145 145 0 19286 0
[pid=26547] vsize: 77724
Current children cumulated CPU time (s) 489.19
Current children cumulated vsize (Kb) 79848

[startup+500.045 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18732 0 0 0 49818 102 0 0 25 0 1 0 1854885815 79589376 17928 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19431 17928 145 145 0 19286 0
[pid=26547] vsize: 77724
Current children cumulated CPU time (s) 499.2
Current children cumulated vsize (Kb) 79848

[startup+510.045 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18733 0 0 0 50818 102 0 0 25 0 1 0 1854885815 79593472 17929 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19432 17929 145 145 0 19287 0
[pid=26547] vsize: 77728
Current children cumulated CPU time (s) 509.2
Current children cumulated vsize (Kb) 79852

[startup+520.046 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18744 0 0 0 51818 102 0 0 25 0 1 0 1854885815 79630336 17940 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19441 17940 145 145 0 19296 0
[pid=26547] vsize: 77764
Current children cumulated CPU time (s) 519.2
Current children cumulated vsize (Kb) 79888

[startup+530.047 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18745 0 0 0 52818 102 0 0 25 0 1 0 1854885815 79630336 17941 4294967295 134512640 135094434 3221224432 3221223120 134558987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19441 17941 145 145 0 19296 0
[pid=26547] vsize: 77764
Current children cumulated CPU time (s) 529.2
Current children cumulated vsize (Kb) 79888

[startup+540.047 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18791 0 0 0 53817 102 0 0 25 0 1 0 1854885815 79798272 17987 4294967295 134512640 135094434 3221224432 3221223136 134559005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26547/statm): 19482 17987 145 145 0 19337 0
[pid=26547] vsize: 77928
Current children cumulated CPU time (s) 539.19
Current children cumulated vsize (Kb) 80052

[startup+550.049 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18861 0 0 0 54816 103 0 0 25 0 1 0 1854885815 80142336 18057 4294967295 134512640 135094434 3221224432 3221223092 134553512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19566 18057 145 145 0 19421 0
[pid=26547] vsize: 78264
Current children cumulated CPU time (s) 549.19
Current children cumulated vsize (Kb) 80388

[startup+560.049 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18876 0 0 0 55816 103 0 0 25 0 1 0 1854885815 80199680 18072 4294967295 134512640 135094434 3221224432 3221223044 134563080 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19580 18072 145 145 0 19435 0
[pid=26547] vsize: 78320
Current children cumulated CPU time (s) 559.19
Current children cumulated vsize (Kb) 80444

[startup+570.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18884 0 0 0 56816 103 0 0 25 0 1 0 1854885815 80228352 18080 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19587 18080 145 145 0 19442 0
[pid=26547] vsize: 78348
Current children cumulated CPU time (s) 569.19
Current children cumulated vsize (Kb) 80472

[startup+580.051 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18886 0 0 0 57816 103 0 0 25 0 1 0 1854885815 80236544 18082 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19589 18082 145 145 0 19444 0
[pid=26547] vsize: 78356
Current children cumulated CPU time (s) 579.19
Current children cumulated vsize (Kb) 80480

[startup+590.051 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18888 0 0 0 58816 103 0 0 25 0 1 0 1854885815 80244736 18084 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19591 18084 145 145 0 19446 0
[pid=26547] vsize: 78364
Current children cumulated CPU time (s) 589.19
Current children cumulated vsize (Kb) 80488

[startup+600.053 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18897 0 0 0 59816 103 0 0 25 0 1 0 1854885815 80281600 18093 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19600 18093 145 145 0 19455 0
[pid=26547] vsize: 78400
Current children cumulated CPU time (s) 599.19
Current children cumulated vsize (Kb) 80524

[startup+610.053 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18905 0 0 0 60816 103 0 0 25 0 1 0 1854885815 80310272 18101 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19607 18101 145 145 0 19462 0
[pid=26547] vsize: 78428
Current children cumulated CPU time (s) 609.19
Current children cumulated vsize (Kb) 80552

[startup+620.054 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18912 0 0 0 61817 103 0 0 25 0 1 0 1854885815 80322560 18108 4294967295 134512640 135094434 3221224432 3221223108 134553524 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19610 18108 145 145 0 19465 0
[pid=26547] vsize: 78440
Current children cumulated CPU time (s) 619.2
Current children cumulated vsize (Kb) 80564

[startup+630.055 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18915 0 0 0 62817 103 0 0 25 0 1 0 1854885815 80334848 18111 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19613 18111 145 145 0 19468 0
[pid=26547] vsize: 78452
Current children cumulated CPU time (s) 629.2
Current children cumulated vsize (Kb) 80576

[startup+640.057 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18927 0 0 0 63817 104 0 0 25 0 1 0 1854885815 80379904 18123 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19624 18123 145 145 0 19479 0
[pid=26547] vsize: 78496
Current children cumulated CPU time (s) 639.21
Current children cumulated vsize (Kb) 80620

[startup+650.058 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18935 0 0 0 64817 104 0 0 25 0 1 0 1854885815 80408576 18131 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19631 18131 145 145 0 19486 0
[pid=26547] vsize: 78524
Current children cumulated CPU time (s) 649.21
Current children cumulated vsize (Kb) 80648

[startup+660.058 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18939 0 0 0 65817 104 0 0 25 0 1 0 1854885815 80424960 18135 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19635 18135 145 145 0 19490 0
[pid=26547] vsize: 78540
Current children cumulated CPU time (s) 659.21
Current children cumulated vsize (Kb) 80664

[startup+670.059 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18947 0 0 0 66817 104 0 0 25 0 1 0 1854885815 80441344 18143 4294967295 134512640 135094434 3221224432 3221223056 134557726 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19639 18143 145 145 0 19494 0
[pid=26547] vsize: 78556
Current children cumulated CPU time (s) 669.21
Current children cumulated vsize (Kb) 80680

[startup+680.06 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18960 0 0 0 67817 104 0 0 25 0 1 0 1854885815 80490496 18156 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19651 18156 145 145 0 19506 0
[pid=26547] vsize: 78604
Current children cumulated CPU time (s) 679.21
Current children cumulated vsize (Kb) 80728

[startup+690.06 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18980 0 0 0 68817 104 0 0 25 0 1 0 1854885815 80568320 18176 4294967295 134512640 135094434 3221224432 3221223060 134557564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19670 18176 145 145 0 19525 0
[pid=26547] vsize: 78680
Current children cumulated CPU time (s) 689.21
Current children cumulated vsize (Kb) 80804

[startup+700.061 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18996 0 0 0 69817 104 0 0 25 0 1 0 1854885815 80629760 18192 4294967295 134512640 135094434 3221224432 3221223136 134559019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19685 18192 145 145 0 19540 0
[pid=26547] vsize: 78740
Current children cumulated CPU time (s) 699.21
Current children cumulated vsize (Kb) 80864

[startup+710.061 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 18999 0 0 0 70818 104 0 0 25 0 1 0 1854885815 80637952 18195 4294967295 134512640 135094434 3221224432 3221223088 134558298 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19687 18195 145 145 0 19542 0
[pid=26547] vsize: 78748
Current children cumulated CPU time (s) 709.22
Current children cumulated vsize (Kb) 80872

[startup+720.062 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 19004 0 0 0 71818 104 0 0 25 0 1 0 1854885815 80658432 18200 4294967295 134512640 135094434 3221224432 3221223120 134558992 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19692 18200 145 145 0 19547 0
[pid=26547] vsize: 78768
Current children cumulated CPU time (s) 719.22
Current children cumulated vsize (Kb) 80892

[startup+730.064 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 19011 0 0 0 72818 104 0 0 25 0 1 0 1854885815 80683008 18207 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19698 18207 145 145 0 19553 0
[pid=26547] vsize: 78792
Current children cumulated CPU time (s) 729.22
Current children cumulated vsize (Kb) 80916

[startup+740.064 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 19018 0 0 0 73818 104 0 0 25 0 1 0 1854885815 80711680 18214 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19705 18214 145 145 0 19560 0
[pid=26547] vsize: 78820
Current children cumulated CPU time (s) 739.22
Current children cumulated vsize (Kb) 80944

[startup+750.066 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 19041 0 0 0 74818 104 0 0 25 0 1 0 1854885815 80769024 18237 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19719 18237 145 145 0 19574 0
[pid=26547] vsize: 78876
Current children cumulated CPU time (s) 749.22
Current children cumulated vsize (Kb) 81000

[startup+760.066 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 19047 0 0 0 75818 104 0 0 25 0 1 0 1854885815 80789504 18243 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19724 18243 145 145 0 19579 0
[pid=26547] vsize: 78896
Current children cumulated CPU time (s) 759.22
Current children cumulated vsize (Kb) 81020

[startup+770.066 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 19053 0 0 0 76819 104 0 0 25 0 1 0 1854885815 80814080 18249 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19730 18249 145 145 0 19585 0
[pid=26547] vsize: 78920
Current children cumulated CPU time (s) 769.23
Current children cumulated vsize (Kb) 81044

[startup+780.068 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 19092 0 0 0 77819 104 0 0 25 0 1 0 1854885815 81104896 18288 4294967295 134512640 135094434 3221224432 3221223044 134563061 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19801 18288 145 145 0 19656 0
[pid=26547] vsize: 79204
Current children cumulated CPU time (s) 779.23
Current children cumulated vsize (Kb) 81328

[startup+790.068 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 19096 0 0 0 78817 105 0 0 25 0 1 0 1854885815 81104896 18292 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19801 18292 145 145 0 19656 0
[pid=26547] vsize: 79204
Current children cumulated CPU time (s) 789.22
Current children cumulated vsize (Kb) 81328

[startup+800.068 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 19097 0 0 0 79818 105 0 0 25 0 1 0 1854885815 81104896 18293 4294967295 134512640 135094434 3221224432 3221223092 134553501 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19801 18293 145 145 0 19656 0
[pid=26547] vsize: 79204
Current children cumulated CPU time (s) 799.23
Current children cumulated vsize (Kb) 81328

[startup+810.068 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 19097 0 0 0 80818 105 0 0 25 0 1 0 1854885815 81104896 18293 4294967295 134512640 135094434 3221224432 3221223092 134553519 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19801 18293 145 145 0 19656 0
[pid=26547] vsize: 79204
Current children cumulated CPU time (s) 809.23
Current children cumulated vsize (Kb) 81328

[startup+820.069 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 19098 0 0 0 81818 105 0 0 25 0 1 0 1854885815 81104896 18294 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19801 18294 145 145 0 19656 0
[pid=26547] vsize: 79204
Current children cumulated CPU time (s) 819.23
Current children cumulated vsize (Kb) 81328

[startup+830.07 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 19110 0 0 0 82818 105 0 0 25 0 1 0 1854885815 81145856 18306 4294967295 134512640 135094434 3221224432 3221223044 134563087 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19811 18306 145 145 0 19666 0
[pid=26547] vsize: 79244
Current children cumulated CPU time (s) 829.23
Current children cumulated vsize (Kb) 81368

[startup+840.07 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 19132 0 0 0 83818 105 0 0 25 0 1 0 1854885815 81215488 18328 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19828 18328 145 145 0 19683 0
[pid=26547] vsize: 79312
Current children cumulated CPU time (s) 839.23
Current children cumulated vsize (Kb) 81436

[startup+850.071 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 19142 0 0 0 84818 105 0 0 25 0 1 0 1854885815 81256448 18338 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26547/statm): 19838 18338 145 145 0 19693 0
[pid=26547] vsize: 79352
Current children cumulated CPU time (s) 849.23
Current children cumulated vsize (Kb) 81476

[startup+860.072 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 19160 0 0 0 85817 105 0 0 25 0 1 0 1854885815 81326080 18356 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26547/statm): 19855 18356 145 145 0 19710 0
[pid=26547] vsize: 79420
Current children cumulated CPU time (s) 859.22
Current children cumulated vsize (Kb) 81544

[startup+870.072 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 19177 0 0 0 86816 106 0 0 25 0 1 0 1854885815 81391616 18373 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19871 18373 145 145 0 19726 0
[pid=26547] vsize: 79484
Current children cumulated CPU time (s) 869.22
Current children cumulated vsize (Kb) 81608

[startup+880.074 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 19195 0 0 0 87816 106 0 0 25 0 1 0 1854885815 81461248 18391 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19888 18391 145 145 0 19743 0
[pid=26547] vsize: 79552
Current children cumulated CPU time (s) 879.22
Current children cumulated vsize (Kb) 81676

[startup+890.074 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 19211 0 0 0 88816 106 0 0 25 0 1 0 1854885815 81522688 18407 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19903 18407 145 145 0 19758 0
[pid=26547] vsize: 79612
Current children cumulated CPU time (s) 889.22
Current children cumulated vsize (Kb) 81736

[startup+900.075 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 19249 0 0 0 89816 106 0 0 25 0 1 0 1854885815 81670144 18445 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19939 18445 145 145 0 19794 0
[pid=26547] vsize: 79756
Current children cumulated CPU time (s) 899.22
Current children cumulated vsize (Kb) 81880

[startup+910.076 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 19266 0 0 0 90816 106 0 0 25 0 1 0 1854885815 81735680 18462 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19955 18462 145 145 0 19810 0
[pid=26547] vsize: 79820
Current children cumulated CPU time (s) 909.22
Current children cumulated vsize (Kb) 81944

[startup+920.076 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 19297 0 0 0 91816 106 0 0 25 0 1 0 1854885815 81854464 18493 4294967295 134512640 135094434 3221224432 3221223092 134553450 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 19984 18493 145 145 0 19839 0
[pid=26547] vsize: 79936
Current children cumulated CPU time (s) 919.22
Current children cumulated vsize (Kb) 82060

[startup+930.077 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 19338 0 0 0 92815 107 0 0 25 0 1 0 1854885815 82014208 18534 4294967295 134512640 135094434 3221224432 3221223056 134557604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 20023 18534 145 145 0 19878 0
[pid=26547] vsize: 80092
Current children cumulated CPU time (s) 929.22
Current children cumulated vsize (Kb) 82216

[startup+940.077 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 19380 0 0 0 93815 107 0 0 25 0 1 0 1854885815 82178048 18576 4294967295 134512640 135094434 3221224432 3221223092 134553519 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 20063 18576 145 145 0 19918 0
[pid=26547] vsize: 80252
Current children cumulated CPU time (s) 939.22
Current children cumulated vsize (Kb) 82376

[startup+950.078 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 19411 0 0 0 94814 107 0 0 25 0 1 0 1854885815 82300928 18607 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26547/statm): 20093 18607 145 145 0 19948 0
[pid=26547] vsize: 80372
Current children cumulated CPU time (s) 949.21
Current children cumulated vsize (Kb) 82496

[startup+960.078 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 19436 0 0 0 95812 108 0 0 25 0 1 0 1854885815 82395136 18632 4294967295 134512640 135094434 3221224432 3221223136 134559005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 20116 18632 145 145 0 19971 0
[pid=26547] vsize: 80464
Current children cumulated CPU time (s) 959.2
Current children cumulated vsize (Kb) 82588

[startup+970.079 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 19468 0 0 0 96812 108 0 0 25 0 1 0 1854885815 82522112 18664 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 20147 18664 145 145 0 20002 0
[pid=26547] vsize: 80588
Current children cumulated CPU time (s) 969.2
Current children cumulated vsize (Kb) 82712

[startup+980.08 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 19521 0 0 0 97811 109 0 0 25 0 1 0 1854885815 82726912 18717 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 20197 18717 145 145 0 20052 0
[pid=26547] vsize: 80788
Current children cumulated CPU time (s) 979.2
Current children cumulated vsize (Kb) 82912

[startup+990.08 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 19553 0 0 0 98811 109 0 0 25 0 1 0 1854885815 82853888 18749 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 20228 18749 145 145 0 20083 0
[pid=26547] vsize: 80912
Current children cumulated CPU time (s) 989.2
Current children cumulated vsize (Kb) 83036

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 19585 0 0 0 99811 109 0 0 25 0 1 0 1854885815 82976768 18781 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 20258 18781 145 145 0 20113 0
[pid=26547] vsize: 81032
Current children cumulated CPU time (s) 999.2
Current children cumulated vsize (Kb) 83156

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 19681 0 0 0 100810 110 0 0 25 0 1 0 1854885815 83353600 18877 4294967295 134512640 135094434 3221224432 3221223044 134563112 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 20350 18877 145 145 0 20205 0
[pid=26547] vsize: 81400
Current children cumulated CPU time (s) 1009.2
Current children cumulated vsize (Kb) 83524

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 19727 0 0 0 101809 110 0 0 25 0 1 0 1854885815 83795968 18923 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 20458 18923 145 145 0 20313 0
[pid=26547] vsize: 81832
Current children cumulated CPU time (s) 1019.19
Current children cumulated vsize (Kb) 83956

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 19776 0 0 0 102808 110 0 0 25 0 1 0 1854885815 83988480 18972 4294967295 134512640 135094434 3221224432 3221223092 134553450 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 20505 18972 145 145 0 20360 0
[pid=26547] vsize: 82020
Current children cumulated CPU time (s) 1029.18
Current children cumulated vsize (Kb) 84144

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 19814 0 0 0 103807 111 0 0 25 0 1 0 1854885815 84135936 19010 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 20541 19010 145 145 0 20396 0
[pid=26547] vsize: 82164
Current children cumulated CPU time (s) 1039.18
Current children cumulated vsize (Kb) 84288

[startup+1050.08 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 19860 0 0 0 104807 111 0 0 25 0 1 0 1854885815 84316160 19056 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 20585 19056 145 145 0 20440 0
[pid=26547] vsize: 82340
Current children cumulated CPU time (s) 1049.18
Current children cumulated vsize (Kb) 84464

[startup+1060.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 19921 0 0 0 105806 112 0 0 25 0 1 0 1854885815 84553728 19117 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 20643 19117 145 145 0 20498 0
[pid=26547] vsize: 82572
Current children cumulated CPU time (s) 1059.18
Current children cumulated vsize (Kb) 84696

[startup+1070.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 19966 0 0 0 106805 112 0 0 25 0 1 0 1854885815 84729856 19162 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 20686 19162 145 145 0 20541 0
[pid=26547] vsize: 82744
Current children cumulated CPU time (s) 1069.17
Current children cumulated vsize (Kb) 84868

[startup+1080.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 20061 0 0 0 107804 113 0 0 25 0 1 0 1854885815 85106688 19257 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 20778 19257 145 145 0 20633 0
[pid=26547] vsize: 83112
Current children cumulated CPU time (s) 1079.17
Current children cumulated vsize (Kb) 85236

[startup+1090.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 20105 0 0 0 108804 113 0 0 25 0 1 0 1854885815 85278720 19301 4294967295 134512640 135094434 3221224432 3221223088 134558435 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 20820 19301 145 145 0 20675 0
[pid=26547] vsize: 83280
Current children cumulated CPU time (s) 1089.17
Current children cumulated vsize (Kb) 85404

[startup+1100.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 20180 0 0 0 109803 114 0 0 25 0 1 0 1854885815 85573632 19376 4294967295 134512640 135094434 3221224432 3221223044 134563134 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 20892 19376 145 145 0 20747 0
[pid=26547] vsize: 83568
Current children cumulated CPU time (s) 1099.17
Current children cumulated vsize (Kb) 85692

[startup+1110.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 20250 0 0 0 110802 114 0 0 25 0 1 0 1854885815 85848064 19446 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 20959 19446 145 145 0 20814 0
[pid=26547] vsize: 83836
Current children cumulated CPU time (s) 1109.16
Current children cumulated vsize (Kb) 85960

[startup+1120.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 20292 0 0 0 111802 115 0 0 25 0 1 0 1854885815 86011904 19488 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 20999 19488 145 145 0 20854 0
[pid=26547] vsize: 83996
Current children cumulated CPU time (s) 1119.17
Current children cumulated vsize (Kb) 86120

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 20358 0 0 0 112800 115 0 0 25 0 1 0 1854885815 86269952 19554 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 21062 19554 145 145 0 20917 0
[pid=26547] vsize: 84248
Current children cumulated CPU time (s) 1129.15
Current children cumulated vsize (Kb) 86372

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 20380 0 0 0 113800 116 0 0 25 0 1 0 1854885815 86355968 19576 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 21083 19576 145 145 0 20938 0
[pid=26547] vsize: 84332
Current children cumulated CPU time (s) 1139.16
Current children cumulated vsize (Kb) 86456

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 20419 0 0 0 114800 116 0 0 25 0 1 0 1854885815 86507520 19615 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 21120 19615 145 145 0 20975 0
[pid=26547] vsize: 84480
Current children cumulated CPU time (s) 1149.16
Current children cumulated vsize (Kb) 86604

[startup+1160.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 20449 0 0 0 115800 116 0 0 25 0 1 0 1854885815 86622208 19645 4294967295 134512640 135094434 3221224432 3221223136 134559013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 21148 19645 145 145 0 21003 0
[pid=26547] vsize: 84592
Current children cumulated CPU time (s) 1159.16
Current children cumulated vsize (Kb) 86716

[startup+1170.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 20519 0 0 0 116799 116 0 0 25 0 1 0 1854885815 86900736 19715 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 21216 19715 145 145 0 21071 0
[pid=26547] vsize: 84864
Current children cumulated CPU time (s) 1169.15
Current children cumulated vsize (Kb) 86988

[startup+1180.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 20585 0 0 0 117798 117 0 0 25 0 1 0 1854885815 87158784 19781 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 21279 19781 145 145 0 21134 0
[pid=26547] vsize: 85116
Current children cumulated CPU time (s) 1179.15
Current children cumulated vsize (Kb) 87240

[startup+1190.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 20676 0 0 0 118796 118 0 0 25 0 1 0 1854885815 87515136 19872 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 21366 19872 145 145 0 21221 0
[pid=26547] vsize: 85464
Current children cumulated CPU time (s) 1189.14
Current children cumulated vsize (Kb) 87588

[startup+1200.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 20740 0 0 0 119795 118 0 0 25 0 1 0 1854885815 87769088 19936 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 21428 19936 145 145 0 21283 0
[pid=26547] vsize: 85712
Current children cumulated CPU time (s) 1199.13
Current children cumulated vsize (Kb) 87836

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 20791 0 0 0 120794 119 0 0 25 0 1 0 1854885815 87965696 19987 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 21476 19987 145 145 0 21331 0
[pid=26547] vsize: 85904
Current children cumulated CPU time (s) 1209.13
Current children cumulated vsize (Kb) 88028



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 26547
Raw data (/proc/26543/stat): 26543 (minisat+_script) S 26542 26543 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854885810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26543/statm): 531 226 485 147 0 384 0
[pid=26543] vsize: 2124
Raw data (/proc/26547/stat): 26547 (minisat+_64-bit) R 26543 26543 4419 0 -1 0 20791 0 0 0 120795 119 0 0 25 0 1 0 1854885815 87965696 19987 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26547/statm): 21476 19987 145 145 0 21331 0
[pid=26547] vsize: 85904
Current children cumulated CPU time (s) 1209.14
Current children cumulated vsize (Kb) 88028

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

Child status: 0
Real time (s): 1210.14
CPU time (s): 1209.18
CPU user time (s): 1207.95
CPU system time (s): 1.23081
CPU usage (%): 99.9208
Max. virtual memory (cumulated for all children) (Kb): 88028