\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. ((E3G25(X) \rightarrow E1G25(X)) \land $ \\ 
 $ (E4G9(X) \rightarrow E2G9(X)) \land $ \\ 
 $ (( \Lbox  \Ldiamond  \Rbox E2G9(X) \land $ \\ 
 $  \Rbox  \Rbox (E1G8(X) \land $ \\ 
 $ E3G14(X))) \rightarrow  \Lbox  \Lbox  \Lbox ( \Rdiamond (C23(X) \land $ \\ 
 $ C24(X)) \land $ \\ 
 $  \Ldiamond C13(X))) \land $ \\ 
 $ (E2G29(X) \rightarrow  \Rbox  \Lbox E2G29(X)) \land $ \\ 
 $ (E3G11(X) \rightarrow  \Rbox  \Lbox E3G11(X)) \land $ \\ 
 $ (E1G9(X) \rightarrow  \Rbox  \Lbox E1G9(X)) \land $ \\ 
 $ (E1G25(X) \rightarrow  \Rbox  \Lbox E1G25(X)) \land $ \\ 
 $ (E4G14(X) \rightarrow E3G14(X)) \land $ \\ 
 $ (E1G2(X) \rightarrow  \Rbox  \Lbox E1G2(X)) \land $ \\ 
 $ (( \Lbox ( \Rdiamond C11(X) \land $ \\ 
 $  \Rdiamond  \lnot E4G8(X)) \land $ \\ 
 $  \Lbox C8(X)) \rightarrow  \Rbox (C24(X) \land $ \\ 
 $  \Lbox C11(X) \land $ \\ 
 $  \Ldiamond C23(X) \land $ \\ 
 $ E4G17(X))) \land $ \\ 
 $ (E4G17(X) \rightarrow  \Rbox  \Lbox E4G17(X)) \land $ \\ 
 $ ( \Lbox  \Lbox  \Rbox (E4G4(X) \land $ \\ 
 $  \Ldiamond C6(X) \land $ \\ 
 $  \Ldiamond C15(X)) \rightarrow ( \Ldiamond  \Rbox (E4G25(X) \land $ \\ 
 $ C4(X)) \land $ \\ 
 $  \lnot C13(X) \land $ \\ 
 $ C7(X))) \land $ \\ 
 $ (E3G27(X) \rightarrow E1G27(X)) \land $ \\ 
 $ (( \Rbox  \Lbox (E4G25(X) \land $ \\ 
 $  \Ldiamond E2G3(X)) \land $ \\ 
 $  \Rdiamond  \Lbox C25(X)) \rightarrow  \Rbox  \Rbox ( \lnot C1(X) \land $ \\ 
 $  \Rdiamond (E5G29(X) \land $ \\ 
 $  \Ldiamond C28(X)))) \land $ \\ 
 $ (E3G7(X) \rightarrow  \Rbox  \Lbox E3G7(X)) \land $ \\ 
 $ (E2G20(X) \rightarrow  \Rbox  \Lbox E2G20(X)) \land $ \\ 
 $ (E4L1(X) \rightarrow E1L1(X)) \land $ \\ 
 $ (E3G28(X) \rightarrow E1G28(X)) \land $ \\ 
 $ ( \Ldiamond  \Rbox ( \Rdiamond (E4G12(X) \land $ \\ 
 $ E3G7(X)) \land $ \\ 
 $  \Lbox  \Rbox E3G25(X)) \rightarrow ( \Ldiamond  \Ldiamond  \Rdiamond  \Ldiamond C12(X) \land $ \\ 
 $ E1G3(X) \land $ \\ 
 $  \Rbox C28(X))) \land $ \\ 
 $ (E4G8(X) \rightarrow E1G8(X)) \land $ \\ 
 $ (E4L15(X) \rightarrow E1L15(X)) \land $ \\ 
 $ (E4G4(X) \rightarrow  \Rbox  \Lbox E4G4(X)) \land $ \\ 
 $ (E1G23(X) \rightarrow  \Rbox  \Lbox E1G23(X)) \land $ \\ 
 $ (E1G20(X) \rightarrow  \Rbox  \Lbox E1G20(X)) \land $ \\ 
 $ (E4G25(X) \rightarrow  \Rbox  \Lbox E4G25(X)) \land $ \\ 
 $ (E2G5(X) \rightarrow  \Rbox  \Lbox E2G5(X)) \land $ \\ 
 $ (E5G17(X) \rightarrow E4G17(X)) \land $ \\ 
 $ (E5G2(X) \rightarrow E3G2(X)) \land $ \\ 
 $ (E4G25(X) \rightarrow E3G25(X)) \land $ \\ 
 $ (E1G11(X) \rightarrow  \Rbox  \Lbox E1G11(X)) \land $ \\ 
 $ (E3G28(X) \rightarrow  \Rbox  \Lbox E3G28(X)) \land $ \\ 
 $ ( \Ldiamond (E4G14(X) \land $ \\ 
 $  \Lbox  \Rbox  \Ldiamond  \Ldiamond  \Ldiamond  \lnot C18(X)) \rightarrow  \Rdiamond ( \Rbox  \Rbox E2G20(X) \land $ \\ 
 $  \Rdiamond  \Ldiamond  \Ldiamond  \lnot C13(X))) \land $ \\ 
 $ ( \Rdiamond  \Ldiamond (E2L29(X) \land $ \\ 
 $  \Lbox  \Rdiamond  \Rdiamond  \Ldiamond  \lnot E5L1(X)) \rightarrow  \Ldiamond (C25(X) \land $ \\ 
 $  \Rbox  \Ldiamond  \Rdiamond  \Rdiamond  \Rdiamond  \Ldiamond E3G27(X))) \land $ \\ 
 $ (E1G8(X) \rightarrow  \Rbox  \Lbox E1G8(X)) \land $ \\ 
 $ (E2G9(X) \rightarrow E1G9(X)) \land $ \\ 
 $ (E1G4(X) \rightarrow  \Rbox  \Lbox E1G4(X)) \land $ \\ 
 $ (E2G29(X) \rightarrow E1G29(X)) \land $ \\ 
 $ ( \Lbox  \Rbox (C21(X) \land $ \\ 
 $ E3G28(X) \land $ \\ 
 $  \lnot E5G17(X) \land $ \\ 
 $ C15(X)) \rightarrow  \Rdiamond  \Rbox  \Ldiamond  \Ldiamond  \Ldiamond ( \Ldiamond C6(X) \land $ \\ 
 $  \lnot C25(X))) \land $ \\ 
 $ (E3G11(X) \rightarrow E1G11(X)) \land $ \\ 
 $ (E3G2(X) \rightarrow  \Rbox  \Lbox E3G2(X)) \land $ \\ 
 $ ( \Lbox  \Ldiamond (C16(X) \land $ \\ 
 $ E2G5(X) \land $ \\ 
 $  \Ldiamond  \Rbox  \lnot C13(X)) \rightarrow  \Rdiamond  \Rdiamond  \Rbox  \Rdiamond  \Rdiamond  \Rbox  \Rbox  \Rbox  \Rdiamond E1G19(X)) \land $ \\ 
 $ (E3G4(X) \rightarrow E1G4(X)) \land $ \\ 
 $ (E3G18(X) \rightarrow E2G18(X)) \land $ \\ 
 $ (E2G20(X) \rightarrow E1G20(X)) \land $ \\ 
 $ (E1G12(X) \rightarrow  \Rbox  \Lbox E1G12(X)) \land $ \\ 
 $ (E1G3(X) \rightarrow  \Rbox  \Lbox E1G3(X)) \land $ \\ 
 $ (E3G25(X) \rightarrow  \Rbox  \Lbox E3G25(X)) \land $ \\ 
 $ (E2G3(X) \rightarrow E1G3(X)) \land $ \\ 
 $ (E3G2(X) \rightarrow E1G2(X)) \land $ \\ 
 $ (E5G2(X) \rightarrow  \Rbox  \Lbox E5G2(X)) \land $ \\ 
 $ (E1G16(X) \rightarrow  \Rbox  \Lbox E1G16(X)) \land $ \\ 
 $ (E2G3(X) \rightarrow  \Rbox  \Lbox E2G3(X)) \land $ \\ 
 $ (E4G9(X) \rightarrow  \Rbox  \Lbox E4G9(X)) \land $ \\ 
 $ (E4G14(X) \rightarrow  \Rbox  \Lbox E4G14(X)) \land $ \\ 
 $ (E1G28(X) \rightarrow  \Rbox  \Lbox E1G28(X)) \land $ \\ 
 $ ( \Rbox  \Ldiamond (E3G4(X) \land $ \\ 
 $  \Ldiamond  \Lbox E5G2(X) \land $ \\ 
 $  \Lbox E1G7(X)) \rightarrow  \Rbox  \Rbox ( \Rbox (C17(X) \land $ \\ 
 $ E4L1(X)) \land $ \\ 
 $  \Ldiamond  \Ldiamond C25(X))) \land $ \\ 
 $ (E5G29(X) \rightarrow E2G29(X)) \land $ \\ 
 $ (E1G7(X) \rightarrow  \Rbox  \Lbox E1G7(X)) \land $ \\ 
 $ (E3G18(X) \rightarrow  \Rbox  \Lbox E3G18(X)) \land $ \\ 
 $ (E3G14(X) \rightarrow  \Rbox  \Lbox E3G14(X)) \land $ \\ 
 $ (E1G5(X) \rightarrow  \Rbox  \Lbox E1G5(X)) \land $ \\ 
 $ (E4G17(X) \rightarrow E1G17(X)) \land $ \\ 
 $ (E3G27(X) \rightarrow  \Rbox  \Lbox E3G27(X)) \land $ \\ 
 $ (E3G7(X) \rightarrow E1G7(X)) \land $ \\ 
 $ (E2L29(X) \rightarrow E1L29(X)) \land $ \\ 
 $ (E5G29(X) \rightarrow  \Rbox  \Lbox E5G29(X)) \land $ \\ 
 $ ( \Rbox ( \Rbox  \Ldiamond  \Rbox  \lnot E3G11(X) \land $ \\ 
 $  \Lbox  \Ldiamond C14(X)) \rightarrow  \Lbox  \Rdiamond ( \Rdiamond C16(X) \land $ \\ 
 $ E4G9(X) \land $ \\ 
 $ E3G2(X) \land $ \\ 
 $ E1G7(X))) \land $ \\ 
 $ (E1G17(X) \rightarrow  \Rbox  \Lbox E1G17(X)) \land $ \\ 
 $ (E1G19(X) \rightarrow  \Rbox  \Lbox E1G19(X)) \land $ \\ 
 $ ( \Rdiamond (C11(X) \land $ \\ 
 $  \Rdiamond (C18(X) \land $ \\ 
 $ E3G25(X)) \land $ \\ 
 $  \Ldiamond E5G4(X)) \rightarrow  \Ldiamond  \Rbox  \Lbox  \Rdiamond  \Lbox  \Rbox  \Lbox  \Rdiamond  \Rbox E1G23(X)) \land $ \\ 
 $ (E4G4(X) \rightarrow E3G4(X)) \land $ \\ 
 $ (E2G5(X) \rightarrow E1G5(X)) \land $ \\ 
 $ (E4G12(X) \rightarrow  \Rbox  \Lbox E4G12(X)) \land $ \\ 
 $ (E4G8(X) \rightarrow  \Rbox  \Lbox E4G8(X)) \land $ \\ 
 $ (E1G18(X) \rightarrow  \Rbox  \Lbox E1G18(X)) \land $ \\ 
 $ (( \Rdiamond E5G2(X) \land $ \\ 
 $  \Rbox  \Rbox  \Ldiamond  \Rdiamond (C19(X) \land $ \\ 
 $ E3G25(X))) \rightarrow  \Lbox ( \Lbox  \lnot E2G18(X) \land $ \\ 
 $  \Ldiamond  \Ldiamond (C1(X) \land $ \\ 
 $ E3G18(X)))) \land $ \\ 
 $ (E5G17(X) \rightarrow  \Rbox  \Lbox E5G17(X)) \land $ \\ 
 $ (E2G18(X) \rightarrow E1G18(X)) \land $ \\ 
 $ (E5G4(X) \rightarrow E4G4(X)) \land $ \\ 
 $ ( \Rdiamond  \Lbox  \Rdiamond  \Rdiamond (C7(X) \land $ \\ 
 $  \Lbox E1L26(X) \land $ \\ 
 $ C8(X)) \rightarrow  \Rbox ( \Ldiamond E2G29(X) \land $ \\ 
 $  \Rbox C13(X) \land $ \\ 
 $  \Lbox  \Ldiamond E1G16(X))) \land $ \\ 
 $ (E3G4(X) \rightarrow  \Rbox  \Lbox E3G4(X)) \land $ \\ 
 $ (E3G14(X) \rightarrow E1G14(X)) \land $ \\ 
 $ (E5L1(X) \rightarrow E4L1(X)) \land $ \\ 
 $ (E4G12(X) \rightarrow E1G12(X)) \land $ \\ 
 $ (E1G29(X) \rightarrow  \Rbox  \Lbox E1G29(X)) \land $ \\ 
 $ (E2G9(X) \rightarrow  \Rbox  \Lbox E2G9(X)) \land $ \\ 
 $ (E1G27(X) \rightarrow  \Rbox  \Lbox E1G27(X)) \land $ \\ 
 $ (E5G4(X) \rightarrow  \Rbox  \Lbox E5G4(X)) \land $ \\ 
 $ (E1G14(X) \rightarrow  \Rbox  \Lbox E1G14(X)) \land $ \\ 
 $ ( \Rdiamond  \Ldiamond  \Rbox  \Lbox  \Rbox  \Rbox  \Rdiamond  \Rbox  \lnot C4(X) \rightarrow  \Lbox  \Ldiamond  \Lbox (C12(X) \land $ \\ 
 $  \Ldiamond  \Rdiamond E4L15(X) \land $ \\ 
 $ C10(X))) \land $ \\ 
 $ (E2G18(X) \rightarrow  \Rbox  \Lbox E2G18(X)) \land $ \\ 
 $ (E1G9(X) \rightarrow  \SVbox PG9) \land $ \\ 
 $ (PinvG16 \rightarrow E1G16(dG16)) \land $ \\ 
 $ (E1G27Inv(X) \rightarrow  \SVbox PinvG27) \land $ \\ 
 $ (PG4 \rightarrow E1G4Inv(dG4Inv)) \land $ \\ 
 $ (E1L15(X) \rightarrow  \SVbox PL15) \land $ \\ 
 $ (PG18 \rightarrow E1G18Inv(dG18Inv)) \land $ \\ 
 $ (PinvG11 \rightarrow E1G11(dG11)) \land $ \\ 
 $ (PG9 \rightarrow E1G9Inv(dG9Inv)) \land $ \\ 
 $ (PinvG20 \rightarrow E1G20(dG20)) \land $ \\ 
 $ (E1G27(X) \rightarrow  \SVbox PG27) \land $ \\ 
 $ (PG2 \rightarrow E1G2Inv(dG2Inv)) \land $ \\ 
 $ (PinvL26 \rightarrow E1L26(dL26)) \land $ \\ 
 $ (E1G23(X) \rightarrow  \SVbox PG23) \land $ \\ 
 $ (E1G8Inv(X) \rightarrow  \SVbox PinvG8) \land $ \\ 
 $ (PinvG18 \rightarrow E1G18(dG18)) \land $ \\ 
 $ (E1G28Inv(X) \rightarrow  \SVbox PinvG28) \land $ \\ 
 $ (E1L26Inv(X) \rightarrow  \SVbox PinvL26) \land $ \\ 
 $ (PG14 \rightarrow E1G14Inv(dG14Inv)) \land $ \\ 
 $ (PL26 \rightarrow E1L26Inv(dL26Inv)) \land $ \\ 
 $ (PinvL15 \rightarrow E1L15(dL15)) \land $ \\ 
 $ (E1G12(X) \rightarrow  \SVbox PG12) \land $ \\ 
 $ (E1L1Inv(X) \rightarrow  \SVbox PinvL1) \land $ \\ 
 $ (E1G5Inv(X) \rightarrow  \SVbox PinvG5) \land $ \\ 
 $ (PinvL29 \rightarrow E1L29(dL29)) \land $ \\ 
 $ (E1L1(X) \rightarrow  \SVbox PL1) \land $ \\ 
 $ (E1G18Inv(X) \rightarrow  \SVbox PinvG18) \land $ \\ 
 $ (E1G19Inv(X) \rightarrow  \SVbox PinvG19) \land $ \\ 
 $ (PG28 \rightarrow E1G28Inv(dG28Inv)) \land $ \\ 
 $ (E1G16(X) \rightarrow  \SVbox PG16) \land $ \\ 
 $ (PinvG7 \rightarrow E1G7(dG7)) \land $ \\ 
 $ (E1G4Inv(X) \rightarrow  \SVbox PinvG4) \land $ \\ 
 $ (PG7 \rightarrow E1G7Inv(dG7Inv)) \land $ \\ 
 $ (PinvG14 \rightarrow E1G14(dG14)) \land $ \\ 
 $ (E1G11(X) \rightarrow  \SVbox PG11) \land $ \\ 
 $ (E1G17(X) \rightarrow  \SVbox PG17) \land $ \\ 
 $ (PG27 \rightarrow E1G27Inv(dG27Inv)) \land $ \\ 
 $ (PG8 \rightarrow E1G8Inv(dG8Inv)) \land $ \\ 
 $ (E1G19(X) \rightarrow  \SVbox PG19) \land $ \\ 
 $ (PinvG23 \rightarrow E1G23(dG23)) \land $ \\ 
 $ (E1G23Inv(X) \rightarrow  \SVbox PinvG23) \land $ \\ 
 $ (E1G14Inv(X) \rightarrow  \SVbox PinvG14) \land $ \\ 
 $ (PG19 \rightarrow E1G19Inv(dG19Inv)) \land $ \\ 
 $ (PG16 \rightarrow E1G16Inv(dG16Inv)) \land $ \\ 
 $ (PL1 \rightarrow E1L1Inv(dL1Inv)) \land $ \\ 
 $ (E1G9Inv(X) \rightarrow  \SVbox PinvG9) \land $ \\ 
 $ (E1G2(X) \rightarrow  \SVbox PG2) \land $ \\ 
 $ (PG17 \rightarrow E1G17Inv(dG17Inv)) \land $ \\ 
 $ (E1G3Inv(X) \rightarrow  \SVbox PinvG3) \land $ \\ 
 $ (PL29 \rightarrow E1L29Inv(dL29Inv)) \land $ \\ 
 $ (PG29 \rightarrow E1G29Inv(dG29Inv)) \land $ \\ 
 $ (E1G14(X) \rightarrow  \SVbox PG14) \land $ \\ 
 $ (E1G11Inv(X) \rightarrow  \SVbox PinvG11) \land $ \\ 
 $ (E1G29Inv(X) \rightarrow  \SVbox PinvG29) \land $ \\ 
 $ (PinvG2 \rightarrow E1G2(dG2)) \land $ \\ 
 $ (E1G28(X) \rightarrow  \SVbox PG28) \land $ \\ 
 $ (PinvG5 \rightarrow E1G5(dG5)) \land $ \\ 
 $ (E1G3(X) \rightarrow  \SVbox PG3) \land $ \\ 
 $ (E1G20Inv(X) \rightarrow  \SVbox PinvG20) \land $ \\ 
 $ (E1G25Inv(X) \rightarrow  \SVbox PinvG25) \land $ \\ 
 $ (E1G12Inv(X) \rightarrow  \SVbox PinvG12) \land $ \\ 
 $ (E1G4(X) \rightarrow  \SVbox PG4) \land $ \\ 
 $ (PinvG8 \rightarrow E1G8(dG8)) \land $ \\ 
 $ (E1L26(X) \rightarrow  \SVbox PL26) \land $ \\ 
 $ (PG3 \rightarrow E1G3Inv(dG3Inv)) \land $ \\ 
 $ (PinvG27 \rightarrow E1G27(dG27)) \land $ \\ 
 $ (E1G18(X) \rightarrow  \SVbox PG18) \land $ \\ 
 $ (E1L29Inv(X) \rightarrow  \SVbox PinvL29) \land $ \\ 
 $ (PG11 \rightarrow E1G11Inv(dG11Inv)) \land $ \\ 
 $ (PinvG4 \rightarrow E1G4(dG4)) \land $ \\ 
 $ (E1G16Inv(X) \rightarrow  \SVbox PinvG16) \land $ \\ 
 $ (PinvG9 \rightarrow E1G9(dG9)) \land $ \\ 
 $ (PinvG25 \rightarrow E1G25(dG25)) \land $ \\ 
 $ (PG12 \rightarrow E1G12Inv(dG12Inv)) \land $ \\ 
 $ (PL15 \rightarrow E1L15Inv(dL15Inv)) \land $ \\ 
 $ (E1G8(X) \rightarrow  \SVbox PG8) \land $ \\ 
 $ (E1G7(X) \rightarrow  \SVbox PG7) \land $ \\ 
 $ (E1G17Inv(X) \rightarrow  \SVbox PinvG17) \land $ \\ 
 $ (PinvG29 \rightarrow E1G29(dG29)) \land $ \\ 
 $ (PG5 \rightarrow E1G5Inv(dG5Inv)) \land $ \\ 
 $ (E1L29(X) \rightarrow  \SVbox PL29) \land $ \\ 
 $ (PinvG28 \rightarrow E1G28(dG28)) \land $ \\ 
 $ (PG25 \rightarrow E1G25Inv(dG25Inv)) \land $ \\ 
 $ (E1G7Inv(X) \rightarrow  \SVbox PinvG7) \land $ \\ 
 $ (PG23 \rightarrow E1G23Inv(dG23Inv)) \land $ \\ 
 $ (E1G29(X) \rightarrow  \SVbox PG29) \land $ \\ 
 $ (E1G5(X) \rightarrow  \SVbox PG5) \land $ \\ 
 $ (PinvL1 \rightarrow E1L1(dL1)) \land $ \\ 
 $ (E1G25(X) \rightarrow  \SVbox PG25) \land $ \\ 
 $ (PinvG3 \rightarrow E1G3(dG3)) \land $ \\ 
 $ (PinvG12 \rightarrow E1G12(dG12)) \land $ \\ 
 $ (PinvG19 \rightarrow E1G19(dG19)) \land $ \\ 
 $ (E1G2Inv(X) \rightarrow  \SVbox PinvG2) \land $ \\ 
 $ (E1L15Inv(X) \rightarrow  \SVbox PinvL15) \land $ \\ 
 $ (E1G20(X) \rightarrow  \SVbox PG20) \land $ \\ 
 $ (PinvG17 \rightarrow E1G17(dG17)) \land $ \\ 
 $ (PG20 \rightarrow E1G20Inv(dG20Inv)))$ 
\end{document}