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

[startup+10.0044 s]
Raw data (loadavg): 0.93 0.95 0.90 1/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) T 26736 26736 9854 0 -1 0 14521 0 0 0 882 55 0 0 22 0 1 0 1793810496 64548864 13710 4294967295 134512640 135094434 3221224432 3221191164 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/26740/statm): 15759 13710 145 145 0 15614 0
[pid=26740] vsize: 63036
Current children cumulated CPU time (s) 9.37
Current children cumulated vsize (Kb) 65160

[startup+20.0062 s]
Raw data (loadavg): 0.94 0.96 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 18304 0 0 0 1849 71 0 0 25 0 1 0 1793810496 78131200 17493 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26740/statm): 19075 17493 145 145 0 18930 0
[pid=26740] vsize: 76300
Current children cumulated CPU time (s) 19.2
Current children cumulated vsize (Kb) 78424

[startup+30.007 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 18306 0 0 0 2848 71 0 0 25 0 1 0 1793810496 78131200 17495 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26740/statm): 19075 17495 145 145 0 18930 0
[pid=26740] vsize: 76300
Current children cumulated CPU time (s) 29.19
Current children cumulated vsize (Kb) 78424

[startup+40.0077 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 18315 0 0 0 3848 71 0 0 25 0 1 0 1793810496 78135296 17504 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19076 17504 145 145 0 18931 0
[pid=26740] vsize: 76304
Current children cumulated CPU time (s) 39.19
Current children cumulated vsize (Kb) 78428

[startup+50.0085 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 18315 0 0 0 4848 71 0 0 25 0 1 0 1793810496 78135296 17504 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19076 17504 145 145 0 18931 0
[pid=26740] vsize: 76304
Current children cumulated CPU time (s) 49.19
Current children cumulated vsize (Kb) 78428

[startup+60.0093 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 18315 0 0 0 5848 71 0 0 25 0 1 0 1793810496 78135296 17504 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19076 17504 145 145 0 18931 0
[pid=26740] vsize: 76304
Current children cumulated CPU time (s) 59.19
Current children cumulated vsize (Kb) 78428

[startup+70.0111 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 18316 0 0 0 6847 71 0 0 25 0 1 0 1793810496 78135296 17505 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19076 17505 145 145 0 18931 0
[pid=26740] vsize: 76304
Current children cumulated CPU time (s) 69.18
Current children cumulated vsize (Kb) 78428

[startup+80.0119 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 18320 0 0 0 7848 71 0 0 25 0 1 0 1793810496 78139392 17509 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19077 17509 145 145 0 18932 0
[pid=26740] vsize: 76308
Current children cumulated CPU time (s) 79.19
Current children cumulated vsize (Kb) 78432

[startup+90.0117 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 18322 0 0 0 8848 72 0 0 25 0 1 0 1793810496 78139392 17511 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19077 17511 145 145 0 18932 0
[pid=26740] vsize: 76308
Current children cumulated CPU time (s) 89.2
Current children cumulated vsize (Kb) 78432

[startup+100.012 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 18330 0 0 0 9848 72 0 0 25 0 1 0 1793810496 78155776 17519 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19081 17519 145 145 0 18936 0
[pid=26740] vsize: 76324
Current children cumulated CPU time (s) 99.2
Current children cumulated vsize (Kb) 78448

[startup+110.014 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 18334 0 0 0 10848 72 0 0 25 0 1 0 1793810496 78155776 17523 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19081 17523 145 145 0 18936 0
[pid=26740] vsize: 76324
Current children cumulated CPU time (s) 109.2
Current children cumulated vsize (Kb) 78448

[startup+120.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 18349 0 0 0 11848 72 0 0 25 0 1 0 1793810496 78204928 17538 4294967295 134512640 135094434 3221224432 3221223104 134553523 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19093 17538 145 145 0 18948 0
[pid=26740] vsize: 76372
Current children cumulated CPU time (s) 119.2
Current children cumulated vsize (Kb) 78496

[startup+130.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 18379 0 0 0 12848 72 0 0 25 0 1 0 1793810496 78311424 17568 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19119 17568 145 145 0 18974 0
[pid=26740] vsize: 76476
Current children cumulated CPU time (s) 129.2
Current children cumulated vsize (Kb) 78600

[startup+140.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 18396 0 0 0 13848 72 0 0 25 0 1 0 1793810496 78364672 17585 4294967295 134512640 135094434 3221224432 3221223136 134559005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19132 17585 145 145 0 18987 0
[pid=26740] vsize: 76528
Current children cumulated CPU time (s) 139.2
Current children cumulated vsize (Kb) 78652

[startup+150.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 18406 0 0 0 14848 72 0 0 25 0 1 0 1793810496 78401536 17595 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19141 17595 145 145 0 18996 0
[pid=26740] vsize: 76564
Current children cumulated CPU time (s) 149.2
Current children cumulated vsize (Kb) 78688

[startup+160.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 18423 0 0 0 15848 72 0 0 25 0 1 0 1793810496 78458880 17612 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19155 17612 145 145 0 19010 0
[pid=26740] vsize: 76620
Current children cumulated CPU time (s) 159.2
Current children cumulated vsize (Kb) 78744

[startup+170.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 18434 0 0 0 16848 72 0 0 25 0 1 0 1793810496 78499840 17623 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19165 17623 145 145 0 19020 0
[pid=26740] vsize: 76660
Current children cumulated CPU time (s) 169.2
Current children cumulated vsize (Kb) 78784

[startup+180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 18437 0 0 0 17848 72 0 0 25 0 1 0 1793810496 78512128 17626 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19168 17626 145 145 0 19023 0
[pid=26740] vsize: 76672
Current children cumulated CPU time (s) 179.2
Current children cumulated vsize (Kb) 78796

[startup+190.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 18463 0 0 0 18848 72 0 0 25 0 1 0 1793810496 78594048 17652 4294967295 134512640 135094434 3221224432 3221223128 134558980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19188 17652 145 145 0 19043 0
[pid=26740] vsize: 76752
Current children cumulated CPU time (s) 189.2
Current children cumulated vsize (Kb) 78876

[startup+200.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 18465 0 0 0 19848 72 0 0 25 0 1 0 1793810496 78602240 17654 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19190 17654 145 145 0 19045 0
[pid=26740] vsize: 76760
Current children cumulated CPU time (s) 199.2
Current children cumulated vsize (Kb) 78884

[startup+210.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 18476 0 0 0 20849 72 0 0 25 0 1 0 1793810496 78651392 17665 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19202 17665 145 145 0 19057 0
[pid=26740] vsize: 76808
Current children cumulated CPU time (s) 209.21
Current children cumulated vsize (Kb) 78932

[startup+220.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 18476 0 0 0 21849 72 0 0 25 0 1 0 1793810496 78651392 17665 4294967295 134512640 135094434 3221224432 3221223092 134553444 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19202 17665 145 145 0 19057 0
[pid=26740] vsize: 76808
Current children cumulated CPU time (s) 219.21
Current children cumulated vsize (Kb) 78932

[startup+230.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 18483 0 0 0 22849 72 0 0 25 0 1 0 1793810496 78667776 17672 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19206 17672 145 145 0 19061 0
[pid=26740] vsize: 76824
Current children cumulated CPU time (s) 229.21
Current children cumulated vsize (Kb) 78948

[startup+240.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 18554 0 0 0 23848 73 0 0 25 0 1 0 1793810496 78921728 17743 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19268 17743 145 145 0 19123 0
[pid=26740] vsize: 77072
Current children cumulated CPU time (s) 239.21
Current children cumulated vsize (Kb) 79196

[startup+250.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 18571 0 0 0 24848 73 0 0 25 0 1 0 1793810496 78987264 17760 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19284 17760 145 145 0 19139 0
[pid=26740] vsize: 77136
Current children cumulated CPU time (s) 249.21
Current children cumulated vsize (Kb) 79260

[startup+260.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 18584 0 0 0 25848 73 0 0 25 0 1 0 1793810496 79069184 17773 4294967295 134512640 135094434 3221224432 3221223092 134553489 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19304 17773 145 145 0 19159 0
[pid=26740] vsize: 77216
Current children cumulated CPU time (s) 259.21
Current children cumulated vsize (Kb) 79340

[startup+270.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 18603 0 0 0 26848 74 0 0 25 0 1 0 1793810496 79142912 17792 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19322 17792 145 145 0 19177 0
[pid=26740] vsize: 77288
Current children cumulated CPU time (s) 269.22
Current children cumulated vsize (Kb) 79412

[startup+280.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 18612 0 0 0 27848 74 0 0 25 0 1 0 1793810496 79155200 17801 4294967295 134512640 135094434 3221224432 3221223088 134561734 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19325 17801 145 145 0 19180 0
[pid=26740] vsize: 77300
Current children cumulated CPU time (s) 279.22
Current children cumulated vsize (Kb) 79424

[startup+290.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 18642 0 0 0 28847 74 0 0 25 0 1 0 1793810496 79273984 17831 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19354 17831 145 145 0 19209 0
[pid=26740] vsize: 77416
Current children cumulated CPU time (s) 289.21
Current children cumulated vsize (Kb) 79540

[startup+300.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 18766 0 0 0 29845 75 0 0 25 0 1 0 1793810496 79765504 17955 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19474 17955 145 145 0 19329 0
[pid=26740] vsize: 77896
Current children cumulated CPU time (s) 299.2
Current children cumulated vsize (Kb) 80020

[startup+310.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 18812 0 0 0 30845 75 0 0 25 0 1 0 1793810496 80015360 18001 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19535 18001 145 145 0 19390 0
[pid=26740] vsize: 78140
Current children cumulated CPU time (s) 309.2
Current children cumulated vsize (Kb) 80264

[startup+320.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 18821 0 0 0 31846 75 0 0 25 0 1 0 1793810496 80048128 18010 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19543 18010 145 145 0 19398 0
[pid=26740] vsize: 78172
Current children cumulated CPU time (s) 319.21
Current children cumulated vsize (Kb) 80296

[startup+330.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 18930 0 0 0 32844 76 0 0 25 0 1 0 1793810496 80490496 18119 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19651 18119 145 145 0 19506 0
[pid=26740] vsize: 78604
Current children cumulated CPU time (s) 329.2
Current children cumulated vsize (Kb) 80728

[startup+340.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 18937 0 0 0 33844 76 0 0 25 0 1 0 1793810496 80515072 18126 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19657 18126 145 145 0 19512 0
[pid=26740] vsize: 78628
Current children cumulated CPU time (s) 339.2
Current children cumulated vsize (Kb) 80752

[startup+350.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 18961 0 0 0 34844 76 0 0 25 0 1 0 1793810496 80609280 18150 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19680 18150 145 145 0 19535 0
[pid=26740] vsize: 78720
Current children cumulated CPU time (s) 349.2
Current children cumulated vsize (Kb) 80844

[startup+360.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 18978 0 0 0 35844 76 0 0 25 0 1 0 1793810496 80678912 18167 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19697 18167 145 145 0 19552 0
[pid=26740] vsize: 78788
Current children cumulated CPU time (s) 359.2
Current children cumulated vsize (Kb) 80912

[startup+370.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 18995 0 0 0 36844 76 0 0 25 0 1 0 1793810496 80748544 18184 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19714 18184 145 145 0 19569 0
[pid=26740] vsize: 78856
Current children cumulated CPU time (s) 369.2
Current children cumulated vsize (Kb) 80980

[startup+380.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 19007 0 0 0 37844 76 0 0 25 0 1 0 1793810496 80789504 18196 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19724 18196 145 145 0 19579 0
[pid=26740] vsize: 78896
Current children cumulated CPU time (s) 379.2
Current children cumulated vsize (Kb) 81020

[startup+390.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 19043 0 0 0 38844 76 0 0 25 0 1 0 1793810496 80928768 18232 4294967295 134512640 135094434 3221224432 3221223088 134561717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19758 18232 145 145 0 19613 0
[pid=26740] vsize: 79032
Current children cumulated CPU time (s) 389.2
Current children cumulated vsize (Kb) 81156

[startup+400.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 19063 0 0 0 39844 76 0 0 25 0 1 0 1793810496 81002496 18252 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19776 18252 145 145 0 19631 0
[pid=26740] vsize: 79104
Current children cumulated CPU time (s) 399.2
Current children cumulated vsize (Kb) 81228

[startup+410.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 19067 0 0 0 40844 76 0 0 25 0 1 0 1793810496 81018880 18256 4294967295 134512640 135094434 3221224432 3221223080 134558260 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19780 18256 145 145 0 19635 0
[pid=26740] vsize: 79120
Current children cumulated CPU time (s) 409.2
Current children cumulated vsize (Kb) 81244

[startup+420.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 19124 0 0 0 41843 77 0 0 25 0 1 0 1793810496 81248256 18313 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19836 18313 145 145 0 19691 0
[pid=26740] vsize: 79344
Current children cumulated CPU time (s) 419.2
Current children cumulated vsize (Kb) 81468

[startup+430.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 19135 0 0 0 42843 77 0 0 25 0 1 0 1793810496 81289216 18324 4294967295 134512640 135094434 3221224432 3221223072 134562085 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19846 18324 145 145 0 19701 0
[pid=26740] vsize: 79384
Current children cumulated CPU time (s) 429.2
Current children cumulated vsize (Kb) 81508

[startup+440.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 19152 0 0 0 43843 77 0 0 25 0 1 0 1793810496 81354752 18341 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19862 18341 145 145 0 19717 0
[pid=26740] vsize: 79448
Current children cumulated CPU time (s) 439.2
Current children cumulated vsize (Kb) 81572

[startup+450.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 19166 0 0 0 44843 77 0 0 25 0 1 0 1793810496 81412096 18355 4294967295 134512640 135094434 3221224432 3221223112 134553433 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19876 18355 145 145 0 19731 0
[pid=26740] vsize: 79504
Current children cumulated CPU time (s) 449.2
Current children cumulated vsize (Kb) 81628

[startup+460.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 19169 0 0 0 45843 77 0 0 25 0 1 0 1793810496 81424384 18358 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19879 18358 145 145 0 19734 0
[pid=26740] vsize: 79516
Current children cumulated CPU time (s) 459.2
Current children cumulated vsize (Kb) 81640

[startup+470.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 19212 0 0 0 46843 77 0 0 25 0 1 0 1793810496 81719296 18401 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19951 18401 145 145 0 19806 0
[pid=26740] vsize: 79804
Current children cumulated CPU time (s) 469.2
Current children cumulated vsize (Kb) 81928

[startup+480.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 19213 0 0 0 47843 77 0 0 25 0 1 0 1793810496 81719296 18402 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 19951 18402 145 145 0 19806 0
[pid=26740] vsize: 79804
Current children cumulated CPU time (s) 479.2
Current children cumulated vsize (Kb) 81928

[startup+490.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 19270 0 0 0 48842 78 0 0 25 0 1 0 1793810496 81940480 18459 4294967295 134512640 135094434 3221224432 3221223092 134553444 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 20005 18459 145 145 0 19860 0
[pid=26740] vsize: 80020
Current children cumulated CPU time (s) 489.2
Current children cumulated vsize (Kb) 82144

[startup+500.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 19312 0 0 0 49841 78 0 0 25 0 1 0 1793810496 82116608 18501 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 20048 18501 145 145 0 19903 0
[pid=26740] vsize: 80192
Current children cumulated CPU time (s) 499.19
Current children cumulated vsize (Kb) 82316

[startup+510.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 19321 0 0 0 50841 78 0 0 25 0 1 0 1793810496 82153472 18510 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 20057 18510 145 145 0 19912 0
[pid=26740] vsize: 80228
Current children cumulated CPU time (s) 509.19
Current children cumulated vsize (Kb) 82352

[startup+520.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 19370 0 0 0 51841 78 0 0 25 0 1 0 1793810496 82345984 18559 4294967295 134512640 135094434 3221224432 3221223136 134559005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 20104 18559 145 145 0 19959 0
[pid=26740] vsize: 80416
Current children cumulated CPU time (s) 519.19
Current children cumulated vsize (Kb) 82540

[startup+530.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 19400 0 0 0 52841 79 0 0 25 0 1 0 1793810496 82464768 18589 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 20133 18589 145 145 0 19988 0
[pid=26740] vsize: 80532
Current children cumulated CPU time (s) 529.2
Current children cumulated vsize (Kb) 82656

[startup+540.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 19426 0 0 0 53840 79 0 0 25 0 1 0 1793810496 82563072 18615 4294967295 134512640 135094434 3221224432 3221223044 134563059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 20157 18615 145 145 0 20012 0
[pid=26740] vsize: 80628
Current children cumulated CPU time (s) 539.19
Current children cumulated vsize (Kb) 82752

[startup+550.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 19461 0 0 0 54840 79 0 0 25 0 1 0 1793810496 82706432 18650 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 20192 18650 145 145 0 20047 0
[pid=26740] vsize: 80768
Current children cumulated CPU time (s) 549.19
Current children cumulated vsize (Kb) 82892

[startup+560.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 19485 0 0 0 55840 79 0 0 25 0 1 0 1793810496 82800640 18674 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 20215 18674 145 145 0 20070 0
[pid=26740] vsize: 80860
Current children cumulated CPU time (s) 559.19
Current children cumulated vsize (Kb) 82984

[startup+570.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 19602 0 0 0 56839 80 0 0 25 0 1 0 1793810496 83275776 18791 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 20331 18791 145 145 0 20186 0
[pid=26740] vsize: 81324
Current children cumulated CPU time (s) 569.19
Current children cumulated vsize (Kb) 83448

[startup+580.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 19622 0 0 0 57839 80 0 0 25 0 1 0 1793810496 83349504 18811 4294967295 134512640 135094434 3221224432 3221223136 134559017 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 20349 18811 145 145 0 20204 0
[pid=26740] vsize: 81396
Current children cumulated CPU time (s) 579.19
Current children cumulated vsize (Kb) 83520

[startup+590.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 19637 0 0 0 58839 80 0 0 25 0 1 0 1793810496 83410944 18826 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 20364 18826 145 145 0 20219 0
[pid=26740] vsize: 81456
Current children cumulated CPU time (s) 589.19
Current children cumulated vsize (Kb) 83580

[startup+600.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 19658 0 0 0 59839 80 0 0 25 0 1 0 1793810496 83492864 18847 4294967295 134512640 135094434 3221224432 3221223092 134553487 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 20384 18847 145 145 0 20239 0
[pid=26740] vsize: 81536
Current children cumulated CPU time (s) 599.19
Current children cumulated vsize (Kb) 83660

[startup+610.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 19711 0 0 0 60838 81 0 0 25 0 1 0 1793810496 83693568 18900 4294967295 134512640 135094434 3221224432 3221223092 134553454 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 20433 18900 145 145 0 20288 0
[pid=26740] vsize: 81732
Current children cumulated CPU time (s) 609.19
Current children cumulated vsize (Kb) 83856

[startup+620.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 19809 0 0 0 61836 82 0 0 25 0 1 0 1793810496 84086784 18998 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 20529 18998 145 145 0 20384 0
[pid=26740] vsize: 82116
Current children cumulated CPU time (s) 619.18
Current children cumulated vsize (Kb) 84240

[startup+630.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 20175 0 0 0 62830 84 0 0 25 0 1 0 1793810496 85549056 19364 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 20886 19364 145 145 0 20741 0
[pid=26740] vsize: 83544
Current children cumulated CPU time (s) 629.14
Current children cumulated vsize (Kb) 85668

[startup+640.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 20425 0 0 0 63826 86 0 0 25 0 1 0 1793810496 86831104 19614 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 21199 19614 145 145 0 21054 0
[pid=26740] vsize: 84796
Current children cumulated CPU time (s) 639.12
Current children cumulated vsize (Kb) 86920

[startup+650.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 20603 0 0 0 64823 87 0 0 25 0 1 0 1793810496 87642112 19792 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26740/statm): 21397 19792 145 145 0 21252 0
[pid=26740] vsize: 85588
Current children cumulated CPU time (s) 649.1
Current children cumulated vsize (Kb) 87712

[startup+660.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 20808 0 0 0 65820 88 0 0 25 0 1 0 1793810496 88457216 19997 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 21596 19997 145 145 0 21451 0
[pid=26740] vsize: 86384
Current children cumulated CPU time (s) 659.08
Current children cumulated vsize (Kb) 88508

[startup+670.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 20924 0 0 0 66817 90 0 0 25 0 1 0 1793810496 88924160 20113 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 21710 20113 145 145 0 21565 0
[pid=26740] vsize: 86840
Current children cumulated CPU time (s) 669.07
Current children cumulated vsize (Kb) 88964

[startup+680.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 21059 0 0 0 67815 91 0 0 25 0 1 0 1793810496 89513984 20248 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 21854 20248 145 145 0 21709 0
[pid=26740] vsize: 87416
Current children cumulated CPU time (s) 679.06
Current children cumulated vsize (Kb) 89540

[startup+690.058 s]
Raw data (loadavg): 1.07 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 21220 0 0 0 68812 92 0 0 25 0 1 0 1793810496 90185728 20409 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 22018 20409 145 145 0 21873 0
[pid=26740] vsize: 88072
Current children cumulated CPU time (s) 689.04
Current children cumulated vsize (Kb) 90196

[startup+700.06 s]
Raw data (loadavg): 1.06 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 21358 0 0 0 69810 93 0 0 25 0 1 0 1793810496 90746880 20547 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 22155 20547 145 145 0 22010 0
[pid=26740] vsize: 88620
Current children cumulated CPU time (s) 699.03
Current children cumulated vsize (Kb) 90744

[startup+710.061 s]
Raw data (loadavg): 1.05 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 21560 0 0 0 70806 95 0 0 25 0 1 0 1793810496 91541504 20749 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 22349 20749 145 145 0 22204 0
[pid=26740] vsize: 89396
Current children cumulated CPU time (s) 709.01
Current children cumulated vsize (Kb) 91520

[startup+720.062 s]
Raw data (loadavg): 1.04 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 21799 0 0 0 71802 96 0 0 25 0 1 0 1793810496 92520448 20988 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 22588 20988 145 145 0 22443 0
[pid=26740] vsize: 90352
Current children cumulated CPU time (s) 718.98
Current children cumulated vsize (Kb) 92476

[startup+730.062 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 22057 0 0 0 72798 97 0 0 25 0 1 0 1793810496 93573120 21246 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 22845 21246 145 145 0 22700 0
[pid=26740] vsize: 91380
Current children cumulated CPU time (s) 728.95
Current children cumulated vsize (Kb) 93504

[startup+740.062 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 22272 0 0 0 73795 99 0 0 25 0 1 0 1793810496 94412800 21461 4294967295 134512640 135094434 3221224432 3221223056 134557627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 23050 21461 145 145 0 22905 0
[pid=26740] vsize: 92200
Current children cumulated CPU time (s) 738.94
Current children cumulated vsize (Kb) 94324

[startup+750.063 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 22452 0 0 0 74792 100 0 0 25 0 1 0 1793810496 95191040 21641 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26740/statm): 23240 21641 145 145 0 23095 0
[pid=26740] vsize: 92960
Current children cumulated CPU time (s) 748.92
Current children cumulated vsize (Kb) 95084

[startup+760.064 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 22839 0 0 0 75785 103 0 0 25 0 1 0 1793810496 96768000 22028 4294967295 134512640 135094434 3221224432 3221223088 134558172 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 23625 22028 145 145 0 23480 0
[pid=26740] vsize: 94500
Current children cumulated CPU time (s) 758.88
Current children cumulated vsize (Kb) 96624

[startup+770.065 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 23039 0 0 0 76783 104 0 0 25 0 1 0 1793810496 97595392 22228 4294967295 134512640 135094434 3221224432 3221223104 134556239 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26740/statm): 23827 22228 145 145 0 23682 0
[pid=26740] vsize: 95308
Current children cumulated CPU time (s) 768.87
Current children cumulated vsize (Kb) 97432

[startup+780.065 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 23346 0 0 0 77778 105 0 0 25 0 1 0 1793810496 99356672 22535 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 24257 22535 145 145 0 24112 0
[pid=26740] vsize: 97028
Current children cumulated CPU time (s) 778.83
Current children cumulated vsize (Kb) 99152

[startup+790.066 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 23587 0 0 0 78775 106 0 0 25 0 1 0 1793810496 100364288 22776 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 24503 22776 145 145 0 24358 0
[pid=26740] vsize: 98012
Current children cumulated CPU time (s) 788.81
Current children cumulated vsize (Kb) 100136

[startup+800.067 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 23833 0 0 0 79771 108 0 0 25 0 1 0 1793810496 101388288 23022 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 24753 23022 145 145 0 24608 0
[pid=26740] vsize: 99012
Current children cumulated CPU time (s) 798.79
Current children cumulated vsize (Kb) 101136

[startup+810.068 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 24085 0 0 0 80767 110 0 0 25 0 1 0 1793810496 102412288 23274 4294967295 134512640 135094434 3221224432 3221223088 134558240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 25003 23274 145 145 0 24858 0
[pid=26740] vsize: 100012
Current children cumulated CPU time (s) 808.77
Current children cumulated vsize (Kb) 102136

[startup+820.068 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 24275 0 0 0 81764 111 0 0 25 0 1 0 1793810496 103141376 23464 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 25181 23464 145 145 0 25036 0
[pid=26740] vsize: 100724
Current children cumulated CPU time (s) 818.75
Current children cumulated vsize (Kb) 102848

[startup+830.069 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 24480 0 0 0 82761 113 0 0 25 0 1 0 1793810496 103972864 23669 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 25384 23669 145 145 0 25239 0
[pid=26740] vsize: 101536
Current children cumulated CPU time (s) 828.74
Current children cumulated vsize (Kb) 103660

[startup+840.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 24656 0 0 0 83758 114 0 0 25 0 1 0 1793810496 104677376 23845 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 25556 23845 145 145 0 25411 0
[pid=26740] vsize: 102224
Current children cumulated CPU time (s) 838.72
Current children cumulated vsize (Kb) 104348

[startup+850.071 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 24815 0 0 0 84757 115 0 0 25 0 1 0 1793810496 105349120 24004 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 25720 24004 145 145 0 25575 0
[pid=26740] vsize: 102880
Current children cumulated CPU time (s) 848.72
Current children cumulated vsize (Kb) 105004

[startup+860.072 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 24969 0 0 0 85754 116 0 0 25 0 1 0 1793810496 105979904 24158 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 25874 24158 145 145 0 25729 0
[pid=26740] vsize: 103496
Current children cumulated CPU time (s) 858.7
Current children cumulated vsize (Kb) 105620

[startup+870.073 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 25129 0 0 0 86752 117 0 0 25 0 1 0 1793810496 106586112 24318 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26740/statm): 26022 24318 145 145 0 25877 0
[pid=26740] vsize: 104088
Current children cumulated CPU time (s) 868.69
Current children cumulated vsize (Kb) 106212

[startup+880.074 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 25271 0 0 0 87749 118 0 0 25 0 1 0 1793810496 107241472 24460 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26740/statm): 26182 24460 145 145 0 26037 0
[pid=26740] vsize: 104728
Current children cumulated CPU time (s) 878.67
Current children cumulated vsize (Kb) 106852

[startup+890.075 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 25349 0 0 0 88748 118 0 0 25 0 1 0 1793810496 107540480 24538 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 26255 24538 145 145 0 26110 0
[pid=26740] vsize: 105020
Current children cumulated CPU time (s) 888.66
Current children cumulated vsize (Kb) 107144

[startup+900.076 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 25417 0 0 0 89747 119 0 0 25 0 1 0 1793810496 107786240 24606 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 26315 24606 145 145 0 26170 0
[pid=26740] vsize: 105260
Current children cumulated CPU time (s) 898.66
Current children cumulated vsize (Kb) 107384

[startup+910.077 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 25530 0 0 0 90745 120 0 0 25 0 1 0 1793810496 108314624 24719 4294967295 134512640 135094434 3221224432 3221223092 134553494 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 26444 24719 145 145 0 26299 0
[pid=26740] vsize: 105776
Current children cumulated CPU time (s) 908.65
Current children cumulated vsize (Kb) 107900

[startup+920.077 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 25618 0 0 0 91745 120 0 0 25 0 1 0 1793810496 108740608 24807 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 26548 24807 145 145 0 26403 0
[pid=26740] vsize: 106192
Current children cumulated CPU time (s) 918.65
Current children cumulated vsize (Kb) 108316

[startup+930.078 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 25764 0 0 0 92743 121 0 0 25 0 1 0 1793810496 109432832 24953 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 26717 24953 145 145 0 26572 0
[pid=26740] vsize: 106868
Current children cumulated CPU time (s) 928.64
Current children cumulated vsize (Kb) 108992

[startup+940.079 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 25888 0 0 0 93741 122 0 0 25 0 1 0 1793810496 109858816 25077 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 26821 25077 145 145 0 26676 0
[pid=26740] vsize: 107284
Current children cumulated CPU time (s) 938.63
Current children cumulated vsize (Kb) 109408

[startup+950.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 25948 0 0 0 94741 122 0 0 25 0 1 0 1793810496 110129152 25137 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 26887 25137 145 145 0 26742 0
[pid=26740] vsize: 107548
Current children cumulated CPU time (s) 948.63
Current children cumulated vsize (Kb) 109672

[startup+960.081 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 26023 0 0 0 95740 123 0 0 25 0 1 0 1793810496 110436352 25212 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 26962 25212 145 145 0 26817 0
[pid=26740] vsize: 107848
Current children cumulated CPU time (s) 958.63
Current children cumulated vsize (Kb) 109972

[startup+970.082 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 26104 0 0 0 96738 124 0 0 25 0 1 0 1793810496 110751744 25293 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 27039 25293 145 145 0 26894 0
[pid=26740] vsize: 108156
Current children cumulated CPU time (s) 968.62
Current children cumulated vsize (Kb) 110280

[startup+980.083 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 26183 0 0 0 97738 124 0 0 25 0 1 0 1793810496 111058944 25372 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 27114 25372 145 145 0 26969 0
[pid=26740] vsize: 108456
Current children cumulated CPU time (s) 978.62
Current children cumulated vsize (Kb) 110580

[startup+990.083 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 26283 0 0 0 98737 125 0 0 25 0 1 0 1793810496 111480832 25472 4294967295 134512640 135094434 3221224432 3221223088 134558232 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 27217 25472 145 145 0 27072 0
[pid=26740] vsize: 108868
Current children cumulated CPU time (s) 988.62
Current children cumulated vsize (Kb) 110992

[startup+1000.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 26376 0 0 0 99736 125 0 0 25 0 1 0 1793810496 111837184 25565 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 27304 25565 145 145 0 27159 0
[pid=26740] vsize: 109216
Current children cumulated CPU time (s) 998.61
Current children cumulated vsize (Kb) 111340

[startup+1010.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 26515 0 0 0 100734 125 0 0 25 0 1 0 1793810496 112369664 25704 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 27434 25704 145 145 0 27289 0
[pid=26740] vsize: 109736
Current children cumulated CPU time (s) 1008.59
Current children cumulated vsize (Kb) 111860

[startup+1020.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 26576 0 0 0 101733 126 0 0 25 0 1 0 1793810496 112664576 25765 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 27506 25765 145 145 0 27361 0
[pid=26740] vsize: 110024
Current children cumulated CPU time (s) 1018.59
Current children cumulated vsize (Kb) 112148

[startup+1030.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 26635 0 0 0 102733 126 0 0 25 0 1 0 1793810496 112885760 25824 4294967295 134512640 135094434 3221224432 3221223088 134557917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 27560 25824 145 145 0 27415 0
[pid=26740] vsize: 110240
Current children cumulated CPU time (s) 1028.59
Current children cumulated vsize (Kb) 112364

[startup+1040.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 26705 0 0 0 103732 127 0 0 25 0 1 0 1793810496 113180672 25894 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 27632 25894 145 145 0 27487 0
[pid=26740] vsize: 110528
Current children cumulated CPU time (s) 1038.59
Current children cumulated vsize (Kb) 112652

[startup+1050.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 26796 0 0 0 104731 127 0 0 25 0 1 0 1793810496 113569792 25985 4294967295 134512640 135094434 3221224432 3221223056 134557691 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 27727 25985 145 145 0 27582 0
[pid=26740] vsize: 110908
Current children cumulated CPU time (s) 1048.58
Current children cumulated vsize (Kb) 113032

[startup+1060.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 26893 0 0 0 105729 128 0 0 25 0 1 0 1793810496 113950720 26082 4294967295 134512640 135094434 3221224432 3221223024 134556928 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 27820 26082 145 145 0 27675 0
[pid=26740] vsize: 111280
Current children cumulated CPU time (s) 1058.57
Current children cumulated vsize (Kb) 113404

[startup+1070.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 26978 0 0 0 106728 128 0 0 25 0 1 0 1793810496 114294784 26167 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 27904 26167 145 145 0 27759 0
[pid=26740] vsize: 111616
Current children cumulated CPU time (s) 1068.56
Current children cumulated vsize (Kb) 113740

[startup+1080.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 27062 0 0 0 107727 129 0 0 25 0 1 0 1793810496 114630656 26251 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 27986 26251 145 145 0 27841 0
[pid=26740] vsize: 111944
Current children cumulated CPU time (s) 1078.56
Current children cumulated vsize (Kb) 114068

[startup+1090.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 27159 0 0 0 108726 129 0 0 25 0 1 0 1793810496 115027968 26348 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 28083 26348 145 145 0 27938 0
[pid=26740] vsize: 112332
Current children cumulated CPU time (s) 1088.55
Current children cumulated vsize (Kb) 114456

[startup+1100.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 27241 0 0 0 109725 130 0 0 25 0 1 0 1793810496 115351552 26430 4294967295 134512640 135094434 3221224432 3221223088 134558147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 28162 26430 145 145 0 28017 0
[pid=26740] vsize: 112648
Current children cumulated CPU time (s) 1098.55
Current children cumulated vsize (Kb) 114772

[startup+1110.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 27319 0 0 0 110724 131 0 0 25 0 1 0 1793810496 115646464 26508 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 28234 26508 145 145 0 28089 0
[pid=26740] vsize: 112936
Current children cumulated CPU time (s) 1108.55
Current children cumulated vsize (Kb) 115060

[startup+1120.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 27413 0 0 0 111724 131 0 0 25 0 1 0 1793810496 116035584 26602 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 28329 26602 145 145 0 28184 0
[pid=26740] vsize: 113316
Current children cumulated CPU time (s) 1118.55
Current children cumulated vsize (Kb) 115440

[startup+1130.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 27488 0 0 0 112723 131 0 0 25 0 1 0 1793810496 116326400 26677 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 28400 26677 145 145 0 28255 0
[pid=26740] vsize: 113600
Current children cumulated CPU time (s) 1128.54
Current children cumulated vsize (Kb) 115724

[startup+1140.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 27559 0 0 0 113723 132 0 0 25 0 1 0 1793810496 116715520 26748 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 28495 26748 145 145 0 28350 0
[pid=26740] vsize: 113980
Current children cumulated CPU time (s) 1138.55
Current children cumulated vsize (Kb) 116104

[startup+1150.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 27628 0 0 0 114721 132 0 0 25 0 1 0 1793810496 116973568 26817 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 28558 26817 145 145 0 28413 0
[pid=26740] vsize: 114232
Current children cumulated CPU time (s) 1148.53
Current children cumulated vsize (Kb) 116356

[startup+1160.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 27717 0 0 0 115720 133 0 0 25 0 1 0 1793810496 117350400 26906 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 28650 26906 145 145 0 28505 0
[pid=26740] vsize: 114600
Current children cumulated CPU time (s) 1158.53
Current children cumulated vsize (Kb) 116724

[startup+1170.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 27791 0 0 0 116719 133 0 0 25 0 1 0 1793810496 117641216 26980 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 28721 26980 145 145 0 28576 0
[pid=26740] vsize: 114884
Current children cumulated CPU time (s) 1168.52
Current children cumulated vsize (Kb) 117008

[startup+1180.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 27845 0 0 0 117719 133 0 0 25 0 1 0 1793810496 117846016 27034 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 28771 27034 145 145 0 28626 0
[pid=26740] vsize: 115084
Current children cumulated CPU time (s) 1178.52
Current children cumulated vsize (Kb) 117208

[startup+1190.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 27897 0 0 0 118719 134 0 0 25 0 1 0 1793810496 118165504 27086 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 28849 27086 145 145 0 28704 0
[pid=26740] vsize: 115396
Current children cumulated CPU time (s) 1188.53
Current children cumulated vsize (Kb) 117520

[startup+1200.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 28004 0 0 0 119718 134 0 0 25 0 1 0 1793810496 118661120 27193 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 28970 27193 145 145 0 28825 0
[pid=26740] vsize: 115880
Current children cumulated CPU time (s) 1198.52
Current children cumulated vsize (Kb) 118004

[startup+1210.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 28070 0 0 0 120718 135 0 0 25 0 1 0 1793810496 118964224 27259 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 29044 27259 145 145 0 28899 0
[pid=26740] vsize: 116176
Current children cumulated CPU time (s) 1208.53
Current children cumulated vsize (Kb) 118300



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 26740
Raw data (/proc/26736/stat): 26736 (minisat+_script) S 26735 26736 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793810491 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26736/statm): 531 226 485 147 0 384 0
[pid=26736] vsize: 2124
Raw data (/proc/26740/stat): 26740 (minisat+_64-bit) R 26736 26736 9854 0 -1 0 28070 0 0 0 120718 135 0 0 25 0 1 0 1793810496 118964224 27259 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26740/statm): 29044 27259 145 145 0 28899 0
[pid=26740] vsize: 116176
Current children cumulated CPU time (s) 1208.53
Current children cumulated vsize (Kb) 118300

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

Child status: 0
Real time (s): 1210.16
CPU time (s): 1208.59
CPU user time (s): 1207.19
CPU system time (s): 1.40279
CPU usage (%): 99.8701
Max. virtual memory (cumulated for all children) (Kb): 118300