# HG changeset patch
# User blanchet
# Date 1443812792 -7200
# Node ID 9a50ea544fd3a708adc122bb03f7b036ae601025
# Parent  a2548e708f03c14df4674c96ab265f579c38f4ff
better compliance with TPTP SZS standard

diff -r a2548e708f03 -r 9a50ea544fd3 src/HOL/TPTP/atp_problem_import.ML
--- a/src/HOL/TPTP/atp_problem_import.ML	Fri Oct 02 20:28:56 2015 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML	Fri Oct 02 21:06:32 2015 +0200
@@ -116,7 +116,7 @@
       (if s = "genuine" then
          if falsify then "CounterSatisfiable" else "Satisfiable"
        else
-         "Unknown")
+         "GaveUp")
       |> writeln
     val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy snd file_name
     val params =
@@ -268,7 +268,7 @@
     (if success then
        if null conjs then "Unsatisfiable" else "Theorem"
      else
-       "Unknown"))
+       "GaveUp"))
 
 fun sledgehammer_tptp_file thy timeout file_name =
   let
diff -r a2548e708f03 -r 9a50ea544fd3 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Fri Oct 02 20:28:56 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Fri Oct 02 21:06:32 2015 +0200
@@ -636,7 +636,7 @@
                (if genuine then
                   if falsify then "CounterSatisfiable" else "Satisfiable"
                 else
-                  "Unknown") ^ "\n" ^
+                  "GaveUp") ^ "\n" ^
                "% SZS output start FiniteModel")
         val (reconstructed_model, codatatypes_ok) =
           reconstruct_hol_model