Tseitin - Maple Help

Logic

 Tseitin
 apply Tseitin's transformation

 Calling Sequence Tseitin(b)

Parameters

 b - Boolean expression

Description

 • Tseitin accepts an arbitrary Boolean expression b and returns an expression in conjunctive normal form (CNF) which is equisatisfiable, that is, a satisfying assignment of truth values exists for b if and only if a satisfying assignment exists for Tseitin(b).
 • The result of the Tseitin command will typically include additional variables not present in the original expression.
 • Note that it is possible to transform a boolean formula into CNF simply by repeated use of De Morgan's law, and this will produce an expression which is not merely equisatisfiable but logically equivalent. However, in general this will result in an exponential increase in the number of terms. By contrast the result of Tseitin's transformation is linear in the number of Boolean operators in b.

Examples

 > $\mathrm{with}\left(\mathrm{Logic}\right):$
 > $\mathrm{Tseitin}\left(a&orb&andc\right)$
 $\left({\mathrm{&or}}{}\left({\mathrm{B0}}\right)\right){\wedge }\left({\mathrm{B0}}{\vee }\left({¬}{a}\right)\right){\wedge }\left({\mathrm{B0}}{\vee }\left({¬}{B}\right)\right){\wedge }\left(\left({¬}{\mathrm{B0}}\right){\vee }{a}{\vee }{B}\right){\wedge }\left(\left({¬}{B}\right){\vee }{b}\right){\wedge }\left(\left({¬}{B}\right){\vee }{c}\right){\wedge }\left({B}{\vee }\left({¬}{b}\right){\vee }\left({¬}{c}\right)\right)$ (1)
 > $\mathrm{Tseitin}\left(a&impliesb\right)$
 ${\mathrm{&and}}{}\left({b}{\vee }\left({¬}{a}\right)\right)$ (2)

Illustrate the difference in increase in expression size between a straightforward application of De Morgan's law and the Tseitin transform.

 > $E≔\mathrm{&or}\left(\mathrm{X1}&and\mathrm{Y1},\mathrm{X2}&and\mathrm{Y2},\mathrm{X3}&and\mathrm{Y3},\mathrm{X4}&and\mathrm{Y4},\mathrm{X5}&and\mathrm{Y5},\mathrm{X6}&and\mathrm{Y6},\mathrm{X7}&and\mathrm{Y7},\mathrm{X8}&and\mathrm{Y8}\right)$
 ${E}{≔}\left({\mathrm{X1}}{\wedge }{\mathrm{Y1}}\right){\vee }\left({\mathrm{X2}}{\wedge }{\mathrm{Y2}}\right){\vee }\left({\mathrm{X3}}{\wedge }{\mathrm{Y3}}\right){\vee }\left({\mathrm{X4}}{\wedge }{\mathrm{Y4}}\right){\vee }\left({\mathrm{X5}}{\wedge }{\mathrm{Y5}}\right){\vee }\left({\mathrm{X6}}{\wedge }{\mathrm{Y6}}\right){\vee }\left({\mathrm{X7}}{\wedge }{\mathrm{Y7}}\right){\vee }\left({\mathrm{X8}}{\wedge }{\mathrm{Y8}}\right)$ (3)
 > $\mathrm{Result_DeMorgan}≔\mathrm{Logic}:-\mathrm{Normalize}\left(E,\mathrm{form}=\mathrm{CNF}\right)$
 ${\mathrm{Result_DeMorgan}}{≔}\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y6}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y5}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y4}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y6}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y3}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y6}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y5}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y6}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y2}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y6}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y5}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y4}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y6}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y6}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y5}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y6}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y6}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y5}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y4}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y6}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X3}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y3}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y6}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y5}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y6}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X2}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}\right){\wedge }\left({\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y6}}\right){\wedge }\left({\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y5}}\right){\wedge }\left({\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}\right){\wedge }\left({\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X3}}{\vee }{\mathrm{X4}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X3}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y4}}\right){\wedge }\left({\mathrm{X3}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X3}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X3}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X3}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y6}}\right){\wedge }\left({\mathrm{X3}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X3}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X3}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X3}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}\right){\wedge }\left({\mathrm{X3}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X3}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X3}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X3}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}\right){\wedge }\left({\mathrm{X3}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X3}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X3}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}\right){\wedge }\left({\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y6}}\right){\wedge }\left({\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X4}}{\vee }{\mathrm{X5}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X4}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y5}}\right){\wedge }\left({\mathrm{X4}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X4}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X4}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X4}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}\right){\wedge }\left({\mathrm{X4}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X4}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X4}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}\right){\wedge }\left({\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X5}}{\vee }{\mathrm{X6}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X5}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y6}}\right){\wedge }\left({\mathrm{X5}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X5}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X5}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}\right){\wedge }\left({\mathrm{X6}}{\vee }{\mathrm{X7}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X6}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{X6}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X7}}{\vee }{\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}\right){\wedge }\left({\mathrm{X7}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y8}}\right){\wedge }\left({\mathrm{X8}}{\vee }{\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}\right){\wedge }\left({\mathrm{Y1}}{\vee }{\mathrm{Y2}}{\vee }{\mathrm{Y3}}{\vee }{\mathrm{Y4}}{\vee }{\mathrm{Y5}}{\vee }{\mathrm{Y6}}{\vee }{\mathrm{Y7}}{\vee }{\mathrm{Y8}}\right)$ (4)
 > $\mathrm{length}\left(\mathrm{Result_DeMorgan}\right)$
 ${8200}$ (5)
 > $\mathrm{Result_Tseitin}≔\mathrm{Tseitin}\left(E\right):$
 > $\mathrm{length}\left(\mathrm{Result_Tseitin}\right)$
 ${895}$ (6)

References

 Tseitin, G.S. On the complexity of derivation in propositional calculus. In A. O. Slisenko, editor, Studies in Constructive Mathematics and Mathematical Logic, pp. 115–125, 1970.

Compatibility

 • The Logic[Tseitin] command was introduced in Maple 2016.