changeset 46370 | b3e53dd6f10a |
child 46403 | 3069344da626 |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/ATP/scripts/spass_new Mon Jan 30 17:18:58 2012 +0100 @@ -0,0 +1,14 @@ +#!/usr/bin/env bash +# +# Wrapper for SPASS 3.8 that also outputs the clause-to-formula relation +# +# Author: Jasmin Blanchette, TU Muenchen + +options=${@:1:$(($#-1))} +name=${@:$(($#)):1} + +rm -f $name.prf +"$SPASS_NEW_HOME/SPASS" -FPDFGProof -FPFCR $options $name \ + | sed 's/\(Formulae used in the proof :\).*/\1 N\/A/' +cat $name.prf +#rm -f $name.cnf