src/HOL/TPTP/atp_problem_import.ML

     fun print_szs_of_outcome falsify s =
       "% SZS status " ^
       (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 =
       [("maxtime", string_of_int timeout),
        ("maxvars", "100000")]

 fun print_szs_of_success conjs success =
   writeln ("% SZS status " ^
     (if success then
        if null conjs then "Unsatisfiable" else "Theorem"
      else
-       "Unknown"))
+       "GaveUp"))
 
 fun sledgehammer_tptp_file thy timeout file_name =
   let
     val (conjs, assms, ctxt) = read_tptp_file thy (freeze_problem_consts thy o snd) file_name
     val conj = make_conj ([], []) conjs