snapshot

[helm.git] / helm / software / components / ng_paramodulation / paramod.ml

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index 1bd9bcf4f1e710273948013f02f9d6ce659e1d7b..fb93ec7f84edb4d70e3f14c0e0270f2d15ce4545 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -1,4 +1,5 @@
 let nparamod metasenv subst context t table =
+  prerr_endline "========================================";
   let module C = struct
     let metasenv = metasenv
     let subst = subst
@@ -45,9 +46,12 @@ let nparamod metasenv subst context t table =
   let table =  
     List.fold_left IDX.index_unit_clause IDX.DT.empty active_clauses
   in
+  prerr_endline "Active table:";
+  List.iter (fun uc -> prerr_endline (Pp.pp_unit_clause uc)) active_clauses;
   let bag, maxvar, newclauses = 
     Sup.superposition_right_with_table bag maxvar clause table
   in
   prerr_endline "Output clauses :";
   List.iter (fun c -> prerr_endline (Pp.pp_unit_clause c)) newclauses;
+  prerr_endline "========================================";
 ;;