\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. ((E5G18(X) \rightarrow  \Rbox  \Lbox E5G18(X)) \land $ \\ 
 $ (E1G20(X) \rightarrow  \Rbox  \Lbox E1G20(X)) \land $ \\ 
 $ ( \Ldiamond  \Rbox  \Rbox  \Rbox  \Rdiamond  \Rbox  \Rdiamond  \Rdiamond  \Ldiamond E2G21(X) \rightarrow  \Lbox  \Ldiamond  \Lbox ( \Lbox  \Rbox  \Ldiamond C12(X) \land $ \\ 
 $  \lnot E3G8(X))) \land $ \\ 
 $ (E4G0(X) \rightarrow E1G0(X)) \land $ \\ 
 $ (E3G9(X) \rightarrow E1G9(X)) \land $ \\ 
 $ (E4G10(X) \rightarrow E3G10(X)) \land $ \\ 
 $ ( \Ldiamond  \Rdiamond  \Ldiamond ( \Rdiamond  \Lbox  \Ldiamond E2G21(X) \land $ \\ 
 $  \Lbox E4L6(X)) \rightarrow  \Lbox  \Rbox  \Ldiamond  \Rdiamond  \Ldiamond  \Rbox  \Rdiamond  \Rbox  \Ldiamond C11(X)) \land $ \\ 
 $ ( \Lbox  \Lbox  \Ldiamond  \Lbox  \Rdiamond (E3G13(X) \land $ \\ 
 $  \Ldiamond  \Lbox C12(X)) \rightarrow  \Rdiamond  \Ldiamond  \Rdiamond  \Rbox ( \Rbox  \Ldiamond E5G2(X) \land $ \\ 
 $  \Rdiamond E1G4(X))) \land $ \\ 
 $ (E5G2(X) \rightarrow  \Rbox  \Lbox E5G2(X)) \land $ \\ 
 $ (E5G28(X) \rightarrow E1G28(X)) \land $ \\ 
 $ (E1G10(X) \rightarrow  \Rbox  \Lbox E1G10(X)) \land $ \\ 
 $ (E2G13(X) \rightarrow  \Rbox  \Lbox E2G13(X)) \land $ \\ 
 $ (E3G8(X) \rightarrow E1G8(X)) \land $ \\ 
 $ ( \Rbox  \Rbox ( \Rbox  \Lbox  \Rbox C26(X) \land $ \\ 
 $  \Rbox  \Rdiamond C9(X)) \rightarrow  \Rbox  \Rdiamond  \Rdiamond  \Lbox  \Rbox  \Lbox  \Ldiamond  \Rbox  \Rdiamond E2G13(X)) \land $ \\ 
 $ (( \Ldiamond  \Ldiamond  \Ldiamond  \Lbox  \Ldiamond  \Rbox C27(X) \land $ \\ 
 $  \Rdiamond E2G20(X)) \rightarrow  \Rdiamond ( \Lbox  \Rbox (E5G11(X) \land $ \\ 
 $  \Rdiamond E1G5(X)) \land $ \\ 
 $  \lnot E3G10(X))) \land $ \\ 
 $ (E1G17(X) \rightarrow  \Rbox  \Lbox E1G17(X)) \land $ \\ 
 $ (E1G2(X) \rightarrow  \Rbox  \Lbox E1G2(X)) \land $ \\ 
 $ (E5G27(X) \rightarrow E1G27(X)) \land $ \\ 
 $ (E3G13(X) \rightarrow  \Rbox  \Lbox E3G13(X)) \land $ \\ 
 $ (E3G10(X) \rightarrow  \Rbox  \Lbox E3G10(X)) \land $ \\ 
 $ ( \Rbox  \Rbox ( \Lbox  \Ldiamond C27(X) \land $ \\ 
 $  \Lbox  \Rdiamond  \Lbox E5G18(X)) \rightarrow  \Rbox  \Lbox  \Lbox  \Rbox  \Lbox  \Lbox  \Lbox  \Ldiamond  \Lbox E1G5(X)) \land $ \\ 
 $ (E1G4(X) \rightarrow  \Rbox  \Lbox E1G4(X)) \land $ \\ 
 $ ( \Rbox ( \Rbox  \Rbox E1G6(X) \land $ \\ 
 $  \Rbox (C7(X) \land $ \\ 
 $  \Lbox E5G17(X))) \rightarrow  \Rbox ( \Rdiamond  \Ldiamond  \Ldiamond E5G5(X) \land $ \\ 
 $  \Rdiamond  \Rdiamond  \Rbox C7(X))) \land $ \\ 
 $ (E1G0(X) \rightarrow  \Rbox  \Lbox E1G0(X)) \land $ \\ 
 $ (E5G17(X) \rightarrow  \Rbox  \Lbox E5G17(X)) \land $ \\ 
 $ (E5G28(X) \rightarrow  \Rbox  \Lbox E5G28(X)) \land $ \\ 
 $ (E2G20(X) \rightarrow E1G20(X)) \land $ \\ 
 $ (E5G17(X) \rightarrow E1G17(X)) \land $ \\ 
 $ (E5G14(X) \rightarrow E1G14(X)) \land $ \\ 
 $ ( \Ldiamond  \Lbox  \Lbox  \Lbox  \Ldiamond  \Rdiamond  \Lbox  \Lbox  \Lbox E4G10(X) \rightarrow  \Rbox  \Ldiamond ( \Rbox E1G21(X) \land $ \\ 
 $  \Ldiamond  \Lbox  \Lbox  \Rdiamond E5G14(X))) \land $ \\ 
 $ (E4G0(X) \rightarrow  \Rbox  \Lbox E4G0(X)) \land $ \\ 
 $ (E1G27(X) \rightarrow  \Rbox  \Lbox E1G27(X)) \land $ \\ 
 $ (( \Rbox E4G4(X) \land $ \\ 
 $  \Ldiamond  \Lbox  \Rdiamond (E4G10(X) \land $ \\ 
 $  \Ldiamond C29(X))) \rightarrow  \Lbox  \Rdiamond  \Rdiamond  \Ldiamond ( \Lbox E4G7(X) \land $ \\ 
 $  \Ldiamond  \Lbox E1G14(X))) \land $ \\ 
 $ (E5G2(X) \rightarrow E1G2(X)) \land $ \\ 
 $ (E5G11(X) \rightarrow  \Rbox  \Lbox E5G11(X)) \land $ \\ 
 $ ( \Lbox  \Rbox ( \Rbox  \Rdiamond  \Ldiamond  \Rbox C20(X) \land $ \\ 
 $  \Rdiamond E3G1(X)) \rightarrow  \Ldiamond  \Ldiamond  \Ldiamond  \Ldiamond  \Lbox  \Rbox  \Ldiamond  \Ldiamond  \Lbox C0(X)) \land $ \\ 
 $ ( \Lbox  \Rbox  \Rbox  \Lbox  \Ldiamond  \Rdiamond  \Rdiamond  \Rbox  \lnot E4G0(X) \rightarrow ( \Rdiamond ( \Rbox E1G16(X) \land $ \\ 
 $  \Rdiamond C2(X)) \land $ \\ 
 $  \Ldiamond  \Ldiamond E5G27(X))) \land $ \\ 
 $ (E4G7(X) \rightarrow E1G7(X)) \land $ \\ 
 $ (E5G5(X) \rightarrow  \Rbox  \Lbox E5G5(X)) \land $ \\ 
 $ (E1G6(X) \rightarrow  \Rbox  \Lbox E1G6(X)) \land $ \\ 
 $ (E1G14(X) \rightarrow  \Rbox  \Lbox E1G14(X)) \land $ \\ 
 $ (E4G10(X) \rightarrow  \Rbox  \Lbox E4G10(X)) \land $ \\ 
 $ (E2G13(X) \rightarrow E1G13(X)) \land $ \\ 
 $ (E2G21(X) \rightarrow  \Rbox  \Lbox E2G21(X)) \land $ \\ 
 $ (E3G10(X) \rightarrow E1G10(X)) \land $ \\ 
 $ (E4G13(X) \rightarrow E3G13(X)) \land $ \\ 
 $ (E3G9(X) \rightarrow  \Rbox  \Lbox E3G9(X)) \land $ \\ 
 $ (E1G18(X) \rightarrow  \Rbox  \Lbox E1G18(X)) \land $ \\ 
 $ (E4G4(X) \rightarrow  \Rbox  \Lbox E4G4(X)) \land $ \\ 
 $ (E1G9(X) \rightarrow  \Rbox  \Lbox E1G9(X)) \land $ \\ 
 $ (E1G21(X) \rightarrow  \Rbox  \Lbox E1G21(X)) \land $ \\ 
 $ ( \Ldiamond  \Rbox  \Ldiamond  \Ldiamond  \Rdiamond  \Rdiamond  \Ldiamond  \Lbox  \Ldiamond E4G13(X) \rightarrow  \Rdiamond  \Rdiamond  \Rbox  \Rdiamond  \Lbox  \Ldiamond  \Rbox  \Rdiamond  \Rdiamond C25(X)) \land $ \\ 
 $ (E3G1(X) \rightarrow E1G1(X)) \land $ \\ 
 $ (E5G11(X) \rightarrow E1G11(X)) \land $ \\ 
 $ (E3G8(X) \rightarrow  \Rbox  \Lbox E3G8(X)) \land $ \\ 
 $ ( \Lbox  \Ldiamond  \Rdiamond  \Ldiamond (C1(X) \land $ \\ 
 $  \Ldiamond  \Ldiamond  \lnot C9(X)) \rightarrow  \Rbox  \Rbox  \Rbox  \Rbox  \Ldiamond  \Rbox  \Rbox (C21(X) \land $ \\ 
 $ C17(X))) \land $ \\ 
 $ (E1G28(X) \rightarrow  \Rbox  \Lbox E1G28(X)) \land $ \\ 
 $ (E5G27(X) \rightarrow  \Rbox  \Lbox E5G27(X)) \land $ \\ 
 $ (E1G13(X) \rightarrow  \Rbox  \Lbox E1G13(X)) \land $ \\ 
 $ (E4G7(X) \rightarrow  \Rbox  \Lbox E4G7(X)) \land $ \\ 
 $ (E1G11(X) \rightarrow  \Rbox  \Lbox E1G11(X)) \land $ \\ 
 $ (E1G8(X) \rightarrow  \Rbox  \Lbox E1G8(X)) \land $ \\ 
 $ (E1G7(X) \rightarrow  \Rbox  \Lbox E1G7(X)) \land $ \\ 
 $ (E5G5(X) \rightarrow E1G5(X)) \land $ \\ 
 $ ( \Ldiamond  \Rbox  \Lbox  \Rdiamond  \Rdiamond ( \lnot C28(X) \land $ \\ 
 $  \Lbox C6(X)) \rightarrow  \Lbox  \Rdiamond  \Ldiamond  \Rdiamond ( \Lbox E5G28(X) \land $ \\ 
 $  \Rdiamond  \Ldiamond C5(X))) \land $ \\ 
 $ (E1G5(X) \rightarrow  \Rbox  \Lbox E1G5(X)) \land $ \\ 
 $ (E1G1(X) \rightarrow  \Rbox  \Lbox E1G1(X)) \land $ \\ 
 $ (E4G4(X) \rightarrow E1G4(X)) \land $ \\ 
 $ (E3G1(X) \rightarrow  \Rbox  \Lbox E3G1(X)) \land $ \\ 
 $ (E1G16(X) \rightarrow  \Rbox  \Lbox E1G16(X)) \land $ \\ 
 $ (E5G14(X) \rightarrow  \Rbox  \Lbox E5G14(X)) \land $ \\ 
 $ (E4L6(X) \rightarrow E1L6(X)) \land $ \\ 
 $ (E3G13(X) \rightarrow E2G13(X)) \land $ \\ 
 $ (E4G13(X) \rightarrow  \Rbox  \Lbox E4G13(X)) \land $ \\ 
 $ (E2G21(X) \rightarrow E1G21(X)) \land $ \\ 
 $ ( \Lbox  \Rdiamond  \Rdiamond  \Rdiamond  \Lbox  \Rdiamond  \Lbox  \Lbox  \lnot C26(X) \rightarrow  \Ldiamond  \Ldiamond  \Lbox  \Lbox  \Ldiamond (E5G28(X) \land $ \\ 
 $  \Rbox  \lnot E3G9(X))) \land $ \\ 
 $ (E5G18(X) \rightarrow E1G18(X)) \land $ \\ 
 $ (E2G20(X) \rightarrow  \Rbox  \Lbox E2G20(X)) \land $ \\ 
 $ (E1G20Inv(X) \rightarrow  \SVbox PinvG20) \land $ \\ 
 $ (PG4 \rightarrow E1G4Inv(dG4Inv)) \land $ \\ 
 $ (E1L6Inv(X) \rightarrow  \SVbox PinvL6) \land $ \\ 
 $ (PG14 \rightarrow E1G14Inv(dG14Inv)) \land $ \\ 
 $ (E1G6Inv(X) \rightarrow  \SVbox PinvG6) \land $ \\ 
 $ (E1G7(X) \rightarrow  \SVbox PG7) \land $ \\ 
 $ (PG0 \rightarrow E1G0Inv(dG0Inv)) \land $ \\ 
 $ (E1G28(X) \rightarrow  \SVbox PG28) \land $ \\ 
 $ (E1G13Inv(X) \rightarrow  \SVbox PinvG13) \land $ \\ 
 $ (PinvG27 \rightarrow E1G27(dG27)) \land $ \\ 
 $ (E1G11(X) \rightarrow  \SVbox PG11) \land $ \\ 
 $ (PG16 \rightarrow E1G16Inv(dG16Inv)) \land $ \\ 
 $ (E1G4(X) \rightarrow  \SVbox PG4) \land $ \\ 
 $ (E1G2Inv(X) \rightarrow  \SVbox PinvG2) \land $ \\ 
 $ (PG11 \rightarrow E1G11Inv(dG11Inv)) \land $ \\ 
 $ (E1G2(X) \rightarrow  \SVbox PG2) \land $ \\ 
 $ (PinvG16 \rightarrow E1G16(dG16)) \land $ \\ 
 $ (E1G16Inv(X) \rightarrow  \SVbox PinvG16) \land $ \\ 
 $ (PinvG0 \rightarrow E1G0(dG0)) \land $ \\ 
 $ (E1G5(X) \rightarrow  \SVbox PG5) \land $ \\ 
 $ (PinvG7 \rightarrow E1G7(dG7)) \land $ \\ 
 $ (E1G8(X) \rightarrow  \SVbox PG8) \land $ \\ 
 $ (PG5 \rightarrow E1G5Inv(dG5Inv)) \land $ \\ 
 $ (PinvG21 \rightarrow E1G21(dG21)) \land $ \\ 
 $ (PinvG13 \rightarrow E1G13(dG13)) \land $ \\ 
 $ (E1G9(X) \rightarrow  \SVbox PG9) \land $ \\ 
 $ (E1G7Inv(X) \rightarrow  \SVbox PinvG7) \land $ \\ 
 $ (PinvG4 \rightarrow E1G4(dG4)) \land $ \\ 
 $ (E1G9Inv(X) \rightarrow  \SVbox PinvG9) \land $ \\ 
 $ (E1G10Inv(X) \rightarrow  \SVbox PinvG10) \land $ \\ 
 $ (E1G10(X) \rightarrow  \SVbox PG10) \land $ \\ 
 $ (PinvG17 \rightarrow E1G17(dG17)) \land $ \\ 
 $ (E1G16(X) \rightarrow  \SVbox PG16) \land $ \\ 
 $ (PG13 \rightarrow E1G13Inv(dG13Inv)) \land $ \\ 
 $ (PG6 \rightarrow E1G6Inv(dG6Inv)) \land $ \\ 
 $ (E1G0(X) \rightarrow  \SVbox PG0) \land $ \\ 
 $ (PinvG11 \rightarrow E1G11(dG11)) \land $ \\ 
 $ (E1G1Inv(X) \rightarrow  \SVbox PinvG1) \land $ \\ 
 $ (E1G5Inv(X) \rightarrow  \SVbox PinvG5) \land $ \\ 
 $ (E1G17Inv(X) \rightarrow  \SVbox PinvG17) \land $ \\ 
 $ (PinvG10 \rightarrow E1G10(dG10)) \land $ \\ 
 $ (PinvG18 \rightarrow E1G18(dG18)) \land $ \\ 
 $ (PinvG2 \rightarrow E1G2(dG2)) \land $ \\ 
 $ (E1G21Inv(X) \rightarrow  \SVbox PinvG21) \land $ \\ 
 $ (PG10 \rightarrow E1G10Inv(dG10Inv)) \land $ \\ 
 $ (PG20 \rightarrow E1G20Inv(dG20Inv)) \land $ \\ 
 $ (E1G4Inv(X) \rightarrow  \SVbox PinvG4) \land $ \\ 
 $ (PinvG14 \rightarrow E1G14(dG14)) \land $ \\ 
 $ (PinvG6 \rightarrow E1G6(dG6)) \land $ \\ 
 $ (E1G14Inv(X) \rightarrow  \SVbox PinvG14) \land $ \\ 
 $ (E1G17(X) \rightarrow  \SVbox PG17) \land $ \\ 
 $ (E1G14(X) \rightarrow  \SVbox PG14) \land $ \\ 
 $ (E1G1(X) \rightarrow  \SVbox PG1) \land $ \\ 
 $ (PinvL6 \rightarrow E1L6(dL6)) \land $ \\ 
 $ (PG17 \rightarrow E1G17Inv(dG17Inv)) \land $ \\ 
 $ (E1G18(X) \rightarrow  \SVbox PG18) \land $ \\ 
 $ (PG18 \rightarrow E1G18Inv(dG18Inv)) \land $ \\ 
 $ (PinvG1 \rightarrow E1G1(dG1)) \land $ \\ 
 $ (PG2 \rightarrow E1G2Inv(dG2Inv)) \land $ \\ 
 $ (E1G0Inv(X) \rightarrow  \SVbox PinvG0) \land $ \\ 
 $ (E1G28Inv(X) \rightarrow  \SVbox PinvG28) \land $ \\ 
 $ (PinvG8 \rightarrow E1G8(dG8)) \land $ \\ 
 $ (PG9 \rightarrow E1G9Inv(dG9Inv)) \land $ \\ 
 $ (PL6 \rightarrow E1L6Inv(dL6Inv)) \land $ \\ 
 $ (E1G18Inv(X) \rightarrow  \SVbox PinvG18) \land $ \\ 
 $ (PG8 \rightarrow E1G8Inv(dG8Inv)) \land $ \\ 
 $ (E1L6(X) \rightarrow  \SVbox PL6) \land $ \\ 
 $ (E1G13(X) \rightarrow  \SVbox PG13) \land $ \\ 
 $ (PG21 \rightarrow E1G21Inv(dG21Inv)) \land $ \\ 
 $ (E1G27Inv(X) \rightarrow  \SVbox PinvG27) \land $ \\ 
 $ (E1G6(X) \rightarrow  \SVbox PG6) \land $ \\ 
 $ (E1G20(X) \rightarrow  \SVbox PG20) \land $ \\ 
 $ (PinvG9 \rightarrow E1G9(dG9)) \land $ \\ 
 $ (PG1 \rightarrow E1G1Inv(dG1Inv)) \land $ \\ 
 $ (E1G21(X) \rightarrow  \SVbox PG21) \land $ \\ 
 $ (PinvG20 \rightarrow E1G20(dG20)) \land $ \\ 
 $ (PinvG5 \rightarrow E1G5(dG5)) \land $ \\ 
 $ (E1G8Inv(X) \rightarrow  \SVbox PinvG8) \land $ \\ 
 $ (PinvG28 \rightarrow E1G28(dG28)) \land $ \\ 
 $ (PG27 \rightarrow E1G27Inv(dG27Inv)) \land $ \\ 
 $ (E1G11Inv(X) \rightarrow  \SVbox PinvG11) \land $ \\ 
 $ (E1G27(X) \rightarrow  \SVbox PG27) \land $ \\ 
 $ (PG28 \rightarrow E1G28Inv(dG28Inv)) \land $ \\ 
 $ (PG7 \rightarrow E1G7Inv(dG7Inv)))$ 
\end{document}