X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fparamod.ml;h=86a964c1487f36a7f72deb0c8f2608f621ec2aac;hb=4a747f4352bd5961c60a7d75eaa95ac3ee4f54f9;hp=7fc13b504290aebbf11bbcfbf5032131ce60ad7d;hpb=320c0f89a7e31e996b6eff2b4165eb74e8141cec;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index 7fc13b504..86a964c14 100644
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -567,10 +567,12 @@ module Paramod (B : Orderings.Blob) = struct
 let demod s goal =
   let bag,maxvar,actives,passives,g_actives,g_passives = s in
   let (bag,maxvar), g = mk_goal (bag,maxvar) goal in
+  let bag, ((i,_,_,_) as g1) = Sup.demodulate bag g (snd actives) in
+    if g1 = g then GaveUp else compute_result bag i []
+(*
   if Terms.is_eq_clause g then 
-    let bag, ((i,_,_,_) as g1) = Sup.demodulate bag g (snd actives) in
-      if g1 = g then GaveUp else compute_result bag i []
-  else GaveUp
+
+  else GaveUp *)
 
 let fast_eq_check s goal =
   let (_,_,_,_,_,g_passives) as s = initialize_goal s goal in