Extended the equality case to non ground terms

[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..13b1d7270bc3fd1f785d8831a97ac284ec0b0bce 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
-  let bag, maxvar, newclauses = 
-    Sup.superposition_right_with_table bag maxvar clause table
+  prerr_endline "Active table:";
+  List.iter (fun uc -> prerr_endline (Pp.pp_unit_clause uc)) active_clauses;
+  let bag, maxvar, _, newclauses = 
+    Sup.superposition_right bag maxvar clause (active_clauses, table)
   in
   prerr_endline "Output clauses :";
   List.iter (fun c -> prerr_endline (Pp.pp_unit_clause c)) newclauses;
+  prerr_endline "========================================";
 ;;