where we used that we 0 = w. Finally, by plugging (26) into (25) we get

$$\operatorname*{min}_{\begin{array}{l}{\alpha\in{\cal C}_{*}}\\ {\alpha\neq p}\end{array}}w_{\overline{{{\alpha}}}}\ \leq\ \operatorname*{min}\left(w_{q}\,,\,\operatorname*{min}_{\begin{array}{l}{\alpha\in{\cal C}_{2}}\\ {\alpha\neq\overline{{{q}}}}\\ {\alpha\neq p}\end{array}}w_{\overline{{{\alpha}}}}\right)\ =\ \operatorname*{min}_{\begin{array}{l}{\alpha\in{\cal C}_{2}}\\ {\alpha\neq p}\end{array}}w_{\overline{{{\alpha}}}}\ \leq\ \widetilde{w}_{p}^{\prime},\tag{27}$$

as desired. Corollary 4.6. *Any disjoint-resolvable prime conjunctive normal form is*
∗-equivalent to the Blake canonical form.

Proof. Let Φ and Φ denote respectively the Blake canonical form and a e disjoint-resolvable prime conjunctive normal form. Since we can go from Φe to Φ via disjoint resolution and absorption, Propositions 4.5 and 4.2 ensure that v
∗ ≤ ve
∗. On the other hand, the reverse inequality is guaranteed by Proposition 4.3, since the disjoint resolvability of Φ certainly ensures that e Φ is logically equivalent to Φ. e Related to the preceding results, one can see that disjoint resolvability ensures not only ∗-equivalence, but also equivalence with respect to the property of definite consistency of a partial truth assignment:
Proposition 4.7. A partial truth assignment is definitely consistent for a disjoint-resolvable conjunctive normal form if and only if it is definitely consistent for the corresponding Blake canonical form.

Proof. Let Φ and Φ denote respectively the Blake canonical form and a e disjoint-resolvable conjunctive normal form. The claim that definite consistency with Φ implies definite consistency with Φ follows from the easily e checked fact that definite consistency is preserved by the operations of absorption and disjoint resolution. The converse implication is a simple consequence of the definition of the Blake canonical form, which ensures that every clause of Φ contains, as a set of literals, some clause of Φ. e Remark. The definition of disjoint resolvability implies going through (a special form of) the process of generating the Blake canonical form. On the other hand, the latter is also required for checking whether a given conjunctive normal form is prime. It would certainly be very interesting to be able to recognise these properties without having to go through the process of generating the Blake canonical form.