diff -r a0125644ccff -r 39229c760636 src/HOL/TPTP/atp_problem_import.ML
--- a/src/HOL/TPTP/atp_problem_import.ML	Tue Apr 24 09:47:40 2012 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML	Tue Apr 24 09:47:40 2012 +0200
@@ -24,20 +24,16 @@
 
 (** TPTP parsing based on ML-Yacc-generated "TPTP_Parser" **)
 
-fun mk_meta_not P = Logic.mk_implies (P, @{prop False})
-
 (* cf. "close_form" in "refute.ML" *)
 fun close_form t =
   fold (fn ((s, i), T) => fn t' =>
            Logic.all_const T $ Abs (s, T, abstract_over (Var ((s, i), T), t')))
        (Term.add_vars t []) t
 
-fun get_tptp_formula (_, role, P, _) =
-  P |> Logic.varify_global |> close_form
-    |> role = TPTP_Syntax.Role_Conjecture ? mk_meta_not
-
 fun read_tptp_file thy file_name =
   let
+    fun has_role role (_, role', _, _) = (role' = role)
+    fun get_prop (_, _, P, _) = P |> Logic.varify_global |> close_form
     val path =
       Path.explode file_name
       |> (fn path =>
@@ -45,12 +41,12 @@
                      ? Path.append (Path.explode "$PWD"))
     val ((_, _, problem), thy) =
       TPTP_Interpret.interpret_file true (Path.explode "$TPTP") path [] [] thy
-    val partitioned_problem =
-      List.partition (fn (_, role, _, _) => role = TPTP_Syntax.Role_Definition)
-                     problem
+    val (conjs, defs_and_nondefs) =
+      problem |> List.partition (has_role TPTP_Syntax.Role_Conjecture)
+              ||> List.partition (has_role TPTP_Syntax.Role_Definition)
   in
-    (exists (fn (_, role, _, _) => role = TPTP_Syntax.Role_Conjecture) problem,
-     pairself (map get_tptp_formula) partitioned_problem, Theory.checkpoint thy)
+    (map get_prop conjs, pairself (map get_prop) defs_and_nondefs,
+     Theory.checkpoint thy)
   end
 
 (** Isabelle (combination of provers) **)
@@ -60,11 +56,15 @@
 
 (** Nitpick (alias Nitrox) **)
 
+fun aptrueprop f ((t0 as @{const Trueprop}) $ t1) = t0 $ f t1
+  | aptrueprop f t = f t
+
 fun nitpick_tptp_file timeout file_name =
   let
-    val (falsify, (defs, nondefs), thy) = read_tptp_file @{theory} file_name
+    val (conjs, (defs, nondefs), thy) = read_tptp_file @{theory} file_name
     val ctxt = Proof_Context.init_global thy
-    val defs = defs |> map (ATP_Util.extensionalize_term ctxt)
+    val defs = defs |> map (ATP_Util.extensionalize_term ctxt
+                            #> aptrueprop (open_form I))
     val state = Proof.init ctxt
     val params =
       [("card", "1\<emdash>100"),
@@ -72,14 +72,15 @@
        ("sat_solver", "smart"),
        ("max_threads", "1"),
        ("batch_size", "10"),
-       ("falsify", if falsify then "true" else "false"),
+       ("falsify", if null conjs then "false" else "true"),
        (* ("debug", "true"), *)
        ("verbose", "true"),
        (* ("overlord", "true"), *)
        ("show_consts", "true"),
        ("format", "1000"),
        ("max_potential", "0"),
-       ("timeout", string_of_int timeout)]
+       ("timeout", string_of_int timeout),
+       ("tac_timeout", string_of_int ((timeout + 49) div 50))]
       |> Nitpick_Isar.default_params thy
     val i = 1
     val n = 1
@@ -87,7 +88,8 @@
     val subst = []
   in
     Nitpick.pick_nits_in_term state params Nitpick.TPTP i n step subst
-        defs nondefs (if falsify then @{prop False} else @{prop True}); ()
+        defs nondefs (case conjs of conj :: _ => conj | _ => @{prop True});
+    ()
   end
 
 
@@ -103,14 +105,15 @@
 
 fun refute_tptp_file timeout file_name =
   let
-    val (falsify, (defs, nondefs), thy) = read_tptp_file @{theory} file_name
+    val (conjs, (defs, nondefs), thy) = read_tptp_file @{theory} file_name
     val ctxt = Proof_Context.init_global thy
     val params =
       [("maxtime", string_of_int timeout),
        ("maxvars", "100000")]
   in
-    Refute.refute_term ctxt params (defs @ nondefs) @{prop False}
-    |> print_szs_from_outcome falsify
+    Refute.refute_term ctxt params (defs @ nondefs)
+        (case conjs of conj :: _ => conj | _ => @{prop True})
+    |> print_szs_from_outcome (not (null conjs))
   end