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/22275/stat): 22275 (minisat+_script) R 22274 22275 19818 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1841349890 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/22275/statm): 174 3 169 147 0 27 0
[pid=22275] 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=22276
New process pid=22277
New process pid=22278
execve syscall for /bin/sed executable
One traced child (pid=22277) 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=22278) exited with status: 0
One traced child (pid=22276) exited with status: 0
New process pid=22279
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc29/normalized-rot.b.opb

[startup+10.0033 s]
Raw data (loadavg): 0.93 0.96 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 5495 0 0 0 951 22 0 0 25 0 1 0 1841349894 23855104 5424 4294967295 134512640 135094434 3221224448 3221053792 134519916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 5824 5424 145 145 0 5679 0
[pid=22279] vsize: 23296
Current children cumulated CPU time (s) 9.74
Current children cumulated vsize (Kb) 25420

[startup+20.0041 s]
Raw data (loadavg): 0.94 0.96 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 6783 0 0 0 1940 27 0 0 25 0 1 0 1841349894 30855168 6547 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22279/statm): 7533 6547 145 145 0 7388 0
[pid=22279] vsize: 30132
Current children cumulated CPU time (s) 19.68
Current children cumulated vsize (Kb) 32256

[startup+30.0049 s]
Raw data (loadavg): 0.95 0.96 0.98 1/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) T 22275 22275 19818 0 -1 0 7037 0 0 0 2934 30 0 0 25 0 1 0 1841349894 31916032 6801 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/22279/statm): 7792 6801 145 145 0 7647 0
[pid=22279] vsize: 31168
Current children cumulated CPU time (s) 29.65
Current children cumulated vsize (Kb) 33292

[startup+40.0056 s]
Raw data (loadavg): 0.95 0.96 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 7205 0 0 0 3930 32 0 0 25 0 1 0 1841349894 32595968 6969 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 7958 6969 145 145 0 7813 0
[pid=22279] vsize: 31832
Current children cumulated CPU time (s) 39.63
Current children cumulated vsize (Kb) 33956

[startup+50.0064 s]
Raw data (loadavg): 0.96 0.96 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 7549 0 0 0 4923 34 0 0 25 0 1 0 1841349894 33992704 7313 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 8299 7313 145 145 0 8154 0
[pid=22279] vsize: 33196
Current children cumulated CPU time (s) 49.58
Current children cumulated vsize (Kb) 35320

[startup+60.0072 s]
Raw data (loadavg): 0.97 0.96 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 7793 0 0 0 5920 36 0 0 25 0 1 0 1841349894 35045376 7557 4294967295 134512640 135094434 3221224448 3221223104 134557792 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 8556 7557 145 145 0 8411 0
[pid=22279] vsize: 34224
Current children cumulated CPU time (s) 59.57
Current children cumulated vsize (Kb) 36348

[startup+70.009 s]
Raw data (loadavg): 0.97 0.96 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 8034 0 0 0 6916 38 0 0 25 0 1 0 1841349894 36028416 7798 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 8796 7798 145 145 0 8651 0
[pid=22279] vsize: 35184
Current children cumulated CPU time (s) 69.55
Current children cumulated vsize (Kb) 37308

[startup+80.0098 s]
Raw data (loadavg): 0.98 0.96 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 8274 0 0 0 7910 41 0 0 25 0 1 0 1841349894 37007360 8038 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 9035 8038 145 145 0 8890 0
[pid=22279] vsize: 36140
Current children cumulated CPU time (s) 79.52
Current children cumulated vsize (Kb) 38264

[startup+90.0106 s]
Raw data (loadavg): 0.98 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 8539 0 0 0 8904 44 0 0 25 0 1 0 1841349894 38084608 8303 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22279/statm): 9298 8303 145 145 0 9153 0
[pid=22279] vsize: 37192
Current children cumulated CPU time (s) 89.49
Current children cumulated vsize (Kb) 39316

[startup+100.011 s]
Raw data (loadavg): 0.98 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 8753 0 0 0 9899 46 0 0 25 0 1 0 1841349894 38952960 8517 4294967295 134512640 135094434 3221224448 3221223040 134551908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 9510 8517 145 145 0 9365 0
[pid=22279] vsize: 38040
Current children cumulated CPU time (s) 99.46
Current children cumulated vsize (Kb) 40164

[startup+110.012 s]
Raw data (loadavg): 0.98 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 9044 0 0 0 10895 48 0 0 25 0 1 0 1841349894 39936000 8808 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 9750 8808 145 145 0 9605 0
[pid=22279] vsize: 39000
Current children cumulated CPU time (s) 109.44
Current children cumulated vsize (Kb) 41124

[startup+120.013 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 9291 0 0 0 11892 50 0 0 25 0 1 0 1841349894 40935424 9055 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 9994 9055 145 145 0 9849 0
[pid=22279] vsize: 39976
Current children cumulated CPU time (s) 119.43
Current children cumulated vsize (Kb) 42100

[startup+130.013 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 9613 0 0 0 12885 53 0 0 25 0 1 0 1841349894 42246144 9377 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 10314 9377 145 145 0 10169 0
[pid=22279] vsize: 41256
Current children cumulated CPU time (s) 129.39
Current children cumulated vsize (Kb) 43380

[startup+140.013 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 9898 0 0 0 13879 55 0 0 25 0 1 0 1841349894 43409408 9662 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 10598 9662 145 145 0 10453 0
[pid=22279] vsize: 42392
Current children cumulated CPU time (s) 139.35
Current children cumulated vsize (Kb) 44516

[startup+150.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 10244 0 0 0 14873 58 0 0 25 0 1 0 1841349894 44945408 10008 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 10973 10008 145 145 0 10828 0
[pid=22279] vsize: 43892
Current children cumulated CPU time (s) 149.32
Current children cumulated vsize (Kb) 46016

[startup+160.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 10614 0 0 0 15867 61 0 0 25 0 1 0 1841349894 46141440 10303 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 11265 10303 145 145 0 11120 0
[pid=22279] vsize: 45060
Current children cumulated CPU time (s) 159.29
Current children cumulated vsize (Kb) 47184

[startup+170.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 10614 0 0 0 16867 61 0 0 25 0 1 0 1841349894 46141440 10303 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 11265 10303 145 145 0 11120 0
[pid=22279] vsize: 45060
Current children cumulated CPU time (s) 169.29
Current children cumulated vsize (Kb) 47184

[startup+180.017 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 10616 0 0 0 17867 61 0 0 25 0 1 0 1841349894 46141440 10305 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 11265 10305 145 145 0 11120 0
[pid=22279] vsize: 45060
Current children cumulated CPU time (s) 179.29
Current children cumulated vsize (Kb) 47184

[startup+190.017 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 10618 0 0 0 18867 61 0 0 25 0 1 0 1841349894 46141440 10307 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 11265 10307 145 145 0 11120 0
[pid=22279] vsize: 45060
Current children cumulated CPU time (s) 189.29
Current children cumulated vsize (Kb) 47184

[startup+200.018 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 10810 0 0 0 19862 63 0 0 25 0 1 0 1841349894 46919680 10499 4294967295 134512640 135094434 3221224448 3221223104 134557962 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 11455 10499 145 145 0 11310 0
[pid=22279] vsize: 45820
Current children cumulated CPU time (s) 199.26
Current children cumulated vsize (Kb) 47944

[startup+210.019 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 11093 0 0 0 20858 65 0 0 25 0 1 0 1841349894 48066560 10782 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 11735 10782 145 145 0 11590 0
[pid=22279] vsize: 46940
Current children cumulated CPU time (s) 209.24
Current children cumulated vsize (Kb) 49064

[startup+220.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 11269 0 0 0 21855 66 0 0 25 0 1 0 1841349894 48783360 10958 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 11910 10959 145 145 0 11765 0
[pid=22279] vsize: 47640
Current children cumulated CPU time (s) 219.22
Current children cumulated vsize (Kb) 49764

[startup+230.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 11521 0 0 0 22850 68 0 0 25 0 1 0 1841349894 49803264 11210 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 12159 11210 145 145 0 12014 0
[pid=22279] vsize: 48636
Current children cumulated CPU time (s) 229.19
Current children cumulated vsize (Kb) 50760

[startup+240.022 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 11833 0 0 0 23844 71 0 0 25 0 1 0 1841349894 51077120 11522 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 12470 11522 145 145 0 12325 0
[pid=22279] vsize: 49880
Current children cumulated CPU time (s) 239.16
Current children cumulated vsize (Kb) 52004

[startup+250.023 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 11977 0 0 0 24841 72 0 0 25 0 1 0 1841349894 51658752 11666 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 12612 11666 145 145 0 12467 0
[pid=22279] vsize: 50448
Current children cumulated CPU time (s) 249.14
Current children cumulated vsize (Kb) 52572

[startup+260.024 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 12194 0 0 0 25836 74 0 0 25 0 1 0 1841349894 52539392 11883 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 12827 11883 145 145 0 12682 0
[pid=22279] vsize: 51308
Current children cumulated CPU time (s) 259.11
Current children cumulated vsize (Kb) 53432

[startup+270.025 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 12431 0 0 0 26831 76 0 0 25 0 1 0 1841349894 53501952 12120 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 13062 12120 145 145 0 12917 0
[pid=22279] vsize: 52248
Current children cumulated CPU time (s) 269.08
Current children cumulated vsize (Kb) 54372

[startup+280.025 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 12688 0 0 0 27826 78 0 0 25 0 1 0 1841349894 54546432 12377 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 13317 12377 145 145 0 13172 0
[pid=22279] vsize: 53268
Current children cumulated CPU time (s) 279.05
Current children cumulated vsize (Kb) 55392

[startup+290.026 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 12877 0 0 0 28822 80 0 0 25 0 1 0 1841349894 55312384 12566 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 13504 12566 145 145 0 13359 0
[pid=22279] vsize: 54016
Current children cumulated CPU time (s) 289.03
Current children cumulated vsize (Kb) 56140

[startup+300.027 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 13070 0 0 0 29817 82 0 0 25 0 1 0 1841349894 56094720 12759 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22279/statm): 13695 12759 145 145 0 13550 0
[pid=22279] vsize: 54780
Current children cumulated CPU time (s) 299
Current children cumulated vsize (Kb) 56904

[startup+310.028 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 13289 0 0 0 30814 84 0 0 25 0 1 0 1841349894 57249792 12978 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22279/statm): 13977 12978 145 145 0 13832 0
[pid=22279] vsize: 55908
Current children cumulated CPU time (s) 308.99
Current children cumulated vsize (Kb) 58032

[startup+320.03 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 13521 0 0 0 31808 87 0 0 25 0 1 0 1841349894 58191872 13210 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22279/statm): 14207 13210 145 145 0 14062 0
[pid=22279] vsize: 56828
Current children cumulated CPU time (s) 318.96
Current children cumulated vsize (Kb) 58952

[startup+330.03 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 13771 0 0 0 32802 89 0 0 25 0 1 0 1841349894 59211776 13460 4294967295 134512640 135094434 3221224448 3221222976 134783376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22279/statm): 14456 13460 145 145 0 14311 0
[pid=22279] vsize: 57824
Current children cumulated CPU time (s) 328.92
Current children cumulated vsize (Kb) 59948

[startup+340.032 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 13989 0 0 0 33799 91 0 0 25 0 1 0 1841349894 60108800 13678 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22279/statm): 14675 13678 145 145 0 14530 0
[pid=22279] vsize: 58700
Current children cumulated CPU time (s) 338.91
Current children cumulated vsize (Kb) 60824

[startup+350.033 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 14222 0 0 0 34794 93 0 0 25 0 1 0 1841349894 61050880 13911 4294967295 134512640 135094434 3221224448 3221223104 134558129 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22279/statm): 14905 13911 145 145 0 14760 0
[pid=22279] vsize: 59620
Current children cumulated CPU time (s) 348.88
Current children cumulated vsize (Kb) 61744

[startup+360.034 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 14507 0 0 0 35790 95 0 0 25 0 1 0 1841349894 62218240 14196 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22279/statm): 15190 14196 145 145 0 15045 0
[pid=22279] vsize: 60760
Current children cumulated CPU time (s) 358.86
Current children cumulated vsize (Kb) 62884

[startup+370.036 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 14730 0 0 0 36784 97 0 0 25 0 1 0 1841349894 63127552 14419 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22279/statm): 15412 14419 145 145 0 15267 0
[pid=22279] vsize: 61648
Current children cumulated CPU time (s) 368.82
Current children cumulated vsize (Kb) 63772

[startup+380.036 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 14874 0 0 0 37782 98 0 0 25 0 1 0 1841349894 63713280 14563 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22279/statm): 15555 14563 145 145 0 15410 0
[pid=22279] vsize: 62220
Current children cumulated CPU time (s) 378.81
Current children cumulated vsize (Kb) 64344

[startup+390.038 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 15028 0 0 0 38779 100 0 0 25 0 1 0 1841349894 64339968 14717 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22279/statm): 15708 14717 145 145 0 15563 0
[pid=22279] vsize: 62832
Current children cumulated CPU time (s) 388.8
Current children cumulated vsize (Kb) 64956

[startup+400.039 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 15218 0 0 0 39775 101 0 0 25 0 1 0 1841349894 65114112 14907 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22279/statm): 15897 14907 145 145 0 15752 0
[pid=22279] vsize: 63588
Current children cumulated CPU time (s) 398.77
Current children cumulated vsize (Kb) 65712

[startup+410.04 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 15485 0 0 0 40769 104 0 0 25 0 1 0 1841349894 66199552 15174 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22279/statm): 16162 15174 145 145 0 16017 0
[pid=22279] vsize: 64648
Current children cumulated CPU time (s) 408.74
Current children cumulated vsize (Kb) 66772

[startup+420.041 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 15675 0 0 0 41765 107 0 0 25 0 1 0 1841349894 66973696 15364 4294967295 134512640 135094434 3221224448 3221223040 134556999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 16351 15364 145 145 0 16206 0
[pid=22279] vsize: 65404
Current children cumulated CPU time (s) 418.73
Current children cumulated vsize (Kb) 67528

[startup+430.042 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 15877 0 0 0 42762 109 0 0 25 0 1 0 1841349894 67792896 15566 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 16551 15566 145 145 0 16406 0
[pid=22279] vsize: 66204
Current children cumulated CPU time (s) 428.72
Current children cumulated vsize (Kb) 68328

[startup+440.044 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 16073 0 0 0 43759 110 0 0 25 0 1 0 1841349894 68591616 15762 4294967295 134512640 135094434 3221224448 3221223104 134557890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 16746 15762 145 145 0 16601 0
[pid=22279] vsize: 66984
Current children cumulated CPU time (s) 438.7
Current children cumulated vsize (Kb) 69108

[startup+450.045 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) T 22275 22275 19818 0 -1 0 16285 0 0 0 44755 112 0 0 25 0 1 0 1841349894 69455872 15974 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/22279/statm): 16957 15974 145 145 0 16812 0
[pid=22279] vsize: 67828
Current children cumulated CPU time (s) 448.68
Current children cumulated vsize (Kb) 69952

[startup+460.046 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 16483 0 0 0 45752 113 0 0 25 0 1 0 1841349894 70266880 16172 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 17155 16172 145 145 0 17010 0
[pid=22279] vsize: 68620
Current children cumulated CPU time (s) 458.66
Current children cumulated vsize (Kb) 70744

[startup+470.046 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 16685 0 0 0 46748 115 0 0 25 0 1 0 1841349894 71086080 16374 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 17355 16374 145 145 0 17210 0
[pid=22279] vsize: 69420
Current children cumulated CPU time (s) 468.64
Current children cumulated vsize (Kb) 71544

[startup+480.047 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 16973 0 0 0 47742 118 0 0 25 0 1 0 1841349894 72261632 16662 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22279/statm): 17642 16662 145 145 0 17497 0
[pid=22279] vsize: 70568
Current children cumulated CPU time (s) 478.61
Current children cumulated vsize (Kb) 72692

[startup+490.049 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 17159 0 0 0 48737 120 0 0 25 0 1 0 1841349894 73015296 16848 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 17826 16848 145 145 0 17681 0
[pid=22279] vsize: 71304
Current children cumulated CPU time (s) 488.58
Current children cumulated vsize (Kb) 73428

[startup+500.05 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 17346 0 0 0 49734 122 0 0 25 0 1 0 1841349894 73777152 17035 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 18012 17035 145 145 0 17867 0
[pid=22279] vsize: 72048
Current children cumulated CPU time (s) 498.57
Current children cumulated vsize (Kb) 74172

[startup+510.05 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 17594 0 0 0 50729 124 0 0 25 0 1 0 1841349894 74784768 17283 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 18258 17283 145 145 0 18113 0
[pid=22279] vsize: 73032
Current children cumulated CPU time (s) 508.54
Current children cumulated vsize (Kb) 75156

[startup+520.051 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 17732 0 0 0 51727 125 0 0 25 0 1 0 1841349894 75345920 17421 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 18395 17421 145 145 0 18250 0
[pid=22279] vsize: 73580
Current children cumulated CPU time (s) 518.53
Current children cumulated vsize (Kb) 75704

[startup+530.052 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 17884 0 0 0 52724 126 0 0 25 0 1 0 1841349894 75964416 17573 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 18546 17573 145 145 0 18401 0
[pid=22279] vsize: 74184
Current children cumulated CPU time (s) 528.51
Current children cumulated vsize (Kb) 76308

[startup+540.054 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 18114 0 0 0 53720 128 0 0 25 0 1 0 1841349894 76898304 17803 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 18774 17803 145 145 0 18629 0
[pid=22279] vsize: 75096
Current children cumulated CPU time (s) 538.49
Current children cumulated vsize (Kb) 77220

[startup+550.055 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 18249 0 0 0 54718 128 0 0 25 0 1 0 1841349894 77451264 17938 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 18909 17938 145 145 0 18764 0
[pid=22279] vsize: 75636
Current children cumulated CPU time (s) 548.47
Current children cumulated vsize (Kb) 77760

[startup+560.055 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 18417 0 0 0 55715 130 0 0 25 0 1 0 1841349894 78127104 18106 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 19074 18106 145 145 0 18929 0
[pid=22279] vsize: 76296
Current children cumulated CPU time (s) 558.46
Current children cumulated vsize (Kb) 78420

[startup+570.056 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 18613 0 0 0 56711 131 0 0 25 0 1 0 1841349894 78925824 18302 4294967295 134512640 135094434 3221224448 3221223040 134556851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 19269 18302 145 145 0 19124 0
[pid=22279] vsize: 77076
Current children cumulated CPU time (s) 568.43
Current children cumulated vsize (Kb) 79200

[startup+580.057 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 18769 0 0 0 57706 134 0 0 25 0 1 0 1841349894 79564800 18458 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22279/statm): 19425 18458 145 145 0 19280 0
[pid=22279] vsize: 77700
Current children cumulated CPU time (s) 578.41
Current children cumulated vsize (Kb) 79824

[startup+590.059 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 18968 0 0 0 58701 136 0 0 25 0 1 0 1841349894 80375808 18657 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 19623 18657 145 145 0 19478 0
[pid=22279] vsize: 78492
Current children cumulated CPU time (s) 588.38
Current children cumulated vsize (Kb) 80616

[startup+600.06 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 19186 0 0 0 59698 137 0 0 25 0 1 0 1841349894 81260544 18875 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 19839 18875 145 145 0 19694 0
[pid=22279] vsize: 79356
Current children cumulated CPU time (s) 598.36
Current children cumulated vsize (Kb) 81480

[startup+610.06 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 19373 0 0 0 60695 138 0 0 25 0 1 0 1841349894 82022400 19062 4294967295 134512640 135094434 3221224448 3221223072 134557585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 20025 19062 145 145 0 19880 0
[pid=22279] vsize: 80100
Current children cumulated CPU time (s) 608.34
Current children cumulated vsize (Kb) 82224

[startup+620.062 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 19519 0 0 0 61692 139 0 0 25 0 1 0 1841349894 82616320 19208 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 20170 19208 145 145 0 20025 0
[pid=22279] vsize: 80680
Current children cumulated CPU time (s) 618.32
Current children cumulated vsize (Kb) 82804

[startup+630.063 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 19649 0 0 0 62689 140 0 0 25 0 1 0 1841349894 83144704 19338 4294967295 134512640 135094434 3221224448 3221223072 134557598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 20299 19338 145 145 0 20154 0
[pid=22279] vsize: 81196
Current children cumulated CPU time (s) 628.3
Current children cumulated vsize (Kb) 83320

[startup+640.064 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 19828 0 0 0 63686 142 0 0 25 0 1 0 1841349894 83873792 19517 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 20477 19517 145 145 0 20332 0
[pid=22279] vsize: 81908
Current children cumulated CPU time (s) 638.29
Current children cumulated vsize (Kb) 84032

[startup+650.064 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 20037 0 0 0 64681 144 0 0 25 0 1 0 1841349894 84721664 19726 4294967295 134512640 135094434 3221224448 3221223072 134557585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 20684 19726 145 145 0 20539 0
[pid=22279] vsize: 82736
Current children cumulated CPU time (s) 648.26
Current children cumulated vsize (Kb) 84860

[startup+660.065 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 20255 0 0 0 65677 146 0 0 25 0 1 0 1841349894 85610496 19944 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 20901 19944 145 145 0 20756 0
[pid=22279] vsize: 83604
Current children cumulated CPU time (s) 658.24
Current children cumulated vsize (Kb) 85728

[startup+670.066 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 20431 0 0 0 66674 147 0 0 25 0 1 0 1841349894 86327296 20120 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 21076 20120 145 145 0 20931 0
[pid=22279] vsize: 84304
Current children cumulated CPU time (s) 668.22
Current children cumulated vsize (Kb) 86428

[startup+680.067 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 20649 0 0 0 67669 149 0 0 25 0 1 0 1841349894 87212032 20338 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 21292 20338 145 145 0 21147 0
[pid=22279] vsize: 85168
Current children cumulated CPU time (s) 678.19
Current children cumulated vsize (Kb) 87292

[startup+690.069 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 20870 0 0 0 68665 151 0 0 25 0 1 0 1841349894 88121344 20559 4294967295 134512640 135094434 3221224448 3221223092 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 21514 20559 145 145 0 21369 0
[pid=22279] vsize: 86056
Current children cumulated CPU time (s) 688.17
Current children cumulated vsize (Kb) 88180

[startup+700.069 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 21102 0 0 0 69661 153 0 0 25 0 1 0 1841349894 89059328 20791 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 21743 20791 145 145 0 21598 0
[pid=22279] vsize: 86972
Current children cumulated CPU time (s) 698.15
Current children cumulated vsize (Kb) 89096

[startup+710.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 21304 0 0 0 70657 154 0 0 25 0 1 0 1841349894 89890816 20993 4294967295 134512640 135094434 3221224448 3221223040 134556840 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 21946 20993 145 145 0 21801 0
[pid=22279] vsize: 87784
Current children cumulated CPU time (s) 708.12
Current children cumulated vsize (Kb) 89908

[startup+720.071 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 21471 0 0 0 71653 157 0 0 25 0 1 0 1841349894 90570752 21160 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22279/statm): 22112 21160 145 145 0 21967 0
[pid=22279] vsize: 88448
Current children cumulated CPU time (s) 718.11
Current children cumulated vsize (Kb) 90572

[startup+730.073 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 21629 0 0 0 72649 158 0 0 25 0 1 0 1841349894 91213824 21318 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 22269 21318 145 145 0 22124 0
[pid=22279] vsize: 89076
Current children cumulated CPU time (s) 728.08
Current children cumulated vsize (Kb) 91200

[startup+740.075 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 21906 0 0 0 73644 161 0 0 25 0 1 0 1841349894 92340224 21595 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 22544 21595 145 145 0 22399 0
[pid=22279] vsize: 90176
Current children cumulated CPU time (s) 738.06
Current children cumulated vsize (Kb) 92300

[startup+750.075 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 22137 0 0 0 74639 163 0 0 25 0 1 0 1841349894 93282304 21826 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 22774 21826 145 145 0 22629 0
[pid=22279] vsize: 91096
Current children cumulated CPU time (s) 748.03
Current children cumulated vsize (Kb) 93220

[startup+760.076 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 22436 0 0 0 75633 166 0 0 25 0 1 0 1841349894 95023104 22125 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 23199 22125 145 145 0 23054 0
[pid=22279] vsize: 92796
Current children cumulated CPU time (s) 758
Current children cumulated vsize (Kb) 94920

[startup+770.077 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 22609 0 0 0 76629 167 0 0 25 0 1 0 1841349894 95727616 22298 4294967295 134512640 135094434 3221224448 3221223120 134555811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 23371 22298 145 145 0 23226 0
[pid=22279] vsize: 93484
Current children cumulated CPU time (s) 767.97
Current children cumulated vsize (Kb) 95608

[startup+780.078 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 22785 0 0 0 77627 168 0 0 25 0 1 0 1841349894 96444416 22474 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 23546 22474 145 145 0 23401 0
[pid=22279] vsize: 94184
Current children cumulated CPU time (s) 777.96
Current children cumulated vsize (Kb) 96308

[startup+790.078 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 23002 0 0 0 78623 169 0 0 25 0 1 0 1841349894 97325056 22691 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 23761 22691 145 145 0 23616 0
[pid=22279] vsize: 95044
Current children cumulated CPU time (s) 787.93
Current children cumulated vsize (Kb) 97168

[startup+800.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 23212 0 0 0 79620 171 0 0 25 0 1 0 1841349894 98181120 22901 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 23970 22901 145 145 0 23825 0
[pid=22279] vsize: 95880
Current children cumulated CPU time (s) 797.92
Current children cumulated vsize (Kb) 98004

[startup+810.081 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 23449 0 0 0 80615 173 0 0 25 0 1 0 1841349894 99135488 23138 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 24203 23138 145 145 0 24058 0
[pid=22279] vsize: 96812
Current children cumulated CPU time (s) 807.89
Current children cumulated vsize (Kb) 98936

[startup+820.082 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 23607 0 0 0 81612 175 0 0 25 0 1 0 1841349894 99778560 23296 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 24360 23296 145 145 0 24215 0
[pid=22279] vsize: 97440
Current children cumulated CPU time (s) 817.88
Current children cumulated vsize (Kb) 99564

[startup+830.083 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 23761 0 0 0 82609 176 0 0 25 0 1 0 1841349894 100405248 23450 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 24513 23450 145 145 0 24368 0
[pid=22279] vsize: 98052
Current children cumulated CPU time (s) 827.86
Current children cumulated vsize (Kb) 100176

[startup+840.084 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 23964 0 0 0 83607 177 0 0 25 0 1 0 1841349894 101232640 23653 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 24715 23653 145 145 0 24570 0
[pid=22279] vsize: 98860
Current children cumulated CPU time (s) 837.85
Current children cumulated vsize (Kb) 100984

[startup+850.085 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 24162 0 0 0 84603 178 0 0 25 0 1 0 1841349894 102039552 23851 4294967295 134512640 135094434 3221224448 3221223136 134554796 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 24912 23851 145 145 0 24767 0
[pid=22279] vsize: 99648
Current children cumulated CPU time (s) 847.82
Current children cumulated vsize (Kb) 101772

[startup+860.086 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 24361 0 0 0 85599 180 0 0 25 0 1 0 1841349894 102850560 24050 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 25110 24050 145 145 0 24965 0
[pid=22279] vsize: 100440
Current children cumulated CPU time (s) 857.8
Current children cumulated vsize (Kb) 102564

[startup+870.088 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 24605 0 0 0 86594 182 0 0 25 0 1 0 1841349894 103845888 24294 4294967295 134512640 135094434 3221224448 3221223104 134557928 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 25353 24294 145 145 0 25208 0
[pid=22279] vsize: 101412
Current children cumulated CPU time (s) 867.77
Current children cumulated vsize (Kb) 103536

[startup+880.089 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 24779 0 0 0 87591 184 0 0 25 0 1 0 1841349894 104554496 24468 4294967295 134512640 135094434 3221224448 3221223072 134557568 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 25526 24468 145 145 0 25381 0
[pid=22279] vsize: 102104
Current children cumulated CPU time (s) 877.76
Current children cumulated vsize (Kb) 104228

[startup+890.089 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 24988 0 0 0 88587 186 0 0 25 0 1 0 1841349894 105414656 24677 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 25736 24677 145 145 0 25591 0
[pid=22279] vsize: 102944
Current children cumulated CPU time (s) 887.74
Current children cumulated vsize (Kb) 105068

[startup+900.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 25155 0 0 0 89584 187 0 0 25 0 1 0 1841349894 106098688 24844 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 25903 24844 145 145 0 25758 0
[pid=22279] vsize: 103612
Current children cumulated CPU time (s) 897.72
Current children cumulated vsize (Kb) 105736

[startup+910.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 25356 0 0 0 90581 189 0 0 25 0 1 0 1841349894 106926080 25045 4294967295 134512640 135094434 3221224448 3221223072 134557636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 26105 25045 145 145 0 25960 0
[pid=22279] vsize: 104420
Current children cumulated CPU time (s) 907.71
Current children cumulated vsize (Kb) 106544

[startup+920.091 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 25549 0 0 0 91578 190 0 0 25 0 1 0 1841349894 107720704 25238 4294967295 134512640 135094434 3221224448 3221223072 134557574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 26299 25238 145 145 0 26154 0
[pid=22279] vsize: 105196
Current children cumulated CPU time (s) 917.69
Current children cumulated vsize (Kb) 107320

[startup+930.091 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 25751 0 0 0 92574 192 0 0 25 0 1 0 1841349894 108544000 25440 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 26500 25440 145 145 0 26355 0
[pid=22279] vsize: 106000
Current children cumulated CPU time (s) 927.67
Current children cumulated vsize (Kb) 108124

[startup+940.092 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 25981 0 0 0 93570 194 0 0 25 0 1 0 1841349894 109477888 25670 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 26728 25670 145 145 0 26583 0
[pid=22279] vsize: 106912
Current children cumulated CPU time (s) 937.65
Current children cumulated vsize (Kb) 109036

[startup+950.093 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 26176 0 0 0 94565 196 0 0 25 0 1 0 1841349894 110268416 25865 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 26921 25865 145 145 0 26776 0
[pid=22279] vsize: 107684
Current children cumulated CPU time (s) 947.62
Current children cumulated vsize (Kb) 109808

[startup+960.094 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 26388 0 0 0 95561 198 0 0 25 0 1 0 1841349894 111132672 26077 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 27132 26077 145 145 0 26987 0
[pid=22279] vsize: 108528
Current children cumulated CPU time (s) 957.6
Current children cumulated vsize (Kb) 110652

[startup+970.095 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 26574 0 0 0 96556 200 0 0 25 0 1 0 1841349894 111890432 26263 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 27317 26263 145 145 0 27172 0
[pid=22279] vsize: 109268
Current children cumulated CPU time (s) 967.57
Current children cumulated vsize (Kb) 111392

[startup+980.095 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 26777 0 0 0 97552 202 0 0 25 0 1 0 1841349894 112726016 26466 4294967295 134512640 135094434 3221224448 3221223040 134556817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 27521 26466 145 145 0 27376 0
[pid=22279] vsize: 110084
Current children cumulated CPU time (s) 977.55
Current children cumulated vsize (Kb) 112208

[startup+990.096 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 26973 0 0 0 98548 204 0 0 25 0 1 0 1841349894 113524736 26662 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 27716 26662 145 145 0 27571 0
[pid=22279] vsize: 110864
Current children cumulated CPU time (s) 987.53
Current children cumulated vsize (Kb) 112988

[startup+1000.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 27156 0 0 0 99545 205 0 0 25 0 1 0 1841349894 114290688 26845 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 27903 26845 145 145 0 27758 0
[pid=22279] vsize: 111612
Current children cumulated CPU time (s) 997.51
Current children cumulated vsize (Kb) 113736

[startup+1010.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 27328 0 0 0 100541 208 0 0 25 0 1 0 1841349894 114999296 27017 4294967295 134512640 135094434 3221224448 3221223104 134558022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 28076 27017 145 145 0 27931 0
[pid=22279] vsize: 112304
Current children cumulated CPU time (s) 1007.5
Current children cumulated vsize (Kb) 114428

[startup+1020.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 27514 0 0 0 101537 210 0 0 25 0 1 0 1841349894 115765248 27203 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 28263 27203 145 145 0 28118 0
[pid=22279] vsize: 113052
Current children cumulated CPU time (s) 1017.48
Current children cumulated vsize (Kb) 115176

[startup+1030.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 27702 0 0 0 102533 211 0 0 25 0 1 0 1841349894 116531200 27391 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 28450 27391 145 145 0 28305 0
[pid=22279] vsize: 113800
Current children cumulated CPU time (s) 1027.45
Current children cumulated vsize (Kb) 115924

[startup+1040.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 27847 0 0 0 103530 213 0 0 25 0 1 0 1841349894 117121024 27536 4294967295 134512640 135094434 3221224448 3221223136 134554705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 28594 27536 145 145 0 28449 0
[pid=22279] vsize: 114376
Current children cumulated CPU time (s) 1037.44
Current children cumulated vsize (Kb) 116500

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 28002 0 0 0 104527 214 0 0 25 0 1 0 1841349894 117760000 27691 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 28750 27691 145 145 0 28605 0
[pid=22279] vsize: 115000
Current children cumulated CPU time (s) 1047.42
Current children cumulated vsize (Kb) 117124

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 28180 0 0 0 105524 215 0 0 25 0 1 0 1841349894 118480896 27869 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 28926 27869 145 145 0 28781 0
[pid=22279] vsize: 115704
Current children cumulated CPU time (s) 1057.4
Current children cumulated vsize (Kb) 117828

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 28432 0 0 0 106520 218 0 0 25 0 1 0 1841349894 119529472 28121 4294967295 134512640 135094434 3221224448 3221223104 134557872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 29182 28121 145 145 0 29037 0
[pid=22279] vsize: 116728
Current children cumulated CPU time (s) 1067.39
Current children cumulated vsize (Kb) 118852

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 28636 0 0 0 107515 220 0 0 25 0 1 0 1841349894 120344576 28325 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22279/statm): 29381 28325 145 145 0 29236 0
[pid=22279] vsize: 117524
Current children cumulated CPU time (s) 1077.36
Current children cumulated vsize (Kb) 119648

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 28766 0 0 0 108512 221 0 0 25 0 1 0 1841349894 120872960 28455 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 29510 28455 145 145 0 29365 0
[pid=22279] vsize: 118040
Current children cumulated CPU time (s) 1087.34
Current children cumulated vsize (Kb) 120164

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 28909 0 0 0 109508 223 0 0 25 0 1 0 1841349894 121454592 28598 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 29652 28598 145 145 0 29507 0
[pid=22279] vsize: 118608
Current children cumulated CPU time (s) 1097.32
Current children cumulated vsize (Kb) 120732

[startup+1110.11 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 29055 0 0 0 110506 224 0 0 25 0 1 0 1841349894 122044416 28744 4294967295 134512640 135094434 3221224448 3221223104 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 29796 28744 145 145 0 29651 0
[pid=22279] vsize: 119184
Current children cumulated CPU time (s) 1107.31
Current children cumulated vsize (Kb) 121308

[startup+1120.11 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 29194 0 0 0 111503 225 0 0 25 0 1 0 1841349894 122613760 28883 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 29935 28883 145 145 0 29790 0
[pid=22279] vsize: 119740
Current children cumulated CPU time (s) 1117.29
Current children cumulated vsize (Kb) 121864

[startup+1130.11 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 29337 0 0 0 112501 226 0 0 25 0 1 0 1841349894 123195392 29026 4294967295 134512640 135094434 3221224448 3221223088 134558264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 30077 29026 145 145 0 29932 0
[pid=22279] vsize: 120308
Current children cumulated CPU time (s) 1127.28
Current children cumulated vsize (Kb) 122432

[startup+1140.11 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 29473 0 0 0 113499 227 0 0 25 0 1 0 1841349894 123748352 29162 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 30212 29162 145 145 0 30067 0
[pid=22279] vsize: 120848
Current children cumulated CPU time (s) 1137.27
Current children cumulated vsize (Kb) 122972

[startup+1150.11 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 29626 0 0 0 114496 229 0 0 25 0 1 0 1841349894 124375040 29315 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 30365 29315 145 145 0 30220 0
[pid=22279] vsize: 121460
Current children cumulated CPU time (s) 1147.26
Current children cumulated vsize (Kb) 123584

[startup+1160.11 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 29829 0 0 0 115492 231 0 0 25 0 1 0 1841349894 125218816 29518 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 30571 29518 145 145 0 30426 0
[pid=22279] vsize: 122284
Current children cumulated CPU time (s) 1157.24
Current children cumulated vsize (Kb) 124408

[startup+1170.11 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 30075 0 0 0 116488 233 0 0 25 0 1 0 1841349894 126218240 29764 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 30815 29764 145 145 0 30670 0
[pid=22279] vsize: 123260
Current children cumulated CPU time (s) 1167.22
Current children cumulated vsize (Kb) 125384

[startup+1180.11 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 30340 0 0 0 117485 234 0 0 25 0 1 0 1841349894 127299584 30029 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 31079 30029 145 145 0 30934 0
[pid=22279] vsize: 124316
Current children cumulated CPU time (s) 1177.2
Current children cumulated vsize (Kb) 126440

[startup+1190.11 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 30584 0 0 0 118480 237 0 0 25 0 1 0 1841349894 128290816 30273 4294967295 134512640 135094434 3221224448 3221223040 134557196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 31321 30273 145 145 0 31176 0
[pid=22279] vsize: 125284
Current children cumulated CPU time (s) 1187.18
Current children cumulated vsize (Kb) 127408

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 30863 0 0 0 119476 239 0 0 25 0 1 0 1841349894 129429504 30552 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22279/statm): 31599 30552 145 145 0 31454 0
[pid=22279] vsize: 126396
Current children cumulated CPU time (s) 1197.16
Current children cumulated vsize (Kb) 128520

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 31135 0 0 0 120470 242 0 0 25 0 1 0 1841349894 130535424 30824 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 31869 30824 145 145 0 31724 0
[pid=22279] vsize: 127476
Current children cumulated CPU time (s) 1207.13
Current children cumulated vsize (Kb) 129600



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22279
Raw data (/proc/22275/stat): 22275 (minisat+_script) S 22274 22275 19818 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1841349890 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22275/statm): 531 226 485 147 0 384 0
[pid=22275] vsize: 2124
Raw data (/proc/22279/stat): 22279 (minisat+_64-bit) R 22275 22275 19818 0 -1 0 31135 0 0 0 120470 242 0 0 25 0 1 0 1841349894 130535424 30824 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22279/statm): 31869 30824 145 145 0 31724 0
[pid=22279] vsize: 127476
Current children cumulated CPU time (s) 1207.13
Current children cumulated vsize (Kb) 129600

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

Child status: 10
Real time (s): 1210.18
CPU time (s): 1207.19
CPU user time (s): 1204.7
CPU system time (s): 2.48062
CPU usage (%): 99.7525
Max. virtual memory (cumulated for all children) (Kb): 129600