diff --git a/src/printers/pyrat.ml b/src/printers/pyrat.ml
index 0a8132c2819e36f21d117b1f20b2a3e8e54de4b0..59705230a5a71728a170c6a1c6ccb1dd280ff7e9 100644
--- a/src/printers/pyrat.ml
+++ b/src/printers/pyrat.ml
@@ -54,18 +54,29 @@ let rec print_base_term info fmt t =
       | Some s, [] -> Fmt.string fmt s
       | _ -> Printer.unsupportedTerm t "Unknown variable(s)"))
 
-let rec print_term ~sep info fmt t =
-  (* Don't print things we don't know. *)
-  let t_is_known =
-    Term.t_s_all
-      (fun _ -> true)
-      (fun ls ->
-        Ident.Mid.mem ls.ls_name info.info_syn || Term.Hls.mem info.variables ls)
-  in
+(* We do not want to print unknown symbols: returns false if not a known syntax
+   or variable. *)
+let t_is_known info =
+  Term.t_s_all
+    (fun _ -> true)
+    (fun ls ->
+      Ident.Mid.mem ls.ls_name info.info_syn || Term.Hls.mem info.variables ls)
+
+let rec print_premise_term info fmt t =
+  match t.Term.t_node with
+  | Tquant _ -> ()
+  | Tbinop (Tand, t1, t2) ->
+    if t_is_known info t1 && t_is_known info t2
+    then
+      Fmt.pf fmt "%a%a" (print_premise_term info) t1 (print_premise_term info)
+        t2
+  | _ -> if t_is_known info t then Fmt.pf fmt "%a@." (print_base_term info) t
+
+let rec print_goal_term info fmt t =
   match t.Term.t_node with
   | Tquant _ -> ()
   | Tbinop (((Tand | Tor) as lop), t1, t2) ->
-    if t_is_known t1 && t_is_known t2
+    if t_is_known info t1 && t_is_known info t2
     then
       let psx, lop, pdx =
         match lop with
@@ -73,9 +84,9 @@ let rec print_term ~sep info fmt t =
         | Tor -> ("(", "or", ")")
         | _ -> assert false
       in
-      Fmt.pf fmt "%s%a %s %a%s" psx (print_term ~sep info) t1 lop
-        (print_term ~sep info) t2 pdx
-  | _ -> if t_is_known t then Fmt.pf fmt "%a%(%)" (print_base_term info) t sep
+      Fmt.pf fmt "%s%a %s %a%s" psx (print_goal_term info) t1 lop
+        (print_goal_term info) t2 pdx
+  | _ -> if t_is_known info t then Fmt.pf fmt "%a" (print_base_term info) t
 
 let print_decl info fmt d =
   match d.Decl.d_node with
@@ -86,10 +97,9 @@ let print_decl info fmt d =
   | Dind _ -> ()
   | Dprop (Decl.Plemma, _, _) -> assert false
   | Dprop (Decl.Paxiom, _, f) ->
-    (* PyRAT supports simple axioms only, ie without logical operators. We print
-       axioms one per line, hence the separator [sep]. *)
-    print_term ~sep:"@." info fmt f
-  | Dprop (Decl.Pgoal, _, f) -> print_term ~sep:"" info fmt f
+    (* PyRAT supports simple axioms only, ie without logical operators. *)
+    print_premise_term info fmt f
+  | Dprop (Decl.Pgoal, _, f) -> print_goal_term info fmt f
 
 let rec print_tdecl info fmt task =
   match task with