\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. ( \Rbox (( \Rdiamond (C0(X) \land $ \\ 
 $  \Rdiamond E2G1(X)) \rightarrow  \Rbox (C0(X) \land $ \\ 
 $  \Rbox E3L0(X))) \land $ \\ 
 $ ( \Rdiamond  \Rbox  \Rbox  \Rdiamond C0(X) \rightarrow (E3G0(X) \land $ \\ 
 $  \Rdiamond  \Rnext C1(X))) \land $ \\ 
 $ ( \Rbox  \Rbox  \Rbox  \Rnext E1G0(X) \rightarrow  \Rbox (C0(X) \land $ \\ 
 $  \Rnext C0(X))) \land $ \\ 
 $ ((C0(X) \land $ \\ 
 $ E3L0(X) \land $ \\ 
 $ C1(X)) \rightarrow  \Rdiamond  \Rbox (C0(X) \land $ \\ 
 $ E3G0(X))) \land $ \\ 
 $ ((C0(X) \land $ \\ 
 $  \Rdiamond  \Rbox C1(X)) \rightarrow  \Rdiamond (E3L0(X) \land $ \\ 
 $  \Rbox C1(X))) \land $ \\ 
 $ ( \Rbox  \Rdiamond (E2L0(X) \land $ \\ 
 $ E1L1(X)) \rightarrow  \Rdiamond  \Rbox (E2G0(X) \land $ \\ 
 $ E3L1(X))) \land $ \\ 
 $ (( \Rnext E2L1(X) \land $ \\ 
 $  \Rbox E2G1(X)) \rightarrow ( \Rnext C0(X) \land $ \\ 
 $  \Rbox C0(X))) \land $ \\ 
 $ ( \Rdiamond (C0(X) \land $ \\ 
 $  \Rnext E2L0(X)) \rightarrow  \Rdiamond  \Rdiamond (E2G0(X) \land $ \\ 
 $ C0(X))) \land $ \\ 
 $ ((C0(X) \land $ \\ 
 $  \Rbox  \Rdiamond C1(X)) \rightarrow (E2G0(X) \land $ \\ 
 $ E2G1(X) \land $ \\ 
 $ C1(X))) \land $ \\ 
 $ (( \Rnext E3G0(X) \land $ \\ 
 $  \Rnext C0(X)) \rightarrow  \Rbox (E1G0(X) \land $ \\ 
 $  \Rdiamond C1(X))) \land $ \\ 
 $ (E2G1(X) \rightarrow E1G1(X)) \land $ \\ 
 $ (E2L1(X) \rightarrow E1L1(X)) \land $ \\ 
 $ (E2G0(X) \rightarrow E1G0(X)) \land $ \\ 
 $ (E3L1(X) \rightarrow E2L1(X)) \land $ \\ 
 $ (E3L0(X) \rightarrow E2L0(X)) \land $ \\ 
 $ (E2L0(X) \rightarrow E1L0(X)) \land $ \\ 
 $ (E3G0(X) \rightarrow E2G0(X))) \land $ \\ 
 $ ( \Rdiamond E1G0Inv(X) \rightarrow  \Rbox E1G0Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1G1(X) \rightarrow  \Rbox PG1) \land $ \\ 
 $ ( \Rdiamond E1L0Inv(X) \rightarrow  \Rbox PinvL0) \land $ \\ 
 $ ( \Rdiamond E1G1(X) \rightarrow  \Rbox E1G1(X)) \land $ \\ 
 $ ( \Rdiamond E2G0(X) \rightarrow  \Rbox E2G0(X)) \land $ \\ 
 $ ( \Rdiamond E2G1(X) \rightarrow  \Rbox E2G1(X)) \land $ \\ 
 $ ( \Rdiamond E1G0Inv(X) \rightarrow  \Rbox PinvG0) \land $ \\ 
 $ ( \Rdiamond E1G1Inv(X) \rightarrow  \Rbox PinvG1) \land $ \\ 
 $ ( \Rdiamond E1L1Inv(X) \rightarrow  \Rbox PinvL1) \land $ \\ 
 $ ( \Rdiamond E1G0(X) \rightarrow  \Rbox PG0) \land $ \\ 
 $ ( \Rdiamond E1G0(X) \rightarrow  \Rbox E1G0(X)) \land $ \\ 
 $ ( \Rdiamond E1G1Inv(X) \rightarrow  \Rbox E1G1Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1L0(X) \rightarrow  \Rbox PL0) \land $ \\ 
 $ ( \Rdiamond E3G0(X) \rightarrow  \Rbox E3G0(X)) \land $ \\ 
 $ ( \Rdiamond E1L1(X) \rightarrow  \Rbox PL1)) \land $ \\ 
 $ (PinvG1 \rightarrow E1G1(dG1)) \land $ \\ 
 $ (PL0 \rightarrow E1L0Inv(dL0Inv)) \land $ \\ 
 $ (PL1 \rightarrow E1L1Inv(dL1Inv)) \land $ \\ 
 $ (PinvG0 \rightarrow E1G0(dG0)) \land $ \\ 
 $ (PinvL0 \rightarrow E1L0(dL0)) \land $ \\ 
 $ (PG0 \rightarrow E1G0Inv(dG0Inv)) \land $ \\ 
 $ (PG1 \rightarrow E1G1Inv(dG1Inv)) \land $ \\ 
 $ (PinvL1 \rightarrow E1L1(dL1)))$ 
\end{document}