\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}}


$((BOX19F_{John} \leftrightarrow BOX8P_{John}) \land $ \\ 
 $ (E1NameF_{dNameInv} \leftrightarrow E1NameP_{dNameInv}) \land $ \\ 
 $ (BOX22F_{N0} \leftrightarrow BOX11P_{N0}) \land $ \\ 
 $ (BOX14F_{N0} \leftrightarrow BOX3P_{N0}) \land $ \\ 
 $ (BOX17F_{dName} \leftrightarrow BOX6P_{dName}) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $ (BOX14F_{dName} \leftrightarrow BOX3P_{dName}) \land $ \\ 
 $ (BOX13F_{dNameInv} \leftrightarrow BOX2P_{dNameInv}) \land $ \\ 
 $ (PersonF_{dNameInv} \leftrightarrow PersonP_{dNameInv}) \land $ \\ 
 $ (BOX14F_{dNameInv} \leftrightarrow BOX3P_{dNameInv}) \land $ \\ 
 $ (BOX21F_{N0} \leftrightarrow BOX10P_{N0}) \land $ \\ 
 $  \Rbox ((BOX4P_{dName} \leftrightarrow  \Rbox PNameP) \land $ \\ 
 $ ( \Rnext BOX13F_{dName} \leftrightarrow ( \Rnext ((PersonF_{dName} \rightarrow  \lnot E2NameF_{dName}) \land $ \\ 
 $ (PersonF_{dName} \rightarrow E1NameF_{dName}) \land $ \\ 
 $ (E1NameF_{dName} \rightarrow BOX14F_{dName}) \land $ \\ 
 $ (E1NameF_{dName} \rightarrow BOX16F_{dName}) \land $ \\ 
 $ (E1NameInvF_{dName} \rightarrow BOX18F_{dName}) \land $ \\ 
 $ (E2NameF_{dName} \rightarrow BOX20F_{dName}) \land $ \\ 
 $ (E2NameF_{dName} \rightarrow E1NameF_{dName}) \land $ \\ 
 $ (E1NameInvF_{dName} \rightarrow BOX22F_{dName})) \land $ \\ 
 $ BOX13F_{dName})) \land $ \\ 
 $ (BOX0F_{dName} \leftrightarrow  \Rbox BOX13F_{dName}) \land $ \\ 
 $ ( \Rnext BOX17F_{dName} \leftrightarrow ( \Rnext E1NameF_{dName} \land $ \\ 
 $ BOX17F_{dName})) \land $ \\ 
 $ ( \Rnext BOX11P_{dName} \leftrightarrow ( \Rnext BOX12P_{dName} \land $ \\ 
 $ BOX11P_{dName})) \land $ \\ 
 $ (BOX16F_{dName} \leftrightarrow  \Rbox BOX17F_{dName}) \land $ \\ 
 $ (BOX2P_{dName} \leftrightarrow  \Rbox ((PersonP_{dName} \rightarrow  \lnot E2NameP_{dName}) \land $ \\ 
 $ (PersonP_{dName} \rightarrow E1NameP_{dName}) \land $ \\ 
 $ (E1NameP_{dName} \rightarrow BOX3P_{dName}) \land $ \\ 
 $ (E1NameP_{dName} \rightarrow BOX5P_{dName}) \land $ \\ 
 $ (E1NameInvP_{dName} \rightarrow BOX7P_{dName}) \land $ \\ 
 $ (E2NameP_{dName} \rightarrow BOX9P_{dName}) \land $ \\ 
 $ (E2NameP_{dName} \rightarrow E1NameP_{dName}) \land $ \\ 
 $ (E1NameInvP_{dName} \rightarrow BOX11P_{dName}))) \land $ \\ 
 $ ( \Rnext BOX7P_{dName} \leftrightarrow ( \Rnext BOX8P_{dName} \land $ \\ 
 $ BOX7P_{dName})) \land $ \\ 
 $ (BOX20F_{dName} \leftrightarrow  \Rbox BOX21F_{dName}) \land $ \\ 
 $ ( \Rnext BOX3P_{dName} \leftrightarrow ( \Rnext BOX4P_{dName} \land $ \\ 
 $ BOX3P_{dName})) \land $ \\ 
 $ (BOX14F_{dName} \leftrightarrow  \Rbox BOX15F_{dName}) \land $ \\ 
 $ ( \Rnext BOX21F_{dName} \leftrightarrow ( \Rnext E2NameF_{dName} \land $ \\ 
 $ BOX21F_{dName})) \land $ \\ 
 $ ( \Rnext BOX19F_{dName} \leftrightarrow ( \Rnext PinvNameF \land $ \\ 
 $ BOX19F_{dName})) \land $ \\ 
 $ ( \Rnext BOX5P_{dName} \leftrightarrow ( \Rnext BOX6P_{dName} \land $ \\ 
 $ BOX5P_{dName})) \land $ \\ 
 $ (BOX18F_{dName} \leftrightarrow  \Rbox BOX19F_{dName}) \land $ \\ 
 $ ( \Rnext BOX23F_{dName} \leftrightarrow ( \Rnext E1NameInvF_{dName} \land $ \\ 
 $ BOX23F_{dName})) \land $ \\ 
 $ ( \Rnext BOX15F_{dName} \leftrightarrow ( \Rnext PNameF \land $ \\ 
 $ BOX15F_{dName})) \land $ \\ 
 $ (BOX8P_{dName} \leftrightarrow  \Rbox PinvNameP) \land $ \\ 
 $ (BOX10P_{dName} \leftrightarrow  \Rbox E2NameP_{dName}) \land $ \\ 
 $ ( \Rnext BOX1P_{dName} \leftrightarrow ( \Rnext BOX2P_{dName} \land $ \\ 
 $ BOX1P_{dName})) \land $ \\ 
 $ (BOX22F_{dName} \leftrightarrow  \Rbox BOX23F_{dName}) \land $ \\ 
 $ (BOX12P_{dName} \leftrightarrow  \Rbox E1NameInvP_{dName}) \land $ \\ 
 $ ( \Rnext BOX9P_{dName} \leftrightarrow ( \Rnext BOX10P_{dName} \land $ \\ 
 $ BOX9P_{dName})) \land $ \\ 
 $ (BOX6P_{dName} \leftrightarrow  \Rbox E1NameP_{dName})) \land $ \\ 
 $ (BOX16F_{John} \leftrightarrow BOX5P_{John}) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $ (BOX23F_{dNameInv} \leftrightarrow BOX12P_{dNameInv}) \land $ \\ 
 $ (BOX15F_{John} \leftrightarrow BOX4P_{John}) \land $ \\ 
 $ (E1NameF_{John} \leftrightarrow E1NameP_{John}) \land $ \\ 
 $ (BOX13F_{John} \leftrightarrow BOX2P_{John}) \land $ \\ 
 $ (BOX20F_{John} \leftrightarrow BOX9P_{John}) \land $ \\ 
 $ BOX0F_{dNameInv} \land $ \\ 
 $ (PNameF \leftrightarrow PNameP) \land $ \\ 
 $ (E1NameInvF_{John} \leftrightarrow E1NameInvP_{John}) \land $ \\ 
 $ (BOX13F_{N0} \leftrightarrow BOX2P_{N0}) \land $ \\ 
 $ (BOX17F_{dNameInv} \leftrightarrow BOX6P_{dNameInv}) \land $ \\ 
 $ (BOX15F_{dNameInv} \leftrightarrow BOX4P_{dNameInv}) \land $ \\ 
 $ (BOX14F_{John} \leftrightarrow BOX3P_{John}) \land $ \\ 
 $ (BOX0F_{dName} \leftrightarrow BOX1P_{dName}) \land $ \\ 
 $ (BOX21F_{dNameInv} \leftrightarrow BOX10P_{dNameInv}) \land $ \\ 
 $ (BOX18F_{dNameInv} \leftrightarrow BOX7P_{dNameInv}) \land $ \\ 
 $ (E1NameInvF_{dName} \leftrightarrow E1NameInvP_{dName}) \land $ \\ 
 $ (BOX15F_{N0} \leftrightarrow BOX4P_{N0}) \land $ \\ 
 $ (BOX23F_{N0} \leftrightarrow BOX12P_{N0}) \land $ \\ 
 $  \Rbox ((BOX4P_{N0} \leftrightarrow  \Rbox PNameP) \land $ \\ 
 $ ( \Rnext BOX13F_{N0} \leftrightarrow ( \Rnext ((PersonF_{N0} \rightarrow  \lnot E2NameF_{N0}) \land $ \\ 
 $ (PersonF_{N0} \rightarrow E1NameF_{N0}) \land $ \\ 
 $ (E1NameF_{N0} \rightarrow BOX14F_{N0}) \land $ \\ 
 $ (E1NameF_{N0} \rightarrow BOX16F_{N0}) \land $ \\ 
 $ (E1NameInvF_{N0} \rightarrow BOX18F_{N0}) \land $ \\ 
 $ (E2NameF_{N0} \rightarrow BOX20F_{N0}) \land $ \\ 
 $ (E2NameF_{N0} \rightarrow E1NameF_{N0}) \land $ \\ 
 $ (E1NameInvF_{N0} \rightarrow BOX22F_{N0})) \land $ \\ 
 $ BOX13F_{N0})) \land $ \\ 
 $ (BOX0F_{N0} \leftrightarrow  \Rbox BOX13F_{N0}) \land $ \\ 
 $ ( \Rnext BOX17F_{N0} \leftrightarrow ( \Rnext E1NameF_{N0} \land $ \\ 
 $ BOX17F_{N0})) \land $ \\ 
 $ ( \Rnext BOX11P_{N0} \leftrightarrow ( \Rnext BOX12P_{N0} \land $ \\ 
 $ BOX11P_{N0})) \land $ \\ 
 $ (BOX16F_{N0} \leftrightarrow  \Rbox BOX17F_{N0}) \land $ \\ 
 $ (BOX2P_{N0} \leftrightarrow  \Rbox ((PersonP_{N0} \rightarrow  \lnot E2NameP_{N0}) \land $ \\ 
 $ (PersonP_{N0} \rightarrow E1NameP_{N0}) \land $ \\ 
 $ (E1NameP_{N0} \rightarrow BOX3P_{N0}) \land $ \\ 
 $ (E1NameP_{N0} \rightarrow BOX5P_{N0}) \land $ \\ 
 $ (E1NameInvP_{N0} \rightarrow BOX7P_{N0}) \land $ \\ 
 $ (E2NameP_{N0} \rightarrow BOX9P_{N0}) \land $ \\ 
 $ (E2NameP_{N0} \rightarrow E1NameP_{N0}) \land $ \\ 
 $ (E1NameInvP_{N0} \rightarrow BOX11P_{N0}))) \land $ \\ 
 $ ( \Rnext BOX7P_{N0} \leftrightarrow ( \Rnext BOX8P_{N0} \land $ \\ 
 $ BOX7P_{N0})) \land $ \\ 
 $ (BOX20F_{N0} \leftrightarrow  \Rbox BOX21F_{N0}) \land $ \\ 
 $ ( \Rnext BOX3P_{N0} \leftrightarrow ( \Rnext BOX4P_{N0} \land $ \\ 
 $ BOX3P_{N0})) \land $ \\ 
 $ (BOX14F_{N0} \leftrightarrow  \Rbox BOX15F_{N0}) \land $ \\ 
 $ ( \Rnext BOX21F_{N0} \leftrightarrow ( \Rnext E2NameF_{N0} \land $ \\ 
 $ BOX21F_{N0})) \land $ \\ 
 $ ( \Rnext BOX19F_{N0} \leftrightarrow ( \Rnext PinvNameF \land $ \\ 
 $ BOX19F_{N0})) \land $ \\ 
 $ ( \Rnext BOX5P_{N0} \leftrightarrow ( \Rnext BOX6P_{N0} \land $ \\ 
 $ BOX5P_{N0})) \land $ \\ 
 $ (BOX18F_{N0} \leftrightarrow  \Rbox BOX19F_{N0}) \land $ \\ 
 $ ( \Rnext BOX23F_{N0} \leftrightarrow ( \Rnext E1NameInvF_{N0} \land $ \\ 
 $ BOX23F_{N0})) \land $ \\ 
 $ ( \Rnext BOX15F_{N0} \leftrightarrow ( \Rnext PNameF \land $ \\ 
 $ BOX15F_{N0})) \land $ \\ 
 $ (BOX8P_{N0} \leftrightarrow  \Rbox PinvNameP) \land $ \\ 
 $ (BOX10P_{N0} \leftrightarrow  \Rbox E2NameP_{N0}) \land $ \\ 
 $ ( \Rnext BOX1P_{N0} \leftrightarrow ( \Rnext BOX2P_{N0} \land $ \\ 
 $ BOX1P_{N0})) \land $ \\ 
 $ (BOX22F_{N0} \leftrightarrow  \Rbox BOX23F_{N0}) \land $ \\ 
 $ (BOX12P_{N0} \leftrightarrow  \Rbox E1NameInvP_{N0}) \land $ \\ 
 $ ( \Rnext BOX9P_{N0} \leftrightarrow ( \Rnext BOX10P_{N0} \land $ \\ 
 $ BOX9P_{N0})) \land $ \\ 
 $ (BOX6P_{N0} \leftrightarrow  \Rbox E1NameP_{N0})) \land $ \\ 
 $ (PinvNameF \leftrightarrow PinvNameP) \land $ \\ 
 $ (PNameF \leftrightarrow PNameP) \land $ \\ 
 $ (BOX15F_{dName} \leftrightarrow BOX4P_{dName}) \land $ \\ 
 $ BOX0F_{John} \land $ \\ 
 $ BOX0F_{dName} \land $ \\ 
 $ (BOX18F_{dName} \leftrightarrow BOX7P_{dName}) \land $ \\ 
 $ (BOX20F_{N0} \leftrightarrow BOX9P_{N0}) \land $ \\ 
 $ (BOX18F_{John} \leftrightarrow BOX7P_{John}) \land $ \\ 
 $ BOX0F_{N0} \land $ \\ 
 $ (PNameF \leftrightarrow PNameP) \land $ \\ 
 $ (PNameF \leftrightarrow PNameP) \land $ \\ 
 $  \Rbox ((BOX4P_{John} \leftrightarrow  \Rbox PNameP) \land $ \\ 
 $ ( \Rnext BOX13F_{John} \leftrightarrow ( \Rnext ((PersonF_{John} \rightarrow  \lnot E2NameF_{John}) \land $ \\ 
 $ (PersonF_{John} \rightarrow E1NameF_{John}) \land $ \\ 
 $ (E1NameF_{John} \rightarrow BOX14F_{John}) \land $ \\ 
 $ (E1NameF_{John} \rightarrow BOX16F_{John}) \land $ \\ 
 $ (E1NameInvF_{John} \rightarrow BOX18F_{John}) \land $ \\ 
 $ (E2NameF_{John} \rightarrow BOX20F_{John}) \land $ \\ 
 $ (E2NameF_{John} \rightarrow E1NameF_{John}) \land $ \\ 
 $ (E1NameInvF_{John} \rightarrow BOX22F_{John})) \land $ \\ 
 $ BOX13F_{John})) \land $ \\ 
 $ (BOX0F_{John} \leftrightarrow  \Rbox BOX13F_{John}) \land $ \\ 
 $ ( \Rnext BOX17F_{John} \leftrightarrow ( \Rnext E1NameF_{John} \land $ \\ 
 $ BOX17F_{John})) \land $ \\ 
 $ ( \Rnext BOX11P_{John} \leftrightarrow ( \Rnext BOX12P_{John} \land $ \\ 
 $ BOX11P_{John})) \land $ \\ 
 $ (BOX16F_{John} \leftrightarrow  \Rbox BOX17F_{John}) \land $ \\ 
 $ (BOX2P_{John} \leftrightarrow  \Rbox ((PersonP_{John} \rightarrow  \lnot E2NameP_{John}) \land $ \\ 
 $ (PersonP_{John} \rightarrow E1NameP_{John}) \land $ \\ 
 $ (E1NameP_{John} \rightarrow BOX3P_{John}) \land $ \\ 
 $ (E1NameP_{John} \rightarrow BOX5P_{John}) \land $ \\ 
 $ (E1NameInvP_{John} \rightarrow BOX7P_{John}) \land $ \\ 
 $ (E2NameP_{John} \rightarrow BOX9P_{John}) \land $ \\ 
 $ (E2NameP_{John} \rightarrow E1NameP_{John}) \land $ \\ 
 $ (E1NameInvP_{John} \rightarrow BOX11P_{John}))) \land $ \\ 
 $ ( \Rnext BOX7P_{John} \leftrightarrow ( \Rnext BOX8P_{John} \land $ \\ 
 $ BOX7P_{John})) \land $ \\ 
 $ (BOX20F_{John} \leftrightarrow  \Rbox BOX21F_{John}) \land $ \\ 
 $ ( \Rnext BOX3P_{John} \leftrightarrow ( \Rnext BOX4P_{John} \land $ \\ 
 $ BOX3P_{John})) \land $ \\ 
 $ (BOX14F_{John} \leftrightarrow  \Rbox BOX15F_{John}) \land $ \\ 
 $ ( \Rnext BOX21F_{John} \leftrightarrow ( \Rnext E2NameF_{John} \land $ \\ 
 $ BOX21F_{John})) \land $ \\ 
 $ ( \Rnext BOX19F_{John} \leftrightarrow ( \Rnext PinvNameF \land $ \\ 
 $ BOX19F_{John})) \land $ \\ 
 $ ( \Rnext BOX5P_{John} \leftrightarrow ( \Rnext BOX6P_{John} \land $ \\ 
 $ BOX5P_{John})) \land $ \\ 
 $ (BOX18F_{John} \leftrightarrow  \Rbox BOX19F_{John}) \land $ \\ 
 $ ( \Rnext BOX23F_{John} \leftrightarrow ( \Rnext E1NameInvF_{John} \land $ \\ 
 $ BOX23F_{John})) \land $ \\ 
 $ ( \Rnext BOX15F_{John} \leftrightarrow ( \Rnext PNameF \land $ \\ 
 $ BOX15F_{John})) \land $ \\ 
 $ (BOX8P_{John} \leftrightarrow  \Rbox PinvNameP) \land $ \\ 
 $ (BOX10P_{John} \leftrightarrow  \Rbox E2NameP_{John}) \land $ \\ 
 $ ( \Rnext BOX1P_{John} \leftrightarrow ( \Rnext BOX2P_{John} \land $ \\ 
 $ BOX1P_{John})) \land $ \\ 
 $ (BOX22F_{John} \leftrightarrow  \Rbox BOX23F_{John}) \land $ \\ 
 $ (BOX12P_{John} \leftrightarrow  \Rbox E1NameInvP_{John}) \land $ \\ 
 $ ( \Rnext BOX9P_{John} \leftrightarrow ( \Rnext BOX10P_{John} \land $ \\ 
 $ BOX9P_{John})) \land $ \\ 
 $ (BOX6P_{John} \leftrightarrow  \Rbox E1NameP_{John})) \land $ \\ 
 $ (PinvNameF \leftrightarrow PinvNameP) \land $ \\ 
 $ (BOX16F_{dNameInv} \leftrightarrow BOX5P_{dNameInv}) \land $ \\ 
 $ (BOX23F_{John} \leftrightarrow BOX12P_{John}) \land $ \\ 
 $ (E2NameF_{John} \leftrightarrow E2NameP_{John}) \land $ \\ 
 $ (PersonF_{John} \leftrightarrow PersonP_{John}) \land $ \\ 
 $ (BOX19F_{N0} \leftrightarrow BOX8P_{N0}) \land $ \\ 
 $ (BOX22F_{John} \leftrightarrow BOX11P_{John}) \land $ \\ 
 $ (BOX19F_{dNameInv} \leftrightarrow BOX8P_{dNameInv}) \land $ \\ 
 $ (E1NameInvF_{dNameInv} \leftrightarrow E1NameInvP_{dNameInv}) \land $ \\ 
 $ (BOX17F_{John} \leftrightarrow BOX6P_{John}) \land $ \\ 
 $ (BOX18F_{N0} \leftrightarrow BOX7P_{N0}) \land $ \\ 
 $ (E2NameF_{N0} \leftrightarrow E2NameP_{N0}) \land $ \\ 
 $ (BOX16F_{N0} \leftrightarrow BOX5P_{N0}) \land $ \\ 
 $ (BOX20F_{dName} \leftrightarrow BOX9P_{dName}) \land $ \\ 
 $ (BOX23F_{dName} \leftrightarrow BOX12P_{dName}) \land $ \\ 
 $ (BOX21F_{dName} \leftrightarrow BOX10P_{dName}) \land $ \\ 
 $ (BOX21F_{John} \leftrightarrow BOX10P_{John}) \land $ \\ 
 $ (BOX13F_{dName} \leftrightarrow BOX2P_{dName}) \land $ \\ 
 $ (E2NameF_{dName} \leftrightarrow E2NameP_{dName}) \land $ \\ 
 $ (BOX22F_{dName} \leftrightarrow BOX11P_{dName}) \land $ \\ 
 $ (E1NameF_{dName} \leftrightarrow E1NameP_{dName}) \land $ \\ 
 $ (PinvNameF \leftrightarrow PinvNameP) \land $ \\ 
 $ (E1NameInvF_{N0} \leftrightarrow E1NameInvP_{N0}) \land $ \\ 
 $ (E1NameF_{N0} \leftrightarrow E1NameP_{N0}) \land $ \\ 
 $ (BOX19F_{dName} \leftrightarrow BOX8P_{dName}) \land $ \\ 
 $ (PersonF_{dName} \leftrightarrow PersonP_{dName}) \land $ \\ 
 $ (E2NameF_{dNameInv} \leftrightarrow E2NameP_{dNameInv}) \land $ \\ 
 $ (BOX0F_{dNameInv} \leftrightarrow BOX1P_{dNameInv}) \land $ \\ 
 $ (BOX16F_{dName} \leftrightarrow BOX5P_{dName}) \land $ \\ 
 $ (BOX0F_{N0} \leftrightarrow BOX1P_{N0}) \land $ \\ 
 $ (BOX22F_{dNameInv} \leftrightarrow BOX11P_{dNameInv}) \land $ \\ 
 $ (PinvNameF \leftrightarrow PinvNameP) \land $ \\ 
 $  \Rbox ((BOX4P_{dNameInv} \leftrightarrow  \Rbox PNameP) \land $ \\ 
 $ ( \Rnext BOX13F_{dNameInv} \leftrightarrow ( \Rnext ((PersonF_{dNameInv} \rightarrow  \lnot E2NameF_{dNameInv}) \land $ \\ 
 $ (PersonF_{dNameInv} \rightarrow E1NameF_{dNameInv}) \land $ \\ 
 $ (E1NameF_{dNameInv} \rightarrow BOX14F_{dNameInv}) \land $ \\ 
 $ (E1NameF_{dNameInv} \rightarrow BOX16F_{dNameInv}) \land $ \\ 
 $ (E1NameInvF_{dNameInv} \rightarrow BOX18F_{dNameInv}) \land $ \\ 
 $ (E2NameF_{dNameInv} \rightarrow BOX20F_{dNameInv}) \land $ \\ 
 $ (E2NameF_{dNameInv} \rightarrow E1NameF_{dNameInv}) \land $ \\ 
 $ (E1NameInvF_{dNameInv} \rightarrow BOX22F_{dNameInv})) \land $ \\ 
 $ BOX13F_{dNameInv})) \land $ \\ 
 $ (BOX0F_{dNameInv} \leftrightarrow  \Rbox BOX13F_{dNameInv}) \land $ \\ 
 $ ( \Rnext BOX17F_{dNameInv} \leftrightarrow ( \Rnext E1NameF_{dNameInv} \land $ \\ 
 $ BOX17F_{dNameInv})) \land $ \\ 
 $ ( \Rnext BOX11P_{dNameInv} \leftrightarrow ( \Rnext BOX12P_{dNameInv} \land $ \\ 
 $ BOX11P_{dNameInv})) \land $ \\ 
 $ (BOX16F_{dNameInv} \leftrightarrow  \Rbox BOX17F_{dNameInv}) \land $ \\ 
 $ (BOX2P_{dNameInv} \leftrightarrow  \Rbox ((PersonP_{dNameInv} \rightarrow  \lnot E2NameP_{dNameInv}) \land $ \\ 
 $ (PersonP_{dNameInv} \rightarrow E1NameP_{dNameInv}) \land $ \\ 
 $ (E1NameP_{dNameInv} \rightarrow BOX3P_{dNameInv}) \land $ \\ 
 $ (E1NameP_{dNameInv} \rightarrow BOX5P_{dNameInv}) \land $ \\ 
 $ (E1NameInvP_{dNameInv} \rightarrow BOX7P_{dNameInv}) \land $ \\ 
 $ (E2NameP_{dNameInv} \rightarrow BOX9P_{dNameInv}) \land $ \\ 
 $ (E2NameP_{dNameInv} \rightarrow E1NameP_{dNameInv}) \land $ \\ 
 $ (E1NameInvP_{dNameInv} \rightarrow BOX11P_{dNameInv}))) \land $ \\ 
 $ ( \Rnext BOX7P_{dNameInv} \leftrightarrow ( \Rnext BOX8P_{dNameInv} \land $ \\ 
 $ BOX7P_{dNameInv})) \land $ \\ 
 $ (BOX20F_{dNameInv} \leftrightarrow  \Rbox BOX21F_{dNameInv}) \land $ \\ 
 $ ( \Rnext BOX3P_{dNameInv} \leftrightarrow ( \Rnext BOX4P_{dNameInv} \land $ \\ 
 $ BOX3P_{dNameInv})) \land $ \\ 
 $ (BOX14F_{dNameInv} \leftrightarrow  \Rbox BOX15F_{dNameInv}) \land $ \\ 
 $ ( \Rnext BOX21F_{dNameInv} \leftrightarrow ( \Rnext E2NameF_{dNameInv} \land $ \\ 
 $ BOX21F_{dNameInv})) \land $ \\ 
 $ ( \Rnext BOX19F_{dNameInv} \leftrightarrow ( \Rnext PinvNameF \land $ \\ 
 $ BOX19F_{dNameInv})) \land $ \\ 
 $ ( \Rnext BOX5P_{dNameInv} \leftrightarrow ( \Rnext BOX6P_{dNameInv} \land $ \\ 
 $ BOX5P_{dNameInv})) \land $ \\ 
 $ (BOX18F_{dNameInv} \leftrightarrow  \Rbox BOX19F_{dNameInv}) \land $ \\ 
 $ ( \Rnext BOX23F_{dNameInv} \leftrightarrow ( \Rnext E1NameInvF_{dNameInv} \land $ \\ 
 $ BOX23F_{dNameInv})) \land $ \\ 
 $ ( \Rnext BOX15F_{dNameInv} \leftrightarrow ( \Rnext PNameF \land $ \\ 
 $ BOX15F_{dNameInv})) \land $ \\ 
 $ (BOX8P_{dNameInv} \leftrightarrow  \Rbox PinvNameP) \land $ \\ 
 $ (BOX10P_{dNameInv} \leftrightarrow  \Rbox E2NameP_{dNameInv}) \land $ \\ 
 $ ( \Rnext BOX1P_{dNameInv} \leftrightarrow ( \Rnext BOX2P_{dNameInv} \land $ \\ 
 $ BOX1P_{dNameInv})) \land $ \\ 
 $ (BOX22F_{dNameInv} \leftrightarrow  \Rbox BOX23F_{dNameInv}) \land $ \\ 
 $ (BOX12P_{dNameInv} \leftrightarrow  \Rbox E1NameInvP_{dNameInv}) \land $ \\ 
 $ ( \Rnext BOX9P_{dNameInv} \leftrightarrow ( \Rnext BOX10P_{dNameInv} \land $ \\ 
 $ BOX9P_{dNameInv})) \land $ \\ 
 $ (BOX6P_{dNameInv} \leftrightarrow  \Rbox E1NameP_{dNameInv})) \land $ \\ 
 $ (BOX20F_{dNameInv} \leftrightarrow BOX9P_{dNameInv}) \land $ \\ 
 $ (BOX17F_{N0} \leftrightarrow BOX6P_{N0}) \land $ \\ 
 $ (PersonF_{N0} \leftrightarrow PersonP_{N0}) \land $ \\ 
 $ (BOX0F_{John} \leftrightarrow BOX1P_{John}) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E1NameInvF_{N0} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameInvF_{N0} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameInvF_{N0} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameInvF_{N0} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameInvF_{N0} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E1NameF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameInvF_{N0} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameInvF_{N0} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameInvF_{N0} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameInvF_{N0} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameInvF_{N0} \land $ \\ 
 $  \Rnext  \Rnext E1NameF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameInvF_{N0} \land $ \\ 
 $ E1NameInvF_{N0} \land $ \\ 
 $  \Rnext E1NameF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameInvF_{N0} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameInvF_{N0} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameInvF_{N0} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameInvF_{N0} \land $ \\ 
 $  \Rnext E1NameInvF_{N0} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameInvF_{N0} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameInvF_{N0} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameInvF_{N0} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameInvF_{N0} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E1NameF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameInvF_{N0} \land $ \\ 
 $  \Rnext  \Rnext E1NameInvF_{N0} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameInvF_{N0} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameInvF_{N0} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameInvF_{N0} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameInvF_{N0} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameInvF_{N0} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E1NameInvF_{N0} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameF_{John} \land $ \\ 
 $ PersonF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameInvF_{N0} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameInvF_{N0} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameInvF_{N0} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameInvF_{N0} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameInvF_{N0} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameF_{John} \land $ \\ 
 $ E1NameF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameInvF_{N0} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameInvF_{N0} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameInvF_{N0} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameInvF_{N0} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameInvF_{N0} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameInvF_{N0} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameF_{John})$ 
\end{document}