...

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 6d10c86d8ad01842fe807925f930b898b2ad3acc..b002dce33a05c4be5bc2f823d31f0c952293ed31 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -16,6 +16,7 @@ module Superposition (B : Terms.Blob) =
     module IDX = Index.Index(B)
     module Unif = FoUnif.Founif(B)
     module Subst = FoSubst.Subst(B)
+    module Order = Orderings.Orderings(B)
 
     let all_positions t f =
       let rec aux pos ctx = function
@@ -67,7 +68,9 @@ module Superposition (B : Terms.Blob) =
                  let r = Subst.apply_subst subst r in
                  let l = Subst.apply_subst subst l in
                  let ty = Subst.apply_subst subst ty in
-                 (0, Terms.Equation (l,r,ty,Terms.Incomparable), vl, proof))
+                 let o = Order.compare_terms l r in
+                 (* can unif compute the right vl for both sides? *)
+                 (0, Terms.Equation (l,r,ty,o), vl, proof))
               res
           in
           (* fresh ID and metas and compute orientataion of new_clauses *)