Furthermore, the maximal length of a < increasing chain of constraints is bounded by n 2 , where n is the number of variables.
applications of (Distr) can only be iterated a finite number of times on constraints without simple hypernormal cycles (given redundancy elimination), and it follows by induction that ϕ is satisfiable.