Unit Deletion "Unit Deletion acts rather like demodulation, automatically removing a literal in a clause when a unit clause exists that unifies with the literal, that is opposite in sign, and such that the unification does not affect the variables in the literal in question."