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


$((PNameF \rightarrow E1NameInvF(dNameInv)) \land $ \\ 
 $  \forall X. (BOX0F(X) \land $ \\ 
 $  \Rbox ((BOX10P(X) \leftrightarrow  \Rbox E2NameP(X)) \land $ \\ 
 $ ( \Rnext BOX21F(X) \leftrightarrow (BOX21F(X) \land $ \\ 
 $  \Rnext E2NameF(X))) \land $ \\ 
 $ ( \Rnext BOX19F(X) \leftrightarrow (BOX19F(X) \land $ \\ 
 $  \Rnext PNameF)) \land $ \\ 
 $ (BOX2P(X) \leftrightarrow  \Rbox ((PersonP(X) \rightarrow  \lnot E2NameP(X)) \land $ \\ 
 $ (PersonP(X) \rightarrow E1NameP(X)) \land $ \\ 
 $ (E2NameP(X) \rightarrow E1NameP(X)) \land $ \\ 
 $ (E1NameP(X) \rightarrow BOX3P(X)) \land $ \\ 
 $ (E1NameInvP(X) \rightarrow BOX5P(X)) \land $ \\ 
 $ (E1NameP(X) \rightarrow BOX7P(X)) \land $ \\ 
 $ (E2NameP(X) \rightarrow BOX9P(X)) \land $ \\ 
 $ (E1NameInvP(X) \rightarrow BOX11P(X)))) \land $ \\ 
 $ ( \Rnext BOX15F(X) \leftrightarrow (BOX15F(X) \land $ \\ 
 $  \Rnext E1NameF(X))) \land $ \\ 
 $ (BOX6P(X) \leftrightarrow  \Rbox E1NameInvP(X)) \land $ \\ 
 $ (BOX22F(X) \leftrightarrow  \Rbox BOX23F(X)) \land $ \\ 
 $ ( \Rnext BOX23F(X) \leftrightarrow (BOX23F(X) \land $ \\ 
 $  \Rnext PinvNameF)) \land $ \\ 
 $ (BOX14F(X) \leftrightarrow  \Rbox BOX15F(X)) \land $ \\ 
 $ ( \Rnext BOX9P(X) \leftrightarrow (BOX9P(X) \land $ \\ 
 $  \Rnext BOX10P(X))) \land $ \\ 
 $ ( \Rnext BOX3P(X) \leftrightarrow (BOX3P(X) \land $ \\ 
 $  \Rnext BOX4P(X))) \land $ \\ 
 $ (BOX16F(X) \leftrightarrow  \Rbox BOX17F(X)) \land $ \\ 
 $ ( \Rnext BOX13F(X) \leftrightarrow (BOX13F(X) \land $ \\ 
 $  \Rnext ((PersonF(X) \rightarrow  \lnot E2NameF(X)) \land $ \\ 
 $ (PersonF(X) \rightarrow E1NameF(X)) \land $ \\ 
 $ (E2NameF(X) \rightarrow E1NameF(X)) \land $ \\ 
 $ (E1NameF(X) \rightarrow BOX14F(X)) \land $ \\ 
 $ (E1NameInvF(X) \rightarrow BOX16F(X)) \land $ \\ 
 $ (E1NameF(X) \rightarrow BOX18F(X)) \land $ \\ 
 $ (E2NameF(X) \rightarrow BOX20F(X)) \land $ \\ 
 $ (E1NameInvF(X) \rightarrow BOX22F(X))))) \land $ \\ 
 $ (BOX4P(X) \leftrightarrow  \Rbox E1NameP(X)) \land $ \\ 
 $ (BOX18F(X) \leftrightarrow  \Rbox BOX19F(X)) \land $ \\ 
 $ (BOX12P(X) \leftrightarrow  \Rbox PinvNameP) \land $ \\ 
 $ (BOX0F(X) \leftrightarrow  \Rbox BOX13F(X)) \land $ \\ 
 $ ( \Rnext BOX11P(X) \leftrightarrow (BOX11P(X) \land $ \\ 
 $  \Rnext BOX12P(X))) \land $ \\ 
 $ (BOX20F(X) \leftrightarrow  \Rbox BOX21F(X)) \land $ \\ 
 $ ( \Rnext BOX7P(X) \leftrightarrow (BOX7P(X) \land $ \\ 
 $  \Rnext BOX8P(X))) \land $ \\ 
 $ (BOX8P(X) \leftrightarrow  \Rbox PNameP) \land $ \\ 
 $ ( \Rnext BOX17F(X) \leftrightarrow (BOX17F(X) \land $ \\ 
 $  \Rnext E1NameInvF(X))) \land $ \\ 
 $ ( \Rnext BOX5P(X) \leftrightarrow (BOX5P(X) \land $ \\ 
 $  \Rnext BOX6P(X))) \land $ \\ 
 $ ( \Rnext BOX1P(X) \leftrightarrow (BOX1P(X) \land $ \\ 
 $  \Rnext BOX2P(X)))) \land $ \\ 
 $ (BOX22F(X) \leftrightarrow BOX11P(X)) \land $ \\ 
 $ (E1NameF(X) \leftrightarrow E1NameP(X)) \land $ \\ 
 $ (BOX0F(X) \leftrightarrow BOX1P(X)) \land $ \\ 
 $ (BOX20F(X) \leftrightarrow BOX9P(X)) \land $ \\ 
 $ (E1NameInvF(X) \leftrightarrow E1NameInvP(X)) \land $ \\ 
 $ (BOX18F(X) \leftrightarrow BOX7P(X)) \land $ \\ 
 $ (PNameF \leftrightarrow PNameP) \land $ \\ 
 $ (BOX15F(X) \leftrightarrow BOX4P(X)) \land $ \\ 
 $ (BOX23F(X) \leftrightarrow BOX12P(X)) \land $ \\ 
 $ (BOX19F(X) \leftrightarrow BOX8P(X)) \land $ \\ 
 $ (BOX17F(X) \leftrightarrow BOX6P(X)) \land $ \\ 
 $ (BOX16F(X) \leftrightarrow BOX5P(X)) \land $ \\ 
 $ (PinvNameF \leftrightarrow PinvNameP) \land $ \\ 
 $ (E2NameF(X) \leftrightarrow E2NameP(X)) \land $ \\ 
 $ (BOX21F(X) \leftrightarrow BOX10P(X)) \land $ \\ 
 $ (BOX13F(X) \leftrightarrow BOX2P(X)) \land $ \\ 
 $ (PersonF(X) \leftrightarrow PersonP(X)) \land $ \\ 
 $ (BOX14F(X) \leftrightarrow BOX3P(X))) \land $ \\ 
 $ (PinvNameF \rightarrow E1NameF(dName)) \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 E1NameInvF(N0) \land $ \\ 
 $  \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 E1NameInvF(N0) \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 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 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 E1NameInvF(N0) \land $ \\ 
 $  \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 E1NameInvF(N0) \land $ \\ 
 $  \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 E1NameF(John) \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  \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 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 $ \\ 
 $ E1NameInvF(N0) \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 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 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 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  \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 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 E1NameInvF(N0) \land $ \\ 
 $  \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 E1NameInvF(N0) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameF(John) \land $ \\ 
 $  \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 E1NameF(John) \land $ \\ 
 $  \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  \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 E1NameF(John) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameInvF(N0) \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 E1NameInvF(N0) \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 E1NameF(John) \land $ \\ 
 $  \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  \Rnext  \Rnext E1NameF(John) \land $ \\ 
 $ PersonF(John) \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  \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  \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 E1NameF(John) \land $ \\ 
 $  \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 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 $ \\ 
 $ E1NameF(John) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1NameF(John))$ 
\end{document}