PB'05 competition: run trace

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/20966/stat): 20966 (minisat+_script) R 20965 20966 10120 0 -1 0 18 0 0 0 0 0 0 0 22 0 1 0 1740347058 712704 3 4294967295 134512640 135087896 3221221664 3221221664 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/20966/statm): 174 3 169 147 0 27 0
[pid=20966] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file /usr/local/intel-8.0-20031016/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /usr/local/intel-8.0-20031016/lib/tls/i686/libtermcap.so.2
open syscall for file /usr/local/intel-8.0-20031016/lib/tls/mmx/libtermcap.so.2
open syscall for file /usr/local/intel-8.0-20031016/lib/tls/libtermcap.so.2
open syscall for file /usr/local/intel-8.0-20031016/lib/i686/mmx/libtermcap.so.2
open syscall for file /usr/local/intel-8.0-20031016/lib/i686/libtermcap.so.2
open syscall for file /usr/local/intel-8.0-20031016/lib/mmx/libtermcap.so.2
open syscall for file /usr/local/intel-8.0-20031016/lib/libtermcap.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/i686/libtermcap.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/mmx/libtermcap.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/libtermcap.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/i686/mmx/libtermcap.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/i686/libtermcap.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/mmx/libtermcap.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/libtermcap.so.2
open syscall for file /usr/local/globus-2.4.3/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /usr/local/globus-2.4.3/lib/tls/i686/libtermcap.so.2
open syscall for file /usr/local/globus-2.4.3/lib/tls/mmx/libtermcap.so.2
open syscall for file /usr/local/globus-2.4.3/lib/tls/libtermcap.so.2
open syscall for file /usr/local/globus-2.4.3/lib/i686/mmx/libtermcap.so.2
open syscall for file /usr/local/globus-2.4.3/lib/i686/libtermcap.so.2
open syscall for file /usr/local/globus-2.4.3/lib/mmx/libtermcap.so.2
open syscall for file /usr/local/globus-2.4.3/lib/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 /usr/local/intel-8.0-20031016/lib/libdl.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/libdl.so.2
open syscall for file /usr/local/globus-2.4.3/lib/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 /usr/local/intel-8.0-20031016/lib/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/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 /usr/lib/locale/locale-archive
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
open syscall for file /usr/lib/gconv/gconv-modules.cache
New process pid=20967
New process pid=20968
New process pid=20969
execve syscall for /bin/sed executable
One traced child (pid=20968) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file /usr/local/intel-8.0-20031016/lib/tls/i686/mmx/libc.so.6
open syscall for file /usr/local/intel-8.0-20031016/lib/tls/i686/libc.so.6
open syscall for file /usr/local/intel-8.0-20031016/lib/tls/mmx/libc.so.6
open syscall for file /usr/local/intel-8.0-20031016/lib/tls/libc.so.6
open syscall for file /usr/local/intel-8.0-20031016/lib/i686/mmx/libc.so.6
open syscall for file /usr/local/intel-8.0-20031016/lib/i686/libc.so.6
open syscall for file /usr/local/intel-8.0-20031016/lib/mmx/libc.so.6
open syscall for file /usr/local/intel-8.0-20031016/lib/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/i686/mmx/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/i686/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/mmx/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/i686/mmx/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/i686/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/mmx/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/tls/i686/mmx/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/tls/i686/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/tls/mmx/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/tls/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/i686/mmx/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/i686/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/mmx/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/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
open syscall for file /usr/lib/locale/locale-archive
open syscall for file /usr/lib/gconv/gconv-modules.cache
One traced child (pid=20969) exited with status: 0
One traced child (pid=20967) exited with status: 0
New process pid=20970
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-opt1217.opb

[startup+10.0032 s]
Raw data (loadavg): 1.07 1.01 0.93 2/56 20970
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 1776 0 0 0 976 7 0 0 25 0 1 0 1740347064 7708672 1723 4294967295 134512640 135094434 3221221600 3221220224 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 1882 1723 145 145 0 1737 0
[pid=20970] vsize: 7528
Current children cumulated CPU time (s) 9.84
Current children cumulated vsize (Kb) 11724

[startup+20.004 s]
Raw data (loadavg): 1.06 1.01 0.93 2/56 20970
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 2079 0 0 0 1972 9 0 0 25 0 1 0 1740347064 8966144 2026 4294967295 134512640 135094434 3221221600 3221220256 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 2189 2026 145 145 0 2044 0
[pid=20970] vsize: 8756
Current children cumulated CPU time (s) 19.82
Current children cumulated vsize (Kb) 12952

[startup+30.0047 s]
Raw data (loadavg): 1.05 1.01 0.93 2/56 20970
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 2607 0 0 0 2963 14 0 0 25 0 1 0 1740347064 11112448 2554 4294967295 134512640 135094434 3221221600 3221220192 134557319 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 2713 2554 145 145 0 2568 0
[pid=20970] vsize: 10852
Current children cumulated CPU time (s) 29.78
Current children cumulated vsize (Kb) 15048

[startup+40.0046 s]
Raw data (loadavg): 1.04 1.01 0.93 2/56 20970
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 3064 0 0 0 3954 19 0 0 25 0 1 0 1740347064 13029376 3011 4294967295 134512640 135094434 3221221600 3221220224 134562057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20970/statm): 3181 3011 145 145 0 3036 0
[pid=20970] vsize: 12724
Current children cumulated CPU time (s) 39.74
Current children cumulated vsize (Kb) 16920

[startup+50.0063 s]
Raw data (loadavg): 1.04 1.01 0.93 2/56 20970
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 3382 0 0 0 4948 22 0 0 25 0 1 0 1740347064 14319616 3329 4294967295 134512640 135094434 3221221600 3221220192 134557416 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20970/statm): 3496 3329 145 145 0 3351 0
[pid=20970] vsize: 13984
Current children cumulated CPU time (s) 49.71
Current children cumulated vsize (Kb) 18180

[startup+60.0071 s]
Raw data (loadavg): 1.03 1.01 0.93 2/56 20970
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 3667 0 0 0 5943 25 0 0 25 0 1 0 1740347064 15470592 3614 4294967295 134512640 135094434 3221221600 3221220256 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20970/statm): 3777 3614 145 145 0 3632 0
[pid=20970] vsize: 15108
Current children cumulated CPU time (s) 59.69
Current children cumulated vsize (Kb) 19304

[startup+70.0079 s]
Raw data (loadavg): 1.02 1.01 0.93 2/56 20970
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 3953 0 0 0 6937 28 0 0 25 0 1 0 1740347064 16625664 3900 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20970/statm): 4059 3900 145 145 0 3914 0
[pid=20970] vsize: 16236
Current children cumulated CPU time (s) 69.66
Current children cumulated vsize (Kb) 20432

[startup+80.0097 s]
Raw data (loadavg): 1.02 1.01 0.93 2/56 20970
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 4209 0 0 0 7932 30 0 0 25 0 1 0 1740347064 17793024 4156 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20970/statm): 4344 4156 145 145 0 4199 0
[pid=20970] vsize: 17376
Current children cumulated CPU time (s) 79.63
Current children cumulated vsize (Kb) 21572

[startup+90.0105 s]
Raw data (loadavg): 1.02 1.01 0.93 2/56 20970
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 4492 0 0 0 8927 33 0 0 25 0 1 0 1740347064 18939904 4439 4294967295 134512640 135094434 3221221600 3221220192 134557429 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20970/statm): 4624 4439 145 145 0 4479 0
[pid=20970] vsize: 18496
Current children cumulated CPU time (s) 89.61
Current children cumulated vsize (Kb) 22692

[startup+100.011 s]
Raw data (loadavg): 1.01 1.01 0.93 2/56 20970
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 5047 0 0 0 9918 37 0 0 25 0 1 0 1740347064 21196800 4994 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20970/statm): 5175 4994 145 145 0 5030 0
[pid=20970] vsize: 20700
Current children cumulated CPU time (s) 99.56
Current children cumulated vsize (Kb) 24896

[startup+110.012 s]
Raw data (loadavg): 1.01 1.00 0.93 2/56 20970
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 5966 0 0 0 10901 44 0 0 25 0 1 0 1740347064 24948736 5913 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20970/statm): 6091 5913 145 145 0 5946 0
[pid=20970] vsize: 24364
Current children cumulated CPU time (s) 109.46
Current children cumulated vsize (Kb) 28560

[startup+120.013 s]
Raw data (loadavg): 1.01 1.00 0.93 2/56 20970
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 6764 0 0 0 11888 48 0 0 25 0 1 0 1740347064 28213248 6711 4294967295 134512640 135094434 3221221600 3221220256 134558218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20970/statm): 6888 6711 145 145 0 6743 0
[pid=20970] vsize: 27552
Current children cumulated CPU time (s) 119.37
Current children cumulated vsize (Kb) 31748

[startup+130.014 s]
Raw data (loadavg): 1.01 1.00 0.93 2/56 20970
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 7413 0 0 0 12878 53 0 0 25 0 1 0 1740347064 30863360 7360 4294967295 134512640 135094434 3221221600 3221220272 134556252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20970/statm): 7535 7360 145 145 0 7390 0
[pid=20970] vsize: 30140
Current children cumulated CPU time (s) 129.32
Current children cumulated vsize (Kb) 34336

[startup+140.014 s]
Raw data (loadavg): 1.01 1.00 0.93 2/56 20970
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 8031 0 0 0 13867 57 0 0 25 0 1 0 1740347064 33386496 7978 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20970/statm): 8151 7978 145 145 0 8006 0
[pid=20970] vsize: 32604
Current children cumulated CPU time (s) 139.25
Current children cumulated vsize (Kb) 36800

[startup+150.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20970
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 8570 0 0 0 14859 61 0 0 25 0 1 0 1740347064 35594240 8517 4294967295 134512640 135094434 3221221600 3221220192 134556826 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20970/statm): 8690 8517 145 145 0 8545 0
[pid=20970] vsize: 34760
Current children cumulated CPU time (s) 149.21
Current children cumulated vsize (Kb) 38956

[startup+160.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20970
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 8570 0 0 0 15858 62 0 0 25 0 1 0 1740347064 35594240 8517 4294967295 134512640 135094434 3221221600 3221220192 134557202 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20970/statm): 8690 8517 145 145 0 8545 0
[pid=20970] vsize: 34760
Current children cumulated CPU time (s) 159.21
Current children cumulated vsize (Kb) 38956

[startup+170.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20970
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 8571 0 0 0 16858 62 0 0 25 0 1 0 1740347064 35594240 8518 4294967295 134512640 135094434 3221221600 3221220256 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20970/statm): 8690 8518 145 145 0 8545 0
[pid=20970] vsize: 34760
Current children cumulated CPU time (s) 169.21
Current children cumulated vsize (Kb) 38956

[startup+180.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20970
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 8571 0 0 0 17858 62 0 0 25 0 1 0 1740347064 35594240 8518 4294967295 134512640 135094434 3221221600 3221220256 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20970/statm): 8690 8518 145 145 0 8545 0
[pid=20970] vsize: 34760
Current children cumulated CPU time (s) 179.21
Current children cumulated vsize (Kb) 38956

[startup+190.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20970
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 8571 0 0 0 18857 63 0 0 25 0 1 0 1740347064 35594240 8518 4294967295 134512640 135094434 3221221600 3221220272 134555570 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20970/statm): 8690 8518 145 145 0 8545 0
[pid=20970] vsize: 34760
Current children cumulated CPU time (s) 189.21
Current children cumulated vsize (Kb) 38956

[startup+200.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20970
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 8571 0 0 0 19856 64 0 0 25 0 1 0 1740347064 35594240 8518 4294967295 134512640 135094434 3221221600 3221220256 134558392 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20970/statm): 8690 8518 145 145 0 8545 0
[pid=20970] vsize: 34760
Current children cumulated CPU time (s) 199.21
Current children cumulated vsize (Kb) 38956

[startup+210.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20970
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 9004 0 0 0 20848 67 0 0 25 0 1 0 1740347064 37376000 8951 4294967295 134512640 135094434 3221221600 3221220256 134557875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20970/statm): 9125 8951 145 145 0 8980 0
[pid=20970] vsize: 36500
Current children cumulated CPU time (s) 209.16
Current children cumulated vsize (Kb) 40696

[startup+220.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20970
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 9544 0 0 0 21839 72 0 0 25 0 1 0 1740347064 39587840 9491 4294967295 134512640 135094434 3221221600 3221220192 134556878 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 9665 9491 145 145 0 9520 0
[pid=20970] vsize: 38660
Current children cumulated CPU time (s) 219.12
Current children cumulated vsize (Kb) 42856

[startup+230.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20972
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 10246 0 0 0 22828 76 0 0 25 0 1 0 1740347064 42459136 10193 4294967295 134512640 135094434 3221221600 3221220256 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 10366 10193 145 145 0 10221 0
[pid=20970] vsize: 41464
Current children cumulated CPU time (s) 229.05
Current children cumulated vsize (Kb) 45660

[startup+240.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20972
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 10807 0 0 0 23818 79 0 0 25 0 1 0 1740347064 44765184 10754 4294967295 134512640 135094434 3221221600 3221220192 134556757 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 10929 10754 145 145 0 10784 0
[pid=20970] vsize: 43716
Current children cumulated CPU time (s) 238.98
Current children cumulated vsize (Kb) 47912

[startup+250.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20972
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 11405 0 0 0 24807 84 0 0 25 0 1 0 1740347064 47218688 11352 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 11528 11352 145 145 0 11383 0
[pid=20970] vsize: 46112
Current children cumulated CPU time (s) 248.92
Current children cumulated vsize (Kb) 50308

[startup+260.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20972
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 11955 0 0 0 25799 88 0 0 25 0 1 0 1740347064 49471488 11902 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 12078 11902 145 145 0 11933 0
[pid=20970] vsize: 48312
Current children cumulated CPU time (s) 258.88
Current children cumulated vsize (Kb) 52508

[startup+270.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20972
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 12585 0 0 0 26788 92 0 0 25 0 1 0 1740347064 52051968 12532 4294967295 134512640 135094434 3221221600 3221220256 134557945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 12708 12532 145 145 0 12563 0
[pid=20970] vsize: 50832
Current children cumulated CPU time (s) 268.81
Current children cumulated vsize (Kb) 55028

[startup+280.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20972
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 13132 0 0 0 27779 96 0 0 25 0 1 0 1740347064 54292480 13079 4294967295 134512640 135094434 3221221600 3221220256 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 13255 13079 145 145 0 13110 0
[pid=20970] vsize: 53020
Current children cumulated CPU time (s) 278.76
Current children cumulated vsize (Kb) 57216

[startup+290.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20972
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 13885 0 0 0 28766 102 0 0 25 0 1 0 1740347064 57368576 13832 4294967295 134512640 135094434 3221221600 3221220256 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 14006 13832 145 145 0 13861 0
[pid=20970] vsize: 56024
Current children cumulated CPU time (s) 288.69
Current children cumulated vsize (Kb) 60220

[startup+300.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20972
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 14527 0 0 0 29757 105 0 0 25 0 1 0 1740347064 59998208 14474 4294967295 134512640 135094434 3221221600 3221220192 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 14648 14474 145 145 0 14503 0
[pid=20970] vsize: 58592
Current children cumulated CPU time (s) 298.63
Current children cumulated vsize (Kb) 62788

[startup+310.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20972
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 15075 0 0 0 30747 109 0 0 25 0 1 0 1740347064 62234624 15022 4294967295 134512640 135094434 3221221600 3221220224 134562139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 15194 15022 145 145 0 15049 0
[pid=20970] vsize: 60776
Current children cumulated CPU time (s) 308.57
Current children cumulated vsize (Kb) 64972

[startup+320.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20972
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 15670 0 0 0 31738 114 0 0 25 0 1 0 1740347064 64663552 15617 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 15787 15617 145 145 0 15642 0
[pid=20970] vsize: 63148
Current children cumulated CPU time (s) 318.53
Current children cumulated vsize (Kb) 67344

[startup+330.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20972
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 16122 0 0 0 32730 117 0 0 25 0 1 0 1740347064 66510848 16069 4294967295 134512640 135094434 3221221600 3221220192 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 16238 16069 145 145 0 16093 0
[pid=20970] vsize: 64952
Current children cumulated CPU time (s) 328.48
Current children cumulated vsize (Kb) 69148

[startup+340.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20972
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 16122 0 0 0 33730 117 0 0 25 0 1 0 1740347064 66510848 16069 4294967295 134512640 135094434 3221221600 3221220064 134781514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 16238 16069 145 145 0 16093 0
[pid=20970] vsize: 64952
Current children cumulated CPU time (s) 338.48
Current children cumulated vsize (Kb) 69148

[startup+350.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20972
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 16122 0 0 0 34731 117 0 0 25 0 1 0 1740347064 66510848 16069 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 16238 16069 145 145 0 16093 0
[pid=20970] vsize: 64952
Current children cumulated CPU time (s) 348.49
Current children cumulated vsize (Kb) 69148

[startup+360.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20972
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 16122 0 0 0 35731 117 0 0 25 0 1 0 1740347064 66510848 16069 4294967295 134512640 135094434 3221221600 3221220256 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 16238 16069 145 145 0 16093 0
[pid=20970] vsize: 64952
Current children cumulated CPU time (s) 358.49
Current children cumulated vsize (Kb) 69148

[startup+370.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20972
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 16122 0 0 0 36731 117 0 0 25 0 1 0 1740347064 66510848 16069 4294967295 134512640 135094434 3221221600 3221220192 134551702 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 16238 16069 145 145 0 16093 0
[pid=20970] vsize: 64952
Current children cumulated CPU time (s) 368.49
Current children cumulated vsize (Kb) 69148

[startup+380.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20972
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 16122 0 0 0 37731 117 0 0 25 0 1 0 1740347064 66510848 16069 4294967295 134512640 135094434 3221221600 3221220192 134556785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 16238 16069 145 145 0 16093 0
[pid=20970] vsize: 64952
Current children cumulated CPU time (s) 378.49
Current children cumulated vsize (Kb) 69148

[startup+390.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20972
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 16122 0 0 0 38732 117 0 0 25 0 1 0 1740347064 66510848 16069 4294967295 134512640 135094434 3221221600 3221220256 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 16238 16069 145 145 0 16093 0
[pid=20970] vsize: 64952
Current children cumulated CPU time (s) 388.5
Current children cumulated vsize (Kb) 69148

[startup+400.033 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20972
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 16122 0 0 0 39732 117 0 0 25 0 1 0 1740347064 66510848 16069 4294967295 134512640 135094434 3221221600 3221220224 134562108 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 16238 16069 145 145 0 16093 0
[pid=20970] vsize: 64952
Current children cumulated CPU time (s) 398.5
Current children cumulated vsize (Kb) 69148

[startup+410.034 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20972
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 16122 0 0 0 40732 117 0 0 25 0 1 0 1740347064 66510848 16069 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 16238 16069 145 145 0 16093 0
[pid=20970] vsize: 64952
Current children cumulated CPU time (s) 408.5
Current children cumulated vsize (Kb) 69148

[startup+420.033 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20972
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 16122 0 0 0 41732 117 0 0 25 0 1 0 1740347064 66510848 16069 4294967295 134512640 135094434 3221221600 3221220256 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 16238 16069 145 145 0 16093 0
[pid=20970] vsize: 64952
Current children cumulated CPU time (s) 418.5
Current children cumulated vsize (Kb) 69148

[startup+430.034 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20972
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 16122 0 0 0 42733 117 0 0 25 0 1 0 1740347064 66510848 16069 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 16238 16069 145 145 0 16093 0
[pid=20970] vsize: 64952
Current children cumulated CPU time (s) 428.51
Current children cumulated vsize (Kb) 69148

[startup+440.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20972
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 16122 0 0 0 43733 117 0 0 25 0 1 0 1740347064 66510848 16069 4294967295 134512640 135094434 3221221600 3221220192 134557413 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 16238 16069 145 145 0 16093 0
[pid=20970] vsize: 64952
Current children cumulated CPU time (s) 438.51
Current children cumulated vsize (Kb) 69148

[startup+450.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20972
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 16122 0 0 0 44733 117 0 0 25 0 1 0 1740347064 66510848 16069 4294967295 134512640 135094434 3221221600 3221220256 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 16238 16069 145 145 0 16093 0
[pid=20970] vsize: 64952
Current children cumulated CPU time (s) 448.51
Current children cumulated vsize (Kb) 69148

[startup+460.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20972
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 16122 0 0 0 45733 117 0 0 25 0 1 0 1740347064 66510848 16069 4294967295 134512640 135094434 3221221600 3221220288 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 16238 16069 145 145 0 16093 0
[pid=20970] vsize: 64952
Current children cumulated CPU time (s) 458.51
Current children cumulated vsize (Kb) 69148

[startup+470.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20972
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 16122 0 0 0 46733 117 0 0 25 0 1 0 1740347064 66510848 16069 4294967295 134512640 135094434 3221221600 3221220256 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 16238 16069 145 145 0 16093 0
[pid=20970] vsize: 64952
Current children cumulated CPU time (s) 468.51
Current children cumulated vsize (Kb) 69148

[startup+480.038 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20972
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 16122 0 0 0 47734 117 0 0 25 0 1 0 1740347064 66510848 16069 4294967295 134512640 135094434 3221221600 3221220192 134557512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 16238 16069 145 145 0 16093 0
[pid=20970] vsize: 64952
Current children cumulated CPU time (s) 478.52
Current children cumulated vsize (Kb) 69148

[startup+490.039 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20972
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 16122 0 0 0 48734 117 0 0 25 0 1 0 1740347064 66510848 16069 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 16238 16069 145 145 0 16093 0
[pid=20970] vsize: 64952
Current children cumulated CPU time (s) 488.52
Current children cumulated vsize (Kb) 69148

[startup+500.041 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20972
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 16122 0 0 0 49734 117 0 0 25 0 1 0 1740347064 66510848 16069 4294967295 134512640 135094434 3221221600 3221220192 134556949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 16238 16069 145 145 0 16093 0
[pid=20970] vsize: 64952
Current children cumulated CPU time (s) 498.52
Current children cumulated vsize (Kb) 69148

[startup+510.042 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20972
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 16122 0 0 0 50734 117 0 0 25 0 1 0 1740347064 66510848 16069 4294967295 134512640 135094434 3221221600 3221220256 134557972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 16238 16069 145 145 0 16093 0
[pid=20970] vsize: 64952
Current children cumulated CPU time (s) 508.52
Current children cumulated vsize (Kb) 69148

[startup+520.041 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20972
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 16122 0 0 0 51735 117 0 0 25 0 1 0 1740347064 66510848 16069 4294967295 134512640 135094434 3221221600 3221220256 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 16238 16069 145 145 0 16093 0
[pid=20970] vsize: 64952
Current children cumulated CPU time (s) 518.53
Current children cumulated vsize (Kb) 69148

[startup+530.042 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20972
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 16122 0 0 0 52735 117 0 0 25 0 1 0 1740347064 66510848 16069 4294967295 134512640 135094434 3221221600 3221220192 134557512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 16238 16069 145 145 0 16093 0
[pid=20970] vsize: 64952
Current children cumulated CPU time (s) 528.53
Current children cumulated vsize (Kb) 69148

[startup+540.043 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20972
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 16122 0 0 0 53735 117 0 0 25 0 1 0 1740347064 66510848 16069 4294967295 134512640 135094434 3221221600 3221220192 134556773 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 16238 16069 145 145 0 16093 0
[pid=20970] vsize: 64952
Current children cumulated CPU time (s) 538.53
Current children cumulated vsize (Kb) 69148

[startup+550.044 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20972
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 16377 0 0 0 54731 119 0 0 25 0 1 0 1740347064 67555328 16324 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 16493 16324 145 145 0 16348 0
[pid=20970] vsize: 65972
Current children cumulated CPU time (s) 548.51
Current children cumulated vsize (Kb) 70168

[startup+560.044 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20972
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 16885 0 0 0 55721 123 0 0 25 0 1 0 1740347064 69636096 16832 4294967295 134512640 135094434 3221221600 3221220256 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 17001 16832 145 145 0 16856 0
[pid=20970] vsize: 68004
Current children cumulated CPU time (s) 558.45
Current children cumulated vsize (Kb) 72200

[startup+570.045 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20972
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 17375 0 0 0 56712 127 0 0 25 0 1 0 1740347064 71643136 17322 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 17491 17322 145 145 0 17346 0
[pid=20970] vsize: 69964
Current children cumulated CPU time (s) 568.4
Current children cumulated vsize (Kb) 74160

[startup+580.046 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20972
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 17871 0 0 0 57704 130 0 0 25 0 1 0 1740347064 73674752 17818 4294967295 134512640 135094434 3221221600 3221220192 134557518 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 17987 17818 145 145 0 17842 0
[pid=20970] vsize: 71948
Current children cumulated CPU time (s) 578.35
Current children cumulated vsize (Kb) 76144

[startup+590.047 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20972
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 18236 0 0 0 58698 133 0 0 25 0 1 0 1740347064 75173888 18183 4294967295 134512640 135094434 3221221600 3221220224 134557714 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 18353 18183 145 145 0 18208 0
[pid=20970] vsize: 73412
Current children cumulated CPU time (s) 588.32
Current children cumulated vsize (Kb) 77608

[startup+600.048 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20972
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 18674 0 0 0 59690 136 0 0 25 0 1 0 1740347064 76967936 18621 4294967295 134512640 135094434 3221221600 3221220256 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 18791 18621 145 145 0 18646 0
[pid=20970] vsize: 75164
Current children cumulated CPU time (s) 598.27
Current children cumulated vsize (Kb) 79360

[startup+610.048 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20972
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 19176 0 0 0 60682 139 0 0 25 0 1 0 1740347064 79036416 19123 4294967295 134512640 135094434 3221221600 3221220256 134558062 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 19296 19123 145 145 0 19151 0
[pid=20970] vsize: 77184
Current children cumulated CPU time (s) 608.22
Current children cumulated vsize (Kb) 81380

[startup+620.049 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20972
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 19796 0 0 0 61670 144 0 0 25 0 1 0 1740347064 81575936 19743 4294967295 134512640 135094434 3221221600 3221220256 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 19916 19743 145 145 0 19771 0
[pid=20970] vsize: 79664
Current children cumulated CPU time (s) 618.15
Current children cumulated vsize (Kb) 83860

[startup+630.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/58 20974
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20400 0 0 0 62659 149 0 0 25 0 1 0 1740347064 84045824 20347 4294967295 134512640 135094434 3221221600 3221220252 134558255 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20519 20347 145 145 0 20374 0
[pid=20970] vsize: 82076
Current children cumulated CPU time (s) 628.09
Current children cumulated vsize (Kb) 86272

[startup+640.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20974
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20691 0 0 0 63654 152 0 0 25 0 1 0 1740347064 85233664 20638 4294967295 134512640 135094434 3221221600 3221220192 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20638 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 638.07
Current children cumulated vsize (Kb) 87432

[startup+650.052 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20974
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20691 0 0 0 64654 152 0 0 25 0 1 0 1740347064 85233664 20638 4294967295 134512640 135094434 3221221600 3221220256 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20638 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 648.07
Current children cumulated vsize (Kb) 87432

[startup+660.052 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20974
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20691 0 0 0 65654 152 0 0 25 0 1 0 1740347064 85233664 20638 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20638 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 658.07
Current children cumulated vsize (Kb) 87432

[startup+670.052 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20974
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20691 0 0 0 66654 152 0 0 25 0 1 0 1740347064 85233664 20638 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20638 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 668.07
Current children cumulated vsize (Kb) 87432

[startup+680.054 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20974
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20691 0 0 0 67654 152 0 0 25 0 1 0 1740347064 85233664 20638 4294967295 134512640 135094434 3221221600 3221220192 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20638 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 678.07
Current children cumulated vsize (Kb) 87432

[startup+690.055 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 20974
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20691 0 0 0 68655 152 0 0 25 0 1 0 1740347064 85233664 20638 4294967295 134512640 135094434 3221221600 3221220272 134555566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20638 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 688.08
Current children cumulated vsize (Kb) 87432

[startup+700.056 s]
Raw data (loadavg): 1.23 1.05 0.94 5/70 20991
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20691 0 0 0 69651 152 0 0 25 0 1 0 1740347064 85233664 20638 4294967295 134512640 135094434 3221221600 3221220272 134555811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20970/statm): 20809 20638 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 698.04
Current children cumulated vsize (Kb) 87432

[startup+710.06 s]
Raw data (loadavg): 1.65 1.15 0.97 3/70 20991
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20691 0 0 0 70647 152 0 0 25 0 1 0 1740347064 85233664 20638 4294967295 134512640 135094434 3221221600 3221220256 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20638 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 708
Current children cumulated vsize (Kb) 87432

[startup+720.06 s]
Raw data (loadavg): 1.86 1.21 1.00 4/65 21168
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20691 0 0 0 71640 153 0 0 25 0 1 0 1740347064 85233664 20638 4294967295 134512640 135094434 3221221600 3221220272 134555943 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20638 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 717.94
Current children cumulated vsize (Kb) 87432

[startup+730.061 s]
Raw data (loadavg): 1.95 1.25 1.01 2/62 21225
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20691 0 0 0 72639 153 0 0 25 0 1 0 1740347064 85233664 20638 4294967295 134512640 135094434 3221221600 3221220192 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20638 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 727.93
Current children cumulated vsize (Kb) 87432

[startup+740.062 s]
Raw data (loadavg): 1.96 1.27 1.02 2/62 21237
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20691 0 0 0 73640 153 0 0 25 0 1 0 1740347064 85233664 20638 4294967295 134512640 135094434 3221221600 3221220256 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20638 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 737.94
Current children cumulated vsize (Kb) 87432

[startup+750.062 s]
Raw data (loadavg): 1.97 1.30 1.03 4/62 21264
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20691 0 0 0 74638 154 0 0 25 0 1 0 1740347064 85233664 20638 4294967295 134512640 135094434 3221221600 3221220272 134556266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20638 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 747.93
Current children cumulated vsize (Kb) 87432

[startup+760.063 s]
Raw data (loadavg): 1.82 1.29 1.03 2/56 21295
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20691 0 0 0 75638 154 0 0 25 0 1 0 1740347064 85233664 20638 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20638 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 757.93
Current children cumulated vsize (Kb) 87432

[startup+770.063 s]
Raw data (loadavg): 1.69 1.28 1.03 2/56 21295
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20691 0 0 0 76638 154 0 0 25 0 1 0 1740347064 85233664 20638 4294967295 134512640 135094434 3221221600 3221220256 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20638 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 767.93
Current children cumulated vsize (Kb) 87432

[startup+780.064 s]
Raw data (loadavg): 1.58 1.27 1.03 2/56 21295
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20691 0 0 0 77638 154 0 0 25 0 1 0 1740347064 85233664 20638 4294967295 134512640 135094434 3221221600 3221220256 134557972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20638 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 777.93
Current children cumulated vsize (Kb) 87432

[startup+790.065 s]
Raw data (loadavg): 1.49 1.26 1.03 2/56 21295
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20691 0 0 0 78639 154 0 0 25 0 1 0 1740347064 85233664 20638 4294967295 134512640 135094434 3221221600 3221220256 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20638 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 787.94
Current children cumulated vsize (Kb) 87432

[startup+800.066 s]
Raw data (loadavg): 1.42 1.25 1.03 2/56 21295
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20691 0 0 0 79639 154 0 0 25 0 1 0 1740347064 85233664 20638 4294967295 134512640 135094434 3221221600 3221220256 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20638 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 797.94
Current children cumulated vsize (Kb) 87432

[startup+810.068 s]
Raw data (loadavg): 1.35 1.24 1.02 2/56 21295
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20691 0 0 0 80639 154 0 0 25 0 1 0 1740347064 85233664 20638 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20638 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 807.94
Current children cumulated vsize (Kb) 87432

[startup+820.068 s]
Raw data (loadavg): 1.30 1.23 1.02 2/56 21295
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20691 0 0 0 81639 154 0 0 25 0 1 0 1740347064 85233664 20638 4294967295 134512640 135094434 3221221600 3221220256 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20638 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 817.94
Current children cumulated vsize (Kb) 87432

[startup+830.069 s]
Raw data (loadavg): 1.25 1.22 1.02 2/56 21295
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20691 0 0 0 82640 154 0 0 25 0 1 0 1740347064 85233664 20638 4294967295 134512640 135094434 3221221600 3221220192 134556837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20638 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 827.95
Current children cumulated vsize (Kb) 87432

[startup+840.07 s]
Raw data (loadavg): 1.21 1.22 1.02 2/56 21295
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20691 0 0 0 83640 154 0 0 25 0 1 0 1740347064 85233664 20638 4294967295 134512640 135094434 3221221600 3221220192 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20638 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 837.95
Current children cumulated vsize (Kb) 87432

[startup+850.071 s]
Raw data (loadavg): 1.18 1.21 1.02 3/56 21295
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20691 0 0 0 84902 154 0 0 25 0 1 0 1740347064 85233664 20638 4294967295 134512640 135094434 3221221600 3221220256 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20638 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 850.57
Current children cumulated vsize (Kb) 87432

[startup+862.683 s]
Raw data (loadavg): 1.15 1.20 1.02 2/56 21295
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20691 0 0 0 85902 154 0 0 25 0 1 0 1740347064 85233664 20638 4294967295 134512640 135094434 3221221600 3221220192 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20638 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 860.57
Current children cumulated vsize (Kb) 87432

[startup+872.684 s]
Raw data (loadavg): 1.13 1.19 1.02 2/56 21295
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20691 0 0 0 86902 154 0 0 25 0 1 0 1740347064 85233664 20638 4294967295 134512640 135094434 3221221600 3221220256 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20638 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 870.57
Current children cumulated vsize (Kb) 87432

[startup+882.685 s]
Raw data (loadavg): 1.11 1.19 1.02 2/56 21295
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20691 0 0 0 87902 154 0 0 25 0 1 0 1740347064 85233664 20638 4294967295 134512640 135094434 3221221600 3221220192 134557537 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20638 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 880.57
Current children cumulated vsize (Kb) 87432

[startup+892.685 s]
Raw data (loadavg): 1.09 1.18 1.02 2/56 21295
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20691 0 0 0 88902 154 0 0 25 0 1 0 1740347064 85233664 20638 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20638 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 890.57
Current children cumulated vsize (Kb) 87432

[startup+902.685 s]
Raw data (loadavg): 1.08 1.17 1.02 2/56 21295
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20691 0 0 0 89903 154 0 0 25 0 1 0 1740347064 85233664 20638 4294967295 134512640 135094434 3221221600 3221220272 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20638 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 900.58
Current children cumulated vsize (Kb) 87432

[startup+912.686 s]
Raw data (loadavg): 1.06 1.17 1.01 2/56 21295
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20692 0 0 0 90903 154 0 0 25 0 1 0 1740347064 85233664 20639 4294967295 134512640 135094434 3221221600 3221220256 134558227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20639 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 910.58
Current children cumulated vsize (Kb) 87432

[startup+922.687 s]
Raw data (loadavg): 1.05 1.16 1.01 2/56 21295
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20693 0 0 0 91903 154 0 0 25 0 1 0 1740347064 85233664 20640 4294967295 134512640 135094434 3221221600 3221220192 134556809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20640 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 920.58
Current children cumulated vsize (Kb) 87432

[startup+932.688 s]
Raw data (loadavg): 1.05 1.16 1.01 2/56 21295
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20694 0 0 0 92903 154 0 0 25 0 1 0 1740347064 85233664 20641 4294967295 134512640 135094434 3221221600 3221220192 134556789 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20641 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 930.58
Current children cumulated vsize (Kb) 87432

[startup+942.688 s]
Raw data (loadavg): 1.04 1.15 1.01 2/56 21295
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20694 0 0 0 93903 154 0 0 25 0 1 0 1740347064 85233664 20641 4294967295 134512640 135094434 3221221600 3221220256 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20641 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 940.58
Current children cumulated vsize (Kb) 87432

[startup+952.688 s]
Raw data (loadavg): 1.03 1.14 1.01 2/56 21295
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20694 0 0 0 94903 154 0 0 25 0 1 0 1740347064 85233664 20641 4294967295 134512640 135094434 3221221600 3221220256 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20641 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 950.58
Current children cumulated vsize (Kb) 87432

[startup+962.689 s]
Raw data (loadavg): 1.03 1.14 1.01 2/56 21295
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20694 0 0 0 95903 154 0 0 25 0 1 0 1740347064 85233664 20641 4294967295 134512640 135094434 3221221600 3221220256 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20641 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 960.58
Current children cumulated vsize (Kb) 87432

[startup+972.689 s]
Raw data (loadavg): 1.02 1.13 1.01 2/56 21295
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20694 0 0 0 96904 154 0 0 25 0 1 0 1740347064 85233664 20641 4294967295 134512640 135094434 3221221600 3221220192 134557028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20641 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 970.59
Current children cumulated vsize (Kb) 87432

[startup+982.69 s]
Raw data (loadavg): 1.02 1.13 1.01 2/56 21295
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20694 0 0 0 97904 154 0 0 25 0 1 0 1740347064 85233664 20641 4294967295 134512640 135094434 3221221600 3221220256 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20641 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 980.59
Current children cumulated vsize (Kb) 87432

[startup+992.69 s]
Raw data (loadavg): 1.02 1.12 1.01 2/56 21295
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20694 0 0 0 98904 154 0 0 25 0 1 0 1740347064 85233664 20641 4294967295 134512640 135094434 3221221600 3221220272 134556426 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20641 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 990.59
Current children cumulated vsize (Kb) 87432

[startup+1002.69 s]
Raw data (loadavg): 1.01 1.12 1.01 2/56 21295
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20694 0 0 0 99904 154 0 0 25 0 1 0 1740347064 85233664 20641 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20641 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 1000.59
Current children cumulated vsize (Kb) 87432

[startup+1012.69 s]
Raw data (loadavg): 1.01 1.12 1.00 2/56 21295
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20694 0 0 0 100904 154 0 0 25 0 1 0 1740347064 85233664 20641 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20641 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 1010.59
Current children cumulated vsize (Kb) 87432

[startup+1022.69 s]
Raw data (loadavg): 1.01 1.11 1.00 2/56 21295
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20694 0 0 0 101905 154 0 0 25 0 1 0 1740347064 85233664 20641 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20641 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 1020.6
Current children cumulated vsize (Kb) 87432

[startup+1032.69 s]
Raw data (loadavg): 1.01 1.11 1.00 2/56 21295
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20694 0 0 0 102905 154 0 0 25 0 1 0 1740347064 85233664 20641 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20641 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 1030.6
Current children cumulated vsize (Kb) 87432

[startup+1042.69 s]
Raw data (loadavg): 1.00 1.10 1.00 2/56 21295
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20694 0 0 0 103905 154 0 0 25 0 1 0 1740347064 85233664 20641 4294967295 134512640 135094434 3221221600 3221220256 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20641 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 1040.6
Current children cumulated vsize (Kb) 87432

[startup+1052.69 s]
Raw data (loadavg): 1.00 1.10 1.00 2/56 21297
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20694 0 0 0 104905 154 0 0 25 0 1 0 1740347064 85233664 20641 4294967295 134512640 135094434 3221221600 3221220256 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20641 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 1050.6
Current children cumulated vsize (Kb) 87432

[startup+1062.69 s]
Raw data (loadavg): 1.00 1.10 1.00 2/56 21297
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20694 0 0 0 105906 154 0 0 25 0 1 0 1740347064 85233664 20641 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20641 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 1060.61
Current children cumulated vsize (Kb) 87432

[startup+1072.69 s]
Raw data (loadavg): 1.00 1.09 1.00 2/56 21297
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20694 0 0 0 106906 154 0 0 25 0 1 0 1740347064 85233664 20641 4294967295 134512640 135094434 3221221600 3221220256 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20641 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 1070.61
Current children cumulated vsize (Kb) 87432

[startup+1082.7 s]
Raw data (loadavg): 1.00 1.09 1.00 2/56 21297
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20694 0 0 0 107906 154 0 0 25 0 1 0 1740347064 85233664 20641 4294967295 134512640 135094434 3221221600 3221220192 134557363 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20641 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 1080.61
Current children cumulated vsize (Kb) 87432

[startup+1092.7 s]
Raw data (loadavg): 1.00 1.08 1.00 2/56 21297
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20694 0 0 0 108906 154 0 0 25 0 1 0 1740347064 85233664 20641 4294967295 134512640 135094434 3221221600 3221220272 134555811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20641 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 1090.61
Current children cumulated vsize (Kb) 87432

[startup+1102.7 s]
Raw data (loadavg): 1.00 1.08 1.00 2/56 21297
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20694 0 0 0 109906 154 0 0 25 0 1 0 1740347064 85233664 20641 4294967295 134512640 135094434 3221221600 3221220272 134556410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20641 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 1100.61
Current children cumulated vsize (Kb) 87432

[startup+1112.7 s]
Raw data (loadavg): 1.00 1.08 1.00 2/56 21297
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20694 0 0 0 110907 154 0 0 25 0 1 0 1740347064 85233664 20641 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20641 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 1110.62
Current children cumulated vsize (Kb) 87432

[startup+1122.7 s]
Raw data (loadavg): 1.00 1.08 1.00 2/56 21297
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20694 0 0 0 111907 154 0 0 25 0 1 0 1740347064 85233664 20641 4294967295 134512640 135094434 3221221600 3221220256 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20641 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 1120.62
Current children cumulated vsize (Kb) 87432

[startup+1132.7 s]
Raw data (loadavg): 1.00 1.07 1.00 2/56 21297
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20694 0 0 0 112907 154 0 0 25 0 1 0 1740347064 85233664 20641 4294967295 134512640 135094434 3221221600 3221220192 134557518 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20641 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 1130.62
Current children cumulated vsize (Kb) 87432

[startup+1142.7 s]
Raw data (loadavg): 1.00 1.07 1.00 2/56 21297
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20694 0 0 0 113907 154 0 0 25 0 1 0 1740347064 85233664 20641 4294967295 134512640 135094434 3221221600 3221220256 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20641 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 1140.62
Current children cumulated vsize (Kb) 87432

[startup+1152.7 s]
Raw data (loadavg): 1.00 1.07 1.00 2/56 21297
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20694 0 0 0 114908 154 0 0 25 0 1 0 1740347064 85233664 20641 4294967295 134512640 135094434 3221221600 3221220256 134558105 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20641 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 1150.63
Current children cumulated vsize (Kb) 87432

[startup+1162.7 s]
Raw data (loadavg): 1.00 1.06 1.00 2/56 21297
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20694 0 0 0 115908 154 0 0 25 0 1 0 1740347064 85233664 20641 4294967295 134512640 135094434 3221221600 3221220256 134558002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20641 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 1160.63
Current children cumulated vsize (Kb) 87432

[startup+1172.7 s]
Raw data (loadavg): 1.00 1.06 1.00 2/56 21297
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20694 0 0 0 116908 154 0 0 25 0 1 0 1740347064 85233664 20641 4294967295 134512640 135094434 3221221600 3221220272 134556307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20641 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 1170.63
Current children cumulated vsize (Kb) 87432

[startup+1182.7 s]
Raw data (loadavg): 1.00 1.06 1.00 2/56 21297
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20694 0 0 0 117908 154 0 0 25 0 1 0 1740347064 85233664 20641 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20641 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 1180.63
Current children cumulated vsize (Kb) 87432

[startup+1192.7 s]
Raw data (loadavg): 1.00 1.06 1.00 2/56 21297
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20694 0 0 0 118909 154 0 0 25 0 1 0 1740347064 85233664 20641 4294967295 134512640 135094434 3221221600 3221220192 134557375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20641 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 1190.64
Current children cumulated vsize (Kb) 87432

[startup+1202.7 s]
Raw data (loadavg): 1.00 1.05 1.00 2/56 21297
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20694 0 0 0 119909 154 0 0 25 0 1 0 1740347064 85233664 20641 4294967295 134512640 135094434 3221221600 3221220288 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20641 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 1200.64
Current children cumulated vsize (Kb) 87432



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1202.7 s]
Raw data (loadavg): 1.00 1.05 1.00 2/56 21297
Raw data (/proc/20966/stat): 20966 (minisat+_script) S 20965 20966 10120 0 -1 0 322 277 0 0 0 1 0 0 21 0 1 0 1740347058 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20966/statm): 1049 256 1003 147 0 902 0
[pid=20966] vsize: 4196
Raw data (/proc/20970/stat): 20970 (minisat+_64-bit) R 20966 20966 10120 0 -1 0 20694 0 0 0 119909 154 0 0 25 0 1 0 1740347064 85233664 20641 4294967295 134512640 135094434 3221221600 3221220256 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20970/statm): 20809 20641 145 145 0 20664 0
[pid=20970] vsize: 83236
Current children cumulated CPU time (s) 1200.64
Current children cumulated vsize (Kb) 87432

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

Child status: 10
Real time (s): 1202.75
CPU time (s): 1200.68
CPU user time (s): 1199.1
CPU system time (s): 1.58676
CPU usage (%): 99.8284
Max. virtual memory (cumulated for all children) (Kb): 87432
Name	mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-opt1217.opb
MD5SUM	697fa5beb3d240bccfa43a29ef9b4fb8
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-1536
Optimality of the best value was proved	NO
Number of terms in the objective function	16
Biggest coefficient in the objective function	32768
Number of bits for the biggest coefficient in the objective function	16
Sum of the numbers in the objective function	65535
Number of bits of the sum of numbers in the objective function	16
Biggest number in a constraint	49152
Number of bits of the biggest number in a constraint	16
Biggest sum of numbers in a constraint	114687
Number of bits of the biggest sum of numbers	17
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.03
Number of variables	784
Total number of constraints	833
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	816
Number of constraints which are nor clauses,nor cardinality constraints	17
Minimum length of a constraint	1
Maximum length of a constraint	64
Some explanations

General information on the benchmark

Trace number 6152

Launcher Data

Solver Data

Watcher Data

Verifier Data
