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/26553/stat): 26553 (minisat+_script) R 26552 26553 21452 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1842336833 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/26553/statm): 174 3 169 147 0 27 0
[pid=26553] 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=26554
New process pid=26555
New process pid=26556
execve syscall for /bin/sed executable
One traced child (pid=26555) 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=26556) exited with status: 0
One traced child (pid=26554) exited with status: 0
New process pid=26557
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc22/normalized-ii8d2.opb

[startup+10.0037 s]
Raw data (loadavg): 0.93 0.95 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 7002 0 0 0 941 30 0 0 25 0 1 0 1842336838 31174656 6687 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26557/statm): 7611 6687 145 145 0 7466 0
[pid=26557] vsize: 30444
Current children cumulated CPU time (s) 9.72
Current children cumulated vsize (Kb) 32568

[startup+20.0054 s]
Raw data (loadavg): 0.94 0.95 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 7123 0 0 0 1939 31 0 0 25 0 1 0 1842336838 31682560 6808 4294967295 134512640 135094434 3221224448 3221223060 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26557/statm): 7735 6808 145 145 0 7590 0
[pid=26557] vsize: 30940
Current children cumulated CPU time (s) 19.71
Current children cumulated vsize (Kb) 33064

[startup+30.0061 s]
Raw data (loadavg): 0.95 0.95 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 7398 0 0 0 2937 32 0 0 25 0 1 0 1842336838 33226752 7083 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26557/statm): 8112 7083 145 145 0 7967 0
[pid=26557] vsize: 32448
Current children cumulated CPU time (s) 29.7
Current children cumulated vsize (Kb) 34572

[startup+40.0068 s]
Raw data (loadavg): 0.95 0.95 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 7477 0 0 0 3935 33 0 0 25 0 1 0 1842336838 33570816 7162 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26557/statm): 8196 7162 145 145 0 8051 0
[pid=26557] vsize: 32784
Current children cumulated CPU time (s) 39.69
Current children cumulated vsize (Kb) 34908

[startup+50.0085 s]
Raw data (loadavg): 0.96 0.95 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 7599 0 0 0 4934 34 0 0 25 0 1 0 1842336838 34033664 7284 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 8309 7284 145 145 0 8164 0
[pid=26557] vsize: 33236
Current children cumulated CPU time (s) 49.69
Current children cumulated vsize (Kb) 35360

[startup+60.0082 s]
Raw data (loadavg): 0.97 0.95 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 7721 0 0 0 5932 35 0 0 25 0 1 0 1842336838 34533376 7406 4294967295 134512640 135094434 3221224448 3221223040 134557404 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 8431 7406 145 145 0 8286 0
[pid=26557] vsize: 33724
Current children cumulated CPU time (s) 59.68
Current children cumulated vsize (Kb) 35848

[startup+70.0089 s]
Raw data (loadavg): 0.97 0.95 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 7908 0 0 0 6928 37 0 0 25 0 1 0 1842336838 35295232 7593 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 8617 7593 145 145 0 8472 0
[pid=26557] vsize: 34468
Current children cumulated CPU time (s) 69.66
Current children cumulated vsize (Kb) 36592

[startup+80.0096 s]
Raw data (loadavg): 0.98 0.95 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 8029 0 0 0 7925 38 0 0 25 0 1 0 1842336838 35782656 7714 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 8736 7714 145 145 0 8591 0
[pid=26557] vsize: 34944
Current children cumulated CPU time (s) 79.64
Current children cumulated vsize (Kb) 37068

[startup+90.0103 s]
Raw data (loadavg): 0.98 0.95 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 8136 0 0 0 8924 39 0 0 25 0 1 0 1842336838 36282368 7821 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 8858 7821 145 145 0 8713 0
[pid=26557] vsize: 35432
Current children cumulated CPU time (s) 89.64
Current children cumulated vsize (Kb) 37556

[startup+100.011 s]
Raw data (loadavg): 0.98 0.95 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 8287 0 0 0 9922 40 0 0 25 0 1 0 1842336838 36892672 7972 4294967295 134512640 135094434 3221224448 3221223040 134556809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 9007 7972 145 145 0 8862 0
[pid=26557] vsize: 36028
Current children cumulated CPU time (s) 99.63
Current children cumulated vsize (Kb) 38152

[startup+110.012 s]
Raw data (loadavg): 0.98 0.95 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 8452 0 0 0 10919 41 0 0 25 0 1 0 1842336838 37560320 8137 4294967295 134512640 135094434 3221224448 3221223072 134562108 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 9170 8137 145 145 0 9025 0
[pid=26557] vsize: 36680
Current children cumulated CPU time (s) 109.61
Current children cumulated vsize (Kb) 38804

[startup+120.012 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 8632 0 0 0 11916 43 0 0 25 0 1 0 1842336838 38285312 8317 4294967295 134512640 135094434 3221224448 3221223120 134555323 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 9347 8317 145 145 0 9202 0
[pid=26557] vsize: 37388
Current children cumulated CPU time (s) 119.6
Current children cumulated vsize (Kb) 39512

[startup+130.013 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 8792 0 0 0 12913 44 0 0 25 0 1 0 1842336838 38932480 8477 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 9505 8477 145 145 0 9360 0
[pid=26557] vsize: 38020
Current children cumulated CPU time (s) 129.58
Current children cumulated vsize (Kb) 40144

[startup+140.014 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 9049 0 0 0 13908 47 0 0 25 0 1 0 1842336838 39981056 8734 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 9761 8734 145 145 0 9616 0
[pid=26557] vsize: 39044
Current children cumulated CPU time (s) 139.56
Current children cumulated vsize (Kb) 41168

[startup+150.015 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 9297 0 0 0 14904 49 0 0 25 0 1 0 1842336838 40988672 8982 4294967295 134512640 135094434 3221224448 3221223040 134557037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 10007 8982 145 145 0 9862 0
[pid=26557] vsize: 40028
Current children cumulated CPU time (s) 149.54
Current children cumulated vsize (Kb) 42152

[startup+160.014 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 9551 0 0 0 15900 51 0 0 25 0 1 0 1842336838 42024960 9236 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 10260 9236 145 145 0 10115 0
[pid=26557] vsize: 41040
Current children cumulated CPU time (s) 159.52
Current children cumulated vsize (Kb) 43164

[startup+170.015 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 9699 0 0 0 16897 52 0 0 25 0 1 0 1842336838 42627072 9384 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 10407 9384 145 145 0 10262 0
[pid=26557] vsize: 41628
Current children cumulated CPU time (s) 169.5
Current children cumulated vsize (Kb) 43752

[startup+180.016 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 9983 0 0 0 17893 53 0 0 25 0 1 0 1842336838 43786240 9668 4294967295 134512640 135094434 3221224448 3221223040 134556812 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 10690 9668 145 145 0 10545 0
[pid=26557] vsize: 42760
Current children cumulated CPU time (s) 179.47
Current children cumulated vsize (Kb) 44884

[startup+190.016 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 10114 0 0 0 18891 54 0 0 25 0 1 0 1842336838 44314624 9799 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 10819 9799 145 145 0 10674 0
[pid=26557] vsize: 43276
Current children cumulated CPU time (s) 189.46
Current children cumulated vsize (Kb) 45400

[startup+200.017 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 10238 0 0 0 19890 55 0 0 25 0 1 0 1842336838 44998656 9923 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 10986 9923 145 145 0 10841 0
[pid=26557] vsize: 43944
Current children cumulated CPU time (s) 199.46
Current children cumulated vsize (Kb) 46068

[startup+210.017 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 10452 0 0 0 20887 56 0 0 25 0 1 0 1842336838 45862912 10137 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 11197 10137 145 145 0 11052 0
[pid=26557] vsize: 44788
Current children cumulated CPU time (s) 209.44
Current children cumulated vsize (Kb) 46912

[startup+220.018 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 10630 0 0 0 21884 57 0 0 25 0 1 0 1842336838 46583808 10315 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 11373 10315 145 145 0 11228 0
[pid=26557] vsize: 45492
Current children cumulated CPU time (s) 219.42
Current children cumulated vsize (Kb) 47616

[startup+230.018 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 10738 0 0 0 22883 58 0 0 25 0 1 0 1842336838 47022080 10423 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 11480 10423 145 145 0 11335 0
[pid=26557] vsize: 45920
Current children cumulated CPU time (s) 229.42
Current children cumulated vsize (Kb) 48044

[startup+240.019 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 11004 0 0 0 23879 60 0 0 25 0 1 0 1842336838 48103424 10689 4294967295 134512640 135094434 3221224448 3221223040 134556817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 11744 10689 145 145 0 11599 0
[pid=26557] vsize: 46976
Current children cumulated CPU time (s) 239.4
Current children cumulated vsize (Kb) 49100

[startup+250.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 11366 0 0 0 24873 62 0 0 25 0 1 0 1842336838 49582080 11051 4294967295 134512640 135094434 3221224448 3221223100 134556676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 12105 11051 145 145 0 11960 0
[pid=26557] vsize: 48420
Current children cumulated CPU time (s) 249.36
Current children cumulated vsize (Kb) 50544

[startup+260.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 11714 0 0 0 25869 65 0 0 25 0 1 0 1842336838 51003392 11399 4294967295 134512640 135094434 3221224448 3221223080 134557561 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 12452 11399 145 145 0 12307 0
[pid=26557] vsize: 49808
Current children cumulated CPU time (s) 259.35
Current children cumulated vsize (Kb) 51932

[startup+270.021 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 12179 0 0 0 26861 68 0 0 25 0 1 0 1842336838 52903936 11864 4294967295 134512640 135094434 3221224448 3221223104 134557813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 12916 11864 145 145 0 12771 0
[pid=26557] vsize: 51664
Current children cumulated CPU time (s) 269.3
Current children cumulated vsize (Kb) 53788

[startup+280.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 12577 0 0 0 27856 70 0 0 25 0 1 0 1842336838 54530048 12262 4294967295 134512640 135094434 3221224448 3221223040 134557512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 13313 12262 145 145 0 13168 0
[pid=26557] vsize: 53252
Current children cumulated CPU time (s) 279.27
Current children cumulated vsize (Kb) 55376

[startup+290.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 12997 0 0 0 28851 72 0 0 25 0 1 0 1842336838 56246272 12682 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 13732 12682 145 145 0 13587 0
[pid=26557] vsize: 54928
Current children cumulated CPU time (s) 289.24
Current children cumulated vsize (Kb) 57052

[startup+300.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 13385 0 0 0 29846 75 0 0 25 0 1 0 1842336838 57831424 13070 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 14119 13070 145 145 0 13974 0
[pid=26557] vsize: 56476
Current children cumulated CPU time (s) 299.22
Current children cumulated vsize (Kb) 58600

[startup+310.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 13627 0 0 0 30842 76 0 0 25 0 1 0 1842336838 58818560 13312 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 14360 13312 145 145 0 14215 0
[pid=26557] vsize: 57440
Current children cumulated CPU time (s) 309.19
Current children cumulated vsize (Kb) 59564

[startup+320.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 13886 0 0 0 31837 79 0 0 25 0 1 0 1842336838 59875328 13571 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26557/statm): 14618 13571 145 145 0 14473 0
[pid=26557] vsize: 58472
Current children cumulated CPU time (s) 319.17
Current children cumulated vsize (Kb) 60596

[startup+330.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 14136 0 0 0 32834 80 0 0 25 0 1 0 1842336838 60891136 13821 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26557/statm): 14866 13821 145 145 0 14721 0
[pid=26557] vsize: 59464
Current children cumulated CPU time (s) 329.15
Current children cumulated vsize (Kb) 61588

[startup+340.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 14267 0 0 0 33831 82 0 0 25 0 1 0 1842336838 61423616 13952 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26557/statm): 14996 13952 145 145 0 14851 0
[pid=26557] vsize: 59984
Current children cumulated CPU time (s) 339.14
Current children cumulated vsize (Kb) 62108

[startup+350.029 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 14363 0 0 0 34829 83 0 0 25 0 1 0 1842336838 61808640 14048 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26557/statm): 15090 14048 145 145 0 14945 0
[pid=26557] vsize: 60360
Current children cumulated CPU time (s) 349.13
Current children cumulated vsize (Kb) 62484

[startup+360.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 14496 0 0 0 35826 85 0 0 25 0 1 0 1842336838 62349312 14181 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26557/statm): 15222 14181 145 145 0 15077 0
[pid=26557] vsize: 60888
Current children cumulated CPU time (s) 359.12
Current children cumulated vsize (Kb) 63012

[startup+370.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 14605 0 0 0 36824 86 0 0 25 0 1 0 1842336838 62787584 14290 4294967295 134512640 135094434 3221224448 3221223072 134562149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26557/statm): 15329 14290 145 145 0 15184 0
[pid=26557] vsize: 61316
Current children cumulated CPU time (s) 369.11
Current children cumulated vsize (Kb) 63440

[startup+380.031 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 14799 0 0 0 37820 88 0 0 25 0 1 0 1842336838 63578112 14484 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26557/statm): 15522 14484 145 145 0 15377 0
[pid=26557] vsize: 62088
Current children cumulated CPU time (s) 379.09
Current children cumulated vsize (Kb) 64212

[startup+390.033 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 15003 0 0 0 38818 89 0 0 25 0 1 0 1842336838 64409600 14688 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26557/statm): 15725 14688 145 145 0 15580 0
[pid=26557] vsize: 62900
Current children cumulated CPU time (s) 389.08
Current children cumulated vsize (Kb) 65024

[startup+400.033 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 15175 0 0 0 39815 90 0 0 25 0 1 0 1842336838 65105920 14860 4294967295 134512640 135094434 3221224448 3221223040 134557423 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26557/statm): 15895 14860 145 145 0 15750 0
[pid=26557] vsize: 63580
Current children cumulated CPU time (s) 399.06
Current children cumulated vsize (Kb) 65704

[startup+410.034 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 15322 0 0 0 40813 91 0 0 25 0 1 0 1842336838 65703936 15007 4294967295 134512640 135094434 3221224448 3221223088 134558048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26557/statm): 16041 15007 145 145 0 15896 0
[pid=26557] vsize: 64164
Current children cumulated CPU time (s) 409.05
Current children cumulated vsize (Kb) 66288

[startup+420.036 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 15428 0 0 0 41811 92 0 0 25 0 1 0 1842336838 66129920 15113 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26557/statm): 16145 15113 145 145 0 16000 0
[pid=26557] vsize: 64580
Current children cumulated CPU time (s) 419.04
Current children cumulated vsize (Kb) 66704

[startup+430.038 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 15545 0 0 0 42809 94 0 0 25 0 1 0 1842336838 66863104 15230 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26557/statm): 16324 15230 145 145 0 16179 0
[pid=26557] vsize: 65296
Current children cumulated CPU time (s) 429.04
Current children cumulated vsize (Kb) 67420

[startup+440.039 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 15668 0 0 0 43807 95 0 0 25 0 1 0 1842336838 67362816 15353 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26557/statm): 16446 15353 145 145 0 16301 0
[pid=26557] vsize: 65784
Current children cumulated CPU time (s) 439.03
Current children cumulated vsize (Kb) 67908

[startup+450.04 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 15842 0 0 0 44804 97 0 0 25 0 1 0 1842336838 68075520 15527 4294967295 134512640 135094434 3221224448 3221223072 134557577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26557/statm): 16620 15527 145 145 0 16475 0
[pid=26557] vsize: 66480
Current children cumulated CPU time (s) 449.02
Current children cumulated vsize (Kb) 68604

[startup+460.041 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 15983 0 0 0 45801 98 0 0 25 0 1 0 1842336838 68644864 15668 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26557/statm): 16759 15668 145 145 0 16614 0
[pid=26557] vsize: 67036
Current children cumulated CPU time (s) 459
Current children cumulated vsize (Kb) 69160

[startup+470.042 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 16172 0 0 0 46797 100 0 0 25 0 1 0 1842336838 69414912 15857 4294967295 134512640 135094434 3221224448 3221223136 134554685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26557/statm): 16947 15857 145 145 0 16802 0
[pid=26557] vsize: 67788
Current children cumulated CPU time (s) 468.98
Current children cumulated vsize (Kb) 69912

[startup+480.043 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 16371 0 0 0 47794 102 0 0 25 0 1 0 1842336838 70225920 16056 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26557/statm): 17145 16056 145 145 0 17000 0
[pid=26557] vsize: 68580
Current children cumulated CPU time (s) 478.97
Current children cumulated vsize (Kb) 70704

[startup+490.045 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 16486 0 0 0 48792 103 0 0 25 0 1 0 1842336838 70692864 16171 4294967295 134512640 135094434 3221224448 3221223108 134553499 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 17259 16171 145 145 0 17114 0
[pid=26557] vsize: 69036
Current children cumulated CPU time (s) 488.96
Current children cumulated vsize (Kb) 71160

[startup+500.045 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 16683 0 0 0 49789 105 0 0 25 0 1 0 1842336838 71495680 16368 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 17455 16368 145 145 0 17310 0
[pid=26557] vsize: 69820
Current children cumulated CPU time (s) 498.95
Current children cumulated vsize (Kb) 71944

[startup+510.046 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 16899 0 0 0 50786 106 0 0 25 0 1 0 1842336838 72376320 16584 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 17670 16584 145 145 0 17525 0
[pid=26557] vsize: 70680
Current children cumulated CPU time (s) 508.93
Current children cumulated vsize (Kb) 72804

[startup+520.047 s]
Raw data (loadavg): 0.99 0.97 0.95 1/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) T 26553 26553 21452 0 -1 0 17088 0 0 0 51783 107 0 0 25 0 1 0 1842336838 73142272 16773 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/26557/statm): 17857 16773 145 145 0 17712 0
[pid=26557] vsize: 71428
Current children cumulated CPU time (s) 518.91
Current children cumulated vsize (Kb) 73552

[startup+530.048 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 17281 0 0 0 52781 108 0 0 25 0 1 0 1842336838 73928704 16966 4294967295 134512640 135094434 3221224448 3221223040 134556847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 18049 16966 145 145 0 17904 0
[pid=26557] vsize: 72196
Current children cumulated CPU time (s) 528.9
Current children cumulated vsize (Kb) 74320

[startup+540.049 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 17458 0 0 0 53778 109 0 0 25 0 1 0 1842336838 74649600 17143 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 18225 17143 145 145 0 18080 0
[pid=26557] vsize: 72900
Current children cumulated CPU time (s) 538.88
Current children cumulated vsize (Kb) 75024

[startup+550.05 s]
Raw data (loadavg): 0.99 0.97 0.95 1/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) T 26553 26553 21452 0 -1 0 17609 0 0 0 54775 110 0 0 25 0 1 0 1842336838 75264000 17294 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/26557/statm): 18375 17294 145 145 0 18230 0
[pid=26557] vsize: 73500
Current children cumulated CPU time (s) 548.86
Current children cumulated vsize (Kb) 75624

[startup+560.051 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 17718 0 0 0 55773 111 0 0 25 0 1 0 1842336838 75702272 17403 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 18482 17403 145 145 0 18337 0
[pid=26557] vsize: 73928
Current children cumulated CPU time (s) 558.85
Current children cumulated vsize (Kb) 76052

[startup+570.051 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 17875 0 0 0 56771 111 0 0 25 0 1 0 1842336838 76341248 17560 4294967295 134512640 135094434 3221224448 3221223072 134557658 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 18638 17560 145 145 0 18493 0
[pid=26557] vsize: 74552
Current children cumulated CPU time (s) 568.83
Current children cumulated vsize (Kb) 76676

[startup+580.052 s]
Raw data (loadavg): 0.99 0.97 0.95 1/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) T 26553 26553 21452 0 -1 0 18032 0 0 0 57769 112 0 0 25 0 1 0 1842336838 76980224 17717 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/26557/statm): 18794 17717 145 145 0 18649 0
[pid=26557] vsize: 75176
Current children cumulated CPU time (s) 578.82
Current children cumulated vsize (Kb) 77300

[startup+590.054 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 18282 0 0 0 58765 115 0 0 25 0 1 0 1842336838 78000128 17967 4294967295 134512640 135094434 3221224448 3221223104 134558176 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 19043 17967 145 145 0 18898 0
[pid=26557] vsize: 76172
Current children cumulated CPU time (s) 588.81
Current children cumulated vsize (Kb) 78296

[startup+600.054 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 18546 0 0 0 59762 116 0 0 25 0 1 0 1842336838 79077376 18231 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 19306 18231 145 145 0 19161 0
[pid=26557] vsize: 77224
Current children cumulated CPU time (s) 598.79
Current children cumulated vsize (Kb) 79348

[startup+610.054 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 18775 0 0 0 60758 118 0 0 25 0 1 0 1842336838 80011264 18460 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 19534 18460 145 145 0 19389 0
[pid=26557] vsize: 78136
Current children cumulated CPU time (s) 608.77
Current children cumulated vsize (Kb) 80260

[startup+620.055 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 19007 0 0 0 61755 119 0 0 25 0 1 0 1842336838 80957440 18692 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 19765 18692 145 145 0 19620 0
[pid=26557] vsize: 79060
Current children cumulated CPU time (s) 618.75
Current children cumulated vsize (Kb) 81184

[startup+630.056 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 19245 0 0 0 62752 121 0 0 25 0 1 0 1842336838 81928192 18930 4294967295 134512640 135094434 3221224448 3221223072 134557655 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26557/statm): 20002 18930 145 145 0 19857 0
[pid=26557] vsize: 80008
Current children cumulated CPU time (s) 628.74
Current children cumulated vsize (Kb) 82132

[startup+640.056 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 19456 0 0 0 63748 123 0 0 25 0 1 0 1842336838 82788352 19141 4294967295 134512640 135094434 3221224448 3221223120 134555274 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26557/statm): 20212 19141 145 145 0 20067 0
[pid=26557] vsize: 80848
Current children cumulated CPU time (s) 638.72
Current children cumulated vsize (Kb) 82972

[startup+650.058 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 19612 0 0 0 64745 125 0 0 25 0 1 0 1842336838 83423232 19297 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26557/statm): 20367 19297 145 145 0 20222 0
[pid=26557] vsize: 81468
Current children cumulated CPU time (s) 648.71
Current children cumulated vsize (Kb) 83592

[startup+660.059 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 19797 0 0 0 65743 126 0 0 25 0 1 0 1842336838 84176896 19482 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26557/statm): 20551 19482 145 145 0 20406 0
[pid=26557] vsize: 82204
Current children cumulated CPU time (s) 658.7
Current children cumulated vsize (Kb) 84328

[startup+670.061 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 19924 0 0 0 66740 128 0 0 25 0 1 0 1842336838 84692992 19609 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26557/statm): 20677 19609 145 145 0 20532 0
[pid=26557] vsize: 82708
Current children cumulated CPU time (s) 668.69
Current children cumulated vsize (Kb) 84832

[startup+680.061 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 20002 0 0 0 67738 129 0 0 25 0 1 0 1842336838 85008384 19687 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26557/statm): 20754 19687 145 145 0 20609 0
[pid=26557] vsize: 83016
Current children cumulated CPU time (s) 678.68
Current children cumulated vsize (Kb) 85140

[startup+690.063 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 20270 0 0 0 68733 131 0 0 25 0 1 0 1842336838 86102016 19955 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26557/statm): 21021 19955 145 145 0 20876 0
[pid=26557] vsize: 84084
Current children cumulated CPU time (s) 688.65
Current children cumulated vsize (Kb) 86208

[startup+700.064 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 20392 0 0 0 69730 132 0 0 25 0 1 0 1842336838 86597632 20077 4294967295 134512640 135094434 3221224448 3221223104 134557813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26557/statm): 21142 20077 145 145 0 20997 0
[pid=26557] vsize: 84568
Current children cumulated CPU time (s) 698.63
Current children cumulated vsize (Kb) 86692

[startup+710.064 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 20489 0 0 0 70728 134 0 0 25 0 1 0 1842336838 86990848 20174 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26557/statm): 21238 20174 145 145 0 21093 0
[pid=26557] vsize: 84952
Current children cumulated CPU time (s) 708.63
Current children cumulated vsize (Kb) 87076

[startup+720.066 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 20604 0 0 0 71726 135 0 0 25 0 1 0 1842336838 87457792 20289 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26557/statm): 21352 20289 145 145 0 21207 0
[pid=26557] vsize: 85408
Current children cumulated CPU time (s) 718.62
Current children cumulated vsize (Kb) 87532

[startup+730.067 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 20751 0 0 0 72722 137 0 0 25 0 1 0 1842336838 88051712 20436 4294967295 134512640 135094434 3221224448 3221223104 134558392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26557/statm): 21497 20436 145 145 0 21352 0
[pid=26557] vsize: 85988
Current children cumulated CPU time (s) 728.6
Current children cumulated vsize (Kb) 88112

[startup+740.068 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 20856 0 0 0 73719 138 0 0 25 0 1 0 1842336838 88477696 20541 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26557/statm): 21601 20541 145 145 0 21456 0
[pid=26557] vsize: 86404
Current children cumulated CPU time (s) 738.58
Current children cumulated vsize (Kb) 88528

[startup+750.07 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 20966 0 0 0 74717 139 0 0 25 0 1 0 1842336838 88920064 20651 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26557/statm): 21709 20651 145 145 0 21564 0
[pid=26557] vsize: 86836
Current children cumulated CPU time (s) 748.57
Current children cumulated vsize (Kb) 88960

[startup+760.071 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 21114 0 0 0 75714 141 0 0 25 0 1 0 1842336838 89522176 20799 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 21856 20799 145 145 0 21711 0
[pid=26557] vsize: 87424
Current children cumulated CPU time (s) 758.56
Current children cumulated vsize (Kb) 89548

[startup+770.073 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 21240 0 0 0 76712 142 0 0 25 0 1 0 1842336838 90030080 20925 4294967295 134512640 135094434 3221224448 3221223040 134557401 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26557/statm): 21980 20925 145 145 0 21835 0
[pid=26557] vsize: 87920
Current children cumulated CPU time (s) 768.55
Current children cumulated vsize (Kb) 90044

[startup+780.073 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 21392 0 0 0 77708 144 0 0 25 0 1 0 1842336838 90648576 21077 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 22131 21077 145 145 0 21986 0
[pid=26557] vsize: 88524
Current children cumulated CPU time (s) 778.53
Current children cumulated vsize (Kb) 90648

[startup+790.075 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 21539 0 0 0 78707 145 0 0 25 0 1 0 1842336838 91246592 21224 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 22277 21224 145 145 0 22132 0
[pid=26557] vsize: 89108
Current children cumulated CPU time (s) 788.53
Current children cumulated vsize (Kb) 91232

[startup+800.076 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 21657 0 0 0 79706 146 0 0 25 0 1 0 1842336838 91725824 21342 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 22394 21342 145 145 0 22249 0
[pid=26557] vsize: 89576
Current children cumulated CPU time (s) 798.53
Current children cumulated vsize (Kb) 91700

[startup+810.076 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 21780 0 0 0 80704 147 0 0 25 0 1 0 1842336838 92221440 21465 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 22515 21465 145 145 0 22370 0
[pid=26557] vsize: 90060
Current children cumulated CPU time (s) 808.52
Current children cumulated vsize (Kb) 92184

[startup+820.077 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 21962 0 0 0 81701 148 0 0 25 0 1 0 1842336838 92962816 21647 4294967295 134512640 135094434 3221224448 3221223120 134556610 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 22696 21647 145 145 0 22551 0
[pid=26557] vsize: 90784
Current children cumulated CPU time (s) 818.5
Current children cumulated vsize (Kb) 92908

[startup+830.078 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 22114 0 0 0 82698 150 0 0 25 0 1 0 1842336838 93581312 21799 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 22847 21799 145 145 0 22702 0
[pid=26557] vsize: 91388
Current children cumulated CPU time (s) 828.49
Current children cumulated vsize (Kb) 93512

[startup+840.08 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 22219 0 0 0 83697 150 0 0 25 0 1 0 1842336838 93999104 21904 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 22949 21904 145 145 0 22804 0
[pid=26557] vsize: 91796
Current children cumulated CPU time (s) 838.48
Current children cumulated vsize (Kb) 93920

[startup+850.08 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 22375 0 0 0 84694 152 0 0 25 0 1 0 1842336838 94633984 22060 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 23104 22060 145 145 0 22959 0
[pid=26557] vsize: 92416
Current children cumulated CPU time (s) 848.47
Current children cumulated vsize (Kb) 94540

[startup+860.08 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 22539 0 0 0 85692 152 0 0 25 0 1 0 1842336838 95301632 22224 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 23267 22224 145 145 0 23122 0
[pid=26557] vsize: 93068
Current children cumulated CPU time (s) 858.45
Current children cumulated vsize (Kb) 95192

[startup+870.081 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 22712 0 0 0 86689 154 0 0 25 0 1 0 1842336838 96006144 22397 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 23439 22397 145 145 0 23294 0
[pid=26557] vsize: 93756
Current children cumulated CPU time (s) 868.44
Current children cumulated vsize (Kb) 95880

[startup+880.081 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 22825 0 0 0 87687 154 0 0 25 0 1 0 1842336838 96464896 22510 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 23551 22510 145 145 0 23406 0
[pid=26557] vsize: 94204
Current children cumulated CPU time (s) 878.42
Current children cumulated vsize (Kb) 96328

[startup+890.083 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 22947 0 0 0 88686 155 0 0 25 0 1 0 1842336838 96960512 22632 4294967295 134512640 135094434 3221224448 3221223072 134562128 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 23672 22632 145 145 0 23527 0
[pid=26557] vsize: 94688
Current children cumulated CPU time (s) 888.42
Current children cumulated vsize (Kb) 96812

[startup+900.084 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 23065 0 0 0 89684 156 0 0 25 0 1 0 1842336838 97439744 22750 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 23789 22750 145 145 0 23644 0
[pid=26557] vsize: 95156
Current children cumulated CPU time (s) 898.41
Current children cumulated vsize (Kb) 97280

[startup+910.085 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 23213 0 0 0 90682 157 0 0 25 0 1 0 1842336838 98041856 22898 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 23936 22898 145 145 0 23791 0
[pid=26557] vsize: 95744
Current children cumulated CPU time (s) 908.4
Current children cumulated vsize (Kb) 97868

[startup+920.085 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 23485 0 0 0 91676 159 0 0 25 0 1 0 1842336838 99151872 23170 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26557/statm): 24207 23170 145 145 0 24062 0
[pid=26557] vsize: 96828
Current children cumulated CPU time (s) 918.36
Current children cumulated vsize (Kb) 98952

[startup+930.086 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 23698 0 0 0 92673 160 0 0 25 0 1 0 1842336838 100020224 23383 4294967295 134512640 135094434 3221224448 3221223076 134557564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 24419 23383 145 145 0 24274 0
[pid=26557] vsize: 97676
Current children cumulated CPU time (s) 928.34
Current children cumulated vsize (Kb) 99800

[startup+940.088 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 23929 0 0 0 93670 162 0 0 25 0 1 0 1842336838 100962304 23614 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 24649 23614 145 145 0 24504 0
[pid=26557] vsize: 98596
Current children cumulated CPU time (s) 938.33
Current children cumulated vsize (Kb) 100720

[startup+950.088 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 24066 0 0 0 94668 163 0 0 25 0 1 0 1842336838 101519360 23751 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 24785 23751 145 145 0 24640 0
[pid=26557] vsize: 99140
Current children cumulated CPU time (s) 948.32
Current children cumulated vsize (Kb) 101264

[startup+960.088 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 24257 0 0 0 95666 164 0 0 25 0 1 0 1842336838 102301696 23942 4294967295 134512640 135094434 3221224448 3221223104 134558411 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 24976 23942 145 145 0 24831 0
[pid=26557] vsize: 99904
Current children cumulated CPU time (s) 958.31
Current children cumulated vsize (Kb) 102028

[startup+970.089 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 24445 0 0 0 96662 165 0 0 25 0 1 0 1842336838 103067648 24130 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 25163 24130 145 145 0 25018 0
[pid=26557] vsize: 100652
Current children cumulated CPU time (s) 968.28
Current children cumulated vsize (Kb) 102776

[startup+980.09 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 24625 0 0 0 97659 166 0 0 25 0 1 0 1842336838 103800832 24310 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 25342 24310 145 145 0 25197 0
[pid=26557] vsize: 101368
Current children cumulated CPU time (s) 978.26
Current children cumulated vsize (Kb) 103492

[startup+990.09 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 24847 0 0 0 98656 168 0 0 25 0 1 0 1842336838 104706048 24532 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 25563 24532 145 145 0 25418 0
[pid=26557] vsize: 102252
Current children cumulated CPU time (s) 988.25
Current children cumulated vsize (Kb) 104376

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 25081 0 0 0 99652 170 0 0 25 0 1 0 1842336838 105664512 24766 4294967295 134512640 135094434 3221224448 3221223040 134556999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 25797 24766 145 145 0 25652 0
[pid=26557] vsize: 103188
Current children cumulated CPU time (s) 998.23
Current children cumulated vsize (Kb) 105312

[startup+1010.09 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 25246 0 0 0 100649 171 0 0 25 0 1 0 1842336838 106860544 24931 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 26089 24931 145 145 0 25944 0
[pid=26557] vsize: 104356
Current children cumulated CPU time (s) 1008.21
Current children cumulated vsize (Kb) 106480

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 25430 0 0 0 101646 172 0 0 25 0 1 0 1842336838 107610112 25115 4294967295 134512640 135094434 3221224448 3221223104 134558286 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 26272 25115 145 145 0 26127 0
[pid=26557] vsize: 105088
Current children cumulated CPU time (s) 1018.19
Current children cumulated vsize (Kb) 107212

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 25626 0 0 0 102643 173 0 0 25 0 1 0 1842336838 108408832 25311 4294967295 134512640 135094434 3221224448 3221223040 134556964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 26467 25311 145 145 0 26322 0
[pid=26557] vsize: 105868
Current children cumulated CPU time (s) 1028.17
Current children cumulated vsize (Kb) 107992

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 25783 0 0 0 103640 175 0 0 25 0 1 0 1842336838 109047808 25468 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 26623 25468 145 145 0 26478 0
[pid=26557] vsize: 106492
Current children cumulated CPU time (s) 1038.16
Current children cumulated vsize (Kb) 108616

[startup+1050.09 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 25979 0 0 0 104637 177 0 0 25 0 1 0 1842336838 109846528 25664 4294967295 134512640 135094434 3221224448 3221223040 134557055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 26818 25664 145 145 0 26673 0
[pid=26557] vsize: 107272
Current children cumulated CPU time (s) 1048.15
Current children cumulated vsize (Kb) 109396

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 26181 0 0 0 105634 178 0 0 25 0 1 0 1842336838 110673920 25866 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 27020 25866 145 145 0 26875 0
[pid=26557] vsize: 108080
Current children cumulated CPU time (s) 1058.13
Current children cumulated vsize (Kb) 110204

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 26352 0 0 0 106632 179 0 0 25 0 1 0 1842336838 111370240 26037 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 27190 26037 145 145 0 27045 0
[pid=26557] vsize: 108760
Current children cumulated CPU time (s) 1068.12
Current children cumulated vsize (Kb) 110884

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 26582 0 0 0 107628 180 0 0 25 0 1 0 1842336838 112308224 26267 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 27419 26267 145 145 0 27274 0
[pid=26557] vsize: 109676
Current children cumulated CPU time (s) 1078.09
Current children cumulated vsize (Kb) 111800

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 26767 0 0 0 108626 181 0 0 25 0 1 0 1842336838 113061888 26452 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26557/statm): 27603 26452 145 145 0 27458 0
[pid=26557] vsize: 110412
Current children cumulated CPU time (s) 1088.08
Current children cumulated vsize (Kb) 112536

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 26914 0 0 0 109623 182 0 0 25 0 1 0 1842336838 113659904 26599 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 27749 26599 145 145 0 27604 0
[pid=26557] vsize: 110996
Current children cumulated CPU time (s) 1098.06
Current children cumulated vsize (Kb) 113120

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 27060 0 0 0 110621 183 0 0 25 0 1 0 1842336838 114253824 26745 4294967295 134512640 135094434 3221224448 3221223136 134554796 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 27894 26745 145 145 0 27749 0
[pid=26557] vsize: 111576
Current children cumulated CPU time (s) 1108.05
Current children cumulated vsize (Kb) 113700

[startup+1120.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 27171 0 0 0 111619 184 0 0 25 0 1 0 1842336838 114704384 26856 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 28004 26856 145 145 0 27859 0
[pid=26557] vsize: 112016
Current children cumulated CPU time (s) 1118.04
Current children cumulated vsize (Kb) 114140

[startup+1130.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 27296 0 0 0 112617 185 0 0 25 0 1 0 1842336838 115220480 26981 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 28130 26981 145 145 0 27985 0
[pid=26557] vsize: 112520
Current children cumulated CPU time (s) 1128.03
Current children cumulated vsize (Kb) 114644

[startup+1140.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 27395 0 0 0 113615 185 0 0 25 0 1 0 1842336838 115617792 27080 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 28227 27080 145 145 0 28082 0
[pid=26557] vsize: 112908
Current children cumulated CPU time (s) 1138.01
Current children cumulated vsize (Kb) 115032

[startup+1150.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 27531 0 0 0 114612 187 0 0 25 0 1 0 1842336838 116170752 27216 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 28362 27216 145 145 0 28217 0
[pid=26557] vsize: 113448
Current children cumulated CPU time (s) 1148
Current children cumulated vsize (Kb) 115572

[startup+1160.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 27641 0 0 0 115611 187 0 0 25 0 1 0 1842336838 116621312 27326 4294967295 134512640 135094434 3221224448 3221223040 134557040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 28472 27326 145 145 0 28327 0
[pid=26557] vsize: 113888
Current children cumulated CPU time (s) 1157.99
Current children cumulated vsize (Kb) 116012

[startup+1170.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 27797 0 0 0 116609 188 0 0 25 0 1 0 1842336838 117256192 27482 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 28627 27482 145 145 0 28482 0
[pid=26557] vsize: 114508
Current children cumulated CPU time (s) 1167.98
Current children cumulated vsize (Kb) 116632

[startup+1180.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 27912 0 0 0 117607 189 0 0 25 0 1 0 1842336838 117723136 27597 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 28741 27597 145 145 0 28596 0
[pid=26557] vsize: 114964
Current children cumulated CPU time (s) 1177.97
Current children cumulated vsize (Kb) 117088

[startup+1190.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 28039 0 0 0 118606 190 0 0 25 0 1 0 1842336838 118239232 27724 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 28867 27724 145 145 0 28722 0
[pid=26557] vsize: 115468
Current children cumulated CPU time (s) 1187.97
Current children cumulated vsize (Kb) 117592

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 28147 0 0 0 119605 190 0 0 25 0 1 0 1842336838 118685696 27832 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 28976 27832 145 145 0 28831 0
[pid=26557] vsize: 115904
Current children cumulated CPU time (s) 1197.96
Current children cumulated vsize (Kb) 118028

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 28261 0 0 0 120603 191 0 0 25 0 1 0 1842336838 119144448 27946 4294967295 134512640 135094434 3221224448 3221223040 134557248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 29088 27946 145 145 0 28943 0
[pid=26557] vsize: 116352
Current children cumulated CPU time (s) 1207.95
Current children cumulated vsize (Kb) 118476



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26557
Raw data (/proc/26553/stat): 26553 (minisat+_script) S 26552 26553 21452 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842336833 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26553/statm): 531 226 485 147 0 384 0
[pid=26553] vsize: 2124
Raw data (/proc/26557/stat): 26557 (minisat+_64-bit) R 26553 26553 21452 0 -1 0 28261 0 0 0 120603 191 0 0 25 0 1 0 1842336838 119144448 27946 4294967295 134512640 135094434 3221224448 3221223136 134554687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26557/statm): 29088 27946 145 145 0 28943 0
[pid=26557] vsize: 116352
Current children cumulated CPU time (s) 1207.95
Current children cumulated vsize (Kb) 118476

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

Child status: 10
Real time (s): 1210.17
CPU time (s): 1208.01
CPU user time (s): 1206.04
CPU system time (s): 1.9667
CPU usage (%): 99.8215
Max. virtual memory (cumulated for all children) (Kb): 118476