# HG changeset patch
# User quigley
# Date 1116854196 -7200
# Node ID 25cb0fe2e1c61f7790a98608d19017efa41c2bdf
# Parent  b2bf9a5cde37b063e002a5bc9359334a70cfaa32
spassshell and testout.py are used to filter the proof part out of SPASS's
output (i.e. cuts out input and search information).

diff -r b2bf9a5cde37 -r 25cb0fe2e1c6 src/HOL/Tools/ATP/spassshell
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP/spassshell	Mon May 23 15:16:36 2005 +0200
@@ -0,0 +1,5 @@
+#/homes/clq20/bin/SPASS -DocProof /homes/clq20/prob_1.dfg |/homes/clq20/testoutput.py
+
+/homes/clq20/bin/SPASS $* |/homes/clq20/IsabelleCVS/isabelle/HOL/Tools/ATP/testoutput.py
+
+#pwd
diff -r b2bf9a5cde37 -r 25cb0fe2e1c6 src/HOL/Tools/ATP/testoutput.py
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP/testoutput.py	Mon May 23 15:16:36 2005 +0200
@@ -0,0 +1,53 @@
+#!/usr/bin/python
+
+import string
+import sys
+
+f = open ("/tmp/args", "w")
+for x in sys.argv:
+  f.write("%s " % x)
+f.write("\n")
+f.close()
+
+#f = open ("/home/clq20/scratch/13354/dfg/spassprooflist", "r")
+#f = open ("/home/clq20/testoutput.py", "r")
+
+mode = 0
+try:
+  while 1:
+    line = sys.stdin.readline()
+    words = line.split()
+    if len(words) > 0:
+      if words[0] == "SPASS":
+        mode = 1
+    if line == '':
+      break
+    line = line[:-1]
+    if mode == 1:
+      print line
+except:
+  pass
+#f.close()
+
+
+
+
+sys.exit()
+
+for i in range(0, 50):
+  print "blah gibberish nonsense"
+
+print """Here is a proof with depth 1, length 9 :
+2[0:Inp] || v_P(tconst_fun(typ__Ha,tconst_bool),v_x)* -> v_P(tconst_fun(typ__Ha,tconst_bool),U)*.
+3[0:Inp] || v_P(tconst_fun(typ__Ha,tconst_bool),U)*+ -> v_P(tconst_fun(typ__Ha,tconst_bool),v_x)*.
+4[0:Inp] ||  -> v_P(tconst_fun(typ__Ha,tconst_bool),U)* v_P(tconst_fun(typ__Ha,tconst_bool),v_xa)*.
+5[0:Inp] || v_P(tconst_fun(typ__Ha,tconst_bool),v_xb)* v_P(tconst_fun(typ__Ha,tconst_bool),U)* -> .
+6[0:Con:4.0] ||  -> v_P(tconst_fun(typ__Ha,tconst_bool),v_xa)*.
+7[0:Con:5.1] || v_P(tconst_fun(typ__Ha,tconst_bool),v_xb)* -> .
+8[0:Res:6.0,3.0] ||  -> v_P(tconst_fun(typ__Ha,tconst_bool),v_x)*.
+9[0:MRR:2.0,8.0] ||  -> v_P(tconst_fun(typ__Ha,tconst_bool),U)*.
+10[0:UnC:9.0,7.0] ||  -> .
+Formulae used in the proof :
+
+--------------------------SPASS-STOP------------------------------
+"""