--- a/src/Tools/Metis/src/Active.sml Tue Nov 13 17:04:16 2007 +0100
+++ b/src/Tools/Metis/src/Active.sml Tue Nov 13 18:29:28 2007 +0100
@@ -453,18 +453,18 @@
(* Derive (unfactored) consequences of a clause. *)
(* ------------------------------------------------------------------------- *)
-fun deduceResolution literals cl (lit,acc) =
+fun deduceResolution literals cl (lit as (_,atm), acc) =
let
fun resolve (cl_lit,acc) =
case total (Clause.resolve cl_lit) (cl,lit) of
SOME cl' => cl' :: acc
| NONE => acc
-
(*TRACE4
val () = Parser.ppTrace Literal.pp "Active.deduceResolution: lit" lit
*)
in
- foldl resolve acc (LiteralNet.unify literals (Literal.negate lit))
+ if Atom.isEq atm then acc
+ else foldl resolve acc (LiteralNet.unify literals (Literal.negate lit))
end;
fun deduceParamodulationWith subterms cl ((lit,ort,tm),acc) =