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