Rewrite rule that applies unit resolution to propagate unit clauses.
See: https://en.wikipedia.org/wiki/Unit_propagation
Applies the transformations:
A AND (NOT A OR B) = A AND B(unit A eliminates NOT A from clause)(NOT A OR B) AND A = B AND A(unit A eliminates NOT A from clause)(NOT A) AND (A OR B) = (NOT A) AND B(unit NOT A eliminates A from clause)(A OR B) AND (NOT A) = B AND (NOT A)(unit NOT A eliminates A from clause)
Unit resolution propagates the effect of unit clauses (single literals) by eliminating contradictory literals from other clauses.