From bd90828605dc049e1917536171808c0bae91b045 Mon Sep 17 00:00:00 2001
From: Guillaume Burel <guillaume.burel@inria.fr>
Date: Tue, 25 Jun 2024 16:13:08 +0200
Subject: [PATCH 1/9] Accept integers as formula names

---
 parsetptp.mly | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/parsetptp.mly b/parsetptp.mly
index ce1e7c4..14769bb 100644
--- a/parsetptp.mly
+++ b/parsetptp.mly
@@ -99,19 +99,15 @@ phrase:
   | INCLUDE OPEN LIDENT CLOSE DOT  { Phrase.Include ($3, None) }
   | INCLUDE OPEN LIDENT COMMA LBRACKET name_list RBRACKET CLOSE DOT
                                    { Phrase.Include ($3, Some ($6)) }
-  | INPUT_FORMULA OPEN LIDENT COMMA LIDENT COMMA formula extra CLOSE DOT
+  | INPUT_FORMULA OPEN name COMMA LIDENT COMMA formula extra CLOSE DOT
                                    { Phrase.Formula (ns_hyp $3, $5, $7, None) }
-  | INPUT_CLAUSE OPEN LIDENT COMMA LIDENT COMMA cnf_formula extra CLOSE DOT
+  | INPUT_CLAUSE OPEN name COMMA LIDENT COMMA cnf_formula extra CLOSE DOT
      { Phrase.Formula (ns_hyp $3, $5, cnf_to_formula $7, None) }
-  | INPUT_TFF_FORMULA OPEN LIDENT COMMA LIDENT COMMA formula COMMA LIDENT extra CLOSE DOT
+  | INPUT_TFF_FORMULA OPEN name COMMA LIDENT COMMA formula COMMA LIDENT extra CLOSE DOT
      { Phrase.Formula (ns_hyp $3, "tff_" ^ $5, $7, Some $9) }
-  | INPUT_TFF_FORMULA OPEN LIDENT COMMA LIDENT COMMA formula extra CLOSE DOT
+  | INPUT_TFF_FORMULA OPEN name COMMA LIDENT COMMA formula extra CLOSE DOT
      { Phrase.Formula (ns_hyp $3, "tff_" ^ $5, $7, None) }
-  | INPUT_TFF_FORMULA OPEN LIDENT COMMA LIDENT COMMA type_def extra CLOSE DOT
-     { Phrase.Formula (ns_hyp $3, "tff_" ^ $5, $7, None) }
-  | INPUT_TFF_FORMULA OPEN INT COMMA LIDENT COMMA formula extra CLOSE DOT
-     { Phrase.Formula (ns_hyp $3, "tff_" ^ $5, $7, None) }
-  | INPUT_TFF_FORMULA OPEN INT COMMA LIDENT COMMA type_def extra CLOSE DOT
+  | INPUT_TFF_FORMULA OPEN name COMMA LIDENT COMMA type_def extra CLOSE DOT
      { Phrase.Formula (ns_hyp $3, "tff_" ^ $5, $7, None) }
   | ANNOT                          { Phrase.Annotation $1 }
 ;
@@ -224,4 +220,8 @@ atom:
   | FALSE                          { efalse }
   | expr                           { $1 }
 ;
+
+name:
+  LIDENT { $1 }
+  |INT { "zenon_tptp_formula_" ^ $1 }
 %%

From 01c06cdc050a5d9d5680d0ef643dc156d089a5a2 Mon Sep 17 00:00:00 2001
From: Guillaume Burel <guillaume.burel@inria.fr>
Date: Thu, 11 Jul 2024 17:18:40 +0200
Subject: [PATCH 2/9] Fix bug where a free variable was printed in the proof
 term.

---
 lpprint.ml | 275 ++++++++++++++++++++++++++---------------------------
 1 file changed, 137 insertions(+), 138 deletions(-)

diff --git a/lpprint.ml b/lpprint.ml
index 5226086..a1d854a 100644
--- a/lpprint.ml
+++ b/lpprint.ml
@@ -18,26 +18,23 @@ let escape_name s =
     then s else "{|" ^ s ^ "|}"
 
 
-let check_pvar v l = if List.mem v l then "&" ^ v else v
-let delete_pvar v l = List.filter (fun x -> x <> v) l
-
-let rec print_dk_type_aux o (t, l_rule) =
+let rec print_dk_type_aux o (t, var_context) =
   match t with
   | Dktypetype -> fprintf o "Type"
   | Dktypeprop -> fprintf o "Prop"
   | Dkarrow (l, r) ->
      begin
-       List.iter (fun x -> fprintf o "%a → " print_dk_type_aux (x, l_rule)) l;
-       print_dk_type_aux o (r, l_rule);
+       List.iter (fun x -> fprintf o "%a → " print_dk_type_aux (x, var_context)) l;
+       print_dk_type_aux o (r, var_context);
      end
   | Dkpi (Dkvar (_, t1) as var, t2) ->
   let pvar = escape_name (get_var_newname var) in
       fprintf o "Π (%s : %a),\n %a"
-	      pvar print_dk_type_aux (t1, l_rule) print_dk_type_aux (t2, delete_pvar pvar l_rule)
+	      pvar print_dk_type_aux (t1, var_context) print_dk_type_aux (t2, pvar::var_context)
   | Dkpi _ -> assert false
   | Dkproof (t) ->
-     fprintf o "ϵ (%a)" print_dk_term_aux (t, l_rule)
-  | t -> fprintf o "τ (%a)" print_dk_zentype_aux (t, l_rule)
+     fprintf o "ϵ (%a)" print_dk_term_aux (t, var_context)
+  | t -> fprintf o "τ (%a)" print_dk_zentype_aux (t, var_context)
 and print_dk_type o t = print_dk_type_aux o (t, [])
 and print_dk_zentype_aux o (t, l) =
   match t with
@@ -57,211 +54,213 @@ and print_dk_cst o t =
           fprintf o " %s" !Globals.neg_conj
       end
 
-and print_dk_term_aux o (t, l_rule) =
+and print_dk_term_aux o (t, var_context) =
   match t with
-  | Dkvar (_, _) as var ->
-      let pvar = (escape_name (get_var_newname var)) in
-      fprintf o "%s" (check_pvar pvar l_rule)
+  | Dkvar (v, _) as var ->
+    let pvar = (escape_name (get_var_newname var)) in
+    if not (List.mem pvar var_context)
+    then fprintf o "select ι"
+    else fprintf o "%s" pvar
  | Dklam (Dkvar (_, t1) as var, t2) ->
       let pvar = (escape_name (get_var_newname var)) in
      fprintf o "λ (%s : %a),\n %a"
 	     pvar
-	     print_dk_type_aux (t1, l_rule) print_dk_term_aux (t2, (delete_pvar pvar l_rule))
+	     print_dk_type_aux (t1, var_context) print_dk_term_aux (t2, (pvar::var_context))
   | Dklam (Dkapp (v, t1, []), t2) ->
       let pvar = escape_name v in
      fprintf o "λ (%s : %a),\n %a"
-	     pvar print_dk_type_aux (t1, l_rule) print_dk_term_aux (t2, (delete_pvar pvar l_rule))
+	     pvar print_dk_type_aux (t1, var_context) print_dk_term_aux (t2, (pvar::var_context))
   | Dklam _ -> assert false
   | Dkapp (v, _, l) ->
      begin
        print_dk_cst o v;
-       List.iter (fun x -> fprintf o " (%a)" print_dk_term_aux (x, l_rule)) l;
+       List.iter (fun x -> fprintf o " (%a)" print_dk_term_aux (x, var_context)) l;
 (*       fprintf o "\n ";*)
      end
   | Dkseq -> fprintf o "ϵ ⊥"
   | Dknot (t) ->
-     fprintf o "¬\n (%a)" print_dk_term_aux  (t, l_rule)
+     fprintf o "¬\n (%a)" print_dk_term_aux  (t, var_context)
   | Dkand (t1, t2) ->
-     fprintf o "(%a)\n∧\n(%a)\n" print_dk_term_aux (t1, l_rule) print_dk_term_aux (t2, l_rule)
+     fprintf o "(%a)\n∧\n(%a)\n" print_dk_term_aux (t1, var_context) print_dk_term_aux (t2, var_context)
   | Dkor (t1, t2) ->
-     fprintf o "(%a)\n∨\n(%a)\n" print_dk_term_aux (t1, l_rule) print_dk_term_aux (t2, l_rule)
+     fprintf o "(%a)\n∨\n(%a)\n" print_dk_term_aux (t1, var_context) print_dk_term_aux (t2, var_context)
   | Dkimply (t1, t2) ->
-     fprintf o "(%a)\n⇒\n(%a)\n" print_dk_term_aux (t1, l_rule) print_dk_term_aux (t2, l_rule)
+     fprintf o "(%a)\n⇒\n(%a)\n" print_dk_term_aux (t1, var_context) print_dk_term_aux (t2, var_context)
   | Dkequiv (t1, t2) ->
-     fprintf o "(%a)\n⇔\n(%a)\n" print_dk_term_aux (t1, l_rule) print_dk_term_aux (t2, l_rule)
+     fprintf o "(%a)\n⇔\n(%a)\n" print_dk_term_aux (t1, var_context) print_dk_term_aux (t2, var_context)
   | Dkforall (_, t2) ->
-     fprintf o "∀α (%a)" print_dk_term_aux (t2, l_rule)
-     (* fprintf o "@∀ (%a)\n (%a)" print_dk_zentype_aux (t1, l_rule) print_dk_term_aux (t2, l_rule) *)
+     fprintf o "∀α (%a)" print_dk_term_aux (t2, var_context)
+     (* fprintf o "@∀ (%a)\n (%a)" print_dk_zentype_aux (t1, var_context) print_dk_term_aux (t2, var_context) *)
   | Dkexists (_, t2) ->
-     fprintf o "∃α (%a)" print_dk_term_aux (t2, l_rule)
-     (* fprintf o "@∃ (%a)\n (%a)" print_dk_zentype_aux  (t1, l_rule) print_dk_term_aux (t2, l_rule) *)
+     fprintf o "∃α (%a)" print_dk_term_aux (t2, var_context)
+     (* fprintf o "@∃ (%a)\n (%a)" print_dk_zentype_aux  (t1, var_context) print_dk_term_aux (t2, var_context) *)
   | Dkforalltype (t) ->
-     fprintf o "foralltype\n (%a)" print_dk_term_aux (t, l_rule)
+     fprintf o "foralltype\n (%a)" print_dk_term_aux (t, var_context)
   | Dkexiststype (t) ->
-     fprintf o "existstype\n (%a)" print_dk_term_aux (t, l_rule)
+     fprintf o "existstype\n (%a)" print_dk_term_aux (t, var_context)
   | Dktrue -> fprintf o "⊤"
   | Dkfalse -> fprintf o "⊥"
   | Dkequal (_, t2, t3) ->
      fprintf o "(%a) =α (%a)"
-	     print_dk_term_aux (t2, l_rule)
-	     print_dk_term_aux (t3, l_rule)
-  | DkRfalse (pr) -> fprintf o "Rfalse\n (%a)" print_dk_term_aux (pr, l_rule)
-  | DkRnottrue (pr) -> fprintf o "Rnottrue\n (%a)" print_dk_term_aux (pr, l_rule)
+	     print_dk_term_aux (t2, var_context)
+	     print_dk_term_aux (t3, var_context)
+  | DkRfalse (pr) -> fprintf o "Rfalse\n (%a)" print_dk_term_aux (pr, var_context)
+  | DkRnottrue (pr) -> fprintf o "Rnottrue\n (%a)" print_dk_term_aux (pr, var_context)
   | DkRaxiom (p, pr1, pr2) ->
      fprintf o "Raxiom\n (%a)\n (%a)\n (%a)\n"
-	     print_dk_term_aux (p, l_rule)
-	     print_dk_term_aux (pr1, l_rule)
-	     print_dk_term_aux (pr2, l_rule)
+	     print_dk_term_aux (p, var_context)
+	     print_dk_term_aux (pr1, var_context)
+	     print_dk_term_aux (pr2, var_context)
   | DkRnoteq (a, t, pr) ->
      fprintf o "Rnoteq\n (%a)\n (%a)\n (%a)\n"
-	     print_dk_zentype_aux (a, l_rule)
-	     print_dk_term_aux (t, l_rule)
-	     print_dk_term_aux (pr, l_rule)
+	     print_dk_zentype_aux (a, var_context)
+	     print_dk_term_aux (t, var_context)
+	     print_dk_term_aux (pr, var_context)
   | DkReqsym (a, t, u, pr1, pr2) ->
      fprintf o "Reqsym\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
-	     print_dk_zentype_aux (a, l_rule)
-	     print_dk_term_aux (t, l_rule)
-	     print_dk_term_aux (u, l_rule)
-	     print_dk_term_aux (pr1, l_rule)
-	     print_dk_term_aux (pr2, l_rule)
+	     print_dk_zentype_aux (a, var_context)
+	     print_dk_term_aux (t, var_context)
+	     print_dk_term_aux (u, var_context)
+	     print_dk_term_aux (pr1, var_context)
+	     print_dk_term_aux (pr2, var_context)
   | DkRcut (p, pr1, pr2) ->
      fprintf o "Rcut\n (%a)\n (%a)\n (%a)\n"
-	     print_dk_term_aux (p, l_rule)
-	     print_dk_term_aux (pr1, l_rule)
-	     print_dk_term_aux (pr2, l_rule)
+	     print_dk_term_aux (p, var_context)
+	     print_dk_term_aux (pr1, var_context)
+	     print_dk_term_aux (pr2, var_context)
   | DkRnotnot (p, pr1, pr2) ->
      fprintf o "Rnotnot\n (%a)\n (%a)\n (%a)\n"
-	     print_dk_term_aux (p, l_rule)
-	     print_dk_term_aux (pr1, l_rule)
-	     print_dk_term_aux (pr2, l_rule)
+	     print_dk_term_aux (p, var_context)
+	     print_dk_term_aux (pr1, var_context)
+	     print_dk_term_aux (pr2, var_context)
   | DkRand (p, q, pr1, pr2) ->
      fprintf o "Rand\n (%a)\n (%a)\n (%a)\n (%a)\n"
-	     print_dk_term_aux (p, l_rule)
-	     print_dk_term_aux (q, l_rule)
-	     print_dk_term_aux (pr1, l_rule)
-	     print_dk_term_aux (pr2, l_rule)
+	     print_dk_term_aux (p, var_context)
+	     print_dk_term_aux (q, var_context)
+	     print_dk_term_aux (pr1, var_context)
+	     print_dk_term_aux (pr2, var_context)
   | DkRor (p, q, pr1, pr2, pr3) ->
      fprintf o "Ror\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
-	     print_dk_term_aux (p, l_rule)
-	     print_dk_term_aux (q, l_rule)
-	     print_dk_term_aux (pr1, l_rule)
-	     print_dk_term_aux (pr2, l_rule)
-	     print_dk_term_aux (pr3, l_rule)
+	     print_dk_term_aux (p, var_context)
+	     print_dk_term_aux (q, var_context)
+	     print_dk_term_aux (pr1, var_context)
+	     print_dk_term_aux (pr2, var_context)
+	     print_dk_term_aux (pr3, var_context)
   | DkRimply (p, q, pr1, pr2, pr3) ->
      fprintf o "Rimply\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
-	     print_dk_term_aux (p, l_rule)
-	     print_dk_term_aux (q, l_rule)
-	     print_dk_term_aux (pr1, l_rule)
-	     print_dk_term_aux (pr2, l_rule)
-	     print_dk_term_aux (pr3, l_rule)
+	     print_dk_term_aux (p, var_context)
+	     print_dk_term_aux (q, var_context)
+	     print_dk_term_aux (pr1, var_context)
+	     print_dk_term_aux (pr2, var_context)
+	     print_dk_term_aux (pr3, var_context)
   | DkRequiv (p, q, pr1, pr2, pr3) ->
      fprintf o "Requiv\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
-	     print_dk_term_aux (p, l_rule)
-	     print_dk_term_aux (q, l_rule)
-	     print_dk_term_aux (pr1, l_rule)
-	     print_dk_term_aux (pr2, l_rule)
-	     print_dk_term_aux (pr3, l_rule)
+	     print_dk_term_aux (p, var_context)
+	     print_dk_term_aux (q, var_context)
+	     print_dk_term_aux (pr1, var_context)
+	     print_dk_term_aux (pr2, var_context)
+	     print_dk_term_aux (pr3, var_context)
   | DkRnotand (p, q, pr1, pr2, pr3) ->
      fprintf o "Rnotand\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
-	     print_dk_term_aux (p, l_rule)
-	     print_dk_term_aux (q, l_rule)
-	     print_dk_term_aux (pr1, l_rule)
-	     print_dk_term_aux (pr2, l_rule)
-	     print_dk_term_aux (pr3, l_rule)
+	     print_dk_term_aux (p, var_context)
+	     print_dk_term_aux (q, var_context)
+	     print_dk_term_aux (pr1, var_context)
+	     print_dk_term_aux (pr2, var_context)
+	     print_dk_term_aux (pr3, var_context)
   | DkRnotor (p, q, pr1, pr2) ->
      fprintf o "Rnotor\n (%a)\n (%a)\n (%a)\n (%a)\n"
-	     print_dk_term_aux (p, l_rule)
-	     print_dk_term_aux (q, l_rule)
-	     print_dk_term_aux (pr1, l_rule)
-	     print_dk_term_aux (pr2, l_rule)
+	     print_dk_term_aux (p, var_context)
+	     print_dk_term_aux (q, var_context)
+	     print_dk_term_aux (pr1, var_context)
+	     print_dk_term_aux (pr2, var_context)
   | DkRnotimply (p, q, pr1, pr2) ->
      fprintf o "Rnotimply\n (%a)\n (%a)\n (%a)\n (%a)\n"
-	     print_dk_term_aux (p, l_rule)
-	     print_dk_term_aux (q, l_rule)
-	     print_dk_term_aux (pr1, l_rule)
-	     print_dk_term_aux (pr2, l_rule)
+	     print_dk_term_aux (p, var_context)
+	     print_dk_term_aux (q, var_context)
+	     print_dk_term_aux (pr1, var_context)
+	     print_dk_term_aux (pr2, var_context)
   | DkRnotequiv (p, q, pr1, pr2, pr3) ->
      fprintf o "Rnotequiv\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
-	     print_dk_term_aux (p, l_rule)
-	     print_dk_term_aux (q, l_rule)
-	     print_dk_term_aux (pr1, l_rule)
-	     print_dk_term_aux (pr2, l_rule)
-	     print_dk_term_aux (pr3, l_rule)
+	     print_dk_term_aux (p, var_context)
+	     print_dk_term_aux (q, var_context)
+	     print_dk_term_aux (pr1, var_context)
+	     print_dk_term_aux (pr2, var_context)
+	     print_dk_term_aux (pr3, var_context)
   | DkRex (a, p, pr1, pr2) ->
      fprintf o "Rex\n (%a)\n (%a)\n (%a)\n (%a)\n"
-	     print_dk_zentype_aux (a, l_rule)
-	     print_dk_term_aux (p, l_rule)
-	     print_dk_term_aux (pr1, l_rule)
-	     print_dk_term_aux (pr2, l_rule)
+	     print_dk_zentype_aux (a, var_context)
+	     print_dk_term_aux (p, var_context)
+	     print_dk_term_aux (pr1, var_context)
+	     print_dk_term_aux (pr2, var_context)
   | DkRall (a, p, t, pr1, pr2) ->
      fprintf o "Rall\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
-	     print_dk_zentype_aux (a, l_rule)
-	     print_dk_term_aux (p, l_rule)
-	     print_dk_term_aux (t, l_rule)
-	     print_dk_term_aux (pr1, l_rule)
-	     print_dk_term_aux (pr2, l_rule)
+	     print_dk_zentype_aux (a, var_context)
+	     print_dk_term_aux (p, var_context)
+	     print_dk_term_aux (t, var_context)
+	     print_dk_term_aux (pr1, var_context)
+	     print_dk_term_aux (pr2, var_context)
   | DkRnotex (a, p, t, pr1, pr2) ->
      fprintf o "Rnotex\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
-	     print_dk_zentype_aux (a, l_rule)
-	     print_dk_term_aux (p, l_rule)
-	     print_dk_term_aux (t, l_rule)
-	     print_dk_term_aux (pr1, l_rule)
-	     print_dk_term_aux (pr2, l_rule)
+	     print_dk_zentype_aux (a, var_context)
+	     print_dk_term_aux (p, var_context)
+	     print_dk_term_aux (t, var_context)
+	     print_dk_term_aux (pr1, var_context)
+	     print_dk_term_aux (pr2, var_context)
   | DkRnotall (a, p, pr1, pr2) ->
      fprintf o "Rnotall\n (%a)\n (%a)\n (%a)\n (%a)\n"
-	     print_dk_zentype_aux (a, l_rule)
-	     print_dk_term_aux (p, l_rule)
-	     print_dk_term_aux (pr1, l_rule)
-	     print_dk_term_aux (pr2, l_rule)
+	     print_dk_zentype_aux (a, var_context)
+	     print_dk_term_aux (p, var_context)
+	     print_dk_term_aux (pr1, var_context)
+	     print_dk_term_aux (pr2, var_context)
   | DkRextype (p, pr1, pr2) ->
      fprintf o "Rextype\n (%a)\n (%a)\n (%a)\n"
-	     print_dk_term_aux (p, l_rule)
-	     print_dk_term_aux (pr1, l_rule)
-	     print_dk_term_aux (pr2, l_rule)
+	     print_dk_term_aux (p, var_context)
+	     print_dk_term_aux (pr1, var_context)
+	     print_dk_term_aux (pr2, var_context)
   | DkRalltype (p, a, pr1, pr2) ->
      fprintf o "Ralltype\n (%a)\n (%a)\n (%a)\n (%a)\n"
-	     print_dk_term_aux (p, l_rule)
-	     print_dk_zentype_aux (a, l_rule)
-	     print_dk_term_aux (pr1, l_rule)
-	     print_dk_term_aux (pr2, l_rule)
+	     print_dk_term_aux (p, var_context)
+	     print_dk_zentype_aux (a, var_context)
+	     print_dk_term_aux (pr1, var_context)
+	     print_dk_term_aux (pr2, var_context)
   | DkRnotextype (p, a, pr1, pr2) ->
      fprintf o "Rnotextype\n (%a)\n (%a)\n (%a)\n (%a)\n"
-	     print_dk_term_aux (p, l_rule)
-	     print_dk_zentype_aux (a, l_rule)
-	     print_dk_term_aux (pr1, l_rule)
-	     print_dk_term_aux (pr2, l_rule)
+	     print_dk_term_aux (p, var_context)
+	     print_dk_zentype_aux (a, var_context)
+	     print_dk_term_aux (pr1, var_context)
+	     print_dk_term_aux (pr2, var_context)
   | DkRnotalltype (p, pr1, pr2) ->
      fprintf o "Rnotalltype\n (%a)\n (%a)\n (%a)\n"
-	     print_dk_term_aux (p, l_rule)
-	     print_dk_term_aux (pr1, l_rule)
-	     print_dk_term_aux (pr2, l_rule)
+	     print_dk_term_aux (p, var_context)
+	     print_dk_term_aux (pr1, var_context)
+	     print_dk_term_aux (pr2, var_context)
   | DkRsubst  (a, p, t1, t2, pr1, pr2, pr3) ->
      fprintf o "Rsubst\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
-	     print_dk_zentype_aux (a, l_rule)
-	     print_dk_term_aux (p, l_rule)
-	     print_dk_term_aux (t1, l_rule)
-	     print_dk_term_aux (t2, l_rule)
-	     print_dk_term_aux (pr1, l_rule)
-	     print_dk_term_aux (pr2, l_rule)
-	     print_dk_term_aux (pr3, l_rule)
+	     print_dk_zentype_aux (a, var_context)
+	     print_dk_term_aux (p, var_context)
+	     print_dk_term_aux (t1, var_context)
+	     print_dk_term_aux (t2, var_context)
+	     print_dk_term_aux (pr1, var_context)
+	     print_dk_term_aux (pr2, var_context)
+	     print_dk_term_aux (pr3, var_context)
   | DkRconglr (a, p, t1, t2, pr1, pr2, pr3) ->
      fprintf o "Rconglr\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
-	     print_dk_zentype_aux (a, l_rule)
-	     print_dk_term_aux (p, l_rule)
-	     print_dk_term_aux (t1, l_rule)
-	     print_dk_term_aux (t2, l_rule)
-	     print_dk_term_aux (pr1, l_rule)
-	     print_dk_term_aux (pr2, l_rule)
-	     print_dk_term_aux (pr3, l_rule)
+	     print_dk_zentype_aux (a, var_context)
+	     print_dk_term_aux (p, var_context)
+	     print_dk_term_aux (t1, var_context)
+	     print_dk_term_aux (t2, var_context)
+	     print_dk_term_aux (pr1, var_context)
+	     print_dk_term_aux (pr2, var_context)
+	     print_dk_term_aux (pr3, var_context)
   | DkRcongrl (a, p, t1, t2, pr1, pr2, pr3) ->
      fprintf o "Rcongrl\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
-	     print_dk_zentype_aux (a, l_rule)
-	     print_dk_term_aux (p, l_rule)
-	     print_dk_term_aux (t1, l_rule)
-	     print_dk_term_aux (t2, l_rule)
-	     print_dk_term_aux (pr1, l_rule)
-	     print_dk_term_aux (pr2, l_rule)
-	     print_dk_term_aux (pr3, l_rule)
+	     print_dk_zentype_aux (a, var_context)
+	     print_dk_term_aux (p, var_context)
+	     print_dk_term_aux (t1, var_context)
+	     print_dk_term_aux (t2, var_context)
+	     print_dk_term_aux (pr1, var_context)
+	     print_dk_term_aux (pr2, var_context)
+	     print_dk_term_aux (pr3, var_context)
   | _ -> assert false
  and print_dk_term o t = print_dk_term_aux o (t, [])
 

From 5b82f2d579f5ec5a24be6f44f4453c3e8841442a Mon Sep 17 00:00:00 2001
From: Guillaume Burel <guillaume.burel@inria.fr>
Date: Mon, 15 Jul 2024 00:38:22 +0200
Subject: [PATCH 3/9] More close to real TPTP syntax of annotations. (Still
 missing: formula_data, and semantic verification.)

---
 parsetptp.mly | 58 +++++++++++++++++++++++++++++++++++++++++----------
 1 file changed, 47 insertions(+), 11 deletions(-)

diff --git a/parsetptp.mly b/parsetptp.mly
index 14769bb..34d634d 100644
--- a/parsetptp.mly
+++ b/parsetptp.mly
@@ -99,27 +99,63 @@ phrase:
   | INCLUDE OPEN LIDENT CLOSE DOT  { Phrase.Include ($3, None) }
   | INCLUDE OPEN LIDENT COMMA LBRACKET name_list RBRACKET CLOSE DOT
                                    { Phrase.Include ($3, Some ($6)) }
-  | INPUT_FORMULA OPEN name COMMA LIDENT COMMA formula extra CLOSE DOT
+  | INPUT_FORMULA OPEN name COMMA LIDENT COMMA formula annotations CLOSE DOT
                                    { Phrase.Formula (ns_hyp $3, $5, $7, None) }
-  | INPUT_CLAUSE OPEN name COMMA LIDENT COMMA cnf_formula extra CLOSE DOT
+  | INPUT_CLAUSE OPEN name COMMA LIDENT COMMA cnf_formula annotations CLOSE DOT
      { Phrase.Formula (ns_hyp $3, $5, cnf_to_formula $7, None) }
-  | INPUT_TFF_FORMULA OPEN name COMMA LIDENT COMMA formula COMMA LIDENT extra CLOSE DOT
+  | INPUT_TFF_FORMULA OPEN name COMMA LIDENT COMMA formula COMMA LIDENT annotations CLOSE DOT
      { Phrase.Formula (ns_hyp $3, "tff_" ^ $5, $7, Some $9) }
-  | INPUT_TFF_FORMULA OPEN name COMMA LIDENT COMMA formula extra CLOSE DOT
+  | INPUT_TFF_FORMULA OPEN name COMMA LIDENT COMMA formula annotations CLOSE DOT
      { Phrase.Formula (ns_hyp $3, "tff_" ^ $5, $7, None) }
-  | INPUT_TFF_FORMULA OPEN name COMMA LIDENT COMMA type_def extra CLOSE DOT
+  | INPUT_TFF_FORMULA OPEN name COMMA LIDENT COMMA type_def annotations CLOSE DOT
      { Phrase.Formula (ns_hyp $3, "tff_" ^ $5, $7, None) }
   | ANNOT                          { Phrase.Annotation $1 }
 ;
-extra:
+annotations:
   | {}
-  | COMMA extra_expr extra {}
+  | COMMA source optional_info {}
 ;
-extra_expr:
-  | expr {}
-  | LBRACKET extra_expr extra RBRACKET {}
-  | LIDENT OPEN LIDENT extra CLOSE {}
+
+source:
+general_term {}
+;
+
+general_term:
+general_data {}
+  | general_data COLON general_term {}
+  | general_list {}
+;
+
+general_data:
+LIDENT {}
+  | general_function {}
+  | UIDENT {}
+  | INT {}
+  | RAT {}
+  | REAL {}
+  | STRING {}
+/* | formula_data {} unsupported */
+;
+
+general_function:
+LIDENT OPEN general_terms CLOSE {}
 ;
+
+general_terms:
+general_term {}
+  | general_term COMMA general_terms {}
+;
+
+general_list:
+LBRACKET RBRACKET {}
+  | LBRACKET general_terms RBRACKET {}
+;
+
+optional_info:
+COMMA general_list {}
+  | {}
+;
+
 expr:
   | UIDENT                             { tvar_none (ns_var $1) }
   | LIDENT arguments                   { eapp (tvar_none @@ ns_fun $1, $2) }

From 346cb8008d6b8f36f541523b30b69fc8b42d5057 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?=
 <fblanqui@users.noreply.github.com>
Date: Tue, 16 Jul 2024 17:26:18 +0200
Subject: [PATCH 4/9] add support for dune (#24)

---
 dune              | 20 ++++++++++++++++++++
 dune-project      | 19 +++++++++++++++++++
 zenon_modulo.opam | 12 +++++-------
 3 files changed, 44 insertions(+), 7 deletions(-)
 create mode 100644 dune
 create mode 100644 dune-project

diff --git a/dune b/dune
new file mode 100644
index 0000000..cc401e0
--- /dev/null
+++ b/dune
@@ -0,0 +1,20 @@
+(env
+ (dev     (flags :standard))
+ (release (flags :standard)))
+
+(ocamllex lexzen lextptp lexsmtlib lexcoq lexdk)
+(ocamlyacc parsezen parsetptp parsecoq parsedk)
+
+(executable
+ (name main)
+ (public_name zenon_modulo)
+ (modes byte native)
+ (libraries str unix zarith)
+)
+
+(rule
+ (targets checksum.ml)
+ (action
+  (with-stdout-to checksum.ml
+    (run echo "let v = \"\"")))
+ (mode fallback))
diff --git a/dune-project b/dune-project
new file mode 100644
index 0000000..65cefca
--- /dev/null
+++ b/dune-project
@@ -0,0 +1,19 @@
+(lang dune 3.7)
+
+(generate_opam_files true)
+
+(name zenon_modulo)
+(source (github Deducteam/zenon_modulo))
+(authors "INRIA and contributors")
+(maintainers "guillaume.burel@ensiie.fr")
+(license BSD-3-Clause)
+
+(package
+ (name zenon_modulo)
+ (synopsis "Automated theorem prover generating formal proofs")
+ (description
+"Automated theorem prover for typed first-order logic based on the tableau
+method, generating Coq, Dedukti or Lambdapi proofs.")
+ (depends
+  (ocaml (>= 4.08.0))
+))
diff --git a/zenon_modulo.opam b/zenon_modulo.opam
index 5cf2bac..5dbcce9 100644
--- a/zenon_modulo.opam
+++ b/zenon_modulo.opam
@@ -1,18 +1,16 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
-version: "0.5.0"
-synopsis: "Zenon Modulo Theory"
+synopsis: "Automated theorem prover generating formal proofs"
 description: """
-Zenon is a first-order automated theorem
- prover based on the tableau method. It is used in the
- FoCaLiZe project."""
-maintainer: ["Guillaume Burel"]
+Automated theorem prover for typed first-order logic based on the tableau
+method, generating Coq, Dedukti or Lambdapi proofs."""
+maintainer: ["guillaume.burel@ensiie.fr"]
 authors: ["INRIA and contributors"]
 license: "BSD-3-Clause"
 homepage: "https://github.com/Deducteam/zenon_modulo"
 bug-reports: "https://github.com/Deducteam/zenon_modulo/issues"
 depends: [
-  "dune" {>= "3.6"}
+  "dune" {>= "3.7"}
   "ocaml" {>= "4.08.0"}
   "odoc" {with-doc}
   "ocamlfind"

From 375d95037504a0869181e0988f2c7d80508a1fd2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?=
 <fblanqui@users.noreply.github.com>
Date: Wed, 17 Jul 2024 09:26:59 +0200
Subject: [PATCH 5/9] change lp output to use the lambdapi-zenon library (#33)

---
 lpprint.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/lpprint.ml b/lpprint.ml
index 93830c7..1142c48 100644
--- a/lpprint.ml
+++ b/lpprint.ml
@@ -82,7 +82,7 @@ let escape_name s =
 
 let rec print_dk_type_aux o (t, var_context) =
   match t with
-  | Dktypetype -> fprintf o "Type"
+  | Dktypetype -> fprintf o "Set"
   | Dktypeprop -> fprintf o "Prop"
   | Dkarrow (l, r) ->
      begin
@@ -95,7 +95,7 @@ let rec print_dk_type_aux o (t, var_context) =
 	      pvar print_dk_type_aux (t1, var_context) print_dk_type_aux (t2, pvar::var_context)
   | Dkpi _ -> assert false
   | Dkproof (t) ->
-     fprintf o "ϵ (%a)" print_dk_term_aux (t, var_context)
+     fprintf o "π (%a)" print_dk_term_aux (t, var_context)
   | t -> fprintf o "τ (%a)" print_dk_zentype_aux (t, var_context)
 and print_dk_type o t = print_dk_type_aux o (t, [])
 and print_dk_zentype_aux o (t, l) =
@@ -140,7 +140,7 @@ and print_dk_term_aux o (t, var_context) =
        List.iter (fun x -> fprintf o " (%a)" print_dk_term_aux (x, var_context)) l;
 (*       fprintf o "\n ";*)
      end
-  | Dkseq -> fprintf o "ϵ ⊥"
+  | Dkseq -> fprintf o "π ⊥"
   | Dknot (t) ->
      fprintf o "¬\n (%a)" print_dk_term_aux  (t, var_context)
   | Dkand (t1, t2) ->
@@ -152,10 +152,10 @@ and print_dk_term_aux o (t, var_context) =
   | Dkequiv (t1, t2) ->
      fprintf o "(%a)\n⇔\n(%a)\n" print_dk_term_aux (t1, var_context) print_dk_term_aux (t2, var_context)
   | Dkforall (_, t2) ->
-     fprintf o "∀α (%a)" print_dk_term_aux (t2, var_context)
+     fprintf o "∀ (%a)" print_dk_term_aux (t2, var_context)
      (* fprintf o "@∀ (%a)\n (%a)" print_dk_zentype_aux (t1, var_context) print_dk_term_aux (t2, var_context) *)
   | Dkexists (_, t2) ->
-     fprintf o "∃α (%a)" print_dk_term_aux (t2, var_context)
+     fprintf o "∃ (%a)" print_dk_term_aux (t2, var_context)
      (* fprintf o "@∃ (%a)\n (%a)" print_dk_zentype_aux  (t1, var_context) print_dk_term_aux (t2, var_context) *)
   | Dkforalltype (t) ->
      fprintf o "foralltype\n (%a)" print_dk_term_aux (t, var_context)
@@ -164,7 +164,7 @@ and print_dk_term_aux o (t, var_context) =
   | Dktrue -> fprintf o "⊤"
   | Dkfalse -> fprintf o "⊥"
   | Dkequal (_, t2, t3) ->
-     fprintf o "(%a) =α (%a)"
+     fprintf o "(%a) = (%a)"
 	     print_dk_term_aux (t2, var_context)
 	     print_dk_term_aux (t3, var_context)
   | DkRfalse (pr) -> fprintf o "Rfalse\n (%a)" print_dk_term_aux (pr, var_context)

From b88bbaea37df5d6964bcf21439b4f9175ff0f44c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?=
 <fblanqui@users.noreply.github.com>
Date: Wed, 17 Jul 2024 14:05:22 +0200
Subject: [PATCH 6/9] lltolp.ml: fix requires for lambdapi-zenon library (#35)

---
 lltolp.ml | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/lltolp.ml b/lltolp.ml
index 81b50a7..83fab8c 100644
--- a/lltolp.ml
+++ b/lltolp.ml
@@ -1030,7 +1030,8 @@ let output oc phrases llp =
   let dkname = List.hd name in
   let prooftree = extract_prooftree llp in
   let dkproof = make_proof_term (List.hd goal) prooftree in
-  fprintf oc "require open Logic.Zenon.FOL Logic.Zenon.LL Logic.Zenon.ND Logic.Zenon.ND_eps Logic.Zenon.ND_eps_full Logic.Zenon.ND_eps_aux Logic.Zenon.LL_ND Logic.Zenon.zen;\n\n";
+  fprintf oc "require open Stdlib.Prop Stdlib.Set Stdlib.Eq Stdlib.FOL \
+              Logic.Zenon.Main;\n\n";
   if !Globals.signature_name = "" then List.iter (print_line oc) dksigs;
   fprintf oc "\n";
   if !Globals.signature_name = "" then List.iter (print_line oc) dkctx;
@@ -1058,8 +1059,10 @@ let output_term oc phrases _ llp =
   let prooftree = extract_prooftree llp in
   let goal_name = (List.hd llp).name in
   let dkproof = make_proof_term (List.hd goal) prooftree in
-  fprintf oc "require open Logic.Zenon.FOL Logic.Zenon.LL Logic.Zenon.ND Logic.Zenon.ND_eps Logic.Zenon.ND_eps_full Logic.Zenon.ND_eps_aux Logic.Zenon.LL_ND Logic.Zenon.zen;\n";
-  if !Globals.signature_name <> "" then fprintf oc "require %s as S;\n" !Globals.signature_name;
+  fprintf oc "require open Stdlib.Prop Stdlib.Set Stdlib.Eq Stdlib.FOL \
+              Logic.Zenon.Main;\n";
+  if !Globals.signature_name <> "" then
+    fprintf oc "require %s as S;\n" !Globals.signature_name;
   fprintf oc "\nrule S.%s ↪ " goal_name;
   let n = !Globals.neg_conj in
   if n <> "" then fprintf oc "λ %s,\n" n;

From 84d23e9c50863d6d378fc751b52e793f85cbf45e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?=
 <fblanqui@users.noreply.github.com>
Date: Thu, 18 Jul 2024 15:47:46 +0200
Subject: [PATCH 7/9] rename dummy_var into negated_conjecture (#36)

---
 main.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/main.ml b/main.ml
index 6adde0d..b624342 100644
--- a/main.ml
+++ b/main.ml
@@ -184,7 +184,7 @@ let argspec = [
             "           print the proof in lambdapi term format";
   "-conj", Arg.Unit (fun () -> Globals.neg_conj :=
                                  (* keep space at the beginning *)
-                                 " __dummy_var__"),
+                                 " __negated_conjecture__"),
       "              indicate whether there is an explicit conjecture";
   "-check-axiom", Arg.Unit (fun () -> Globals.check_axiom := true),
       "       indicate whether this is a GDV leaf problem";

From 2e812e87af42e845858c1dd1a4d407e2337aad3d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?=
 <fblanqui@users.noreply.github.com>
Date: Fri, 19 Jul 2024 16:59:09 +0200
Subject: [PATCH 8/9] fix dk output for GDV (#37)

---
 Makefile    |   2 +-
 dkprint.ml  | 147 ++++++++++++++++++++++++++++++---------------
 globals.ml  |   2 +-
 globals.mli |   2 +-
 lltodk.ml   |  21 +++++--
 lltolp.ml   |  14 ++---
 lpprint.ml  |  12 ++--
 main.ml     |   4 +-
 zenon.dk    | 169 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 9 files changed, 301 insertions(+), 72 deletions(-)
 create mode 100644 zenon.dk

diff --git a/Makefile b/Makefile
index 183facb..7b6132a 100644
--- a/Makefile
+++ b/Makefile
@@ -41,7 +41,7 @@ SOURCES = log.ml version.ml config.dummy misc.ml heap.ml globals.ml error.ml \
 
 COQSRC = zenon.v zenon_coqbool.v zenon_equiv.v zenon_induct.v zenon_focal.v zenon_arith.v zenon_arith_reals.v
 
-DKSRC = cc.dk dk_bool.dk dk_logic.dk dk_tuple.dk basics_minimal.dk zen.dk zenon_focal.dk
+DKSRC = cc.dk dk_bool.dk dk_logic.dk dk_tuple.dk basics_minimal.dk zen.dk zenon_focal.dk zenon.dk
 
 DOCSRC =
 
diff --git a/dkprint.ml b/dkprint.ml
index 4a353b8..a182b6b 100644
--- a/dkprint.ml
+++ b/dkprint.ml
@@ -1,10 +1,56 @@
 open Printf
 open Dkterm
 
+(* taken on 19/07/24 from
+https://github.com/Deducteam/Dedukti/blob/master/parsing/lexer.mll *)
+let forbidden_idents = [
+  "(;"
+  ; ";)"
+  ; "."
+  ; ","
+  ; ":"
+  ; "=="
+  ; "["
+  ; "]"
+  ; "{"
+  ; "}"
+  ; "("
+  ; ")"
+  ; "-->"
+  ; "->"
+  ; "=>"
+  ; ":="
+  ; "Type"
+  ; "def"
+  ; "defac"
+  ; "defacu"
+  ; "injective"
+  ; "thm"
+  ; "private"
+  ; "require"
+  ; "assert"
+  ; "#NAME"
+  ; "#REQUIRE"
+  ; "#EVAL"
+  ; "#INFER"
+  ; "#CHECK"
+  ; "#CHECKNOT"
+  ; "#ASSERT"
+  ; "#ASSERTNOT"
+  ; "#PRINT"
+  ; "#GDT"
+  ]
+
+let escape_name s =
+  let id_regex = Str.regexp "^[a-zA-Z_][a-zA-Z0-9_]*$" in
+  if Str.string_match id_regex s 0
+    && List.for_all ((<>) s) forbidden_idents
+    then s else "{|" ^ s ^ "|}"
+
 let rec print_dk_type o t =
   match t with
-  | Dktypetype -> fprintf o "zen.type"
-  | Dktypeprop -> fprintf o "zen.prop"
+  | Dktypetype -> fprintf o "zenon.type"
+  | Dktypeprop -> fprintf o "zenon.prop"
   | Dkarrow (l, r) ->
      begin
        List.iter (fun x -> fprintf o "%a -> " print_dk_type x) l;
@@ -15,21 +61,28 @@ let rec print_dk_type o t =
 	     (get_var_newname var) print_dk_type t1 print_dk_type t2
   | Dkpi _ -> assert false
   | Dkproof (t) ->
-     fprintf o "zen.proof (%a)" print_dk_term t
-  | t -> fprintf o "zen.term (%a)" print_dk_zentype t
+     fprintf o "zenon.proof (%a)" print_dk_term t
+  | t -> fprintf o "zenon.term (%a)" print_dk_zentype t
 
 and print_dk_zentype o t =
   match t with
-  | Dktypeiota -> fprintf o "zen.iota"
+  | Dktypeiota -> fprintf o "zenon.iota"
   | t -> print_dk_term o t
 
 and print_dk_cst o t =
   match t with
   | "Is_true" -> fprintf o "dk_logic.ebP"
   | "FOCAL.ifthenelse" -> fprintf o "dk_bool.ite"
-  | s -> if !Globals.signature_name = "" then fprintf o "%s" s else
-    if Mltoll.is_meta s then fprintf o "zen.select (zen.iota)" else
-      fprintf o "%s.%s" !Globals.signature_name s
+  | s ->
+     if Mltoll.is_meta s then fprintf o "zenon.select (zenon.iota)"
+     else
+       begin
+         if !Globals.signature_name = "" then fprintf o "%s" (escape_name s)
+         else fprintf o "%s.%s" !Globals.signature_name (escape_name s);
+         if !Globals.conjecture <> ""
+            && not !Globals.check_axiom && Typetptp.is_axiom s then
+           fprintf o " __negated_conjecture_proof__"
+       end
 
 and print_dk_term o t =
   match t with
@@ -49,164 +102,164 @@ and print_dk_term o t =
        List.iter (fun x -> fprintf o " (%a)" print_dk_term x) l;
 (*       fprintf o "\n ";*)
      end
-  | Dkseq -> fprintf o "zen.seq"
+  | Dkseq -> fprintf o "zenon.seq"
   | Dknot (t) ->
-     fprintf o "zen.not\n (%a)" print_dk_term t
+     fprintf o "zenon.not\n (%a)" print_dk_term t
   | Dkand (t1, t2) ->
-     fprintf o "zen.and\n (%a) (%a)" print_dk_term t1 print_dk_term t2
+     fprintf o "zenon.and\n (%a) (%a)" print_dk_term t1 print_dk_term t2
   | Dkor (t1, t2) ->
-     fprintf o "zen.or\n (%a) (%a)" print_dk_term t1 print_dk_term t2
+     fprintf o "zenon.or\n (%a) (%a)" print_dk_term t1 print_dk_term t2
   | Dkimply (t1, t2) ->
-     fprintf o "zen.imp\n (%a) (%a)" print_dk_term t1 print_dk_term t2
+     fprintf o "zenon.imp\n (%a) (%a)" print_dk_term t1 print_dk_term t2
   | Dkequiv (t1, t2) ->
-     fprintf o "zen.eqv\n (%a) (%a)" print_dk_term t1 print_dk_term t2
+     fprintf o "zenon.eqv\n (%a) (%a)" print_dk_term t1 print_dk_term t2
   | Dkforall (t1, t2) ->
-     fprintf o "zen.forall (%a)\n (%a)" print_dk_zentype t1 print_dk_term t2
+     fprintf o "zenon.forall (%a)\n (%a)" print_dk_zentype t1 print_dk_term t2
   | Dkexists (t1, t2) ->
-     fprintf o "zen.exists (%a)\n (%a)" print_dk_zentype t1 print_dk_term t2
+     fprintf o "zenon.exists (%a)\n (%a)" print_dk_zentype t1 print_dk_term t2
   | Dkforalltype (t) ->
-     fprintf o "zen.foralltype\n (%a)" print_dk_term t
+     fprintf o "zenon.foralltype\n (%a)" print_dk_term t
   | Dkexiststype (t) ->
-     fprintf o "zen.existstype\n (%a)" print_dk_term t
-  | Dktrue -> fprintf o "zen.True"
-  | Dkfalse -> fprintf o "zen.False"
+     fprintf o "zenon.existstype\n (%a)" print_dk_term t
+  | Dktrue -> fprintf o "zenon.True"
+  | Dkfalse -> fprintf o "zenon.False"
   | Dkequal (t1, t2, t3) ->
-     fprintf o "zen.equal (%a)\n (%a)\n (%a)"
+     fprintf o "zenon.equal (%a)\n (%a)\n (%a)"
 	     print_dk_zentype t1
 	     print_dk_term t2
 	     print_dk_term t3
-  | DkRfalse (pr) -> fprintf o "zen.Rfalse\n (%a)" print_dk_term pr
-  | DkRnottrue (pr) -> fprintf o "zen.Rnottrue\n (%a)" print_dk_term pr
+  | DkRfalse (pr) -> fprintf o "zenon.Rfalse\n (%a)" print_dk_term pr
+  | DkRnottrue (pr) -> fprintf o "zenon.Rnottrue\n (%a)" print_dk_term pr
   | DkRaxiom (p, pr1, pr2) ->
-     fprintf o "zen.Raxiom\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Raxiom\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRnoteq (a, t, pr) ->
-     fprintf o "zen.Rnoteq\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rnoteq\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_zentype a
 	     print_dk_term t
 	     print_dk_term pr
   | DkReqsym (a, t, u, pr1, pr2) ->
-     fprintf o "zen.Reqsym\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Reqsym\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_zentype a
 	     print_dk_term t
 	     print_dk_term u
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRcut (p, pr1, pr2) ->
-     fprintf o "zen.Rcut\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rcut\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRnotnot (p, pr1, pr2) ->
-     fprintf o "zen.Rnotnot\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rnotnot\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRand (p, q, pr1, pr2) ->
-     fprintf o "zen.Rand\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rand\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_term q
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRor (p, q, pr1, pr2, pr3) ->
-     fprintf o "zen.Ror\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Ror\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_term q
 	     print_dk_term pr1
 	     print_dk_term pr2
 	     print_dk_term pr3
   | DkRimply (p, q, pr1, pr2, pr3) ->
-     fprintf o "zen.Rimply\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rimply\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_term q
 	     print_dk_term pr1
 	     print_dk_term pr2
 	     print_dk_term pr3
   | DkRequiv (p, q, pr1, pr2, pr3) ->
-     fprintf o "zen.Requiv\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Requiv\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_term q
 	     print_dk_term pr1
 	     print_dk_term pr2
 	     print_dk_term pr3
   | DkRnotand (p, q, pr1, pr2, pr3) ->
-     fprintf o "zen.Rnotand\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rnotand\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_term q
 	     print_dk_term pr1
 	     print_dk_term pr2
 	     print_dk_term pr3
   | DkRnotor (p, q, pr1, pr2) ->
-     fprintf o "zen.Rnotor\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rnotor\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_term q
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRnotimply (p, q, pr1, pr2) ->
-     fprintf o "zen.Rnotimply\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rnotimply\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_term q
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRnotequiv (p, q, pr1, pr2, pr3) ->
-     fprintf o "zen.Rnotequiv\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rnotequiv\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_term q
 	     print_dk_term pr1
 	     print_dk_term pr2
 	     print_dk_term pr3
   | DkRex (a, p, pr1, pr2) ->
-     fprintf o "zen.Rex\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rex\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_zentype a
 	     print_dk_term p
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRall (a, p, t, pr1, pr2) ->
-     fprintf o "zen.Rall\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rall\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_zentype a
 	     print_dk_term p
 	     print_dk_term t
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRnotex (a, p, t, pr1, pr2) ->
-     fprintf o "zen.Rnotex\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rnotex\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_zentype a
 	     print_dk_term p
 	     print_dk_term t
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRnotall (a, p, pr1, pr2) ->
-     fprintf o "zen.Rnotall\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rnotall\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_zentype a
 	     print_dk_term p
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRextype (p, pr1, pr2) ->
-     fprintf o "zen.Rextype\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rextype\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRalltype (p, a, pr1, pr2) ->
-     fprintf o "zen.Ralltype\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Ralltype\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_zentype a
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRnotextype (p, a, pr1, pr2) ->
-     fprintf o "zen.Rnotextype\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rnotextype\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_zentype a
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRnotalltype (p, pr1, pr2) ->
-     fprintf o "zen.Rnotalltype\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rnotalltype\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRsubst  (a, p, t1, t2, pr1, pr2, pr3) ->
-     fprintf o "zen.Rsubst\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rsubst\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_zentype a
 	     print_dk_term p
 	     print_dk_term t1
@@ -215,7 +268,7 @@ and print_dk_term o t =
 	     print_dk_term pr2
 	     print_dk_term pr3
   | DkRconglr (a, p, t1, t2, pr1, pr2, pr3) ->
-     fprintf o "zen.Rconglr\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rconglr\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_zentype a
 	     print_dk_term p
 	     print_dk_term t1
@@ -224,7 +277,7 @@ and print_dk_term o t =
 	     print_dk_term pr2
 	     print_dk_term pr3
   | DkRcongrl (a, p, t1, t2, pr1, pr2, pr3) ->
-     fprintf o "zen.Rcongrl\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rcongrl\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_zentype a
 	     print_dk_term p
 	     print_dk_term t1
diff --git a/globals.ml b/globals.ml
index 3ad0ad6..54e8a08 100644
--- a/globals.ml
+++ b/globals.ml
@@ -31,7 +31,7 @@ let debug_rwrt = ref false;;
 
 let output_sig = ref false;;
 let signature_name = ref "";;
-let neg_conj = ref "";;
+let conjecture = ref "";;
 let check_axiom = ref false;;
 
 let begin_comment() =
diff --git a/globals.mli b/globals.mli
index 6d918d4..f266da4 100644
--- a/globals.mli
+++ b/globals.mli
@@ -31,7 +31,7 @@ val debug_rwrt : bool ref;;
 
 val output_sig : bool ref;;
 val signature_name : string ref;;
-val neg_conj : string ref;;
+val conjecture : string ref;;
 val check_axiom : bool ref;;
 
 val begin_comment : unit -> string;;
diff --git a/lltodk.ml b/lltodk.ml
index d77097f..8aeaee5 100644
--- a/lltodk.ml
+++ b/lltodk.ml
@@ -1033,7 +1033,7 @@ let output oc phrases llp =
   let dkname = List.hd name in
   let prooftree = extract_prooftree llp in
   let dkproof = make_proof_term (List.hd goal) prooftree in
-
+  fprintf oc "#REQUIRE zenon;\n\n";
   if !Globals.signature_name = "" then List.iter (print_line oc) dksigs;
   fprintf oc "\n";
   if !Globals.signature_name = "" then List.iter (print_line oc) dkctx;
@@ -1058,10 +1058,19 @@ let output_term oc phrases _ llp =
   in
   let dkgoal = translate_expr ngoal in
   let prooftree = extract_prooftree llp in
+  let goal_name = (List.hd llp).name in
   let dkproof = make_proof_term (List.hd goal) prooftree in
-  if !Globals.signature_name = "" then () else fprintf oc "def delta : zen.proof (%a) \n := \n " print_dk_term dkgoal;
-  fprintf oc "zen.nnpp (%a)\n\n(%a)"
-	  print_dk_term dkgoal
-	  print_dk_term dkproof;
-    if !Globals.signature_name = "" then () else fprintf oc ".";
+  fprintf oc "#REQUIRE zenon.\n";
+  if !Globals.signature_name <> "" then
+    begin
+      fprintf oc "#REQUIRE %s.\n" !Globals.signature_name;
+      fprintf oc "\n[] %s.%s --> " !Globals.signature_name goal_name
+    end
+  else fprintf oc "\n[] %s --> " goal_name;
+  if !Globals.conjecture <> "" then
+    fprintf oc "__negated_conjecture_proof__ : \
+                zenon.proof (zenon.not Signature.conjecture) =>\n";
+  fprintf oc "zenon.nnpp (%a)\n(%a)"
+    print_dk_term dkgoal print_dk_term dkproof;
+  if !Globals.signature_name <> "" then fprintf oc ".";
   []
diff --git a/lltolp.ml b/lltolp.ml
index 83fab8c..ecedbdb 100644
--- a/lltolp.ml
+++ b/lltolp.ml
@@ -1064,15 +1064,15 @@ let output_term oc phrases _ llp =
   if !Globals.signature_name <> "" then
     fprintf oc "require %s as S;\n" !Globals.signature_name;
   fprintf oc "\nrule S.%s ↪ " goal_name;
-  let n = !Globals.neg_conj in
-  if n <> "" then fprintf oc "λ %s,\n" n;
+  if !Globals.conjecture <> "" then
+    fprintf oc "λ __negated_conjecture_proof__,";
   begin
     match dkgoal with
-    | Some g -> fprintf oc "\n  nnpp (%a)\n    (%a);\n"
-	          print_dk_term g
-	          print_dk_term dkproof
-    | None -> fprintf oc "\n %a;\n"
-	        print_dk_term dkproof
+    | Some g ->
+       fprintf oc "\n  nnpp (%a)\n    (%a);\n"
+         print_dk_term g print_dk_term dkproof
+    | None ->
+       fprintf oc "\n %a;\n" print_dk_term dkproof
   end;
   []
 
diff --git a/lpprint.ml b/lpprint.ml
index 1142c48..9c4b968 100644
--- a/lpprint.ml
+++ b/lpprint.ml
@@ -79,7 +79,6 @@ let escape_name s =
     && List.for_all ((<>) s) forbidden_idents
     then s else "{|" ^ s ^ "|}"
 
-
 let rec print_dk_type_aux o (t, var_context) =
   match t with
   | Dktypetype -> fprintf o "Set"
@@ -108,13 +107,14 @@ and print_dk_cst o t =
   | "Is_true" -> fprintf o "dk_logic.ebP"
   | "FOCAL.ifthenelse" -> fprintf o "dk_bool.ite"
   | s ->
-     if !Globals.signature_name = "" then fprintf o "%s" (escape_name s)
-     else if Mltoll.is_meta s then fprintf o "select ι"
+     if Mltoll.is_meta s then fprintf o "select ι"
      else
        begin
-         fprintf o "S.%s" (escape_name s);
-         if !Globals.neg_conj <> "" && not !Globals.check_axiom
-            && Typetptp.is_axiom s then fprintf o "%s" !Globals.neg_conj
+         if !Globals.signature_name = "" then fprintf o "%s" (escape_name s)
+         else fprintf o "S.%s" (escape_name s);
+         if !Globals.conjecture <> ""
+            && not !Globals.check_axiom && Typetptp.is_axiom s then
+           fprintf o " __negated_conjecture_proof__"
        end
 
 and print_dk_term_aux o (t, var_context) =
diff --git a/main.ml b/main.ml
index b624342..4576e2a 100644
--- a/main.ml
+++ b/main.ml
@@ -182,9 +182,7 @@ let argspec = [
 				  opt_level := 0;
 				  Globals.output_lp := true),
             "           print the proof in lambdapi term format";
-  "-conj", Arg.Unit (fun () -> Globals.neg_conj :=
-                                 (* keep space at the beginning *)
-                                 " __negated_conjecture__"),
+  "-conj", Arg.Unit (fun () -> Globals.conjecture := "conjecture"),
       "              indicate whether there is an explicit conjecture";
   "-check-axiom", Arg.Unit (fun () -> Globals.check_axiom := true),
       "       indicate whether this is a GDV leaf problem";
diff --git a/zenon.dk b/zenon.dk
new file mode 100644
index 0000000..d317209
--- /dev/null
+++ b/zenon.dk
@@ -0,0 +1,169 @@
+(; propositions ;)
+prop : Type.
+True : prop.
+False : prop.
+imp : prop -> prop -> prop.
+def not : prop -> prop := p : prop => imp p False.
+and : prop -> prop -> prop.
+or : prop -> prop -> prop.
+def eqv : prop -> prop -> prop := p : prop => q : prop => and (imp p q) (imp q p).
+
+(; sorts ;)
+type : Type.
+def iota : type.
+
+(; interpretation of sorts as types ;)
+injective term : type -> Type.
+
+(; axiom saying that every sort is inhabited ;)
+def select : a : type -> term a.
+
+(; sorted equality and quantifiers ;)
+equal : a : type -> term a -> term a -> prop.
+forall : a : type -> (term a -> prop) -> prop.
+exists : a : type -> (term a -> prop) -> prop.
+
+(; interpretation of propositions as types ;)
+injective proof : prop -> Type.
+[p, q] proof (imp p q) --> proof p -> proof q.
+[a, p] proof (forall a p) --> x : term a -> proof (p x).
+
+(; axiom equivalent to the excluded middle ;)
+def nnpp : p : prop -> proof (not (not p)) -> proof p.
+
+(; epsilon ;)
+def epsilon : a : type -> p : (term a -> prop) -> term a.
+def epsilon_intro : a : type -> p : (term a -> prop) -> proof (exists a p) -> proof (p (epsilon a p)).
+
+(; Zenon rules ;)
+
+def Rfalse : proof False -> proof False.
+
+def Rnottrue : proof (not True) -> proof False.
+
+def Raxiom : p : prop -> proof p -> proof (not p) -> proof False.
+
+def Rnoteq : a : type -> t : term a -> proof (not (equal a t t)) -> proof False.
+
+def Reqsym : a : type ->
+             t : term a ->
+             u : term a ->
+             proof (equal a t u) ->
+             proof (not (equal a u t)) ->
+             proof False.
+
+def Rcut : p : prop ->
+           (proof p -> proof False) ->
+           (proof (not p) -> proof False) ->
+           proof False.
+
+def Rnotnot : p : prop ->
+              (proof p -> proof False) ->
+              proof (not (not p)) ->
+              proof False.
+
+def Rand : p : prop ->
+           q : prop ->
+           (proof p -> proof q -> proof False) ->
+           proof (and p q) ->
+           proof False.
+
+def Ror : p : prop ->
+          q : prop ->
+          (proof p -> proof False) ->
+          (proof q -> proof False) ->
+          proof (or p q) ->
+          proof False.
+
+def Rimply : p : prop ->
+             q : prop ->
+             (proof (not p) -> proof False) ->
+             (proof q -> proof False) ->
+             proof (imp p q) ->
+             proof False.
+
+def Requiv : p : prop ->
+             q : prop ->
+             (proof (not p) -> proof (not q) -> proof False) ->
+             (proof p -> proof q -> proof False) ->
+             proof (eqv p q) ->
+             proof False.
+
+def Rnotand : p : prop ->
+              q : prop ->
+              (proof (not p) -> proof False) ->
+              (proof (not q) -> proof False) ->
+              proof (not (and p q)) ->
+              proof False.
+
+def Rnotor : p : prop ->
+             q : prop ->
+             (proof (not p) -> proof (not q) -> proof False) ->
+             proof (not (or p q)) ->
+             proof False.
+
+def Rnotimply : p : prop ->
+                q : prop ->
+                (proof p -> proof (not q) -> proof False) ->
+                proof (not (imp p q)) ->
+                proof False.
+
+def Rnotequiv : p : prop ->
+                q : prop ->
+                (proof (not p) -> proof q -> proof False) ->
+                (proof p -> proof (not q) -> proof False) ->
+                proof (not (eqv p q)) ->
+                proof False.
+
+def Rex : a : type ->
+          p : (term a -> prop) ->
+          (t : term a -> proof (p t) -> proof False) ->
+          proof (exists a p) ->
+          proof False.
+
+def Rall : a : type ->
+           p : (term a -> prop) ->
+           t : term a ->
+           (proof (p t) -> proof False) ->
+           proof (forall a p) ->
+           proof False.
+
+def Rnotex : a : type ->
+             p : (term a -> prop) ->
+             t : term a ->
+             (proof (not (p t)) -> proof False) ->
+             proof (not (exists a p)) ->
+             proof False.
+
+def Rnotall : a : type ->
+              p : (term a -> prop) ->
+              (t : term a -> proof (not (p t)) -> proof False) ->
+              proof (not (forall a p)) ->
+              proof False.
+
+def Rsubst : a : type ->
+             p : (term a -> prop) ->
+             t1 : term a ->
+             t2 : term a ->
+             (proof (not (equal a t1 t2)) -> proof False) ->
+             (proof (p t2) -> proof False) ->
+             proof (p t1) ->
+             proof False.
+
+def Rconglr : a : type ->
+              p : (term a -> prop) ->
+              t1 : term a ->
+              t2 : term a ->
+              (proof (p t2) -> proof False) ->
+              proof (p t1) ->
+              proof (equal a t1 t2) ->
+              proof False.
+
+def Rcongrl : a : type ->
+              p : (term a -> prop) ->
+              t1 : term a ->
+              t2 : term a ->
+              (proof (p t2) -> proof False) ->
+              proof (p t1) ->
+              proof (equal a t2 t1) ->
+              proof False.

From 69b5c37d7a50ea8f9187d5c7926707b84a930ea4 Mon Sep 17 00:00:00 2001
From: Guillaume Burel <guillaume.burel@inria.fr>
Date: Wed, 11 Sep 2024 17:15:13 +0200
Subject: [PATCH 9/9] Add SZS status in the output

---
 globals.ml    |  2 ++
 globals.mli   |  3 +++
 main.ml       | 62 +++++++++++++++++++++++++++++++++++++++++++--------
 parsetptp.mly |  2 +-
 tptp.ml       | 16 +++++++------
 5 files changed, 68 insertions(+), 17 deletions(-)

diff --git a/globals.ml b/globals.ml
index 54e8a08..2391152 100644
--- a/globals.ml
+++ b/globals.ml
@@ -43,3 +43,5 @@ let end_comment() =
   if !output_dk then ";)"
   else if !output_lp then "*/"
   else "*)"
+
+let has_a_conjecture = ref true
diff --git a/globals.mli b/globals.mli
index f266da4..4286bfb 100644
--- a/globals.mli
+++ b/globals.mli
@@ -36,3 +36,6 @@ val check_axiom : bool ref;;
 
 val begin_comment : unit -> string;;
 val end_comment : unit -> string;;
+
+(* Has a conjecture, useful for SZS output *)
+val has_a_conjecture : bool ref;;
diff --git a/main.ml b/main.ml
index 4576e2a..712523c 100644
--- a/main.ml
+++ b/main.ml
@@ -7,6 +7,53 @@ open Globals;;
 open Namespace;;
 open Expr;;
 
+(* part of SZS ontology, see
+   https://tptp.org/cgi-bin/SeeTPTP?Category=Documents&File=SZSOntology
+*)
+type szs_success =
+    Success
+  | Theorem
+  | Unsatisfiable
+
+type szs_error =
+    NoSuccess
+  | Unknown
+  | ResourceOut
+
+type szs_status =
+    Suc of szs_success
+  | Err of szs_error
+
+let szs_status out (status, file) =
+  fprintf out "%% SZS status %a for %s"
+    (fun out -> function
+      | Suc Success -> fprintf out "Success"
+      | Suc Theorem -> fprintf out "Theorem"
+      | Suc Unsatisfiable -> fprintf out "Unsatisfiable"
+      | Err NoSuccess -> fprintf out "NoSuccess"
+      | Err Unknown -> fprintf out "Unknown"
+      | Err ResourceOut -> fprintf out "ResourceOut"
+    )
+    status file
+
+let get_status found =
+  if found then
+    if !Globals.has_a_conjecture then
+      Suc Theorem
+    else
+      Suc Unsatisfiable
+  else
+    Err Unknown
+
+let print_status status file =
+  printf "%s %s\n%a\n%s\n"
+    (begin_comment ())
+    (match status with Suc _ -> " PROOF-FOUND "
+                     | Err _ ->  "NO-PROOF")
+    szs_status (status, file)
+    (end_comment())
+
+
 type proof_level =
   | Proof_none
   | Proof_h of int
@@ -457,14 +504,9 @@ let main () =
     if is_open then
         retcode := 12;
     if not !quiet_flag then begin
-      if is_open then
-        if !Globals.signature_name <> "" then ()
-        else printf "%s" (begin_comment() ^ " NO-PROOF " ^ end_comment() ^ "\n")
-      else
-        if !Globals.signature_name <> "" then ()
-        else printf "%s" (begin_comment() ^ " PROOF-FOUND " ^ end_comment() ^ "\n");
+      print_status (get_status @@ not is_open) file;
       flush stdout
-      end;
+    end;
     let llp = lazy (optim (Extension.postprocess
                              (Mltoll.translate th_name ppphrases proof)))
     in
@@ -504,10 +546,12 @@ let main () =
   with
   | Prove.NoProof ->
      retcode := 12;
-     if not !quiet_flag then (if !Globals.signature_name <> "" then () else printf "(* NO-PROOF *)\n");
+     if not !quiet_flag then
+       print_status (Err Unknown) file
   | Prove.LimitsExceeded ->
      retcode := 13;
-     if not !quiet_flag then (if !Globals.signature_name <> "" then () else printf "(* NO-PROOF *)\n");
+     if not !quiet_flag then
+       print_status (Err ResourceOut) file
   end;
   if !stats_flag then begin
     eprintf "nodes searched: %d\n" !Globals.inferences;
diff --git a/parsetptp.mly b/parsetptp.mly
index 34d634d..accab75 100644
--- a/parsetptp.mly
+++ b/parsetptp.mly
@@ -93,7 +93,7 @@ let cnf_to_formula l =
 
 file:
   | EOF             { [] }
-  | phrase file     { $1 :: $2 }
+  | phrase file     { Globals.has_a_conjecture := false; $1 :: $2 }
 ;
 phrase:
   | INCLUDE OPEN LIDENT CLOSE DOT  { Phrase.Include ($3, None) }
diff --git a/tptp.ml b/tptp.ml
index 75be43d..c1303b6 100644
--- a/tptp.ml
+++ b/tptp.ml
@@ -141,11 +141,12 @@ let rec translate_one dirs accu p =
   | Formula (name, ("lemma"|"theorem"), body, None) ->
       Hyp (name, body, 1) :: accu
   | Formula (name, "conjecture", body, None) ->
-      tptp_thm_name := name;
-      Hyp (goal_name, enot (body), 0) :: accu
+    tptp_thm_name := name;
+    Globals.has_a_conjecture := true;
+    Hyp (goal_name, enot (body), 0) :: accu
   | Formula (name, "negated_conjecture", body, None) ->
-      tptp_thm_name := "negation_of_" ^ name;
-      Hyp (name, body, 0) :: accu
+    tptp_thm_name := "negation_of_" ^ name;
+    Hyp (name, body, 0) :: accu
   (* TFF formulas *)
   | Formula (name, "tff_type", body, None) ->
       Hyp (name, body, 13) :: accu
@@ -162,10 +163,11 @@ let rec translate_one dirs accu p =
   | Formula (name, ("tff_lemma"|"tff_theorem"), body, None) ->
       Hyp (name, body, 11) :: accu
   | Formula (name, "tff_conjecture", body, None) ->
-      tptp_thm_name := name;
-      Hyp (goal_name, enot (body), 10) :: accu
+    tptp_thm_name := name;
+    Globals.has_a_conjecture := true;
+    Hyp (goal_name, enot (body), 10) :: accu
   | Formula (name, "tff_negated_conjecture", body, None) ->
-      Hyp (name, body, 10) :: accu
+    Hyp (name, body, 10) :: accu
   (* Fallback *)
   | Formula (name, k, body, _) ->
       Error.warn ("unknown formula kind: " ^ k);