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


$( \forall X. ((PNameF \rightarrow E1NameInvF(dNameInv)) \land $ \\ 
 $ BOX2F(X) \land $ \\ 
 $ BOX0F(X) \land $ \\ 
 $ BOX1F(X) \land $ \\ 
 $ (PinvNameF \rightarrow E1NameF(dName)) \land $ \\ 
 $  \Rbox (( \Rnext NXT11F(X) \leftrightarrow BOX12F(X)) \land $ \\ 
 $ (NXT17P(X) \leftrightarrow  \Rnext BOX18P(X)) \land $ \\ 
 $ (NXT9F(X) \leftrightarrow  \Rnext BOX10F(X)) \land $ \\ 
 $ ( \Rnext NXT13F(X) \leftrightarrow BOX14F(X)) \land $ \\ 
 $ (NXT15P(X) \leftrightarrow  \Rnext BOX16P(X)) \land $ \\ 
 $ (NXT7F(X) \leftrightarrow  \Rnext BOX8F(X)) \land $ \\ 
 $ ( \Rnext NXT5P(X) \leftrightarrow BOX6P(X)) \land $ \\ 
 $ ( \Rnext NXT3P(X) \leftrightarrow BOX4P(X)) \land $ \\ 
 $ ( \Rnext BOX30F(X) \leftrightarrow (BOX30F(X) \land $ \\ 
 $  \Rnext BOX31F(X))) \land $ \\ 
 $ (BOX31F(X) \leftrightarrow  \Rbox PNameF) \land $ \\ 
 $ ( \Rnext BOX25P(X) \leftrightarrow (BOX25P(X) \land $ \\ 
 $  \Rnext ((PersonP(X) \rightarrow E1NameP(X)) \land $ \\ 
 $ (PersonP(X) \rightarrow  \lnot E2NameP(X)) \land $ \\ 
 $ (E2NameP(X) \rightarrow E1NameP(X)) \land $ \\ 
 $ (E1NameP(X) \rightarrow NXT3P(X)) \land $ \\ 
 $ (E2NameP(X) \rightarrow NXT5P(X))))) \land $ \\ 
 $ (BOX8F(X) \leftrightarrow  \Rbox NXT11F(X)) \land $ \\ 
 $ ( \Rnext BOX24P(X) \leftrightarrow (BOX24P(X) \land $ \\ 
 $  \Rnext PNameF)) \land $ \\ 
 $ ( \Rnext BOX6P(X) \leftrightarrow (BOX6P(X) \land $ \\ 
 $  \Rnext NXT17P(X))) \land $ \\ 
 $ ( \Rnext BOX1F(X) \leftrightarrow (BOX1F(X) \land $ \\ 
 $  \Rnext BOX29F(X))) \land $ \\ 
 $ (BOX23P(X) \leftrightarrow  \Rbox BOX24P(X)) \land $ \\ 
 $ ( \Rnext BOX21P(X) \leftrightarrow (BOX21P(X) \land $ \\ 
 $  \Rnext PinvNameF)) \land $ \\ 
 $ (BOX28F(X) \leftrightarrow  \Rbox PinvNameF) \land $ \\ 
 $ (BOX20P(X) \leftrightarrow  \Rbox BOX21P(X)) \land $ \\ 
 $ ( \Rnext BOX4P(X) \leftrightarrow (BOX4P(X) \land $ \\ 
 $  \Rnext NXT15P(X))) \land $ \\ 
 $ ( \Rnext BOX0F(X) \leftrightarrow (BOX0F(X) \land $ \\ 
 $  \Rnext BOX26F(X))) \land $ \\ 
 $ (BOX35P(X) \leftrightarrow  \Rbox BOX25P(X)) \land $ \\ 
 $ (BOX16P(X) \leftrightarrow  \Rbox E1NameP(X)) \land $ \\ 
 $ (BOX10F(X) \leftrightarrow  \Rbox NXT13F(X)) \land $ \\ 
 $ ( \Rnext BOX19P(X) \leftrightarrow (BOX19P(X) \land $ \\ 
 $  \Rnext (E1NameInvP(X) \rightarrow BOX20P(X)))) \land $ \\ 
 $ (BOX26F(X) \leftrightarrow  \Rbox (E1NameInvF(X) \rightarrow BOX27F(X))) \land $ \\ 
 $ ( \Rnext BOX27F(X) \leftrightarrow (BOX27F(X) \land $ \\ 
 $  \Rnext BOX28F(X))) \land $ \\ 
 $ (BOX32F(X) \leftrightarrow  \Rbox ((PersonF(X) \rightarrow E1NameF(X)) \land $ \\ 
 $ (PersonF(X) \rightarrow  \lnot E2NameF(X)) \land $ \\ 
 $ (E2NameF(X) \rightarrow E1NameF(X)) \land $ \\ 
 $ (E1NameF(X) \rightarrow NXT7F(X)) \land $ \\ 
 $ (E2NameF(X) \rightarrow NXT9F(X)))) \land $ \\ 
 $ ( \Rnext BOX12F(X) \leftrightarrow (BOX12F(X) \land $ \\ 
 $  \Rnext E1NameF(X))) \land $ \\ 
 $ (BOX34P(X) \leftrightarrow  \Rbox BOX22P(X)) \land $ \\ 
 $ ( \Rnext BOX14F(X) \leftrightarrow (BOX14F(X) \land $ \\ 
 $  \Rnext E2NameF(X))) \land $ \\ 
 $ (BOX29F(X) \leftrightarrow  \Rbox (E1NameF(X) \rightarrow BOX30F(X))) \land $ \\ 
 $ (BOX18P(X) \leftrightarrow  \Rbox E2NameP(X)) \land $ \\ 
 $ (BOX33P(X) \leftrightarrow  \Rbox BOX19P(X)) \land $ \\ 
 $ ( \Rnext BOX22P(X) \leftrightarrow (BOX22P(X) \land $ \\ 
 $  \Rnext (E1NameP(X) \rightarrow BOX23P(X)))) \land $ \\ 
 $ ( \Rnext BOX2F(X) \leftrightarrow (BOX2F(X) \land $ \\ 
 $  \Rnext BOX32F(X)))) \land $ \\ 
 $ (PersonF(X) \leftrightarrow PersonP(X)) \land $ \\ 
 $ (NXT11F(X) \leftrightarrow NXT15P(X)) \land $ \\ 
 $ (BOX31F(X) \leftrightarrow BOX24P(X)) \land $ \\ 
 $ (BOX8F(X) \leftrightarrow BOX4P(X)) \land $ \\ 
 $ (PinvNameF \leftrightarrow PinvNameF) \land $ \\ 
 $ (PinvNameF \leftrightarrow PinvNameP) \land $ \\ 
 $ (PNameF \leftrightarrow PNameF) \land $ \\ 
 $ (NXT7F(X) \leftrightarrow NXT3P(X)) \land $ \\ 
 $ (BOX28F(X) \leftrightarrow BOX21P(X)) \land $ \\ 
 $ (BOX27F(X) \leftrightarrow BOX20P(X)) \land $ \\ 
 $ (E1NameInvF(X) \leftrightarrow E1NameInvP(X)) \land $ \\ 
 $ (E2NameF(X) \leftrightarrow E2NameP(X)) \land $ \\ 
 $ (BOX2F(X) \leftrightarrow BOX35P(X)) \land $ \\ 
 $ (PNameF \leftrightarrow PNameP) \land $ \\ 
 $ (BOX26F(X) \leftrightarrow BOX19P(X)) \land $ \\ 
 $ (E1NameF(dName) \leftrightarrow E1NameP(dName)) \land $ \\ 
 $ (BOX29F(X) \leftrightarrow BOX22P(X)) \land $ \\ 
 $ (NXT13F(X) \leftrightarrow NXT17P(X)) \land $ \\ 
 $ (E1NameF(X) \leftrightarrow E1NameP(X)) \land $ \\ 
 $ (NXT9F(X) \leftrightarrow NXT5P(X)) \land $ \\ 
 $ (BOX32F(X) \leftrightarrow BOX25P(X)) \land $ \\ 
 $ (BOX12F(X) \leftrightarrow BOX16P(X)) \land $ \\ 
 $ (E1NameInvF(dNameInv) \leftrightarrow E1NameInvP(dNameInv)) \land $ \\ 
 $ (BOX10F(X) \leftrightarrow BOX6P(X)) \land $ \\ 
 $ (BOX14F(X) \leftrightarrow BOX18P(X)) \land $ \\ 
 $ (BOX1F(X) \leftrightarrow BOX34P(X)) \land $ \\ 
 $ (BOX30F(X) \leftrightarrow BOX23P(X)) \land $ \\ 
 $ (BOX0F(X) \leftrightarrow BOX33P(X))) \land $ \\ 
 $ E1NameInvF(N13) \land $ \\ 
 $ E1NameInvF(N39) \land $ \\ 
 $ E1NameInvF(N22) \land $ \\ 
 $ E1NameInvF(N29) \land $ \\ 
 $ E1NameInvF(N49) \land $ \\ 
 $ E1NameInvF(N16) \land $ \\ 
 $ E1NameInvF(N46) \land $ \\ 
 $ E1NameInvF(N20) \land $ \\ 
 $ E1NameInvF(N23) \land $ \\ 
 $ E1NameInvF(N27) \land $ \\ 
 $ E1NameInvF(N35) \land $ \\ 
 $ E1NameInvF(N24) \land $ \\ 
 $ E1NameInvF(N21) \land $ \\ 
 $ E1NameInvF(N28) \land $ \\ 
 $ E1NameInvF(N40) \land $ \\ 
 $ E1NameInvF(N44) \land $ \\ 
 $ E1NameInvF(N32) \land $ \\ 
 $ E1NameInvF(N3) \land $ \\ 
 $ E1NameInvF(N42) \land $ \\ 
 $ E1NameInvF(N19) \land $ \\ 
 $ E1NameInvF(N9) \land $ \\ 
 $ E1NameInvF(N36) \land $ \\ 
 $ E1NameInvF(N14) \land $ \\ 
 $ E1NameInvF(N26) \land $ \\ 
 $ E1NameInvF(N34) \land $ \\ 
 $ E1NameInvF(N45) \land $ \\ 
 $ E1NameInvF(N12) \land $ \\ 
 $ E1NameInvF(N18) \land $ \\ 
 $ E1NameInvF(N33) \land $ \\ 
 $ E1NameInvF(N37) \land $ \\ 
 $ E1NameInvF(N43) \land $ \\ 
 $ E1NameInvF(N4) \land $ \\ 
 $ E1NameInvF(N2) \land $ \\ 
 $ E1NameInvF(N1) \land $ \\ 
 $ E1NameInvF(N31) \land $ \\ 
 $ E1NameInvF(N0) \land $ \\ 
 $ E1NameInvF(N47) \land $ \\ 
 $ E1NameInvF(N8) \land $ \\ 
 $ E1NameInvF(N48) \land $ \\ 
 $ E1NameInvF(N38) \land $ \\ 
 $ E1NameInvF(N30) \land $ \\ 
 $ E1NameInvF(N6) \land $ \\ 
 $ E1NameInvF(N10) \land $ \\ 
 $ E1NameInvF(N17) \land $ \\ 
 $ E1NameInvF(N5) \land $ \\ 
 $ E1NameInvF(N11) \land $ \\ 
 $ E1NameInvF(N41) \land $ \\ 
 $ E1NameInvF(N7) \land $ \\ 
 $ E1NameInvF(N15) \land $ \\ 
 $ E1NameInvF(N25) \land $ \\ 
 $ E2NameF(John) \land $ \\ 
 $ PersonF(John))$ 
\end{document}