X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fsuperposition.ml;h=6ec6048de9147191b13cfd96b14b5e763df8c255;hb=88efee4c688d660d2205c5933d302770acb5b407;hp=6f1fb0f7f91a3e1395bf3dc71fa6a65cb39a3136;hpb=dce1bca274f93a3bddcc0f6b04cbf126ccff42b0;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 6f1fb0f7f..6ec6048de 100644
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -247,10 +247,12 @@ module Superposition (B : Orderings.Blob) =
                      ((*prerr_endline ("Filtering: " ^ 
                         Pp.pp_foterm side ^ " =(< || =)" ^ 
                         Pp.pp_foterm newside ^ " coming from " ^ 
-                        Pp.pp_unit_clause uc );*)None)
+                        Pp.pp_unit_clause uc );*)
+		       debug (lazy "not applied");None)
                  else
                    Some (newside, subst, id, dir)
-               with FoUnif.UnificationFailure _ -> None)
+               with FoUnif.UnificationFailure _ -> 
+                 debug (lazy "not applied"); None)
         (IDX.ClauseSet.elements cands)
     ;;
 
@@ -268,7 +270,7 @@ module Superposition (B : Orderings.Blob) =
     ;;
       
     let rec demodulate bag (id, literal, vl, pr) table =
-      debug (lazy "demodulate...");
+      debug (lazy ("demodulate " ^ (string_of_int id)));
        match literal with
       | Terms.Predicate t -> assert false
       | Terms.Equation (l,r,ty,_) ->
@@ -750,6 +752,10 @@ module Superposition (B : Orderings.Blob) =
              bag, maxvar, newc @ acc)
           (bag, maxvar, []) alist
       in
+        debug
+	(lazy 
+	 ("New clauses :" ^ (String.concat ";\n" 
+	    (List.map Pp.pp_unit_clause new_clauses)))); 
         debug (lazy "First superpositions");
         (* We add current to active clauses so that it can be *
          * superposed with itself                             *)