diff --git a/CoAlgMisc.ml b/CoAlgMisc.ml
index 30f92b0f40748ddbccb532c02948cf2924b786e1..3d9c9643dbc58d277c94368c4f3ef473fdf21024 100644
--- a/CoAlgMisc.ml
+++ b/CoAlgMisc.ml
@@ -710,14 +710,18 @@ let ppFormulae nomTbl tbox (s, f) =
     raise (C.CoAlgException "Number of sorts must be positive.")
   else ();
   let nnfAndSimplify f = C.simplify (C.nnf f) in
-  let f1 = nnfAndSimplify f in
-  let tbox1 = List.map (fun (s, f) -> (s, nnfAndSimplify f)) tbox in
-
-  let hcF =  C.HcFormula.create true in
-  let hcf = C.hc_formula hcF f1 in
-  let hctbox = List.map (fun (s, f) -> (s, C.hc_formula hcF f)) tbox1 in
+  let  f1    = nnfAndSimplify f in
+  let nf1    = nnfAndSimplify (C.NOT f) in
+  let  tbox1 = List.map (fun (s, f) -> (s, nnfAndSimplify f)) tbox in
+  let ntbox1 = List.map (fun (s, f) -> (s, nnfAndSimplify (C.NOT f))) tbox in
+
+  let hcF     =  C.HcFormula.create true in
+  let  hcf    = C.hc_formula hcF  f1 in
+  let nhcf    = C.hc_formula hcF nf1 in
+  let  hctbox = List.map (fun (s, f) -> (s, C.hc_formula hcF f))  tbox1 in
+  let nhctbox = List.map (fun (s, f) -> (s, C.hc_formula hcF f)) ntbox1 in
   let hcfalse = C.hc_formula hcF C.FALSE in
-  let hctrue = C.hc_formula hcF C.TRUE in
+  let hctrue  = C.hc_formula hcF C.TRUE in
 
   let fset = Array.init card (fun _ -> C.HcFHt.create 128) in
   let atset = C.HcFHt.create 64 in
@@ -726,8 +730,10 @@ let ppFormulae nomTbl tbox (s, f) =
     detClosure nomTbl hcF fset atset nomset i hcfalse;
     detClosure nomTbl hcF fset atset nomset i hctrue;
   done;
-  detClosure nomTbl hcF fset atset nomset s hcf;
-  List.iter (fun (s, f) -> detClosure nomTbl hcF fset atset nomset s f) hctbox;
+  detClosure nomTbl hcF fset atset nomset s  hcf;
+  detClosure nomTbl hcF fset atset nomset s nhcf;
+  List.iter (fun (s, f) -> detClosure nomTbl hcF fset atset nomset s f)  hctbox;
+  List.iter (fun (s, f) -> detClosure nomTbl hcF fset atset nomset s f) nhctbox;
   Hashtbl.iter (fun n s -> C.HcFHt.iter (detClosureAt hcF atset n) fset.(s)) nomset;
 
   let htF = Array.init card (fun _ -> C.HcFHt.create 128) in