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/32154/stat): 32154 (minisat+_script) R 32153 32154 9854 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1796855666 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/32154/statm): 174 3 169 147 0 27 0
[pid=32154] 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=32155
New process pid=32156
New process pid=32157
execve syscall for /bin/sed executable
One traced child (pid=32156) 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=32157) exited with status: 0
One traced child (pid=32155) exited with status: 0
New process pid=32158
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-13-7-sctap1.opb

[startup+10.004 s]
Raw data (loadavg): 0.82 0.93 0.96 1/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) T 32154 32154 9854 0 -1 0 11666 0 0 0 905 47 0 0 21 0 1 0 1796855671 47210496 10973 4294967295 134512640 135094434 3221224432 3221195772 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/32158/statm): 11526 10973 145 145 0 11381 0
[pid=32158] vsize: 46104
Current children cumulated CPU time (s) 9.53
Current children cumulated vsize (Kb) 48228

[startup+20.0048 s]
Raw data (loadavg): 0.85 0.93 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 19511 0 0 0 1831 81 0 0 25 0 1 0 1796855671 81944576 18818 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 20006 18818 145 145 0 19861 0
[pid=32158] vsize: 80024
Current children cumulated CPU time (s) 19.13
Current children cumulated vsize (Kb) 82148

[startup+30.0066 s]
Raw data (loadavg): 0.87 0.93 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 19637 0 0 0 2828 82 0 0 25 0 1 0 1796855671 82399232 18944 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32158/statm): 20117 18944 145 145 0 19972 0
[pid=32158] vsize: 80468
Current children cumulated CPU time (s) 29.11
Current children cumulated vsize (Kb) 82592

[startup+40.0074 s]
Raw data (loadavg): 0.89 0.93 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 19756 0 0 0 3825 83 0 0 25 0 1 0 1796855671 82788352 19063 4294967295 134512640 135094434 3221224432 3221223120 134558992 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 20212 19063 145 145 0 20067 0
[pid=32158] vsize: 80848
Current children cumulated CPU time (s) 39.09
Current children cumulated vsize (Kb) 82972

[startup+50.0092 s]
Raw data (loadavg): 0.91 0.93 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 19858 0 0 0 4824 84 0 0 25 0 1 0 1796855671 83181568 19165 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 20308 19165 145 145 0 20163 0
[pid=32158] vsize: 81232
Current children cumulated CPU time (s) 49.09
Current children cumulated vsize (Kb) 83356

[startup+60.01 s]
Raw data (loadavg): 0.92 0.94 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 20055 0 0 0 5822 85 0 0 25 0 1 0 1796855671 83980288 19362 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 20503 19362 145 145 0 20358 0
[pid=32158] vsize: 82012
Current children cumulated CPU time (s) 59.08
Current children cumulated vsize (Kb) 84136

[startup+70.0108 s]
Raw data (loadavg): 0.93 0.94 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 20220 0 0 0 6818 86 0 0 25 0 1 0 1796855671 84606976 19527 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32158/statm): 20656 19527 145 145 0 20511 0
[pid=32158] vsize: 82624
Current children cumulated CPU time (s) 69.05
Current children cumulated vsize (Kb) 84748

[startup+80.0125 s]
Raw data (loadavg): 0.94 0.94 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 20276 0 0 0 7817 86 0 0 25 0 1 0 1796855671 84815872 19583 4294967295 134512640 135094434 3221224432 3221223056 134562048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 20707 19583 145 145 0 20562 0
[pid=32158] vsize: 82828
Current children cumulated CPU time (s) 79.04
Current children cumulated vsize (Kb) 84952

[startup+90.0133 s]
Raw data (loadavg): 0.95 0.94 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 20413 0 0 0 8816 87 0 0 25 0 1 0 1796855671 85491712 19720 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 20872 19720 145 145 0 20727 0
[pid=32158] vsize: 83488
Current children cumulated CPU time (s) 89.04
Current children cumulated vsize (Kb) 85612

[startup+100.014 s]
Raw data (loadavg): 0.96 0.94 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 20507 0 0 0 9815 88 0 0 25 0 1 0 1796855671 85831680 19814 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 20955 19814 145 145 0 20810 0
[pid=32158] vsize: 83820
Current children cumulated CPU time (s) 99.04
Current children cumulated vsize (Kb) 85944

[startup+110.015 s]
Raw data (loadavg): 0.96 0.94 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 20550 0 0 0 10814 88 0 0 25 0 1 0 1796855671 85999616 19857 4294967295 134512640 135094434 3221224432 3221223044 134563071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 20996 19857 145 145 0 20851 0
[pid=32158] vsize: 83984
Current children cumulated CPU time (s) 109.03
Current children cumulated vsize (Kb) 86108

[startup+120.016 s]
Raw data (loadavg): 0.97 0.94 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 20666 0 0 0 11812 89 0 0 25 0 1 0 1796855671 86437888 19973 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 21103 19973 145 145 0 20958 0
[pid=32158] vsize: 84412
Current children cumulated CPU time (s) 119.02
Current children cumulated vsize (Kb) 86536

[startup+130.016 s]
Raw data (loadavg): 0.97 0.95 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 20733 0 0 0 12811 89 0 0 25 0 1 0 1796855671 86700032 20040 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 21167 20040 145 145 0 21022 0
[pid=32158] vsize: 84668
Current children cumulated CPU time (s) 129.01
Current children cumulated vsize (Kb) 86792

[startup+140.017 s]
Raw data (loadavg): 0.98 0.95 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) T 32154 32154 9854 0 -1 0 20989 0 0 0 13807 92 0 0 25 0 1 0 1796855671 87724032 20296 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/32158/statm): 21417 20296 145 145 0 21272 0
[pid=32158] vsize: 85668
Current children cumulated CPU time (s) 139
Current children cumulated vsize (Kb) 87792

[startup+150.019 s]
Raw data (loadavg): 0.98 0.95 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 21090 0 0 0 14804 93 0 0 25 0 1 0 1796855671 88117248 20397 4294967295 134512640 135094434 3221224432 3221222912 134781282 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 21513 20397 145 145 0 21368 0
[pid=32158] vsize: 86052
Current children cumulated CPU time (s) 148.98
Current children cumulated vsize (Kb) 88176

[startup+160.02 s]
Raw data (loadavg): 0.98 0.95 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 21253 0 0 0 15802 94 0 0 25 0 1 0 1796855671 88764416 20560 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 21671 20560 145 145 0 21526 0
[pid=32158] vsize: 86684
Current children cumulated CPU time (s) 158.97
Current children cumulated vsize (Kb) 88808

[startup+170.021 s]
Raw data (loadavg): 0.98 0.95 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 21398 0 0 0 16801 94 0 0 25 0 1 0 1796855671 89337856 20705 4294967295 134512640 135094434 3221224432 3221223092 134553528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 21811 20705 145 145 0 21666 0
[pid=32158] vsize: 87244
Current children cumulated CPU time (s) 168.96
Current children cumulated vsize (Kb) 89368

[startup+180.021 s]
Raw data (loadavg): 0.99 0.95 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 21453 0 0 0 17800 95 0 0 25 0 1 0 1796855671 89817088 20760 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 21928 20760 145 145 0 21783 0
[pid=32158] vsize: 87712
Current children cumulated CPU time (s) 178.96
Current children cumulated vsize (Kb) 89836

[startup+190.022 s]
Raw data (loadavg): 0.99 0.95 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 21484 0 0 0 18800 95 0 0 25 0 1 0 1796855671 89935872 20791 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 21957 20791 145 145 0 21812 0
[pid=32158] vsize: 87828
Current children cumulated CPU time (s) 188.96
Current children cumulated vsize (Kb) 89952

[startup+200.024 s]
Raw data (loadavg): 0.99 0.95 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 21588 0 0 0 19798 96 0 0 25 0 1 0 1796855671 90349568 20895 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 22058 20895 145 145 0 21913 0
[pid=32158] vsize: 88232
Current children cumulated CPU time (s) 198.95
Current children cumulated vsize (Kb) 90356

[startup+210.025 s]
Raw data (loadavg): 0.99 0.95 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 21633 0 0 0 20797 97 0 0 25 0 1 0 1796855671 90525696 20940 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 22101 20940 145 145 0 21956 0
[pid=32158] vsize: 88404
Current children cumulated CPU time (s) 208.95
Current children cumulated vsize (Kb) 90528

[startup+220.026 s]
Raw data (loadavg): 0.99 0.95 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 21680 0 0 0 21796 97 0 0 25 0 1 0 1796855671 90705920 20987 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 22145 20987 145 145 0 22000 0
[pid=32158] vsize: 88580
Current children cumulated CPU time (s) 218.94
Current children cumulated vsize (Kb) 90704

[startup+230.027 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 21723 0 0 0 22795 98 0 0 25 0 1 0 1796855671 90873856 21030 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 22186 21030 145 145 0 22041 0
[pid=32158] vsize: 88744
Current children cumulated CPU time (s) 228.94
Current children cumulated vsize (Kb) 90868

[startup+240.028 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 21754 0 0 0 23795 98 0 0 25 0 1 0 1796855671 90992640 21061 4294967295 134512640 135094434 3221224432 3221223088 134550396 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 22215 21061 145 145 0 22070 0
[pid=32158] vsize: 88860
Current children cumulated CPU time (s) 238.94
Current children cumulated vsize (Kb) 90984

[startup+250.03 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 21805 0 0 0 24795 98 0 0 25 0 1 0 1796855671 91123712 21112 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 22247 21112 145 145 0 22102 0
[pid=32158] vsize: 88988
Current children cumulated CPU time (s) 248.94
Current children cumulated vsize (Kb) 91112

[startup+260.031 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 21833 0 0 0 25795 98 0 0 25 0 1 0 1796855671 91230208 21140 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 22273 21140 145 145 0 22128 0
[pid=32158] vsize: 89092
Current children cumulated CPU time (s) 258.94
Current children cumulated vsize (Kb) 91216

[startup+270.031 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 21867 0 0 0 26794 98 0 0 25 0 1 0 1796855671 91340800 21174 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 22300 21174 145 145 0 22155 0
[pid=32158] vsize: 89200
Current children cumulated CPU time (s) 268.93
Current children cumulated vsize (Kb) 91324

[startup+280.032 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 21896 0 0 0 27794 99 0 0 25 0 1 0 1796855671 91447296 21203 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32158/statm): 22326 21203 145 145 0 22181 0
[pid=32158] vsize: 89304
Current children cumulated CPU time (s) 278.94
Current children cumulated vsize (Kb) 91428

[startup+290.034 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 21963 0 0 0 28792 99 0 0 25 0 1 0 1796855671 91648000 21270 4294967295 134512640 135094434 3221224432 3221223072 134558269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32158/statm): 22375 21270 145 145 0 22230 0
[pid=32158] vsize: 89500
Current children cumulated CPU time (s) 288.92
Current children cumulated vsize (Kb) 91624

[startup+300.036 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 22006 0 0 0 29791 100 0 0 25 0 1 0 1796855671 91811840 21313 4294967295 134512640 135094434 3221224432 3221223104 134554886 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 22415 21313 145 145 0 22270 0
[pid=32158] vsize: 89660
Current children cumulated CPU time (s) 298.92
Current children cumulated vsize (Kb) 91784

[startup+310.037 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 22048 0 0 0 30791 100 0 0 25 0 1 0 1796855671 91975680 21355 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 22455 21355 145 145 0 22310 0
[pid=32158] vsize: 89820
Current children cumulated CPU time (s) 308.92
Current children cumulated vsize (Kb) 91944

[startup+320.037 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 22074 0 0 0 31791 100 0 0 25 0 1 0 1796855671 92078080 21381 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 22480 21381 145 145 0 22335 0
[pid=32158] vsize: 89920
Current children cumulated CPU time (s) 318.92
Current children cumulated vsize (Kb) 92044

[startup+330.038 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 22139 0 0 0 32790 101 0 0 25 0 1 0 1796855671 92323840 21446 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 22540 21446 145 145 0 22395 0
[pid=32158] vsize: 90160
Current children cumulated CPU time (s) 328.92
Current children cumulated vsize (Kb) 92284

[startup+340.039 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 22208 0 0 0 33789 101 0 0 25 0 1 0 1796855671 92594176 21515 4294967295 134512640 135094434 3221224432 3221223136 134559017 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 22606 21515 145 145 0 22461 0
[pid=32158] vsize: 90424
Current children cumulated CPU time (s) 338.91
Current children cumulated vsize (Kb) 92548

[startup+350.041 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 22246 0 0 0 34788 102 0 0 25 0 1 0 1796855671 92741632 21553 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 22642 21553 145 145 0 22497 0
[pid=32158] vsize: 90568
Current children cumulated CPU time (s) 348.91
Current children cumulated vsize (Kb) 92692

[startup+360.042 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 22280 0 0 0 35788 102 0 0 25 0 1 0 1796855671 92872704 21587 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 22674 21587 145 145 0 22529 0
[pid=32158] vsize: 90696
Current children cumulated CPU time (s) 358.91
Current children cumulated vsize (Kb) 92820

[startup+370.041 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 22310 0 0 0 36788 102 0 0 25 0 1 0 1796855671 92987392 21617 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 22702 21617 145 145 0 22557 0
[pid=32158] vsize: 90808
Current children cumulated CPU time (s) 368.91
Current children cumulated vsize (Kb) 92932

[startup+380.042 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 22335 0 0 0 37787 102 0 0 25 0 1 0 1796855671 93085696 21642 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 22726 21642 145 145 0 22581 0
[pid=32158] vsize: 90904
Current children cumulated CPU time (s) 378.9
Current children cumulated vsize (Kb) 93028

[startup+390.043 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 22459 0 0 0 38786 103 0 0 25 0 1 0 1796855671 93577216 21766 4294967295 134512640 135094434 3221224432 3221223056 134557604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 22846 21766 145 145 0 22701 0
[pid=32158] vsize: 91384
Current children cumulated CPU time (s) 388.9
Current children cumulated vsize (Kb) 93508

[startup+400.044 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 22492 0 0 0 39785 103 0 0 25 0 1 0 1796855671 93704192 21799 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 22877 21799 145 145 0 22732 0
[pid=32158] vsize: 91508
Current children cumulated CPU time (s) 398.89
Current children cumulated vsize (Kb) 93632

[startup+410.046 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 22586 0 0 0 40784 104 0 0 25 0 1 0 1796855671 94076928 21893 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 22968 21893 145 145 0 22823 0
[pid=32158] vsize: 91872
Current children cumulated CPU time (s) 408.89
Current children cumulated vsize (Kb) 93996

[startup+420.046 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 22684 0 0 0 41782 105 0 0 25 0 1 0 1796855671 94466048 21991 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 23063 21991 145 145 0 22918 0
[pid=32158] vsize: 92252
Current children cumulated CPU time (s) 418.88
Current children cumulated vsize (Kb) 94376

[startup+430.047 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 22726 0 0 0 42782 105 0 0 25 0 1 0 1796855671 94629888 22033 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 23103 22033 145 145 0 22958 0
[pid=32158] vsize: 92412
Current children cumulated CPU time (s) 428.88
Current children cumulated vsize (Kb) 94536

[startup+440.048 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 22752 0 0 0 43782 105 0 0 25 0 1 0 1796855671 94728192 22059 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 23127 22059 145 145 0 22982 0
[pid=32158] vsize: 92508
Current children cumulated CPU time (s) 438.88
Current children cumulated vsize (Kb) 94632

[startup+450.05 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 22794 0 0 0 44782 106 0 0 25 0 1 0 1796855671 94892032 22101 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 23167 22101 145 145 0 23022 0
[pid=32158] vsize: 92668
Current children cumulated CPU time (s) 448.89
Current children cumulated vsize (Kb) 94792

[startup+460.05 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 22853 0 0 0 45780 106 0 0 25 0 1 0 1796855671 95125504 22160 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 23224 22160 145 145 0 23079 0
[pid=32158] vsize: 92896
Current children cumulated CPU time (s) 458.87
Current children cumulated vsize (Kb) 95020

[startup+470.051 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 22895 0 0 0 46780 106 0 0 25 0 1 0 1796855671 95289344 22202 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32158/statm): 23264 22202 145 145 0 23119 0
[pid=32158] vsize: 93056
Current children cumulated CPU time (s) 468.87
Current children cumulated vsize (Kb) 95180

[startup+480.053 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 22995 0 0 0 47777 107 0 0 25 0 1 0 1796855671 96206848 22302 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 23488 22302 145 145 0 23343 0
[pid=32158] vsize: 93952
Current children cumulated CPU time (s) 478.85
Current children cumulated vsize (Kb) 96076

[startup+490.054 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 23056 0 0 0 48776 108 0 0 25 0 1 0 1796855671 96448512 22363 4294967295 134512640 135094434 3221224432 3221223044 134563089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 23547 22363 145 145 0 23402 0
[pid=32158] vsize: 94188
Current children cumulated CPU time (s) 488.85
Current children cumulated vsize (Kb) 96312

[startup+500.056 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 23091 0 0 0 49776 108 0 0 25 0 1 0 1796855671 96583680 22398 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 23580 22398 145 145 0 23435 0
[pid=32158] vsize: 94320
Current children cumulated CPU time (s) 498.85
Current children cumulated vsize (Kb) 96444

[startup+510.057 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 23123 0 0 0 50776 109 0 0 25 0 1 0 1796855671 96706560 22430 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 23610 22430 145 145 0 23465 0
[pid=32158] vsize: 94440
Current children cumulated CPU time (s) 508.86
Current children cumulated vsize (Kb) 96564

[startup+520.057 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 23150 0 0 0 51775 109 0 0 25 0 1 0 1796855671 96813056 22457 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 23636 22457 145 145 0 23491 0
[pid=32158] vsize: 94544
Current children cumulated CPU time (s) 518.85
Current children cumulated vsize (Kb) 96668

[startup+530.059 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 23175 0 0 0 52775 109 0 0 25 0 1 0 1796855671 96907264 22482 4294967295 134512640 135094434 3221224432 3221223088 134561759 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 23659 22482 145 145 0 23514 0
[pid=32158] vsize: 94636
Current children cumulated CPU time (s) 528.85
Current children cumulated vsize (Kb) 96760

[startup+540.06 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 23203 0 0 0 53774 109 0 0 25 0 1 0 1796855671 97017856 22510 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 23686 22510 145 145 0 23541 0
[pid=32158] vsize: 94744
Current children cumulated CPU time (s) 538.84
Current children cumulated vsize (Kb) 96868

[startup+550.061 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 23240 0 0 0 54774 110 0 0 25 0 1 0 1796855671 97161216 22547 4294967295 134512640 135094434 3221224432 3221223120 134558992 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 23721 22547 145 145 0 23576 0
[pid=32158] vsize: 94884
Current children cumulated CPU time (s) 548.85
Current children cumulated vsize (Kb) 97008

[startup+560.061 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) T 32154 32154 9854 0 -1 0 23313 0 0 0 55771 111 0 0 25 0 1 0 1796855671 97447936 22620 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/32158/statm): 23791 22620 145 145 0 23646 0
[pid=32158] vsize: 95164
Current children cumulated CPU time (s) 558.83
Current children cumulated vsize (Kb) 97288

[startup+570.062 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 23349 0 0 0 56771 111 0 0 25 0 1 0 1796855671 97587200 22656 4294967295 134512640 135094434 3221224432 3221223120 134558992 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 23825 22656 145 145 0 23680 0
[pid=32158] vsize: 95300
Current children cumulated CPU time (s) 568.83
Current children cumulated vsize (Kb) 97424

[startup+580.063 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 23390 0 0 0 57771 111 0 0 25 0 1 0 1796855671 97746944 22697 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 23864 22697 145 145 0 23719 0
[pid=32158] vsize: 95456
Current children cumulated CPU time (s) 578.83
Current children cumulated vsize (Kb) 97580

[startup+590.064 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 23441 0 0 0 58771 112 0 0 25 0 1 0 1796855671 97947648 22748 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 23913 22748 145 145 0 23768 0
[pid=32158] vsize: 95652
Current children cumulated CPU time (s) 588.84
Current children cumulated vsize (Kb) 97776

[startup+600.064 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 23492 0 0 0 59770 112 0 0 25 0 1 0 1796855671 98148352 22799 4294967295 134512640 135094434 3221224432 3221223120 134558992 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 23962 22799 145 145 0 23817 0
[pid=32158] vsize: 95848
Current children cumulated CPU time (s) 598.83
Current children cumulated vsize (Kb) 97972

[startup+610.065 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) T 32154 32154 9854 0 -1 0 23555 0 0 0 60768 113 0 0 25 0 1 0 1796855671 98398208 22862 4294967295 134512640 135094434 3221224432 3221222780 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/32158/statm): 24023 22862 145 145 0 23878 0
[pid=32158] vsize: 96092
Current children cumulated CPU time (s) 608.82
Current children cumulated vsize (Kb) 98216

[startup+620.066 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 23665 0 0 0 61766 114 0 0 25 0 1 0 1796855671 98832384 22972 4294967295 134512640 135094434 3221224432 3221223136 134554526 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 24129 22972 145 145 0 23984 0
[pid=32158] vsize: 96516
Current children cumulated CPU time (s) 618.81
Current children cumulated vsize (Kb) 98640

[startup+630.068 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 23750 0 0 0 62765 114 0 0 25 0 1 0 1796855671 99168256 23057 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 24211 23057 145 145 0 24066 0
[pid=32158] vsize: 96844
Current children cumulated CPU time (s) 628.8
Current children cumulated vsize (Kb) 98968

[startup+640.069 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 23794 0 0 0 63765 115 0 0 25 0 1 0 1796855671 99340288 23101 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 24253 23101 145 145 0 24108 0
[pid=32158] vsize: 97012
Current children cumulated CPU time (s) 638.81
Current children cumulated vsize (Kb) 99136

[startup+650.069 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 23843 0 0 0 64765 115 0 0 25 0 1 0 1796855671 99532800 23150 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 24300 23150 145 145 0 24155 0
[pid=32158] vsize: 97200
Current children cumulated CPU time (s) 648.81
Current children cumulated vsize (Kb) 99324

[startup+660.071 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 23883 0 0 0 65764 115 0 0 25 0 1 0 1796855671 99688448 23190 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 24338 23190 145 145 0 24193 0
[pid=32158] vsize: 97352
Current children cumulated CPU time (s) 658.8
Current children cumulated vsize (Kb) 99476

[startup+670.071 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 23926 0 0 0 66764 115 0 0 25 0 1 0 1796855671 99856384 23233 4294967295 134512640 135094434 3221224432 3221223044 134563074 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 24379 23233 145 145 0 24234 0
[pid=32158] vsize: 97516
Current children cumulated CPU time (s) 668.8
Current children cumulated vsize (Kb) 99640

[startup+680.072 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 23955 0 0 0 67764 115 0 0 25 0 1 0 1796855671 99966976 23262 4294967295 134512640 135094434 3221224432 3221223072 134558264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 24406 23262 145 145 0 24261 0
[pid=32158] vsize: 97624
Current children cumulated CPU time (s) 678.8
Current children cumulated vsize (Kb) 99748

[startup+690.072 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 24001 0 0 0 68763 116 0 0 25 0 1 0 1796855671 100147200 23308 4294967295 134512640 135094434 3221224432 3221223044 134563110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 24450 23308 145 145 0 24305 0
[pid=32158] vsize: 97800
Current children cumulated CPU time (s) 688.8
Current children cumulated vsize (Kb) 99924

[startup+700.072 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 24027 0 0 0 69763 116 0 0 25 0 1 0 1796855671 100245504 23334 4294967295 134512640 135094434 3221224432 3221223092 134553444 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 24474 23334 145 145 0 24329 0
[pid=32158] vsize: 97896
Current children cumulated CPU time (s) 698.8
Current children cumulated vsize (Kb) 100020

[startup+710.073 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 24107 0 0 0 70762 116 0 0 25 0 1 0 1796855671 100544512 23414 4294967295 134512640 135094434 3221224432 3221223056 134557636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 24547 23414 145 145 0 24402 0
[pid=32158] vsize: 98188
Current children cumulated CPU time (s) 708.79
Current children cumulated vsize (Kb) 100312

[startup+720.074 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 24173 0 0 0 71760 117 0 0 25 0 1 0 1796855671 100806656 23480 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 24611 23480 145 145 0 24466 0
[pid=32158] vsize: 98444
Current children cumulated CPU time (s) 718.78
Current children cumulated vsize (Kb) 100568

[startup+730.075 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 24260 0 0 0 72759 118 0 0 25 0 1 0 1796855671 101150720 23567 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 24695 23567 145 145 0 24550 0
[pid=32158] vsize: 98780
Current children cumulated CPU time (s) 728.78
Current children cumulated vsize (Kb) 100904

[startup+740.075 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 24314 0 0 0 73759 118 0 0 25 0 1 0 1796855671 101363712 23621 4294967295 134512640 135094434 3221224432 3221223056 134557675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 24747 23621 145 145 0 24602 0
[pid=32158] vsize: 98988
Current children cumulated CPU time (s) 738.78
Current children cumulated vsize (Kb) 101112

[startup+750.076 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 24404 0 0 0 74757 119 0 0 25 0 1 0 1796855671 101715968 23711 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 24833 23711 145 145 0 24688 0
[pid=32158] vsize: 99332
Current children cumulated CPU time (s) 748.77
Current children cumulated vsize (Kb) 101456

[startup+760.077 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 24551 0 0 0 75754 120 0 0 25 0 1 0 1796855671 102301696 23858 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 24976 23858 145 145 0 24831 0
[pid=32158] vsize: 99904
Current children cumulated CPU time (s) 758.75
Current children cumulated vsize (Kb) 102028

[startup+770.078 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 24700 0 0 0 76751 122 0 0 25 0 1 0 1796855671 102891520 24007 4294967295 134512640 135094434 3221224432 3221223088 134558162 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 25120 24007 145 145 0 24975 0
[pid=32158] vsize: 100480
Current children cumulated CPU time (s) 768.74
Current children cumulated vsize (Kb) 102604

[startup+780.079 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 24780 0 0 0 77750 122 0 0 25 0 1 0 1796855671 103211008 24087 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 25198 24087 145 145 0 25053 0
[pid=32158] vsize: 100792
Current children cumulated CPU time (s) 778.73
Current children cumulated vsize (Kb) 102916

[startup+790.079 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 25081 0 0 0 78745 124 0 0 25 0 1 0 1796855671 104415232 24388 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 25492 24388 145 145 0 25347 0
[pid=32158] vsize: 101968
Current children cumulated CPU time (s) 788.7
Current children cumulated vsize (Kb) 104092

[startup+800.08 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 25256 0 0 0 79742 126 0 0 25 0 1 0 1796855671 105115648 24563 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 25663 24563 145 145 0 25518 0
[pid=32158] vsize: 102652
Current children cumulated CPU time (s) 798.69
Current children cumulated vsize (Kb) 104776

[startup+810.081 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 25370 0 0 0 80740 126 0 0 25 0 1 0 1796855671 105566208 24677 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 25773 24677 145 145 0 25628 0
[pid=32158] vsize: 103092
Current children cumulated CPU time (s) 808.67
Current children cumulated vsize (Kb) 105216

[startup+820.082 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 25478 0 0 0 81739 127 0 0 25 0 1 0 1796855671 105996288 24785 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 25878 24785 145 145 0 25733 0
[pid=32158] vsize: 103512
Current children cumulated CPU time (s) 818.67
Current children cumulated vsize (Kb) 105636

[startup+830.083 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 25581 0 0 0 82738 127 0 0 25 0 1 0 1796855671 106401792 24888 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 25977 24888 145 145 0 25832 0
[pid=32158] vsize: 103908
Current children cumulated CPU time (s) 828.66
Current children cumulated vsize (Kb) 106032

[startup+840.084 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 25661 0 0 0 83736 128 0 0 25 0 1 0 1796855671 106717184 24968 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 26054 24968 145 145 0 25909 0
[pid=32158] vsize: 104216
Current children cumulated CPU time (s) 838.65
Current children cumulated vsize (Kb) 106340

[startup+850.084 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 25705 0 0 0 84735 129 0 0 25 0 1 0 1796855671 106893312 25012 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 26097 25012 145 145 0 25952 0
[pid=32158] vsize: 104388
Current children cumulated CPU time (s) 848.65
Current children cumulated vsize (Kb) 106512

[startup+860.087 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 25736 0 0 0 85735 129 0 0 25 0 1 0 1796855671 107012096 25043 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 26126 25043 145 145 0 25981 0
[pid=32158] vsize: 104504
Current children cumulated CPU time (s) 858.65
Current children cumulated vsize (Kb) 106628

[startup+870.088 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 25771 0 0 0 86734 129 0 0 25 0 1 0 1796855671 107147264 25078 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 26159 25078 145 145 0 26014 0
[pid=32158] vsize: 104636
Current children cumulated CPU time (s) 868.64
Current children cumulated vsize (Kb) 106760

[startup+880.088 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 25834 0 0 0 87733 130 0 0 25 0 1 0 1796855671 107397120 25141 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 26220 25141 145 145 0 26075 0
[pid=32158] vsize: 104880
Current children cumulated CPU time (s) 878.64
Current children cumulated vsize (Kb) 107004

[startup+890.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 25879 0 0 0 88733 130 0 0 25 0 1 0 1796855671 107560960 25186 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 26260 25186 145 145 0 26115 0
[pid=32158] vsize: 105040
Current children cumulated CPU time (s) 888.64
Current children cumulated vsize (Kb) 107164

[startup+900.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 25917 0 0 0 89732 131 0 0 25 0 1 0 1796855671 107708416 25224 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 26296 25224 145 145 0 26151 0
[pid=32158] vsize: 105184
Current children cumulated CPU time (s) 898.64
Current children cumulated vsize (Kb) 107308

[startup+910.091 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 25955 0 0 0 90731 131 0 0 25 0 1 0 1796855671 107855872 25262 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 26332 25262 145 145 0 26187 0
[pid=32158] vsize: 105328
Current children cumulated CPU time (s) 908.63
Current children cumulated vsize (Kb) 107452

[startup+920.092 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 25997 0 0 0 91731 132 0 0 25 0 1 0 1796855671 108019712 25304 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 26372 25304 145 145 0 26227 0
[pid=32158] vsize: 105488
Current children cumulated CPU time (s) 918.64
Current children cumulated vsize (Kb) 107612

[startup+930.092 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 26046 0 0 0 92730 132 0 0 25 0 1 0 1796855671 108212224 25353 4294967295 134512640 135094434 3221224432 3221223088 134557818 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 26419 25353 145 145 0 26274 0
[pid=32158] vsize: 105676
Current children cumulated CPU time (s) 928.63
Current children cumulated vsize (Kb) 107800

[startup+940.093 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 26110 0 0 0 93729 132 0 0 25 0 1 0 1796855671 108466176 25417 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 26481 25417 145 145 0 26336 0
[pid=32158] vsize: 105924
Current children cumulated CPU time (s) 938.62
Current children cumulated vsize (Kb) 108048

[startup+950.094 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 26203 0 0 0 94728 132 0 0 25 0 1 0 1796855671 108834816 25510 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 26571 25510 145 145 0 26426 0
[pid=32158] vsize: 106284
Current children cumulated CPU time (s) 948.61
Current children cumulated vsize (Kb) 108408

[startup+960.095 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 26233 0 0 0 95728 133 0 0 25 0 1 0 1796855671 108953600 25540 4294967295 134512640 135094434 3221224432 3221223092 134553494 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 26600 25540 145 145 0 26455 0
[pid=32158] vsize: 106400
Current children cumulated CPU time (s) 958.62
Current children cumulated vsize (Kb) 108524

[startup+970.095 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 26299 0 0 0 96727 133 0 0 25 0 1 0 1796855671 109211648 25606 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 26663 25606 145 145 0 26518 0
[pid=32158] vsize: 106652
Current children cumulated CPU time (s) 968.61
Current children cumulated vsize (Kb) 108776

[startup+980.095 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 26413 0 0 0 97725 134 0 0 25 0 1 0 1796855671 110714880 25720 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 27030 25720 145 145 0 26885 0
[pid=32158] vsize: 108120
Current children cumulated CPU time (s) 978.6
Current children cumulated vsize (Kb) 110244

[startup+990.096 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 26442 0 0 0 98725 134 0 0 25 0 1 0 1796855671 110829568 25749 4294967295 134512640 135094434 3221224432 3221223120 134558992 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 27058 25749 145 145 0 26913 0
[pid=32158] vsize: 108232
Current children cumulated CPU time (s) 988.6
Current children cumulated vsize (Kb) 110356

[startup+1000.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 26468 0 0 0 99725 134 0 0 25 0 1 0 1796855671 110931968 25775 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 27083 25775 145 145 0 26938 0
[pid=32158] vsize: 108332
Current children cumulated CPU time (s) 998.6
Current children cumulated vsize (Kb) 110456

[startup+1010.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 26502 0 0 0 100724 134 0 0 25 0 1 0 1796855671 111063040 25809 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 27115 25809 145 145 0 26970 0
[pid=32158] vsize: 108460
Current children cumulated CPU time (s) 1008.59
Current children cumulated vsize (Kb) 110584

[startup+1020.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 26525 0 0 0 101724 135 0 0 25 0 1 0 1796855671 111153152 25832 4294967295 134512640 135094434 3221224432 3221223056 134557636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 27137 25832 145 145 0 26992 0
[pid=32158] vsize: 108548
Current children cumulated CPU time (s) 1018.6
Current children cumulated vsize (Kb) 110672

[startup+1030.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 26568 0 0 0 102723 135 0 0 25 0 1 0 1796855671 111321088 25875 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 27178 25875 145 145 0 27033 0
[pid=32158] vsize: 108712
Current children cumulated CPU time (s) 1028.59
Current children cumulated vsize (Kb) 110836

[startup+1040.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 26619 0 0 0 103722 136 0 0 25 0 1 0 1796855671 111521792 25926 4294967295 134512640 135094434 3221224432 3221223120 134554851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 27227 25926 145 145 0 27082 0
[pid=32158] vsize: 108908
Current children cumulated CPU time (s) 1038.59
Current children cumulated vsize (Kb) 111032

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 26735 0 0 0 104721 136 0 0 25 0 1 0 1796855671 111984640 26042 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 27340 26042 145 145 0 27195 0
[pid=32158] vsize: 109360
Current children cumulated CPU time (s) 1048.58
Current children cumulated vsize (Kb) 111484

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 26860 0 0 0 105719 137 0 0 25 0 1 0 1796855671 112484352 26167 4294967295 134512640 135094434 3221224432 3221223044 134563024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 27462 26167 145 145 0 27317 0
[pid=32158] vsize: 109848
Current children cumulated CPU time (s) 1058.57
Current children cumulated vsize (Kb) 111972

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 26906 0 0 0 106719 137 0 0 25 0 1 0 1796855671 112664576 26213 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 27506 26213 145 145 0 27361 0
[pid=32158] vsize: 110024
Current children cumulated CPU time (s) 1068.57
Current children cumulated vsize (Kb) 112148

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 26952 0 0 0 107718 138 0 0 25 0 1 0 1796855671 112844800 26259 4294967295 134512640 135094434 3221224432 3221223056 134557612 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 27550 26259 145 145 0 27405 0
[pid=32158] vsize: 110200
Current children cumulated CPU time (s) 1078.57
Current children cumulated vsize (Kb) 112324

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 27018 0 0 0 108717 139 0 0 25 0 1 0 1796855671 113102848 26325 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 27613 26325 145 145 0 27468 0
[pid=32158] vsize: 110452
Current children cumulated CPU time (s) 1088.57
Current children cumulated vsize (Kb) 112576

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 27275 0 0 0 109714 139 0 0 25 0 1 0 1796855671 114130944 26582 4294967295 134512640 135094434 3221224432 3221223072 134562139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 27864 26582 145 145 0 27719 0
[pid=32158] vsize: 111456
Current children cumulated CPU time (s) 1098.54
Current children cumulated vsize (Kb) 113580

[startup+1110.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 27416 0 0 0 110710 141 0 0 25 0 1 0 1796855671 114692096 26723 4294967295 134512640 135094434 3221224432 3221223104 134553437 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32158/statm): 28001 26723 145 145 0 27856 0
[pid=32158] vsize: 112004
Current children cumulated CPU time (s) 1108.52
Current children cumulated vsize (Kb) 114128

[startup+1120.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 27495 0 0 0 111708 141 0 0 25 0 1 0 1796855671 115003392 26802 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 28077 26802 145 145 0 27932 0
[pid=32158] vsize: 112308
Current children cumulated CPU time (s) 1118.5
Current children cumulated vsize (Kb) 114432

[startup+1130.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 27530 0 0 0 112707 142 0 0 25 0 1 0 1796855671 115146752 26837 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 28112 26837 145 145 0 27967 0
[pid=32158] vsize: 112448
Current children cumulated CPU time (s) 1128.5
Current children cumulated vsize (Kb) 114572

[startup+1140.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 27621 0 0 0 113706 142 0 0 25 0 1 0 1796855671 115511296 26928 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 28201 26928 145 145 0 28056 0
[pid=32158] vsize: 112804
Current children cumulated CPU time (s) 1138.49
Current children cumulated vsize (Kb) 114928

[startup+1150.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 27669 0 0 0 114705 143 0 0 25 0 1 0 1796855671 115699712 26976 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 28247 26976 145 145 0 28102 0
[pid=32158] vsize: 112988
Current children cumulated CPU time (s) 1148.49
Current children cumulated vsize (Kb) 115112

[startup+1160.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 27713 0 0 0 115705 143 0 0 25 0 1 0 1796855671 115871744 27020 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 28289 27020 145 145 0 28144 0
[pid=32158] vsize: 113156
Current children cumulated CPU time (s) 1158.49
Current children cumulated vsize (Kb) 115280

[startup+1170.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 27755 0 0 0 116704 143 0 0 25 0 1 0 1796855671 116035584 27062 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 28329 27062 145 145 0 28184 0
[pid=32158] vsize: 113316
Current children cumulated CPU time (s) 1168.48
Current children cumulated vsize (Kb) 115440

[startup+1180.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 27940 0 0 0 117700 145 0 0 25 0 1 0 1796855671 116781056 27247 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 28511 27247 145 145 0 28366 0
[pid=32158] vsize: 114044
Current children cumulated CPU time (s) 1178.46
Current children cumulated vsize (Kb) 116168

[startup+1190.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 28000 0 0 0 118699 145 0 0 25 0 1 0 1796855671 117018624 27307 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 28569 27307 145 145 0 28424 0
[pid=32158] vsize: 114276
Current children cumulated CPU time (s) 1188.45
Current children cumulated vsize (Kb) 116400

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 28139 0 0 0 119697 146 0 0 25 0 1 0 1796855671 117575680 27446 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 28705 27446 145 145 0 28560 0
[pid=32158] vsize: 114820
Current children cumulated CPU time (s) 1198.44
Current children cumulated vsize (Kb) 116944

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 28217 0 0 0 120697 146 0 0 25 0 1 0 1796855671 117866496 27524 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 28776 27524 145 145 0 28631 0
[pid=32158] vsize: 115104
Current children cumulated CPU time (s) 1208.44
Current children cumulated vsize (Kb) 117228



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 32158
Raw data (/proc/32154/stat): 32154 (minisat+_script) S 32153 32154 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796855666 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32154/statm): 531 226 485 147 0 384 0
[pid=32154] vsize: 2124
Raw data (/proc/32158/stat): 32158 (minisat+_64-bit) R 32154 32154 9854 0 -1 0 28217 0 0 0 120697 146 0 0 25 0 1 0 1796855671 117866496 27524 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32158/statm): 28776 27524 145 145 0 28631 0
[pid=32158] vsize: 115104
Current children cumulated CPU time (s) 1208.44
Current children cumulated vsize (Kb) 117228

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

Child status: 0
Real time (s): 1210.17
CPU time (s): 1208.49
CPU user time (s): 1206.97
CPU system time (s): 1.51677
CPU usage (%): 99.8613
Max. virtual memory (cumulated for all children) (Kb): 117228