diff -r c124032ac96f -r 0134d6650092 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Sun May 22 14:50:32 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Sun May 22 14:51:01 2011 +0200
@@ -15,7 +15,7 @@
     AConn of connective * ('a, 'b, 'c) formula list |
     AAtom of 'c
 
-  datatype format = UEQ | FOF | TFF
+  datatype format = CNF_UEQ | FOF | TFF
   datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
   datatype 'a problem_line =
     Decl of string * 'a * 'a list * 'a |
@@ -23,18 +23,20 @@
                * string fo_term option * string fo_term option
   type 'a problem = (string * 'a problem_line list) list
 
-(* official TPTP syntax *)
+  (* official TPTP syntax *)
   val tptp_special_prefix : string
   val tptp_false : string
   val tptp_true : string
   val tptp_tff_type_of_types : string
   val tptp_tff_bool_type : string
   val tptp_tff_individual_type : string
+  val is_atp_variable : string -> bool
   val timestamp : unit -> string
   val hashw : word * word -> word
   val hashw_string : string * word -> word
-  val is_atp_variable : string -> bool
   val tptp_strings_for_atp_problem : format -> string problem -> string list
+  val filter_cnf_ueq_problem :
+    (string * string) problem -> (string * string) problem
   val nice_atp_problem :
     bool -> ('a * (string * string) problem_line list) list
     -> ('a * string problem_line list) list
@@ -54,7 +56,7 @@
   AConn of connective * ('a, 'b, 'c) formula list |
   AAtom of 'c
 
-datatype format = UEQ | FOF | TFF
+datatype format = CNF_UEQ | FOF | TFF
 datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
 datatype 'a problem_line =
   Decl of string * 'a * 'a list * 'a |
@@ -70,6 +72,8 @@
 val tptp_tff_bool_type = "$o"
 val tptp_tff_individual_type = "$i"
 
+fun is_atp_variable s = Char.isUpper (String.sub (s, 0))
+
 val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
 
 (* This hash function is recommended in Compilers: Principles, Techniques, and
@@ -129,12 +133,11 @@
 fun string_for_problem_line _ (Decl (ident, sym, arg_tys, res_ty)) =
     "tff(" ^ ident ^ ", type,\n    " ^ sym ^ " : " ^
     string_for_symbol_type arg_tys res_ty ^ ").\n"
-  | string_for_problem_line format
-                            (Formula (ident, kind, phi, source, useful_info)) =
-    (case format of UEQ => "cnf" | FOF => "fof" | TFF => "tff") ^
+  | string_for_problem_line format (Formula (ident, kind, phi, source, info)) =
+    (case format of CNF_UEQ => "cnf" | FOF => "fof" | TFF => "tff") ^
     "(" ^ ident ^ ", " ^ string_for_kind kind ^ ",\n    (" ^
     string_for_formula format phi ^ ")" ^
-    (case (source, useful_info) of
+    (case (source, info) of
        (NONE, NONE) => ""
      | (SOME tm, NONE) => ", " ^ string_for_term tm
      | (_, SOME tm) =>
@@ -149,7 +152,37 @@
            map (string_for_problem_line format) lines)
        problem
 
-fun is_atp_variable s = Char.isUpper (String.sub (s, 0))
+
+(** CNF UEQ (Waldmeister) **)
+
+exception LOST_CONJECTURE of unit
+
+fun is_problem_line_negated (Formula (_, _, AConn (ANot, _), _, _)) = true
+  | is_problem_line_negated _ = false
+
+fun is_problem_line_cnf_ueq
+        (Formula (_, _, AAtom (ATerm (("equal", _), _)), _, _)) = true
+  | is_problem_line_cnf_ueq _ = false
+
+fun open_formula (AQuant (AForall, _, phi)) = open_formula phi
+  | open_formula phi = phi
+fun open_non_conjecture_line (line as Formula (_, Conjecture, _, _, _)) = line
+  | open_non_conjecture_line (Formula (ident, kind, phi, source, info)) =
+    Formula (ident, kind, open_formula phi, source, info)
+  | open_non_conjecture_line line = line
+
+fun negate_conjecture_line (Formula (ident, Conjecture, phi, source, info)) =
+    Formula (ident, Hypothesis, AConn (ANot, [phi]), source, info)
+  | negate_conjecture_line line = line
+
+val filter_cnf_ueq_problem =
+  map (apsnd (map open_non_conjecture_line
+              #> filter is_problem_line_cnf_ueq
+              #> map negate_conjecture_line))
+  #> (fn problem =>
+         let
+           val conjs = problem |> maps snd |> filter is_problem_line_negated
+         in if length conjs = 1 then problem else [] end)
 
 
 (** Nice names **)
@@ -178,14 +211,15 @@
    problem files. "equal" is reserved by some ATPs. "eq" is reserved to ensure
    that "HOL.eq" is correctly mapped to equality. *)
 val reserved_nice_names = ["op", "equal", "eq"]
+
 fun readable_name full_name s =
   if s = full_name then
     s
   else
     s |> no_qualifiers
       |> Name.desymbolize (Char.isUpper (String.sub (full_name, 0)))
-         (* SNARK doesn't like sort (type) names that end with digits. We make
-            an effort to avoid this here. *)
+         (* SNARK 20080805r024 doesn't like sort (type) names that end with
+            digits. We make an effort to avoid this here. *)
       |> (fn s => if Char.isDigit (String.sub (s, size s - 1)) then s ^ "_"
                   else s)
       |> (fn s =>
@@ -209,7 +243,8 @@
         val nice_prefix = readable_name full_name desired_name
         fun add j =
           let
-            (* The trailing "_" is for SNARK (cf. comment above). *)
+            (* The trailing "_" is for SNARK 20080805r024 (see comment
+               above). *)
             val nice_name =
               nice_prefix ^ (if j = 0 then "" else "_" ^ string_of_int j ^ "_")
           in
@@ -240,9 +275,8 @@
     ##>> pool_map nice_name arg_tys
     ##>> nice_name res_ty
     #>> (fn ((sym, arg_tys), res_ty) => Decl (ident, sym, arg_tys, res_ty))
-  | nice_problem_line (Formula (ident, kind, phi, source, useful_info)) =
-    nice_formula phi
-    #>> (fn phi => Formula (ident, kind, phi, source, useful_info))
+  | nice_problem_line (Formula (ident, kind, phi, source, info)) =
+    nice_formula phi #>> (fn phi => Formula (ident, kind, phi, source, info))
 fun nice_problem problem =
   pool_map (fn (heading, lines) =>
                pool_map nice_problem_line lines #>> pair heading) problem