diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/FORMULA.sig b/lib/forgejo.ballcloud.cc/wball/proof-checker/FORMULA.sig
index c79c6a2..d329de7 100644
--- a/lib/forgejo.ballcloud.cc/wball/proof-checker/FORMULA.sig
+++ b/lib/forgejo.ballcloud.cc/wball/proof-checker/FORMULA.sig
@@ -20,4 +20,7 @@ sig
   val matchVariable: int -> t * t -> Term.t option
 
   val occurs: Term.t -> t -> bool
+
+  val ppd: int -> int -> t -> string
+  val pp: t -> string
 end
diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/Formula.sml b/lib/forgejo.ballcloud.cc/wball/proof-checker/Formula.sml
index 8671b21..24c5902 100644
--- a/lib/forgejo.ballcloud.cc/wball/proof-checker/Formula.sml
+++ b/lib/forgejo.ballcloud.cc/wball/proof-checker/Formula.sml
@@ -75,18 +75,63 @@ struct
     | matchVariable x (Iff (phi, psi), Iff (phi', psi')) =
         Term.mergeOption
           (matchVariable x (phi, phi'), matchVariable x (psi, psi'))
-    | matchVariable x (Exists phi, Exists psi) = matchVariable (x + 1) (phi, psi)
-    | matchVariable x (Forall phi, Forall psi) = matchVariable (x + 1) (phi, psi)
+    | matchVariable x (Exists phi, Exists psi) =
+        matchVariable (x + 1) (phi, psi)
+    | matchVariable x (Forall phi, Forall psi) =
+        matchVariable (x + 1) (phi, psi)
     | matchVariable _ _ = raise MatchFailure
 
-  fun occurs t (Relation (_, ts)) = List.exists (Term.occurs t) ts
-    | occurs t (Equal (p, q)) = Term.occurs t p orelse Term.occurs t q
+  fun occurs t (Relation (_, ts)) =
+        List.exists (Term.occurs t) ts
+    | occurs t (Equal (p, q)) =
+        Term.occurs t p orelse Term.occurs t q
     | occurs t Bottom = false
     | occurs t (Neg phi) = occurs t phi
-    | occurs t (Conj (phi, psi)) = occurs t phi orelse occurs t psi
-    | occurs t (Disj (phi, psi)) = occurs t phi orelse occurs t psi
-    | occurs t (Impl (phi, psi)) = occurs t phi orelse occurs t psi
-    | occurs t (Iff (phi, psi)) = occurs t phi orelse occurs t psi
-    | occurs t (Exists phi) = occurs (Term.incVars t) phi
-    | occurs t (Forall phi) = occurs (Term.incVars t) phi
+    | occurs t (Conj (phi, psi)) =
+        occurs t phi orelse occurs t psi
+    | occurs t (Disj (phi, psi)) =
+        occurs t phi orelse occurs t psi
+    | occurs t (Impl (phi, psi)) =
+        occurs t phi orelse occurs t psi
+    | occurs t (Iff (phi, psi)) =
+        occurs t phi orelse occurs t psi
+    | occurs t (Exists phi) =
+        occurs (Term.incVars t) phi
+    | occurs t (Forall phi) =
+        occurs (Term.incVars t) phi
+
+  val precedence =
+    fn Bottom => 10
+     | Relation _ => 10
+     | Equal _ => 10
+     | Neg _ => 9
+     | Conj _ => 8
+     | Disj _ => 7
+     | Impl _ => 6
+     | Iff _ => 5
+     | Forall _ => 4
+     | Exists _ => 4
+
+  fun ppd d prec prop =
+    let
+      val np = precedence prop
+      val str =
+        case prop of
+          Bottom => "\226\138\165"
+        | Relation (f, args) =>
+            f ^ "(" ^ (String.concatWith ", " (map (Term.ppd d) args)) ^ ")"
+        | Equal (t, s) => Term.ppd d t ^ " = " ^ Term.ppd d s
+        | Neg (Equal (t, s)) => Term.ppd d t ^ " != " ^ Term.ppd d s
+        | Neg phi => "~" ^ ppd d np phi
+        | Conj (phi, psi) => ppd d np phi ^ " \226\136\167 " ^ ppd d np psi
+        | Disj (phi, psi) => ppd d np phi ^ " \226\136\168 " ^ ppd d np psi
+        | Impl (phi, psi) => ppd d np phi ^ " => " ^ ppd d np psi
+        | Iff (phi, psi) => ppd d np phi ^ " <=> " ^ ppd d np psi
+        | Forall phi => "\226\136\128" ^ Var.name d ^ ". " ^ ppd (d + 1) np phi
+        | Exists phi => "\226\136\131" ^ Var.name d ^ ". " ^ ppd (d + 1) np phi
+    in
+      if np < prec then "(" ^ str ^ ")" else str
+    end
+
+  val pp = ppd 0 0
 end
diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/Proof.sml b/lib/forgejo.ballcloud.cc/wball/proof-checker/Proof.sml
index c95b9bd..ffba7d2 100644
--- a/lib/forgejo.ballcloud.cc/wball/proof-checker/Proof.sml
+++ b/lib/forgejo.ballcloud.cc/wball/proof-checker/Proof.sml
@@ -20,7 +20,7 @@ struct
   | ExistsI
   | ExistsE
 
-  exception ProofError of int
+  exception ProofError of string
 
   datatype t = Proof of {children: t list, label: label, formula: Formula.t}
 
@@ -170,57 +170,56 @@ struct
           ) =
           valid (left, a) andalso valid (right, a)
           andalso Formula.checkSubst (t, s) (phi, psi)
-  | valid
-      ( Proof
-          { children = [kid as Proof {formula = Forall phi, ...}]
-          , label = ForallE
-          , formula = psi
-          }
-      , a
-      ) =
-      valid (kid, a)
-      andalso
-      (case Formula.matchVariable 0 (phi, psi) of
-         _ => true handle MatchFailure => false)
-  | valid
-      ( Proof
-          { children = [kid as Proof {formula = phi, ...}]
-          , label = ExistsI
-          , formula = Exists psi
-          }
-      , a
-      ) =
-      valid (kid, a)
-      andalso
-      (case Formula.matchVariable 0 (psi, phi) of
-         _ => true handle MatchFailure => false)
-  | valid
-      ( Proof
-          { children = [kid as Proof {formula = phi, ...}]
-          , label = ForallI
-          , formula = Forall psi
-          }
-      , a
-      ) =
-      valid (kid, a)
-      andalso
-      (case Formula.matchVariable 0 (psi, phi) of
-         SOME (t as Term.Free _) => not (List.exists (Formula.occurs t) a)
-       | _ => false handle MatchFailure => false)
-  | valid
-      ( Proof
-          { children =
-              [ kid as Proof {formula = Exists phi, ...} ]
-          , label = ExistsE
-          , formula = psi
-          }
-      , a
-      ) =
-      valid (kid, a)
-      andalso
-      (case Formula.matchVariable 0 (phi, psi) of
-            SOME (t as Term.Free _) => not (List.exists (Formula.occurs t) a)
-          | _ => false handle MatchFailure => false)
-  | valid _ = false
+      | valid
+          ( Proof
+              { children = [kid as Proof {formula = Forall phi, ...}]
+              , label = ForallE
+              , formula = psi
+              }
+          , a
+          ) =
+          valid (kid, a)
+          andalso
+          (case Formula.matchVariable 0 (phi, psi) of
+             _ => true handle MatchFailure => false)
+      | valid
+          ( Proof
+              { children = [kid as Proof {formula = phi, ...}]
+              , label = ExistsI
+              , formula = Exists psi
+              }
+          , a
+          ) =
+          valid (kid, a)
+          andalso
+          (case Formula.matchVariable 0 (psi, phi) of
+             _ => true handle MatchFailure => false)
+      | valid
+          ( Proof
+              { children = [kid as Proof {formula = phi, ...}]
+              , label = ForallI
+              , formula = Forall psi
+              }
+          , a
+          ) =
+          valid (kid, a)
+          andalso
+          (case Formula.matchVariable 0 (psi, phi) of
+             SOME (t as Term.Free _) => not (List.exists (Formula.occurs t) a)
+           | _ => false handle MatchFailure => false)
+      | valid
+          ( Proof
+              { children = [kid as Proof {formula = Exists phi, ...}]
+              , label = ExistsE
+              , formula = psi
+              }
+          , a
+          ) =
+          valid (kid, a)
+          andalso
+          (case Formula.matchVariable 0 (phi, psi) of
+             SOME (t as Term.Free _) => not (List.exists (Formula.occurs t) a)
+           | _ => false handle MatchFailure => false)
+      | valid _ = false
   end
 end
diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/TERM.sig b/lib/forgejo.ballcloud.cc/wball/proof-checker/TERM.sig
index ff22eb2..9588790 100644
--- a/lib/forgejo.ballcloud.cc/wball/proof-checker/TERM.sig
+++ b/lib/forgejo.ballcloud.cc/wball/proof-checker/TERM.sig
@@ -15,7 +15,11 @@ sig
 
   val mergeOption: t option * t option -> t option
 
-  val incVars : t -> t
+  val incVars: t -> t
 
-  val occurs : t -> t -> bool
+  val occurs: t -> t -> bool
+
+  val ppd: int -> t -> string
+
+  val pp: t -> string
 end
diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/Term.sml b/lib/forgejo.ballcloud.cc/wball/proof-checker/Term.sml
index e0c62a1..9378a06 100644
--- a/lib/forgejo.ballcloud.cc/wball/proof-checker/Term.sml
+++ b/lib/forgejo.ballcloud.cc/wball/proof-checker/Term.sml
@@ -46,16 +46,33 @@ struct
     | matchVariable x (Function (f, ts), Function (g, ss)) =
         foldl mergeOption NONE (map (matchVariable x)
           (ListPair.zipEq (ts, ss) handle UnequalLengths => raise MatchFailure))
-    | matchVariable _ (Free s1, Free s2) = if s1 = s2 then NONE else raise MatchFailure
+    | matchVariable _ (Free s1, Free s2) =
+        if s1 = s2 then NONE else raise MatchFailure
     | matchVariable _ _ = raise MatchFailure
 
-  fun incVars (Var x) = Var (x + 1)
-    | incVars (Function (f, args)) = Function (f, map incVars args)
+  fun incVars (Var x) =
+        Var (x + 1)
+    | incVars (Function (f, args)) =
+        Function (f, map incVars args)
     | incVars t = t
 
   fun occurs (Const s1) (Const s2) = s1 = s2
     | occurs (Var x1) (Var x2) = x1 = x2
-    | occurs t (Function (_, ts)) = List.exists (occurs t) ts
+    | occurs t (Function (_, ts)) =
+        List.exists (occurs t) ts
     | occurs (Free s1) (Free s2) = s1 = s2
     | occurs _ _ = false
+
+  fun ppd depth (Const s) = s
+    | ppd depth (Free s) = s
+    | ppd depth (Var x) =
+        Var.name (depth - x - 1)
+    | ppd depth (Function (f, x :: rest)) =
+        f ^ "("
+        ^
+        (foldl (fn (s, acc) => acc ^ ", " ^ s) (ppd depth x)
+           (map (ppd depth) rest)) ^ ")"
+    | ppd depth (Function (f, [])) = f ^ "()"
+
+  val pp = ppd 0
 end
diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/VAR.sig b/lib/forgejo.ballcloud.cc/wball/proof-checker/VAR.sig
new file mode 100644
index 0000000..c3acd7b
--- /dev/null
+++ b/lib/forgejo.ballcloud.cc/wball/proof-checker/VAR.sig
@@ -0,0 +1,4 @@
+signature VAR =
+sig
+  val name: int -> string
+end
diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/Var.sml b/lib/forgejo.ballcloud.cc/wball/proof-checker/Var.sml
new file mode 100644
index 0000000..d9acce8
--- /dev/null
+++ b/lib/forgejo.ballcloud.cc/wball/proof-checker/Var.sml
@@ -0,0 +1,6 @@
+structure Var: VAR =
+struct
+  val name_list = ["x", "y", "z", "w", "u", "v"]
+  fun name x =
+    if x < 6 then List.nth (name_list, x) else "x" ^ Int.toString (x - 6)
+end
diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/proof-checker.mlb b/lib/forgejo.ballcloud.cc/wball/proof-checker/proof-checker.mlb
index d0b4bbf..7fb49f1 100644
--- a/lib/forgejo.ballcloud.cc/wball/proof-checker/proof-checker.mlb
+++ b/lib/forgejo.ballcloud.cc/wball/proof-checker/proof-checker.mlb
@@ -1,6 +1,8 @@
 $(SML_LIB)/basis/basis.mlb
 ../../../github.com/diku-dk/sml-parse/parse.mlb
 ../../../github.com/diku-dk/sml-parse/simple_token.mlb
+VAR.sig
+Var.sml
 TERM.sig
 Term.sml
 FORMULA.sig