1# I/O files 2DIR=$2 3IN="$DIR/atp_in" 4OUT="$DIR/out" 5OUT1="$DIR/out1" 6OUT2="$DIR/out2" 7STATUS="$DIR/status" 8ERROR="$DIR/error" 9 10# Running Vampire (4.2.2) 11timeout $1 ./vampire --time_limit $1 --proof tptp --output_axiom_names on $IN 2> $ERROR \ 12 | grep "file[(]'\| SZS" > $OUT1 13# Extracting status 14grep "SZS status" $OUT1 > $STATUS 2> $ERROR 15sed -i -e 's/^%[ ]*SZS[ ]*status\(.*\)[ ]*for.*$/\1/' $STATUS 2> $ERROR 16sed -i 's/ //g' $STATUS 2> $ERROR 17# Extracting axioms 18grep "^[ ]*file[(].*,\(.*\)[)])\..*$" $OUT1 > $OUT2 2> $ERROR 19sed -e 's/^[ ]*file[(].*,\(.*\)[)])\..*$/\1/' $OUT2 > $OUT 2> $ERROR 20