Soit $\Sigma$ un ensemble de clauses contradictoires. Alors il existe un arbre de réfutation de $\Sigma$.