\documentclass[a4paper,10pt]{article}
\usepackage[utf8]{inputenc}
\usepackage{pdfpages}
\usepackage{latexsym}
\usepackage{amssymb,amsthm,amsmath}
\usepackage{amsthm}

\begin{document}
 \newcommand{\nxt}{{\ensuremath\raisebox{0.25ex}{\text{\scriptsize$\bigcirc$}}}}
\newcommand{\Rdiamond}{\Diamond_{\!F}}
\newcommand{\Rbox}{\Box_{\!F}}
\newcommand{\Rnext}{\nxt_{\!F}}
\newcommand{\Ldiamond}{\Diamond_{\!P}}
\newcommand{\Lbox}{\Box_{\!P}}
\newcommand{\Lnext}{\nxt_{\!P}}
\newcommand{\SVdiamond}{\mathop{\ooalign{$\Diamond$ \cr \kern0.5ex
    \raisebox{0.35ex}{\scalebox{0.7}{$*$}}} \kern-0.9ex}}
\newcommand{\SVbox}{\mathop{\ooalign{$\Box$ \cr \kern0.42ex
    \raisebox{0.3ex}{\scalebox{0.7}{$*$}}} \kern-0.9ex}}


$((BOX14F_{John} \leftrightarrow BOX18P_{John}) \land $ \\ 
 $ (BOX14F_{N0} \leftrightarrow BOX18P_{N0}) \land $ \\ 
 $ (PinvNameF \leftrightarrow PinvNameF) \land $ \\ 
 $ (BOX27F_{N0} \leftrightarrow BOX20P_{N0}) \land $ \\ 
 $ (BOX29F_{dNameInv} \leftrightarrow BOX22P_{dNameInv}) \land $ \\ 
 $ (BOX0F_{dNameInv} \leftrightarrow BOX33P_{dNameInv}) \land $ \\ 
 $ (E1NameInvF_{N0} \leftrightarrow E1NameInvP_{N0}) \land $ \\ 
 $ (BOX30F_{dName} \leftrightarrow BOX23P_{dName}) \land $ \\ 
 $ (BOX1F_{dNameInv} \leftrightarrow BOX34P_{dNameInv}) \land $ \\ 
 $ (E1NameF_{dNameInv} \leftrightarrow E1NameP_{dNameInv}) \land $ \\ 
 $ (BOX10F_{N0} \leftrightarrow BOX6P_{N0}) \land $ \\ 
 $ (BOX12F_{dName} \leftrightarrow BOX16P_{dName}) \land $ \\ 
 $ (PinvNameF \leftrightarrow PinvNameF) \land $ \\ 
 $ (E1NameF_{dName} \leftrightarrow E1NameP_{dName}) \land $ \\ 
 $ (PNameF \leftrightarrow PNameF) \land $ \\ 
 $ (E1NameInvF_{dNameInv} \leftrightarrow E1NameInvP_{dNameInv}) \land $ \\ 
 $ (BOX30F_{N0} \leftrightarrow BOX23P_{N0}) \land $ \\ 
 $ (PersonF_{dName} \leftrightarrow PersonP_{dName}) \land $ \\ 
 $ (BOX30F_{John} \leftrightarrow BOX23P_{John}) \land $ \\ 
 $  \Rbox ((NXT17P_{N0} \leftrightarrow  \Rnext BOX18P_{N0}) \land $ \\ 
 $ ( \Rnext NXT13F_{N0} \leftrightarrow BOX14F_{N0}) \land $ \\ 
 $ (NXT7F_{N0} \leftrightarrow  \Rnext BOX8F_{N0}) \land $ \\ 
 $ (NXT9F_{N0} \leftrightarrow  \Rnext BOX10F_{N0}) \land $ \\ 
 $ ( \Rnext NXT11F_{N0} \leftrightarrow BOX12F_{N0}) \land $ \\ 
 $ ( \Rnext NXT5P_{N0} \leftrightarrow BOX6P_{N0}) \land $ \\ 
 $ (NXT15P_{N0} \leftrightarrow  \Rnext BOX16P_{N0}) \land $ \\ 
 $ ( \Rnext NXT3P_{N0} \leftrightarrow BOX4P_{N0}) \land $ \\ 
 $ (BOX18P_{N0} \leftrightarrow  \Rbox E2NameP_{N0}) \land $ \\ 
 $ ( \Rnext BOX14F_{N0} \leftrightarrow ( \Rnext E2NameF_{N0} \land $ \\ 
 $ BOX14F_{N0})) \land $ \\ 
 $ ( \Rnext BOX0F_{N0} \leftrightarrow ( \Rnext BOX26F_{N0} \land $ \\ 
 $ BOX0F_{N0})) \land $ \\ 
 $ (BOX20P_{N0} \leftrightarrow  \Rbox BOX21P_{N0}) \land $ \\ 
 $ (BOX10F_{N0} \leftrightarrow  \Rbox NXT13F_{N0}) \land $ \\ 
 $ ( \Rnext BOX1F_{N0} \leftrightarrow ( \Rnext BOX29F_{N0} \land $ \\ 
 $ BOX1F_{N0})) \land $ \\ 
 $ (BOX16P_{N0} \leftrightarrow  \Rbox E1NameP_{N0}) \land $ \\ 
 $ (BOX32F_{N0} \leftrightarrow  \Rbox ((PersonF_{N0} \rightarrow E1NameF_{N0}) \land $ \\ 
 $ (PersonF_{N0} \rightarrow  \lnot E2NameF_{N0}) \land $ \\ 
 $ (E2NameF_{N0} \rightarrow E1NameF_{N0}) \land $ \\ 
 $ (E1NameF_{N0} \rightarrow NXT7F_{N0}) \land $ \\ 
 $ (E2NameF_{N0} \rightarrow NXT9F_{N0}))) \land $ \\ 
 $ ( \Rnext BOX2F_{N0} \leftrightarrow ( \Rnext BOX32F_{N0} \land $ \\ 
 $ BOX2F_{N0})) \land $ \\ 
 $ (BOX29F_{N0} \leftrightarrow  \Rbox (E1NameF_{N0} \rightarrow BOX30F_{N0})) \land $ \\ 
 $ ( \Rnext BOX27F_{N0} \leftrightarrow ( \Rnext BOX28F_{N0} \land $ \\ 
 $ BOX27F_{N0})) \land $ \\ 
 $ ( \Rnext BOX4P_{N0} \leftrightarrow ( \Rnext NXT15P_{N0} \land $ \\ 
 $ BOX4P_{N0})) \land $ \\ 
 $ (BOX23P_{N0} \leftrightarrow  \Rbox BOX24P_{N0}) \land $ \\ 
 $ ( \Rnext BOX22P_{N0} \leftrightarrow ( \Rnext (E1NameP_{N0} \rightarrow BOX23P_{N0}) \land $ \\ 
 $ BOX22P_{N0})) \land $ \\ 
 $ (BOX34P_{N0} \leftrightarrow  \Rbox BOX22P_{N0}) \land $ \\ 
 $ ( \Rnext BOX6P_{N0} \leftrightarrow ( \Rnext NXT17P_{N0} \land $ \\ 
 $ BOX6P_{N0})) \land $ \\ 
 $ (BOX31F_{N0} \leftrightarrow  \Rbox PNameF) \land $ \\ 
 $ ( \Rnext BOX30F_{N0} \leftrightarrow ( \Rnext BOX31F_{N0} \land $ \\ 
 $ BOX30F_{N0})) \land $ \\ 
 $ (BOX26F_{N0} \leftrightarrow  \Rbox (E1NameInvF_{N0} \rightarrow BOX27F_{N0})) \land $ \\ 
 $ (BOX35P_{N0} \leftrightarrow  \Rbox BOX25P_{N0}) \land $ \\ 
 $ (BOX33P_{N0} \leftrightarrow  \Rbox BOX19P_{N0}) \land $ \\ 
 $ ( \Rnext BOX25P_{N0} \leftrightarrow ( \Rnext ((PersonP_{N0} \rightarrow E1NameP_{N0}) \land $ \\ 
 $ (PersonP_{N0} \rightarrow  \lnot E2NameP_{N0}) \land $ \\ 
 $ (E2NameP_{N0} \rightarrow E1NameP_{N0}) \land $ \\ 
 $ (E1NameP_{N0} \rightarrow NXT3P_{N0}) \land $ \\ 
 $ (E2NameP_{N0} \rightarrow NXT5P_{N0})) \land $ \\ 
 $ BOX25P_{N0})) \land $ \\ 
 $ ( \Rnext BOX24P_{N0} \leftrightarrow ( \Rnext PNameF \land $ \\ 
 $ BOX24P_{N0})) \land $ \\ 
 $ (BOX28F_{N0} \leftrightarrow  \Rbox PinvNameF) \land $ \\ 
 $ ( \Rnext BOX21P_{N0} \leftrightarrow ( \Rnext PinvNameF \land $ \\ 
 $ BOX21P_{N0})) \land $ \\ 
 $ ( \Rnext BOX12F_{N0} \leftrightarrow ( \Rnext E1NameF_{N0} \land $ \\ 
 $ BOX12F_{N0})) \land $ \\ 
 $ (BOX8F_{N0} \leftrightarrow  \Rbox NXT11F_{N0}) \land $ \\ 
 $ ( \Rnext BOX19P_{N0} \leftrightarrow ( \Rnext (E1NameInvP_{N0} \rightarrow BOX20P_{N0}) \land $ \\ 
 $ BOX19P_{N0}))) \land $ \\ 
 $ (E1NameF_{N0} \leftrightarrow E1NameP_{N0}) \land $ \\ 
 $ (BOX32F_{N0} \leftrightarrow BOX25P_{N0}) \land $ \\ 
 $ (E1NameInvF_{dNameInv} \leftrightarrow E1NameInvP_{dNameInv}) \land $ \\ 
 $ (BOX1F_{John} \leftrightarrow BOX34P_{John}) \land $ \\ 
 $ (BOX31F_{John} \leftrightarrow BOX24P_{John}) \land $ \\ 
 $ (BOX26F_{dName} \leftrightarrow BOX19P_{dName}) \land $ \\ 
 $ (E2NameF_{dNameInv} \leftrightarrow E2NameP_{dNameInv}) \land $ \\ 
 $ (BOX28F_{dNameInv} \leftrightarrow BOX21P_{dNameInv}) \land $ \\ 
 $ (BOX31F_{dNameInv} \leftrightarrow BOX24P_{dNameInv}) \land $ \\ 
 $ (PNameF \rightarrow E1NameInvF_{dNameInv}) \land $ \\ 
 $ (NXT7F_{dNameInv} \leftrightarrow NXT3P_{dNameInv}) \land $ \\ 
 $ (BOX32F_{dName} \leftrightarrow BOX25P_{dName}) \land $ \\ 
 $ (E1NameInvF_{John} \leftrightarrow E1NameInvP_{John}) \land $ \\ 
 $ (NXT9F_{John} \leftrightarrow NXT5P_{John}) \land $ \\ 
 $ (BOX29F_{John} \leftrightarrow BOX22P_{John}) \land $ \\ 
 $ (BOX2F_{dNameInv} \leftrightarrow BOX35P_{dNameInv}) \land $ \\ 
 $ (BOX27F_{dName} \leftrightarrow BOX20P_{dName}) \land $ \\ 
 $ (E1NameF_{dName} \leftrightarrow E1NameP_{dName}) \land $ \\ 
 $ (NXT11F_{John} \leftrightarrow NXT15P_{John}) \land $ \\ 
 $ (PinvNameF \leftrightarrow PinvNameP) \land $ \\ 
 $ (BOX30F_{dNameInv} \leftrightarrow BOX23P_{dNameInv}) \land $ \\ 
 $ (PNameF \rightarrow E1NameInvF_{dNameInv}) \land $ \\ 
 $ (BOX28F_{N0} \leftrightarrow BOX21P_{N0}) \land $ \\ 
 $ (PNameF \rightarrow E1NameInvF_{dNameInv}) \land $ \\ 
 $ (E1NameF_{dName} \leftrightarrow E1NameP_{dName}) \land $ \\ 
 $ (E1NameInvF_{dName} \leftrightarrow E1NameInvP_{dName}) \land $ \\ 
 $ (BOX26F_{N0} \leftrightarrow BOX19P_{N0}) \land $ \\ 
 $ (PersonF_{John} \leftrightarrow PersonP_{John}) \land $ \\ 
 $ (PNameF \leftrightarrow PNameF) \land $ \\ 
 $ (E1NameInvF_{dNameInv} \leftrightarrow E1NameInvP_{dNameInv}) \land $ \\ 
 $ (BOX14F_{dNameInv} \leftrightarrow BOX18P_{dNameInv}) \land $ \\ 
 $ (PNameF \leftrightarrow PNameP) \land $ \\ 
 $ (BOX32F_{John} \leftrightarrow BOX25P_{John}) \land $ \\ 
 $ (E1NameF_{dName} \leftrightarrow E1NameP_{dName}) \land $ \\ 
 $ (NXT13F_{dName} \leftrightarrow NXT17P_{dName}) \land $ \\ 
 $ (E2NameF_{N0} \leftrightarrow E2NameP_{N0}) \land $ \\ 
 $ (E1NameF_{John} \leftrightarrow E1NameP_{John}) \land $ \\ 
 $ (BOX14F_{dName} \leftrightarrow BOX18P_{dName}) \land $ \\ 
 $ (BOX2F_{John} \leftrightarrow BOX35P_{John}) \land $ \\ 
 $ (NXT9F_{dName} \leftrightarrow NXT5P_{dName}) \land $ \\ 
 $ (BOX8F_{dNameInv} \leftrightarrow BOX4P_{dNameInv}) \land $ \\ 
 $ (BOX1F_{N0} \leftrightarrow BOX34P_{N0}) \land $ \\ 
 $ (PNameF \leftrightarrow PNameF) \land $ \\ 
 $ (BOX27F_{dNameInv} \leftrightarrow BOX20P_{dNameInv}) \land $ \\ 
 $ (PinvNameF \rightarrow E1NameF_{dName}) \land $ \\ 
 $ (BOX28F_{dName} \leftrightarrow BOX21P_{dName}) \land $ \\ 
 $ (BOX31F_{dName} \leftrightarrow BOX24P_{dName}) \land $ \\ 
 $ (E1NameF_{dName} \leftrightarrow E1NameP_{dName}) \land $ \\ 
 $ (NXT7F_{dName} \leftrightarrow NXT3P_{dName}) \land $ \\ 
 $ (PNameF \leftrightarrow PNameF) \land $ \\ 
 $ (BOX29F_{dName} \leftrightarrow BOX22P_{dName}) \land $ \\ 
 $ (BOX10F_{dNameInv} \leftrightarrow BOX6P_{dNameInv}) \land $ \\ 
 $ (BOX32F_{dNameInv} \leftrightarrow BOX25P_{dNameInv}) \land $ \\ 
 $ (BOX8F_{dName} \leftrightarrow BOX4P_{dName}) \land $ \\ 
 $ (PinvNameF \leftrightarrow PinvNameP) \land $ \\ 
 $ (BOX28F_{John} \leftrightarrow BOX21P_{John}) \land $ \\ 
 $ (NXT9F_{dNameInv} \leftrightarrow NXT5P_{dNameInv}) \land $ \\ 
 $ (BOX26F_{dNameInv} \leftrightarrow BOX19P_{dNameInv}) \land $ \\ 
 $ (E1NameInvF_{dNameInv} \leftrightarrow E1NameInvP_{dNameInv}) \land $ \\ 
 $ (E2NameF_{dName} \leftrightarrow E2NameP_{dName}) \land $ \\ 
 $ (E2NameF_{John} \leftrightarrow E2NameP_{John}) \land $ \\ 
 $ (NXT13F_{dNameInv} \leftrightarrow NXT17P_{dNameInv}) \land $ \\ 
 $ (NXT13F_{N0} \leftrightarrow NXT17P_{N0}) \land $ \\ 
 $ (NXT11F_{dNameInv} \leftrightarrow NXT15P_{dNameInv}) \land $ \\ 
 $ (NXT13F_{John} \leftrightarrow NXT17P_{John}) \land $ \\ 
 $ (BOX0F_{dName} \leftrightarrow BOX33P_{dName}) \land $ \\ 
 $ (BOX29F_{N0} \leftrightarrow BOX22P_{N0}) \land $ \\ 
 $ (PNameF \leftrightarrow PNameP) \land $ \\ 
 $ (NXT11F_{N0} \leftrightarrow NXT15P_{N0}) \land $ \\ 
 $ (BOX10F_{dName} \leftrightarrow BOX6P_{dName}) \land $ \\ 
 $  \Rbox ((NXT17P_{John} \leftrightarrow  \Rnext BOX18P_{John}) \land $ \\ 
 $ ( \Rnext NXT13F_{John} \leftrightarrow BOX14F_{John}) \land $ \\ 
 $ (NXT7F_{John} \leftrightarrow  \Rnext BOX8F_{John}) \land $ \\ 
 $ (NXT9F_{John} \leftrightarrow  \Rnext BOX10F_{John}) \land $ \\ 
 $ ( \Rnext NXT11F_{John} \leftrightarrow BOX12F_{John}) \land $ \\ 
 $ ( \Rnext NXT5P_{John} \leftrightarrow BOX6P_{John}) \land $ \\ 
 $ (NXT15P_{John} \leftrightarrow  \Rnext BOX16P_{John}) \land $ \\ 
 $ ( \Rnext NXT3P_{John} \leftrightarrow BOX4P_{John}) \land $ \\ 
 $ (BOX18P_{John} \leftrightarrow  \Rbox E2NameP_{John}) \land $ \\ 
 $ ( \Rnext BOX14F_{John} \leftrightarrow ( \Rnext E2NameF_{John} \land $ \\ 
 $ BOX14F_{John})) \land $ \\ 
 $ ( \Rnext BOX0F_{John} \leftrightarrow ( \Rnext BOX26F_{John} \land $ \\ 
 $ BOX0F_{John})) \land $ \\ 
 $ (BOX20P_{John} \leftrightarrow  \Rbox BOX21P_{John}) \land $ \\ 
 $ (BOX10F_{John} \leftrightarrow  \Rbox NXT13F_{John}) \land $ \\ 
 $ ( \Rnext BOX1F_{John} \leftrightarrow ( \Rnext BOX29F_{John} \land $ \\ 
 $ BOX1F_{John})) \land $ \\ 
 $ (BOX16P_{John} \leftrightarrow  \Rbox E1NameP_{John}) \land $ \\ 
 $ (BOX32F_{John} \leftrightarrow  \Rbox ((PersonF_{John} \rightarrow E1NameF_{John}) \land $ \\ 
 $ (PersonF_{John} \rightarrow  \lnot E2NameF_{John}) \land $ \\ 
 $ (E2NameF_{John} \rightarrow E1NameF_{John}) \land $ \\ 
 $ (E1NameF_{John} \rightarrow NXT7F_{John}) \land $ \\ 
 $ (E2NameF_{John} \rightarrow NXT9F_{John}))) \land $ \\ 
 $ ( \Rnext BOX2F_{John} \leftrightarrow ( \Rnext BOX32F_{John} \land $ \\ 
 $ BOX2F_{John})) \land $ \\ 
 $ (BOX29F_{John} \leftrightarrow  \Rbox (E1NameF_{John} \rightarrow BOX30F_{John})) \land $ \\ 
 $ ( \Rnext BOX27F_{John} \leftrightarrow ( \Rnext BOX28F_{John} \land $ \\ 
 $ BOX27F_{John})) \land $ \\ 
 $ ( \Rnext BOX4P_{John} \leftrightarrow ( \Rnext NXT15P_{John} \land $ \\ 
 $ BOX4P_{John})) \land $ \\ 
 $ (BOX23P_{John} \leftrightarrow  \Rbox BOX24P_{John}) \land $ \\ 
 $ ( \Rnext BOX22P_{John} \leftrightarrow ( \Rnext (E1NameP_{John} \rightarrow BOX23P_{John}) \land $ \\ 
 $ BOX22P_{John})) \land $ \\ 
 $ (BOX34P_{John} \leftrightarrow  \Rbox BOX22P_{John}) \land $ \\ 
 $ ( \Rnext BOX6P_{John} \leftrightarrow ( \Rnext NXT17P_{John} \land $ \\ 
 $ BOX6P_{John})) \land $ \\ 
 $ (BOX31F_{John} \leftrightarrow  \Rbox PNameF) \land $ \\ 
 $ ( \Rnext BOX30F_{John} \leftrightarrow ( \Rnext BOX31F_{John} \land $ \\ 
 $ BOX30F_{John})) \land $ \\ 
 $ (BOX26F_{John} \leftrightarrow  \Rbox (E1NameInvF_{John} \rightarrow BOX27F_{John})) \land $ \\ 
 $ (BOX35P_{John} \leftrightarrow  \Rbox BOX25P_{John}) \land $ \\ 
 $ (BOX33P_{John} \leftrightarrow  \Rbox BOX19P_{John}) \land $ \\ 
 $ ( \Rnext BOX25P_{John} \leftrightarrow ( \Rnext ((PersonP_{John} \rightarrow E1NameP_{John}) \land $ \\ 
 $ (PersonP_{John} \rightarrow  \lnot E2NameP_{John}) \land $ \\ 
 $ (E2NameP_{John} \rightarrow E1NameP_{John}) \land $ \\ 
 $ (E1NameP_{John} \rightarrow NXT3P_{John}) \land $ \\ 
 $ (E2NameP_{John} \rightarrow NXT5P_{John})) \land $ \\ 
 $ BOX25P_{John})) \land $ \\ 
 $ ( \Rnext BOX24P_{John} \leftrightarrow ( \Rnext PNameF \land $ \\ 
 $ BOX24P_{John})) \land $ \\ 
 $ (BOX28F_{John} \leftrightarrow  \Rbox PinvNameF) \land $ \\ 
 $ ( \Rnext BOX21P_{John} \leftrightarrow ( \Rnext PinvNameF \land $ \\ 
 $ BOX21P_{John})) \land $ \\ 
 $ ( \Rnext BOX12F_{John} \leftrightarrow ( \Rnext E1NameF_{John} \land $ \\ 
 $ BOX12F_{John})) \land $ \\ 
 $ (BOX8F_{John} \leftrightarrow  \Rbox NXT11F_{John}) \land $ \\ 
 $ ( \Rnext BOX19P_{John} \leftrightarrow ( \Rnext (E1NameInvP_{John} \rightarrow BOX20P_{John}) \land $ \\ 
 $ BOX19P_{John}))) \land $ \\ 
 $ (PinvNameF \rightarrow E1NameF_{dName}) \land $ \\ 
 $ (PinvNameF \rightarrow E1NameF_{dName}) \land $ \\ 
 $ (BOX10F_{John} \leftrightarrow BOX6P_{John}) \land $ \\ 
 $ (E1NameInvF_{dNameInv} \leftrightarrow E1NameInvP_{dNameInv}) \land $ \\ 
 $ (BOX8F_{John} \leftrightarrow BOX4P_{John}) \land $ \\ 
 $ (PinvNameF \rightarrow E1NameF_{dName}) \land $ \\ 
 $ (PersonF_{N0} \leftrightarrow PersonP_{N0}) \land $ \\ 
 $ (PNameF \leftrightarrow PNameP) \land $ \\ 
 $ (BOX12F_{N0} \leftrightarrow BOX16P_{N0}) \land $ \\ 
 $ (BOX8F_{N0} \leftrightarrow BOX4P_{N0}) \land $ \\ 
 $ (PNameF \rightarrow E1NameInvF_{dNameInv}) \land $ \\ 
 $ (NXT7F_{N0} \leftrightarrow NXT3P_{N0}) \land $ \\ 
 $ (PinvNameF \leftrightarrow PinvNameF) \land $ \\ 
 $  \Rbox ((NXT17P_{dNameInv} \leftrightarrow  \Rnext BOX18P_{dNameInv}) \land $ \\ 
 $ ( \Rnext NXT13F_{dNameInv} \leftrightarrow BOX14F_{dNameInv}) \land $ \\ 
 $ (NXT7F_{dNameInv} \leftrightarrow  \Rnext BOX8F_{dNameInv}) \land $ \\ 
 $ (NXT9F_{dNameInv} \leftrightarrow  \Rnext BOX10F_{dNameInv}) \land $ \\ 
 $ ( \Rnext NXT11F_{dNameInv} \leftrightarrow BOX12F_{dNameInv}) \land $ \\ 
 $ ( \Rnext NXT5P_{dNameInv} \leftrightarrow BOX6P_{dNameInv}) \land $ \\ 
 $ (NXT15P_{dNameInv} \leftrightarrow  \Rnext BOX16P_{dNameInv}) \land $ \\ 
 $ ( \Rnext NXT3P_{dNameInv} \leftrightarrow BOX4P_{dNameInv}) \land $ \\ 
 $ (BOX18P_{dNameInv} \leftrightarrow  \Rbox E2NameP_{dNameInv}) \land $ \\ 
 $ ( \Rnext BOX14F_{dNameInv} \leftrightarrow ( \Rnext E2NameF_{dNameInv} \land $ \\ 
 $ BOX14F_{dNameInv})) \land $ \\ 
 $ ( \Rnext BOX0F_{dNameInv} \leftrightarrow ( \Rnext BOX26F_{dNameInv} \land $ \\ 
 $ BOX0F_{dNameInv})) \land $ \\ 
 $ (BOX20P_{dNameInv} \leftrightarrow  \Rbox BOX21P_{dNameInv}) \land $ \\ 
 $ (BOX10F_{dNameInv} \leftrightarrow  \Rbox NXT13F_{dNameInv}) \land $ \\ 
 $ ( \Rnext BOX1F_{dNameInv} \leftrightarrow ( \Rnext BOX29F_{dNameInv} \land $ \\ 
 $ BOX1F_{dNameInv})) \land $ \\ 
 $ (BOX16P_{dNameInv} \leftrightarrow  \Rbox E1NameP_{dNameInv}) \land $ \\ 
 $ (BOX32F_{dNameInv} \leftrightarrow  \Rbox ((PersonF_{dNameInv} \rightarrow E1NameF_{dNameInv}) \land $ \\ 
 $ (PersonF_{dNameInv} \rightarrow  \lnot E2NameF_{dNameInv}) \land $ \\ 
 $ (E2NameF_{dNameInv} \rightarrow E1NameF_{dNameInv}) \land $ \\ 
 $ (E1NameF_{dNameInv} \rightarrow NXT7F_{dNameInv}) \land $ \\ 
 $ (E2NameF_{dNameInv} \rightarrow NXT9F_{dNameInv}))) \land $ \\ 
 $ ( \Rnext BOX2F_{dNameInv} \leftrightarrow ( \Rnext BOX32F_{dNameInv} \land $ \\ 
 $ BOX2F_{dNameInv})) \land $ \\ 
 $ (BOX29F_{dNameInv} \leftrightarrow  \Rbox (E1NameF_{dNameInv} \rightarrow BOX30F_{dNameInv})) \land $ \\ 
 $ ( \Rnext BOX27F_{dNameInv} \leftrightarrow ( \Rnext BOX28F_{dNameInv} \land $ \\ 
 $ BOX27F_{dNameInv})) \land $ \\ 
 $ ( \Rnext BOX4P_{dNameInv} \leftrightarrow ( \Rnext NXT15P_{dNameInv} \land $ \\ 
 $ BOX4P_{dNameInv})) \land $ \\ 
 $ (BOX23P_{dNameInv} \leftrightarrow  \Rbox BOX24P_{dNameInv}) \land $ \\ 
 $ ( \Rnext BOX22P_{dNameInv} \leftrightarrow ( \Rnext (E1NameP_{dNameInv} \rightarrow BOX23P_{dNameInv}) \land $ \\ 
 $ BOX22P_{dNameInv})) \land $ \\ 
 $ (BOX34P_{dNameInv} \leftrightarrow  \Rbox BOX22P_{dNameInv}) \land $ \\ 
 $ ( \Rnext BOX6P_{dNameInv} \leftrightarrow ( \Rnext NXT17P_{dNameInv} \land $ \\ 
 $ BOX6P_{dNameInv})) \land $ \\ 
 $ (BOX31F_{dNameInv} \leftrightarrow  \Rbox PNameF) \land $ \\ 
 $ ( \Rnext BOX30F_{dNameInv} \leftrightarrow ( \Rnext BOX31F_{dNameInv} \land $ \\ 
 $ BOX30F_{dNameInv})) \land $ \\ 
 $ (BOX26F_{dNameInv} \leftrightarrow  \Rbox (E1NameInvF_{dNameInv} \rightarrow BOX27F_{dNameInv})) \land $ \\ 
 $ (BOX35P_{dNameInv} \leftrightarrow  \Rbox BOX25P_{dNameInv}) \land $ \\ 
 $ (BOX33P_{dNameInv} \leftrightarrow  \Rbox BOX19P_{dNameInv}) \land $ \\ 
 $ ( \Rnext BOX25P_{dNameInv} \leftrightarrow ( \Rnext ((PersonP_{dNameInv} \rightarrow E1NameP_{dNameInv}) \land $ \\ 
 $ (PersonP_{dNameInv} \rightarrow  \lnot E2NameP_{dNameInv}) \land $ \\ 
 $ (E2NameP_{dNameInv} \rightarrow E1NameP_{dNameInv}) \land $ \\ 
 $ (E1NameP_{dNameInv} \rightarrow NXT3P_{dNameInv}) \land $ \\ 
 $ (E2NameP_{dNameInv} \rightarrow NXT5P_{dNameInv})) \land $ \\ 
 $ BOX25P_{dNameInv})) \land $ \\ 
 $ ( \Rnext BOX24P_{dNameInv} \leftrightarrow ( \Rnext PNameF \land $ \\ 
 $ BOX24P_{dNameInv})) \land $ \\ 
 $ (BOX28F_{dNameInv} \leftrightarrow  \Rbox PinvNameF) \land $ \\ 
 $ ( \Rnext BOX21P_{dNameInv} \leftrightarrow ( \Rnext PinvNameF \land $ \\ 
 $ BOX21P_{dNameInv})) \land $ \\ 
 $ ( \Rnext BOX12F_{dNameInv} \leftrightarrow ( \Rnext E1NameF_{dNameInv} \land $ \\ 
 $ BOX12F_{dNameInv})) \land $ \\ 
 $ (BOX8F_{dNameInv} \leftrightarrow  \Rbox NXT11F_{dNameInv}) \land $ \\ 
 $ ( \Rnext BOX19P_{dNameInv} \leftrightarrow ( \Rnext (E1NameInvP_{dNameInv} \rightarrow BOX20P_{dNameInv}) \land $ \\ 
 $ BOX19P_{dNameInv}))) \land $ \\ 
 $ (BOX1F_{dName} \leftrightarrow BOX34P_{dName}) \land $ \\ 
 $ (NXT9F_{N0} \leftrightarrow NXT5P_{N0}) \land $ \\ 
 $ (BOX2F_{dName} \leftrightarrow BOX35P_{dName}) \land $ \\ 
 $ (PNameF \leftrightarrow PNameP) \land $ \\ 
 $ (BOX2F_{N0} \leftrightarrow BOX35P_{N0}) \land $ \\ 
 $ (PinvNameF \leftrightarrow PinvNameP) \land $ \\ 
 $  \Rbox ((NXT17P_{dName} \leftrightarrow  \Rnext BOX18P_{dName}) \land $ \\ 
 $ ( \Rnext NXT13F_{dName} \leftrightarrow BOX14F_{dName}) \land $ \\ 
 $ (NXT7F_{dName} \leftrightarrow  \Rnext BOX8F_{dName}) \land $ \\ 
 $ (NXT9F_{dName} \leftrightarrow  \Rnext BOX10F_{dName}) \land $ \\ 
 $ ( \Rnext NXT11F_{dName} \leftrightarrow BOX12F_{dName}) \land $ \\ 
 $ ( \Rnext NXT5P_{dName} \leftrightarrow BOX6P_{dName}) \land $ \\ 
 $ (NXT15P_{dName} \leftrightarrow  \Rnext BOX16P_{dName}) \land $ \\ 
 $ ( \Rnext NXT3P_{dName} \leftrightarrow BOX4P_{dName}) \land $ \\ 
 $ (BOX18P_{dName} \leftrightarrow  \Rbox E2NameP_{dName}) \land $ \\ 
 $ ( \Rnext BOX14F_{dName} \leftrightarrow ( \Rnext E2NameF_{dName} \land $ \\ 
 $ BOX14F_{dName})) \land $ \\ 
 $ ( \Rnext BOX0F_{dName} \leftrightarrow ( \Rnext BOX26F_{dName} \land $ \\ 
 $ BOX0F_{dName})) \land $ \\ 
 $ (BOX20P_{dName} \leftrightarrow  \Rbox BOX21P_{dName}) \land $ \\ 
 $ (BOX10F_{dName} \leftrightarrow  \Rbox NXT13F_{dName}) \land $ \\ 
 $ ( \Rnext BOX1F_{dName} \leftrightarrow ( \Rnext BOX29F_{dName} \land $ \\ 
 $ BOX1F_{dName})) \land $ \\ 
 $ (BOX16P_{dName} \leftrightarrow  \Rbox E1NameP_{dName}) \land $ \\ 
 $ (BOX32F_{dName} \leftrightarrow  \Rbox ((PersonF_{dName} \rightarrow E1NameF_{dName}) \land $ \\ 
 $ (PersonF_{dName} \rightarrow  \lnot E2NameF_{dName}) \land $ \\ 
 $ (E2NameF_{dName} \rightarrow E1NameF_{dName}) \land $ \\ 
 $ (E1NameF_{dName} \rightarrow NXT7F_{dName}) \land $ \\ 
 $ (E2NameF_{dName} \rightarrow NXT9F_{dName}))) \land $ \\ 
 $ ( \Rnext BOX2F_{dName} \leftrightarrow ( \Rnext BOX32F_{dName} \land $ \\ 
 $ BOX2F_{dName})) \land $ \\ 
 $ (BOX29F_{dName} \leftrightarrow  \Rbox (E1NameF_{dName} \rightarrow BOX30F_{dName})) \land $ \\ 
 $ ( \Rnext BOX27F_{dName} \leftrightarrow ( \Rnext BOX28F_{dName} \land $ \\ 
 $ BOX27F_{dName})) \land $ \\ 
 $ ( \Rnext BOX4P_{dName} \leftrightarrow ( \Rnext NXT15P_{dName} \land $ \\ 
 $ BOX4P_{dName})) \land $ \\ 
 $ (BOX23P_{dName} \leftrightarrow  \Rbox BOX24P_{dName}) \land $ \\ 
 $ ( \Rnext BOX22P_{dName} \leftrightarrow ( \Rnext (E1NameP_{dName} \rightarrow BOX23P_{dName}) \land $ \\ 
 $ BOX22P_{dName})) \land $ \\ 
 $ (BOX34P_{dName} \leftrightarrow  \Rbox BOX22P_{dName}) \land $ \\ 
 $ ( \Rnext BOX6P_{dName} \leftrightarrow ( \Rnext NXT17P_{dName} \land $ \\ 
 $ BOX6P_{dName})) \land $ \\ 
 $ (BOX31F_{dName} \leftrightarrow  \Rbox PNameF) \land $ \\ 
 $ ( \Rnext BOX30F_{dName} \leftrightarrow ( \Rnext BOX31F_{dName} \land $ \\ 
 $ BOX30F_{dName})) \land $ \\ 
 $ (BOX26F_{dName} \leftrightarrow  \Rbox (E1NameInvF_{dName} \rightarrow BOX27F_{dName})) \land $ \\ 
 $ (BOX35P_{dName} \leftrightarrow  \Rbox BOX25P_{dName}) \land $ \\ 
 $ (BOX33P_{dName} \leftrightarrow  \Rbox BOX19P_{dName}) \land $ \\ 
 $ ( \Rnext BOX25P_{dName} \leftrightarrow ( \Rnext ((PersonP_{dName} \rightarrow E1NameP_{dName}) \land $ \\ 
 $ (PersonP_{dName} \rightarrow  \lnot E2NameP_{dName}) \land $ \\ 
 $ (E2NameP_{dName} \rightarrow E1NameP_{dName}) \land $ \\ 
 $ (E1NameP_{dName} \rightarrow NXT3P_{dName}) \land $ \\ 
 $ (E2NameP_{dName} \rightarrow NXT5P_{dName})) \land $ \\ 
 $ BOX25P_{dName})) \land $ \\ 
 $ ( \Rnext BOX24P_{dName} \leftrightarrow ( \Rnext PNameF \land $ \\ 
 $ BOX24P_{dName})) \land $ \\ 
 $ (BOX28F_{dName} \leftrightarrow  \Rbox PinvNameF) \land $ \\ 
 $ ( \Rnext BOX21P_{dName} \leftrightarrow ( \Rnext PinvNameF \land $ \\ 
 $ BOX21P_{dName})) \land $ \\ 
 $ ( \Rnext BOX12F_{dName} \leftrightarrow ( \Rnext E1NameF_{dName} \land $ \\ 
 $ BOX12F_{dName})) \land $ \\ 
 $ (BOX8F_{dName} \leftrightarrow  \Rbox NXT11F_{dName}) \land $ \\ 
 $ ( \Rnext BOX19P_{dName} \leftrightarrow ( \Rnext (E1NameInvP_{dName} \rightarrow BOX20P_{dName}) \land $ \\ 
 $ BOX19P_{dName}))) \land $ \\ 
 $ (BOX31F_{N0} \leftrightarrow BOX24P_{N0}) \land $ \\ 
 $ (PinvNameF \leftrightarrow PinvNameP) \land $ \\ 
 $ (PinvNameF \leftrightarrow PinvNameF) \land $ \\ 
 $ (BOX0F_{John} \leftrightarrow BOX33P_{John}) \land $ \\ 
 $ (NXT7F_{John} \leftrightarrow NXT3P_{John}) \land $ \\ 
 $ (PersonF_{dNameInv} \leftrightarrow PersonP_{dNameInv}) \land $ \\ 
 $ (BOX0F_{N0} \leftrightarrow BOX33P_{N0}) \land $ \\ 
 $ (BOX12F_{dNameInv} \leftrightarrow BOX16P_{dNameInv}) \land $ \\ 
 $ (BOX27F_{John} \leftrightarrow BOX20P_{John}) \land $ \\ 
 $ (BOX26F_{John} \leftrightarrow BOX19P_{John}) \land $ \\ 
 $ (NXT11F_{dName} \leftrightarrow NXT15P_{dName}) \land $ \\ 
 $ (BOX12F_{John} \leftrightarrow BOX16P_{John}) \land $ \\ 
 $ BOX1F_{dNameInv} \land $ \\ 
 $ BOX1F_{N0} \land $ \\ 
 $ BOX1F_{John} \land $ \\ 
 $ BOX1F_{dName} \land $ \\ 
 $ BOX2F_{dNameInv} \land $ \\ 
 $ BOX2F_{N0} \land $ \\ 
 $ BOX2F_{John} \land $ \\ 
 $ BOX2F_{dName} \land $ \\ 
 $ BOX0F_{dNameInv} \land $ \\ 
 $ BOX0F_{N0} \land $ \\ 
 $ BOX0F_{John} \land $ \\ 
 $ BOX0F_{dName} \land $ \\ 
 $ E1NameF_{John} \land $ \\ 
 $ E1NameInvF_{N0} \land $ \\ 
 $ PersonF_{John})$ 
\end{document}