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/17952/stat): 17952 (minisat+_script) R 17951 17952 15400 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1783146834 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/17952/statm): 174 3 169 147 0 27 0
[pid=17952] 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=17953
New process pid=17954
New process pid=17955
execve syscall for /bin/sed executable
One traced child (pid=17954) 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=17955) exited with status: 0
One traced child (pid=17953) exited with status: 0
New process pid=17956
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc7/normalized-bench1.pi.opb

[startup+10.0034 s]
Raw data (loadavg): 0.93 0.95 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) T 17952 17952 15400 0 -1 0 7169 0 0 0 955 24 0 0 25 0 1 0 1783146839 26468352 5835 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/17956/statm): 6462 5835 145 145 0 6317 0
[pid=17956] vsize: 25848
Current children cumulated CPU time (s) 9.8
Current children cumulated vsize (Kb) 27972

[startup+20.004 s]
Raw data (loadavg): 0.94 0.96 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 7579 0 0 0 1948 28 0 0 25 0 1 0 1783146839 28164096 6245 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 6876 6245 145 145 0 6731 0
[pid=17956] vsize: 27504
Current children cumulated CPU time (s) 19.77
Current children cumulated vsize (Kb) 29628

[startup+30.0047 s]
Raw data (loadavg): 0.95 0.96 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 8307 0 0 0 2935 32 0 0 25 0 1 0 1783146839 31170560 6973 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 7610 6973 145 145 0 7465 0
[pid=17956] vsize: 30440
Current children cumulated CPU time (s) 29.68
Current children cumulated vsize (Kb) 32564

[startup+40.0053 s]
Raw data (loadavg): 0.95 0.96 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 9287 0 0 0 3920 39 0 0 25 0 1 0 1783146839 35155968 7953 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 8583 7953 145 145 0 8438 0
[pid=17956] vsize: 34332
Current children cumulated CPU time (s) 39.6
Current children cumulated vsize (Kb) 36456

[startup+50.0069 s]
Raw data (loadavg): 0.96 0.96 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 10060 0 0 0 4907 44 0 0 25 0 1 0 1783146839 38301696 8726 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 9351 8726 145 145 0 9206 0
[pid=17956] vsize: 37404
Current children cumulated CPU time (s) 49.52
Current children cumulated vsize (Kb) 39528

[startup+60.0076 s]
Raw data (loadavg): 0.97 0.96 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 11159 0 0 0 5891 52 0 0 25 0 1 0 1783146839 42921984 9825 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 10479 9825 145 145 0 10334 0
[pid=17956] vsize: 41916
Current children cumulated CPU time (s) 59.44
Current children cumulated vsize (Kb) 44040

[startup+70.0082 s]
Raw data (loadavg): 0.97 0.96 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 12259 0 0 0 6872 60 0 0 25 0 1 0 1783146839 47427584 10925 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 11579 10925 145 145 0 11434 0
[pid=17956] vsize: 46316
Current children cumulated CPU time (s) 69.33
Current children cumulated vsize (Kb) 48440

[startup+80.0098 s]
Raw data (loadavg): 0.98 0.96 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 13316 0 0 0 7856 67 0 0 25 0 1 0 1783146839 51740672 11982 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17956/statm): 12632 11982 145 145 0 12487 0
[pid=17956] vsize: 50528
Current children cumulated CPU time (s) 79.24
Current children cumulated vsize (Kb) 52652

[startup+90.0105 s]
Raw data (loadavg): 0.98 0.96 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 14584 0 0 0 8836 75 0 0 25 0 1 0 1783146839 56918016 13250 4294967295 134512640 135094434 3221224448 3221223040 134557404 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 13896 13250 145 145 0 13751 0
[pid=17956] vsize: 55584
Current children cumulated CPU time (s) 89.12
Current children cumulated vsize (Kb) 57708

[startup+100.011 s]
Raw data (loadavg): 0.98 0.96 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 15609 0 0 0 9819 82 0 0 25 0 1 0 1783146839 61104128 14275 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 14918 14275 145 145 0 14773 0
[pid=17956] vsize: 59672
Current children cumulated CPU time (s) 99.02
Current children cumulated vsize (Kb) 61796

[startup+110.012 s]
Raw data (loadavg): 0.98 0.96 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 16787 0 0 0 10802 88 0 0 25 0 1 0 1783146839 65921024 15453 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 16094 15453 145 145 0 15949 0
[pid=17956] vsize: 64376
Current children cumulated CPU time (s) 108.91
Current children cumulated vsize (Kb) 66500

[startup+120.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 17701 0 0 0 11785 96 0 0 25 0 1 0 1783146839 69636096 16367 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 17001 16367 145 145 0 16856 0
[pid=17956] vsize: 68004
Current children cumulated CPU time (s) 118.82
Current children cumulated vsize (Kb) 70128

[startup+130.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 18761 0 0 0 12768 105 0 0 25 0 1 0 1783146839 73965568 17427 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 18058 17427 145 145 0 17913 0
[pid=17956] vsize: 72232
Current children cumulated CPU time (s) 128.74
Current children cumulated vsize (Kb) 74356

[startup+140.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 19792 0 0 0 13752 111 0 0 25 0 1 0 1783146839 78176256 18458 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 19086 18458 145 145 0 18941 0
[pid=17956] vsize: 76344
Current children cumulated CPU time (s) 138.64
Current children cumulated vsize (Kb) 78468

[startup+150.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 20700 0 0 0 14737 116 0 0 25 0 1 0 1783146839 82153472 19366 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 20057 19366 145 145 0 19912 0
[pid=17956] vsize: 80228
Current children cumulated CPU time (s) 148.54
Current children cumulated vsize (Kb) 82352

[startup+160.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 21574 0 0 0 15722 122 0 0 25 0 1 0 1783146839 85721088 20240 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 20928 20240 145 145 0 20783 0
[pid=17956] vsize: 83712
Current children cumulated CPU time (s) 158.45
Current children cumulated vsize (Kb) 85836

[startup+170.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 22479 0 0 0 16707 128 0 0 25 0 1 0 1783146839 89419776 21145 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17956/statm): 21831 21145 145 145 0 21686 0
[pid=17956] vsize: 87324
Current children cumulated CPU time (s) 168.36
Current children cumulated vsize (Kb) 89448

[startup+180.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) T 17952 17952 15400 0 -1 0 23368 0 0 0 17691 135 0 0 25 0 1 0 1783146839 93052928 22034 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/17956/statm): 22718 22034 145 145 0 22573 0
[pid=17956] vsize: 90872
Current children cumulated CPU time (s) 178.27
Current children cumulated vsize (Kb) 92996

[startup+190.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 24185 0 0 0 18677 141 0 0 25 0 1 0 1783146839 96407552 22851 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 23537 22851 145 145 0 23392 0
[pid=17956] vsize: 94148
Current children cumulated CPU time (s) 188.19
Current children cumulated vsize (Kb) 96272

[startup+200.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 24844 0 0 0 19666 144 0 0 25 0 1 0 1783146839 99110912 23510 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 24197 23510 145 145 0 24052 0
[pid=17956] vsize: 96788
Current children cumulated CPU time (s) 198.11
Current children cumulated vsize (Kb) 98912

[startup+210.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 25569 0 0 0 20653 149 0 0 25 0 1 0 1783146839 102076416 24235 4294967295 134512640 135094434 3221224448 3221223120 134556513 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 24921 24235 145 145 0 24776 0
[pid=17956] vsize: 99684
Current children cumulated CPU time (s) 208.03
Current children cumulated vsize (Kb) 101808

[startup+220.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 26246 0 0 0 21642 154 0 0 25 0 1 0 1783146839 104849408 24912 4294967295 134512640 135094434 3221224448 3221222976 134783376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 25598 24912 145 145 0 25453 0
[pid=17956] vsize: 102392
Current children cumulated CPU time (s) 217.97
Current children cumulated vsize (Kb) 104516

[startup+230.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 26938 0 0 0 22629 159 0 0 25 0 1 0 1783146839 107675648 25604 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 26288 25604 145 145 0 26143 0
[pid=17956] vsize: 105152
Current children cumulated CPU time (s) 227.89
Current children cumulated vsize (Kb) 107276

[startup+240.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 27592 0 0 0 23619 164 0 0 25 0 1 0 1783146839 110362624 26258 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 26944 26258 145 145 0 26799 0
[pid=17956] vsize: 107776
Current children cumulated CPU time (s) 237.84
Current children cumulated vsize (Kb) 109900

[startup+250.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) T 17952 17952 15400 0 -1 0 28411 0 0 0 24606 169 0 0 25 0 1 0 1783146839 113717248 27077 4294967295 134512640 135094434 3221224448 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/17956/statm): 27763 27077 145 145 0 27618 0
[pid=17956] vsize: 111052
Current children cumulated CPU time (s) 247.76
Current children cumulated vsize (Kb) 113176

[startup+260.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 28635 0 0 0 25602 171 0 0 25 0 1 0 1783146839 114638848 27301 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17956/statm): 27988 27301 145 145 0 27843 0
[pid=17956] vsize: 111952
Current children cumulated CPU time (s) 257.74
Current children cumulated vsize (Kb) 114076

[startup+270.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 28635 0 0 0 26601 171 0 0 25 0 1 0 1783146839 114638848 27301 4294967295 134512640 135094434 3221224448 3221223040 134557040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 27988 27301 145 145 0 27843 0
[pid=17956] vsize: 111952
Current children cumulated CPU time (s) 267.73
Current children cumulated vsize (Kb) 114076

[startup+280.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 28635 0 0 0 27601 171 0 0 25 0 1 0 1783146839 114638848 27301 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 27988 27301 145 145 0 27843 0
[pid=17956] vsize: 111952
Current children cumulated CPU time (s) 277.73
Current children cumulated vsize (Kb) 114076

[startup+290.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 28635 0 0 0 28601 171 0 0 25 0 1 0 1783146839 114638848 27301 4294967295 134512640 135094434 3221224448 3221223040 134557421 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 27988 27301 145 145 0 27843 0
[pid=17956] vsize: 111952
Current children cumulated CPU time (s) 287.73
Current children cumulated vsize (Kb) 114076

[startup+300.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 28635 0 0 0 29602 171 0 0 25 0 1 0 1783146839 114638848 27301 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 27988 27301 145 145 0 27843 0
[pid=17956] vsize: 111952
Current children cumulated CPU time (s) 297.74
Current children cumulated vsize (Kb) 114076

[startup+310.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 28635 0 0 0 30602 171 0 0 25 0 1 0 1783146839 114638848 27301 4294967295 134512640 135094434 3221224448 3221223104 134557956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 27988 27301 145 145 0 27843 0
[pid=17956] vsize: 111952
Current children cumulated CPU time (s) 307.74
Current children cumulated vsize (Kb) 114076

[startup+320.027 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 28635 0 0 0 31602 171 0 0 25 0 1 0 1783146839 114638848 27301 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 27988 27301 145 145 0 27843 0
[pid=17956] vsize: 111952
Current children cumulated CPU time (s) 317.74
Current children cumulated vsize (Kb) 114076

[startup+330.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 28635 0 0 0 32602 171 0 0 25 0 1 0 1783146839 114638848 27301 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 27988 27301 145 145 0 27843 0
[pid=17956] vsize: 111952
Current children cumulated CPU time (s) 327.74
Current children cumulated vsize (Kb) 114076

[startup+340.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 28635 0 0 0 33603 171 0 0 25 0 1 0 1783146839 114638848 27301 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 27988 27301 145 145 0 27843 0
[pid=17956] vsize: 111952
Current children cumulated CPU time (s) 337.75
Current children cumulated vsize (Kb) 114076

[startup+350.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 28635 0 0 0 34603 171 0 0 25 0 1 0 1783146839 114638848 27301 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 27988 27301 145 145 0 27843 0
[pid=17956] vsize: 111952
Current children cumulated CPU time (s) 347.75
Current children cumulated vsize (Kb) 114076

[startup+360.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 28635 0 0 0 35603 171 0 0 25 0 1 0 1783146839 114638848 27301 4294967295 134512640 135094434 3221224448 3221223040 134551897 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 27988 27301 145 145 0 27843 0
[pid=17956] vsize: 111952
Current children cumulated CPU time (s) 357.75
Current children cumulated vsize (Kb) 114076

[startup+370.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 28635 0 0 0 36603 172 0 0 25 0 1 0 1783146839 114638848 27301 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 27988 27301 145 145 0 27843 0
[pid=17956] vsize: 111952
Current children cumulated CPU time (s) 367.76
Current children cumulated vsize (Kb) 114076

[startup+380.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 28635 0 0 0 37603 172 0 0 25 0 1 0 1783146839 114638848 27301 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 27988 27301 145 145 0 27843 0
[pid=17956] vsize: 111952
Current children cumulated CPU time (s) 377.76
Current children cumulated vsize (Kb) 114076

[startup+390.033 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 28635 0 0 0 38604 172 0 0 25 0 1 0 1783146839 114638848 27301 4294967295 134512640 135094434 3221224448 3221223104 134557956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 27988 27301 145 145 0 27843 0
[pid=17956] vsize: 111952
Current children cumulated CPU time (s) 387.77
Current children cumulated vsize (Kb) 114076

[startup+400.034 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 28635 0 0 0 39604 172 0 0 25 0 1 0 1783146839 114638848 27301 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 27988 27301 145 145 0 27843 0
[pid=17956] vsize: 111952
Current children cumulated CPU time (s) 397.77
Current children cumulated vsize (Kb) 114076

[startup+410.035 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 28635 0 0 0 40604 172 0 0 25 0 1 0 1783146839 114638848 27301 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 27988 27301 145 145 0 27843 0
[pid=17956] vsize: 111952
Current children cumulated CPU time (s) 407.77
Current children cumulated vsize (Kb) 114076

[startup+420.035 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 29014 0 0 0 41597 174 0 0 25 0 1 0 1783146839 116203520 27680 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 28370 27680 145 145 0 28225 0
[pid=17956] vsize: 113480
Current children cumulated CPU time (s) 417.72
Current children cumulated vsize (Kb) 115604

[startup+430.036 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 29896 0 0 0 42583 180 0 0 25 0 1 0 1783146839 119824384 28562 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 29254 28562 145 145 0 29109 0
[pid=17956] vsize: 117016
Current children cumulated CPU time (s) 427.64
Current children cumulated vsize (Kb) 119140

[startup+440.037 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 30730 0 0 0 43572 184 0 0 25 0 1 0 1783146839 123244544 29396 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 30089 29396 145 145 0 29944 0
[pid=17956] vsize: 120356
Current children cumulated CPU time (s) 437.57
Current children cumulated vsize (Kb) 122480

[startup+450.037 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 31536 0 0 0 44561 188 0 0 25 0 1 0 1783146839 126554112 30202 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 30897 30202 145 145 0 30752 0
[pid=17956] vsize: 123588
Current children cumulated CPU time (s) 447.5
Current children cumulated vsize (Kb) 125712

[startup+460.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 32365 0 0 0 45548 193 0 0 25 0 1 0 1783146839 129970176 31031 4294967295 134512640 135094434 3221224448 3221223040 134557352 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 31731 31031 145 145 0 31586 0
[pid=17956] vsize: 126924
Current children cumulated CPU time (s) 457.42
Current children cumulated vsize (Kb) 129048

[startup+470.039 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 33180 0 0 0 46536 197 0 0 25 0 1 0 1783146839 133324800 31846 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 32550 31846 145 145 0 32405 0
[pid=17956] vsize: 130200
Current children cumulated CPU time (s) 467.34
Current children cumulated vsize (Kb) 132324

[startup+480.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 34020 0 0 0 47524 203 0 0 25 0 1 0 1783146839 136753152 32686 4294967295 134512640 135094434 3221224448 3221223040 134557199 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 33387 32686 145 145 0 33242 0
[pid=17956] vsize: 133548
Current children cumulated CPU time (s) 477.28
Current children cumulated vsize (Kb) 135672

[startup+490.041 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 34732 0 0 0 48514 207 0 0 25 0 1 0 1783146839 139689984 33398 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 34104 33398 145 145 0 33959 0
[pid=17956] vsize: 136416
Current children cumulated CPU time (s) 487.22
Current children cumulated vsize (Kb) 138540

[startup+500.043 s]
Raw data (loadavg): 0.99 0.97 0.94 1/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) T 17952 17952 15400 0 -1 0 35456 0 0 0 49503 212 0 0 25 0 1 0 1783146839 142635008 34122 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/17956/statm): 34823 34122 145 145 0 34678 0
[pid=17956] vsize: 139292
Current children cumulated CPU time (s) 497.16
Current children cumulated vsize (Kb) 141416

[startup+510.043 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 36162 0 0 0 50492 217 0 0 25 0 1 0 1783146839 145522688 34828 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17956/statm): 35528 34828 145 145 0 35383 0
[pid=17956] vsize: 142112
Current children cumulated CPU time (s) 507.1
Current children cumulated vsize (Kb) 144236

[startup+520.044 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 36645 0 0 0 51486 220 0 0 25 0 1 0 1783146839 147517440 35311 4294967295 134512640 135094434 3221224448 3221223040 134552106 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 36015 35311 145 145 0 35870 0
[pid=17956] vsize: 144060
Current children cumulated CPU time (s) 517.07
Current children cumulated vsize (Kb) 146184

[startup+530.044 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 37198 0 0 0 52476 225 0 0 25 0 1 0 1783146839 149798912 35864 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 36572 35864 145 145 0 36427 0
[pid=17956] vsize: 146288
Current children cumulated CPU time (s) 527.02
Current children cumulated vsize (Kb) 148412

[startup+540.047 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 37680 0 0 0 53469 228 0 0 25 0 1 0 1783146839 151785472 36346 4294967295 134512640 135094434 3221224448 3221222976 134780484 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 37057 36346 145 145 0 36912 0
[pid=17956] vsize: 148228
Current children cumulated CPU time (s) 536.98
Current children cumulated vsize (Kb) 150352

[startup+550.048 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 38182 0 0 0 54460 233 0 0 25 0 1 0 1783146839 153829376 36848 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 37556 36848 145 145 0 37411 0
[pid=17956] vsize: 150224
Current children cumulated CPU time (s) 546.94
Current children cumulated vsize (Kb) 152348

[startup+560.048 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 38648 0 0 0 55452 237 0 0 25 0 1 0 1783146839 155729920 37314 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 38020 37314 145 145 0 37875 0
[pid=17956] vsize: 152080
Current children cumulated CPU time (s) 556.9
Current children cumulated vsize (Kb) 154204

[startup+570.049 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 39078 0 0 0 56445 240 0 0 25 0 1 0 1783146839 157483008 37744 4294967295 134512640 135094434 3221224448 3221223040 134551434 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 38448 37744 145 145 0 38303 0
[pid=17956] vsize: 153792
Current children cumulated CPU time (s) 566.86
Current children cumulated vsize (Kb) 155916

[startup+580.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 39078 0 0 0 57445 240 0 0 25 0 1 0 1783146839 157483008 37744 4294967295 134512640 135094434 3221224448 3221223120 134556450 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 38448 37744 145 145 0 38303 0
[pid=17956] vsize: 153792
Current children cumulated CPU time (s) 576.86
Current children cumulated vsize (Kb) 155916

[startup+590.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 39078 0 0 0 58445 240 0 0 25 0 1 0 1783146839 157483008 37744 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 38448 37744 145 145 0 38303 0
[pid=17956] vsize: 153792
Current children cumulated CPU time (s) 586.86
Current children cumulated vsize (Kb) 155916

[startup+600.052 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 39078 0 0 0 59446 240 0 0 25 0 1 0 1783146839 157483008 37744 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 38448 37744 145 145 0 38303 0
[pid=17956] vsize: 153792
Current children cumulated CPU time (s) 596.87
Current children cumulated vsize (Kb) 155916

[startup+610.053 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 39078 0 0 0 60446 240 0 0 25 0 1 0 1783146839 157483008 37744 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 38448 37744 145 145 0 38303 0
[pid=17956] vsize: 153792
Current children cumulated CPU time (s) 606.87
Current children cumulated vsize (Kb) 155916

[startup+620.053 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 39078 0 0 0 61446 240 0 0 25 0 1 0 1783146839 157483008 37744 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 38448 37744 145 145 0 38303 0
[pid=17956] vsize: 153792
Current children cumulated CPU time (s) 616.87
Current children cumulated vsize (Kb) 155916

[startup+630.054 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 39078 0 0 0 62446 240 0 0 25 0 1 0 1783146839 157483008 37744 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 38448 37744 145 145 0 38303 0
[pid=17956] vsize: 153792
Current children cumulated CPU time (s) 626.87
Current children cumulated vsize (Kb) 155916

[startup+640.054 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 39078 0 0 0 63446 241 0 0 25 0 1 0 1783146839 157483008 37744 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 38448 37744 145 145 0 38303 0
[pid=17956] vsize: 153792
Current children cumulated CPU time (s) 636.88
Current children cumulated vsize (Kb) 155916

[startup+650.056 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 39078 0 0 0 64447 241 0 0 25 0 1 0 1783146839 157483008 37744 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 38448 37744 145 145 0 38303 0
[pid=17956] vsize: 153792
Current children cumulated CPU time (s) 646.89
Current children cumulated vsize (Kb) 155916

[startup+660.057 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 39078 0 0 0 65447 241 0 0 25 0 1 0 1783146839 157483008 37744 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 38448 37744 145 145 0 38303 0
[pid=17956] vsize: 153792
Current children cumulated CPU time (s) 656.89
Current children cumulated vsize (Kb) 155916

[startup+670.057 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 39078 0 0 0 66447 241 0 0 25 0 1 0 1783146839 157483008 37744 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 38448 37744 145 145 0 38303 0
[pid=17956] vsize: 153792
Current children cumulated CPU time (s) 666.89
Current children cumulated vsize (Kb) 155916

[startup+680.058 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 39078 0 0 0 67447 241 0 0 25 0 1 0 1783146839 157483008 37744 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 38448 37744 145 145 0 38303 0
[pid=17956] vsize: 153792
Current children cumulated CPU time (s) 676.89
Current children cumulated vsize (Kb) 155916

[startup+690.059 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 39078 0 0 0 68447 241 0 0 25 0 1 0 1783146839 157483008 37744 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 38448 37744 145 145 0 38303 0
[pid=17956] vsize: 153792
Current children cumulated CPU time (s) 686.89
Current children cumulated vsize (Kb) 155916

[startup+700.06 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 39078 0 0 0 69448 241 0 0 25 0 1 0 1783146839 157483008 37744 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 38448 37744 145 145 0 38303 0
[pid=17956] vsize: 153792
Current children cumulated CPU time (s) 696.9
Current children cumulated vsize (Kb) 155916

[startup+710.061 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 39078 0 0 0 70448 241 0 0 25 0 1 0 1783146839 157483008 37744 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 38448 37744 145 145 0 38303 0
[pid=17956] vsize: 153792
Current children cumulated CPU time (s) 706.9
Current children cumulated vsize (Kb) 155916

[startup+720.062 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 39078 0 0 0 71448 241 0 0 25 0 1 0 1783146839 157483008 37744 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 38448 37744 145 145 0 38303 0
[pid=17956] vsize: 153792
Current children cumulated CPU time (s) 716.9
Current children cumulated vsize (Kb) 155916

[startup+730.062 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 39078 0 0 0 72448 241 0 0 25 0 1 0 1783146839 157483008 37744 4294967295 134512640 135094434 3221224448 3221223060 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 38448 37744 145 145 0 38303 0
[pid=17956] vsize: 153792
Current children cumulated CPU time (s) 726.9
Current children cumulated vsize (Kb) 155916

[startup+740.063 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 39079 0 0 0 73448 241 0 0 25 0 1 0 1783146839 157483008 37745 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 38448 37745 145 145 0 38303 0
[pid=17956] vsize: 153792
Current children cumulated CPU time (s) 736.9
Current children cumulated vsize (Kb) 155916

[startup+750.064 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 39079 0 0 0 74448 241 0 0 25 0 1 0 1783146839 157483008 37745 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 38448 37745 145 145 0 38303 0
[pid=17956] vsize: 153792
Current children cumulated CPU time (s) 746.9
Current children cumulated vsize (Kb) 155916

[startup+760.065 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 39079 0 0 0 75448 241 0 0 25 0 1 0 1783146839 157483008 37745 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 38448 37745 145 145 0 38303 0
[pid=17956] vsize: 153792
Current children cumulated CPU time (s) 756.9
Current children cumulated vsize (Kb) 155916

[startup+770.066 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 39079 0 0 0 76448 241 0 0 25 0 1 0 1783146839 157483008 37745 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 38448 37745 145 145 0 38303 0
[pid=17956] vsize: 153792
Current children cumulated CPU time (s) 766.9
Current children cumulated vsize (Kb) 155916

[startup+780.067 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 39079 0 0 0 77449 241 0 0 25 0 1 0 1783146839 157483008 37745 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 38448 37745 145 145 0 38303 0
[pid=17956] vsize: 153792
Current children cumulated CPU time (s) 776.91
Current children cumulated vsize (Kb) 155916

[startup+790.068 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 39079 0 0 0 78449 241 0 0 25 0 1 0 1783146839 157483008 37745 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 38448 37745 145 145 0 38303 0
[pid=17956] vsize: 153792
Current children cumulated CPU time (s) 786.91
Current children cumulated vsize (Kb) 155916

[startup+800.07 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 39079 0 0 0 79449 241 0 0 25 0 1 0 1783146839 157483008 37745 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 38448 37745 145 145 0 38303 0
[pid=17956] vsize: 153792
Current children cumulated CPU time (s) 796.91
Current children cumulated vsize (Kb) 155916

[startup+810.07 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 39079 0 0 0 80449 242 0 0 25 0 1 0 1783146839 157483008 37745 4294967295 134512640 135094434 3221224448 3221223112 134555971 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 38448 37745 145 145 0 38303 0
[pid=17956] vsize: 153792
Current children cumulated CPU time (s) 806.92
Current children cumulated vsize (Kb) 155916

[startup+820.071 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 39079 0 0 0 81450 242 0 0 25 0 1 0 1783146839 157483008 37745 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 38448 37745 145 145 0 38303 0
[pid=17956] vsize: 153792
Current children cumulated CPU time (s) 816.93
Current children cumulated vsize (Kb) 155916

[startup+830.072 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 39079 0 0 0 82450 242 0 0 25 0 1 0 1783146839 157483008 37745 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 38448 37745 145 145 0 38303 0
[pid=17956] vsize: 153792
Current children cumulated CPU time (s) 826.93
Current children cumulated vsize (Kb) 155916

[startup+840.072 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 39079 0 0 0 83450 242 0 0 25 0 1 0 1783146839 157483008 37745 4294967295 134512640 135094434 3221224448 3221223120 134555666 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 38448 37745 145 145 0 38303 0
[pid=17956] vsize: 153792
Current children cumulated CPU time (s) 836.93
Current children cumulated vsize (Kb) 155916

[startup+850.074 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 39079 0 0 0 84451 242 0 0 25 0 1 0 1783146839 157483008 37745 4294967295 134512640 135094434 3221224448 3221223104 134558156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 38448 37745 145 145 0 38303 0
[pid=17956] vsize: 153792
Current children cumulated CPU time (s) 846.94
Current children cumulated vsize (Kb) 155916

[startup+860.074 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 39079 0 0 0 85451 242 0 0 25 0 1 0 1783146839 157483008 37745 4294967295 134512640 135094434 3221224448 3221223120 134556288 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 38448 37745 145 145 0 38303 0
[pid=17956] vsize: 153792
Current children cumulated CPU time (s) 856.94
Current children cumulated vsize (Kb) 155916

[startup+870.075 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 39079 0 0 0 86451 242 0 0 25 0 1 0 1783146839 157483008 37745 4294967295 134512640 135094434 3221224448 3221223112 134555971 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 38448 37745 145 145 0 38303 0
[pid=17956] vsize: 153792
Current children cumulated CPU time (s) 866.94
Current children cumulated vsize (Kb) 155916

[startup+880.076 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 39079 0 0 0 87451 242 0 0 25 0 1 0 1783146839 157483008 37745 4294967295 134512640 135094434 3221224448 3221223040 134557213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 38448 37745 145 145 0 38303 0
[pid=17956] vsize: 153792
Current children cumulated CPU time (s) 876.94
Current children cumulated vsize (Kb) 155916

[startup+890.076 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 39079 0 0 0 88451 242 0 0 25 0 1 0 1783146839 157483008 37745 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 38448 37745 145 145 0 38303 0
[pid=17956] vsize: 153792
Current children cumulated CPU time (s) 886.94
Current children cumulated vsize (Kb) 155916

[startup+900.078 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 39079 0 0 0 89452 242 0 0 25 0 1 0 1783146839 157483008 37745 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 38448 37745 145 145 0 38303 0
[pid=17956] vsize: 153792
Current children cumulated CPU time (s) 896.95
Current children cumulated vsize (Kb) 155916

[startup+910.079 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 39079 0 0 0 90452 242 0 0 25 0 1 0 1783146839 157483008 37745 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 38448 37745 145 145 0 38303 0
[pid=17956] vsize: 153792
Current children cumulated CPU time (s) 906.95
Current children cumulated vsize (Kb) 155916

[startup+920.079 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 39079 0 0 0 91452 242 0 0 25 0 1 0 1783146839 157483008 37745 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 38448 37745 145 145 0 38303 0
[pid=17956] vsize: 153792
Current children cumulated CPU time (s) 916.95
Current children cumulated vsize (Kb) 155916

[startup+930.08 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 39143 0 0 0 92451 242 0 0 25 0 1 0 1783146839 157745152 37809 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 38512 37809 145 145 0 38367 0
[pid=17956] vsize: 154048
Current children cumulated CPU time (s) 926.94
Current children cumulated vsize (Kb) 156172

[startup+940.081 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 39742 0 0 0 93441 247 0 0 25 0 1 0 1783146839 160206848 38408 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 39113 38408 145 145 0 38968 0
[pid=17956] vsize: 156452
Current children cumulated CPU time (s) 936.89
Current children cumulated vsize (Kb) 158576

[startup+950.082 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 40366 0 0 0 94430 252 0 0 25 0 1 0 1783146839 162770944 39032 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 39739 39032 145 145 0 39594 0
[pid=17956] vsize: 158956
Current children cumulated CPU time (s) 946.83
Current children cumulated vsize (Kb) 161080

[startup+960.083 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 40928 0 0 0 95421 256 0 0 25 0 1 0 1783146839 165072896 39594 4294967295 134512640 135094434 3221224448 3221223104 134557972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 40301 39594 145 145 0 40156 0
[pid=17956] vsize: 161204
Current children cumulated CPU time (s) 956.78
Current children cumulated vsize (Kb) 163328

[startup+970.083 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 41526 0 0 0 96412 260 0 0 25 0 1 0 1783146839 167526400 40192 4294967295 134512640 135094434 3221224448 3221223040 134557319 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 40900 40192 145 145 0 40755 0
[pid=17956] vsize: 163600
Current children cumulated CPU time (s) 966.73
Current children cumulated vsize (Kb) 165724

[startup+980.084 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 42002 0 0 0 97404 263 0 0 25 0 1 0 1783146839 169488384 40668 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 41379 40668 145 145 0 41234 0
[pid=17956] vsize: 165516
Current children cumulated CPU time (s) 976.68
Current children cumulated vsize (Kb) 167640

[startup+990.085 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 42513 0 0 0 98397 266 0 0 25 0 1 0 1783146839 171581440 41179 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17956/statm): 41890 41179 145 145 0 41745 0
[pid=17956] vsize: 167560
Current children cumulated CPU time (s) 986.64
Current children cumulated vsize (Kb) 169684

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 42993 0 0 0 99388 270 0 0 25 0 1 0 1783146839 173535232 41659 4294967295 134512640 135094434 3221224448 3221223120 134555950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 42367 41659 145 145 0 42222 0
[pid=17956] vsize: 169468
Current children cumulated CPU time (s) 996.59
Current children cumulated vsize (Kb) 171592

[startup+1010.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 43442 0 0 0 100381 273 0 0 25 0 1 0 1783146839 175374336 42108 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 42816 42108 145 145 0 42671 0
[pid=17956] vsize: 171264
Current children cumulated CPU time (s) 1006.55
Current children cumulated vsize (Kb) 173388

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 43909 0 0 0 101374 276 0 0 25 0 1 0 1783146839 177291264 42575 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 43284 42575 145 145 0 43139 0
[pid=17956] vsize: 173136
Current children cumulated CPU time (s) 1016.51
Current children cumulated vsize (Kb) 175260

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 44421 0 0 0 102366 280 0 0 25 0 1 0 1783146839 179396608 43087 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 43798 43087 145 145 0 43653 0
[pid=17956] vsize: 175192
Current children cumulated CPU time (s) 1026.47
Current children cumulated vsize (Kb) 177316

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 44792 0 0 0 103359 283 0 0 25 0 1 0 1783146839 180899840 43458 4294967295 134512640 135094434 3221224448 3221223040 134551434 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 44165 43458 145 145 0 44020 0
[pid=17956] vsize: 176660
Current children cumulated CPU time (s) 1036.43
Current children cumulated vsize (Kb) 178784

[startup+1050.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 44792 0 0 0 104360 283 0 0 25 0 1 0 1783146839 180899840 43458 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 44165 43458 145 145 0 44020 0
[pid=17956] vsize: 176660
Current children cumulated CPU time (s) 1046.44
Current children cumulated vsize (Kb) 178784

[startup+1060.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 44792 0 0 0 105360 283 0 0 25 0 1 0 1783146839 180899840 43458 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 44165 43458 145 145 0 44020 0
[pid=17956] vsize: 176660
Current children cumulated CPU time (s) 1056.44
Current children cumulated vsize (Kb) 178784

[startup+1070.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 44792 0 0 0 106360 283 0 0 25 0 1 0 1783146839 180899840 43458 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 44165 43458 145 145 0 44020 0
[pid=17956] vsize: 176660
Current children cumulated CPU time (s) 1066.44
Current children cumulated vsize (Kb) 178784

[startup+1080.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 44793 0 0 0 107360 283 0 0 25 0 1 0 1783146839 180899840 43459 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 44165 43459 145 145 0 44020 0
[pid=17956] vsize: 176660
Current children cumulated CPU time (s) 1076.44
Current children cumulated vsize (Kb) 178784

[startup+1090.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 44793 0 0 0 108361 283 0 0 25 0 1 0 1783146839 180899840 43459 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 44165 43459 145 145 0 44020 0
[pid=17956] vsize: 176660
Current children cumulated CPU time (s) 1086.45
Current children cumulated vsize (Kb) 178784

[startup+1100.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 44793 0 0 0 109361 283 0 0 25 0 1 0 1783146839 180899840 43459 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 44165 43459 145 145 0 44020 0
[pid=17956] vsize: 176660
Current children cumulated CPU time (s) 1096.45
Current children cumulated vsize (Kb) 178784

[startup+1110.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 44793 0 0 0 110361 283 0 0 25 0 1 0 1783146839 180899840 43459 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 44165 43459 145 145 0 44020 0
[pid=17956] vsize: 176660
Current children cumulated CPU time (s) 1106.45
Current children cumulated vsize (Kb) 178784

[startup+1120.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 44793 0 0 0 111361 283 0 0 25 0 1 0 1783146839 180899840 43459 4294967295 134512640 135094434 3221224448 3221223040 134551908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 44165 43459 145 145 0 44020 0
[pid=17956] vsize: 176660
Current children cumulated CPU time (s) 1116.45
Current children cumulated vsize (Kb) 178784

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 44793 0 0 0 112360 284 0 0 25 0 1 0 1783146839 180899840 43459 4294967295 134512640 135094434 3221224448 3221223040 134557410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 44165 43459 145 145 0 44020 0
[pid=17956] vsize: 176660
Current children cumulated CPU time (s) 1126.45
Current children cumulated vsize (Kb) 178784

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 44793 0 0 0 113360 284 0 0 25 0 1 0 1783146839 180899840 43459 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 44165 43459 145 145 0 44020 0
[pid=17956] vsize: 176660
Current children cumulated CPU time (s) 1136.45
Current children cumulated vsize (Kb) 178784

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 44793 0 0 0 114360 284 0 0 25 0 1 0 1783146839 180899840 43459 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 44165 43459 145 145 0 44020 0
[pid=17956] vsize: 176660
Current children cumulated CPU time (s) 1146.45
Current children cumulated vsize (Kb) 178784

[startup+1160.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 44793 0 0 0 115360 284 0 0 25 0 1 0 1783146839 180899840 43459 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 44165 43459 145 145 0 44020 0
[pid=17956] vsize: 176660
Current children cumulated CPU time (s) 1156.45
Current children cumulated vsize (Kb) 178784

[startup+1170.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 44794 0 0 0 116360 285 0 0 25 0 1 0 1783146839 180899840 43460 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17956/statm): 44165 43460 145 145 0 44020 0
[pid=17956] vsize: 176660
Current children cumulated CPU time (s) 1166.46
Current children cumulated vsize (Kb) 178784

[startup+1180.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 44794 0 0 0 117359 285 0 0 25 0 1 0 1783146839 180899840 43460 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 44165 43460 145 145 0 44020 0
[pid=17956] vsize: 176660
Current children cumulated CPU time (s) 1176.45
Current children cumulated vsize (Kb) 178784

[startup+1190.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 44794 0 0 0 118360 285 0 0 25 0 1 0 1783146839 180899840 43460 4294967295 134512640 135094434 3221224448 3221223060 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 44165 43460 145 145 0 44020 0
[pid=17956] vsize: 176660
Current children cumulated CPU time (s) 1186.46
Current children cumulated vsize (Kb) 178784

[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 44794 0 0 0 119360 285 0 0 25 0 1 0 1783146839 180899840 43460 4294967295 134512640 135094434 3221224448 3221223104 134557872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 44165 43460 145 145 0 44020 0
[pid=17956] vsize: 176660
Current children cumulated CPU time (s) 1196.46
Current children cumulated vsize (Kb) 178784

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 44794 0 0 0 120360 285 0 0 25 0 1 0 1783146839 180899840 43460 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 44165 43460 145 145 0 44020 0
[pid=17956] vsize: 176660
Current children cumulated CPU time (s) 1206.46
Current children cumulated vsize (Kb) 178784



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 17956
Raw data (/proc/17952/stat): 17952 (minisat+_script) S 17951 17952 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783146834 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17952/statm): 531 226 485 147 0 384 0
[pid=17952] vsize: 2124
Raw data (/proc/17956/stat): 17956 (minisat+_64-bit) R 17952 17952 15400 0 -1 0 44794 0 0 0 120360 285 0 0 25 0 1 0 1783146839 180899840 43460 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17956/statm): 44165 43460 145 145 0 44020 0
[pid=17956] vsize: 176660
Current children cumulated CPU time (s) 1206.46
Current children cumulated vsize (Kb) 178784

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

Child status: 10
Real time (s): 1210.2
CPU time (s): 1206.55
CPU user time (s): 1203.61
CPU system time (s): 2.93955
CPU usage (%): 99.6989
Max. virtual memory (cumulated for all children) (Kb): 178784