Satz: Falls M eine Teilformel T (also x = y oder x y)
enthält, die auf keinem Widerspruchskreis vorkommt,
dann ist M' : = M[T/true] erfüllbarkeitsäquivalent zu M.
Beweis: eine Richtung ist trivial, für die andere: konstruiere aus erfüllender Belegung von M' eine erfüllende Belegung von M.
Algorithmus: solange wie möglich