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


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