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/7770/stat): 7770 (minisat+_script) R 7769 7770 5299 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1841368948 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/7770/statm): 174 3 169 147 0 27 0
[pid=7770] 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=7771
New process pid=7772
New process pid=7773
execve syscall for /bin/sed executable
One traced child (pid=7772) 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=7773) exited with status: 0
One traced child (pid=7771) exited with status: 0
New process pid=7774
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc23/normalized-jac3.opb

[startup+10.004 s]
Raw data (loadavg): 0.93 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 6621 0 0 0 944 28 0 0 25 0 1 0 1841368953 30289920 6226 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7774/statm): 7395 6226 145 145 0 7250 0
[pid=7774] vsize: 29580
Current children cumulated CPU time (s) 9.72
Current children cumulated vsize (Kb) 31704

[startup+20.0046 s]
Raw data (loadavg): 0.94 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 7207 0 0 0 1933 33 0 0 25 0 1 0 1841368953 32366592 6733 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 7902 6733 145 145 0 7757 0
[pid=7774] vsize: 31608
Current children cumulated CPU time (s) 19.66
Current children cumulated vsize (Kb) 33732

[startup+30.0063 s]
Raw data (loadavg): 0.95 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 7783 0 0 0 2922 37 0 0 25 0 1 0 1841368953 34734080 7309 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 8480 7309 145 145 0 8335 0
[pid=7774] vsize: 33920
Current children cumulated CPU time (s) 29.59
Current children cumulated vsize (Kb) 36044

[startup+40.0069 s]
Raw data (loadavg): 0.96 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 8378 0 0 0 3910 42 0 0 25 0 1 0 1841368953 37163008 7904 4294967295 134512640 135094434 3221224448 3221223060 134563052 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 9073 7904 145 145 0 8928 0
[pid=7774] vsize: 36292
Current children cumulated CPU time (s) 39.52
Current children cumulated vsize (Kb) 38416

[startup+50.0086 s]
Raw data (loadavg): 0.96 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 9384 0 0 0 4893 48 0 0 25 0 1 0 1841368953 41312256 8910 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 10086 8910 145 145 0 9941 0
[pid=7774] vsize: 40344
Current children cumulated CPU time (s) 49.41
Current children cumulated vsize (Kb) 42468

[startup+60.0092 s]
Raw data (loadavg): 0.97 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 9744 0 0 0 5886 51 0 0 25 0 1 0 1841368953 42782720 9270 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 10445 9270 145 145 0 10300 0
[pid=7774] vsize: 41780
Current children cumulated CPU time (s) 59.37
Current children cumulated vsize (Kb) 43904

[startup+70.0098 s]
Raw data (loadavg): 0.97 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 10236 0 0 0 6878 54 0 0 25 0 1 0 1841368953 44793856 9762 4294967295 134512640 135094434 3221224448 3221223080 134557638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 10936 9762 145 145 0 10791 0
[pid=7774] vsize: 43744
Current children cumulated CPU time (s) 69.32
Current children cumulated vsize (Kb) 45868

[startup+80.0105 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 10577 0 0 0 7873 56 0 0 25 0 1 0 1841368953 46186496 10103 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 11276 10103 145 145 0 11131 0
[pid=7774] vsize: 45104
Current children cumulated CPU time (s) 79.29
Current children cumulated vsize (Kb) 47228

[startup+90.0111 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 10770 0 0 0 8868 58 0 0 25 0 1 0 1841368953 46972928 10296 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 11468 10296 145 145 0 11323 0
[pid=7774] vsize: 45872
Current children cumulated CPU time (s) 89.26
Current children cumulated vsize (Kb) 47996

[startup+100.012 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 10929 0 0 0 9865 59 0 0 25 0 1 0 1841368953 47620096 10455 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7774/statm): 11626 10455 145 145 0 11481 0
[pid=7774] vsize: 46504
Current children cumulated CPU time (s) 99.24
Current children cumulated vsize (Kb) 48628

[startup+110.013 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 11072 0 0 0 10862 60 0 0 25 0 1 0 1841368953 48201728 10598 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 11768 10598 145 145 0 11623 0
[pid=7774] vsize: 47072
Current children cumulated CPU time (s) 109.22
Current children cumulated vsize (Kb) 49196

[startup+120.014 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 11390 0 0 0 11858 62 0 0 25 0 1 0 1841368953 49565696 10916 4294967295 134512640 135094434 3221224448 3221223120 134555560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 12101 10916 145 145 0 11956 0
[pid=7774] vsize: 48404
Current children cumulated CPU time (s) 119.2
Current children cumulated vsize (Kb) 50528

[startup+130.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 11699 0 0 0 12852 64 0 0 25 0 1 0 1841368953 50827264 11225 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7774/statm): 12409 11225 145 145 0 12264 0
[pid=7774] vsize: 49636
Current children cumulated CPU time (s) 129.16
Current children cumulated vsize (Kb) 51760

[startup+140.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 11978 0 0 0 13846 67 0 0 25 0 1 0 1841368953 51965952 11504 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 12687 11504 145 145 0 12542 0
[pid=7774] vsize: 50748
Current children cumulated CPU time (s) 139.13
Current children cumulated vsize (Kb) 52872

[startup+150.017 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 12244 0 0 0 14841 70 0 0 25 0 1 0 1841368953 53043200 11770 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 12950 11770 145 145 0 12805 0
[pid=7774] vsize: 51800
Current children cumulated CPU time (s) 149.11
Current children cumulated vsize (Kb) 53924

[startup+160.018 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 12574 0 0 0 15836 72 0 0 25 0 1 0 1841368953 54390784 12100 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 13279 12100 145 145 0 13134 0
[pid=7774] vsize: 53116
Current children cumulated CPU time (s) 159.08
Current children cumulated vsize (Kb) 55240

[startup+170.018 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 13083 0 0 0 16827 75 0 0 25 0 1 0 1841368953 56467456 12609 4294967295 134512640 135094434 3221224448 3221223120 134555830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 13786 12609 145 145 0 13641 0
[pid=7774] vsize: 55144
Current children cumulated CPU time (s) 169.02
Current children cumulated vsize (Kb) 57268

[startup+180.019 s]
Raw data (loadavg): 0.99 0.98 0.99 1/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) T 7770 7770 5299 0 -1 0 13516 0 0 0 17820 78 0 0 25 0 1 0 1841368953 58245120 13042 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7774/statm): 14220 13042 145 145 0 14075 0
[pid=7774] vsize: 56880
Current children cumulated CPU time (s) 178.98
Current children cumulated vsize (Kb) 59004

[startup+190.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 14313 0 0 0 18804 84 0 0 25 0 1 0 1841368953 61501440 13839 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7774/statm): 15015 13839 145 145 0 14870 0
[pid=7774] vsize: 60060
Current children cumulated CPU time (s) 188.88
Current children cumulated vsize (Kb) 62184

[startup+200.021 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 14996 0 0 0 19793 88 0 0 25 0 1 0 1841368953 64294912 14522 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 15697 14522 145 145 0 15552 0
[pid=7774] vsize: 62788
Current children cumulated CPU time (s) 198.81
Current children cumulated vsize (Kb) 64912

[startup+210.022 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 15484 0 0 0 20786 90 0 0 25 0 1 0 1841368953 66105344 14931 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 16139 14931 145 145 0 15994 0
[pid=7774] vsize: 64556
Current children cumulated CPU time (s) 208.76
Current children cumulated vsize (Kb) 66680

[startup+220.022 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 15746 0 0 0 21781 93 0 0 25 0 1 0 1841368953 67178496 15193 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 16401 15193 145 145 0 16256 0
[pid=7774] vsize: 65604
Current children cumulated CPU time (s) 218.74
Current children cumulated vsize (Kb) 67728

[startup+230.023 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 16008 0 0 0 22776 95 0 0 25 0 1 0 1841368953 68239360 15455 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 16660 15455 145 145 0 16515 0
[pid=7774] vsize: 66640
Current children cumulated CPU time (s) 228.71
Current children cumulated vsize (Kb) 68764

[startup+240.024 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 16678 0 0 0 23765 100 0 0 23 0 1 0 1841368953 70975488 16125 4294967295 134512640 135094434 3221224448 3221223120 134555957 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 17328 16125 145 145 0 17183 0
[pid=7774] vsize: 69312
Current children cumulated CPU time (s) 238.65
Current children cumulated vsize (Kb) 71436

[startup+250.024 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 17185 0 0 0 24758 104 0 0 25 0 1 0 1841368953 73060352 16632 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 17837 16632 145 145 0 17692 0
[pid=7774] vsize: 71348
Current children cumulated CPU time (s) 248.62
Current children cumulated vsize (Kb) 73472

[startup+260.025 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 17543 0 0 0 25752 107 0 0 25 0 1 0 1841368953 74522624 16990 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 18194 16990 145 145 0 18049 0
[pid=7774] vsize: 72776
Current children cumulated CPU time (s) 258.59
Current children cumulated vsize (Kb) 74900

[startup+270.026 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 17870 0 0 0 26747 109 0 0 25 0 1 0 1841368953 75853824 17317 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 18519 17317 145 145 0 18374 0
[pid=7774] vsize: 74076
Current children cumulated CPU time (s) 268.56
Current children cumulated vsize (Kb) 76200

[startup+280.026 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 18537 0 0 0 27736 115 0 0 25 0 1 0 1841368953 78581760 17984 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 19185 17984 145 145 0 19040 0
[pid=7774] vsize: 76740
Current children cumulated CPU time (s) 278.51
Current children cumulated vsize (Kb) 78864

[startup+290.027 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 19008 0 0 0 28728 118 0 0 25 0 1 0 1841368953 80502784 18455 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 19654 18455 145 145 0 19509 0
[pid=7774] vsize: 78616
Current children cumulated CPU time (s) 288.46
Current children cumulated vsize (Kb) 80740

[startup+300.028 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 19332 0 0 0 29722 120 0 0 25 0 1 0 1841368953 81825792 18779 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 19977 18779 145 145 0 19832 0
[pid=7774] vsize: 79908
Current children cumulated CPU time (s) 298.42
Current children cumulated vsize (Kb) 82032

[startup+310.028 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 19781 0 0 0 30716 122 0 0 25 0 1 0 1841368953 83660800 19228 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 20425 19228 145 145 0 20280 0
[pid=7774] vsize: 81700
Current children cumulated CPU time (s) 308.38
Current children cumulated vsize (Kb) 83824

[startup+320.029 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 20130 0 0 0 31709 125 0 0 25 0 1 0 1841368953 85102592 19577 4294967295 134512640 135094434 3221224448 3221223040 134556742 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 20777 19577 145 145 0 20632 0
[pid=7774] vsize: 83108
Current children cumulated CPU time (s) 318.34
Current children cumulated vsize (Kb) 85232

[startup+330.031 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 20382 0 0 0 32704 128 0 0 25 0 1 0 1841368953 86130688 19829 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 21028 19829 145 145 0 20883 0
[pid=7774] vsize: 84112
Current children cumulated CPU time (s) 328.32
Current children cumulated vsize (Kb) 86236

[startup+340.031 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 20673 0 0 0 33698 132 0 0 25 0 1 0 1841368953 87318528 20120 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 21318 20120 145 145 0 21173 0
[pid=7774] vsize: 85272
Current children cumulated CPU time (s) 338.3
Current children cumulated vsize (Kb) 87396

[startup+350.032 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 20904 0 0 0 34694 134 0 0 25 0 1 0 1841368953 88260608 20351 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 21548 20351 145 145 0 21403 0
[pid=7774] vsize: 86192
Current children cumulated CPU time (s) 348.28
Current children cumulated vsize (Kb) 88316

[startup+360.032 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 21429 0 0 0 35685 138 0 0 25 0 1 0 1841368953 90402816 20876 4294967295 134512640 135094434 3221224448 3221223136 134554760 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 22071 20876 145 145 0 21926 0
[pid=7774] vsize: 88284
Current children cumulated CPU time (s) 358.23
Current children cumulated vsize (Kb) 90408

[startup+370.032 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 21765 0 0 0 36680 139 0 0 25 0 1 0 1841368953 91787264 21212 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 22409 21212 145 145 0 22264 0
[pid=7774] vsize: 89636
Current children cumulated CPU time (s) 368.19
Current children cumulated vsize (Kb) 91760

[startup+380.033 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 22116 0 0 0 37673 142 0 0 25 0 1 0 1841368953 93220864 21563 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 22759 21563 145 145 0 22614 0
[pid=7774] vsize: 91036
Current children cumulated CPU time (s) 378.15
Current children cumulated vsize (Kb) 93160

[startup+390.033 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 22492 0 0 0 38667 145 0 0 25 0 1 0 1841368953 94760960 21939 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 23135 21939 145 145 0 22990 0
[pid=7774] vsize: 92540
Current children cumulated CPU time (s) 388.12
Current children cumulated vsize (Kb) 94664

[startup+400.035 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 22882 0 0 0 39660 148 0 0 25 0 1 0 1841368953 96350208 22329 4294967295 134512640 135094434 3221224448 3221223040 134556904 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 23523 22329 145 145 0 23378 0
[pid=7774] vsize: 94092
Current children cumulated CPU time (s) 398.08
Current children cumulated vsize (Kb) 96216

[startup+410.036 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 23365 0 0 0 40654 151 0 0 25 0 1 0 1841368953 98328576 22812 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 24006 22812 145 145 0 23861 0
[pid=7774] vsize: 96024
Current children cumulated CPU time (s) 408.05
Current children cumulated vsize (Kb) 98148

[startup+420.036 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 23593 0 0 0 41648 153 0 0 25 0 1 0 1841368953 99258368 23040 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 24233 23040 145 145 0 24088 0
[pid=7774] vsize: 96932
Current children cumulated CPU time (s) 418.01
Current children cumulated vsize (Kb) 99056

[startup+430.038 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 24060 0 0 0 42641 156 0 0 25 0 1 0 1841368953 101163008 23507 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 24698 23507 145 145 0 24553 0
[pid=7774] vsize: 98792
Current children cumulated CPU time (s) 427.97
Current children cumulated vsize (Kb) 100916

[startup+440.039 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 24425 0 0 0 43634 159 0 0 25 0 1 0 1841368953 102653952 23872 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 25062 23872 145 145 0 24917 0
[pid=7774] vsize: 100248
Current children cumulated CPU time (s) 437.93
Current children cumulated vsize (Kb) 102372

[startup+450.039 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 24838 0 0 0 44628 162 0 0 25 0 1 0 1841368953 104341504 24285 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 25474 24285 145 145 0 25329 0
[pid=7774] vsize: 101896
Current children cumulated CPU time (s) 447.9
Current children cumulated vsize (Kb) 104020

[startup+460.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 25111 0 0 0 45624 165 0 0 25 0 1 0 1841368953 105459712 24558 4294967295 134512640 135094434 3221224448 3221223104 134557893 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 25747 24558 145 145 0 25602 0
[pid=7774] vsize: 102988
Current children cumulated CPU time (s) 457.89
Current children cumulated vsize (Kb) 105112

[startup+470.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 25461 0 0 0 46617 167 0 0 25 0 1 0 1841368953 106893312 24908 4294967295 134512640 135094434 3221224448 3221223104 134557956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 26097 24908 145 145 0 25952 0
[pid=7774] vsize: 104388
Current children cumulated CPU time (s) 467.84
Current children cumulated vsize (Kb) 106512

[startup+480.041 s]
Raw data (loadavg): 0.99 0.98 0.99 1/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) T 7770 7770 5299 0 -1 0 25768 0 0 0 47611 170 0 0 25 0 1 0 1841368953 108417024 25215 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7774/statm): 26469 25215 145 145 0 26324 0
[pid=7774] vsize: 105876
Current children cumulated CPU time (s) 477.81
Current children cumulated vsize (Kb) 108000

[startup+490.042 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 25989 0 0 0 48606 171 0 0 25 0 1 0 1841368953 109318144 25436 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 26689 25436 145 145 0 26544 0
[pid=7774] vsize: 106756
Current children cumulated CPU time (s) 487.77
Current children cumulated vsize (Kb) 108880

[startup+500.043 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 26409 0 0 0 49597 175 0 0 25 0 1 0 1841368953 111042560 25856 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 27110 25856 145 145 0 26965 0
[pid=7774] vsize: 108440
Current children cumulated CPU time (s) 497.72
Current children cumulated vsize (Kb) 110564

[startup+510.044 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 26749 0 0 0 50589 178 0 0 25 0 1 0 1841368953 112427008 26196 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7774/statm): 27448 26196 145 145 0 27303 0
[pid=7774] vsize: 109792
Current children cumulated CPU time (s) 507.67
Current children cumulated vsize (Kb) 111916

[startup+520.045 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 27024 0 0 0 51583 180 0 0 25 0 1 0 1841368953 113557504 26471 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7774/statm): 27724 26471 145 145 0 27579 0
[pid=7774] vsize: 110896
Current children cumulated CPU time (s) 517.63
Current children cumulated vsize (Kb) 113020

[startup+530.046 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 27277 0 0 0 52578 182 0 0 25 0 1 0 1841368953 114597888 26724 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 27978 26724 145 145 0 27833 0
[pid=7774] vsize: 111912
Current children cumulated CPU time (s) 527.6
Current children cumulated vsize (Kb) 114036

[startup+540.047 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) T 7770 7770 5299 0 -1 0 27670 0 0 0 53571 185 0 0 25 0 1 0 1841368953 116199424 27117 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7774/statm): 28369 27117 145 145 0 28224 0
[pid=7774] vsize: 113476
Current children cumulated CPU time (s) 537.56
Current children cumulated vsize (Kb) 115600

[startup+550.049 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 27991 0 0 0 54566 187 0 0 25 0 1 0 1841368953 117510144 27438 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 28689 27438 145 145 0 28544 0
[pid=7774] vsize: 114756
Current children cumulated CPU time (s) 547.53
Current children cumulated vsize (Kb) 116880

[startup+560.049 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 28292 0 0 0 55559 190 0 0 25 0 1 0 1841368953 118738944 27739 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 28989 27739 145 145 0 28844 0
[pid=7774] vsize: 115956
Current children cumulated CPU time (s) 557.49
Current children cumulated vsize (Kb) 118080

[startup+570.05 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 28770 0 0 0 56551 194 0 0 25 0 1 0 1841368953 120692736 28217 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 29466 28217 145 145 0 29321 0
[pid=7774] vsize: 117864
Current children cumulated CPU time (s) 567.45
Current children cumulated vsize (Kb) 119988

[startup+580.051 s]
Raw data (loadavg): 0.99 0.98 0.99 1/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) T 7770 7770 5299 0 -1 0 29139 0 0 0 57544 197 0 0 25 0 1 0 1841368953 122204160 28586 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7774/statm): 29835 28586 145 145 0 29690 0
[pid=7774] vsize: 119340
Current children cumulated CPU time (s) 577.41
Current children cumulated vsize (Kb) 121464

[startup+590.05 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 29506 0 0 0 58537 201 0 0 25 0 1 0 1841368953 123711488 28953 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 30203 28953 145 145 0 30058 0
[pid=7774] vsize: 120812
Current children cumulated CPU time (s) 587.38
Current children cumulated vsize (Kb) 122936

[startup+600.051 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 29769 0 0 0 59533 203 0 0 25 0 1 0 1841368953 124776448 29216 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 30463 29216 145 145 0 30318 0
[pid=7774] vsize: 121852
Current children cumulated CPU time (s) 597.36
Current children cumulated vsize (Kb) 123976

[startup+610.051 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 29987 0 0 0 60529 204 0 0 25 0 1 0 1841368953 125665280 29434 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 30680 29434 145 145 0 30535 0
[pid=7774] vsize: 122720
Current children cumulated CPU time (s) 607.33
Current children cumulated vsize (Kb) 124844

[startup+620.052 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 30392 0 0 0 61522 207 0 0 25 0 1 0 1841368953 127344640 29839 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 31090 29839 145 145 0 30945 0
[pid=7774] vsize: 124360
Current children cumulated CPU time (s) 617.29
Current children cumulated vsize (Kb) 126484

[startup+630.053 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 30801 0 0 0 62514 211 0 0 25 0 1 0 1841368953 129007616 30248 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 31496 30248 145 145 0 31351 0
[pid=7774] vsize: 125984
Current children cumulated CPU time (s) 627.25
Current children cumulated vsize (Kb) 128108

[startup+640.053 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 31173 0 0 0 63508 214 0 0 25 0 1 0 1841368953 130527232 30620 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 31867 30620 145 145 0 31722 0
[pid=7774] vsize: 127468
Current children cumulated CPU time (s) 637.22
Current children cumulated vsize (Kb) 129592

[startup+650.055 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 31502 0 0 0 64503 216 0 0 25 0 1 0 1841368953 131866624 30949 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 32194 30949 145 145 0 32049 0
[pid=7774] vsize: 128776
Current children cumulated CPU time (s) 647.19
Current children cumulated vsize (Kb) 130900

[startup+660.056 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 31872 0 0 0 65496 219 0 0 25 0 1 0 1841368953 133382144 31319 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 32564 31319 145 145 0 32419 0
[pid=7774] vsize: 130256
Current children cumulated CPU time (s) 657.15
Current children cumulated vsize (Kb) 132380

[startup+670.056 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 32163 0 0 0 66492 221 0 0 25 0 1 0 1841368953 134586368 31610 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 32858 31610 145 145 0 32713 0
[pid=7774] vsize: 131432
Current children cumulated CPU time (s) 667.13
Current children cumulated vsize (Kb) 133556

[startup+680.058 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 32454 0 0 0 67486 223 0 0 25 0 1 0 1841368953 135778304 31901 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 33149 31901 145 145 0 33004 0
[pid=7774] vsize: 132596
Current children cumulated CPU time (s) 677.09
Current children cumulated vsize (Kb) 134720

[startup+690.059 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 32815 0 0 0 68479 225 0 0 25 0 1 0 1841368953 137252864 32262 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 33509 32262 145 145 0 33364 0
[pid=7774] vsize: 134036
Current children cumulated CPU time (s) 687.04
Current children cumulated vsize (Kb) 136160

[startup+700.06 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 33090 0 0 0 69475 228 0 0 25 0 1 0 1841368953 138387456 32537 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 33786 32537 145 145 0 33641 0
[pid=7774] vsize: 135144
Current children cumulated CPU time (s) 697.03
Current children cumulated vsize (Kb) 137268

[startup+710.062 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 33386 0 0 0 70469 230 0 0 25 0 1 0 1841368953 139599872 32833 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7774/statm): 34082 32833 145 145 0 33937 0
[pid=7774] vsize: 136328
Current children cumulated CPU time (s) 706.99
Current children cumulated vsize (Kb) 138452

[startup+720.062 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 33743 0 0 0 71463 233 0 0 25 0 1 0 1841368953 141078528 33190 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 34443 33190 145 145 0 34298 0
[pid=7774] vsize: 137772
Current children cumulated CPU time (s) 716.96
Current children cumulated vsize (Kb) 139896

[startup+730.063 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 34056 0 0 0 72458 235 0 0 25 0 1 0 1841368953 142356480 33503 4294967295 134512640 135094434 3221224448 3221223072 134562133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 34755 33503 145 145 0 34610 0
[pid=7774] vsize: 139020
Current children cumulated CPU time (s) 726.93
Current children cumulated vsize (Kb) 141144

[startup+740.064 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 34442 0 0 0 73453 237 0 0 25 0 1 0 1841368953 143941632 33889 4294967295 134512640 135094434 3221224448 3221223040 134557137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 35142 33889 145 145 0 34997 0
[pid=7774] vsize: 140568
Current children cumulated CPU time (s) 736.9
Current children cumulated vsize (Kb) 142692

[startup+750.065 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 34734 0 0 0 74449 238 0 0 25 0 1 0 1841368953 145137664 34181 4294967295 134512640 135094434 3221224448 3221223040 134556964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 35434 34181 145 145 0 35289 0
[pid=7774] vsize: 141736
Current children cumulated CPU time (s) 746.87
Current children cumulated vsize (Kb) 143860

[startup+760.066 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 35095 0 0 0 75443 241 0 0 25 0 1 0 1841368953 146616320 34542 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 35795 34542 145 145 0 35650 0
[pid=7774] vsize: 143180
Current children cumulated CPU time (s) 756.84
Current children cumulated vsize (Kb) 145304

[startup+770.067 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 35403 0 0 0 76438 242 0 0 25 0 1 0 1841368953 147873792 34850 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36102 34850 145 145 0 35957 0
[pid=7774] vsize: 144408
Current children cumulated CPU time (s) 766.8
Current children cumulated vsize (Kb) 146532

[startup+780.068 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 35635 0 0 0 77435 244 0 0 25 0 1 0 1841368953 148819968 35082 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36333 35082 145 145 0 36188 0
[pid=7774] vsize: 145332
Current children cumulated CPU time (s) 776.79
Current children cumulated vsize (Kb) 147456

[startup+790.069 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 35941 0 0 0 78429 247 0 0 25 0 1 0 1841368953 150065152 35388 4294967295 134512640 135094434 3221224448 3221223104 134558281 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35388 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 786.76
Current children cumulated vsize (Kb) 148672

[startup+800.071 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36020 0 0 0 79429 248 0 0 25 0 1 0 1841368953 150065152 35388 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35388 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 796.77
Current children cumulated vsize (Kb) 148672

[startup+810.071 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36020 0 0 0 80429 248 0 0 25 0 1 0 1841368953 150065152 35388 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35388 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 806.77
Current children cumulated vsize (Kb) 148672

[startup+820.072 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36020 0 0 0 81427 250 0 0 25 0 1 0 1841368953 150065152 35388 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35388 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 816.77
Current children cumulated vsize (Kb) 148672

[startup+830.073 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36020 0 0 0 82427 250 0 0 25 0 1 0 1841368953 150065152 35388 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35388 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 826.77
Current children cumulated vsize (Kb) 148672

[startup+840.073 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36020 0 0 0 83427 251 0 0 25 0 1 0 1841368953 150065152 35388 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35388 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 836.78
Current children cumulated vsize (Kb) 148672

[startup+850.075 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36020 0 0 0 84427 251 0 0 25 0 1 0 1841368953 150065152 35388 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35388 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 846.78
Current children cumulated vsize (Kb) 148672

[startup+860.076 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36020 0 0 0 85427 251 0 0 25 0 1 0 1841368953 150065152 35388 4294967295 134512640 135094434 3221224448 3221223080 134557561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35388 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 856.78
Current children cumulated vsize (Kb) 148672

[startup+870.076 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36020 0 0 0 86427 251 0 0 25 0 1 0 1841368953 150065152 35388 4294967295 134512640 135094434 3221224448 3221223040 134556809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35388 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 866.78
Current children cumulated vsize (Kb) 148672

[startup+880.078 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36020 0 0 0 87427 252 0 0 25 0 1 0 1841368953 150065152 35388 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35388 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 876.79
Current children cumulated vsize (Kb) 148672

[startup+890.078 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36020 0 0 0 88427 252 0 0 25 0 1 0 1841368953 150065152 35388 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35388 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 886.79
Current children cumulated vsize (Kb) 148672

[startup+900.08 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36020 0 0 0 89427 252 0 0 25 0 1 0 1841368953 150065152 35388 4294967295 134512640 135094434 3221224448 3221223116 134555968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35388 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 896.79
Current children cumulated vsize (Kb) 148672

[startup+910.081 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36020 0 0 0 90427 252 0 0 25 0 1 0 1841368953 150065152 35388 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35388 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 906.79
Current children cumulated vsize (Kb) 148672

[startup+920.081 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36020 0 0 0 91428 252 0 0 25 0 1 0 1841368953 150065152 35388 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35388 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 916.8
Current children cumulated vsize (Kb) 148672

[startup+930.082 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36020 0 0 0 92427 253 0 0 25 0 1 0 1841368953 150065152 35388 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35388 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 926.8
Current children cumulated vsize (Kb) 148672

[startup+940.083 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36020 0 0 0 93428 253 0 0 25 0 1 0 1841368953 150065152 35388 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35388 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 936.81
Current children cumulated vsize (Kb) 148672

[startup+950.084 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36020 0 0 0 94428 253 0 0 25 0 1 0 1841368953 150065152 35388 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35388 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 946.81
Current children cumulated vsize (Kb) 148672

[startup+960.085 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36020 0 0 0 95428 253 0 0 25 0 1 0 1841368953 150065152 35388 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35388 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 956.81
Current children cumulated vsize (Kb) 148672

[startup+970.086 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36020 0 0 0 96428 253 0 0 25 0 1 0 1841368953 150065152 35388 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35388 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 966.81
Current children cumulated vsize (Kb) 148672

[startup+980.086 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36020 0 0 0 97428 253 0 0 25 0 1 0 1841368953 150065152 35388 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35388 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 976.81
Current children cumulated vsize (Kb) 148672

[startup+990.087 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36020 0 0 0 98429 253 0 0 25 0 1 0 1841368953 150065152 35388 4294967295 134512640 135094434 3221224448 3221223080 134557561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35388 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 986.82
Current children cumulated vsize (Kb) 148672

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36020 0 0 0 99428 253 0 0 25 0 1 0 1841368953 150065152 35388 4294967295 134512640 135094434 3221224448 3221223076 134557564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35388 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 996.81
Current children cumulated vsize (Kb) 148672

[startup+1010.09 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36020 0 0 0 100429 253 0 0 25 0 1 0 1841368953 150065152 35388 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35388 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 1006.82
Current children cumulated vsize (Kb) 148672

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36020 0 0 0 101429 253 0 0 25 0 1 0 1841368953 150065152 35388 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35388 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 1016.82
Current children cumulated vsize (Kb) 148672

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36020 0 0 0 102429 253 0 0 25 0 1 0 1841368953 150065152 35388 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35388 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 1026.82
Current children cumulated vsize (Kb) 148672

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36020 0 0 0 103429 253 0 0 25 0 1 0 1841368953 150065152 35388 4294967295 134512640 135094434 3221224448 3221223072 134557648 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35388 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 1036.82
Current children cumulated vsize (Kb) 148672

[startup+1050.09 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36020 0 0 0 104429 254 0 0 25 0 1 0 1841368953 150065152 35388 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35388 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 1046.83
Current children cumulated vsize (Kb) 148672

[startup+1060.09 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36020 0 0 0 105430 254 0 0 25 0 1 0 1841368953 150065152 35388 4294967295 134512640 135094434 3221224448 3221223040 134557143 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35388 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 1056.84
Current children cumulated vsize (Kb) 148672

[startup+1070.09 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36020 0 0 0 106430 254 0 0 25 0 1 0 1841368953 150065152 35388 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35388 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 1066.84
Current children cumulated vsize (Kb) 148672

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36020 0 0 0 107430 254 0 0 25 0 1 0 1841368953 150065152 35388 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35388 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 1076.84
Current children cumulated vsize (Kb) 148672

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36020 0 0 0 108431 254 0 0 25 0 1 0 1841368953 150065152 35388 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35388 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 1086.85
Current children cumulated vsize (Kb) 148672

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36020 0 0 0 109430 254 0 0 25 0 1 0 1841368953 150065152 35388 4294967295 134512640 135094434 3221224448 3221223072 134557711 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35388 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 1096.84
Current children cumulated vsize (Kb) 148672

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36020 0 0 0 110431 254 0 0 25 0 1 0 1841368953 150065152 35388 4294967295 134512640 135094434 3221224448 3221223040 134556906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35388 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 1106.85
Current children cumulated vsize (Kb) 148672

[startup+1120.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36022 0 0 0 111431 254 0 0 25 0 1 0 1841368953 150065152 35390 4294967295 134512640 135094434 3221224448 3221223104 134558286 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35390 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 1116.85
Current children cumulated vsize (Kb) 148672

[startup+1130.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36023 0 0 0 112431 254 0 0 25 0 1 0 1841368953 150065152 35391 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35391 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 1126.85
Current children cumulated vsize (Kb) 148672

[startup+1140.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36023 0 0 0 113431 254 0 0 25 0 1 0 1841368953 150065152 35391 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35391 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 1136.85
Current children cumulated vsize (Kb) 148672

[startup+1150.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36023 0 0 0 114432 254 0 0 25 0 1 0 1841368953 150065152 35391 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35391 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 1146.86
Current children cumulated vsize (Kb) 148672

[startup+1160.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36023 0 0 0 115432 255 0 0 25 0 1 0 1841368953 150065152 35391 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35391 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 1156.87
Current children cumulated vsize (Kb) 148672

[startup+1170.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36023 0 0 0 116432 255 0 0 25 0 1 0 1841368953 150065152 35391 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35391 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 1166.87
Current children cumulated vsize (Kb) 148672

[startup+1180.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36024 0 0 0 117432 255 0 0 25 0 1 0 1841368953 150065152 35392 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35392 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 1176.87
Current children cumulated vsize (Kb) 148672

[startup+1190.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36024 0 0 0 118432 255 0 0 25 0 1 0 1841368953 150065152 35392 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35392 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 1186.87
Current children cumulated vsize (Kb) 148672

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36024 0 0 0 119433 255 0 0 25 0 1 0 1841368953 150065152 35392 4294967295 134512640 135094434 3221224448 3221223104 134557928 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35392 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 1196.88
Current children cumulated vsize (Kb) 148672

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36024 0 0 0 120433 255 0 0 25 0 1 0 1841368953 150065152 35392 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35392 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 1206.88
Current children cumulated vsize (Kb) 148672



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 7774
Raw data (/proc/7770/stat): 7770 (minisat+_script) S 7769 7770 5299 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841368948 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7770/statm): 531 226 485 147 0 384 0
[pid=7770] vsize: 2124
Raw data (/proc/7774/stat): 7774 (minisat+_64-bit) R 7770 7770 5299 0 -1 0 36024 0 0 0 120433 255 0 0 25 0 1 0 1841368953 150065152 35392 4294967295 134512640 135094434 3221224448 3221223104 134557872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7774/statm): 36637 35392 145 145 0 36492 0
[pid=7774] vsize: 146548
Current children cumulated CPU time (s) 1206.88
Current children cumulated vsize (Kb) 148672

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

Child status: 10
Real time (s): 1210.18
CPU time (s): 1206.95
CPU user time (s): 1204.34
CPU system time (s): 2.6176
CPU usage (%): 99.7333
Max. virtual memory (cumulated for all children) (Kb): 148672