In proof compression LowerUnits (LU) is an algorithm used to compress propositional logic resolution proofs. The main idea of LowerUnits is to exploit the following fact: Theorem: Let be a potentially redundant proof, and be the redundant proof | redundant node. If ’s clause is a unit clause, then is redundant. The algorithm targets exactly the class of global redundancy stemming from multiple resolutions with unit clauses. The algorithm takes its name from the fact that, when this rewriting is done and the resulting proof is displayed as a DAG (directed acyclic graph), the unit node depends on from