Tseitin - Maple Help

Logic

 Tseitin
 apply Tseitin's transformation

 Calling Sequence Tseitin(b)

Parameters

 b - Boolean expression

Description

 • The Tseitin command 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).
 • It is possible to transform a boolean formula into CNF simply by repeated use of De Morgan's law, however in general this will result in an exponential increase in the number of terms. The result of Tseitin's transformation is linear in the number of Boolean operators in b.
 • The result of the Tseitin command will typically include additional variables not present in the original expression.

Examples

 > $\mathrm{with}\left(\mathrm{Logic}\right):$
 > $\mathrm{Tseitin}\left(a\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}&or\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left(b\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}&and\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}c\right)\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\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}&implies\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}b\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}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}&and\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathrm{Y1},\mathrm{X2}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}&and\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathrm{Y2},\mathrm{X3}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}&and\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathrm{Y3},\mathrm{X4}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}&and\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathrm{Y4},\mathrm{X5}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}&and\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathrm{Y5},\mathrm{X6}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}&and\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathrm{Y6},\mathrm{X7}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}&and\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathrm{Y7},\mathrm{X8}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}&and\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\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}}\right)$