Unit propagation minimizes the setup.

Clauses subsumed by new resolvents are removed.
While unit propagation itself becomes more expensive, it generally
improves performance because of smaller setups.