diff --git a/bin/main.ml b/bin/main.ml
index 669bfba95240852dc313c73f3d862f7ebe8553b3..608effba243315ccc2c5b097e00d80fe373cd5ef 100644
--- a/bin/main.ml
+++ b/bin/main.ml
@@ -36,17 +36,24 @@ let translate_file (src : string) =
   in
   let module Encoding = (val Lpvs.ToCert.make pcert_ss) in
   let module Pcert = Lpvs.ToCert.Make (Encoding) in
+  Console.out 1 "Loaded PVS-Cert encoding";
   let ast = Parser.parse_file src in
   let _ss = compile_ast pcert_ss ast in
   let syms = get_symbols sign in
   let pcertast = StrMap.map (fun (sym, _) -> Pcert.import sym) syms in
-  let p name ty = Format.printf "symbol %s:@ %a;@." name Lpvs.ToCert.pp ty in
-  StrMap.iter p pcertast
+  let lp name ty = Format.printf "@[symbol@ %s:@ %a;@]@." name Lpvs.ToCert.pp ty in
+  let tptp name ty =
+    let e = Lpvs.ToCert.tptp_of ty in
+    Format.printf "fof(@[%s,@ %a@]).@." name Lpvs.Tptp.Term.pp e
+  in
+  StrMap.iter lp pcertast; StrMap.iter tptp pcertast
 
 let () =
   let files = ref [] in
   Arg.parse speclist (fun f -> files := f :: !files) usage;
   Library.set_lib_root (if !lib_root = "" then None else Some !lib_root);
+  (* Silence lambdapi to have environment-independent output. *)
+  Timed.(Console.verbose := 0);
   let f = List.hd !files in
   try translate_file f
   with Error.Fatal (pos, msg) -> (
diff --git a/lib/dune b/lib/dune
index 161664b85f23e8b86aa93e2defd55b0214a5d4b8..871db88ff1ebf93f4afb741a53e19a5ea0e966c2 100644
--- a/lib/dune
+++ b/lib/dune
@@ -1,8 +1,3 @@
 (library
- (libraries
-  lambdapi.common
-  lambdapi.lplib
-  lambdapi.parsing
-  lambdapi.core
-  dolmen)
+ (libraries lambdapi.common lambdapi.lplib lambdapi.parsing lambdapi.core)
  (name lpvs))
diff --git a/lib/toCert.ml b/lib/toCert.ml
index 591723ebd3d990db47ad240b5a8d7e923829b1df..5e0ca0b35665af089c71dc3ecf976647fc375e51 100644
--- a/lib/toCert.ml
+++ b/lib/toCert.ml
@@ -186,3 +186,5 @@ let rec tptp_of (vm : Tt.t B.var CVMap.t) (t : term) : Tt.t =
           let b = B.bind_var x (Tt.lift b) in
           Lam (B.unbox b)
       | Psub _ | Pi _ -> raise (CannotTranslate t))
+
+let tptp_of (t : term) : Tt.t = tptp_of CVMap.empty t
diff --git a/lib/tptp.ml b/lib/tptp.ml
index 2ab3eb063b43d4601291529a8b0f7eaad024e99b..a0f77fedd79dd3ea3e8ef927d342512bd08ebb50 100644
--- a/lib/tptp.ml
+++ b/lib/tptp.ml
@@ -64,20 +64,13 @@ module Term = struct
     | Equiv (t, u) -> out (wrap "@[%a@ <=> %a@]") (pp true) t (pp true) u
     | All u ->
         let x, b = B.unbind u in
-        out (wrap "@[!@ [%a]@ :@ (%a)@]") pp_var x (pp false) b
+        out (wrap "@[!@ [%a]@ :@ %a@]") pp_var x (pp false) b
     | Ex u ->
         let x, b = B.unbind u in
-        out (wrap "@[? [%a]@ :@ (%a)@]") pp_var x (pp false) b
+        out (wrap "@[? [%a]@ :@ %a@]") pp_var x (pp false) b
     | Lam u ->
         let x, b = B.unbind u in
-        out (wrap "@[`@ [%a]@ :@ (%a)@]") pp_var x (pp false) b
+        out (wrap "@[`@ [%a]@ :@ %a@]") pp_var x (pp false) b
 
   let pp (ppf : Format.formatter) (t : t) : unit = pp false ppf t
 end
-
-module Clause = struct
-  type t = { label : string; expr : Term.t }
-
-  let pp (ppf : Format.formatter) ({ label; expr } : t) : unit =
-    Format.fprintf ppf "@[fof(%s,@ %a).@]" label Term.pp expr
-end
diff --git a/test/dune b/test/dune
index 08f89a2523183a4f81a2143a0281b97b4450840f..f4540ea39fe147eb4a31d5b3ebbdc162f40e37b0 100644
--- a/test/dune
+++ b/test/dune
@@ -1,2 +1,10 @@
 (test
  (name lpvs))
+
+(cram
+ (deps
+  ../bin/main.exe
+  lambdapi.pkg
+  encoding/lhol.lp
+  encoding/pvs_cert.lp
+  false.lp))
diff --git a/test/lpvs.t b/test/lpvs.t
new file mode 100644
index 0000000000000000000000000000000000000000..1a9410985cb744b533c603358a6dfffc673a1404
--- /dev/null
+++ b/test/lpvs.t
@@ -0,0 +1,5 @@
+  $ lpvs --lib-root encoding/ false.lp
+  symbol false: ∀ prop (\p: prop. p);
+  symbol true: ∀ prop (\p: prop. ⇒ p (\_: p. p));
+  fof(false, ∀ prop (` [p] : p)).
+  fof(true, ∀ prop (` [p] : ⇒ p (` [_] : p))).