\documentclass{article}
\newtheorem{axiom}{Axiom}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{proposition}{Proposition}
\newtheorem{definition}{Definition}
\newtheorem{example}{Example}
\newtheorem{conjecture}{Conjecture}
\newcommand\unicdcdgdad{\not=}
\newcommand\unicdcdcdbg{\cup}
\newcommand\unicdcdbdgd{\setminus}
\newcommand\unicdcdcdjd{\cap}
\newcommand\unicdcdadad{\forall}
\newcommand\unicdbdjdcd{\Rightarrow}
\newcommand\unicdcdadjd{\notin}
\newcommand\unicdbdjded{\Leftrightarrow}
\newcommand\unicdcdcdid{\lor}
\newcommand\unicdcdcdhd{\land}
\newcommand\uniddcgcg{\lambda}
\newcommand\unicdcdaddd{\exists}
\newcommand\unicdcdidid{\not\subseteq}
\newcommand\preoh[1]{\lnot #1}
\newcommand\mname[1]{{\mathsf{#1}}}
\begin{document}
\title{t5\_gate\_3 (TMVfDFh8px1dF5CBNStRiuRPFPfh4aTFyDe)}
\maketitle
Let $ v1\_xboole\_0 : {{\iota}{\unicdbdjdcd}{o}}$ be given.
Let $ k14\_gate\_1 : {{\iota}{\unicdbdjdcd}{{\iota}{\unicdbdjdcd}{{\iota}{\unicdbdjdcd}{{\iota}{\unicdbdjdcd}{\iota}}}}}$ be given.
Let $ k1\_gate\_1 : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} X0 .  {\unicdcdadad} X1 .  {\unicdcdadad} X2 .  {\unicdcdadad} X3 .  (\preoh v1\_xboole\_0~(k14\_gate\_1~\\
X0~X1~X2~X3)){\unicdbdjded}((\preoh v1\_xboole\_0~X0){\unicdcdcdhd}((\preoh v1\_xboole\_0~X1){\unicdcdcdhd}((\preoh v1\_xboole\_0~\\
X2){\unicdcdcdhd}(\preoh v1\_xboole\_0~X3))))\end{array}
\label{hyp:ehcdadpfhgbgehfgpfbd}
\end{equation}
Assume the following.
\begin{equation}
{{\unicdcdadad} X0 .  {{({\preoh{{{v1\_xboole\_0}~{X0}}}})}{\unicdbdjdcd}{({{v1\_xboole\_0}~{({{k1\_gate\_1}~{X0}})}})}}}\label{hyp:ggdgcdpfhgbgehfgpfbd}
\end{equation}
Assume the following.
\begin{equation}
{{\unicdcdadad} X0 .  {{({{v1\_xboole\_0}~{X0}})}{\unicdbdjdcd}{({\preoh{{{v1\_xboole\_0}~{({{k1\_gate\_1}~{X0}})}}}})}}}\label{hyp:ggdgbdpfhgbgehfgpfbd}
\end{equation}
\begin{theorem}\label{thm:ehfdpfhgbgehfgpfdd}
$$\begin{array}{c}{\unicdcdadad} X0 .  {\unicdcdadad} X1 .  {\unicdcdadad} X2 .  {\unicdcdadad} X3 .  {\unicdcdadad} X4 .  {\unicdcdadad} X5 .  \\
{\unicdcdadad} X6 .  {\unicdcdadad} X7 .  {\unicdcdadad} X8 .  {\unicdcdadad} X9 .  {\unicdcdadad} X10 .  {\unicdcdadad} X11 .  \\
{\unicdcdadad} X12 .  {\unicdcdadad} X13 .  {\unicdcdadad} X14 .  {\unicdcdadad} X15 .  {\unicdcdadad} X16 .  \\
{\unicdcdadad} X17 .  {\unicdcdadad} X18 .  {\unicdcdadad} X19 .  {\unicdcdadad} X20 .  {\unicdcdadad} X21 .  \\
{\unicdcdadad} X22 .  {\unicdcdadad} X23 .  {\unicdcdadad} X24 .  {\unicdcdadad} X25 .  {\unicdcdadad} X26 .  \\
{\unicdcdadad} X27 .  {\unicdcdadad} X28 .  {\unicdcdadad} X29 .  {\unicdcdadad} X30 .  {\unicdcdadad} X31 .  \\
{\unicdcdadad} X32 .  {\unicdcdadad} X33 .  {\unicdcdadad} X34 .  {\unicdcdadad} X35 .  {\unicdcdadad} X36 .  \\
{\unicdcdadad} X37 .  {\unicdcdadad} X38 .  {\unicdcdadad} X39 .  \preoh (\preoh (\preoh v1\_xboole\_0~X0){\unicdcdcdhd}(v1\_xboole\_0~\\
(k14\_gate\_1~(k1\_gate\_1~X35)~(k1\_gate\_1~X34)~(k1\_gate\_1~X33)~(k1\_gate\_1~\\
X32)))){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~(k14\_gate\_1~(k1\_gate\_1~X35)~(k1\_gate\_1~\\
X34)~(k1\_gate\_1~X33)~(k1\_gate\_1~X32))){\unicdcdcdhd}(v1\_xboole\_0~X0)){\unicdcdcdhd}((\preoh \\
(\preoh v1\_xboole\_0~X1){\unicdcdcdhd}(v1\_xboole\_0~(k14\_gate\_1~(k1\_gate\_1~X35)~(\\
k1\_gate\_1~X34)~(k1\_gate\_1~X33)~X32))){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~(k14\_gate\_1~\\
(k1\_gate\_1~X35)~(k1\_gate\_1~X34)~(k1\_gate\_1~X33)~X32)){\unicdcdcdhd}(v1\_xboole\_0~\\
X1)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X2){\unicdcdcdhd}(v1\_xboole\_0~(k14\_gate\_1~(k1\_gate\_1~\\
X35)~(k1\_gate\_1~X34)~X33~(k1\_gate\_1~X32)))){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~\\
(k14\_gate\_1~(k1\_gate\_1~X35)~(k1\_gate\_1~X34)~X33~(k1\_gate\_1~X32))){\unicdcdcdhd}\\
(v1\_xboole\_0~X2)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X3){\unicdcdcdhd}(v1\_xboole\_0~(k14\_gate\_1~\\
(k1\_gate\_1~X35)~(k1\_gate\_1~X34)~X33~X32))){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~(\\
k14\_gate\_1~(k1\_gate\_1~X35)~(k1\_gate\_1~X34)~X33~X32)){\unicdcdcdhd}(v1\_xboole\_0~\\
X3)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X4){\unicdcdcdhd}(v1\_xboole\_0~(k14\_gate\_1~(k1\_gate\_1~\\
X35)~X34~(k1\_gate\_1~X33)~(k1\_gate\_1~X32)))){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~\\
(k14\_gate\_1~(k1\_gate\_1~X35)~X34~(k1\_gate\_1~X33)~(k1\_gate\_1~X32))){\unicdcdcdhd}\\
(v1\_xboole\_0~X4)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X5){\unicdcdcdhd}(v1\_xboole\_0~(k14\_gate\_1~\\
(k1\_gate\_1~X35)~X34~(k1\_gate\_1~X33)~X32))){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~(\\
k14\_gate\_1~(k1\_gate\_1~X35)~X34~(k1\_gate\_1~X33)~X32)){\unicdcdcdhd}(v1\_xboole\_0~\\
X5)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X6){\unicdcdcdhd}(v1\_xboole\_0~(k14\_gate\_1~(k1\_gate\_1~\\
X35)~X34~X33~(k1\_gate\_1~X32)))){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~(k14\_gate\_1~\\
(k1\_gate\_1~X35)~X34~X33~(k1\_gate\_1~X32))){\unicdcdcdhd}(v1\_xboole\_0~X6)){\unicdcdcdhd}(\\
(\preoh (\preoh v1\_xboole\_0~X7){\unicdcdcdhd}(v1\_xboole\_0~(k14\_gate\_1~(k1\_gate\_1~X35)~\\
X34~X33~X32))){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~(k14\_gate\_1~(k1\_gate\_1~X35)~X34~\\
X33~X32)){\unicdcdcdhd}(v1\_xboole\_0~X7)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X8){\unicdcdcdhd}(v1\_xboole\_0~\\
(k14\_gate\_1~X35~(k1\_gate\_1~X34)~(k1\_gate\_1~X33)~(k1\_gate\_1~X32)))){\unicdcdcdhd}\\
((\preoh (\preoh v1\_xboole\_0~(k14\_gate\_1~X35~(k1\_gate\_1~X34)~(k1\_gate\_1~X33)~\\
(k1\_gate\_1~X32))){\unicdcdcdhd}(v1\_xboole\_0~X8)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X9){\unicdcdcdhd}(\\
v1\_xboole\_0~(k14\_gate\_1~X35~(k1\_gate\_1~X34)~(k1\_gate\_1~X33)~X32))){\unicdcdcdhd}\\
((\preoh (\preoh v1\_xboole\_0~(k14\_gate\_1~X35~(k1\_gate\_1~X34)~(k1\_gate\_1~X33)~\\
X32)){\unicdcdcdhd}(v1\_xboole\_0~X9)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X10){\unicdcdcdhd}(v1\_xboole\_0~\\
(k14\_gate\_1~X35~(k1\_gate\_1~X34)~X33~(k1\_gate\_1~X32)))){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~\\
(k14\_gate\_1~X35~(k1\_gate\_1~X34)~X33~(k1\_gate\_1~X32))){\unicdcdcdhd}(v1\_xboole\_0~\\
X10)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X11){\unicdcdcdhd}(v1\_xboole\_0~(k14\_gate\_1~X35~(k1\_gate\_1~\\
X34)~X33~X32))){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~(k14\_gate\_1~X35~(k1\_gate\_1~X34)~\\
X33~X32)){\unicdcdcdhd}(v1\_xboole\_0~X11)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X12){\unicdcdcdhd}(v1\_xboole\_0~\\
(k14\_gate\_1~X35~X34~(k1\_gate\_1~X33)~(k1\_gate\_1~X32)))){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~\\
(k14\_gate\_1~X35~X34~(k1\_gate\_1~X33)~(k1\_gate\_1~X32))){\unicdcdcdhd}(v1\_xboole\_0~\\
X12)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X13){\unicdcdcdhd}(v1\_xboole\_0~(k14\_gate\_1~X35~X34~\\
(k1\_gate\_1~X33)~X32))){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~(k14\_gate\_1~X35~X34~(\\
k1\_gate\_1~X33)~X32)){\unicdcdcdhd}(v1\_xboole\_0~X13)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X14){\unicdcdcdhd}\\
(v1\_xboole\_0~(k14\_gate\_1~X35~X34~X33~(k1\_gate\_1~X32)))){\unicdcdcdhd}((\preoh (\preoh \\
v1\_xboole\_0~(k14\_gate\_1~X35~X34~X33~(k1\_gate\_1~X32))){\unicdcdcdhd}(v1\_xboole\_0~\\
X14)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X15){\unicdcdcdhd}(v1\_xboole\_0~(k14\_gate\_1~X35~X34~\\
X33~X32))){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~(k14\_gate\_1~X35~X34~X33~X32)){\unicdcdcdhd}(v1\_xboole\_0~\\
X15)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X16){\unicdcdcdhd}(v1\_xboole\_0~(k14\_gate\_1~(k1\_gate\_1~\\
X39)~(k1\_gate\_1~X38)~(k1\_gate\_1~X37)~(k1\_gate\_1~X36)))){\unicdcdcdhd}((\preoh (\preoh \\
v1\_xboole\_0~(k14\_gate\_1~(k1\_gate\_1~X39)~(k1\_gate\_1~X38)~(k1\_gate\_1~\\
X37)~(k1\_gate\_1~X36))){\unicdcdcdhd}(v1\_xboole\_0~X16)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~\\
X17){\unicdcdcdhd}(v1\_xboole\_0~(k14\_gate\_1~(k1\_gate\_1~X39)~(k1\_gate\_1~X38)~\\
(k1\_gate\_1~X37)~X36))){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~(k14\_gate\_1~(k1\_gate\_1~\\
X39)~(k1\_gate\_1~X38)~(k1\_gate\_1~X37)~X36)){\unicdcdcdhd}(v1\_xboole\_0~X17)){\unicdcdcdhd}\\
((\preoh (\preoh v1\_xboole\_0~X18){\unicdcdcdhd}(v1\_xboole\_0~(k14\_gate\_1~(k1\_gate\_1~X39)~\\
(k1\_gate\_1~X38)~X37~(k1\_gate\_1~X36)))){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~(k14\_gate\_1~\\
(k1\_gate\_1~X39)~(k1\_gate\_1~X38)~X37~(k1\_gate\_1~X36))){\unicdcdcdhd}(v1\_xboole\_0~\\
X18)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X19){\unicdcdcdhd}(v1\_xboole\_0~(k14\_gate\_1~(k1\_gate\_1~\\
X39)~(k1\_gate\_1~X38)~X37~X36))){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~(k14\_gate\_1~\\
(k1\_gate\_1~X39)~(k1\_gate\_1~X38)~X37~X36)){\unicdcdcdhd}(v1\_xboole\_0~X19)){\unicdcdcdhd}\\
((\preoh (\preoh v1\_xboole\_0~X20){\unicdcdcdhd}(v1\_xboole\_0~(k14\_gate\_1~(k1\_gate\_1~X39)~\\
X38~(k1\_gate\_1~X37)~(k1\_gate\_1~X36)))){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~(k14\_gate\_1~\\
(k1\_gate\_1~X39)~X38~(k1\_gate\_1~X37)~(k1\_gate\_1~X36))){\unicdcdcdhd}(v1\_xboole\_0~\\
X20)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X21){\unicdcdcdhd}(v1\_xboole\_0~(k14\_gate\_1~(k1\_gate\_1~\\
X39)~X38~(k1\_gate\_1~X37)~X36))){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~(k14\_gate\_1~\\
(k1\_gate\_1~X39)~X38~(k1\_gate\_1~X37)~X36)){\unicdcdcdhd}(v1\_xboole\_0~X21)){\unicdcdcdhd}\\
((\preoh (\preoh v1\_xboole\_0~X22){\unicdcdcdhd}(v1\_xboole\_0~(k14\_gate\_1~(k1\_gate\_1~X39)~\\
X38~X37~(k1\_gate\_1~X36)))){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~(k14\_gate\_1~(k1\_gate\_1~\\
X39)~X38~X37~(k1\_gate\_1~X36))){\unicdcdcdhd}(v1\_xboole\_0~X22)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~\\
X23){\unicdcdcdhd}(v1\_xboole\_0~(k14\_gate\_1~(k1\_gate\_1~X39)~X38~X37~X36))){\unicdcdcdhd}\\
((\preoh (\preoh v1\_xboole\_0~(k14\_gate\_1~(k1\_gate\_1~X39)~X38~X37~X36)){\unicdcdcdhd}(v1\_xboole\_0~\\
X23)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X24){\unicdcdcdhd}(v1\_xboole\_0~(k14\_gate\_1~X39~(k1\_gate\_1~\\
X38)~(k1\_gate\_1~X37)~(k1\_gate\_1~X36)))){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~(k14\_gate\_1~\\
X39~(k1\_gate\_1~X38)~(k1\_gate\_1~X37)~(k1\_gate\_1~X36))){\unicdcdcdhd}(v1\_xboole\_0~\\
X24)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X25){\unicdcdcdhd}(v1\_xboole\_0~(k14\_gate\_1~X39~(k1\_gate\_1~\\
X38)~(k1\_gate\_1~X37)~X36))){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~(k14\_gate\_1~X39~\\
(k1\_gate\_1~X38)~(k1\_gate\_1~X37)~X36)){\unicdcdcdhd}(v1\_xboole\_0~X25)){\unicdcdcdhd}((\preoh \\
(\preoh v1\_xboole\_0~X26){\unicdcdcdhd}(v1\_xboole\_0~(k14\_gate\_1~X39~(k1\_gate\_1~X38)~\\
X37~(k1\_gate\_1~X36)))){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~(k14\_gate\_1~X39~(k1\_gate\_1~\\
X38)~X37~(k1\_gate\_1~X36))){\unicdcdcdhd}(v1\_xboole\_0~X26)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~\\
X27){\unicdcdcdhd}(v1\_xboole\_0~(k14\_gate\_1~X39~(k1\_gate\_1~X38)~X37~X36))){\unicdcdcdhd}\\
((\preoh (\preoh v1\_xboole\_0~(k14\_gate\_1~X39~(k1\_gate\_1~X38)~X37~X36)){\unicdcdcdhd}(v1\_xboole\_0~\\
X27)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X28){\unicdcdcdhd}(v1\_xboole\_0~(k14\_gate\_1~X39~X38~\\
(k1\_gate\_1~X37)~(k1\_gate\_1~X36)))){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~(k14\_gate\_1~\\
X39~X38~(k1\_gate\_1~X37)~(k1\_gate\_1~X36))){\unicdcdcdhd}(v1\_xboole\_0~X28)){\unicdcdcdhd}\\
((\preoh (\preoh v1\_xboole\_0~X29){\unicdcdcdhd}(v1\_xboole\_0~(k14\_gate\_1~X39~X38~(k1\_gate\_1~\\
X37)~X36))){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~(k14\_gate\_1~X39~X38~(k1\_gate\_1~X37)~\\
X36)){\unicdcdcdhd}(v1\_xboole\_0~X29)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X30){\unicdcdcdhd}(v1\_xboole\_0~\\
(k14\_gate\_1~X39~X38~X37~(k1\_gate\_1~X36)))){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~(\\
k14\_gate\_1~X39~X38~X37~(k1\_gate\_1~X36))){\unicdcdcdhd}(v1\_xboole\_0~X30)){\unicdcdcdhd}(\\
(\preoh (\preoh v1\_xboole\_0~X31){\unicdcdcdhd}(v1\_xboole\_0~(k14\_gate\_1~X39~X38~X37~X36))){\unicdcdcdhd}\\
((\preoh (\preoh v1\_xboole\_0~(k14\_gate\_1~X39~X38~X37~X36)){\unicdcdcdhd}(v1\_xboole\_0~X31)){\unicdcdcdhd}\\
((\preoh (\preoh v1\_xboole\_0~X36){\unicdcdcdhd}(v1\_xboole\_0~(k1\_gate\_1~X35))){\unicdcdcdhd}((\preoh (\preoh \\
v1\_xboole\_0~(k1\_gate\_1~X35)){\unicdcdcdhd}(v1\_xboole\_0~X36)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~\\
X37){\unicdcdcdhd}(v1\_xboole\_0~X32)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X32){\unicdcdcdhd}(v1\_xboole\_0~\\
X37)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X38){\unicdcdcdhd}(v1\_xboole\_0~X33)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~\\
X33){\unicdcdcdhd}(v1\_xboole\_0~X38)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X39){\unicdcdcdhd}(v1\_xboole\_0~\\
X34)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X34){\unicdcdcdhd}(v1\_xboole\_0~X39)){\unicdcdcdhd}(\preoh (\preoh (\preoh v1\_xboole\_0~\\
X17){\unicdcdcdhd}(v1\_xboole\_0~X0)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X0){\unicdcdcdhd}(v1\_xboole\_0~X17)){\unicdcdcdhd}\\
((\preoh (\preoh v1\_xboole\_0~X19){\unicdcdcdhd}(v1\_xboole\_0~X1)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X1){\unicdcdcdhd}\\
(v1\_xboole\_0~X19)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X23){\unicdcdcdhd}(v1\_xboole\_0~X3)){\unicdcdcdhd}\\
((\preoh (\preoh v1\_xboole\_0~X3){\unicdcdcdhd}(v1\_xboole\_0~X23)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X31){\unicdcdcdhd}\\
(v1\_xboole\_0~X7)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X7){\unicdcdcdhd}(v1\_xboole\_0~X31)){\unicdcdcdhd}\\
((\preoh (\preoh v1\_xboole\_0~X30){\unicdcdcdhd}(v1\_xboole\_0~X15)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~\\
X15){\unicdcdcdhd}(v1\_xboole\_0~X30)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X28){\unicdcdcdhd}(v1\_xboole\_0~\\
X14)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X14){\unicdcdcdhd}(v1\_xboole\_0~X28)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~\\
X24){\unicdcdcdhd}(v1\_xboole\_0~X12)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X12){\unicdcdcdhd}(v1\_xboole\_0~\\
X24)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X16){\unicdcdcdhd}(v1\_xboole\_0~X8)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~\\
X8){\unicdcdcdhd}(v1\_xboole\_0~X16)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X21){\unicdcdcdhd}(v1\_xboole\_0~\\
X2)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X2){\unicdcdcdhd}(v1\_xboole\_0~X21)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~\\
X27){\unicdcdcdhd}(v1\_xboole\_0~X5)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X5){\unicdcdcdhd}(v1\_xboole\_0~X27)){\unicdcdcdhd}\\
((\preoh (\preoh v1\_xboole\_0~X22){\unicdcdcdhd}(v1\_xboole\_0~X11)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~\\
X11){\unicdcdcdhd}(v1\_xboole\_0~X22)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X29){\unicdcdcdhd}(v1\_xboole\_0~\\
X6)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X6){\unicdcdcdhd}(v1\_xboole\_0~X29)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~\\
X26){\unicdcdcdhd}(v1\_xboole\_0~X13)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X13){\unicdcdcdhd}(v1\_xboole\_0~\\
X26)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X20){\unicdcdcdhd}(v1\_xboole\_0~X10)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~\\
X10){\unicdcdcdhd}(v1\_xboole\_0~X20)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X25){\unicdcdcdhd}(v1\_xboole\_0~\\
X4)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X4){\unicdcdcdhd}(v1\_xboole\_0~X25)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~\\
X18){\unicdcdcdhd}(v1\_xboole\_0~X9)){\unicdcdcdhd}(\preoh (\preoh v1\_xboole\_0~X9){\unicdcdcdhd}(v1\_xboole\_0~X18))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))\end{array}$$
\end{theorem}
\end{document}
