\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}}


$( \Rbox  \Lbox  \forall X. (( \Rdiamond ( \Ldiamond  \lnot C26(X) \land $ \\ 
 $  \Ldiamond C25(X) \land $ \\ 
 $  \Rdiamond E3G12(X)) \rightarrow ( \Rdiamond  \Ldiamond  \Rdiamond C10(X) \land $ \\ 
 $  \lnot C20(X) \land $ \\ 
 $  \Rbox E4L20(X))) \land $ \\ 
 $ ( \Rbox  \Rdiamond  \Rdiamond (C28(X) \land $ \\ 
 $  \Lbox E4G13(X) \land $ \\ 
 $  \Ldiamond E3L28(X)) \rightarrow (E4L26(X) \land $ \\ 
 $  \lnot E5G25(X) \land $ \\ 
 $ E2L8(X) \land $ \\ 
 $  \Rbox  \Rbox C22(X))) \land $ \\ 
 $ ( \Rbox ( \lnot C5(X) \land $ \\ 
 $  \Rdiamond (E3L9(X) \land $ \\ 
 $ E3G25(X)) \land $ \\ 
 $ C6(X)) \rightarrow ( \lnot C2(X) \land $ \\ 
 $  \Rdiamond  \lnot E4G28(X) \land $ \\ 
 $  \Rdiamond  \lnot E5G18(X))) \land $ \\ 
 $ (( \lnot C18(X) \land $ \\ 
 $  \Rdiamond  \Rdiamond C7(X) \land $ \\ 
 $  \Ldiamond  \Ldiamond C8(X)) \rightarrow  \Rdiamond  \Rbox  \Lbox  \Rdiamond (C24(X) \land $ \\ 
 $ E1L26(X) \land $ \\ 
 $  \lnot E2L14(X))) \land $ \\ 
 $ ( \Rdiamond ( \Rbox  \Lbox  \Ldiamond  \lnot C9(X) \land $ \\ 
 $  \Rdiamond  \Rdiamond E3G10(X)) \rightarrow  \Rbox (C24(X) \land $ \\ 
 $  \Lbox  \Lbox (C3(X) \land $ \\ 
 $  \Rbox  \Ldiamond E3G14(X)))) \land $ \\ 
 $ (( \Rbox  \Lbox  \Lbox  \Ldiamond  \lnot E2L2(X) \land $ \\ 
 $  \Rdiamond  \lnot C26(X)) \rightarrow ( \Rdiamond C15(X) \land $ \\ 
 $  \Ldiamond ( \Rdiamond C28(X) \land $ \\ 
 $ C6(X) \land $ \\ 
 $ E1G18(X)))) \land $ \\ 
 $ (( \Rbox C5(X) \land $ \\ 
 $  \Rbox  \Lbox E3L3(X) \land $ \\ 
 $ C10(X) \land $ \\ 
 $ C17(X)) \rightarrow ( \Ldiamond  \lnot C24(X) \land $ \\ 
 $  \Ldiamond  \Ldiamond (E5L17(X) \land $ \\ 
 $  \lnot C24(X)))) \land $ \\ 
 $ ( \Rbox  \Ldiamond  \Rbox  \Lbox ( \Lbox C18(X) \land $ \\ 
 $ E2G11(X) \land $ \\ 
 $ C3(X)) \rightarrow ( \lnot E2G11(X) \land $ \\ 
 $ C19(X) \land $ \\ 
 $  \Lbox  \Lbox (C10(X) \land $ \\ 
 $ C19(X)))) \land $ \\ 
 $ (( \Lbox  \Rdiamond  \Rdiamond  \Rbox  \lnot C20(X) \land $ \\ 
 $  \Ldiamond  \Rdiamond E2L23(X)) \rightarrow  \Ldiamond (E1L13(X) \land $ \\ 
 $ E1G5(X) \land $ \\ 
 $  \Ldiamond  \Ldiamond  \Lbox  \Rbox C4(X))) \land $ \\ 
 $ ( \Ldiamond ( \Rbox  \lnot C0(X) \land $ \\ 
 $ C3(X) \land $ \\ 
 $  \Ldiamond  \lnot C8(X)) \rightarrow  \Rbox ( \Rbox  \Lbox  \lnot E2L3(X) \land $ \\ 
 $  \Ldiamond (E1G26(X) \land $ \\ 
 $ C22(X)))) \land $ \\ 
 $ ( \Rbox (E2L19(X) \land $ \\ 
 $ C11(X) \land $ \\ 
 $  \Ldiamond E3L0(X) \land $ \\ 
 $  \lnot C14(X)) \rightarrow  \Rdiamond  \Ldiamond ( \lnot C17(X) \land $ \\ 
 $  \lnot E1G2(X) \land $ \\ 
 $  \lnot E5G10(X))) \land $ \\ 
 $ ((E4L9(X) \land $ \\ 
 $  \Ldiamond C3(X) \land $ \\ 
 $ C28(X) \land $ \\ 
 $ E1G16(X) \land $ \\ 
 $ C16(X)) \rightarrow  \Ldiamond  \Rbox  \Lbox ( \lnot E3G2(X) \land $ \\ 
 $  \Rbox  \Rbox  \lnot E1L22(X))) \land $ \\ 
 $ (( \Lbox C3(X) \land $ \\ 
 $  \Rdiamond  \Rdiamond  \Ldiamond (C4(X) \land $ \\ 
 $  \lnot C26(X))) \rightarrow  \Ldiamond ( \lnot C9(X) \land $ \\ 
 $  \Ldiamond (C19(X) \land $ \\ 
 $  \Lbox  \lnot C27(X)))) \land $ \\ 
 $ ( \Ldiamond  \Rdiamond (E3L19(X) \land $ \\ 
 $  \lnot C20(X) \land $ \\ 
 $  \Lbox  \lnot E4G11(X)) \rightarrow ( \Lbox (E1G26(X) \land $ \\ 
 $  \Lbox  \Rbox E5L14(X)) \land $ \\ 
 $  \Ldiamond  \lnot E2G21(X))) \land $ \\ 
 $ (( \Rdiamond  \lnot C28(X) \land $ \\ 
 $  \Rdiamond  \Lbox (E4G1(X) \land $ \\ 
 $  \lnot E4L25(X))) \rightarrow  \Rdiamond  \Rbox  \Rdiamond (E1G9(X) \land $ \\ 
 $ C28(X) \land $ \\ 
 $ C0(X) \land $ \\ 
 $ E5G7(X))) \land $ \\ 
 $ ( \Rbox  \Ldiamond  \Rdiamond  \Ldiamond ( \lnot E5L15(X) \land $ \\ 
 $  \Rbox  \Rdiamond C13(X)) \rightarrow  \Rbox (E3G15(X) \land $ \\ 
 $  \Rdiamond (C20(X) \land $ \\ 
 $  \Ldiamond E5L18(X) \land $ \\ 
 $ C15(X)))) \land $ \\ 
 $ ( \Lbox  \Rbox  \Rdiamond  \Lbox  \Rdiamond  \Rdiamond (E1L29(X) \land $ \\ 
 $  \Ldiamond C1(X)) \rightarrow ( \Lbox  \Rbox C23(X) \land $ \\ 
 $ E3L3(X) \land $ \\ 
 $  \Lbox (E4L17(X) \land $ \\ 
 $ E4L28(X)))) \land $ \\ 
 $ ( \Rbox ( \Lbox E2L2(X) \land $ \\ 
 $  \Rdiamond  \Lbox  \Ldiamond  \Rbox  \Ldiamond C15(X)) \rightarrow  \Lbox  \Lbox (C20(X) \land $ \\ 
 $  \Ldiamond  \Ldiamond  \Rbox E1G14(X))) \land $ \\ 
 $ ( \Rdiamond  \Rdiamond ( \Lbox  \Ldiamond E3L7(X) \land $ \\ 
 $  \Ldiamond  \Rdiamond  \Ldiamond E2L20(X)) \rightarrow ( \Rbox  \Rbox  \Rdiamond (E5L8(X) \land $ \\ 
 $ E4G0(X)) \land $ \\ 
 $  \Rbox  \Lbox E5G9(X))) \land $ \\ 
 $ ( \Rbox  \Ldiamond ( \Ldiamond  \lnot C10(X) \land $ \\ 
 $ E3G23(X) \land $ \\ 
 $  \Rbox E4G18(X)) \rightarrow  \Rbox  \Rbox ( \lnot C2(X) \land $ \\ 
 $  \Rbox C8(X) \land $ \\ 
 $  \lnot E2G28(X))) \land $ \\ 
 $ (( \Rdiamond ( \lnot C27(X) \land $ \\ 
 $  \Lbox E5G26(X)) \land $ \\ 
 $  \Rdiamond  \Ldiamond E1L29(X)) \rightarrow (C13(X) \land $ \\ 
 $  \Ldiamond ( \Ldiamond  \Lbox C3(X) \land $ \\ 
 $ E1L22(X) \land $ \\ 
 $ E4G14(X)))) \land $ \\ 
 $ ( \Rbox  \Ldiamond  \Ldiamond  \Rbox (E2L5(X) \land $ \\ 
 $  \Ldiamond (C18(X) \land $ \\ 
 $ C3(X))) \rightarrow ( \Rbox  \lnot E5G10(X) \land $ \\ 
 $  \Ldiamond  \Ldiamond C23(X) \land $ \\ 
 $  \lnot E4L0(X))) \land $ \\ 
 $ (( \Rdiamond  \lnot E3L0(X) \land $ \\ 
 $ E4L11(X) \land $ \\ 
 $ C23(X) \land $ \\ 
 $  \Ldiamond C25(X)) \rightarrow  \Lbox  \Ldiamond ( \Lbox  \Ldiamond  \Rbox E4L21(X) \land $ \\ 
 $ C20(X) \land $ \\ 
 $ C8(X))) \land $ \\ 
 $ ( \Rbox (C16(X) \land $ \\ 
 $ C14(X) \land $ \\ 
 $  \Ldiamond  \Ldiamond  \Lbox  \lnot C24(X)) \rightarrow (E1G4(X) \land $ \\ 
 $ C15(X) \land $ \\ 
 $  \Rdiamond E5L28(X) \land $ \\ 
 $  \Ldiamond  \Rdiamond E1G26(X))) \land $ \\ 
 $ ( \Lbox ( \Lbox C22(X) \land $ \\ 
 $ E1L3(X) \land $ \\ 
 $ C21(X) \land $ \\ 
 $  \Ldiamond C25(X)) \rightarrow ( \Rdiamond (C26(X) \land $ \\ 
 $ E1G9(X)) \land $ \\ 
 $  \Lbox (E3G5(X) \land $ \\ 
 $  \Lbox C8(X)))) \land $ \\ 
 $ (( \Lbox ( \lnot E5L9(X) \land $ \\ 
 $  \Ldiamond E3L18(X)) \land $ \\ 
 $  \Rdiamond  \lnot E2L12(X)) \rightarrow (E5L19(X) \land $ \\ 
 $ E1G6(X) \land $ \\ 
 $  \Ldiamond  \Rdiamond (C3(X) \land $ \\ 
 $  \Rdiamond E3G24(X)))) \land $ \\ 
 $ (( \Rbox ( \Lbox C9(X) \land $ \\ 
 $  \Ldiamond E5L2(X)) \land $ \\ 
 $ E4L10(X) \land $ \\ 
 $ C2(X)) \rightarrow ( \Rdiamond E4G22(X) \land $ \\ 
 $  \Ldiamond  \Lbox  \Ldiamond (C1(X) \land $ \\ 
 $  \lnot C26(X)))) \land $ \\ 
 $ (( \Lbox  \Rdiamond  \lnot E3G13(X) \land $ \\ 
 $  \lnot E2G0(X) \land $ \\ 
 $  \Lbox E2L6(X)) \rightarrow  \Rdiamond ( \Rbox  \Lbox  \Rbox E3L5(X) \land $ \\ 
 $ E2G0(X) \land $ \\ 
 $  \Ldiamond E2L27(X))) \land $ \\ 
 $ ((C23(X) \land $ \\ 
 $  \Lbox  \Rbox C3(X) \land $ \\ 
 $ E5G2(X) \land $ \\ 
 $  \Lbox E2G14(X)) \rightarrow  \Rdiamond ( \Rbox  \Ldiamond  \Lbox  \lnot E1L23(X) \land $ \\ 
 $ C7(X) \land $ \\ 
 $ C2(X))) \land $ \\ 
 $ (( \lnot C6(X) \land $ \\ 
 $  \lnot E3G14(X) \land $ \\ 
 $  \Rdiamond (C25(X) \land $ \\ 
 $ E3L21(X))) \rightarrow ( \lnot E5G27(X) \land $ \\ 
 $  \Rbox C6(X) \land $ \\ 
 $  \Lbox E2G20(X) \land $ \\ 
 $ E3L24(X))) \land $ \\ 
 $ ( \Lbox  \Rbox ( \lnot C10(X) \land $ \\ 
 $  \lnot C2(X) \land $ \\ 
 $  \Rdiamond C1(X)) \rightarrow ( \Rdiamond  \Lbox (E1L9(X) \land $ \\ 
 $ C12(X)) \land $ \\ 
 $ E3G19(X) \land $ \\ 
 $  \lnot E5G28(X))) \land $ \\ 
 $ ( \Lbox  \Rbox ( \Rdiamond (C20(X) \land $ \\ 
 $  \Rbox E2L23(X)) \land $ \\ 
 $  \Ldiamond E4L3(X)) \rightarrow  \Lbox (E3G15(X) \land $ \\ 
 $  \Lbox ( \Rdiamond  \Lbox C20(X) \land $ \\ 
 $  \lnot C17(X)))) \land $ \\ 
 $ ( \Rbox  \Rdiamond ( \lnot C16(X) \land $ \\ 
 $ C12(X) \land $ \\ 
 $  \Lbox  \Rbox C15(X)) \rightarrow  \Lbox ( \Rdiamond  \Ldiamond  \Ldiamond (C18(X) \land $ \\ 
 $ C3(X)) \land $ \\ 
 $  \lnot C27(X))) \land $ \\ 
 $ ( \Lbox  \Lbox ( \Lbox  \Ldiamond C6(X) \land $ \\ 
 $  \Rdiamond (E1G19(X) \land $ \\ 
 $ E4G12(X))) \rightarrow  \Lbox ( \Rbox  \Rbox  \Rbox  \Ldiamond E4L19(X) \land $ \\ 
 $ E2L0(X) \land $ \\ 
 $ C8(X))) \land $ \\ 
 $ (E1G1(X) \rightarrow  \Rbox  \Lbox E1G1(X)) \land $ \\ 
 $ (E4L0(X) \rightarrow E3L0(X)) \land $ \\ 
 $ (E1G15(X) \rightarrow  \Rbox  \Lbox PG15) \land $ \\ 
 $ (E1G23Inv(X) \rightarrow  \Rbox  \Lbox PinvG23) \land $ \\ 
 $ (E1G16Inv(X) \rightarrow  \Rbox  \Lbox PinvG16) \land $ \\ 
 $ (E1G18Inv(X) \rightarrow  \Rbox  \Lbox E1G18Inv(X)) \land $ \\ 
 $ (E1G10Inv(X) \rightarrow  \Rbox  \Lbox E1G10Inv(X)) \land $ \\ 
 $ (E5L9(X) \rightarrow E4L9(X)) \land $ \\ 
 $ (E1L14(X) \rightarrow  \Rbox  \Lbox PL14) \land $ \\ 
 $ (E5G10(X) \rightarrow E3G10(X)) \land $ \\ 
 $ (E1L19Inv(X) \rightarrow  \Rbox  \Lbox PinvL19) \land $ \\ 
 $ (E4L3(X) \rightarrow E3L3(X)) \land $ \\ 
 $ (E1L11Inv(X) \rightarrow  \Rbox  \Lbox PinvL11) \land $ \\ 
 $ (E1G23(X) \rightarrow  \Rbox  \Lbox E1G23(X)) \land $ \\ 
 $ (E3G13(X) \rightarrow E1G13(X)) \land $ \\ 
 $ (E4G13(X) \rightarrow  \Rbox  \Lbox E4G13(X)) \land $ \\ 
 $ (E3G12(X) \rightarrow  \Rbox  \Lbox E3G12(X)) \land $ \\ 
 $ (E1L7(X) \rightarrow  \Rbox  \Lbox PL7) \land $ \\ 
 $ (E1G25Inv(X) \rightarrow  \Rbox  \Lbox PinvG25) \land $ \\ 
 $ (E1G16(X) \rightarrow  \Rbox  \Lbox PG16) \land $ \\ 
 $ (E1L9(X) \rightarrow  \Rbox  \Lbox PL9) \land $ \\ 
 $ (E1G28Inv(X) \rightarrow  \Rbox  \Lbox PinvG28) \land $ \\ 
 $ (E1G26Inv(X) \rightarrow  \Rbox  \Lbox E1G26Inv(X)) \land $ \\ 
 $ (E1G10(X) \rightarrow  \Rbox  \Lbox E1G10(X)) \land $ \\ 
 $ (E1G22(X) \rightarrow  \Rbox  \Lbox E1G22(X)) \land $ \\ 
 $ (E4G0(X) \rightarrow E2G0(X)) \land $ \\ 
 $ (E1G19(X) \rightarrow  \Rbox  \Lbox E1G19(X)) \land $ \\ 
 $ (E1G27(X) \rightarrow  \Rbox  \Lbox PG27) \land $ \\ 
 $ (E1G7(X) \rightarrow  \Rbox  \Lbox E1G7(X)) \land $ \\ 
 $ (E1G19(X) \rightarrow  \Rbox  \Lbox PG19) \land $ \\ 
 $ (E2L5(X) \rightarrow E1L5(X)) \land $ \\ 
 $ (E3G14(X) \rightarrow E2G14(X)) \land $ \\ 
 $ (E1G26Inv(X) \rightarrow  \Rbox  \Lbox PinvG26) \land $ \\ 
 $ (E2G21(X) \rightarrow  \Rbox  \Lbox E2G21(X)) \land $ \\ 
 $ (E4L25(X) \rightarrow E1L25(X)) \land $ \\ 
 $ (E4G1(X) \rightarrow  \Rbox  \Lbox E4G1(X)) \land $ \\ 
 $ (E1L26(X) \rightarrow  \Rbox  \Lbox PL26) \land $ \\ 
 $ (E2G20(X) \rightarrow E1G20(X)) \land $ \\ 
 $ (E1L12(X) \rightarrow  \Rbox  \Lbox PL12) \land $ \\ 
 $ (E1L29Inv(X) \rightarrow  \Rbox  \Lbox PinvL29) \land $ \\ 
 $ (E3G23(X) \rightarrow  \Rbox  \Lbox E3G23(X)) \land $ \\ 
 $ (E3L7(X) \rightarrow E1L7(X)) \land $ \\ 
 $ (E2G11(X) \rightarrow  \Rbox  \Lbox E2G11(X)) \land $ \\ 
 $ (E4G1(X) \rightarrow E1G1(X)) \land $ \\ 
 $ (E2L19(X) \rightarrow E1L19(X)) \land $ \\ 
 $ (E1G27Inv(X) \rightarrow  \Rbox  \Lbox E1G27Inv(X)) \land $ \\ 
 $ (E1G12Inv(X) \rightarrow  \Rbox  \Lbox PinvG12) \land $ \\ 
 $ (E5G10(X) \rightarrow  \Rbox  \Lbox E5G10(X)) \land $ \\ 
 $ (E4L9(X) \rightarrow E3L9(X)) \land $ \\ 
 $ (E1L0Inv(X) \rightarrow  \Rbox  \Lbox PinvL0) \land $ \\ 
 $ (E1G0Inv(X) \rightarrow  \Rbox  \Lbox E1G0Inv(X)) \land $ \\ 
 $ (E3G15(X) \rightarrow E1G15(X)) \land $ \\ 
 $ (E1G13Inv(X) \rightarrow  \Rbox  \Lbox PinvG13) \land $ \\ 
 $ (E3G25(X) \rightarrow E1G25(X)) \land $ \\ 
 $ (E1G28(X) \rightarrow  \Rbox  \Lbox PG28) \land $ \\ 
 $ (E1G15Inv(X) \rightarrow  \Rbox  \Lbox PinvG15) \land $ \\ 
 $ (E2L0(X) \rightarrow E1L0(X)) \land $ \\ 
 $ (E1L5Inv(X) \rightarrow  \Rbox  \Lbox PinvL5) \land $ \\ 
 $ (E1G2Inv(X) \rightarrow  \Rbox  \Lbox E1G2Inv(X)) \land $ \\ 
 $ (E1G18Inv(X) \rightarrow  \Rbox  \Lbox PinvG18) \land $ \\ 
 $ (E1G9(X) \rightarrow  \Rbox  \Lbox E1G9(X)) \land $ \\ 
 $ (E3G5(X) \rightarrow E1G5(X)) \land $ \\ 
 $ (E4G14(X) \rightarrow  \Rbox  \Lbox E4G14(X)) \land $ \\ 
 $ (E5L15(X) \rightarrow E1L15(X)) \land $ \\ 
 $ (E1L0(X) \rightarrow  \Rbox  \Lbox PL0) \land $ \\ 
 $ (E2L3(X) \rightarrow E1L3(X)) \land $ \\ 
 $ (E2G0(X) \rightarrow  \Rbox  \Lbox E2G0(X)) \land $ \\ 
 $ (E2G21(X) \rightarrow E1G21(X)) \land $ \\ 
 $ (E1L5(X) \rightarrow  \Rbox  \Lbox PL5) \land $ \\ 
 $ (E1G15Inv(X) \rightarrow  \Rbox  \Lbox E1G15Inv(X)) \land $ \\ 
 $ (E1G13Inv(X) \rightarrow  \Rbox  \Lbox E1G13Inv(X)) \land $ \\ 
 $ (E1G16(X) \rightarrow  \Rbox  \Lbox E1G16(X)) \land $ \\ 
 $ (E2L6(X) \rightarrow E1L6(X)) \land $ \\ 
 $ (E1G14(X) \rightarrow  \Rbox  \Lbox E1G14(X)) \land $ \\ 
 $ (E1G6(X) \rightarrow  \Rbox  \Lbox PG6) \land $ \\ 
 $ (E4L11(X) \rightarrow E1L11(X)) \land $ \\ 
 $ (E1G4Inv(X) \rightarrow  \Rbox  \Lbox PinvG4) \land $ \\ 
 $ (E3G13(X) \rightarrow  \Rbox  \Lbox E3G13(X)) \land $ \\ 
 $ (E1L15Inv(X) \rightarrow  \Rbox  \Lbox PinvL15) \land $ \\ 
 $ (E1L2(X) \rightarrow  \Rbox  \Lbox PL2) \land $ \\ 
 $ (E1G12(X) \rightarrow  \Rbox  \Lbox E1G12(X)) \land $ \\ 
 $ (E1G24Inv(X) \rightarrow  \Rbox  \Lbox PinvG24) \land $ \\ 
 $ (E1G4(X) \rightarrow  \Rbox  \Lbox PG4) \land $ \\ 
 $ (E1G2(X) \rightarrow  \Rbox  \Lbox PG2) \land $ \\ 
 $ (E3G2(X) \rightarrow E1G2(X)) \land $ \\ 
 $ (E1G6Inv(X) \rightarrow  \Rbox  \Lbox PinvG6) \land $ \\ 
 $ (E1G28Inv(X) \rightarrow  \Rbox  \Lbox E1G28Inv(X)) \land $ \\ 
 $ (E3G19(X) \rightarrow  \Rbox  \Lbox E3G19(X)) \land $ \\ 
 $ (E1L10(X) \rightarrow  \Rbox  \Lbox PL10) \land $ \\ 
 $ (E1L17Inv(X) \rightarrow  \Rbox  \Lbox PinvL17) \land $ \\ 
 $ (E1G4Inv(X) \rightarrow  \Rbox  \Lbox E1G4Inv(X)) \land $ \\ 
 $ (E5G28(X) \rightarrow E4G28(X)) \land $ \\ 
 $ (E1G7Inv(X) \rightarrow  \Rbox  \Lbox PinvG7) \land $ \\ 
 $ (E1L21Inv(X) \rightarrow  \Rbox  \Lbox PinvL21) \land $ \\ 
 $ (E1L24Inv(X) \rightarrow  \Rbox  \Lbox PinvL24) \land $ \\ 
 $ (E3L0(X) \rightarrow E2L0(X)) \land $ \\ 
 $ (E2L23(X) \rightarrow E1L23(X)) \land $ \\ 
 $ (E1L21(X) \rightarrow  \Rbox  \Lbox PL21) \land $ \\ 
 $ (E1G14Inv(X) \rightarrow  \Rbox  \Lbox PinvG14) \land $ \\ 
 $ (E1G21(X) \rightarrow  \Rbox  \Lbox E1G21(X)) \land $ \\ 
 $ (E1G20Inv(X) \rightarrow  \Rbox  \Lbox E1G20Inv(X)) \land $ \\ 
 $ (E1G28(X) \rightarrow  \Rbox  \Lbox E1G28(X)) \land $ \\ 
 $ (E5G25(X) \rightarrow  \Rbox  \Lbox E5G25(X)) \land $ \\ 
 $ (E1G13(X) \rightarrow  \Rbox  \Lbox E1G13(X)) \land $ \\ 
 $ (E4L20(X) \rightarrow E3L20(X)) \land $ \\ 
 $ (E5L19(X) \rightarrow E4L19(X)) \land $ \\ 
 $ (E5G27(X) \rightarrow  \Rbox  \Lbox E5G27(X)) \land $ \\ 
 $ (E1G9Inv(X) \rightarrow  \Rbox  \Lbox E1G9Inv(X)) \land $ \\ 
 $ (E1G12Inv(X) \rightarrow  \Rbox  \Lbox E1G12Inv(X)) \land $ \\ 
 $ (E5G26(X) \rightarrow E1G26(X)) \land $ \\ 
 $ (E2L2(X) \rightarrow E1L2(X)) \land $ \\ 
 $ (E1L29(X) \rightarrow  \Rbox  \Lbox PL29) \land $ \\ 
 $ (E1L15(X) \rightarrow  \Rbox  \Lbox PL15) \land $ \\ 
 $ (E1G18(X) \rightarrow  \Rbox  \Lbox E1G18(X)) \land $ \\ 
 $ (E5G2(X) \rightarrow E3G2(X)) \land $ \\ 
 $ (E1G11(X) \rightarrow  \Rbox  \Lbox E1G11(X)) \land $ \\ 
 $ (E1L7Inv(X) \rightarrow  \Rbox  \Lbox PinvL7) \land $ \\ 
 $ (E2G0(X) \rightarrow E1G0(X)) \land $ \\ 
 $ (E1G1(X) \rightarrow  \Rbox  \Lbox PG1) \land $ \\ 
 $ (E4L19(X) \rightarrow E3L19(X)) \land $ \\ 
 $ (E1L27Inv(X) \rightarrow  \Rbox  \Lbox PinvL27) \land $ \\ 
 $ (E1L8(X) \rightarrow  \Rbox  \Lbox PL8) \land $ \\ 
 $ (E4L10(X) \rightarrow E1L10(X)) \land $ \\ 
 $ (E4G22(X) \rightarrow  \Rbox  \Lbox E4G22(X)) \land $ \\ 
 $ (E1G14Inv(X) \rightarrow  \Rbox  \Lbox E1G14Inv(X)) \land $ \\ 
 $ (E1L17(X) \rightarrow  \Rbox  \Lbox PL17) \land $ \\ 
 $ (E1G22(X) \rightarrow  \Rbox  \Lbox PG22) \land $ \\ 
 $ (E5G18(X) \rightarrow  \Rbox  \Lbox E5G18(X)) \land $ \\ 
 $ (E1L23Inv(X) \rightarrow  \Rbox  \Lbox PinvL23) \land $ \\ 
 $ (E1G7Inv(X) \rightarrow  \Rbox  \Lbox E1G7Inv(X)) \land $ \\ 
 $ (E1G1Inv(X) \rightarrow  \Rbox  \Lbox E1G1Inv(X)) \land $ \\ 
 $ (E1L28(X) \rightarrow  \Rbox  \Lbox PL28) \land $ \\ 
 $ (E4G22(X) \rightarrow E1G22(X)) \land $ \\ 
 $ (E5L14(X) \rightarrow E2L14(X)) \land $ \\ 
 $ (E3G23(X) \rightarrow E1G23(X)) \land $ \\ 
 $ (E1G25Inv(X) \rightarrow  \Rbox  \Lbox E1G25Inv(X)) \land $ \\ 
 $ (E1L19(X) \rightarrow  \Rbox  \Lbox PL19) \land $ \\ 
 $ (E3L9(X) \rightarrow E1L9(X)) \land $ \\ 
 $ (E1L11(X) \rightarrow  \Rbox  \Lbox PL11) \land $ \\ 
 $ (E3L5(X) \rightarrow E2L5(X)) \land $ \\ 
 $ (E1G24(X) \rightarrow  \Rbox  \Lbox E1G24(X)) \land $ \\ 
 $ (E1G5Inv(X) \rightarrow  \Rbox  \Lbox E1G5Inv(X)) \land $ \\ 
 $ (E3L28(X) \rightarrow E1L28(X)) \land $ \\ 
 $ (E1L9Inv(X) \rightarrow  \Rbox  \Lbox PinvL9) \land $ \\ 
 $ (E1L26Inv(X) \rightarrow  \Rbox  \Lbox PinvL26) \land $ \\ 
 $ (E3G2(X) \rightarrow  \Rbox  \Lbox E3G2(X)) \land $ \\ 
 $ (E1G26(X) \rightarrow  \Rbox  \Lbox PG26) \land $ \\ 
 $ (E3G24(X) \rightarrow  \Rbox  \Lbox E3G24(X)) \land $ \\ 
 $ (E2G28(X) \rightarrow E1G28(X)) \land $ \\ 
 $ (E1G11(X) \rightarrow  \Rbox  \Lbox PG11) \land $ \\ 
 $ (E3L21(X) \rightarrow E1L21(X)) \land $ \\ 
 $ (E1G5(X) \rightarrow  \Rbox  \Lbox PG5) \land $ \\ 
 $ (E2L14(X) \rightarrow E1L14(X)) \land $ \\ 
 $ (E1G24Inv(X) \rightarrow  \Rbox  \Lbox E1G24Inv(X)) \land $ \\ 
 $ (E3L24(X) \rightarrow E1L24(X)) \land $ \\ 
 $ (E2L8(X) \rightarrow E1L8(X)) \land $ \\ 
 $ (E1G21(X) \rightarrow  \Rbox  \Lbox PG21) \land $ \\ 
 $ (E1G21Inv(X) \rightarrow  \Rbox  \Lbox E1G21Inv(X)) \land $ \\ 
 $ (E5L17(X) \rightarrow E4L17(X)) \land $ \\ 
 $ (E1L27(X) \rightarrow  \Rbox  \Lbox PL27) \land $ \\ 
 $ (E1G19Inv(X) \rightarrow  \Rbox  \Lbox E1G19Inv(X)) \land $ \\ 
 $ (E1L14Inv(X) \rightarrow  \Rbox  \Lbox PinvL14) \land $ \\ 
 $ (E5G7(X) \rightarrow E1G7(X)) \land $ \\ 
 $ (E4G18(X) \rightarrow  \Rbox  \Lbox E4G18(X)) \land $ \\ 
 $ (E2L12(X) \rightarrow E1L12(X)) \land $ \\ 
 $ (E1G25(X) \rightarrow  \Rbox  \Lbox E1G25(X)) \land $ \\ 
 $ (E1L3Inv(X) \rightarrow  \Rbox  \Lbox PinvL3) \land $ \\ 
 $ (E1G2(X) \rightarrow  \Rbox  \Lbox E1G2(X)) \land $ \\ 
 $ (E2G11(X) \rightarrow E1G11(X)) \land $ \\ 
 $ (E3G5(X) \rightarrow  \Rbox  \Lbox E3G5(X)) \land $ \\ 
 $ (E1G21Inv(X) \rightarrow  \Rbox  \Lbox PinvG21) \land $ \\ 
 $ (E2G14(X) \rightarrow  \Rbox  \Lbox E2G14(X)) \land $ \\ 
 $ (E4G28(X) \rightarrow E2G28(X)) \land $ \\ 
 $ (E4G28(X) \rightarrow  \Rbox  \Lbox E4G28(X)) \land $ \\ 
 $ (E1G0(X) \rightarrow  \Rbox  \Lbox E1G0(X)) \land $ \\ 
 $ (E1G11Inv(X) \rightarrow  \Rbox  \Lbox PinvG11) \land $ \\ 
 $ (E1G5Inv(X) \rightarrow  \Rbox  \Lbox PinvG5) \land $ \\ 
 $ (E5G2(X) \rightarrow  \Rbox  \Lbox E5G2(X)) \land $ \\ 
 $ (E4G12(X) \rightarrow E3G12(X)) \land $ \\ 
 $ (E3G19(X) \rightarrow E1G19(X)) \land $ \\ 
 $ (E1G15(X) \rightarrow  \Rbox  \Lbox E1G15(X)) \land $ \\ 
 $ (E2G28(X) \rightarrow  \Rbox  \Lbox E2G28(X)) \land $ \\ 
 $ (E4G11(X) \rightarrow E2G11(X)) \land $ \\ 
 $ (E4G14(X) \rightarrow E3G14(X)) \land $ \\ 
 $ (E1G24(X) \rightarrow  \Rbox  \Lbox PG24) \land $ \\ 
 $ (E3L3(X) \rightarrow E2L3(X)) \land $ \\ 
 $ (E1L25(X) \rightarrow  \Rbox  \Lbox PL25) \land $ \\ 
 $ (E3G10(X) \rightarrow  \Rbox  \Lbox E3G10(X)) \land $ \\ 
 $ (E4G13(X) \rightarrow E3G13(X)) \land $ \\ 
 $ (E1G0Inv(X) \rightarrow  \Rbox  \Lbox PinvG0) \land $ \\ 
 $ (E1G25(X) \rightarrow  \Rbox  \Lbox PG25) \land $ \\ 
 $ (E3L19(X) \rightarrow E2L19(X)) \land $ \\ 
 $ (E1G13(X) \rightarrow  \Rbox  \Lbox PG13) \land $ \\ 
 $ (E4G18(X) \rightarrow E1G18(X)) \land $ \\ 
 $ (E1L28Inv(X) \rightarrow  \Rbox  \Lbox PinvL28) \land $ \\ 
 $ (E1G0(X) \rightarrow  \Rbox  \Lbox PG0) \land $ \\ 
 $ (E4L28(X) \rightarrow E3L28(X)) \land $ \\ 
 $ (E3L18(X) \rightarrow E1L18(X)) \land $ \\ 
 $ (E3G15(X) \rightarrow  \Rbox  \Lbox E3G15(X)) \land $ \\ 
 $ (E4G12(X) \rightarrow  \Rbox  \Lbox E4G12(X)) \land $ \\ 
 $ (E4L21(X) \rightarrow E3L21(X)) \land $ \\ 
 $ (E4L17(X) \rightarrow E1L17(X)) \land $ \\ 
 $ (E1L6Inv(X) \rightarrow  \Rbox  \Lbox PinvL6) \land $ \\ 
 $ (E2L20(X) \rightarrow E1L20(X)) \land $ \\ 
 $ (E1L13(X) \rightarrow  \Rbox  \Lbox PL13) \land $ \\ 
 $ (E1G9Inv(X) \rightarrow  \Rbox  \Lbox PinvG9) \land $ \\ 
 $ (E3L20(X) \rightarrow E2L20(X)) \land $ \\ 
 $ (E5G26(X) \rightarrow  \Rbox  \Lbox E5G26(X)) \land $ \\ 
 $ (E5L8(X) \rightarrow E2L8(X)) \land $ \\ 
 $ (E5L18(X) \rightarrow E3L18(X)) \land $ \\ 
 $ (E1L12Inv(X) \rightarrow  \Rbox  \Lbox PinvL12) \land $ \\ 
 $ (E5G7(X) \rightarrow  \Rbox  \Lbox E5G7(X)) \land $ \\ 
 $ (E1G10Inv(X) \rightarrow  \Rbox  \Lbox PinvG10) \land $ \\ 
 $ (E3G14(X) \rightarrow  \Rbox  \Lbox E3G14(X)) \land $ \\ 
 $ (E3G10(X) \rightarrow E1G10(X)) \land $ \\ 
 $ (E3G24(X) \rightarrow E1G24(X)) \land $ \\ 
 $ (E1L8Inv(X) \rightarrow  \Rbox  \Lbox PinvL8) \land $ \\ 
 $ (E1G1Inv(X) \rightarrow  \Rbox  \Lbox PinvG1) \land $ \\ 
 $ (E1L18(X) \rightarrow  \Rbox  \Lbox PL18) \land $ \\ 
 $ (E1L18Inv(X) \rightarrow  \Rbox  \Lbox PinvL18) \land $ \\ 
 $ (E1L23(X) \rightarrow  \Rbox  \Lbox PL23) \land $ \\ 
 $ (E1G4(X) \rightarrow  \Rbox  \Lbox E1G4(X)) \land $ \\ 
 $ (E1G19Inv(X) \rightarrow  \Rbox  \Lbox PinvG19) \land $ \\ 
 $ (E1G16Inv(X) \rightarrow  \Rbox  \Lbox E1G16Inv(X)) \land $ \\ 
 $ (E5G27(X) \rightarrow E1G27(X)) \land $ \\ 
 $ (E1G6Inv(X) \rightarrow  \Rbox  \Lbox E1G6Inv(X)) \land $ \\ 
 $ (E1G11Inv(X) \rightarrow  \Rbox  \Lbox E1G11Inv(X)) \land $ \\ 
 $ (E1G20Inv(X) \rightarrow  \Rbox  \Lbox PinvG20) \land $ \\ 
 $ (E1G5(X) \rightarrow  \Rbox  \Lbox E1G5(X)) \land $ \\ 
 $ (E1L24(X) \rightarrow  \Rbox  \Lbox PL24) \land $ \\ 
 $ (E2L27(X) \rightarrow E1L27(X)) \land $ \\ 
 $ (E1G23(X) \rightarrow  \Rbox  \Lbox PG23) \land $ \\ 
 $ (E3G12(X) \rightarrow E1G12(X)) \land $ \\ 
 $ (E1L10Inv(X) \rightarrow  \Rbox  \Lbox PinvL10) \land $ \\ 
 $ (E1L2Inv(X) \rightarrow  \Rbox  \Lbox PinvL2) \land $ \\ 
 $ (E1G27Inv(X) \rightarrow  \Rbox  \Lbox PinvG27) \land $ \\ 
 $ (E1G7(X) \rightarrow  \Rbox  \Lbox PG7) \land $ \\ 
 $ (E4G11(X) \rightarrow  \Rbox  \Lbox E4G11(X)) \land $ \\ 
 $ (E1L20(X) \rightarrow  \Rbox  \Lbox PL20) \land $ \\ 
 $ (E5G18(X) \rightarrow E4G18(X)) \land $ \\ 
 $ (E1G23Inv(X) \rightarrow  \Rbox  \Lbox E1G23Inv(X)) \land $ \\ 
 $ (E4L26(X) \rightarrow E1L26(X)) \land $ \\ 
 $ (E2G14(X) \rightarrow E1G14(X)) \land $ \\ 
 $ (E1G9(X) \rightarrow  \Rbox  \Lbox PG9) \land $ \\ 
 $ (E1G22Inv(X) \rightarrow  \Rbox  \Lbox E1G22Inv(X)) \land $ \\ 
 $ (E1L25Inv(X) \rightarrow  \Rbox  \Lbox PinvL25) \land $ \\ 
 $ (E1L22Inv(X) \rightarrow  \Rbox  \Lbox PinvL22) \land $ \\ 
 $ (E1L22(X) \rightarrow  \Rbox  \Lbox PL22) \land $ \\ 
 $ (E5L28(X) \rightarrow E4L28(X)) \land $ \\ 
 $ (E1G2Inv(X) \rightarrow  \Rbox  \Lbox PinvG2) \land $ \\ 
 $ (E1G6(X) \rightarrow  \Rbox  \Lbox E1G6(X)) \land $ \\ 
 $ (E1G20(X) \rightarrow  \Rbox  \Lbox PG20) \land $ \\ 
 $ (E1G20(X) \rightarrow  \Rbox  \Lbox E1G20(X)) \land $ \\ 
 $ (E5L2(X) \rightarrow E2L2(X)) \land $ \\ 
 $ (E1L20Inv(X) \rightarrow  \Rbox  \Lbox PinvL20) \land $ \\ 
 $ (E2G20(X) \rightarrow  \Rbox  \Lbox E2G20(X)) \land $ \\ 
 $ (E1L13Inv(X) \rightarrow  \Rbox  \Lbox PinvL13) \land $ \\ 
 $ (E5G25(X) \rightarrow E3G25(X)) \land $ \\ 
 $ (E1G26(X) \rightarrow  \Rbox  \Lbox E1G26(X)) \land $ \\ 
 $ (E1G10(X) \rightarrow  \Rbox  \Lbox PG10) \land $ \\ 
 $ (E1L6(X) \rightarrow  \Rbox  \Lbox PL6) \land $ \\ 
 $ (E1G14(X) \rightarrow  \Rbox  \Lbox PG14) \land $ \\ 
 $ (E5G9(X) \rightarrow E1G9(X)) \land $ \\ 
 $ (E4G0(X) \rightarrow  \Rbox  \Lbox E4G0(X)) \land $ \\ 
 $ (E5G9(X) \rightarrow  \Rbox  \Lbox E5G9(X)) \land $ \\ 
 $ (E1G22Inv(X) \rightarrow  \Rbox  \Lbox PinvG22) \land $ \\ 
 $ (E3G25(X) \rightarrow  \Rbox  \Lbox E3G25(X)) \land $ \\ 
 $ (E1L3(X) \rightarrow  \Rbox  \Lbox PL3) \land $ \\ 
 $ (E1G12(X) \rightarrow  \Rbox  \Lbox PG12) \land $ \\ 
 $ (E1G18(X) \rightarrow  \Rbox  \Lbox PG18) \land $ \\ 
 $ (E1G27(X) \rightarrow  \Rbox  \Lbox E1G27(X)) \land $ \\ 
 $ (E5G28(X) \rightarrow  \Rbox  \Lbox E5G28(X))) \land $ \\ 
 $ (PG18 \rightarrow E1G18Inv(dG18Inv)) \land $ \\ 
 $ (PinvL23 \rightarrow E1L23(dL23)) \land $ \\ 
 $ (PinvG9 \rightarrow E1G9(dG9)) \land $ \\ 
 $ (PL24 \rightarrow E1L24Inv(dL24Inv)) \land $ \\ 
 $ (PG13 \rightarrow E1G13Inv(dG13Inv)) \land $ \\ 
 $ (PG5 \rightarrow E1G5Inv(dG5Inv)) \land $ \\ 
 $ (PG4 \rightarrow E1G4Inv(dG4Inv)) \land $ \\ 
 $ (PL28 \rightarrow E1L28Inv(dL28Inv)) \land $ \\ 
 $ (PinvL7 \rightarrow E1L7(dL7)) \land $ \\ 
 $ (PinvG19 \rightarrow E1G19(dG19)) \land $ \\ 
 $ (PL15 \rightarrow E1L15Inv(dL15Inv)) \land $ \\ 
 $ (PinvG21 \rightarrow E1G21(dG21)) \land $ \\ 
 $ (PG12 \rightarrow E1G12Inv(dG12Inv)) \land $ \\ 
 $ (PG20 \rightarrow E1G20Inv(dG20Inv)) \land $ \\ 
 $ (PL6 \rightarrow E1L6Inv(dL6Inv)) \land $ \\ 
 $ (PL13 \rightarrow E1L13Inv(dL13Inv)) \land $ \\ 
 $ (PL18 \rightarrow E1L18Inv(dL18Inv)) \land $ \\ 
 $ (PG6 \rightarrow E1G6Inv(dG6Inv)) \land $ \\ 
 $ (PL3 \rightarrow E1L3Inv(dL3Inv)) \land $ \\ 
 $ (PinvL29 \rightarrow E1L29(dL29)) \land $ \\ 
 $ (PG22 \rightarrow E1G22Inv(dG22Inv)) \land $ \\ 
 $ (PG28 \rightarrow E1G28Inv(dG28Inv)) \land $ \\ 
 $ (PinvG11 \rightarrow E1G11(dG11)) \land $ \\ 
 $ (PinvG22 \rightarrow E1G22(dG22)) \land $ \\ 
 $ (PinvG12 \rightarrow E1G12(dG12)) \land $ \\ 
 $ (PL8 \rightarrow E1L8Inv(dL8Inv)) \land $ \\ 
 $ (PG14 \rightarrow E1G14Inv(dG14Inv)) \land $ \\ 
 $ (PinvL3 \rightarrow E1L3(dL3)) \land $ \\ 
 $ (PinvG15 \rightarrow E1G15(dG15)) \land $ \\ 
 $ (PG21 \rightarrow E1G21Inv(dG21Inv)) \land $ \\ 
 $ (PL19 \rightarrow E1L19Inv(dL19Inv)) \land $ \\ 
 $ (PinvL18 \rightarrow E1L18(dL18)) \land $ \\ 
 $ (PG15 \rightarrow E1G15Inv(dG15Inv)) \land $ \\ 
 $ (PL25 \rightarrow E1L25Inv(dL25Inv)) \land $ \\ 
 $ (PL0 \rightarrow E1L0Inv(dL0Inv)) \land $ \\ 
 $ (PG7 \rightarrow E1G7Inv(dG7Inv)) \land $ \\ 
 $ (PG25 \rightarrow E1G25Inv(dG25Inv)) \land $ \\ 
 $ (PinvG20 \rightarrow E1G20(dG20)) \land $ \\ 
 $ (PG23 \rightarrow E1G23Inv(dG23Inv)) \land $ \\ 
 $ (PG27 \rightarrow E1G27Inv(dG27Inv)) \land $ \\ 
 $ (PL2 \rightarrow E1L2Inv(dL2Inv)) \land $ \\ 
 $ (PL10 \rightarrow E1L10Inv(dL10Inv)) \land $ \\ 
 $ (PL17 \rightarrow E1L17Inv(dL17Inv)) \land $ \\ 
 $ (PinvL13 \rightarrow E1L13(dL13)) \land $ \\ 
 $ (PG1 \rightarrow E1G1Inv(dG1Inv)) \land $ \\ 
 $ (PinvL15 \rightarrow E1L15(dL15)) \land $ \\ 
 $ (PinvG2 \rightarrow E1G2(dG2)) \land $ \\ 
 $ (PL5 \rightarrow E1L5Inv(dL5Inv)) \land $ \\ 
 $ (PG9 \rightarrow E1G9Inv(dG9Inv)) \land $ \\ 
 $ (PinvG13 \rightarrow E1G13(dG13)) \land $ \\ 
 $ (PinvG7 \rightarrow E1G7(dG7)) \land $ \\ 
 $ (PinvL6 \rightarrow E1L6(dL6)) \land $ \\ 
 $ (PinvL10 \rightarrow E1L10(dL10)) \land $ \\ 
 $ (PinvG0 \rightarrow E1G0(dG0)) \land $ \\ 
 $ (PL14 \rightarrow E1L14Inv(dL14Inv)) \land $ \\ 
 $ (PL23 \rightarrow E1L23Inv(dL23Inv)) \land $ \\ 
 $ (PinvL22 \rightarrow E1L22(dL22)) \land $ \\ 
 $ (PinvL9 \rightarrow E1L9(dL9)) \land $ \\ 
 $ (PG24 \rightarrow E1G24Inv(dG24Inv)) \land $ \\ 
 $ (PinvG5 \rightarrow E1G5(dG5)) \land $ \\ 
 $ (PinvL0 \rightarrow E1L0(dL0)) \land $ \\ 
 $ (PinvL12 \rightarrow E1L12(dL12)) \land $ \\ 
 $ (PG16 \rightarrow E1G16Inv(dG16Inv)) \land $ \\ 
 $ (PL20 \rightarrow E1L20Inv(dL20Inv)) \land $ \\ 
 $ (PinvG16 \rightarrow E1G16(dG16)) \land $ \\ 
 $ (PL9 \rightarrow E1L9Inv(dL9Inv)) \land $ \\ 
 $ (PinvL25 \rightarrow E1L25(dL25)) \land $ \\ 
 $ (PinvL5 \rightarrow E1L5(dL5)) \land $ \\ 
 $ (PinvG24 \rightarrow E1G24(dG24)) \land $ \\ 
 $ (PG2 \rightarrow E1G2Inv(dG2Inv)) \land $ \\ 
 $ (PinvL21 \rightarrow E1L21(dL21)) \land $ \\ 
 $ (PinvL20 \rightarrow E1L20(dL20)) \land $ \\ 
 $ (PG26 \rightarrow E1G26Inv(dG26Inv)) \land $ \\ 
 $ (PL7 \rightarrow E1L7Inv(dL7Inv)) \land $ \\ 
 $ (PinvL26 \rightarrow E1L26(dL26)) \land $ \\ 
 $ (PinvL27 \rightarrow E1L27(dL27)) \land $ \\ 
 $ (PL22 \rightarrow E1L22Inv(dL22Inv)) \land $ \\ 
 $ (PinvG1 \rightarrow E1G1(dG1)) \land $ \\ 
 $ (PL12 \rightarrow E1L12Inv(dL12Inv)) \land $ \\ 
 $ (PinvL8 \rightarrow E1L8(dL8)) \land $ \\ 
 $ (PinvG27 \rightarrow E1G27(dG27)) \land $ \\ 
 $ (PinvG10 \rightarrow E1G10(dG10)) \land $ \\ 
 $ (PL11 \rightarrow E1L11Inv(dL11Inv)) \land $ \\ 
 $ (PG19 \rightarrow E1G19Inv(dG19Inv)) \land $ \\ 
 $ (PinvL17 \rightarrow E1L17(dL17)) \land $ \\ 
 $ (PinvL28 \rightarrow E1L28(dL28)) \land $ \\ 
 $ (PinvG14 \rightarrow E1G14(dG14)) \land $ \\ 
 $ (PG11 \rightarrow E1G11Inv(dG11Inv)) \land $ \\ 
 $ (PinvL11 \rightarrow E1L11(dL11)) \land $ \\ 
 $ (PL26 \rightarrow E1L26Inv(dL26Inv)) \land $ \\ 
 $ (PinvG28 \rightarrow E1G28(dG28)) \land $ \\ 
 $ (PinvG26 \rightarrow E1G26(dG26)) \land $ \\ 
 $ (PinvL2 \rightarrow E1L2(dL2)) \land $ \\ 
 $ (PinvG23 \rightarrow E1G23(dG23)) \land $ \\ 
 $ (PG0 \rightarrow E1G0Inv(dG0Inv)) \land $ \\ 
 $ (PL27 \rightarrow E1L27Inv(dL27Inv)) \land $ \\ 
 $ (PG10 \rightarrow E1G10Inv(dG10Inv)) \land $ \\ 
 $ (PinvG25 \rightarrow E1G25(dG25)) \land $ \\ 
 $ (PinvG4 \rightarrow E1G4(dG4)) \land $ \\ 
 $ (PinvL19 \rightarrow E1L19(dL19)) \land $ \\ 
 $ (PL29 \rightarrow E1L29Inv(dL29Inv)) \land $ \\ 
 $ (PinvL14 \rightarrow E1L14(dL14)) \land $ \\ 
 $ (PL21 \rightarrow E1L21Inv(dL21Inv)) \land $ \\ 
 $ (PinvL24 \rightarrow E1L24(dL24)) \land $ \\ 
 $ (PinvG18 \rightarrow E1G18(dG18)) \land $ \\ 
 $ (PinvG6 \rightarrow E1G6(dG6)))$ 
\end{document}