src/HOL/Tools/ATP/atp_systems.ML

--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Apr 03 22:04:57 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri Apr 04 11:49:47 2014 +0200
@@ -621,7 +621,7 @@
   {exec = K (["Z3_TPTP_HOME"], ["z3_tptp"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
      "-proof -t:" ^ string_of_int (to_secs 1 timeout) ^ " -file:" ^ file_name,
-   proof_delims = [],
+   proof_delims = [("SZS status Theorem", "")],
    known_failures = known_szs_status_failures,
    prem_role = Hypothesis,
    best_slices =