equal
deleted
inserted
replaced
6 # Author: Jasmin Blanchette, TU Muenchen |
6 # Author: Jasmin Blanchette, TU Muenchen |
7 |
7 |
8 options=${@:1:$(($#-1))} |
8 options=${@:1:$(($#-1))} |
9 name=${@:$(($#)):1} |
9 name=${@:$(($#)):1} |
10 |
10 |
11 # Try converting the file from TPTP to DFG, but fail gracefully if it is already |
11 "$SPASS_HOME/SPASS" -Flotter $name \ |
12 # in DFG format. |
|
13 "$SPASS_HOME/tptp2dfg" $name $name.fof.dfg || cp $name $name.fof.dfg |
|
14 "$SPASS_HOME/SPASS" -Flotter $name.fof.dfg \ |
|
15 | sed 's/description({$/description({*/' \ |
12 | sed 's/description({$/description({*/' \ |
16 | sed 's/set_ClauseFormulaRelation()\.//' \ |
13 | sed 's/set_ClauseFormulaRelation()\.//' \ |
17 > $name.cnf.dfg |
14 > $name.cnf |
18 rm -f $name.fof.dfg |
15 cat $name.cnf |
19 cat $name.cnf.dfg |
16 "$SPASS_HOME/SPASS" $options $name.cnf \ |
20 "$SPASS_HOME/SPASS" $options $name.cnf.dfg \ |
|
21 | sed 's/\(Formulae used in the proof :\).*/\1 N\/A/' |
17 | sed 's/\(Formulae used in the proof :\).*/\1 N\/A/' |
22 rm -f $name.cnf.dfg |
18 rm -f $name.cnf |