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/942/stat): 942 (minisat+_script) R 941 942 9102 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1855405930 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/942/statm): 174 3 169 147 0 27 0
[pid=942] 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=943
New process pid=944
New process pid=945
execve syscall for /bin/sed executable
One traced child (pid=944) 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=945) exited with status: 0
One traced child (pid=943) exited with status: 0
New process pid=946
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-pp08a.opb

[startup+10.0038 s]
Raw data (loadavg): 0.92 0.96 0.96 2/58 946
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 5925 0 0 0 948 24 0 0 25 0 1 0 1855405935 28663808 5729 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/946/statm): 6998 5729 145 145 0 6853 0
[pid=946] vsize: 27992
Current children cumulated CPU time (s) 9.72
Current children cumulated vsize (Kb) 30116

[startup+20.0048 s]
Raw data (loadavg): 0.93 0.96 0.96 2/58 948
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 5967 0 0 0 1946 24 0 0 25 0 1 0 1855405935 28819456 5771 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 7036 5771 145 145 0 6891 0
[pid=946] vsize: 28144
Current children cumulated CPU time (s) 19.7
Current children cumulated vsize (Kb) 30268

[startup+30.0067 s]
Raw data (loadavg): 0.94 0.96 0.96 2/58 948
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 5999 0 0 0 2946 25 0 0 25 0 1 0 1855405935 28913664 5803 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/946/statm): 7059 5803 145 145 0 6914 0
[pid=946] vsize: 28236
Current children cumulated CPU time (s) 29.71
Current children cumulated vsize (Kb) 30360

[startup+40.0076 s]
Raw data (loadavg): 0.95 0.97 0.96 2/58 948
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 6023 0 0 0 3945 25 0 0 25 0 1 0 1855405935 29028352 5827 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 7087 5827 145 145 0 6942 0
[pid=946] vsize: 28348
Current children cumulated CPU time (s) 39.7
Current children cumulated vsize (Kb) 30472

[startup+50.0096 s]
Raw data (loadavg): 0.96 0.97 0.96 2/58 948
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 6053 0 0 0 4945 25 0 0 25 0 1 0 1855405935 29126656 5857 4294967295 134512640 135094434 3221224432 3221223044 134563074 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 7111 5857 145 145 0 6966 0
[pid=946] vsize: 28444
Current children cumulated CPU time (s) 49.7
Current children cumulated vsize (Kb) 30568

[startup+60.0105 s]
Raw data (loadavg): 0.96 0.97 0.96 2/58 948
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 6090 0 0 0 5945 26 0 0 25 0 1 0 1855405935 29257728 5894 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 7143 5894 145 145 0 6998 0
[pid=946] vsize: 28572
Current children cumulated CPU time (s) 59.71
Current children cumulated vsize (Kb) 30696

[startup+70.0114 s]
Raw data (loadavg): 0.97 0.97 0.96 2/58 950
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 6121 0 0 0 6945 26 0 0 25 0 1 0 1855405935 29429760 5925 4294967295 134512640 135094434 3221224432 3221223056 134557585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 7185 5925 145 145 0 7040 0
[pid=946] vsize: 28740
Current children cumulated CPU time (s) 69.71
Current children cumulated vsize (Kb) 30864

[startup+80.0124 s]
Raw data (loadavg): 0.97 0.97 0.96 2/58 952
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 6153 0 0 0 7945 26 0 0 25 0 1 0 1855405935 29552640 5957 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 7215 5957 145 145 0 7070 0
[pid=946] vsize: 28860
Current children cumulated CPU time (s) 79.71
Current children cumulated vsize (Kb) 30984

[startup+90.0133 s]
Raw data (loadavg): 0.98 0.97 0.96 2/58 952
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 6186 0 0 0 8944 26 0 0 25 0 1 0 1855405935 29671424 5990 4294967295 134512640 135094434 3221224432 3221223136 134554538 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 7244 5990 145 145 0 7099 0
[pid=946] vsize: 28976
Current children cumulated CPU time (s) 89.7
Current children cumulated vsize (Kb) 31100

[startup+100.014 s]
Raw data (loadavg): 0.98 0.97 0.96 2/58 952
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 6222 0 0 0 9942 27 0 0 25 0 1 0 1855405935 29802496 6026 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 7276 6026 145 145 0 7131 0
[pid=946] vsize: 29104
Current children cumulated CPU time (s) 99.69
Current children cumulated vsize (Kb) 31228

[startup+110.015 s]
Raw data (loadavg): 0.98 0.97 0.96 2/58 952
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 6257 0 0 0 10942 27 0 0 25 0 1 0 1855405935 29929472 6061 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 7307 6061 145 145 0 7162 0
[pid=946] vsize: 29228
Current children cumulated CPU time (s) 109.69
Current children cumulated vsize (Kb) 31352

[startup+120.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 952
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 6331 0 0 0 11941 28 0 0 25 0 1 0 1855405935 30355456 6135 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 7411 6135 145 145 0 7266 0
[pid=946] vsize: 29644
Current children cumulated CPU time (s) 119.69
Current children cumulated vsize (Kb) 31768

[startup+130.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 952
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 6342 0 0 0 12941 28 0 0 25 0 1 0 1855405935 30384128 6146 4294967295 134512640 135094434 3221224432 3221223120 134554717 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 7418 6146 145 145 0 7273 0
[pid=946] vsize: 29672
Current children cumulated CPU time (s) 129.69
Current children cumulated vsize (Kb) 31796

[startup+140.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 954
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 6374 0 0 0 13941 28 0 0 25 0 1 0 1855405935 30507008 6178 4294967295 134512640 135094434 3221224432 3221223184 134559216 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 7448 6178 145 145 0 7303 0
[pid=946] vsize: 29792
Current children cumulated CPU time (s) 139.69
Current children cumulated vsize (Kb) 31916

[startup+150.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 954
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 6413 0 0 0 14941 28 0 0 25 0 1 0 1855405935 30654464 6217 4294967295 134512640 135094434 3221224432 3221223044 134563071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 7484 6217 145 145 0 7339 0
[pid=946] vsize: 29936
Current children cumulated CPU time (s) 149.69
Current children cumulated vsize (Kb) 32060

[startup+160.021 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 954
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 6448 0 0 0 15940 28 0 0 25 0 1 0 1855405935 30785536 6252 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 7516 6252 145 145 0 7371 0
[pid=946] vsize: 30064
Current children cumulated CPU time (s) 159.68
Current children cumulated vsize (Kb) 32188

[startup+170.021 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 954
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 6503 0 0 0 16940 28 0 0 25 0 1 0 1855405935 30994432 6307 4294967295 134512640 135094434 3221224432 3221223044 134563059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 7567 6307 145 145 0 7422 0
[pid=946] vsize: 30268
Current children cumulated CPU time (s) 169.68
Current children cumulated vsize (Kb) 32392

[startup+180.022 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 954
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 6547 0 0 0 17939 29 0 0 25 0 1 0 1855405935 31166464 6351 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 7609 6351 145 145 0 7464 0
[pid=946] vsize: 30436
Current children cumulated CPU time (s) 179.68
Current children cumulated vsize (Kb) 32560

[startup+190.023 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 954
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 6594 0 0 0 18939 29 0 0 25 0 1 0 1855405935 31346688 6398 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 7653 6398 145 145 0 7508 0
[pid=946] vsize: 30612
Current children cumulated CPU time (s) 189.68
Current children cumulated vsize (Kb) 32736

[startup+200.024 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 956
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 6666 0 0 0 19939 29 0 0 25 0 1 0 1855405935 31625216 6470 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 7721 6470 145 145 0 7576 0
[pid=946] vsize: 30884
Current children cumulated CPU time (s) 199.68
Current children cumulated vsize (Kb) 33008

[startup+210.025 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 956
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 6708 0 0 0 20938 30 0 0 25 0 1 0 1855405935 31784960 6512 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 7760 6512 145 145 0 7615 0
[pid=946] vsize: 31040
Current children cumulated CPU time (s) 209.68
Current children cumulated vsize (Kb) 33164

[startup+220.025 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 956
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 6756 0 0 0 21936 30 0 0 25 0 1 0 1855405935 31969280 6560 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 7805 6560 145 145 0 7660 0
[pid=946] vsize: 31220
Current children cumulated CPU time (s) 219.66
Current children cumulated vsize (Kb) 33344

[startup+230.026 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 956
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 6798 0 0 0 22936 30 0 0 25 0 1 0 1855405935 32133120 6602 4294967295 134512640 135094434 3221224432 3221223044 134563104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 7845 6602 145 145 0 7700 0
[pid=946] vsize: 31380
Current children cumulated CPU time (s) 229.66
Current children cumulated vsize (Kb) 33504

[startup+240.027 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 956
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 6857 0 0 0 23935 31 0 0 25 0 1 0 1855405935 32620544 6661 4294967295 134512640 135094434 3221224432 3221223056 134557726 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 7964 6661 145 145 0 7819 0
[pid=946] vsize: 31856
Current children cumulated CPU time (s) 239.66
Current children cumulated vsize (Kb) 33980

[startup+250.028 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 956
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 6923 0 0 0 24934 32 0 0 25 0 1 0 1855405935 32874496 6727 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 8026 6727 145 145 0 7881 0
[pid=946] vsize: 32104
Current children cumulated CPU time (s) 249.66
Current children cumulated vsize (Kb) 34228

[startup+260.029 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 958
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 6985 0 0 0 25933 32 0 0 25 0 1 0 1855405935 33116160 6789 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/946/statm): 8085 6789 145 145 0 7940 0
[pid=946] vsize: 32340
Current children cumulated CPU time (s) 259.65
Current children cumulated vsize (Kb) 34464

[startup+270.03 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 958
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 7035 0 0 0 26932 33 0 0 25 0 1 0 1855405935 33308672 6839 4294967295 134512640 135094434 3221224432 3221223120 134554676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 8132 6839 145 145 0 7987 0
[pid=946] vsize: 32528
Current children cumulated CPU time (s) 269.65
Current children cumulated vsize (Kb) 34652

[startup+280.031 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 958
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 7078 0 0 0 27931 33 0 0 25 0 1 0 1855405935 33468416 6882 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 8171 6882 145 145 0 8026 0
[pid=946] vsize: 32684
Current children cumulated CPU time (s) 279.64
Current children cumulated vsize (Kb) 34808

[startup+290.032 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 958
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 7127 0 0 0 28930 34 0 0 25 0 1 0 1855405935 33660928 6931 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 8218 6931 145 145 0 8073 0
[pid=946] vsize: 32872
Current children cumulated CPU time (s) 289.64
Current children cumulated vsize (Kb) 34996

[startup+300.034 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 958
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 7177 0 0 0 29929 34 0 0 25 0 1 0 1855405935 33853440 6981 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 8265 6981 145 145 0 8120 0
[pid=946] vsize: 33060
Current children cumulated CPU time (s) 299.63
Current children cumulated vsize (Kb) 35184

[startup+310.035 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 958
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 7221 0 0 0 30927 35 0 0 25 0 1 0 1855405935 34025472 7025 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/946/statm): 8307 7025 145 145 0 8162 0
[pid=946] vsize: 33228
Current children cumulated CPU time (s) 309.62
Current children cumulated vsize (Kb) 35352

[startup+320.036 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 960
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 7294 0 0 0 31925 36 0 0 25 0 1 0 1855405935 34312192 7098 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 8377 7098 145 145 0 8232 0
[pid=946] vsize: 33508
Current children cumulated CPU time (s) 319.61
Current children cumulated vsize (Kb) 35632

[startup+330.038 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 960
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 7402 0 0 0 32923 37 0 0 25 0 1 0 1855405935 34738176 7206 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 8481 7206 145 145 0 8336 0
[pid=946] vsize: 33924
Current children cumulated CPU time (s) 329.6
Current children cumulated vsize (Kb) 36048

[startup+340.039 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 960
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 7494 0 0 0 33921 38 0 0 25 0 1 0 1855405935 35102720 7298 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 8570 7298 145 145 0 8425 0
[pid=946] vsize: 34280
Current children cumulated CPU time (s) 339.59
Current children cumulated vsize (Kb) 36404

[startup+350.04 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 960
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 7550 0 0 0 34920 39 0 0 25 0 1 0 1855405935 35319808 7354 4294967295 134512640 135094434 3221224432 3221223044 134563071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 8623 7354 145 145 0 8478 0
[pid=946] vsize: 34492
Current children cumulated CPU time (s) 349.59
Current children cumulated vsize (Kb) 36616

[startup+360.041 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 960
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 7614 0 0 0 35919 39 0 0 25 0 1 0 1855405935 35569664 7418 4294967295 134512640 135094434 3221224432 3221223056 134557585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 8684 7418 145 145 0 8539 0
[pid=946] vsize: 34736
Current children cumulated CPU time (s) 359.58
Current children cumulated vsize (Kb) 36860

[startup+370.041 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 960
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 7675 0 0 0 36918 40 0 0 25 0 1 0 1855405935 35807232 7479 4294967295 134512640 135094434 3221224432 3221223092 134553528 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 8742 7479 145 145 0 8597 0
[pid=946] vsize: 34968
Current children cumulated CPU time (s) 369.58
Current children cumulated vsize (Kb) 37092

[startup+380.042 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 962
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 7725 0 0 0 37917 41 0 0 25 0 1 0 1855405935 36003840 7529 4294967295 134512640 135094434 3221224432 3221223052 134562986 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 8790 7529 145 145 0 8645 0
[pid=946] vsize: 35160
Current children cumulated CPU time (s) 379.58
Current children cumulated vsize (Kb) 37284

[startup+390.043 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 962
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 7772 0 0 0 38916 41 0 0 25 0 1 0 1855405935 36188160 7576 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 8835 7576 145 145 0 8690 0
[pid=946] vsize: 35340
Current children cumulated CPU time (s) 389.57
Current children cumulated vsize (Kb) 37464

[startup+400.045 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 962
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 7827 0 0 0 39915 42 0 0 25 0 1 0 1855405935 36401152 7631 4294967295 134512640 135094434 3221224432 3221223056 134557728 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 8887 7631 145 145 0 8742 0
[pid=946] vsize: 35548
Current children cumulated CPU time (s) 399.57
Current children cumulated vsize (Kb) 37672

[startup+410.046 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 962
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 7888 0 0 0 40914 43 0 0 25 0 1 0 1855405935 36642816 7692 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 8946 7692 145 145 0 8801 0
[pid=946] vsize: 35784
Current children cumulated CPU time (s) 409.57
Current children cumulated vsize (Kb) 37908

[startup+420.047 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 962
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 7942 0 0 0 41913 43 0 0 25 0 1 0 1855405935 36851712 7746 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 8997 7746 145 145 0 8852 0
[pid=946] vsize: 35988
Current children cumulated CPU time (s) 419.56
Current children cumulated vsize (Kb) 38112

[startup+430.049 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 962
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 8002 0 0 0 42913 43 0 0 25 0 1 0 1855405935 37085184 7806 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 9054 7806 145 145 0 8909 0
[pid=946] vsize: 36216
Current children cumulated CPU time (s) 429.56
Current children cumulated vsize (Kb) 38340

[startup+440.05 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 964
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 8070 0 0 0 43911 43 0 0 25 0 1 0 1855405935 37355520 7874 4294967295 134512640 135094434 3221224432 3221223080 134558037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 9120 7874 145 145 0 8975 0
[pid=946] vsize: 36480
Current children cumulated CPU time (s) 439.54
Current children cumulated vsize (Kb) 38604

[startup+450.052 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 964
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 8126 0 0 0 44911 44 0 0 25 0 1 0 1855405935 37572608 7930 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 9173 7930 145 145 0 9028 0
[pid=946] vsize: 36692
Current children cumulated CPU time (s) 449.55
Current children cumulated vsize (Kb) 38816

[startup+460.053 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 964
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 8212 0 0 0 45910 45 0 0 25 0 1 0 1855405935 37912576 8016 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 9256 8016 145 145 0 9111 0
[pid=946] vsize: 37024
Current children cumulated CPU time (s) 459.55
Current children cumulated vsize (Kb) 39148

[startup+470.054 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 964
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 8276 0 0 0 46908 45 0 0 25 0 1 0 1855405935 38686720 8080 4294967295 134512640 135094434 3221224432 3221223056 134557577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 9445 8080 145 145 0 9300 0
[pid=946] vsize: 37780
Current children cumulated CPU time (s) 469.53
Current children cumulated vsize (Kb) 39904

[startup+480.055 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 964
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 8352 0 0 0 47907 46 0 0 25 0 1 0 1855405935 38989824 8156 4294967295 134512640 135094434 3221224432 3221223088 134558279 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 9519 8156 145 145 0 9374 0
[pid=946] vsize: 38076
Current children cumulated CPU time (s) 479.53
Current children cumulated vsize (Kb) 40200

[startup+490.056 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 964
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 8437 0 0 0 48906 46 0 0 25 0 1 0 1855405935 39321600 8241 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 9600 8241 145 145 0 9455 0
[pid=946] vsize: 38400
Current children cumulated CPU time (s) 489.52
Current children cumulated vsize (Kb) 40524

[startup+500.058 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 966
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 8536 0 0 0 49904 48 0 0 25 0 1 0 1855405935 39714816 8340 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 9696 8340 145 145 0 9551 0
[pid=946] vsize: 38784
Current children cumulated CPU time (s) 499.52
Current children cumulated vsize (Kb) 40908

[startup+510.059 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 966
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 8645 0 0 0 50903 48 0 0 25 0 1 0 1855405935 40140800 8449 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 9800 8449 145 145 0 9655 0
[pid=946] vsize: 39200
Current children cumulated CPU time (s) 509.51
Current children cumulated vsize (Kb) 41324

[startup+520.059 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 966
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 8758 0 0 0 51902 49 0 0 25 0 1 0 1855405935 40587264 8562 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 9909 8562 145 145 0 9764 0
[pid=946] vsize: 39636
Current children cumulated CPU time (s) 519.51
Current children cumulated vsize (Kb) 41760

[startup+530.06 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 966
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 8863 0 0 0 52900 49 0 0 25 0 1 0 1855405935 41000960 8667 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 10010 8667 145 145 0 9865 0
[pid=946] vsize: 40040
Current children cumulated CPU time (s) 529.49
Current children cumulated vsize (Kb) 42164

[startup+540.061 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 966
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 9135 0 0 0 53896 51 0 0 25 0 1 0 1855405935 42086400 8939 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 10275 8939 145 145 0 10130 0
[pid=946] vsize: 41100
Current children cumulated CPU time (s) 539.47
Current children cumulated vsize (Kb) 43224

[startup+550.062 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 966
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 9256 0 0 0 54893 53 0 0 25 0 1 0 1855405935 42565632 9060 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 10392 9060 145 145 0 10247 0
[pid=946] vsize: 41568
Current children cumulated CPU time (s) 549.46
Current children cumulated vsize (Kb) 43692

[startup+560.063 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 968
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 9354 0 0 0 55891 53 0 0 25 0 1 0 1855405935 42954752 9158 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 10487 9158 145 145 0 10342 0
[pid=946] vsize: 41948
Current children cumulated CPU time (s) 559.44
Current children cumulated vsize (Kb) 44072

[startup+570.064 s]
Raw data (loadavg): 0.99 0.97 0.96 1/58 968
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) T 942 942 9102 0 -1 0 9479 0 0 0 56890 54 0 0 25 0 1 0 1855405935 43450368 9283 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/946/statm): 10608 9283 145 145 0 10463 0
[pid=946] vsize: 42432
Current children cumulated CPU time (s) 569.44
Current children cumulated vsize (Kb) 44556

[startup+580.101 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 968
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 9568 0 0 0 57889 54 0 0 25 0 1 0 1855405935 43802624 9372 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 10694 9372 145 145 0 10549 0
[pid=946] vsize: 42776
Current children cumulated CPU time (s) 579.43
Current children cumulated vsize (Kb) 44900

[startup+590.102 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 968
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 9676 0 0 0 58888 55 0 0 25 0 1 0 1855405935 44228608 9480 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 10798 9480 145 145 0 10653 0
[pid=946] vsize: 43192
Current children cumulated CPU time (s) 589.43
Current children cumulated vsize (Kb) 45316

[startup+600.103 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 968
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 9740 0 0 0 59887 56 0 0 25 0 1 0 1855405935 44482560 9544 4294967295 134512640 135094434 3221224432 3221223088 134558035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 10860 9544 145 145 0 10715 0
[pid=946] vsize: 43440
Current children cumulated CPU time (s) 599.43
Current children cumulated vsize (Kb) 45564

[startup+610.104 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 968
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 9861 0 0 0 60884 57 0 0 25 0 1 0 1855405935 44961792 9665 4294967295 134512640 135094434 3221224432 3221223072 134562131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 10977 9665 145 145 0 10832 0
[pid=946] vsize: 43908
Current children cumulated CPU time (s) 609.41
Current children cumulated vsize (Kb) 46032

[startup+620.104 s]
Raw data (loadavg): 0.99 0.97 0.96 2/60 970
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 9946 0 0 0 61883 58 0 0 25 0 1 0 1855405935 45297664 9750 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 11059 9750 145 145 0 10914 0
[pid=946] vsize: 44236
Current children cumulated CPU time (s) 619.41
Current children cumulated vsize (Kb) 46360

[startup+630.105 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 970
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 10028 0 0 0 62882 58 0 0 25 0 1 0 1855405935 45621248 9832 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 11138 9832 145 145 0 10993 0
[pid=946] vsize: 44552
Current children cumulated CPU time (s) 629.4
Current children cumulated vsize (Kb) 46676

[startup+640.106 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 970
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 10123 0 0 0 63880 59 0 0 25 0 1 0 1855405935 45998080 9927 4294967295 134512640 135094434 3221224432 3221223004 134690992 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 11230 9927 145 145 0 11085 0
[pid=946] vsize: 44920
Current children cumulated CPU time (s) 639.39
Current children cumulated vsize (Kb) 47044

[startup+650.107 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 970
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 10384 0 0 0 64876 61 0 0 25 0 1 0 1855405935 47042560 10188 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 11485 10188 145 145 0 11340 0
[pid=946] vsize: 45940
Current children cumulated CPU time (s) 649.37
Current children cumulated vsize (Kb) 48064

[startup+660.107 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 970
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 10485 0 0 0 65874 61 0 0 25 0 1 0 1855405935 47439872 10289 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 11582 10289 145 145 0 11437 0
[pid=946] vsize: 46328
Current children cumulated CPU time (s) 659.35
Current children cumulated vsize (Kb) 48452

[startup+670.108 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 970
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 10573 0 0 0 66873 62 0 0 25 0 1 0 1855405935 47788032 10377 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 11667 10377 145 145 0 11522 0
[pid=946] vsize: 46668
Current children cumulated CPU time (s) 669.35
Current children cumulated vsize (Kb) 48792

[startup+680.109 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 972
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 10670 0 0 0 67871 62 0 0 25 0 1 0 1855405935 48173056 10474 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 11761 10474 145 145 0 11616 0
[pid=946] vsize: 47044
Current children cumulated CPU time (s) 679.33
Current children cumulated vsize (Kb) 49168

[startup+690.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 972
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 10810 0 0 0 68869 64 0 0 25 0 1 0 1855405935 48730112 10614 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 11897 10614 145 145 0 11752 0
[pid=946] vsize: 47588
Current children cumulated CPU time (s) 689.33
Current children cumulated vsize (Kb) 49712

[startup+700.111 s]
Raw data (loadavg): 1.07 0.99 0.97 1/58 972
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) T 942 942 9102 0 -1 0 10952 0 0 0 69866 65 0 0 25 0 1 0 1855405935 49295360 10756 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/946/statm): 12035 10756 145 145 0 11890 0
[pid=946] vsize: 48140
Current children cumulated CPU time (s) 699.31
Current children cumulated vsize (Kb) 50264

[startup+710.113 s]
Raw data (loadavg): 1.06 0.99 0.97 2/58 972
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 11161 0 0 0 70862 66 0 0 25 0 1 0 1855405935 50135040 10965 4294967295 134512640 135094434 3221224432 3221223024 134556834 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 12240 10965 145 145 0 12095 0
[pid=946] vsize: 48960
Current children cumulated CPU time (s) 709.28
Current children cumulated vsize (Kb) 51084

[startup+720.114 s]
Raw data (loadavg): 1.05 0.99 0.97 2/58 972
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 11328 0 0 0 71859 68 0 0 25 0 1 0 1855405935 50798592 11132 4294967295 134512640 135094434 3221224432 3221223088 134561460 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 12402 11132 145 145 0 12257 0
[pid=946] vsize: 49608
Current children cumulated CPU time (s) 719.27
Current children cumulated vsize (Kb) 51732

[startup+730.116 s]
Raw data (loadavg): 1.04 0.99 0.97 2/58 972
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 11440 0 0 0 72857 69 0 0 25 0 1 0 1855405935 51245056 11244 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 12511 11244 145 145 0 12366 0
[pid=946] vsize: 50044
Current children cumulated CPU time (s) 729.26
Current children cumulated vsize (Kb) 52168

[startup+740.117 s]
Raw data (loadavg): 1.03 0.99 0.97 2/58 974
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 11557 0 0 0 73854 70 0 0 25 0 1 0 1855405935 51712000 11361 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 12625 11361 145 145 0 12480 0
[pid=946] vsize: 50500
Current children cumulated CPU time (s) 739.24
Current children cumulated vsize (Kb) 52624

[startup+750.119 s]
Raw data (loadavg): 1.03 0.99 0.97 2/58 974
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 11738 0 0 0 74851 71 0 0 25 0 1 0 1855405935 52432896 11542 4294967295 134512640 135094434 3221224432 3221223120 134554763 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 12801 11542 145 145 0 12656 0
[pid=946] vsize: 51204
Current children cumulated CPU time (s) 749.22
Current children cumulated vsize (Kb) 53328

[startup+760.12 s]
Raw data (loadavg): 1.02 0.99 0.97 2/58 974
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 12017 0 0 0 75847 73 0 0 25 0 1 0 1855405935 53551104 11821 4294967295 134512640 135094434 3221224432 3221223056 134557724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 13074 11821 145 145 0 12929 0
[pid=946] vsize: 52296
Current children cumulated CPU time (s) 759.2
Current children cumulated vsize (Kb) 54420

[startup+770.12 s]
Raw data (loadavg): 1.02 0.99 0.97 2/58 974
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 12206 0 0 0 76844 73 0 0 25 0 1 0 1855405935 54304768 12010 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 13258 12010 145 145 0 13113 0
[pid=946] vsize: 53032
Current children cumulated CPU time (s) 769.17
Current children cumulated vsize (Kb) 55156

[startup+780.121 s]
Raw data (loadavg): 1.02 0.99 0.97 2/58 974
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 12402 0 0 0 77841 75 0 0 25 0 1 0 1855405935 55091200 12206 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 13450 12206 145 145 0 13305 0
[pid=946] vsize: 53800
Current children cumulated CPU time (s) 779.16
Current children cumulated vsize (Kb) 55924

[startup+790.122 s]
Raw data (loadavg): 1.01 0.99 0.97 2/58 974
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 12516 0 0 0 78839 75 0 0 25 0 1 0 1855405935 55545856 12320 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 13561 12320 145 145 0 13416 0
[pid=946] vsize: 54244
Current children cumulated CPU time (s) 789.14
Current children cumulated vsize (Kb) 56368

[startup+800.123 s]
Raw data (loadavg): 1.01 0.99 0.97 2/58 976
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 12902 0 0 0 79831 79 0 0 25 0 1 0 1855405935 58142720 12706 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 14195 12706 145 145 0 14050 0
[pid=946] vsize: 56780
Current children cumulated CPU time (s) 799.1
Current children cumulated vsize (Kb) 58904

[startup+810.124 s]
Raw data (loadavg): 1.01 0.99 0.97 2/58 976
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 13025 0 0 0 80828 81 0 0 25 0 1 0 1855405935 58630144 12829 4294967295 134512640 135094434 3221224432 3221223056 134562139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 14314 12829 145 145 0 14169 0
[pid=946] vsize: 57256
Current children cumulated CPU time (s) 809.09
Current children cumulated vsize (Kb) 59380

[startup+820.124 s]
Raw data (loadavg): 1.01 0.99 0.97 2/58 976
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 13161 0 0 0 81825 82 0 0 25 0 1 0 1855405935 59170816 12965 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 14446 12965 145 145 0 14301 0
[pid=946] vsize: 57784
Current children cumulated CPU time (s) 819.07
Current children cumulated vsize (Kb) 59908

[startup+830.125 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 976
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 13418 0 0 0 82821 84 0 0 25 0 1 0 1855405935 60207104 13222 4294967295 134512640 135094434 3221224432 3221223104 134555849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 14699 13222 145 145 0 14554 0
[pid=946] vsize: 58796
Current children cumulated CPU time (s) 829.05
Current children cumulated vsize (Kb) 60920

[startup+840.126 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 976
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 13601 0 0 0 83819 85 0 0 25 0 1 0 1855405935 60944384 13405 4294967295 134512640 135094434 3221224432 3221223088 134557914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 14879 13405 145 145 0 14734 0
[pid=946] vsize: 59516
Current children cumulated CPU time (s) 839.04
Current children cumulated vsize (Kb) 61640

[startup+850.129 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 976
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 13749 0 0 0 84816 85 0 0 25 0 1 0 1855405935 61534208 13553 4294967295 134512640 135094434 3221224432 3221223076 134558261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 15023 13553 145 145 0 14878 0
[pid=946] vsize: 60092
Current children cumulated CPU time (s) 849.01
Current children cumulated vsize (Kb) 62216

[startup+860.13 s]
Raw data (loadavg): 1.00 0.99 0.97 2/60 978
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 13886 0 0 0 85814 87 0 0 25 0 1 0 1855405935 62083072 13690 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 15157 13690 145 145 0 15012 0
[pid=946] vsize: 60628
Current children cumulated CPU time (s) 859.01
Current children cumulated vsize (Kb) 62752

[startup+870.131 s]
Raw data (loadavg): 1.00 0.99 0.97 2/60 978
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 13988 0 0 0 86812 87 0 0 25 0 1 0 1855405935 62484480 13792 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 15255 13792 145 145 0 15110 0
[pid=946] vsize: 61020
Current children cumulated CPU time (s) 868.99
Current children cumulated vsize (Kb) 63144

[startup+880.133 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 978
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 14121 0 0 0 87808 89 0 0 25 0 1 0 1855405935 63016960 13925 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/946/statm): 15385 13925 145 145 0 15240 0
[pid=946] vsize: 61540
Current children cumulated CPU time (s) 878.97
Current children cumulated vsize (Kb) 63664

[startup+890.134 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 978
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 14276 0 0 0 88805 90 0 0 25 0 1 0 1855405935 63635456 14080 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 15536 14080 145 145 0 15391 0
[pid=946] vsize: 62144
Current children cumulated CPU time (s) 888.95
Current children cumulated vsize (Kb) 64268

[startup+900.135 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 978
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 14428 0 0 0 89803 91 0 0 25 0 1 0 1855405935 64241664 14232 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 15684 14232 145 145 0 15539 0
[pid=946] vsize: 62736
Current children cumulated CPU time (s) 898.94
Current children cumulated vsize (Kb) 64860

[startup+910.136 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 978
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) T 942 942 9102 0 -1 0 14536 0 0 0 90801 92 0 0 25 0 1 0 1855405935 64671744 14340 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/946/statm): 15789 14340 145 145 0 15644 0
[pid=946] vsize: 63156
Current children cumulated CPU time (s) 908.93
Current children cumulated vsize (Kb) 65280

[startup+920.137 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 980
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 14652 0 0 0 91799 93 0 0 25 0 1 0 1855405935 65138688 14456 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 15903 14456 145 145 0 15758 0
[pid=946] vsize: 63612
Current children cumulated CPU time (s) 918.92
Current children cumulated vsize (Kb) 65736

[startup+930.138 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 980
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 14918 0 0 0 92794 95 0 0 25 0 1 0 1855405935 66207744 14722 4294967295 134512640 135094434 3221224432 3221223056 134557619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 16164 14722 145 145 0 16019 0
[pid=946] vsize: 64656
Current children cumulated CPU time (s) 928.89
Current children cumulated vsize (Kb) 66780

[startup+940.139 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 980
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 15018 0 0 0 93792 96 0 0 25 0 1 0 1855405935 66605056 14822 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 16261 14822 145 145 0 16116 0
[pid=946] vsize: 65044
Current children cumulated CPU time (s) 938.88
Current children cumulated vsize (Kb) 67168

[startup+950.14 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 980
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 15128 0 0 0 94791 97 0 0 25 0 1 0 1855405935 67043328 14932 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 16368 14932 145 145 0 16223 0
[pid=946] vsize: 65472
Current children cumulated CPU time (s) 948.88
Current children cumulated vsize (Kb) 67596

[startup+960.14 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 980
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 15289 0 0 0 95788 99 0 0 25 0 1 0 1855405935 67686400 15093 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 16525 15093 145 145 0 16380 0
[pid=946] vsize: 66100
Current children cumulated CPU time (s) 958.87
Current children cumulated vsize (Kb) 68224

[startup+970.14 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 980
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 15628 0 0 0 96782 101 0 0 25 0 1 0 1855405935 69042176 15432 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 16856 15432 145 145 0 16711 0
[pid=946] vsize: 67424
Current children cumulated CPU time (s) 968.83
Current children cumulated vsize (Kb) 69548

[startup+980.141 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 982
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 15823 0 0 0 97777 104 0 0 25 0 1 0 1855405935 69824512 15627 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 17047 15627 145 145 0 16902 0
[pid=946] vsize: 68188
Current children cumulated CPU time (s) 978.81
Current children cumulated vsize (Kb) 70312

[startup+990.142 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 982
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 15964 0 0 0 98775 104 0 0 25 0 1 0 1855405935 70385664 15768 4294967295 134512640 135094434 3221224432 3221223088 134558174 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 17184 15768 145 145 0 17039 0
[pid=946] vsize: 68736
Current children cumulated CPU time (s) 988.79
Current children cumulated vsize (Kb) 70860

[startup+1000.14 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 982
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 16190 0 0 0 99772 106 0 0 25 0 1 0 1855405935 71290880 15994 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 17405 15994 145 145 0 17260 0
[pid=946] vsize: 69620
Current children cumulated CPU time (s) 998.78
Current children cumulated vsize (Kb) 71744

[startup+1010.15 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 982
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 16524 0 0 0 100766 108 0 0 25 0 1 0 1855405935 72634368 16328 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 17733 16328 145 145 0 17588 0
[pid=946] vsize: 70932
Current children cumulated CPU time (s) 1008.74
Current children cumulated vsize (Kb) 73056

[startup+1020.15 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 982
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 16653 0 0 0 101764 110 0 0 25 0 1 0 1855405935 73150464 16457 4294967295 134512640 135094434 3221224432 3221223044 134563071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 17859 16457 145 145 0 17714 0
[pid=946] vsize: 71436
Current children cumulated CPU time (s) 1018.74
Current children cumulated vsize (Kb) 73560

[startup+1030.15 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 982
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 16822 0 0 0 102761 111 0 0 25 0 1 0 1855405935 73822208 16626 4294967295 134512640 135094434 3221224432 3221223044 134563112 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 18023 16626 145 145 0 17878 0
[pid=946] vsize: 72092
Current children cumulated CPU time (s) 1028.72
Current children cumulated vsize (Kb) 74216

[startup+1040.15 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 984
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 17344 0 0 0 103753 114 0 0 25 0 1 0 1855405935 75943936 17148 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/946/statm): 18541 17148 145 145 0 18396 0
[pid=946] vsize: 74164
Current children cumulated CPU time (s) 1038.67
Current children cumulated vsize (Kb) 76288

[startup+1050.15 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 984
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 17856 0 0 0 104743 119 0 0 25 0 1 0 1855405935 78032896 17660 4294967295 134512640 135094434 3221224432 3221222080 134562846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/946/statm): 19051 17660 145 145 0 18906 0
[pid=946] vsize: 76204
Current children cumulated CPU time (s) 1048.62
Current children cumulated vsize (Kb) 78328

[startup+1060.15 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 984
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 17856 0 0 0 105742 119 0 0 25 0 1 0 1855405935 78032896 17660 4294967295 134512640 135094434 3221224432 3221223044 134563130 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/946/statm): 19051 17660 145 145 0 18906 0
[pid=946] vsize: 76204
Current children cumulated CPU time (s) 1058.61
Current children cumulated vsize (Kb) 78328

[startup+1070.15 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 984
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 17856 0 0 0 106742 119 0 0 25 0 1 0 1855405935 78032896 17660 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/946/statm): 19051 17660 145 145 0 18906 0
[pid=946] vsize: 76204
Current children cumulated CPU time (s) 1068.61
Current children cumulated vsize (Kb) 78328

[startup+1080.15 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 984
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 17856 0 0 0 107742 120 0 0 25 0 1 0 1855405935 78032896 17660 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/946/statm): 19051 17660 145 145 0 18906 0
[pid=946] vsize: 76204
Current children cumulated CPU time (s) 1078.62
Current children cumulated vsize (Kb) 78328

[startup+1090.15 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 984
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 17856 0 0 0 108742 120 0 0 25 0 1 0 1855405935 78032896 17660 4294967295 134512640 135094434 3221224432 3221223184 134559183 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/946/statm): 19051 17660 145 145 0 18906 0
[pid=946] vsize: 76204
Current children cumulated CPU time (s) 1088.62
Current children cumulated vsize (Kb) 78328

[startup+1100.16 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 986
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 17856 0 0 0 109741 121 0 0 25 0 1 0 1855405935 78032896 17660 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/946/statm): 19051 17660 145 145 0 18906 0
[pid=946] vsize: 76204
Current children cumulated CPU time (s) 1098.62
Current children cumulated vsize (Kb) 78328

[startup+1110.16 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 986
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 17856 0 0 0 110741 121 0 0 25 0 1 0 1855405935 78032896 17660 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/946/statm): 19051 17660 145 145 0 18906 0
[pid=946] vsize: 76204
Current children cumulated CPU time (s) 1108.62
Current children cumulated vsize (Kb) 78328

[startup+1120.16 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 986
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 17856 0 0 0 111740 122 0 0 25 0 1 0 1855405935 78032896 17660 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/946/statm): 19051 17660 145 145 0 18906 0
[pid=946] vsize: 76204
Current children cumulated CPU time (s) 1118.62
Current children cumulated vsize (Kb) 78328

[startup+1130.16 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 986
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 17856 0 0 0 112739 123 0 0 25 0 1 0 1855405935 78032896 17660 4294967295 134512640 135094434 3221224432 3221223044 134563112 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/946/statm): 19051 17660 145 145 0 18906 0
[pid=946] vsize: 76204
Current children cumulated CPU time (s) 1128.62
Current children cumulated vsize (Kb) 78328

[startup+1140.16 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 986
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 17856 0 0 0 113740 123 0 0 25 0 1 0 1855405935 78032896 17660 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/946/statm): 19051 17660 145 145 0 18906 0
[pid=946] vsize: 76204
Current children cumulated CPU time (s) 1138.63
Current children cumulated vsize (Kb) 78328

[startup+1150.16 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 986
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 17856 0 0 0 114739 123 0 0 25 0 1 0 1855405935 78032896 17660 4294967295 134512640 135094434 3221224432 3221223088 134558156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/946/statm): 19051 17660 145 145 0 18906 0
[pid=946] vsize: 76204
Current children cumulated CPU time (s) 1148.62
Current children cumulated vsize (Kb) 78328

[startup+1160.16 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 988
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 17856 0 0 0 115739 123 0 0 25 0 1 0 1855405935 78032896 17660 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 19051 17660 145 145 0 18906 0
[pid=946] vsize: 76204
Current children cumulated CPU time (s) 1158.62
Current children cumulated vsize (Kb) 78328

[startup+1170.17 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 988
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 17856 0 0 0 116739 123 0 0 25 0 1 0 1855405935 78032896 17660 4294967295 134512640 135094434 3221224432 3221223092 134553501 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 19051 17660 145 145 0 18906 0
[pid=946] vsize: 76204
Current children cumulated CPU time (s) 1168.62
Current children cumulated vsize (Kb) 78328

[startup+1180.17 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 988
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 17856 0 0 0 117740 123 0 0 25 0 1 0 1855405935 78032896 17660 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 19051 17660 145 145 0 18906 0
[pid=946] vsize: 76204
Current children cumulated CPU time (s) 1178.63
Current children cumulated vsize (Kb) 78328

[startup+1190.17 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 988
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 17856 0 0 0 118740 123 0 0 25 0 1 0 1855405935 78032896 17660 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 19051 17660 145 145 0 18906 0
[pid=946] vsize: 76204
Current children cumulated CPU time (s) 1188.63
Current children cumulated vsize (Kb) 78328

[startup+1200.17 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 988
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 17856 0 0 0 119740 123 0 0 25 0 1 0 1855405935 78032896 17660 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 19051 17660 145 145 0 18906 0
[pid=946] vsize: 76204
Current children cumulated CPU time (s) 1198.63
Current children cumulated vsize (Kb) 78328

[startup+1210.17 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 988
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 17856 0 0 0 120740 123 0 0 25 0 1 0 1855405935 78032896 17660 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 19051 17660 145 145 0 18906 0
[pid=946] vsize: 76204
Current children cumulated CPU time (s) 1208.63
Current children cumulated vsize (Kb) 78328



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.17 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 988
Raw data (/proc/942/stat): 942 (minisat+_script) S 941 942 9102 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855405930 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/942/statm): 531 226 485 147 0 384 0
[pid=942] vsize: 2124
Raw data (/proc/946/stat): 946 (minisat+_64-bit) R 942 942 9102 0 -1 0 17856 0 0 0 120740 123 0 0 25 0 1 0 1855405935 78032896 17660 4294967295 134512640 135094434 3221224432 3221223072 134558264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/946/statm): 19051 17660 145 145 0 18906 0
[pid=946] vsize: 76204
Current children cumulated CPU time (s) 1208.63
Current children cumulated vsize (Kb) 78328

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

Child status: 0
Real time (s): 1210.21
CPU time (s): 1208.68
CPU user time (s): 1207.41
CPU system time (s): 1.27181
CPU usage (%): 99.8739
Max. virtual memory (cumulated for all children) (Kb): 78328