src/HOL/Tools/ATP/scripts/spass
changeset 44391 7b4104df2be6
parent 41456 006d85ad56d3
child 45302 04c87dec70b8
equal deleted inserted replaced
44390:99ef9fd7341b 44391:7b4104df2be6
     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     | sed 's/set_ClauseFormulaRelation()\.//' \
    14     > $name.cnf.dfg
    15     > $name.cnf.dfg
    15 rm -f $name.fof.dfg
    16 rm -f $name.fof.dfg
    16 cat $name.cnf.dfg
    17 cat $name.cnf.dfg
    17 "$SPASS_HOME/SPASS" $options $name.cnf.dfg \
    18 "$SPASS_HOME/SPASS" $options $name.cnf.dfg \
    18     | sed 's/\(Formulae used in the proof :\).*/\1 N\/A/'
    19     | sed 's/\(Formulae used in the proof :\).*/\1 N\/A/'