Mise sous forme clausale de $C(b, b^{\prime })$

Il est possible de prouver par récurrence sur $l$[2] que l'expression

$$C(b, b^{\prime}) = \bigvee_{i=1}^{l}((\Delta(b)\geq x_{i})\wedge(\Delta(b^{\prime})\geq y_{i}))$$

équivaut à l'expression

$$C(b, b^{\prime}) = (\Delta(b)\geq x_{l})\wedge(\Delta(b^{\pri... ...l-1}((\Delta(b)\geq x_{i})\vee(\Delta(b^{\prime})\geq y_{i+1}))$$

On obtient de cette façon un ensemble de clauses à satisfaire.