For my own memory:
The following command extracts the line with the execution time and the one above it to a new file:
grep ^"Elapsed" output4.3.txt -B 1 | grep -Ev ^"--" > filtered.output4.3.txt
The evenodd script splits the even and odd lines into separate files. The odd file contains the lines with the solution cost and the even file contains the lines with the execution time:
./evenodd.sh filtered.output4.3.txt timelines.4.3.txt costlines.4.3.txt
Finally, the following command extracts just the fields of interest:
cut -d " " -f 5 timelines.4.3.txt > times.4.2.txt
cut -d " " -f 5 costlines.4.3.txt > costs.4.2.txt
And here is a better shell script that makes the job easier:
#!/bin/bash
grep ^"Elapsed" $1 -B 1 | grep -Ev ^"--" | awk 'NR%2==0' | cut -d " " -f 5 > $2
grep ^"Elapsed" $1 -B 1 | grep -Ev ^"--" | awk 'NR%2==1' > $3
