\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. ((E1NameF(X) \rightarrow BOX4F(X)) \land $ \\ 
 $ (E2NameF(X) \rightarrow E1NameF(X)) \land $ \\ 
 $ (E1NameInvF(X) \rightarrow BOX1F(X)) \land $ \\ 
 $ (E2NameF(X) \rightarrow BOX0F(X)) \land $ \\ 
 $ (PersonF(X) \rightarrow E1NameF(X)) \land $ \\ 
 $ (E1NameF(X) \rightarrow BOX2F(X)) \land $ \\ 
 $ (PersonF(X) \rightarrow  \lnot E2NameF(X)) \land $ \\ 
 $ (E1NameInvF(X) \rightarrow StringF(X)) \land $ \\ 
 $ (StringF(X) \rightarrow  \lnot PersonF(X)) \land $ \\ 
 $ (E1NameInvF(X) \rightarrow BOX3F(X)) \land $ \\ 
 $  \Rbox ((BOX1F(X) \leftrightarrow  \Rbox BOX14F(X)) \land $ \\ 
 $ ( \Rnext BOX3F(X) \leftrightarrow (BOX3F(X) \land $ \\ 
 $  \Rnext BOX16F(X))) \land $ \\ 
 $ ( \Rnext BOX12P(X) \leftrightarrow (BOX12P(X) \land $ \\ 
 $  \Rnext PNameP)) \land $ \\ 
 $ (BOX10P(X) \leftrightarrow  \Rbox E1NameP(X)) \land $ \\ 
 $ ( \Rnext BOX4F(X) \leftrightarrow (BOX4F(X) \land $ \\ 
 $  \Rnext BOX17F(X))) \land $ \\ 
 $ ( \Rnext BOX14F(X) \leftrightarrow (BOX14F(X) \land $ \\ 
 $  \Rnext E1NameInvF(X))) \land $ \\ 
 $ ( \Rnext BOX7P(X) \leftrightarrow (BOX7P(X) \land $ \\ 
 $  \Rnext BOX8P(X))) \land $ \\ 
 $ ( \Rnext BOX13F(X) \leftrightarrow (BOX13F(X) \land $ \\ 
 $  \Rnext E2NameF(X))) \land $ \\ 
 $ (BOX18P(X) \leftrightarrow  \Rbox BOX11P(X)) \land $ \\ 
 $ (BOX8P(X) \leftrightarrow  \Rbox E1NameInvP(X)) \land $ \\ 
 $ ( \Rnext BOX15F(X) \leftrightarrow (BOX15F(X) \land $ \\ 
 $  \Rnext E1NameF(X))) \land $ \\ 
 $ (BOX6P(X) \leftrightarrow  \Rbox E2NameP(X)) \land $ \\ 
 $ (BOX16F(X) \leftrightarrow  \Rbox PinvNameF) \land $ \\ 
 $ ( \Rnext BOX9P(X) \leftrightarrow (BOX9P(X) \land $ \\ 
 $  \Rnext BOX10P(X))) \land $ \\ 
 $ (BOX19P(X) \leftrightarrow  \Rbox BOX12P(X)) \land $ \\ 
 $ ( \Rnext BOX11P(X) \leftrightarrow (BOX11P(X) \land $ \\ 
 $  \Rnext PinvNameP)) \land $ \\ 
 $ (BOX17F(X) \leftrightarrow  \Rbox PNameF) \land $ \\ 
 $ (BOX2F(X) \leftrightarrow  \Rbox BOX15F(X)) \land $ \\ 
 $ ( \Rnext BOX5P(X) \leftrightarrow (BOX5P(X) \land $ \\ 
 $  \Rnext BOX6P(X))) \land $ \\ 
 $ (BOX0F(X) \leftrightarrow  \Rbox BOX13F(X))) \land $ \\ 
 $ (BOX15F(X) \leftrightarrow BOX10P(X)) \land $ \\ 
 $ (PersonF(X) \leftrightarrow PersonP(X)) \land $ \\ 
 $ (BOX14F(X) \leftrightarrow BOX8P(X)) \land $ \\ 
 $ (BOX1F(X) \leftrightarrow BOX7P(X)) \land $ \\ 
 $ (BOX13F(X) \leftrightarrow BOX6P(X)) \land $ \\ 
 $ (StringF(X) \leftrightarrow StringP(X)) \land $ \\ 
 $ (BOX3F(X) \leftrightarrow BOX18P(X)) \land $ \\ 
 $ (BOX2F(X) \leftrightarrow BOX9P(X)) \land $ \\ 
 $ (E2NameF(X) \leftrightarrow E2NameP(X)) \land $ \\ 
 $ (PNameF \leftrightarrow PNameP) \land $ \\ 
 $ (BOX4F(X) \leftrightarrow BOX19P(X)) \land $ \\ 
 $ (BOX0F(X) \leftrightarrow BOX5P(X)) \land $ \\ 
 $ (BOX16F(X) \leftrightarrow BOX11P(X)) \land $ \\ 
 $ (PinvNameF \leftrightarrow PinvNameP) \land $ \\ 
 $ (E1NameF(X) \leftrightarrow E1NameP(X)) \land $ \\ 
 $ (PinvNameF \leftrightarrow PinvNameF) \land $ \\ 
 $ (E1NameInvF(X) \leftrightarrow E1NameInvP(X)) \land $ \\ 
 $ (PNameF \leftrightarrow PNameF) \land $ \\ 
 $ (BOX17F(X) \leftrightarrow BOX12P(X))) \land $ \\ 
 $ (PinvName \rightarrow E1Name(dName)) \land $ \\ 
 $ (PName \rightarrow E1NameInv(dNameInv)))$ 
\end{document}