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/8857/stat): 8857 (minisat+_script) R 8856 8857 5245 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1841341126 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/8857/statm): 174 3 169 147 0 27 0
[pid=8857] 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=8858
New process pid=8859
New process pid=8860
execve syscall for /bin/sed executable
One traced child (pid=8859) 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=8860) exited with status: 0
One traced child (pid=8858) exited with status: 0
New process pid=8861
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc30/normalized-exam.pi.opb

[startup+10.0038 s]
Raw data (loadavg): 0.90 0.94 0.93 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 7144 0 0 0 953 24 0 0 25 0 1 0 1841341131 26533888 5852 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8861/statm): 6478 5852 145 145 0 6333 0
[pid=8861] vsize: 25912
Current children cumulated CPU time (s) 9.78
Current children cumulated vsize (Kb) 28036

[startup+20.0056 s]
Raw data (loadavg): 0.91 0.94 0.93 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 7662 0 0 0 1944 28 0 0 25 0 1 0 1841341131 28651520 6370 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 6995 6370 145 145 0 6850 0
[pid=8861] vsize: 27980
Current children cumulated CPU time (s) 19.73
Current children cumulated vsize (Kb) 30104

[startup+30.0064 s]
Raw data (loadavg): 0.92 0.94 0.93 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 8682 0 0 0 2928 35 0 0 25 0 1 0 1841341131 32833536 7390 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 8016 7390 145 145 0 7871 0
[pid=8861] vsize: 32064
Current children cumulated CPU time (s) 29.64
Current children cumulated vsize (Kb) 34188

[startup+40.0072 s]
Raw data (loadavg): 1.09 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 9727 0 0 0 3911 42 0 0 25 0 1 0 1841341131 37163008 8435 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8861/statm): 9073 8435 145 145 0 8928 0
[pid=8861] vsize: 36292
Current children cumulated CPU time (s) 39.54
Current children cumulated vsize (Kb) 38416

[startup+50.008 s]
Raw data (loadavg): 1.08 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 10558 0 0 0 4899 47 0 0 25 0 1 0 1841341131 40546304 9266 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 9899 9266 145 145 0 9754 0
[pid=8861] vsize: 39596
Current children cumulated CPU time (s) 49.47
Current children cumulated vsize (Kb) 41720

[startup+60.0088 s]
Raw data (loadavg): 1.06 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 11492 0 0 0 5885 52 0 0 25 0 1 0 1841341131 44355584 10200 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 10829 10200 145 145 0 10684 0
[pid=8861] vsize: 43316
Current children cumulated CPU time (s) 59.38
Current children cumulated vsize (Kb) 45440

[startup+70.0096 s]
Raw data (loadavg): 1.05 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 12414 0 0 0 6871 58 0 0 25 0 1 0 1841341131 48119808 11122 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 11748 11122 145 145 0 11603 0
[pid=8861] vsize: 46992
Current children cumulated CPU time (s) 69.3
Current children cumulated vsize (Kb) 49116

[startup+80.0104 s]
Raw data (loadavg): 1.04 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 13339 0 0 0 7855 64 0 0 25 0 1 0 1841341131 52027392 12047 4294967295 134512640 135094434 3221224448 3221223120 134556252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8861/statm): 12702 12047 145 145 0 12557 0
[pid=8861] vsize: 50808
Current children cumulated CPU time (s) 79.2
Current children cumulated vsize (Kb) 52932

[startup+90.0112 s]
Raw data (loadavg): 1.04 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 14196 0 0 0 8839 72 0 0 25 0 1 0 1841341131 55525376 12904 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8861/statm): 13556 12904 145 145 0 13411 0
[pid=8861] vsize: 54224
Current children cumulated CPU time (s) 89.12
Current children cumulated vsize (Kb) 56348

[startup+100.012 s]
Raw data (loadavg): 1.03 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 14991 0 0 0 9825 78 0 0 25 0 1 0 1841341131 58769408 13699 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8861/statm): 14348 13699 145 145 0 14203 0
[pid=8861] vsize: 57392
Current children cumulated CPU time (s) 99.04
Current children cumulated vsize (Kb) 59516

[startup+110.014 s]
Raw data (loadavg): 1.03 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 15728 0 0 0 10812 83 0 0 25 0 1 0 1841341131 61775872 14436 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8861/statm): 15082 14436 145 145 0 14937 0
[pid=8861] vsize: 60328
Current children cumulated CPU time (s) 108.96
Current children cumulated vsize (Kb) 62452

[startup+120.016 s]
Raw data (loadavg): 1.02 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 16484 0 0 0 11799 88 0 0 25 0 1 0 1841341131 64868352 15192 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 15837 15192 145 145 0 15692 0
[pid=8861] vsize: 63348
Current children cumulated CPU time (s) 118.88
Current children cumulated vsize (Kb) 65472

[startup+130.015 s]
Raw data (loadavg): 1.02 0.98 0.94 1/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) T 8857 8857 5245 0 -1 0 17327 0 0 0 12785 94 0 0 25 0 1 0 1841341131 68321280 16035 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/8861/statm): 16680 16035 145 145 0 16535 0
[pid=8861] vsize: 66720
Current children cumulated CPU time (s) 128.8
Current children cumulated vsize (Kb) 68844

[startup+140.016 s]
Raw data (loadavg): 1.01 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 18107 0 0 0 13773 98 0 0 25 0 1 0 1841341131 71512064 16815 4294967295 134512640 135094434 3221224448 3221223088 134539506 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 17459 16815 145 145 0 17314 0
[pid=8861] vsize: 69836
Current children cumulated CPU time (s) 138.72
Current children cumulated vsize (Kb) 71960

[startup+150.017 s]
Raw data (loadavg): 1.01 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 18798 0 0 0 14762 102 0 0 25 0 1 0 1841341131 74342400 17506 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 18150 17506 145 145 0 18005 0
[pid=8861] vsize: 72600
Current children cumulated CPU time (s) 148.65
Current children cumulated vsize (Kb) 74724

[startup+160.018 s]
Raw data (loadavg): 1.01 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 19532 0 0 0 15749 107 0 0 25 0 1 0 1841341131 77340672 18240 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 18882 18240 145 145 0 18737 0
[pid=8861] vsize: 75528
Current children cumulated CPU time (s) 158.57
Current children cumulated vsize (Kb) 77652

[startup+170.019 s]
Raw data (loadavg): 1.01 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 20158 0 0 0 16739 112 0 0 25 0 1 0 1841341131 79896576 18866 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 19506 18866 145 145 0 19361 0
[pid=8861] vsize: 78024
Current children cumulated CPU time (s) 168.52
Current children cumulated vsize (Kb) 80148

[startup+180.019 s]
Raw data (loadavg): 1.01 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 20800 0 0 0 17729 116 0 0 25 0 1 0 1841341131 82534400 19508 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 20150 19508 145 145 0 20005 0
[pid=8861] vsize: 80600
Current children cumulated CPU time (s) 178.46
Current children cumulated vsize (Kb) 82724

[startup+190.021 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 21462 0 0 0 18716 121 0 0 25 0 1 0 1841341131 85250048 20170 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 20813 20170 145 145 0 20668 0
[pid=8861] vsize: 83252
Current children cumulated CPU time (s) 188.38
Current children cumulated vsize (Kb) 85376

[startup+200.022 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 22230 0 0 0 19702 126 0 0 25 0 1 0 1841341131 88387584 20938 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 21579 20938 145 145 0 21434 0
[pid=8861] vsize: 86316
Current children cumulated CPU time (s) 198.29
Current children cumulated vsize (Kb) 88440

[startup+210.024 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 22994 0 0 0 20690 131 0 0 17 0 1 0 1841341131 91508736 21702 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 22341 21702 145 145 0 22196 0
[pid=8861] vsize: 89364
Current children cumulated CPU time (s) 208.22
Current children cumulated vsize (Kb) 91488

[startup+220.025 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 23950 0 0 0 21675 138 0 0 25 0 1 0 1841341131 95674368 22658 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 23358 22658 145 145 0 23213 0
[pid=8861] vsize: 93432
Current children cumulated CPU time (s) 218.14
Current children cumulated vsize (Kb) 95556

[startup+230.025 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 24916 0 0 0 22662 143 0 0 25 0 1 0 1841341131 99618816 23624 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 24321 23624 145 145 0 24176 0
[pid=8861] vsize: 97284
Current children cumulated CPU time (s) 228.06
Current children cumulated vsize (Kb) 99408

[startup+240.026 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 25854 0 0 0 23649 148 0 0 25 0 1 0 1841341131 103452672 24562 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 25257 24562 145 145 0 25112 0
[pid=8861] vsize: 101028
Current children cumulated CPU time (s) 237.98
Current children cumulated vsize (Kb) 103152

[startup+250.027 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 26824 0 0 0 24633 155 0 0 25 0 1 0 1841341131 107417600 25532 4294967295 134512640 135094434 3221224448 3221223040 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 26225 25532 145 145 0 26080 0
[pid=8861] vsize: 104900
Current children cumulated CPU time (s) 247.89
Current children cumulated vsize (Kb) 107024

[startup+260.029 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 27690 0 0 0 25621 160 0 0 25 0 1 0 1841341131 110964736 26398 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 27091 26398 145 145 0 26946 0
[pid=8861] vsize: 108364
Current children cumulated CPU time (s) 257.82
Current children cumulated vsize (Kb) 110488

[startup+270.029 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 28509 0 0 0 26608 165 0 0 25 0 1 0 1841341131 114311168 27217 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 27908 27217 145 145 0 27763 0
[pid=8861] vsize: 111632
Current children cumulated CPU time (s) 267.74
Current children cumulated vsize (Kb) 113756

[startup+280.03 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 29335 0 0 0 27596 169 0 0 25 0 1 0 1841341131 117690368 28043 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8861/statm): 28733 28043 145 145 0 28588 0
[pid=8861] vsize: 114932
Current children cumulated CPU time (s) 277.66
Current children cumulated vsize (Kb) 117056

[startup+290.032 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 29994 0 0 0 28585 174 0 0 25 0 1 0 1841341131 120377344 28702 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 29389 28702 145 145 0 29244 0
[pid=8861] vsize: 117556
Current children cumulated CPU time (s) 287.6
Current children cumulated vsize (Kb) 119680

[startup+300.033 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 30543 0 0 0 29576 178 0 0 25 0 1 0 1841341131 122613760 29251 4294967295 134512640 135094434 3221224448 3221223060 134563077 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 29935 29251 145 145 0 29790 0
[pid=8861] vsize: 119740
Current children cumulated CPU time (s) 297.55
Current children cumulated vsize (Kb) 121864

[startup+310.033 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 30543 0 0 0 30575 178 0 0 25 0 1 0 1841341131 122613760 29251 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 29935 29251 145 145 0 29790 0
[pid=8861] vsize: 119740
Current children cumulated CPU time (s) 307.54
Current children cumulated vsize (Kb) 121864

[startup+320.034 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 30543 0 0 0 31576 178 0 0 25 0 1 0 1841341131 122613760 29251 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 29935 29251 145 145 0 29790 0
[pid=8861] vsize: 119740
Current children cumulated CPU time (s) 317.55
Current children cumulated vsize (Kb) 121864

[startup+330.035 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 30543 0 0 0 32576 178 0 0 25 0 1 0 1841341131 122613760 29251 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 29935 29251 145 145 0 29790 0
[pid=8861] vsize: 119740
Current children cumulated CPU time (s) 327.55
Current children cumulated vsize (Kb) 121864

[startup+340.036 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 30543 0 0 0 33576 178 0 0 25 0 1 0 1841341131 122613760 29251 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 29935 29251 145 145 0 29790 0
[pid=8861] vsize: 119740
Current children cumulated CPU time (s) 337.55
Current children cumulated vsize (Kb) 121864

[startup+350.037 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 30543 0 0 0 34577 178 0 0 25 0 1 0 1841341131 122613760 29251 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 29935 29251 145 145 0 29790 0
[pid=8861] vsize: 119740
Current children cumulated CPU time (s) 347.56
Current children cumulated vsize (Kb) 121864

[startup+360.037 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 30543 0 0 0 35577 178 0 0 25 0 1 0 1841341131 122613760 29251 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 29935 29251 145 145 0 29790 0
[pid=8861] vsize: 119740
Current children cumulated CPU time (s) 357.56
Current children cumulated vsize (Kb) 121864

[startup+370.037 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 30543 0 0 0 36577 178 0 0 25 0 1 0 1841341131 122613760 29251 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 29935 29251 145 145 0 29790 0
[pid=8861] vsize: 119740
Current children cumulated CPU time (s) 367.56
Current children cumulated vsize (Kb) 121864

[startup+380.038 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 30543 0 0 0 37577 178 0 0 25 0 1 0 1841341131 122613760 29251 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 29935 29251 145 145 0 29790 0
[pid=8861] vsize: 119740
Current children cumulated CPU time (s) 377.56
Current children cumulated vsize (Kb) 121864

[startup+390.04 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 30543 0 0 0 38577 178 0 0 25 0 1 0 1841341131 122613760 29251 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 29935 29251 145 145 0 29790 0
[pid=8861] vsize: 119740
Current children cumulated CPU time (s) 387.56
Current children cumulated vsize (Kb) 121864

[startup+400.041 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 30543 0 0 0 39577 178 0 0 25 0 1 0 1841341131 122613760 29251 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 29935 29251 145 145 0 29790 0
[pid=8861] vsize: 119740
Current children cumulated CPU time (s) 397.56
Current children cumulated vsize (Kb) 121864

[startup+410.042 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 30543 0 0 0 40578 178 0 0 25 0 1 0 1841341131 122613760 29251 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 29935 29251 145 145 0 29790 0
[pid=8861] vsize: 119740
Current children cumulated CPU time (s) 407.57
Current children cumulated vsize (Kb) 121864

[startup+420.043 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 30543 0 0 0 41578 178 0 0 25 0 1 0 1841341131 122613760 29251 4294967295 134512640 135094434 3221224448 3221223040 134557404 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 29935 29251 145 145 0 29790 0
[pid=8861] vsize: 119740
Current children cumulated CPU time (s) 417.57
Current children cumulated vsize (Kb) 121864

[startup+430.044 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 30543 0 0 0 42578 178 0 0 25 0 1 0 1841341131 122613760 29251 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 29935 29251 145 145 0 29790 0
[pid=8861] vsize: 119740
Current children cumulated CPU time (s) 427.57
Current children cumulated vsize (Kb) 121864

[startup+440.046 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 30543 0 0 0 43579 178 0 0 25 0 1 0 1841341131 122613760 29251 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 29935 29251 145 145 0 29790 0
[pid=8861] vsize: 119740
Current children cumulated CPU time (s) 437.58
Current children cumulated vsize (Kb) 121864

[startup+450.047 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 30543 0 0 0 44578 178 0 0 25 0 1 0 1841341131 122613760 29251 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 29935 29251 145 145 0 29790 0
[pid=8861] vsize: 119740
Current children cumulated CPU time (s) 447.57
Current children cumulated vsize (Kb) 121864

[startup+460.048 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 30543 0 0 0 45578 178 0 0 25 0 1 0 1841341131 122613760 29251 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 29935 29251 145 145 0 29790 0
[pid=8861] vsize: 119740
Current children cumulated CPU time (s) 457.57
Current children cumulated vsize (Kb) 121864

[startup+470.048 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 30543 0 0 0 46579 178 0 0 25 0 1 0 1841341131 122613760 29251 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 29935 29251 145 145 0 29790 0
[pid=8861] vsize: 119740
Current children cumulated CPU time (s) 467.58
Current children cumulated vsize (Kb) 121864

[startup+480.049 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 30543 0 0 0 47578 180 0 0 25 0 1 0 1841341131 122613760 29251 4294967295 134512640 135094434 3221224448 3221223060 134563083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 29935 29251 145 145 0 29790 0
[pid=8861] vsize: 119740
Current children cumulated CPU time (s) 477.59
Current children cumulated vsize (Kb) 121864

[startup+490.051 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 30543 0 0 0 48577 180 0 0 25 0 1 0 1841341131 122613760 29251 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 29935 29251 145 145 0 29790 0
[pid=8861] vsize: 119740
Current children cumulated CPU time (s) 487.58
Current children cumulated vsize (Kb) 121864

[startup+500.052 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 30543 0 0 0 49577 180 0 0 25 0 1 0 1841341131 122613760 29251 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 29935 29251 145 145 0 29790 0
[pid=8861] vsize: 119740
Current children cumulated CPU time (s) 497.58
Current children cumulated vsize (Kb) 121864

[startup+510.053 s]
Raw data (loadavg): 1.00 0.98 0.94 1/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) T 8857 8857 5245 0 -1 0 30596 0 0 0 50576 181 0 0 25 0 1 0 1841341131 122822656 29304 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/8861/statm): 29986 29304 145 145 0 29841 0
[pid=8861] vsize: 119944
Current children cumulated CPU time (s) 507.58
Current children cumulated vsize (Kb) 122068

[startup+520.053 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 31172 0 0 0 51566 186 0 0 25 0 1 0 1841341131 125169664 29880 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 30559 29880 145 145 0 30414 0
[pid=8861] vsize: 122236
Current children cumulated CPU time (s) 517.53
Current children cumulated vsize (Kb) 124360

[startup+530.054 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 31689 0 0 0 52558 190 0 0 25 0 1 0 1841341131 127287296 30397 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 31076 30397 145 145 0 30931 0
[pid=8861] vsize: 124304
Current children cumulated CPU time (s) 527.49
Current children cumulated vsize (Kb) 126428

[startup+540.055 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 32222 0 0 0 53549 193 0 0 25 0 1 0 1841341131 129478656 30930 4294967295 134512640 135094434 3221224448 3221223136 134554733 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 31611 30930 145 145 0 31466 0
[pid=8861] vsize: 126444
Current children cumulated CPU time (s) 537.43
Current children cumulated vsize (Kb) 128568

[startup+550.056 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 32738 0 0 0 54539 197 0 0 25 0 1 0 1841341131 131604480 31446 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8861/statm): 32130 31446 145 145 0 31985 0
[pid=8861] vsize: 128520
Current children cumulated CPU time (s) 547.37
Current children cumulated vsize (Kb) 130644

[startup+560.057 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 33270 0 0 0 55529 202 0 0 25 0 1 0 1841341131 133775360 31978 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 32660 31978 145 145 0 32515 0
[pid=8861] vsize: 130640
Current children cumulated CPU time (s) 557.32
Current children cumulated vsize (Kb) 132764

[startup+570.057 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 33550 0 0 0 56524 204 0 0 25 0 1 0 1841341131 134914048 32258 4294967295 134512640 135094434 3221224448 3221223120 134556519 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 32938 32258 145 145 0 32793 0
[pid=8861] vsize: 131752
Current children cumulated CPU time (s) 567.29
Current children cumulated vsize (Kb) 133876

[startup+580.058 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 33550 0 0 0 57524 204 0 0 25 0 1 0 1841341131 134914048 32258 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 32938 32258 145 145 0 32793 0
[pid=8861] vsize: 131752
Current children cumulated CPU time (s) 577.29
Current children cumulated vsize (Kb) 133876

[startup+590.059 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 33550 0 0 0 58524 204 0 0 25 0 1 0 1841341131 134914048 32258 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 32938 32258 145 145 0 32793 0
[pid=8861] vsize: 131752
Current children cumulated CPU time (s) 587.29
Current children cumulated vsize (Kb) 133876

[startup+600.06 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 33550 0 0 0 59524 204 0 0 25 0 1 0 1841341131 134914048 32258 4294967295 134512640 135094434 3221224448 3221223104 134558169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 32938 32258 145 145 0 32793 0
[pid=8861] vsize: 131752
Current children cumulated CPU time (s) 597.29
Current children cumulated vsize (Kb) 133876

[startup+610.06 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 33550 0 0 0 60524 204 0 0 25 0 1 0 1841341131 134914048 32258 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 32938 32258 145 145 0 32793 0
[pid=8861] vsize: 131752
Current children cumulated CPU time (s) 607.29
Current children cumulated vsize (Kb) 133876

[startup+620.06 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 33550 0 0 0 61525 204 0 0 25 0 1 0 1841341131 134914048 32258 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 32938 32258 145 145 0 32793 0
[pid=8861] vsize: 131752
Current children cumulated CPU time (s) 617.3
Current children cumulated vsize (Kb) 133876

[startup+630.061 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 33550 0 0 0 62525 205 0 0 25 0 1 0 1841341131 134914048 32258 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 32938 32258 145 145 0 32793 0
[pid=8861] vsize: 131752
Current children cumulated CPU time (s) 627.31
Current children cumulated vsize (Kb) 133876

[startup+640.062 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 33550 0 0 0 63525 205 0 0 25 0 1 0 1841341131 134914048 32258 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 32938 32258 145 145 0 32793 0
[pid=8861] vsize: 131752
Current children cumulated CPU time (s) 637.31
Current children cumulated vsize (Kb) 133876

[startup+650.063 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 33550 0 0 0 64525 205 0 0 25 0 1 0 1841341131 134914048 32258 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8861/statm): 32938 32258 145 145 0 32793 0
[pid=8861] vsize: 131752
Current children cumulated CPU time (s) 647.31
Current children cumulated vsize (Kb) 133876

[startup+660.064 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 33550 0 0 0 65524 206 0 0 25 0 1 0 1841341131 134914048 32258 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 32938 32258 145 145 0 32793 0
[pid=8861] vsize: 131752
Current children cumulated CPU time (s) 657.31
Current children cumulated vsize (Kb) 133876

[startup+670.064 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 33550 0 0 0 66524 206 0 0 25 0 1 0 1841341131 134914048 32258 4294967295 134512640 135094434 3221224448 3221223104 134558022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 32938 32258 145 145 0 32793 0
[pid=8861] vsize: 131752
Current children cumulated CPU time (s) 667.31
Current children cumulated vsize (Kb) 133876

[startup+680.065 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 33550 0 0 0 67524 206 0 0 25 0 1 0 1841341131 134914048 32258 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 32938 32258 145 145 0 32793 0
[pid=8861] vsize: 131752
Current children cumulated CPU time (s) 677.31
Current children cumulated vsize (Kb) 133876

[startup+690.066 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 33550 0 0 0 68524 206 0 0 25 0 1 0 1841341131 134914048 32258 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 32938 32258 145 145 0 32793 0
[pid=8861] vsize: 131752
Current children cumulated CPU time (s) 687.31
Current children cumulated vsize (Kb) 133876

[startup+700.067 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 33550 0 0 0 69525 206 0 0 25 0 1 0 1841341131 134914048 32258 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 32938 32258 145 145 0 32793 0
[pid=8861] vsize: 131752
Current children cumulated CPU time (s) 697.32
Current children cumulated vsize (Kb) 133876

[startup+710.067 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 33550 0 0 0 70524 206 0 0 25 0 1 0 1841341131 134914048 32258 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 32938 32258 145 145 0 32793 0
[pid=8861] vsize: 131752
Current children cumulated CPU time (s) 707.31
Current children cumulated vsize (Kb) 133876

[startup+720.067 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 33550 0 0 0 71525 206 0 0 25 0 1 0 1841341131 134914048 32258 4294967295 134512640 135094434 3221224448 3221223120 134555811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 32938 32258 145 145 0 32793 0
[pid=8861] vsize: 131752
Current children cumulated CPU time (s) 717.32
Current children cumulated vsize (Kb) 133876

[startup+730.068 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 33550 0 0 0 72525 206 0 0 25 0 1 0 1841341131 134914048 32258 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 32938 32258 145 145 0 32793 0
[pid=8861] vsize: 131752
Current children cumulated CPU time (s) 727.32
Current children cumulated vsize (Kb) 133876

[startup+740.07 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 33550 0 0 0 73525 206 0 0 25 0 1 0 1841341131 134914048 32258 4294967295 134512640 135094434 3221224448 3221223040 134557251 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 32938 32258 145 145 0 32793 0
[pid=8861] vsize: 131752
Current children cumulated CPU time (s) 737.32
Current children cumulated vsize (Kb) 133876

[startup+750.071 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 33550 0 0 0 74525 206 0 0 25 0 1 0 1841341131 134914048 32258 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 32938 32258 145 145 0 32793 0
[pid=8861] vsize: 131752
Current children cumulated CPU time (s) 747.32
Current children cumulated vsize (Kb) 133876

[startup+760.072 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 33550 0 0 0 75525 206 0 0 25 0 1 0 1841341131 134914048 32258 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 32938 32258 145 145 0 32793 0
[pid=8861] vsize: 131752
Current children cumulated CPU time (s) 757.32
Current children cumulated vsize (Kb) 133876

[startup+770.072 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 33550 0 0 0 76525 207 0 0 25 0 1 0 1841341131 134914048 32258 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 32938 32258 145 145 0 32793 0
[pid=8861] vsize: 131752
Current children cumulated CPU time (s) 767.33
Current children cumulated vsize (Kb) 133876

[startup+780.073 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 33550 0 0 0 77526 207 0 0 25 0 1 0 1841341131 134914048 32258 4294967295 134512640 135094434 3221224448 3221223040 134557352 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 32938 32258 145 145 0 32793 0
[pid=8861] vsize: 131752
Current children cumulated CPU time (s) 777.34
Current children cumulated vsize (Kb) 133876

[startup+790.074 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 33550 0 0 0 78526 207 0 0 25 0 1 0 1841341131 134914048 32258 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 32938 32258 145 145 0 32793 0
[pid=8861] vsize: 131752
Current children cumulated CPU time (s) 787.34
Current children cumulated vsize (Kb) 133876

[startup+800.075 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 33550 0 0 0 79526 207 0 0 25 0 1 0 1841341131 134914048 32258 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 32938 32258 145 145 0 32793 0
[pid=8861] vsize: 131752
Current children cumulated CPU time (s) 797.34
Current children cumulated vsize (Kb) 133876

[startup+810.076 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 33550 0 0 0 80526 207 0 0 25 0 1 0 1841341131 134914048 32258 4294967295 134512640 135094434 3221224448 3221223040 134556729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 32938 32258 145 145 0 32793 0
[pid=8861] vsize: 131752
Current children cumulated CPU time (s) 807.34
Current children cumulated vsize (Kb) 133876

[startup+820.076 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 33550 0 0 0 81526 207 0 0 25 0 1 0 1841341131 134914048 32258 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 32938 32258 145 145 0 32793 0
[pid=8861] vsize: 131752
Current children cumulated CPU time (s) 817.34
Current children cumulated vsize (Kb) 133876

[startup+830.076 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 33550 0 0 0 82526 207 0 0 25 0 1 0 1841341131 134914048 32258 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 32938 32258 145 145 0 32793 0
[pid=8861] vsize: 131752
Current children cumulated CPU time (s) 827.34
Current children cumulated vsize (Kb) 133876

[startup+840.078 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 33550 0 0 0 83527 207 0 0 25 0 1 0 1841341131 134914048 32258 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 32938 32258 145 145 0 32793 0
[pid=8861] vsize: 131752
Current children cumulated CPU time (s) 837.35
Current children cumulated vsize (Kb) 133876

[startup+850.079 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 33550 0 0 0 84527 207 0 0 25 0 1 0 1841341131 134914048 32258 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 32938 32258 145 145 0 32793 0
[pid=8861] vsize: 131752
Current children cumulated CPU time (s) 847.35
Current children cumulated vsize (Kb) 133876

[startup+860.08 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 33995 0 0 0 85518 210 0 0 25 0 1 0 1841341131 136740864 32703 4294967295 134512640 135094434 3221224448 3221223152 134554497 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8861/statm): 33384 32703 145 145 0 33239 0
[pid=8861] vsize: 133536
Current children cumulated CPU time (s) 857.29
Current children cumulated vsize (Kb) 135660

[startup+870.08 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 34763 0 0 0 86506 216 0 0 25 0 1 0 1841341131 139894784 33471 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 34154 33471 145 145 0 34009 0
[pid=8861] vsize: 136616
Current children cumulated CPU time (s) 867.23
Current children cumulated vsize (Kb) 138740

[startup+880.081 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 35564 0 0 0 87494 220 0 0 25 0 1 0 1841341131 143171584 34272 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 34954 34272 145 145 0 34809 0
[pid=8861] vsize: 139816
Current children cumulated CPU time (s) 877.15
Current children cumulated vsize (Kb) 141940

[startup+890.082 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 36280 0 0 0 88482 225 0 0 19 0 1 0 1841341131 146104320 34988 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 35670 34988 145 145 0 35525 0
[pid=8861] vsize: 142680
Current children cumulated CPU time (s) 887.08
Current children cumulated vsize (Kb) 144804

[startup+900.083 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 36868 0 0 0 89471 230 0 0 25 0 1 0 1841341131 148504576 35576 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 36256 35576 145 145 0 36111 0
[pid=8861] vsize: 145024
Current children cumulated CPU time (s) 897.02
Current children cumulated vsize (Kb) 147148

[startup+910.083 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 37532 0 0 0 90460 234 0 0 25 0 1 0 1841341131 151220224 36240 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 36919 36240 145 145 0 36774 0
[pid=8861] vsize: 147676
Current children cumulated CPU time (s) 906.95
Current children cumulated vsize (Kb) 149800

[startup+920.084 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 38199 0 0 0 91450 238 0 0 22 0 1 0 1841341131 153944064 36907 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 37584 36907 145 145 0 37439 0
[pid=8861] vsize: 150336
Current children cumulated CPU time (s) 916.89
Current children cumulated vsize (Kb) 152460

[startup+930.084 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 38751 0 0 0 92439 242 0 0 25 0 1 0 1841341131 156200960 37459 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 38135 37459 145 145 0 37990 0
[pid=8861] vsize: 152540
Current children cumulated CPU time (s) 926.82
Current children cumulated vsize (Kb) 154664

[startup+940.085 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 39411 0 0 0 93426 248 0 0 25 0 1 0 1841341131 158896128 38119 4294967295 134512640 135094434 3221224448 3221223040 134557401 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 38793 38119 145 145 0 38648 0
[pid=8861] vsize: 155172
Current children cumulated CPU time (s) 936.75
Current children cumulated vsize (Kb) 157296

[startup+950.086 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 40091 0 0 0 94416 253 0 0 22 0 1 0 1841341131 161673216 38799 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 39471 38799 145 145 0 39326 0
[pid=8861] vsize: 157884
Current children cumulated CPU time (s) 946.7
Current children cumulated vsize (Kb) 160008

[startup+960.085 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 40688 0 0 0 95407 257 0 0 25 0 1 0 1841341131 164110336 39396 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 40066 39396 145 145 0 39921 0
[pid=8861] vsize: 160264
Current children cumulated CPU time (s) 956.65
Current children cumulated vsize (Kb) 162388

[startup+970.086 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 40842 0 0 0 96405 259 0 0 25 0 1 0 1841341131 164741120 39550 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 40220 39550 145 145 0 40075 0
[pid=8861] vsize: 160880
Current children cumulated CPU time (s) 966.65
Current children cumulated vsize (Kb) 163004

[startup+980.087 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 40842 0 0 0 97405 259 0 0 25 0 1 0 1841341131 164741120 39550 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 40220 39550 145 145 0 40075 0
[pid=8861] vsize: 160880
Current children cumulated CPU time (s) 976.65
Current children cumulated vsize (Kb) 163004

[startup+990.088 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 40842 0 0 0 98405 259 0 0 25 0 1 0 1841341131 164741120 39550 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 40220 39550 145 145 0 40075 0
[pid=8861] vsize: 160880
Current children cumulated CPU time (s) 986.65
Current children cumulated vsize (Kb) 163004

[startup+1000.09 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 40842 0 0 0 99405 259 0 0 25 0 1 0 1841341131 164741120 39550 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 40220 39550 145 145 0 40075 0
[pid=8861] vsize: 160880
Current children cumulated CPU time (s) 996.65
Current children cumulated vsize (Kb) 163004

[startup+1010.09 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 40843 0 0 0 100405 259 0 0 25 0 1 0 1841341131 164741120 39551 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 40220 39551 145 145 0 40075 0
[pid=8861] vsize: 160880
Current children cumulated CPU time (s) 1006.65
Current children cumulated vsize (Kb) 163004

[startup+1020.09 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 40843 0 0 0 101406 259 0 0 25 0 1 0 1841341131 164741120 39551 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 40220 39551 145 145 0 40075 0
[pid=8861] vsize: 160880
Current children cumulated CPU time (s) 1016.66
Current children cumulated vsize (Kb) 163004

[startup+1030.09 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 40843 0 0 0 102406 259 0 0 25 0 1 0 1841341131 164741120 39551 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 40220 39551 145 145 0 40075 0
[pid=8861] vsize: 160880
Current children cumulated CPU time (s) 1026.66
Current children cumulated vsize (Kb) 163004

[startup+1040.09 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 40843 0 0 0 103406 259 0 0 25 0 1 0 1841341131 164741120 39551 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 40220 39551 145 145 0 40075 0
[pid=8861] vsize: 160880
Current children cumulated CPU time (s) 1036.66
Current children cumulated vsize (Kb) 163004

[startup+1050.09 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 40843 0 0 0 104406 259 0 0 25 0 1 0 1841341131 164741120 39551 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 40220 39551 145 145 0 40075 0
[pid=8861] vsize: 160880
Current children cumulated CPU time (s) 1046.66
Current children cumulated vsize (Kb) 163004

[startup+1060.09 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 40843 0 0 0 105406 259 0 0 25 0 1 0 1841341131 164741120 39551 4294967295 134512640 135094434 3221224448 3221223008 134550329 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 40220 39551 145 145 0 40075 0
[pid=8861] vsize: 160880
Current children cumulated CPU time (s) 1056.66
Current children cumulated vsize (Kb) 163004

[startup+1070.09 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 40843 0 0 0 106406 259 0 0 25 0 1 0 1841341131 164741120 39551 4294967295 134512640 135094434 3221224448 3221223120 134556543 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 40220 39551 145 145 0 40075 0
[pid=8861] vsize: 160880
Current children cumulated CPU time (s) 1066.66
Current children cumulated vsize (Kb) 163004

[startup+1080.09 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 40843 0 0 0 107405 260 0 0 25 0 1 0 1841341131 164741120 39551 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 40220 39551 145 145 0 40075 0
[pid=8861] vsize: 160880
Current children cumulated CPU time (s) 1076.66
Current children cumulated vsize (Kb) 163004

[startup+1090.09 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 40843 0 0 0 108405 261 0 0 25 0 1 0 1841341131 164741120 39551 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 40220 39551 145 145 0 40075 0
[pid=8861] vsize: 160880
Current children cumulated CPU time (s) 1086.67
Current children cumulated vsize (Kb) 163004

[startup+1100.1 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 40843 0 0 0 109405 261 0 0 25 0 1 0 1841341131 164741120 39551 4294967295 134512640 135094434 3221224448 3221223040 134557328 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8861/statm): 40220 39551 145 145 0 40075 0
[pid=8861] vsize: 160880
Current children cumulated CPU time (s) 1096.67
Current children cumulated vsize (Kb) 163004

[startup+1110.1 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 40843 0 0 0 110404 262 0 0 25 0 1 0 1841341131 164741120 39551 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 40220 39551 145 145 0 40075 0
[pid=8861] vsize: 160880
Current children cumulated CPU time (s) 1106.67
Current children cumulated vsize (Kb) 163004

[startup+1120.1 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 40843 0 0 0 111404 262 0 0 25 0 1 0 1841341131 164741120 39551 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 40220 39551 145 145 0 40075 0
[pid=8861] vsize: 160880
Current children cumulated CPU time (s) 1116.67
Current children cumulated vsize (Kb) 163004

[startup+1130.1 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 40843 0 0 0 112404 262 0 0 25 0 1 0 1841341131 164741120 39551 4294967295 134512640 135094434 3221224448 3221223040 134551908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 40220 39551 145 145 0 40075 0
[pid=8861] vsize: 160880
Current children cumulated CPU time (s) 1126.67
Current children cumulated vsize (Kb) 163004

[startup+1140.1 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 40843 0 0 0 113404 262 0 0 25 0 1 0 1841341131 164741120 39551 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 40220 39551 145 145 0 40075 0
[pid=8861] vsize: 160880
Current children cumulated CPU time (s) 1136.67
Current children cumulated vsize (Kb) 163004

[startup+1150.1 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 40843 0 0 0 114405 262 0 0 25 0 1 0 1841341131 164741120 39551 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 40220 39551 145 145 0 40075 0
[pid=8861] vsize: 160880
Current children cumulated CPU time (s) 1146.68
Current children cumulated vsize (Kb) 163004

[startup+1160.1 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 40843 0 0 0 115404 263 0 0 25 0 1 0 1841341131 164741120 39551 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 40220 39551 145 145 0 40075 0
[pid=8861] vsize: 160880
Current children cumulated CPU time (s) 1156.68
Current children cumulated vsize (Kb) 163004

[startup+1170.1 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 40843 0 0 0 116405 263 0 0 25 0 1 0 1841341131 164741120 39551 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 40220 39551 145 145 0 40075 0
[pid=8861] vsize: 160880
Current children cumulated CPU time (s) 1166.69
Current children cumulated vsize (Kb) 163004

[startup+1180.1 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 40843 0 0 0 117405 263 0 0 25 0 1 0 1841341131 164741120 39551 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 40220 39551 145 145 0 40075 0
[pid=8861] vsize: 160880
Current children cumulated CPU time (s) 1176.69
Current children cumulated vsize (Kb) 163004

[startup+1190.1 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 40843 0 0 0 118405 263 0 0 25 0 1 0 1841341131 164741120 39551 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 40220 39551 145 145 0 40075 0
[pid=8861] vsize: 160880
Current children cumulated CPU time (s) 1186.69
Current children cumulated vsize (Kb) 163004

[startup+1200.1 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 40843 0 0 0 119405 263 0 0 25 0 1 0 1841341131 164741120 39551 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 40220 39551 145 145 0 40075 0
[pid=8861] vsize: 160880
Current children cumulated CPU time (s) 1196.69
Current children cumulated vsize (Kb) 163004

[startup+1210.11 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 40843 0 0 0 120405 263 0 0 25 0 1 0 1841341131 164741120 39551 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 40220 39551 145 145 0 40075 0
[pid=8861] vsize: 160880
Current children cumulated CPU time (s) 1206.69
Current children cumulated vsize (Kb) 163004



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 1.00 0.98 0.94 2/57 8861
Raw data (/proc/8857/stat): 8857 (minisat+_script) S 8856 8857 5245 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1841341126 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8857/statm): 531 226 485 147 0 384 0
[pid=8857] vsize: 2124
Raw data (/proc/8861/stat): 8861 (minisat+_64-bit) R 8857 8857 5245 0 -1 0 40843 0 0 0 120405 263 0 0 25 0 1 0 1841341131 164741120 39551 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8861/statm): 40220 39551 145 145 0 40075 0
[pid=8861] vsize: 160880
Current children cumulated CPU time (s) 1206.69
Current children cumulated vsize (Kb) 163004

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

Child status: 10
Real time (s): 1210.19
CPU time (s): 1206.77
CPU user time (s): 1204.07
CPU system time (s): 2.70759
CPU usage (%): 99.7174
Max. virtual memory (cumulated for all children) (Kb): 163004