equal
deleted
inserted
replaced
1 #!/usr/bin/env bash |
|
2 # |
|
3 # Wrapper for SPASS that also outputs the Flotter-generated CNF (needed for |
|
4 # Isar proof reconstruction) |
|
5 # |
|
6 # Author: Jasmin Blanchette, TU Muenchen |
|
7 |
|
8 options=${@:1:$(($#-1))} |
|
9 name=${@:$(($#)):1} |
|
10 |
|
11 $SPASS_HOME/tptp2dfg $name $name.fof.dfg |
|
12 $SPASS_HOME/SPASS -Flotter $name.fof.dfg \ |
|
13 | sed 's/description({$/description({*/' \ |
|
14 > $name.cnf.dfg |
|
15 rm -f $name.fof.dfg |
|
16 cat $name.cnf.dfg |
|
17 $SPASS_HOME/SPASS $options $name.cnf.dfg \ |
|
18 | sed 's/\(Formulae used in the proof :\).*/\1 N\/A/' |
|
19 rm -f $name.cnf.dfg |
|