From 19ebfeb8669efc9aece794ab77f9638378dc2e92 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Thu, 6 Nov 2014 21:24:11 +0100
Subject: [PATCH] Now using unicode characters

---
 sat/res.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/sat/res.ml b/sat/res.ml
index 3b86d831..d96e8921 100644
--- a/sat/res.ml
+++ b/sat/res.ml
@@ -48,12 +48,12 @@ module Make(St : Solver_types.S)(Proof : sig type proof end) = struct
 
   (* Printing functions *)
   let print_atom fmt a =
-    Format.fprintf fmt "%s%d" St.(if a.var.pa == a then "" else "-") St.(a.var.vid + 1)
+    Format.fprintf fmt "%s%d" St.(if a.var.pa == a then "" else "¬ ") St.(a.var.vid + 1)
 
   let rec print_cl fmt = function
     | [] -> Format.fprintf fmt "[]"
     | [a] -> print_atom fmt a
-    | a :: ((_ :: _) as r) -> Format.fprintf fmt "%a \\/ %a" print_atom a print_cl r
+    | a :: ((_ :: _) as r) -> Format.fprintf fmt "%a ∨ %a" print_atom a print_cl r
 
   (* Compute resolution of 2 clauses *)
   let resolve l =