src/HOL/Tools/ATP/scripts/spass_new
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