added a flag for age selection

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

diff --git a/helm/software/components/ng_paramodulation/index.ml b/helm/software/components/ng_paramodulation/index.ml
index 5c085c5188db5a4473337995e167d17b290f5bfe..3179f000068897755b450fcc8c315cc051c597ce 100644 (file)
--- a/helm/software/components/ng_paramodulation/index.ml
+++ b/helm/software/components/ng_paramodulation/index.ml
@@ -93,11 +93,11 @@ module Index(B : Orderings.Blob) = struct
     | (_,Terms.Equation (_,r,_,Terms.Lt),_,_) as c -> 
           DT.index t r (Terms.Right2Left, c)
     | (_,Terms.Equation (l,r,_,Terms.Incomparable),vl,_) as c ->
-       if are_invertible maxvar vl l r then
+(*     if are_invertible maxvar vl l r then
          (prerr_endline ("Invertible " ^ (Pp.pp_foterm l) ^ "=" ^
             (Pp.pp_foterm r));
            DT.index t l (Terms.Left2Right, c))
-          else
+          else *)
           DT.index  
            (DT.index t l (Terms.Left2Right, c))
            r (Terms.Right2Left, c)