src/HOL/Tools/ATP/scripts/spass
changeset 41456 006d85ad56d3
parent 38046 6659c15e7421
child 44391 7b4104df2be6
equal deleted inserted replaced
41455:d3be2a414d15 41456:006d85ad56d3
     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 $SPASS_HOME/tptp2dfg $name $name.fof.dfg
    11 "$SPASS_HOME/tptp2dfg" $name $name.fof.dfg
    12 $SPASS_HOME/SPASS -Flotter $name.fof.dfg \
    12 "$SPASS_HOME/SPASS" -Flotter $name.fof.dfg \
    13     | sed 's/description({$/description({*/' \
    13     | sed 's/description({$/description({*/' \
    14     > $name.cnf.dfg
    14     > $name.cnf.dfg
    15 rm -f $name.fof.dfg
    15 rm -f $name.fof.dfg
    16 cat $name.cnf.dfg
    16 cat $name.cnf.dfg
    17 $SPASS_HOME/SPASS $options $name.cnf.dfg \
    17 "$SPASS_HOME/SPASS" $options $name.cnf.dfg \
    18     | sed 's/\(Formulae used in the proof :\).*/\1 N\/A/'
    18     | sed 's/\(Formulae used in the proof :\).*/\1 N\/A/'
    19 rm -f $name.cnf.dfg
    19 rm -f $name.cnf.dfg