right inference step completed

[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 13b1d7270bc3fd1f785d8831a97ac284ec0b0bce..f30a9fcb6ba34949c3ed99f1753a6e6607c820ed 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -49,9 +49,11 @@ let nparamod metasenv subst context t 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)
+    Sup.infer_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 "Proofs: ";
+  prerr_endline (Pp.pp_bag bag);
   prerr_endline "========================================";
 ;;