--- 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