\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. (BOX0F(X) \land $ \\ 
 $  \Rbox ((BOX2P(X) \leftrightarrow  \Rbox ((MinorP(X) \rightarrow PersonP(X)) \land $ \\ 
 $ (AdultP(X) \rightarrow PersonP(X)) \land $ \\ 
 $ (AdultP(X) \rightarrow BOX3P(X)) \land $ \\ 
 $  \lnot (MinorP(X) \land $ \\ 
 $ AdultP(X)))) \land $ \\ 
 $ ( \Rnext BOX1P(X) \leftrightarrow (BOX1P(X) \land $ \\ 
 $  \Rnext BOX2P(X))) \land $ \\ 
 $ (BOX5F(X) \leftrightarrow  \Rbox AdultF(X)) \land $ \\ 
 $ ( \Rnext BOX3P(X) \leftrightarrow (BOX3P(X) \land $ \\ 
 $  \Rnext AdultP(X))) \land $ \\ 
 $ ( \Rnext BOX4F(X) \leftrightarrow (BOX4F(X) \land $ \\ 
 $  \Rnext ((MinorF(X) \rightarrow PersonF(X)) \land $ \\ 
 $ (AdultF(X) \rightarrow PersonF(X)) \land $ \\ 
 $ (AdultF(X) \rightarrow BOX5F(X)) \land $ \\ 
 $  \lnot (MinorF(X) \land $ \\ 
 $ AdultF(X))))) \land $ \\ 
 $ (BOX0F(X) \leftrightarrow  \Rbox BOX4F(X))) \land $ \\ 
 $ (BOX0F(X) \leftrightarrow BOX1P(X)) \land $ \\ 
 $ (BOX4F(X) \leftrightarrow BOX2P(X)) \land $ \\ 
 $ (BOX5F(X) \leftrightarrow BOX3P(X)) \land $ \\ 
 $ (MinorF(X) \leftrightarrow MinorP(X)) \land $ \\ 
 $ (PersonF(X) \leftrightarrow PersonP(X)) \land $ \\ 
 $ (AdultF(X) \leftrightarrow AdultP(X))))$ 
\end{document}