# HG changeset patch
# User blanchet
# Date 1304267845 -7200
# Node ID 67e2f2df68d51d2b274d4e76c119ba27b82aeb97
# Parent  77f94ac04f320a53fdbebed17808e4227022a696
recognize more SystemOnTPTP errors

diff -r 77f94ac04f32 -r 67e2f2df68d5 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Sun May 01 18:37:25 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Sun May 01 18:37:25 2011 +0200
@@ -318,7 +318,8 @@
    proof_delims = insert (op =) tstp_proof_delims proof_delims,
    known_failures =
      known_failures @ known_perl_failures @
-     [(TimedOut, "says Timeout")],
+     [(IncompleteUnprovable, "says Unknown"),
+      (TimedOut, "says Timeout")],
    use_conjecture_for_hypotheses = use_conjecture_for_hypotheses}
 
 fun int_average f xs = fold (Integer.add o f) xs 0 div length xs
@@ -344,8 +345,7 @@
   remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config)
              (K 200 (* FUDGE *)) true
 val remote_sine_e =
-  remote_atp sine_eN "SInE" ["0.4"] [] [(IncompleteUnprovable, "says Unknown")]
-             (K 500 (* FUDGE *)) true
+  remote_atp sine_eN "SInE" ["0.4"] [] [] (K 500 (* FUDGE *)) true
 val remote_snark =
   remote_atp snarkN "SNARK" ["20080805r024"]
              [("refutation.", "end_refutation.")] [] (K 250 (* FUDGE *)) true