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/7790/stat): 7790 (minisat+_script) R 7789 7790 30740 0 -1 0 19 0 0 0 0 0 0 0 21 0 1 0 1785080450 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/7790/statm): 174 3 169 147 0 27 0
[pid=7790] 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=7791
New process pid=7792
New process pid=7793
execve syscall for /bin/sed executable
One traced child (pid=7792) 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=7793) exited with status: 0
One traced child (pid=7791) exited with status: 0
New process pid=7794
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc9/normalized-C432.opb

[startup+10.0035 s]
Raw data (loadavg): 0.87 0.92 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 9505 0 0 0 921 38 0 0 25 0 1 0 1785080455 39837696 9054 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7794/statm): 9726 9054 145 145 0 9581 0
[pid=7794] vsize: 38904
Current children cumulated CPU time (s) 9.6
Current children cumulated vsize (Kb) 41028

[startup+20.0042 s]
Raw data (loadavg): 0.89 0.93 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 9663 0 0 0 1918 40 0 0 25 0 1 0 1785080455 40464384 9212 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7794/statm): 9879 9212 145 145 0 9734 0
[pid=7794] vsize: 39516
Current children cumulated CPU time (s) 19.59
Current children cumulated vsize (Kb) 41640

[startup+30.006 s]
Raw data (loadavg): 0.90 0.93 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 9778 0 0 0 2916 41 0 0 25 0 1 0 1785080455 40955904 9327 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7794/statm): 9999 9327 145 145 0 9854 0
[pid=7794] vsize: 39996
Current children cumulated CPU time (s) 29.58
Current children cumulated vsize (Kb) 42120

[startup+40.0068 s]
Raw data (loadavg): 0.92 0.93 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 9828 0 0 0 3915 42 0 0 25 0 1 0 1785080455 41185280 9377 4294967295 134512640 135094434 3221224448 3221223060 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7794/statm): 10055 9377 145 145 0 9910 0
[pid=7794] vsize: 40220
Current children cumulated CPU time (s) 39.58
Current children cumulated vsize (Kb) 42344

[startup+50.0095 s]
Raw data (loadavg): 0.93 0.93 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 9920 0 0 0 4913 43 0 0 25 0 1 0 1785080455 41545728 9469 4294967295 134512640 135094434 3221224448 3221223120 134555560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7794/statm): 10143 9469 145 145 0 9998 0
[pid=7794] vsize: 40572
Current children cumulated CPU time (s) 49.57
Current children cumulated vsize (Kb) 42696

[startup+60.0103 s]
Raw data (loadavg): 0.94 0.93 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 10168 0 0 0 5908 46 0 0 25 0 1 0 1785080455 42553344 9717 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7794/statm): 10389 9717 145 145 0 10244 0
[pid=7794] vsize: 41556
Current children cumulated CPU time (s) 59.55
Current children cumulated vsize (Kb) 43680

[startup+70.011 s]
Raw data (loadavg): 0.95 0.94 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 10300 0 0 0 6905 47 0 0 25 0 1 0 1785080455 43147264 9849 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 10534 9849 145 145 0 10389 0
[pid=7794] vsize: 42136
Current children cumulated CPU time (s) 69.53
Current children cumulated vsize (Kb) 44260

[startup+80.0128 s]
Raw data (loadavg): 0.96 0.94 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 10417 0 0 0 7903 48 0 0 25 0 1 0 1785080455 43610112 9966 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 10647 9966 145 145 0 10502 0
[pid=7794] vsize: 42588
Current children cumulated CPU time (s) 79.52
Current children cumulated vsize (Kb) 44712

[startup+90.0136 s]
Raw data (loadavg): 0.96 0.94 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 10567 0 0 0 8899 50 0 0 25 0 1 0 1785080455 44204032 10116 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7794/statm): 10792 10116 145 145 0 10647 0
[pid=7794] vsize: 43168
Current children cumulated CPU time (s) 89.5
Current children cumulated vsize (Kb) 45292

[startup+100.015 s]
Raw data (loadavg): 0.97 0.94 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 10712 0 0 0 9896 51 0 0 25 0 1 0 1785080455 44908544 10261 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 10964 10261 145 145 0 10819 0
[pid=7794] vsize: 43856
Current children cumulated CPU time (s) 99.48
Current children cumulated vsize (Kb) 45980

[startup+110.017 s]
Raw data (loadavg): 0.97 0.94 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 10779 0 0 0 10895 52 0 0 25 0 1 0 1785080455 45174784 10328 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 11029 10328 145 145 0 10884 0
[pid=7794] vsize: 44116
Current children cumulated CPU time (s) 109.48
Current children cumulated vsize (Kb) 46240

[startup+120.018 s]
Raw data (loadavg): 0.98 0.94 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 10881 0 0 0 11894 52 0 0 25 0 1 0 1785080455 45576192 10430 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 11127 10430 145 145 0 10982 0
[pid=7794] vsize: 44508
Current children cumulated CPU time (s) 119.47
Current children cumulated vsize (Kb) 46632

[startup+130.019 s]
Raw data (loadavg): 0.98 0.94 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 10967 0 0 0 12893 53 0 0 25 0 1 0 1785080455 45924352 10516 4294967295 134512640 135094434 3221224448 3221223104 134557882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 11212 10516 145 145 0 11067 0
[pid=7794] vsize: 44848
Current children cumulated CPU time (s) 129.47
Current children cumulated vsize (Kb) 46972

[startup+140.019 s]
Raw data (loadavg): 0.98 0.95 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 11044 0 0 0 13892 53 0 0 25 0 1 0 1785080455 46235648 10593 4294967295 134512640 135094434 3221224448 3221223104 134558284 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 11288 10593 145 145 0 11143 0
[pid=7794] vsize: 45152
Current children cumulated CPU time (s) 139.46
Current children cumulated vsize (Kb) 47276

[startup+150.021 s]
Raw data (loadavg): 0.98 0.95 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 11138 0 0 0 14890 54 0 0 25 0 1 0 1785080455 46612480 10687 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 11380 10687 145 145 0 11235 0
[pid=7794] vsize: 45520
Current children cumulated CPU time (s) 149.45
Current children cumulated vsize (Kb) 47644

[startup+160.022 s]
Raw data (loadavg): 0.99 0.95 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 11215 0 0 0 15889 55 0 0 25 0 1 0 1785080455 46919680 10764 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 11455 10764 145 145 0 11310 0
[pid=7794] vsize: 45820
Current children cumulated CPU time (s) 159.45
Current children cumulated vsize (Kb) 47944

[startup+170.023 s]
Raw data (loadavg): 0.99 0.95 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 11331 0 0 0 16887 56 0 0 25 0 1 0 1785080455 47374336 10880 4294967295 134512640 135094434 3221224448 3221223072 134557650 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 11566 10880 145 145 0 11421 0
[pid=7794] vsize: 46264
Current children cumulated CPU time (s) 169.44
Current children cumulated vsize (Kb) 48388

[startup+180.023 s]
Raw data (loadavg): 0.99 0.95 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 11442 0 0 0 17885 57 0 0 25 0 1 0 1785080455 47820800 10991 4294967295 134512640 135094434 3221224448 3221223040 134557512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 11675 10991 145 145 0 11530 0
[pid=7794] vsize: 46700
Current children cumulated CPU time (s) 179.43
Current children cumulated vsize (Kb) 48824

[startup+190.024 s]
Raw data (loadavg): 0.99 0.95 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 11533 0 0 0 18884 57 0 0 25 0 1 0 1785080455 48189440 11082 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 11765 11082 145 145 0 11620 0
[pid=7794] vsize: 47060
Current children cumulated CPU time (s) 189.42
Current children cumulated vsize (Kb) 49184

[startup+200.025 s]
Raw data (loadavg): 0.99 0.95 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 11576 0 0 0 19883 58 0 0 25 0 1 0 1785080455 48357376 11125 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 11806 11125 145 145 0 11661 0
[pid=7794] vsize: 47224
Current children cumulated CPU time (s) 199.42
Current children cumulated vsize (Kb) 49348

[startup+210.026 s]
Raw data (loadavg): 0.99 0.95 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 11641 0 0 0 20883 58 0 0 25 0 1 0 1785080455 48619520 11190 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 11870 11190 145 145 0 11725 0
[pid=7794] vsize: 47480
Current children cumulated CPU time (s) 209.42
Current children cumulated vsize (Kb) 49604

[startup+220.026 s]
Raw data (loadavg): 0.99 0.95 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 11704 0 0 0 21881 58 0 0 25 0 1 0 1785080455 48873472 11253 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 11932 11253 145 145 0 11787 0
[pid=7794] vsize: 47728
Current children cumulated CPU time (s) 219.4
Current children cumulated vsize (Kb) 49852

[startup+230.028 s]
Raw data (loadavg): 0.99 0.95 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 11781 0 0 0 22881 59 0 0 25 0 1 0 1785080455 49184768 11330 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 12008 11330 145 145 0 11863 0
[pid=7794] vsize: 48032
Current children cumulated CPU time (s) 229.41
Current children cumulated vsize (Kb) 50156

[startup+240.029 s]
Raw data (loadavg): 0.99 0.95 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 11853 0 0 0 23879 59 0 0 25 0 1 0 1785080455 49475584 11402 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 12079 11402 145 145 0 11934 0
[pid=7794] vsize: 48316
Current children cumulated CPU time (s) 239.39
Current children cumulated vsize (Kb) 50440

[startup+250.03 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 11939 0 0 0 24878 60 0 0 25 0 1 0 1785080455 49819648 11488 4294967295 134512640 135094434 3221224448 3221223040 134556742 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 12163 11488 145 145 0 12018 0
[pid=7794] vsize: 48652
Current children cumulated CPU time (s) 249.39
Current children cumulated vsize (Kb) 50776

[startup+260.031 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 12049 0 0 0 25875 61 0 0 25 0 1 0 1785080455 50266112 11598 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 12272 11598 145 145 0 12127 0
[pid=7794] vsize: 49088
Current children cumulated CPU time (s) 259.37
Current children cumulated vsize (Kb) 51212

[startup+270.031 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 12152 0 0 0 26873 62 0 0 25 0 1 0 1785080455 50679808 11701 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 12373 11701 145 145 0 12228 0
[pid=7794] vsize: 49492
Current children cumulated CPU time (s) 269.36
Current children cumulated vsize (Kb) 51616

[startup+280.032 s]
Raw data (loadavg): 0.99 0.96 0.95 1/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) T 7790 7790 30740 0 -1 0 12243 0 0 0 27872 62 0 0 25 0 1 0 1785080455 51044352 11792 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/7794/statm): 12462 11792 145 145 0 12317 0
[pid=7794] vsize: 49848
Current children cumulated CPU time (s) 279.35
Current children cumulated vsize (Kb) 51972

[startup+290.033 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 12521 0 0 0 28866 65 0 0 25 0 1 0 1785080455 52170752 12070 4294967295 134512640 135094434 3221224448 3221223072 134557655 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 12737 12070 145 145 0 12592 0
[pid=7794] vsize: 50948
Current children cumulated CPU time (s) 289.32
Current children cumulated vsize (Kb) 53072

[startup+300.033 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 12878 0 0 0 29862 67 0 0 25 0 1 0 1785080455 53624832 12427 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 13092 12427 145 145 0 12947 0
[pid=7794] vsize: 52368
Current children cumulated CPU time (s) 299.3
Current children cumulated vsize (Kb) 54492

[startup+310.033 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 13085 0 0 0 30859 68 0 0 25 0 1 0 1785080455 54730752 12634 4294967295 134512640 135094434 3221224448 3221223104 134558295 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 13362 12634 145 145 0 13217 0
[pid=7794] vsize: 53448
Current children cumulated CPU time (s) 309.28
Current children cumulated vsize (Kb) 55572

[startup+320.034 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 13317 0 0 0 31854 71 0 0 25 0 1 0 1785080455 55676928 12866 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 13593 12866 145 145 0 13448 0
[pid=7794] vsize: 54372
Current children cumulated CPU time (s) 319.26
Current children cumulated vsize (Kb) 56496

[startup+330.036 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 13575 0 0 0 32849 72 0 0 25 0 1 0 1785080455 56729600 13124 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 13850 13124 145 145 0 13705 0
[pid=7794] vsize: 55400
Current children cumulated CPU time (s) 329.22
Current children cumulated vsize (Kb) 57524

[startup+340.037 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 13822 0 0 0 33846 74 0 0 25 0 1 0 1785080455 57733120 13371 4294967295 134512640 135094434 3221224448 3221223040 134556826 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 14095 13371 145 145 0 13950 0
[pid=7794] vsize: 56380
Current children cumulated CPU time (s) 339.21
Current children cumulated vsize (Kb) 58504

[startup+350.037 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 14085 0 0 0 34842 76 0 0 25 0 1 0 1785080455 58806272 13634 4294967295 134512640 135094434 3221224448 3221223040 134557210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 14357 13634 145 145 0 14212 0
[pid=7794] vsize: 57428
Current children cumulated CPU time (s) 349.19
Current children cumulated vsize (Kb) 59552

[startup+360.038 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 14303 0 0 0 35838 78 0 0 25 0 1 0 1785080455 59695104 13852 4294967295 134512640 135094434 3221224448 3221223136 134554685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 14574 13852 145 145 0 14429 0
[pid=7794] vsize: 58296
Current children cumulated CPU time (s) 359.17
Current children cumulated vsize (Kb) 60420

[startup+370.038 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 14512 0 0 0 36835 79 0 0 25 0 1 0 1785080455 60547072 14061 4294967295 134512640 135094434 3221224448 3221223040 134556826 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 14782 14061 145 145 0 14637 0
[pid=7794] vsize: 59128
Current children cumulated CPU time (s) 369.15
Current children cumulated vsize (Kb) 61252

[startup+380.039 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 14722 0 0 0 37833 81 0 0 25 0 1 0 1785080455 61407232 14271 4294967295 134512640 135094434 3221224448 3221223040 134557537 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 14992 14271 145 145 0 14847 0
[pid=7794] vsize: 59968
Current children cumulated CPU time (s) 379.15
Current children cumulated vsize (Kb) 62092

[startup+390.04 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 14944 0 0 0 38829 82 0 0 25 0 1 0 1785080455 62312448 14493 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7794/statm): 15213 14493 145 145 0 15068 0
[pid=7794] vsize: 60852
Current children cumulated CPU time (s) 389.12
Current children cumulated vsize (Kb) 62976

[startup+400.04 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 15183 0 0 0 39824 84 0 0 25 0 1 0 1785080455 63291392 14732 4294967295 134512640 135094434 3221224448 3221223040 134556802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 15452 14732 145 145 0 15307 0
[pid=7794] vsize: 61808
Current children cumulated CPU time (s) 399.09
Current children cumulated vsize (Kb) 63932

[startup+410.041 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 15370 0 0 0 40821 86 0 0 25 0 1 0 1785080455 64053248 14919 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 15638 14919 145 145 0 15493 0
[pid=7794] vsize: 62552
Current children cumulated CPU time (s) 409.08
Current children cumulated vsize (Kb) 64676

[startup+420.042 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 15589 0 0 0 41818 86 0 0 25 0 1 0 1785080455 64950272 15138 4294967295 134512640 135094434 3221224448 3221223040 134556891 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 15857 15138 145 145 0 15712 0
[pid=7794] vsize: 63428
Current children cumulated CPU time (s) 419.05
Current children cumulated vsize (Kb) 65552

[startup+430.043 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 15805 0 0 0 42815 87 0 0 25 0 1 0 1785080455 65830912 15354 4294967295 134512640 135094434 3221224448 3221223104 134558426 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 16072 15354 145 145 0 15927 0
[pid=7794] vsize: 64288
Current children cumulated CPU time (s) 429.03
Current children cumulated vsize (Kb) 66412

[startup+440.043 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 16017 0 0 0 43813 89 0 0 25 0 1 0 1785080455 66699264 15566 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 16284 15566 145 145 0 16139 0
[pid=7794] vsize: 65136
Current children cumulated CPU time (s) 439.03
Current children cumulated vsize (Kb) 67260

[startup+450.043 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 16199 0 0 0 44810 90 0 0 25 0 1 0 1785080455 67440640 15748 4294967295 134512640 135094434 3221224448 3221223040 134556802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 16465 15748 145 145 0 16320 0
[pid=7794] vsize: 65860
Current children cumulated CPU time (s) 449.01
Current children cumulated vsize (Kb) 67984

[startup+460.044 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 16446 0 0 0 45807 92 0 0 25 0 1 0 1785080455 68452352 15995 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 16712 15995 145 145 0 16567 0
[pid=7794] vsize: 66848
Current children cumulated CPU time (s) 459
Current children cumulated vsize (Kb) 68972

[startup+470.045 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 16588 0 0 0 46805 93 0 0 25 0 1 0 1785080455 69029888 16137 4294967295 134512640 135094434 3221224448 3221223072 134562057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 16853 16137 145 145 0 16708 0
[pid=7794] vsize: 67412
Current children cumulated CPU time (s) 468.99
Current children cumulated vsize (Kb) 69536

[startup+480.045 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 16715 0 0 0 47803 94 0 0 25 0 1 0 1785080455 69541888 16264 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 16978 16264 145 145 0 16833 0
[pid=7794] vsize: 67912
Current children cumulated CPU time (s) 478.98
Current children cumulated vsize (Kb) 70036

[startup+490.046 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 16869 0 0 0 48801 95 0 0 25 0 1 0 1785080455 70168576 16418 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 17131 16418 145 145 0 16986 0
[pid=7794] vsize: 68524
Current children cumulated CPU time (s) 488.97
Current children cumulated vsize (Kb) 70648

[startup+500.047 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 16998 0 0 0 49797 97 0 0 25 0 1 0 1785080455 70692864 16547 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7794/statm): 17259 16547 145 145 0 17114 0
[pid=7794] vsize: 69036
Current children cumulated CPU time (s) 498.95
Current children cumulated vsize (Kb) 71160

[startup+510.049 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 17182 0 0 0 50794 98 0 0 25 0 1 0 1785080455 71438336 16731 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 17441 16731 145 145 0 17296 0
[pid=7794] vsize: 69764
Current children cumulated CPU time (s) 508.93
Current children cumulated vsize (Kb) 71888

[startup+520.048 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 17362 0 0 0 51791 100 0 0 25 0 1 0 1785080455 72175616 16911 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 17621 16911 145 145 0 17476 0
[pid=7794] vsize: 70484
Current children cumulated CPU time (s) 518.92
Current children cumulated vsize (Kb) 72608

[startup+530.05 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 17542 0 0 0 52788 101 0 0 25 0 1 0 1785080455 72908800 17091 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7794/statm): 17800 17091 145 145 0 17655 0
[pid=7794] vsize: 71200
Current children cumulated CPU time (s) 528.9
Current children cumulated vsize (Kb) 73324

[startup+540.051 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 17683 0 0 0 53786 102 0 0 25 0 1 0 1785080455 73539584 17232 4294967295 134512640 135094434 3221224448 3221223040 134556933 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 17954 17232 145 145 0 17809 0
[pid=7794] vsize: 71816
Current children cumulated CPU time (s) 538.89
Current children cumulated vsize (Kb) 73940

[startup+550.051 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 17806 0 0 0 54784 103 0 0 25 0 1 0 1785080455 74031104 17355 4294967295 134512640 135094434 3221224448 3221223072 134557636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7794/statm): 18074 17355 145 145 0 17929 0
[pid=7794] vsize: 72296
Current children cumulated CPU time (s) 548.88
Current children cumulated vsize (Kb) 74420

[startup+560.053 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 17863 0 0 0 55782 104 0 0 25 0 1 0 1785080455 74256384 17412 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7794/statm): 18129 17412 145 145 0 17984 0
[pid=7794] vsize: 72516
Current children cumulated CPU time (s) 558.87
Current children cumulated vsize (Kb) 74640

[startup+570.053 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 17906 0 0 0 56781 106 0 0 25 0 1 0 1785080455 74428416 17455 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7794/statm): 18171 17455 145 145 0 18026 0
[pid=7794] vsize: 72684
Current children cumulated CPU time (s) 568.88
Current children cumulated vsize (Kb) 74808

[startup+580.054 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 17997 0 0 0 57779 107 0 0 25 0 1 0 1785080455 74797056 17546 4294967295 134512640 135094434 3221224448 3221223104 134558398 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7794/statm): 18261 17546 145 145 0 18116 0
[pid=7794] vsize: 73044
Current children cumulated CPU time (s) 578.87
Current children cumulated vsize (Kb) 75168

[startup+590.056 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 18190 0 0 0 58775 109 0 0 25 0 1 0 1785080455 75538432 17739 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7794/statm): 18442 17739 145 145 0 18297 0
[pid=7794] vsize: 73768
Current children cumulated CPU time (s) 588.85
Current children cumulated vsize (Kb) 75892

[startup+600.057 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 26654 0 0 0 59711 139 0 0 25 0 1 0 1785080455 112545792 25748 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7794/statm): 27477 25748 145 145 0 27332 0
[pid=7794] vsize: 109908
Current children cumulated CPU time (s) 598.51
Current children cumulated vsize (Kb) 112032

[startup+610.057 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 26773 0 0 0 60710 140 0 0 25 0 1 0 1785080455 112902144 25867 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7794/statm): 27564 25867 145 145 0 27419 0
[pid=7794] vsize: 110256
Current children cumulated CPU time (s) 608.51
Current children cumulated vsize (Kb) 112380

[startup+620.058 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 26874 0 0 0 61708 142 0 0 25 0 1 0 1785080455 113311744 25968 4294967295 134512640 135094434 3221224448 3221223040 134556941 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7794/statm): 27664 25968 145 145 0 27519 0
[pid=7794] vsize: 110656
Current children cumulated CPU time (s) 618.51
Current children cumulated vsize (Kb) 112780

[startup+630.06 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 26921 0 0 0 62707 142 0 0 25 0 1 0 1785080455 113504256 26015 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7794/statm): 27711 26015 145 145 0 27566 0
[pid=7794] vsize: 110844
Current children cumulated CPU time (s) 628.5
Current children cumulated vsize (Kb) 112968

[startup+640.061 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 27029 0 0 0 63705 143 0 0 25 0 1 0 1785080455 113901568 26123 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7794/statm): 27808 26123 145 145 0 27663 0
[pid=7794] vsize: 111232
Current children cumulated CPU time (s) 638.49
Current children cumulated vsize (Kb) 113356

[startup+650.061 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 27120 0 0 0 64703 145 0 0 25 0 1 0 1785080455 114262016 26214 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7794/statm): 27896 26214 145 145 0 27751 0
[pid=7794] vsize: 111584
Current children cumulated CPU time (s) 648.49
Current children cumulated vsize (Kb) 113708

[startup+660.063 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 27229 0 0 0 65700 146 0 0 25 0 1 0 1785080455 114704384 26323 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7794/statm): 28004 26323 145 145 0 27859 0
[pid=7794] vsize: 112016
Current children cumulated CPU time (s) 658.47
Current children cumulated vsize (Kb) 114140

[startup+670.064 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 27335 0 0 0 66698 148 0 0 25 0 1 0 1785080455 115130368 26429 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7794/statm): 28108 26429 145 145 0 27963 0
[pid=7794] vsize: 112432
Current children cumulated CPU time (s) 668.47
Current children cumulated vsize (Kb) 114556

[startup+680.066 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 27448 0 0 0 67697 149 0 0 25 0 1 0 1785080455 115585024 26542 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7794/statm): 28219 26542 145 145 0 28074 0
[pid=7794] vsize: 112876
Current children cumulated CPU time (s) 678.47
Current children cumulated vsize (Kb) 115000

[startup+690.068 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 27506 0 0 0 68695 150 0 0 25 0 1 0 1785080455 115814400 26600 4294967295 134512640 135094434 3221224448 3221223136 134554728 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7794/statm): 28275 26600 145 145 0 28130 0
[pid=7794] vsize: 113100
Current children cumulated CPU time (s) 688.46
Current children cumulated vsize (Kb) 115224

[startup+700.068 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 27581 0 0 0 69693 151 0 0 25 0 1 0 1785080455 116113408 26675 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7794/statm): 28348 26675 145 145 0 28203 0
[pid=7794] vsize: 113392
Current children cumulated CPU time (s) 698.45
Current children cumulated vsize (Kb) 115516

[startup+710.07 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 27684 0 0 0 70692 152 0 0 25 0 1 0 1785080455 116531200 26778 4294967295 134512640 135094434 3221224448 3221223072 134557574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7794/statm): 28450 26778 145 145 0 28305 0
[pid=7794] vsize: 113800
Current children cumulated CPU time (s) 708.45
Current children cumulated vsize (Kb) 115924

[startup+720.071 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 27771 0 0 0 71689 153 0 0 25 0 1 0 1785080455 116875264 26865 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7794/statm): 28534 26865 145 145 0 28389 0
[pid=7794] vsize: 114136
Current children cumulated CPU time (s) 718.43
Current children cumulated vsize (Kb) 116260

[startup+730.072 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 27844 0 0 0 72688 154 0 0 25 0 1 0 1785080455 117166080 26938 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7794/statm): 28605 26938 145 145 0 28460 0
[pid=7794] vsize: 114420
Current children cumulated CPU time (s) 728.43
Current children cumulated vsize (Kb) 116544

[startup+740.072 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 27929 0 0 0 73686 155 0 0 25 0 1 0 1785080455 117510144 27023 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7794/statm): 28689 27023 145 145 0 28544 0
[pid=7794] vsize: 114756
Current children cumulated CPU time (s) 738.42
Current children cumulated vsize (Kb) 116880

[startup+750.073 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 28141 0 0 0 74682 156 0 0 25 0 1 0 1785080455 118272000 27235 4294967295 134512640 135094434 3221224448 3221223040 134557227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7794/statm): 28875 27235 145 145 0 28730 0
[pid=7794] vsize: 115500
Current children cumulated CPU time (s) 748.39
Current children cumulated vsize (Kb) 117624

[startup+760.074 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 28665 0 0 0 75679 158 0 0 25 0 1 0 1785080455 120049664 27634 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7794/statm): 29309 27634 145 145 0 29164 0
[pid=7794] vsize: 117236
Current children cumulated CPU time (s) 758.38
Current children cumulated vsize (Kb) 119360

[startup+770.075 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 28667 0 0 0 76679 158 0 0 25 0 1 0 1785080455 120049664 27636 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 29309 27636 145 145 0 29164 0
[pid=7794] vsize: 117236
Current children cumulated CPU time (s) 768.38
Current children cumulated vsize (Kb) 119360

[startup+780.075 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 28672 0 0 0 77679 158 0 0 25 0 1 0 1785080455 120049664 27641 4294967295 134512640 135094434 3221224448 3221223040 134557213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 29309 27641 145 145 0 29164 0
[pid=7794] vsize: 117236
Current children cumulated CPU time (s) 778.38
Current children cumulated vsize (Kb) 119360

[startup+790.076 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 28766 0 0 0 78678 159 0 0 25 0 1 0 1785080455 120430592 27735 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 29402 27735 145 145 0 29257 0
[pid=7794] vsize: 117608
Current children cumulated CPU time (s) 788.38
Current children cumulated vsize (Kb) 119732

[startup+800.077 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 28832 0 0 0 79677 159 0 0 25 0 1 0 1785080455 120696832 27801 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 29467 27801 145 145 0 29322 0
[pid=7794] vsize: 117868
Current children cumulated CPU time (s) 798.37
Current children cumulated vsize (Kb) 119992

[startup+810.078 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 28890 0 0 0 80676 159 0 0 25 0 1 0 1785080455 120926208 27859 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 29523 27859 145 145 0 29378 0
[pid=7794] vsize: 118092
Current children cumulated CPU time (s) 808.36
Current children cumulated vsize (Kb) 120216

[startup+820.078 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 28917 0 0 0 81676 160 0 0 25 0 1 0 1785080455 121028608 27886 4294967295 134512640 135094434 3221224448 3221223104 134558246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 29548 27886 145 145 0 29403 0
[pid=7794] vsize: 118192
Current children cumulated CPU time (s) 818.37
Current children cumulated vsize (Kb) 120316

[startup+830.08 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 29032 0 0 0 82674 161 0 0 25 0 1 0 1785080455 121499648 28001 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 29663 28001 145 145 0 29518 0
[pid=7794] vsize: 118652
Current children cumulated CPU time (s) 828.36
Current children cumulated vsize (Kb) 120776

[startup+840.081 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 29102 0 0 0 83673 161 0 0 25 0 1 0 1785080455 121782272 28071 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 29732 28071 145 145 0 29587 0
[pid=7794] vsize: 118928
Current children cumulated CPU time (s) 838.35
Current children cumulated vsize (Kb) 121052

[startup+850.081 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 29176 0 0 0 84671 162 0 0 25 0 1 0 1785080455 122605568 28145 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 29933 28145 145 145 0 29788 0
[pid=7794] vsize: 119732
Current children cumulated CPU time (s) 848.34
Current children cumulated vsize (Kb) 121856

[startup+860.082 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 29265 0 0 0 85670 162 0 0 25 0 1 0 1785080455 122966016 28234 4294967295 134512640 135094434 3221224448 3221223104 134558281 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 30021 28234 145 145 0 29876 0
[pid=7794] vsize: 120084
Current children cumulated CPU time (s) 858.33
Current children cumulated vsize (Kb) 122208

[startup+870.083 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 29370 0 0 0 86667 163 0 0 25 0 1 0 1785080455 123392000 28339 4294967295 134512640 135094434 3221224448 3221223136 134554739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 30125 28339 145 145 0 29980 0
[pid=7794] vsize: 120500
Current children cumulated CPU time (s) 868.31
Current children cumulated vsize (Kb) 122624

[startup+880.084 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 29496 0 0 0 87666 163 0 0 25 0 1 0 1785080455 123904000 28465 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 30250 28465 145 145 0 30105 0
[pid=7794] vsize: 121000
Current children cumulated CPU time (s) 878.3
Current children cumulated vsize (Kb) 123124

[startup+890.086 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 29621 0 0 0 88664 165 0 0 25 0 1 0 1785080455 124411904 28590 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 30374 28590 145 145 0 30229 0
[pid=7794] vsize: 121496
Current children cumulated CPU time (s) 888.3
Current children cumulated vsize (Kb) 123620

[startup+900.087 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 29715 0 0 0 89662 165 0 0 25 0 1 0 1785080455 124792832 28684 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 30467 28684 145 145 0 30322 0
[pid=7794] vsize: 121868
Current children cumulated CPU time (s) 898.28
Current children cumulated vsize (Kb) 123992

[startup+910.087 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 30092 0 0 0 90659 167 0 0 25 0 1 0 1785080455 125108224 28774 4294967295 134512640 135094434 3221224448 3221223060 134563083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 30544 28774 145 145 0 30399 0
[pid=7794] vsize: 122176
Current children cumulated CPU time (s) 908.27
Current children cumulated vsize (Kb) 124300

[startup+920.088 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 30146 0 0 0 91658 168 0 0 25 0 1 0 1785080455 125321216 28828 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 30596 28828 145 145 0 30451 0
[pid=7794] vsize: 122384
Current children cumulated CPU time (s) 918.27
Current children cumulated vsize (Kb) 124508

[startup+930.09 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 30197 0 0 0 92657 168 0 0 25 0 1 0 1785080455 125521920 28879 4294967295 134512640 135094434 3221224448 3221223104 134558123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 30645 28879 145 145 0 30500 0
[pid=7794] vsize: 122580
Current children cumulated CPU time (s) 928.26
Current children cumulated vsize (Kb) 124704

[startup+940.091 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 30256 0 0 0 93657 168 0 0 25 0 1 0 1785080455 125755392 28938 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 30702 28938 145 145 0 30557 0
[pid=7794] vsize: 122808
Current children cumulated CPU time (s) 938.26
Current children cumulated vsize (Kb) 124932

[startup+950.091 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 30278 0 0 0 94657 168 0 0 25 0 1 0 1785080455 125841408 28960 4294967295 134512640 135094434 3221224448 3221223104 134558147 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 30723 28960 145 145 0 30578 0
[pid=7794] vsize: 122892
Current children cumulated CPU time (s) 948.26
Current children cumulated vsize (Kb) 125016

[startup+960.092 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 30339 0 0 0 95656 169 0 0 25 0 1 0 1785080455 126083072 29021 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 30782 29021 145 145 0 30637 0
[pid=7794] vsize: 123128
Current children cumulated CPU time (s) 958.26
Current children cumulated vsize (Kb) 125252

[startup+970.093 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 30381 0 0 0 96655 169 0 0 25 0 1 0 1785080455 126246912 29063 4294967295 134512640 135094434 3221224448 3221223108 134553515 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 30822 29063 145 145 0 30677 0
[pid=7794] vsize: 123288
Current children cumulated CPU time (s) 968.25
Current children cumulated vsize (Kb) 125412

[startup+980.094 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 30435 0 0 0 97655 170 0 0 25 0 1 0 1785080455 126464000 29117 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 30875 29117 145 145 0 30730 0
[pid=7794] vsize: 123500
Current children cumulated CPU time (s) 978.26
Current children cumulated vsize (Kb) 125624

[startup+990.095 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 30785 0 0 0 98652 171 0 0 25 0 1 0 1785080455 126717952 29182 4294967295 134512640 135094434 3221224448 3221223136 134554685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 30937 29182 145 145 0 30792 0
[pid=7794] vsize: 123748
Current children cumulated CPU time (s) 988.24
Current children cumulated vsize (Kb) 125872

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 30818 0 0 0 99652 172 0 0 25 0 1 0 1785080455 126849024 29215 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 30969 29215 145 145 0 30824 0
[pid=7794] vsize: 123876
Current children cumulated CPU time (s) 998.25
Current children cumulated vsize (Kb) 126000

[startup+1010.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 30880 0 0 0 100651 172 0 0 25 0 1 0 1785080455 127098880 29277 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 31030 29277 145 145 0 30885 0
[pid=7794] vsize: 124120
Current children cumulated CPU time (s) 1008.24
Current children cumulated vsize (Kb) 126244

[startup+1020.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 30945 0 0 0 101649 173 0 0 25 0 1 0 1785080455 127361024 29342 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 31094 29342 145 145 0 30949 0
[pid=7794] vsize: 124376
Current children cumulated CPU time (s) 1018.23
Current children cumulated vsize (Kb) 126500

[startup+1030.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 31109 0 0 0 102648 173 0 0 25 0 1 0 1785080455 128028672 29506 4294967295 134512640 135094434 3221224448 3221223104 134558254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 31257 29506 145 145 0 31112 0
[pid=7794] vsize: 125028
Current children cumulated CPU time (s) 1028.22
Current children cumulated vsize (Kb) 127152

[startup+1040.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 31211 0 0 0 103646 174 0 0 25 0 1 0 1785080455 128438272 29608 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 31357 29608 145 145 0 31212 0
[pid=7794] vsize: 125428
Current children cumulated CPU time (s) 1038.21
Current children cumulated vsize (Kb) 127552

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 31245 0 0 0 104645 174 0 0 25 0 1 0 1785080455 128573440 29642 4294967295 134512640 135094434 3221224448 3221223120 134555224 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 31390 29642 145 145 0 31245 0
[pid=7794] vsize: 125560
Current children cumulated CPU time (s) 1048.2
Current children cumulated vsize (Kb) 127684

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 31317 0 0 0 105644 175 0 0 25 0 1 0 1785080455 128860160 29714 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 31460 29714 145 145 0 31315 0
[pid=7794] vsize: 125840
Current children cumulated CPU time (s) 1058.2
Current children cumulated vsize (Kb) 127964

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 31379 0 0 0 106644 175 0 0 25 0 1 0 1785080455 129110016 29776 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 31521 29776 145 145 0 31376 0
[pid=7794] vsize: 126084
Current children cumulated CPU time (s) 1068.2
Current children cumulated vsize (Kb) 128208

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 31429 0 0 0 107642 176 0 0 25 0 1 0 1785080455 129306624 29826 4294967295 134512640 135094434 3221224448 3221223072 134562085 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 31569 29826 145 145 0 31424 0
[pid=7794] vsize: 126276
Current children cumulated CPU time (s) 1078.19
Current children cumulated vsize (Kb) 128400

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 31480 0 0 0 108642 177 0 0 25 0 1 0 1785080455 129503232 29877 4294967295 134512640 135094434 3221224448 3221223104 134558426 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 31617 29877 145 145 0 31472 0
[pid=7794] vsize: 126468
Current children cumulated CPU time (s) 1088.2
Current children cumulated vsize (Kb) 128592

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 31557 0 0 0 109641 177 0 0 25 0 1 0 1785080455 129818624 29954 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 31694 29954 145 145 0 31549 0
[pid=7794] vsize: 126776
Current children cumulated CPU time (s) 1098.19
Current children cumulated vsize (Kb) 128900

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 31690 0 0 0 110638 178 0 0 25 0 1 0 1785080455 130351104 30087 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 31824 30087 145 145 0 31679 0
[pid=7794] vsize: 127296
Current children cumulated CPU time (s) 1108.17
Current children cumulated vsize (Kb) 129420

[startup+1120.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 31775 0 0 0 111637 179 0 0 25 0 1 0 1785080455 130691072 30172 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 31907 30172 145 145 0 31762 0
[pid=7794] vsize: 127628
Current children cumulated CPU time (s) 1118.17
Current children cumulated vsize (Kb) 129752

[startup+1130.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 31881 0 0 0 112636 180 0 0 25 0 1 0 1785080455 131112960 30278 4294967295 134512640 135094434 3221224448 3221223108 134553497 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 32010 30278 145 145 0 31865 0
[pid=7794] vsize: 128040
Current children cumulated CPU time (s) 1128.17
Current children cumulated vsize (Kb) 130164

[startup+1140.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 31933 0 0 0 113636 180 0 0 25 0 1 0 1785080455 131317760 30330 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 32060 30330 145 145 0 31915 0
[pid=7794] vsize: 128240
Current children cumulated CPU time (s) 1138.17
Current children cumulated vsize (Kb) 130364

[startup+1150.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 31955 0 0 0 114635 180 0 0 25 0 1 0 1785080455 131403776 30352 4294967295 134512640 135094434 3221224448 3221223104 134557804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 32081 30352 145 145 0 31936 0
[pid=7794] vsize: 128324
Current children cumulated CPU time (s) 1148.16
Current children cumulated vsize (Kb) 130448

[startup+1160.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 31997 0 0 0 115635 181 0 0 25 0 1 0 1785080455 131571712 30394 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 32122 30394 145 145 0 31977 0
[pid=7794] vsize: 128488
Current children cumulated CPU time (s) 1158.17
Current children cumulated vsize (Kb) 130612

[startup+1170.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 32035 0 0 0 116634 181 0 0 25 0 1 0 1785080455 131727360 30432 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 32160 30432 145 145 0 32015 0
[pid=7794] vsize: 128640
Current children cumulated CPU time (s) 1168.16
Current children cumulated vsize (Kb) 130764

[startup+1180.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 32081 0 0 0 117633 182 0 0 25 0 1 0 1785080455 131911680 30478 4294967295 134512640 135094434 3221224448 3221223104 134557917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 32205 30478 145 145 0 32060 0
[pid=7794] vsize: 128820
Current children cumulated CPU time (s) 1178.16
Current children cumulated vsize (Kb) 130944

[startup+1190.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 32134 0 0 0 118633 182 0 0 25 0 1 0 1785080455 132124672 30531 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 32257 30531 145 145 0 32112 0
[pid=7794] vsize: 129028
Current children cumulated CPU time (s) 1188.16
Current children cumulated vsize (Kb) 131152

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 32175 0 0 0 119632 183 0 0 25 0 1 0 1785080455 132288512 30572 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 32297 30572 145 145 0 32152 0
[pid=7794] vsize: 129188
Current children cumulated CPU time (s) 1198.16
Current children cumulated vsize (Kb) 131312

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 32207 0 0 0 120631 183 0 0 25 0 1 0 1785080455 132419584 30604 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 32329 30604 145 145 0 32184 0
[pid=7794] vsize: 129316
Current children cumulated CPU time (s) 1208.15
Current children cumulated vsize (Kb) 131440



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 7794
Raw data (/proc/7790/stat): 7790 (minisat+_script) S 7789 7790 30740 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785080450 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7790/statm): 531 226 485 147 0 384 0
[pid=7790] vsize: 2124
Raw data (/proc/7794/stat): 7794 (minisat+_64-bit) R 7790 7790 30740 0 -1 0 32207 0 0 0 120632 183 0 0 25 0 1 0 1785080455 132419584 30604 4294967295 134512640 135094434 3221224448 3221223104 134557882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7794/statm): 32329 30604 145 145 0 32184 0
[pid=7794] vsize: 129316
Current children cumulated CPU time (s) 1208.16
Current children cumulated vsize (Kb) 131440

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

Child status: 10
Real time (s): 1210.18
CPU time (s): 1208.22
CPU user time (s): 1206.32
CPU system time (s): 1.89271
CPU usage (%): 99.8381
Max. virtual memory (cumulated for all children) (Kb): 131440