\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 (((E2G12(X) \land $ \\ 
 $ E1L15(X) \land $ \\ 
 $ C19(X)) \rightarrow ( \Rbox C38(X) \land $ \\ 
 $  \Rdiamond E1G14(X))) \land $ \\ 
 $ ( \Rbox  \Rdiamond (C39(X) \land $ \\ 
 $ C34(X)) \rightarrow  \Rdiamond  \Rbox  \Rdiamond  \Rbox C45(X)) \land $ \\ 
 $ ( \Rbox (C1(X) \land $ \\ 
 $  \Rnext E2L43(X)) \rightarrow (C36(X) \land $ \\ 
 $  \Rdiamond  \Rnext C29(X))) \land $ \\ 
 $ ( \Rdiamond  \Rdiamond  \Rbox  \Rnext E3G3(X) \rightarrow (C15(X) \land $ \\ 
 $  \Rdiamond  \Rbox E2L2(X))) \land $ \\ 
 $ ( \Rdiamond  \Rdiamond (C38(X) \land $ \\ 
 $ E1L41(X)) \rightarrow  \Rdiamond (E3G47(X) \land $ \\ 
 $  \Rdiamond C36(X))) \land $ \\ 
 $ ( \Rdiamond  \Rbox C39(X) \rightarrow  \Rbox  \Rbox (C29(X) \land $ \\ 
 $ E2G23(X))) \land $ \\ 
 $ (( \Rdiamond E3G26(X) \land $ \\ 
 $  \Rnext C7(X)) \rightarrow (C48(X) \land $ \\ 
 $  \Rdiamond  \Rnext C30(X))) \land $ \\ 
 $ ( \Rdiamond  \Rbox  \Rdiamond  \Rnext E2L19(X) \rightarrow (E1G29(X) \land $ \\ 
 $  \Rbox  \Rnext C44(X))) \land $ \\ 
 $ (( \Rbox C8(X) \land $ \\ 
 $  \Rnext C18(X)) \rightarrow  \Rdiamond  \Rbox (E1G34(X) \land $ \\ 
 $ C9(X))) \land $ \\ 
 $ ((C3(X) \land $ \\ 
 $  \Rbox  \Rnext C19(X)) \rightarrow  \Rdiamond  \Rbox (C23(X) \land $ \\ 
 $ C8(X))) \land $ \\ 
 $ (( \Rnext C26(X) \land $ \\ 
 $  \Rnext E2G0(X)) \rightarrow ( \Rdiamond E3G28(X) \land $ \\ 
 $  \Rdiamond E3G34(X))) \land $ \\ 
 $ ( \Rbox (C46(X) \land $ \\ 
 $  \Rnext C45(X)) \rightarrow  \Rdiamond (E3L47(X) \land $ \\ 
 $  \Rnext C40(X))) \land $ \\ 
 $ ( \Rbox  \Rdiamond (C45(X) \land $ \\ 
 $ C27(X)) \rightarrow (E3L41(X) \land $ \\ 
 $ E3G3(X) \land $ \\ 
 $ C32(X))) \land $ \\ 
 $ ( \Rdiamond (E1G3(X) \land $ \\ 
 $  \Rbox E1G30(X)) \rightarrow ( \Rbox C31(X) \land $ \\ 
 $  \Rnext E3L21(X))) \land $ \\ 
 $ ( \Rbox  \Rdiamond (E1G36(X) \land $ \\ 
 $ C5(X)) \rightarrow (E3G31(X) \land $ \\ 
 $  \Rbox  \Rdiamond C41(X))) \land $ \\ 
 $ ((E1L38(X) \land $ \\ 
 $  \Rbox  \Rnext C19(X)) \rightarrow (C21(X) \land $ \\ 
 $  \Rbox  \Rnext C22(X))) \land $ \\ 
 $ ((C45(X) \land $ \\ 
 $ C20(X) \land $ \\ 
 $ E2G45(X)) \rightarrow  \Rdiamond (C31(X) \land $ \\ 
 $  \Rdiamond E1G47(X))) \land $ \\ 
 $ (( \Rdiamond E1L1(X) \land $ \\ 
 $  \Rdiamond E1G39(X)) \rightarrow (E1L22(X) \land $ \\ 
 $  \Rdiamond  \Rbox C2(X))) \land $ \\ 
 $ ( \Rdiamond  \Rbox (E2G1(X) \land $ \\ 
 $ E3L38(X)) \rightarrow ( \Rbox C40(X) \land $ \\ 
 $  \Rdiamond C1(X))) \land $ \\ 
 $ ((E1L0(X) \land $ \\ 
 $ C17(X) \land $ \\ 
 $ C35(X)) \rightarrow  \Rbox (E2G20(X) \land $ \\ 
 $  \Rdiamond E3L9(X))) \land $ \\ 
 $ ((E3L15(X) \land $ \\ 
 $  \Rdiamond  \Rbox C5(X)) \rightarrow ( \Rnext C38(X) \land $ \\ 
 $  \Rnext C17(X))) \land $ \\ 
 $ ((C3(X) \land $ \\ 
 $  \Rdiamond  \Rdiamond C17(X)) \rightarrow ( \Rdiamond C26(X) \land $ \\ 
 $  \Rnext E2G38(X))) \land $ \\ 
 $ ( \Rbox (C4(X) \land $ \\ 
 $  \Rbox E1G16(X)) \rightarrow (C38(X) \land $ \\ 
 $ E1L27(X) \land $ \\ 
 $ E1G18(X))) \land $ \\ 
 $ ( \Rdiamond (E1L15(X) \land $ \\ 
 $  \Rnext C22(X)) \rightarrow ( \Rdiamond C4(X) \land $ \\ 
 $  \Rdiamond E1L17(X))) \land $ \\ 
 $ (( \Rnext E3L2(X) \land $ \\ 
 $  \Rdiamond C18(X)) \rightarrow  \Rbox (C11(X) \land $ \\ 
 $  \Rdiamond C7(X))) \land $ \\ 
 $ ( \Rdiamond  \Rdiamond  \Rdiamond  \Rdiamond C30(X) \rightarrow  \Rdiamond  \Rbox (C20(X) \land $ \\ 
 $ E2G32(X))) \land $ \\ 
 $ ((E3L10(X) \land $ \\ 
 $ C32(X) \land $ \\ 
 $ C3(X)) \rightarrow (E1G2(X) \land $ \\ 
 $ E1G23(X) \land $ \\ 
 $ E1L47(X))) \land $ \\ 
 $ (( \Rnext C24(X) \land $ \\ 
 $  \Rnext C14(X)) \rightarrow  \Rdiamond (E1L5(X) \land $ \\ 
 $  \Rnext E1G34(X))) \land $ \\ 
 $ ( \Rbox (E1L0(X) \land $ \\ 
 $  \Rdiamond C40(X)) \rightarrow (C5(X) \land $ \\ 
 $  \Rdiamond  \Rnext E3L45(X))) \land $ \\ 
 $ (( \Rdiamond C2(X) \land $ \\ 
 $  \Rnext E2L41(X)) \rightarrow  \Rdiamond (E1G28(X) \land $ \\ 
 $  \Rdiamond C30(X))) \land $ \\ 
 $ ((C6(X) \land $ \\ 
 $  \Rdiamond  \Rbox E3L32(X)) \rightarrow  \Rbox  \Rdiamond  \Rbox  \Rbox E2L15(X)) \land $ \\ 
 $ ( \Rbox (E1L46(X) \land $ \\ 
 $  \Rbox E1G14(X)) \rightarrow  \Rbox  \Rbox (C14(X) \land $ \\ 
 $ E2G33(X))) \land $ \\ 
 $ (( \Rnext E1G0(X) \land $ \\ 
 $  \Rbox E2L3(X)) \rightarrow (C2(X) \land $ \\ 
 $ C37(X) \land $ \\ 
 $ E2L9(X))) \land $ \\ 
 $ (( \Rnext C0(X) \land $ \\ 
 $  \Rbox E2L14(X)) \rightarrow (E2L9(X) \land $ \\ 
 $ E3L4(X) \land $ \\ 
 $ E2G44(X))) \land $ \\ 
 $ ( \Rbox (C46(X) \land $ \\ 
 $  \Rdiamond E3L5(X)) \rightarrow (C42(X) \land $ \\ 
 $  \Rbox  \Rdiamond C16(X))) \land $ \\ 
 $ ( \Rbox  \Rdiamond (E2G5(X) \land $ \\ 
 $ C19(X)) \rightarrow ( \Rdiamond C11(X) \land $ \\ 
 $  \Rdiamond E1L37(X))) \land $ \\ 
 $ (( \Rbox C37(X) \land $ \\ 
 $  \Rnext C15(X)) \rightarrow (C40(X) \land $ \\ 
 $ E2G37(X) \land $ \\ 
 $ E2G17(X))) \land $ \\ 
 $ (( \Rbox C1(X) \land $ \\ 
 $  \Rnext E1G22(X)) \rightarrow ( \Rnext E2L44(X) \land $ \\ 
 $  \Rnext C12(X))) \land $ \\ 
 $ ( \Rbox (C10(X) \land $ \\ 
 $  \Rnext E3G35(X)) \rightarrow  \Rdiamond (C29(X) \land $ \\ 
 $  \Rnext C25(X))) \land $ \\ 
 $ ((E1G12(X) \land $ \\ 
 $  \Rdiamond  \Rbox E1L48(X)) \rightarrow (C2(X) \land $ \\ 
 $ C47(X) \land $ \\ 
 $ C1(X))) \land $ \\ 
 $ (( \Rnext E3G31(X) \land $ \\ 
 $  \Rdiamond C31(X)) \rightarrow  \Rdiamond  \Rdiamond (C22(X) \land $ \\ 
 $ C20(X))) \land $ \\ 
 $ ( \Rbox  \Rdiamond  \Rdiamond  \Rnext C27(X) \rightarrow (E3L5(X) \land $ \\ 
 $  \Rdiamond  \Rdiamond E2G42(X))) \land $ \\ 
 $ ( \Rbox (E2G46(X) \land $ \\ 
 $  \Rbox C8(X)) \rightarrow (C17(X) \land $ \\ 
 $  \Rbox  \Rnext C27(X))) \land $ \\ 
 $ ( \Rbox  \Rbox  \Rdiamond  \Rbox E2L23(X) \rightarrow  \Rdiamond (E3G48(X) \land $ \\ 
 $  \Rdiamond C41(X))) \land $ \\ 
 $ ((E1G14(X) \land $ \\ 
 $  \Rbox  \Rnext E3G48(X)) \rightarrow  \Rdiamond (E1G38(X) \land $ \\ 
 $  \Rnext C6(X))) \land $ \\ 
 $ (( \Rnext E1G34(X) \land $ \\ 
 $  \Rnext C10(X)) \rightarrow ( \Rnext C20(X) \land $ \\ 
 $  \Rdiamond C45(X))) \land $ \\ 
 $ ( \Rbox (C4(X) \land $ \\ 
 $  \Rbox C18(X)) \rightarrow  \Rdiamond  \Rbox (E3L46(X) \land $ \\ 
 $ C35(X))) \land $ \\ 
 $ (( \Rnext E3G21(X) \land $ \\ 
 $  \Rbox E2L25(X)) \rightarrow  \Rdiamond  \Rbox  \Rdiamond  \Rbox E2L17(X)) \land $ \\ 
 $ ( \Rdiamond (E2G42(X) \land $ \\ 
 $  \Rdiamond C28(X)) \rightarrow  \Rdiamond (E2L12(X) \land $ \\ 
 $  \Rdiamond C41(X))) \land $ \\ 
 $ (( \Rnext E2G44(X) \land $ \\ 
 $  \Rnext C34(X)) \rightarrow  \Rdiamond  \Rbox (E3L31(X) \land $ \\ 
 $ E1L0(X))) \land $ \\ 
 $ ((E1G39(X) \land $ \\ 
 $ C24(X) \land $ \\ 
 $ E2G7(X)) \rightarrow  \Rbox  \Rdiamond C30(X)) \land $ \\ 
 $ (( \Rnext C39(X) \land $ \\ 
 $  \Rnext E1L49(X)) \rightarrow  \Rdiamond (C38(X) \land $ \\ 
 $  \Rbox C24(X))) \land $ \\ 
 $ (( \Rbox C37(X) \land $ \\ 
 $  \Rnext E1L48(X)) \rightarrow  \Rbox (E1G19(X) \land $ \\ 
 $  \Rnext E3G29(X))) \land $ \\ 
 $ ( \Rdiamond (C46(X) \land $ \\ 
 $  \Rnext C31(X)) \rightarrow  \Rdiamond (E2G23(X) \land $ \\ 
 $  \Rnext C6(X))) \land $ \\ 
 $ ( \Rbox  \Rbox  \Rdiamond  \Rdiamond C23(X) \rightarrow  \Rbox  \Rdiamond (E3G34(X) \land $ \\ 
 $ C14(X))) \land $ \\ 
 $ ((C1(X) \land $ \\ 
 $ E3L0(X) \land $ \\ 
 $ C33(X)) \rightarrow  \Rbox  \Rdiamond (C25(X) \land $ \\ 
 $ C1(X))) \land $ \\ 
 $ (( \Rbox E1L46(X) \land $ \\ 
 $  \Rnext C25(X)) \rightarrow  \Rdiamond (E3G31(X) \land $ \\ 
 $  \Rnext C12(X))) \land $ \\ 
 $ ((E1G17(X) \land $ \\ 
 $  \Rdiamond  \Rnext E2L13(X)) \rightarrow ( \Rnext C39(X) \land $ \\ 
 $  \Rdiamond E1L49(X))) \land $ \\ 
 $ ((C46(X) \land $ \\ 
 $ C9(X) \land $ \\ 
 $ C3(X)) \rightarrow (C49(X) \land $ \\ 
 $  \Rdiamond  \Rdiamond C41(X))) \land $ \\ 
 $ (( \Rbox E3L36(X) \land $ \\ 
 $  \Rbox C40(X)) \rightarrow (E2G20(X) \land $ \\ 
 $  \Rbox  \Rnext C47(X))) \land $ \\ 
 $ (( \Rbox E2L30(X) \land $ \\ 
 $  \Rnext C26(X)) \rightarrow  \Rbox  \Rdiamond  \Rdiamond  \Rnext C0(X)) \land $ \\ 
 $ ( \Rdiamond  \Rdiamond  \Rdiamond  \Rnext C27(X) \rightarrow  \Rbox  \Rdiamond (C32(X) \land $ \\ 
 $ C40(X))) \land $ \\ 
 $ ((E1L20(X) \land $ \\ 
 $ C8(X) \land $ \\ 
 $ C5(X)) \rightarrow  \Rbox  \Rbox  \Rdiamond  \Rdiamond E2G45(X)) \land $ \\ 
 $ ((E2L20(X) \land $ \\ 
 $  \Rdiamond  \Rdiamond C42(X)) \rightarrow  \Rbox (C43(X) \land $ \\ 
 $  \Rbox C24(X))) \land $ \\ 
 $ ((E3L10(X) \land $ \\ 
 $  \Rdiamond  \Rnext E2G16(X)) \rightarrow  \Rdiamond  \Rbox  \Rdiamond  \Rnext E3L34(X)) \land $ \\ 
 $ (( \Rnext E3G8(X) \land $ \\ 
 $  \Rdiamond E1G8(X)) \rightarrow (E3G4(X) \land $ \\ 
 $  \Rdiamond  \Rdiamond E1G29(X))) \land $ \\ 
 $ ( \Rdiamond  \Rbox  \Rbox  \Rdiamond C36(X) \rightarrow  \Rbox (E2G1(X) \land $ \\ 
 $  \Rnext C5(X))) \land $ \\ 
 $ ((E3L9(X) \land $ \\ 
 $ C47(X) \land $ \\ 
 $ E1L32(X)) \rightarrow  \Rbox (C11(X) \land $ \\ 
 $  \Rnext C11(X))) \land $ \\ 
 $ ( \Rbox (E3L28(X) \land $ \\ 
 $  \Rnext C11(X)) \rightarrow ( \Rnext C13(X) \land $ \\ 
 $  \Rbox E1G33(X))) \land $ \\ 
 $ ((C39(X) \land $ \\ 
 $  \Rdiamond  \Rbox E1L14(X)) \rightarrow  \Rdiamond  \Rbox  \Rdiamond  \Rnext E2L5(X)) \land $ \\ 
 $ (( \Rnext E2L12(X) \land $ \\ 
 $  \Rdiamond E2L3(X)) \rightarrow (C36(X) \land $ \\ 
 $ C23(X) \land $ \\ 
 $ C12(X))) \land $ \\ 
 $ ( \Rbox  \Rdiamond  \Rbox  \Rdiamond C44(X) \rightarrow (C10(X) \land $ \\ 
 $ C37(X) \land $ \\ 
 $ E1G25(X))) \land $ \\ 
 $ (( \Rbox E2G44(X) \land $ \\ 
 $  \Rnext E1L33(X)) \rightarrow (C48(X) \land $ \\ 
 $ E1L28(X) \land $ \\ 
 $ C4(X))) \land $ \\ 
 $ ((C43(X) \land $ \\ 
 $  \Rbox  \Rnext C22(X)) \rightarrow ( \Rnext E2L34(X) \land $ \\ 
 $  \Rnext E3L32(X))) \land $ \\ 
 $ (( \Rnext E1L30(X) \land $ \\ 
 $  \Rnext E1G30(X)) \rightarrow (E1L20(X) \land $ \\ 
 $ E2G26(X) \land $ \\ 
 $ C49(X))) \land $ \\ 
 $ (( \Rbox E1G44(X) \land $ \\ 
 $  \Rbox C33(X)) \rightarrow ( \Rnext C15(X) \land $ \\ 
 $  \Rnext C37(X))) \land $ \\ 
 $ (( \Rdiamond E2L17(X) \land $ \\ 
 $  \Rnext E1G41(X)) \rightarrow  \Rdiamond  \Rbox (C12(X) \land $ \\ 
 $ E3G35(X))) \land $ \\ 
 $ ((C17(X) \land $ \\ 
 $  \Rbox  \Rbox C7(X)) \rightarrow ( \Rnext C33(X) \land $ \\ 
 $  \Rbox C30(X))) \land $ \\ 
 $ ( \Rdiamond  \Rbox (E1G27(X) \land $ \\ 
 $ C7(X)) \rightarrow (C41(X) \land $ \\ 
 $  \Rdiamond  \Rnext E2L37(X))) \land $ \\ 
 $ ((C20(X) \land $ \\ 
 $  \Rdiamond  \Rnext C30(X)) \rightarrow  \Rbox  \Rdiamond (E1G41(X) \land $ \\ 
 $ E3L5(X))) \land $ \\ 
 $ (( \Rdiamond C15(X) \land $ \\ 
 $  \Rbox E1G35(X)) \rightarrow  \Rbox  \Rbox  \Rbox  \Rnext E1G4(X)) \land $ \\ 
 $ ( \Rbox (C34(X) \land $ \\ 
 $  \Rnext E2G1(X)) \rightarrow ( \Rbox C1(X) \land $ \\ 
 $  \Rnext E1G31(X))) \land $ \\ 
 $ ((C33(X) \land $ \\ 
 $ E2L10(X) \land $ \\ 
 $ E3L27(X)) \rightarrow ( \Rnext C5(X) \land $ \\ 
 $  \Rnext C34(X))) \land $ \\ 
 $ (( \Rnext C12(X) \land $ \\ 
 $  \Rbox C7(X)) \rightarrow  \Rdiamond  \Rdiamond  \Rbox  \Rnext C5(X)) \land $ \\ 
 $ ( \Rbox (C48(X) \land $ \\ 
 $  \Rnext C37(X)) \rightarrow  \Rdiamond  \Rbox (E2L48(X) \land $ \\ 
 $ E3G44(X))) \land $ \\ 
 $ ((C43(X) \land $ \\ 
 $ E2L33(X) \land $ \\ 
 $ C45(X)) \rightarrow  \Rbox  \Rdiamond (E3L20(X) \land $ \\ 
 $ E3L31(X))) \land $ \\ 
 $ ( \Rbox (E3G10(X) \land $ \\ 
 $  \Rdiamond C49(X)) \rightarrow  \Rbox (C14(X) \land $ \\ 
 $  \Rbox E1G41(X))) \land $ \\ 
 $ (( \Rbox C33(X) \land $ \\ 
 $  \Rdiamond C11(X)) \rightarrow  \Rbox (C5(X) \land $ \\ 
 $  \Rnext C38(X))) \land $ \\ 
 $ (( \Rnext E3G36(X) \land $ \\ 
 $  \Rdiamond C13(X)) \rightarrow ( \Rnext C43(X) \land $ \\ 
 $  \Rbox E3G4(X))) \land $ \\ 
 $ (( \Rnext E3G13(X) \land $ \\ 
 $  \Rnext E3L6(X)) \rightarrow  \Rbox (C21(X) \land $ \\ 
 $  \Rnext E1L7(X))) \land $ \\ 
 $ ((C4(X) \land $ \\ 
 $  \Rdiamond  \Rdiamond E3G13(X)) \rightarrow  \Rdiamond  \Rbox  \Rbox  \Rdiamond C38(X)) \land $ \\ 
 $ ( \Rdiamond (C48(X) \land $ \\ 
 $  \Rbox C16(X)) \rightarrow (C10(X) \land $ \\ 
 $  \Rdiamond  \Rbox C22(X))) \land $ \\ 
 $ ( \Rbox (C15(X) \land $ \\ 
 $  \Rnext C48(X)) \rightarrow (C15(X) \land $ \\ 
 $  \Rbox  \Rbox E1G18(X))) \land $ \\ 
 $ (( \Rbox E3L48(X) \land $ \\ 
 $  \Rnext E1L45(X)) \rightarrow (E2G41(X) \land $ \\ 
 $ E1L20(X) \land $ \\ 
 $ C7(X))) \land $ \\ 
 $ ( \Rbox (C46(X) \land $ \\ 
 $  \Rbox E2L47(X)) \rightarrow  \Rbox (E3L23(X) \land $ \\ 
 $  \Rdiamond E3G7(X))) \land $ \\ 
 $ (( \Rnext E1L3(X) \land $ \\ 
 $  \Rnext C19(X)) \rightarrow (C10(X) \land $ \\ 
 $ E3L2(X) \land $ \\ 
 $ E2G43(X))) \land $ \\ 
 $ ( \Rbox  \Rdiamond (E2G38(X) \land $ \\ 
 $ C28(X)) \rightarrow ( \Rnext E2L11(X) \land $ \\ 
 $  \Rbox E1G12(X))) \land $ \\ 
 $ ( \Rbox (E3G42(X) \land $ \\ 
 $  \Rbox C5(X)) \rightarrow (C16(X) \land $ \\ 
 $  \Rbox  \Rdiamond C39(X))) \land $ \\ 
 $ ( \Rbox  \Rbox  \Rbox  \Rnext C26(X) \rightarrow (C1(X) \land $ \\ 
 $  \Rbox  \Rbox E3G4(X))) \land $ \\ 
 $ ( \Rdiamond  \Rdiamond  \Rbox  \Rnext C14(X) \rightarrow  \Rdiamond  \Rdiamond (E2L24(X) \land $ \\ 
 $ C22(X))) \land $ \\ 
 $ ((C8(X) \land $ \\ 
 $  \Rdiamond  \Rbox C5(X)) \rightarrow ( \Rnext E1L31(X) \land $ \\ 
 $  \Rdiamond E3G39(X))) \land $ \\ 
 $ (( \Rnext E1L18(X) \land $ \\ 
 $  \Rbox C9(X)) \rightarrow ( \Rnext C47(X) \land $ \\ 
 $  \Rnext C43(X))) \land $ \\ 
 $ ( \Rbox  \Rbox (E3G18(X) \land $ \\ 
 $ E1L37(X)) \rightarrow (C7(X) \land $ \\ 
 $ C10(X) \land $ \\ 
 $ C28(X))) \land $ \\ 
 $ ((C0(X) \land $ \\ 
 $  \Rbox  \Rnext E2G15(X)) \rightarrow  \Rdiamond (E2G40(X) \land $ \\ 
 $  \Rnext C40(X))) \land $ \\ 
 $ ((E3G23(X) \land $ \\ 
 $ E1L45(X) \land $ \\ 
 $ C46(X)) \rightarrow  \Rbox  \Rdiamond  \Rbox  \Rnext C29(X)) \land $ \\ 
 $ ( \Rdiamond  \Rdiamond (E2L0(X) \land $ \\ 
 $ C1(X)) \rightarrow  \Rbox  \Rbox  \Rdiamond  \Rnext E2L5(X)) \land $ \\ 
 $ ( \Rdiamond  \Rdiamond (E2L37(X) \land $ \\ 
 $ C33(X)) \rightarrow (C49(X) \land $ \\ 
 $  \Rbox  \Rnext E3L20(X))) \land $ \\ 
 $ (( \Rdiamond C3(X) \land $ \\ 
 $  \Rdiamond C4(X)) \rightarrow  \Rdiamond  \Rbox (C22(X) \land $ \\ 
 $ E3L35(X))) \land $ \\ 
 $ ( \Rbox  \Rbox (E1L16(X) \land $ \\ 
 $ C4(X)) \rightarrow ( \Rnext E1L17(X) \land $ \\ 
 $  \Rbox E1G40(X))) \land $ \\ 
 $ ( \Rdiamond (C6(X) \land $ \\ 
 $  \Rbox C21(X)) \rightarrow  \Rbox  \Rbox (C0(X) \land $ \\ 
 $ C10(X))) \land $ \\ 
 $ ( \Rbox  \Rdiamond  \Rdiamond  \Rbox C6(X) \rightarrow  \Rdiamond (E2G48(X) \land $ \\ 
 $  \Rnext C4(X))) \land $ \\ 
 $ ((E3G37(X) \land $ \\ 
 $  \Rdiamond  \Rnext E2L24(X)) \rightarrow  \Rbox  \Rbox (E3L13(X) \land $ \\ 
 $ C29(X))) \land $ \\ 
 $ ((E1G21(X) \land $ \\ 
 $  \Rdiamond  \Rbox E2G3(X)) \rightarrow  \Rbox  \Rdiamond (E3L24(X) \land $ \\ 
 $ C30(X))) \land $ \\ 
 $ ( \Rdiamond  \Rbox (E1L28(X) \land $ \\ 
 $ E1L26(X)) \rightarrow  \Rbox  \Rdiamond  \Rdiamond  \Rdiamond C45(X)) \land $ \\ 
 $ ((E3L39(X) \land $ \\ 
 $  \Rdiamond  \Rnext C36(X)) \rightarrow (C13(X) \land $ \\ 
 $  \Rbox  \Rdiamond C16(X))) \land $ \\ 
 $ ( \Rdiamond (C21(X) \land $ \\ 
 $  \Rnext C0(X)) \rightarrow ( \Rdiamond C38(X) \land $ \\ 
 $  \Rnext C30(X))) \land $ \\ 
 $ ( \Rdiamond (E1L44(X) \land $ \\ 
 $  \Rnext E2L34(X)) \rightarrow (E1L40(X) \land $ \\ 
 $  \Rbox  \Rbox C2(X))) \land $ \\ 
 $ ((C16(X) \land $ \\ 
 $ E2L32(X) \land $ \\ 
 $ E3L24(X)) \rightarrow  \Rdiamond (C0(X) \land $ \\ 
 $  \Rbox E1L10(X))) \land $ \\ 
 $ ( \Rdiamond (E1G40(X) \land $ \\ 
 $  \Rdiamond E2G44(X)) \rightarrow (C26(X) \land $ \\ 
 $ C21(X) \land $ \\ 
 $ E2G19(X))) \land $ \\ 
 $ ((C17(X) \land $ \\ 
 $ E1G46(X) \land $ \\ 
 $ C21(X)) \rightarrow  \Rdiamond  \Rdiamond (E1L46(X) \land $ \\ 
 $ E3G38(X))) \land $ \\ 
 $ ( \Rdiamond  \Rdiamond  \Rbox  \Rbox E3G42(X) \rightarrow  \Rdiamond  \Rdiamond (E3L25(X) \land $ \\ 
 $ C28(X))) \land $ \\ 
 $ ( \Rdiamond  \Rdiamond (C25(X) \land $ \\ 
 $ E3L46(X)) \rightarrow  \Rdiamond  \Rdiamond (E2G47(X) \land $ \\ 
 $ C36(X))) \land $ \\ 
 $ ( \Rdiamond (C34(X) \land $ \\ 
 $  \Rbox E2L21(X)) \rightarrow  \Rbox  \Rdiamond (C47(X) \land $ \\ 
 $ C0(X))) \land $ \\ 
 $ ( \Rdiamond  \Rdiamond (E1G48(X) \land $ \\ 
 $ C40(X)) \rightarrow  \Rdiamond (E1G1(X) \land $ \\ 
 $  \Rnext E1G4(X))) \land $ \\ 
 $ (( \Rbox E1G33(X) \land $ \\ 
 $  \Rnext C0(X)) \rightarrow  \Rdiamond  \Rdiamond  \Rdiamond  \Rnext E2L38(X)) \land $ \\ 
 $ ( \Rbox (C20(X) \land $ \\ 
 $  \Rbox C15(X)) \rightarrow ( \Rbox E2L4(X) \land $ \\ 
 $  \Rnext E1L42(X))) \land $ \\ 
 $ ( \Rdiamond  \Rbox  \Rdiamond  \Rnext C32(X) \rightarrow  \Rdiamond (E2L41(X) \land $ \\ 
 $  \Rdiamond C12(X))) \land $ \\ 
 $ ( \Rdiamond (C30(X) \land $ \\ 
 $  \Rnext E1L38(X)) \rightarrow  \Rbox (E2L21(X) \land $ \\ 
 $  \Rbox C22(X))) \land $ \\ 
 $ (( \Rnext C42(X) \land $ \\ 
 $  \Rnext E3L35(X)) \rightarrow (E3G27(X) \land $ \\ 
 $ C24(X) \land $ \\ 
 $ E2L26(X))) \land $ \\ 
 $ ( \Rdiamond  \Rbox  \Rdiamond  \Rnext E2G15(X) \rightarrow ( \Rdiamond C0(X) \land $ \\ 
 $  \Rdiamond C5(X))) \land $ \\ 
 $ (( \Rbox C0(X) \land $ \\ 
 $  \Rdiamond C9(X)) \rightarrow  \Rdiamond  \Rdiamond (C36(X) \land $ \\ 
 $ C14(X))) \land $ \\ 
 $ ( \Rdiamond (C18(X) \land $ \\ 
 $  \Rdiamond C39(X)) \rightarrow (C11(X) \land $ \\ 
 $ C39(X) \land $ \\ 
 $ E1L9(X))) \land $ \\ 
 $ ((E1G22(X) \land $ \\ 
 $  \Rbox  \Rnext C15(X)) \rightarrow (E2L17(X) \land $ \\ 
 $ E2L45(X) \land $ \\ 
 $ C41(X))) \land $ \\ 
 $ (( \Rnext E3L43(X) \land $ \\ 
 $  \Rbox C43(X)) \rightarrow ( \Rbox E2L34(X) \land $ \\ 
 $  \Rnext E2L44(X))) \land $ \\ 
 $ ( \Rbox (C13(X) \land $ \\ 
 $  \Rdiamond C27(X)) \rightarrow  \Rbox (E1L37(X) \land $ \\ 
 $  \Rnext E3L5(X))) \land $ \\ 
 $ (( \Rbox E3G48(X) \land $ \\ 
 $  \Rnext E1L17(X)) \rightarrow ( \Rnext C47(X) \land $ \\ 
 $  \Rnext C13(X))) \land $ \\ 
 $ (( \Rnext C25(X) \land $ \\ 
 $  \Rnext E3L22(X)) \rightarrow ( \Rnext C26(X) \land $ \\ 
 $  \Rnext C20(X))) \land $ \\ 
 $ (( \Rnext E3G40(X) \land $ \\ 
 $  \Rnext C17(X)) \rightarrow  \Rbox  \Rbox  \Rbox  \Rdiamond C7(X)) \land $ \\ 
 $ ( \Rbox  \Rdiamond (E3G26(X) \land $ \\ 
 $ E2G12(X)) \rightarrow ( \Rnext C30(X) \land $ \\ 
 $  \Rdiamond C12(X))) \land $ \\ 
 $ (( \Rnext C37(X) \land $ \\ 
 $  \Rdiamond E3G46(X)) \rightarrow  \Rdiamond  \Rbox  \Rbox  \Rnext E2G9(X)) \land $ \\ 
 $ (( \Rdiamond E3G4(X) \land $ \\ 
 $  \Rnext C11(X)) \rightarrow  \Rbox (E3G13(X) \land $ \\ 
 $  \Rnext C10(X))) \land $ \\ 
 $ ((C41(X) \land $ \\ 
 $  \Rbox  \Rdiamond C15(X)) \rightarrow ( \Rnext C30(X) \land $ \\ 
 $  \Rnext E1L23(X))) \land $ \\ 
 $ ( \Rbox (C10(X) \land $ \\ 
 $  \Rnext C7(X)) \rightarrow  \Rdiamond (E1L15(X) \land $ \\ 
 $  \Rbox C3(X))) \land $ \\ 
 $ (( \Rbox E2G23(X) \land $ \\ 
 $  \Rnext C16(X)) \rightarrow  \Rdiamond  \Rbox (C17(X) \land $ \\ 
 $ E1G29(X))) \land $ \\ 
 $ ((E3L28(X) \land $ \\ 
 $  \Rbox  \Rnext E2L25(X)) \rightarrow ( \Rbox C23(X) \land $ \\ 
 $  \Rbox E3L38(X))) \land $ \\ 
 $ ((C5(X) \land $ \\ 
 $ C3(X)) \rightarrow (E3L29(X) \land $ \\ 
 $  \Rdiamond  \Rbox E3G10(X))) \land $ \\ 
 $ ( \Rbox  \Rdiamond (C8(X) \land $ \\ 
 $ C4(X)) \rightarrow ( \Rnext C11(X) \land $ \\ 
 $  \Rnext C22(X))) \land $ \\ 
 $ (( \Rnext E2G7(X) \land $ \\ 
 $  \Rbox C19(X)) \rightarrow  \Rbox  \Rbox  \Rbox  \Rbox C5(X)) \land $ \\ 
 $ (( \Rdiamond C27(X) \land $ \\ 
 $  \Rnext E3G22(X)) \rightarrow  \Rbox  \Rdiamond (C15(X) \land $ \\ 
 $ E2L22(X))) \land $ \\ 
 $ (( \Rdiamond C44(X) \land $ \\ 
 $  \Rnext C10(X)) \rightarrow  \Rdiamond (E1G47(X) \land $ \\ 
 $  \Rnext C27(X))) \land $ \\ 
 $ (E3G13(X) \rightarrow E1G13(X)) \land $ \\ 
 $ (E2G47(X) \rightarrow E1G47(X)) \land $ \\ 
 $ (E2L45(X) \rightarrow E1L45(X)) \land $ \\ 
 $ (E3L23(X) \rightarrow E2L23(X)) \land $ \\ 
 $ (E2L30(X) \rightarrow E1L30(X)) \land $ \\ 
 $ (E2L24(X) \rightarrow E1L24(X)) \land $ \\ 
 $ (E2G7(X) \rightarrow E1G7(X)) \land $ \\ 
 $ (E2G43(X) \rightarrow E1G43(X)) \land $ \\ 
 $ (E2G15(X) \rightarrow E1G15(X)) \land $ \\ 
 $ (E3L24(X) \rightarrow E2L24(X)) \land $ \\ 
 $ (E3L13(X) \rightarrow E2L13(X)) \land $ \\ 
 $ (E2G45(X) \rightarrow E1G45(X)) \land $ \\ 
 $ (E3L48(X) \rightarrow E2L48(X)) \land $ \\ 
 $ (E3L36(X) \rightarrow E1L36(X)) \land $ \\ 
 $ (E3G22(X) \rightarrow E1G22(X)) \land $ \\ 
 $ (E2L17(X) \rightarrow E1L17(X)) \land $ \\ 
 $ (E2L19(X) \rightarrow E1L19(X)) \land $ \\ 
 $ (E3G35(X) \rightarrow E1G35(X)) \land $ \\ 
 $ (E2L41(X) \rightarrow E1L41(X)) \land $ \\ 
 $ (E2L2(X) \rightarrow E1L2(X)) \land $ \\ 
 $ (E2L11(X) \rightarrow E1L11(X)) \land $ \\ 
 $ (E3G44(X) \rightarrow E2G44(X)) \land $ \\ 
 $ (E3L29(X) \rightarrow E1L29(X)) \land $ \\ 
 $ (E3L41(X) \rightarrow E2L41(X)) \land $ \\ 
 $ (E2L26(X) \rightarrow E1L26(X)) \land $ \\ 
 $ (E2G26(X) \rightarrow E1G26(X)) \land $ \\ 
 $ (E2L9(X) \rightarrow E1L9(X)) \land $ \\ 
 $ (E2L23(X) \rightarrow E1L23(X)) \land $ \\ 
 $ (E2L25(X) \rightarrow E1L25(X)) \land $ \\ 
 $ (E2L44(X) \rightarrow E1L44(X)) \land $ \\ 
 $ (E2L5(X) \rightarrow E1L5(X)) \land $ \\ 
 $ (E3L31(X) \rightarrow E1L31(X)) \land $ \\ 
 $ (E2L43(X) \rightarrow E1L43(X)) \land $ \\ 
 $ (E2L3(X) \rightarrow E1L3(X)) \land $ \\ 
 $ (E2L12(X) \rightarrow E1L12(X)) \land $ \\ 
 $ (E3G29(X) \rightarrow E1G29(X)) \land $ \\ 
 $ (E3L6(X) \rightarrow E1L6(X)) \land $ \\ 
 $ (E2G12(X) \rightarrow E1G12(X)) \land $ \\ 
 $ (E2L14(X) \rightarrow E1L14(X)) \land $ \\ 
 $ (E3G48(X) \rightarrow E2G48(X)) \land $ \\ 
 $ (E2G16(X) \rightarrow E1G16(X)) \land $ \\ 
 $ (E3L43(X) \rightarrow E2L43(X)) \land $ \\ 
 $ (E3L28(X) \rightarrow E1L28(X)) \land $ \\ 
 $ (E3G39(X) \rightarrow E1G39(X)) \land $ \\ 
 $ (E3L45(X) \rightarrow E2L45(X)) \land $ \\ 
 $ (E2G46(X) \rightarrow E1G46(X)) \land $ \\ 
 $ (E3G42(X) \rightarrow E2G42(X)) \land $ \\ 
 $ (E3L32(X) \rightarrow E2L32(X)) \land $ \\ 
 $ (E2L4(X) \rightarrow E1L4(X)) \land $ \\ 
 $ (E2G41(X) \rightarrow E1G41(X)) \land $ \\ 
 $ (E2L32(X) \rightarrow E1L32(X)) \land $ \\ 
 $ (E3G8(X) \rightarrow E1G8(X)) \land $ \\ 
 $ (E2G20(X) \rightarrow E1G20(X)) \land $ \\ 
 $ (E2G3(X) \rightarrow E1G3(X)) \land $ \\ 
 $ (E3G36(X) \rightarrow E1G36(X)) \land $ \\ 
 $ (E3G4(X) \rightarrow E1G4(X)) \land $ \\ 
 $ (E2L34(X) \rightarrow E1L34(X)) \land $ \\ 
 $ (E3G18(X) \rightarrow E1G18(X)) \land $ \\ 
 $ (E2L48(X) \rightarrow E1L48(X)) \land $ \\ 
 $ (E2G23(X) \rightarrow E1G23(X)) \land $ \\ 
 $ (E3L4(X) \rightarrow E2L4(X)) \land $ \\ 
 $ (E2L13(X) \rightarrow E1L13(X)) \land $ \\ 
 $ (E2G44(X) \rightarrow E1G44(X)) \land $ \\ 
 $ (E3L9(X) \rightarrow E2L9(X)) \land $ \\ 
 $ (E3L39(X) \rightarrow E1L39(X)) \land $ \\ 
 $ (E2G9(X) \rightarrow E1G9(X)) \land $ \\ 
 $ (E3L20(X) \rightarrow E2L20(X)) \land $ \\ 
 $ (E3G46(X) \rightarrow E2G46(X)) \land $ \\ 
 $ (E2G19(X) \rightarrow E1G19(X)) \land $ \\ 
 $ (E3G3(X) \rightarrow E2G3(X)) \land $ \\ 
 $ (E2L10(X) \rightarrow E1L10(X)) \land $ \\ 
 $ (E3L38(X) \rightarrow E2L38(X)) \land $ \\ 
 $ (E2L15(X) \rightarrow E1L15(X)) \land $ \\ 
 $ (E3L47(X) \rightarrow E2L47(X)) \land $ \\ 
 $ (E2G42(X) \rightarrow E1G42(X)) \land $ \\ 
 $ (E2G40(X) \rightarrow E1G40(X)) \land $ \\ 
 $ (E3G47(X) \rightarrow E2G47(X)) \land $ \\ 
 $ (E3L22(X) \rightarrow E2L22(X)) \land $ \\ 
 $ (E3L15(X) \rightarrow E2L15(X)) \land $ \\ 
 $ (E3L46(X) \rightarrow E1L46(X)) \land $ \\ 
 $ (E2L33(X) \rightarrow E1L33(X)) \land $ \\ 
 $ (E2L38(X) \rightarrow E1L38(X)) \land $ \\ 
 $ (E3G28(X) \rightarrow E1G28(X)) \land $ \\ 
 $ (E3L10(X) \rightarrow E2L10(X)) \land $ \\ 
 $ (E2L21(X) \rightarrow E1L21(X)) \land $ \\ 
 $ (E3L27(X) \rightarrow E1L27(X)) \land $ \\ 
 $ (E3G38(X) \rightarrow E2G38(X)) \land $ \\ 
 $ (E2G17(X) \rightarrow E1G17(X)) \land $ \\ 
 $ (E2G38(X) \rightarrow E1G38(X)) \land $ \\ 
 $ (E2G32(X) \rightarrow E1G32(X)) \land $ \\ 
 $ (E2L37(X) \rightarrow E1L37(X)) \land $ \\ 
 $ (E2G48(X) \rightarrow E1G48(X)) \land $ \\ 
 $ (E3L35(X) \rightarrow E1L35(X)) \land $ \\ 
 $ (E3G23(X) \rightarrow E2G23(X)) \land $ \\ 
 $ (E3L5(X) \rightarrow E2L5(X)) \land $ \\ 
 $ (E2L22(X) \rightarrow E1L22(X)) \land $ \\ 
 $ (E3G40(X) \rightarrow E2G40(X)) \land $ \\ 
 $ (E3G27(X) \rightarrow E1G27(X)) \land $ \\ 
 $ (E3G7(X) \rightarrow E2G7(X)) \land $ \\ 
 $ (E3L0(X) \rightarrow E2L0(X)) \land $ \\ 
 $ (E2L47(X) \rightarrow E1L47(X)) \land $ \\ 
 $ (E3G31(X) \rightarrow E1G31(X)) \land $ \\ 
 $ (E2L0(X) \rightarrow E1L0(X)) \land $ \\ 
 $ (E3G26(X) \rightarrow E2G26(X)) \land $ \\ 
 $ (E2G5(X) \rightarrow E1G5(X)) \land $ \\ 
 $ (E3G10(X) \rightarrow E1G10(X)) \land $ \\ 
 $ (E2G0(X) \rightarrow E1G0(X)) \land $ \\ 
 $ (E2L20(X) \rightarrow E1L20(X)) \land $ \\ 
 $ (E3L25(X) \rightarrow E2L25(X)) \land $ \\ 
 $ (E3G21(X) \rightarrow E1G21(X)) \land $ \\ 
 $ (E3L21(X) \rightarrow E2L21(X)) \land $ \\ 
 $ (E2G37(X) \rightarrow E1G37(X)) \land $ \\ 
 $ (E2G1(X) \rightarrow E1G1(X)) \land $ \\ 
 $ (E3L34(X) \rightarrow E2L34(X)) \land $ \\ 
 $ (E3L2(X) \rightarrow E2L2(X)) \land $ \\ 
 $ (E3G37(X) \rightarrow E2G37(X)) \land $ \\ 
 $ (E2G33(X) \rightarrow E1G33(X)) \land $ \\ 
 $ (E3G34(X) \rightarrow E1G34(X))) \land $ \\ 
 $ ( \Rdiamond E1G9(X) \rightarrow  \Rbox PG9) \land $ \\ 
 $ ( \Rdiamond E1G2(X) \rightarrow  \Rbox E1G2(X)) \land $ \\ 
 $ ( \Rdiamond E1L43(X) \rightarrow  \Rbox PL43) \land $ \\ 
 $ ( \Rdiamond E3G46(X) \rightarrow  \Rbox E3G46(X)) \land $ \\ 
 $ ( \Rdiamond E1G32Inv(X) \rightarrow  \Rbox E1G32Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1L5Inv(X) \rightarrow  \Rbox PinvL5) \land $ \\ 
 $ ( \Rdiamond E1L46Inv(X) \rightarrow  \Rbox PinvL46) \land $ \\ 
 $ ( \Rdiamond E1G28Inv(X) \rightarrow  \Rbox E1G28Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1L40(X) \rightarrow  \Rbox PL40) \land $ \\ 
 $ ( \Rdiamond E1G41Inv(X) \rightarrow  \Rbox PinvG41) \land $ \\ 
 $ ( \Rdiamond E1G16Inv(X) \rightarrow  \Rbox E1G16Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1G19(X) \rightarrow  \Rbox PG19) \land $ \\ 
 $ ( \Rdiamond E2G43(X) \rightarrow  \Rbox E2G43(X)) \land $ \\ 
 $ ( \Rdiamond E2G0(X) \rightarrow  \Rbox E2G0(X)) \land $ \\ 
 $ ( \Rdiamond E2G38(X) \rightarrow  \Rbox E2G38(X)) \land $ \\ 
 $ ( \Rdiamond E1L3Inv(X) \rightarrow  \Rbox PinvL3) \land $ \\ 
 $ ( \Rdiamond E1G25(X) \rightarrow  \Rbox E1G25(X)) \land $ \\ 
 $ ( \Rdiamond E1G20(X) \rightarrow  \Rbox PG20) \land $ \\ 
 $ ( \Rdiamond E1L9(X) \rightarrow  \Rbox PL9) \land $ \\ 
 $ ( \Rdiamond E1G4Inv(X) \rightarrow  \Rbox E1G4Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1G22(X) \rightarrow  \Rbox PG22) \land $ \\ 
 $ ( \Rdiamond E1G1(X) \rightarrow  \Rbox PG1) \land $ \\ 
 $ ( \Rdiamond E2G26(X) \rightarrow  \Rbox E2G26(X)) \land $ \\ 
 $ ( \Rdiamond E3G37(X) \rightarrow  \Rbox E3G37(X)) \land $ \\ 
 $ ( \Rdiamond E1L26(X) \rightarrow  \Rbox PL26) \land $ \\ 
 $ ( \Rdiamond E1G5(X) \rightarrow  \Rbox E1G5(X)) \land $ \\ 
 $ ( \Rdiamond E1L22Inv(X) \rightarrow  \Rbox PinvL22) \land $ \\ 
 $ ( \Rdiamond E3G28(X) \rightarrow  \Rbox E3G28(X)) \land $ \\ 
 $ ( \Rdiamond E1G8Inv(X) \rightarrow  \Rbox E1G8Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1G40(X) \rightarrow  \Rbox PG40) \land $ \\ 
 $ ( \Rdiamond E1G38(X) \rightarrow  \Rbox PG38) \land $ \\ 
 $ ( \Rdiamond E2G45(X) \rightarrow  \Rbox E2G45(X)) \land $ \\ 
 $ ( \Rdiamond E1G23Inv(X) \rightarrow  \Rbox E1G23Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1G37(X) \rightarrow  \Rbox PG37) \land $ \\ 
 $ ( \Rdiamond E1L21(X) \rightarrow  \Rbox PL21) \land $ \\ 
 $ ( \Rdiamond E1L45Inv(X) \rightarrow  \Rbox PinvL45) \land $ \\ 
 $ ( \Rdiamond E1G21(X) \rightarrow  \Rbox E1G21(X)) \land $ \\ 
 $ ( \Rdiamond E1G32Inv(X) \rightarrow  \Rbox PinvG32) \land $ \\ 
 $ ( \Rdiamond E1G22(X) \rightarrow  \Rbox E1G22(X)) \land $ \\ 
 $ ( \Rdiamond E1G8Inv(X) \rightarrow  \Rbox PinvG8) \land $ \\ 
 $ ( \Rdiamond E1G35(X) \rightarrow  \Rbox PG35) \land $ \\ 
 $ ( \Rdiamond E3G34(X) \rightarrow  \Rbox E3G34(X)) \land $ \\ 
 $ ( \Rdiamond E2G12(X) \rightarrow  \Rbox E2G12(X)) \land $ \\ 
 $ ( \Rdiamond E1L45(X) \rightarrow  \Rbox PL45) \land $ \\ 
 $ ( \Rdiamond E1G37Inv(X) \rightarrow  \Rbox E1G37Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1G3Inv(X) \rightarrow  \Rbox E1G3Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1G33Inv(X) \rightarrow  \Rbox E1G33Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1G39Inv(X) \rightarrow  \Rbox PinvG39) \land $ \\ 
 $ ( \Rdiamond E1G43(X) \rightarrow  \Rbox PG43) \land $ \\ 
 $ ( \Rdiamond E1L1Inv(X) \rightarrow  \Rbox PinvL1) \land $ \\ 
 $ ( \Rdiamond E1G23Inv(X) \rightarrow  \Rbox PinvG23) \land $ \\ 
 $ ( \Rdiamond E1G0Inv(X) \rightarrow  \Rbox E1G0Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1G7(X) \rightarrow  \Rbox E1G7(X)) \land $ \\ 
 $ ( \Rdiamond E2G5(X) \rightarrow  \Rbox E2G5(X)) \land $ \\ 
 $ ( \Rdiamond E1G41(X) \rightarrow  \Rbox E1G41(X)) \land $ \\ 
 $ ( \Rdiamond E1L35(X) \rightarrow  \Rbox PL35) \land $ \\ 
 $ ( \Rdiamond E1G4(X) \rightarrow  \Rbox E1G4(X)) \land $ \\ 
 $ ( \Rdiamond E1L30(X) \rightarrow  \Rbox PL30) \land $ \\ 
 $ ( \Rdiamond E1G9Inv(X) \rightarrow  \Rbox E1G9Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1L0(X) \rightarrow  \Rbox PL0) \land $ \\ 
 $ ( \Rdiamond E1L49(X) \rightarrow  \Rbox PL49) \land $ \\ 
 $ ( \Rdiamond E1G47(X) \rightarrow  \Rbox PG47) \land $ \\ 
 $ ( \Rdiamond E3G44(X) \rightarrow  \Rbox E3G44(X)) \land $ \\ 
 $ ( \Rdiamond E1G40Inv(X) \rightarrow  \Rbox PinvG40) \land $ \\ 
 $ ( \Rdiamond E1L28Inv(X) \rightarrow  \Rbox PinvL28) \land $ \\ 
 $ ( \Rdiamond E1G42Inv(X) \rightarrow  \Rbox E1G42Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1L15(X) \rightarrow  \Rbox PL15) \land $ \\ 
 $ ( \Rdiamond E1G15(X) \rightarrow  \Rbox E1G15(X)) \land $ \\ 
 $ ( \Rdiamond E1G20Inv(X) \rightarrow  \Rbox PinvG20) \land $ \\ 
 $ ( \Rdiamond E1L2Inv(X) \rightarrow  \Rbox PinvL2) \land $ \\ 
 $ ( \Rdiamond E3G38(X) \rightarrow  \Rbox E3G38(X)) \land $ \\ 
 $ ( \Rdiamond E1L39(X) \rightarrow  \Rbox PL39) \land $ \\ 
 $ ( \Rdiamond E1G46Inv(X) \rightarrow  \Rbox PinvG46) \land $ \\ 
 $ ( \Rdiamond E1L7Inv(X) \rightarrow  \Rbox PinvL7) \land $ \\ 
 $ ( \Rdiamond E1L25Inv(X) \rightarrow  \Rbox PinvL25) \land $ \\ 
 $ ( \Rdiamond E3G7(X) \rightarrow  \Rbox E3G7(X)) \land $ \\ 
 $ ( \Rdiamond E1G22Inv(X) \rightarrow  \Rbox E1G22Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1G17(X) \rightarrow  \Rbox E1G17(X)) \land $ \\ 
 $ ( \Rdiamond E2G1(X) \rightarrow  \Rbox E2G1(X)) \land $ \\ 
 $ ( \Rdiamond E1G36(X) \rightarrow  \Rbox E1G36(X)) \land $ \\ 
 $ ( \Rdiamond E1L25(X) \rightarrow  \Rbox PL25) \land $ \\ 
 $ ( \Rdiamond E1G33(X) \rightarrow  \Rbox PG33) \land $ \\ 
 $ ( \Rdiamond E1G47Inv(X) \rightarrow  \Rbox PinvG47) \land $ \\ 
 $ ( \Rdiamond E2G44(X) \rightarrow  \Rbox E2G44(X)) \land $ \\ 
 $ ( \Rdiamond E1L41Inv(X) \rightarrow  \Rbox PinvL41) \land $ \\ 
 $ ( \Rdiamond E1L24(X) \rightarrow  \Rbox PL24) \land $ \\ 
 $ ( \Rdiamond E1G23(X) \rightarrow  \Rbox PG23) \land $ \\ 
 $ ( \Rdiamond E1G21Inv(X) \rightarrow  \Rbox PinvG21) \land $ \\ 
 $ ( \Rdiamond E1G25Inv(X) \rightarrow  \Rbox PinvG25) \land $ \\ 
 $ ( \Rdiamond E1G29Inv(X) \rightarrow  \Rbox PinvG29) \land $ \\ 
 $ ( \Rdiamond E1G8(X) \rightarrow  \Rbox PG8) \land $ \\ 
 $ ( \Rdiamond E1G41(X) \rightarrow  \Rbox PG41) \land $ \\ 
 $ ( \Rdiamond E1L23(X) \rightarrow  \Rbox PL23) \land $ \\ 
 $ ( \Rdiamond E1G9Inv(X) \rightarrow  \Rbox PinvG9) \land $ \\ 
 $ ( \Rdiamond E1G45Inv(X) \rightarrow  \Rbox PinvG45) \land $ \\ 
 $ ( \Rdiamond E1L24Inv(X) \rightarrow  \Rbox PinvL24) \land $ \\ 
 $ ( \Rdiamond E1G13(X) \rightarrow  \Rbox E1G13(X)) \land $ \\ 
 $ ( \Rdiamond E1G48Inv(X) \rightarrow  \Rbox PinvG48) \land $ \\ 
 $ ( \Rdiamond E1G1Inv(X) \rightarrow  \Rbox E1G1Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1G34Inv(X) \rightarrow  \Rbox E1G34Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1L32Inv(X) \rightarrow  \Rbox PinvL32) \land $ \\ 
 $ ( \Rdiamond E1G7Inv(X) \rightarrow  \Rbox PinvG7) \land $ \\ 
 $ ( \Rdiamond E1G38(X) \rightarrow  \Rbox E1G38(X)) \land $ \\ 
 $ ( \Rdiamond E1G45(X) \rightarrow  \Rbox E1G45(X)) \land $ \\ 
 $ ( \Rdiamond E1G46(X) \rightarrow  \Rbox E1G46(X)) \land $ \\ 
 $ ( \Rdiamond E1G8(X) \rightarrow  \Rbox E1G8(X)) \land $ \\ 
 $ ( \Rdiamond E1G0(X) \rightarrow  \Rbox PG0) \land $ \\ 
 $ ( \Rdiamond E1G42(X) \rightarrow  \Rbox PG42) \land $ \\ 
 $ ( \Rdiamond E1G2Inv(X) \rightarrow  \Rbox E1G2Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1L17(X) \rightarrow  \Rbox PL17) \land $ \\ 
 $ ( \Rdiamond E1G15Inv(X) \rightarrow  \Rbox E1G15Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1G0Inv(X) \rightarrow  \Rbox PinvG0) \land $ \\ 
 $ ( \Rdiamond E1G48(X) \rightarrow  \Rbox PG48) \land $ \\ 
 $ ( \Rdiamond E3G29(X) \rightarrow  \Rbox E3G29(X)) \land $ \\ 
 $ ( \Rdiamond E1G14(X) \rightarrow  \Rbox E1G14(X)) \land $ \\ 
 $ ( \Rdiamond E1G14Inv(X) \rightarrow  \Rbox E1G14Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1G48(X) \rightarrow  \Rbox E1G48(X)) \land $ \\ 
 $ ( \Rdiamond E1G46Inv(X) \rightarrow  \Rbox E1G46Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1L14(X) \rightarrow  \Rbox PL14) \land $ \\ 
 $ ( \Rdiamond E1G28Inv(X) \rightarrow  \Rbox PinvG28) \land $ \\ 
 $ ( \Rdiamond E2G19(X) \rightarrow  \Rbox E2G19(X)) \land $ \\ 
 $ ( \Rdiamond E3G35(X) \rightarrow  \Rbox E3G35(X)) \land $ \\ 
 $ ( \Rdiamond E1L19Inv(X) \rightarrow  \Rbox PinvL19) \land $ \\ 
 $ ( \Rdiamond E3G8(X) \rightarrow  \Rbox E3G8(X)) \land $ \\ 
 $ ( \Rdiamond E1G39Inv(X) \rightarrow  \Rbox E1G39Inv(X)) \land $ \\ 
 $ ( \Rdiamond E2G17(X) \rightarrow  \Rbox E2G17(X)) \land $ \\ 
 $ ( \Rdiamond E1G16(X) \rightarrow  \Rbox E1G16(X)) \land $ \\ 
 $ ( \Rdiamond E1G29(X) \rightarrow  \Rbox E1G29(X)) \land $ \\ 
 $ ( \Rdiamond E1L33(X) \rightarrow  \Rbox PL33) \land $ \\ 
 $ ( \Rdiamond E1G46(X) \rightarrow  \Rbox PG46) \land $ \\ 
 $ ( \Rdiamond E1L16(X) \rightarrow  \Rbox PL16) \land $ \\ 
 $ ( \Rdiamond E1G22Inv(X) \rightarrow  \Rbox PinvG22) \land $ \\ 
 $ ( \Rdiamond E1G17Inv(X) \rightarrow  \Rbox PinvG17) \land $ \\ 
 $ ( \Rdiamond E1L31Inv(X) \rightarrow  \Rbox PinvL31) \land $ \\ 
 $ ( \Rdiamond E1G18Inv(X) \rightarrow  \Rbox PinvG18) \land $ \\ 
 $ ( \Rdiamond E1L38Inv(X) \rightarrow  \Rbox PinvL38) \land $ \\ 
 $ ( \Rdiamond E1G34Inv(X) \rightarrow  \Rbox PinvG34) \land $ \\ 
 $ ( \Rdiamond E2G46(X) \rightarrow  \Rbox E2G46(X)) \land $ \\ 
 $ ( \Rdiamond E3G10(X) \rightarrow  \Rbox E3G10(X)) \land $ \\ 
 $ ( \Rdiamond E1L15Inv(X) \rightarrow  \Rbox PinvL15) \land $ \\ 
 $ ( \Rdiamond E1G37(X) \rightarrow  \Rbox E1G37(X)) \land $ \\ 
 $ ( \Rdiamond E1G19(X) \rightarrow  \Rbox E1G19(X)) \land $ \\ 
 $ ( \Rdiamond E1L11Inv(X) \rightarrow  \Rbox PinvL11) \land $ \\ 
 $ ( \Rdiamond E3G47(X) \rightarrow  \Rbox E3G47(X)) \land $ \\ 
 $ ( \Rdiamond E1G27Inv(X) \rightarrow  \Rbox PinvG27) \land $ \\ 
 $ ( \Rdiamond E1G30(X) \rightarrow  \Rbox E1G30(X)) \land $ \\ 
 $ ( \Rdiamond E3G36(X) \rightarrow  \Rbox E3G36(X)) \land $ \\ 
 $ ( \Rdiamond E1L37(X) \rightarrow  \Rbox PL37) \land $ \\ 
 $ ( \Rdiamond E2G33(X) \rightarrow  \Rbox E2G33(X)) \land $ \\ 
 $ ( \Rdiamond E1G9(X) \rightarrow  \Rbox E1G9(X)) \land $ \\ 
 $ ( \Rdiamond E1G28(X) \rightarrow  \Rbox E1G28(X)) \land $ \\ 
 $ ( \Rdiamond E3G3(X) \rightarrow  \Rbox E3G3(X)) \land $ \\ 
 $ ( \Rdiamond E1L35Inv(X) \rightarrow  \Rbox PinvL35) \land $ \\ 
 $ ( \Rdiamond E1G13(X) \rightarrow  \Rbox PG13) \land $ \\ 
 $ ( \Rdiamond E1L48(X) \rightarrow  \Rbox PL48) \land $ \\ 
 $ ( \Rdiamond E1G18Inv(X) \rightarrow  \Rbox E1G18Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1L42(X) \rightarrow  \Rbox PL42) \land $ \\ 
 $ ( \Rdiamond E1G25(X) \rightarrow  \Rbox PG25) \land $ \\ 
 $ ( \Rdiamond E1G27(X) \rightarrow  \Rbox PG27) \land $ \\ 
 $ ( \Rdiamond E1G14(X) \rightarrow  \Rbox PG14) \land $ \\ 
 $ ( \Rdiamond E1L12Inv(X) \rightarrow  \Rbox PinvL12) \land $ \\ 
 $ ( \Rdiamond E1L42Inv(X) \rightarrow  \Rbox PinvL42) \land $ \\ 
 $ ( \Rdiamond E1G16(X) \rightarrow  \Rbox PG16) \land $ \\ 
 $ ( \Rdiamond E1G0(X) \rightarrow  \Rbox E1G0(X)) \land $ \\ 
 $ ( \Rdiamond E1L46(X) \rightarrow  \Rbox PL46) \land $ \\ 
 $ ( \Rdiamond E1G7(X) \rightarrow  \Rbox PG7) \land $ \\ 
 $ ( \Rdiamond E1G10Inv(X) \rightarrow  \Rbox E1G10Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1G43Inv(X) \rightarrow  \Rbox PinvG43) \land $ \\ 
 $ ( \Rdiamond E1G4Inv(X) \rightarrow  \Rbox PinvG4) \land $ \\ 
 $ ( \Rdiamond E1L49Inv(X) \rightarrow  \Rbox PinvL49) \land $ \\ 
 $ ( \Rdiamond E1G34(X) \rightarrow  \Rbox E1G34(X)) \land $ \\ 
 $ ( \Rdiamond E1G40(X) \rightarrow  \Rbox E1G40(X)) \land $ \\ 
 $ ( \Rdiamond E1L41(X) \rightarrow  \Rbox PL41) \land $ \\ 
 $ ( \Rdiamond E1L27(X) \rightarrow  \Rbox PL27) \land $ \\ 
 $ ( \Rdiamond E1G5(X) \rightarrow  \Rbox PG5) \land $ \\ 
 $ ( \Rdiamond E1G42Inv(X) \rightarrow  \Rbox PinvG42) \land $ \\ 
 $ ( \Rdiamond E1L34Inv(X) \rightarrow  \Rbox PinvL34) \land $ \\ 
 $ ( \Rdiamond E1G38Inv(X) \rightarrow  \Rbox E1G38Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1L7(X) \rightarrow  \Rbox PL7) \land $ \\ 
 $ ( \Rdiamond E1G1(X) \rightarrow  \Rbox E1G1(X)) \land $ \\ 
 $ ( \Rdiamond E1L6(X) \rightarrow  \Rbox PL6) \land $ \\ 
 $ ( \Rdiamond E1G3(X) \rightarrow  \Rbox PG3) \land $ \\ 
 $ ( \Rdiamond E2G15(X) \rightarrow  \Rbox E2G15(X)) \land $ \\ 
 $ ( \Rdiamond E2G40(X) \rightarrow  \Rbox E2G40(X)) \land $ \\ 
 $ ( \Rdiamond E1L10Inv(X) \rightarrow  \Rbox PinvL10) \land $ \\ 
 $ ( \Rdiamond E1G27Inv(X) \rightarrow  \Rbox E1G27Inv(X)) \land $ \\ 
 $ ( \Rdiamond E3G18(X) \rightarrow  \Rbox E3G18(X)) \land $ \\ 
 $ ( \Rdiamond E1G36Inv(X) \rightarrow  \Rbox E1G36Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1G32(X) \rightarrow  \Rbox E1G32(X)) \land $ \\ 
 $ ( \Rdiamond E1G39(X) \rightarrow  \Rbox E1G39(X)) \land $ \\ 
 $ ( \Rdiamond E1L11(X) \rightarrow  \Rbox PL11) \land $ \\ 
 $ ( \Rdiamond E1G34(X) \rightarrow  \Rbox PG34) \land $ \\ 
 $ ( \Rdiamond E1G17Inv(X) \rightarrow  \Rbox E1G17Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1G38Inv(X) \rightarrow  \Rbox PinvG38) \land $ \\ 
 $ ( \Rdiamond E2G42(X) \rightarrow  \Rbox E2G42(X)) \land $ \\ 
 $ ( \Rdiamond E1G44Inv(X) \rightarrow  \Rbox E1G44Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1G30Inv(X) \rightarrow  \Rbox PinvG30) \land $ \\ 
 $ ( \Rdiamond E1G5Inv(X) \rightarrow  \Rbox E1G5Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1L6Inv(X) \rightarrow  \Rbox PinvL6) \land $ \\ 
 $ ( \Rdiamond E1G10(X) \rightarrow  \Rbox E1G10(X)) \land $ \\ 
 $ ( \Rdiamond E1G26(X) \rightarrow  \Rbox E1G26(X)) \land $ \\ 
 $ ( \Rdiamond E3G39(X) \rightarrow  \Rbox E3G39(X)) \land $ \\ 
 $ ( \Rdiamond E1G35Inv(X) \rightarrow  \Rbox PinvG35) \land $ \\ 
 $ ( \Rdiamond E2G7(X) \rightarrow  \Rbox E2G7(X)) \land $ \\ 
 $ ( \Rdiamond E1G44(X) \rightarrow  \Rbox PG44) \land $ \\ 
 $ ( \Rdiamond E1L20Inv(X) \rightarrow  \Rbox PinvL20) \land $ \\ 
 $ ( \Rdiamond E1G39(X) \rightarrow  \Rbox PG39) \land $ \\ 
 $ ( \Rdiamond E1G7Inv(X) \rightarrow  \Rbox E1G7Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1G13Inv(X) \rightarrow  \Rbox PinvG13) \land $ \\ 
 $ ( \Rdiamond E2G9(X) \rightarrow  \Rbox E2G9(X)) \land $ \\ 
 $ ( \Rdiamond E1L44Inv(X) \rightarrow  \Rbox PinvL44) \land $ \\ 
 $ ( \Rdiamond E1G15Inv(X) \rightarrow  \Rbox PinvG15) \land $ \\ 
 $ ( \Rdiamond E1L47Inv(X) \rightarrow  \Rbox PinvL47) \land $ \\ 
 $ ( \Rdiamond E2G41(X) \rightarrow  \Rbox E2G41(X)) \land $ \\ 
 $ ( \Rdiamond E1G16Inv(X) \rightarrow  \Rbox PinvG16) \land $ \\ 
 $ ( \Rdiamond E1G44(X) \rightarrow  \Rbox E1G44(X)) \land $ \\ 
 $ ( \Rdiamond E1G45(X) \rightarrow  \Rbox PG45) \land $ \\ 
 $ ( \Rdiamond E1G10(X) \rightarrow  \Rbox PG10) \land $ \\ 
 $ ( \Rdiamond E1G14Inv(X) \rightarrow  \Rbox PinvG14) \land $ \\ 
 $ ( \Rdiamond E1G26Inv(X) \rightarrow  \Rbox E1G26Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1L16Inv(X) \rightarrow  \Rbox PinvL16) \land $ \\ 
 $ ( \Rdiamond E1G30Inv(X) \rightarrow  \Rbox E1G30Inv(X)) \land $ \\ 
 $ ( \Rdiamond E3G27(X) \rightarrow  \Rbox E3G27(X)) \land $ \\ 
 $ ( \Rdiamond E1G21Inv(X) \rightarrow  \Rbox E1G21Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1L3(X) \rightarrow  \Rbox PL3) \land $ \\ 
 $ ( \Rdiamond E1G3(X) \rightarrow  \Rbox E1G3(X)) \land $ \\ 
 $ ( \Rdiamond E1G47Inv(X) \rightarrow  \Rbox E1G47Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1G19Inv(X) \rightarrow  \Rbox PinvG19) \land $ \\ 
 $ ( \Rdiamond E1G31Inv(X) \rightarrow  \Rbox E1G31Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1L38(X) \rightarrow  \Rbox PL38) \land $ \\ 
 $ ( \Rdiamond E1G21(X) \rightarrow  \Rbox PG21) \land $ \\ 
 $ ( \Rdiamond E2G32(X) \rightarrow  \Rbox E2G32(X)) \land $ \\ 
 $ ( \Rdiamond E1G12Inv(X) \rightarrow  \Rbox E1G12Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1G43Inv(X) \rightarrow  \Rbox E1G43Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1L48Inv(X) \rightarrow  \Rbox PinvL48) \land $ \\ 
 $ ( \Rdiamond E1L36(X) \rightarrow  \Rbox PL36) \land $ \\ 
 $ ( \Rdiamond E1L9Inv(X) \rightarrow  \Rbox PinvL9) \land $ \\ 
 $ ( \Rdiamond E1L14Inv(X) \rightarrow  \Rbox PinvL14) \land $ \\ 
 $ ( \Rdiamond E1G12(X) \rightarrow  \Rbox E1G12(X)) \land $ \\ 
 $ ( \Rdiamond E1L22(X) \rightarrow  \Rbox PL22) \land $ \\ 
 $ ( \Rdiamond E1G2(X) \rightarrow  \Rbox PG2) \land $ \\ 
 $ ( \Rdiamond E1G48Inv(X) \rightarrow  \Rbox E1G48Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1L2(X) \rightarrow  \Rbox PL2) \land $ \\ 
 $ ( \Rdiamond E1G43(X) \rightarrow  \Rbox E1G43(X)) \land $ \\ 
 $ ( \Rdiamond E1L23Inv(X) \rightarrow  \Rbox PinvL23) \land $ \\ 
 $ ( \Rdiamond E2G20(X) \rightarrow  \Rbox E2G20(X)) \land $ \\ 
 $ ( \Rdiamond E1G28(X) \rightarrow  \Rbox PG28) \land $ \\ 
 $ ( \Rdiamond E1L17Inv(X) \rightarrow  \Rbox PinvL17) \land $ \\ 
 $ ( \Rdiamond E1L13(X) \rightarrow  \Rbox PL13) \land $ \\ 
 $ ( \Rdiamond E1G12(X) \rightarrow  \Rbox PG12) \land $ \\ 
 $ ( \Rdiamond E3G22(X) \rightarrow  \Rbox E3G22(X)) \land $ \\ 
 $ ( \Rdiamond E1G37Inv(X) \rightarrow  \Rbox PinvG37) \land $ \\ 
 $ ( \Rdiamond E1L19(X) \rightarrow  \Rbox PL19) \land $ \\ 
 $ ( \Rdiamond E1G45Inv(X) \rightarrow  \Rbox E1G45Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1L1(X) \rightarrow  \Rbox PL1) \land $ \\ 
 $ ( \Rdiamond E1G31Inv(X) \rightarrow  \Rbox PinvG31) \land $ \\ 
 $ ( \Rdiamond E1L4(X) \rightarrow  \Rbox PL4) \land $ \\ 
 $ ( \Rdiamond E1G15(X) \rightarrow  \Rbox PG15) \land $ \\ 
 $ ( \Rdiamond E1L31(X) \rightarrow  \Rbox PL31) \land $ \\ 
 $ ( \Rdiamond E1L18(X) \rightarrow  \Rbox PL18) \land $ \\ 
 $ ( \Rdiamond E1G33Inv(X) \rightarrow  \Rbox PinvG33) \land $ \\ 
 $ ( \Rdiamond E1L4Inv(X) \rightarrow  \Rbox PinvL4) \land $ \\ 
 $ ( \Rdiamond E1L47(X) \rightarrow  \Rbox PL47) \land $ \\ 
 $ ( \Rdiamond E1L36Inv(X) \rightarrow  \Rbox PinvL36) \land $ \\ 
 $ ( \Rdiamond E1L12(X) \rightarrow  \Rbox PL12) \land $ \\ 
 $ ( \Rdiamond E1G33(X) \rightarrow  \Rbox E1G33(X)) \land $ \\ 
 $ ( \Rdiamond E1G20Inv(X) \rightarrow  \Rbox E1G20Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1L10(X) \rightarrow  \Rbox PL10) \land $ \\ 
 $ ( \Rdiamond E1G12Inv(X) \rightarrow  \Rbox PinvG12) \land $ \\ 
 $ ( \Rdiamond E1G18(X) \rightarrow  \Rbox E1G18(X)) \land $ \\ 
 $ ( \Rdiamond E2G47(X) \rightarrow  \Rbox E2G47(X)) \land $ \\ 
 $ ( \Rdiamond E1L30Inv(X) \rightarrow  \Rbox PinvL30) \land $ \\ 
 $ ( \Rdiamond E1G18(X) \rightarrow  \Rbox PG18) \land $ \\ 
 $ ( \Rdiamond E1L5(X) \rightarrow  \Rbox PL5) \land $ \\ 
 $ ( \Rdiamond E1G3Inv(X) \rightarrow  \Rbox PinvG3) \land $ \\ 
 $ ( \Rdiamond E1L34(X) \rightarrow  \Rbox PL34) \land $ \\ 
 $ ( \Rdiamond E3G4(X) \rightarrow  \Rbox E3G4(X)) \land $ \\ 
 $ ( \Rdiamond E1G36Inv(X) \rightarrow  \Rbox PinvG36) \land $ \\ 
 $ ( \Rdiamond E1L21Inv(X) \rightarrow  \Rbox PinvL21) \land $ \\ 
 $ ( \Rdiamond E3G13(X) \rightarrow  \Rbox E3G13(X)) \land $ \\ 
 $ ( \Rdiamond E1G40Inv(X) \rightarrow  \Rbox E1G40Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1G36(X) \rightarrow  \Rbox PG36) \land $ \\ 
 $ ( \Rdiamond E1L20(X) \rightarrow  \Rbox PL20) \land $ \\ 
 $ ( \Rdiamond E1G30(X) \rightarrow  \Rbox PG30) \land $ \\ 
 $ ( \Rdiamond E1G2Inv(X) \rightarrow  \Rbox PinvG2) \land $ \\ 
 $ ( \Rdiamond E1G44Inv(X) \rightarrow  \Rbox PinvG44) \land $ \\ 
 $ ( \Rdiamond E1G42(X) \rightarrow  \Rbox E1G42(X)) \land $ \\ 
 $ ( \Rdiamond E3G42(X) \rightarrow  \Rbox E3G42(X)) \land $ \\ 
 $ ( \Rdiamond E1L43Inv(X) \rightarrow  \Rbox PinvL43) \land $ \\ 
 $ ( \Rdiamond E1G31(X) \rightarrow  \Rbox E1G31(X)) \land $ \\ 
 $ ( \Rdiamond E1G19Inv(X) \rightarrow  \Rbox E1G19Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1G10Inv(X) \rightarrow  \Rbox PinvG10) \land $ \\ 
 $ ( \Rdiamond E1G29(X) \rightarrow  \Rbox PG29) \land $ \\ 
 $ ( \Rdiamond E1G27(X) \rightarrow  \Rbox E1G27(X)) \land $ \\ 
 $ ( \Rdiamond E1G47(X) \rightarrow  \Rbox E1G47(X)) \land $ \\ 
 $ ( \Rdiamond E3G40(X) \rightarrow  \Rbox E3G40(X)) \land $ \\ 
 $ ( \Rdiamond E1G29Inv(X) \rightarrow  \Rbox E1G29Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1G41Inv(X) \rightarrow  \Rbox E1G41Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1L29Inv(X) \rightarrow  \Rbox PinvL29) \land $ \\ 
 $ ( \Rdiamond E1G25Inv(X) \rightarrow  \Rbox E1G25Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1L13Inv(X) \rightarrow  \Rbox PinvL13) \land $ \\ 
 $ ( \Rdiamond E1L28(X) \rightarrow  \Rbox PL28) \land $ \\ 
 $ ( \Rdiamond E1L37Inv(X) \rightarrow  \Rbox PinvL37) \land $ \\ 
 $ ( \Rdiamond E1G17(X) \rightarrow  \Rbox PG17) \land $ \\ 
 $ ( \Rdiamond E3G48(X) \rightarrow  \Rbox E3G48(X)) \land $ \\ 
 $ ( \Rdiamond E1G1Inv(X) \rightarrow  \Rbox PinvG1) \land $ \\ 
 $ ( \Rdiamond E1G13Inv(X) \rightarrow  \Rbox E1G13Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1G20(X) \rightarrow  \Rbox E1G20(X)) \land $ \\ 
 $ ( \Rdiamond E1G35Inv(X) \rightarrow  \Rbox E1G35Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1L26Inv(X) \rightarrow  \Rbox PinvL26) \land $ \\ 
 $ ( \Rdiamond E3G26(X) \rightarrow  \Rbox E3G26(X)) \land $ \\ 
 $ ( \Rdiamond E1G4(X) \rightarrow  \Rbox PG4) \land $ \\ 
 $ ( \Rdiamond E1L33Inv(X) \rightarrow  \Rbox PinvL33) \land $ \\ 
 $ ( \Rdiamond E1L27Inv(X) \rightarrow  \Rbox PinvL27) \land $ \\ 
 $ ( \Rdiamond E1G5Inv(X) \rightarrow  \Rbox PinvG5) \land $ \\ 
 $ ( \Rdiamond E3G31(X) \rightarrow  \Rbox E3G31(X)) \land $ \\ 
 $ ( \Rdiamond E1L29(X) \rightarrow  \Rbox PL29) \land $ \\ 
 $ ( \Rdiamond E1L44(X) \rightarrow  \Rbox PL44) \land $ \\ 
 $ ( \Rdiamond E3G23(X) \rightarrow  \Rbox E3G23(X)) \land $ \\ 
 $ ( \Rdiamond E1L18Inv(X) \rightarrow  \Rbox PinvL18) \land $ \\ 
 $ ( \Rdiamond E1G26Inv(X) \rightarrow  \Rbox PinvG26) \land $ \\ 
 $ ( \Rdiamond E1L32(X) \rightarrow  \Rbox PL32) \land $ \\ 
 $ ( \Rdiamond E2G23(X) \rightarrow  \Rbox E2G23(X)) \land $ \\ 
 $ ( \Rdiamond E1G26(X) \rightarrow  \Rbox PG26) \land $ \\ 
 $ ( \Rdiamond E1G31(X) \rightarrow  \Rbox PG31) \land $ \\ 
 $ ( \Rdiamond E1L40Inv(X) \rightarrow  \Rbox PinvL40) \land $ \\ 
 $ ( \Rdiamond E1G35(X) \rightarrow  \Rbox E1G35(X)) \land $ \\ 
 $ ( \Rdiamond E1G32(X) \rightarrow  \Rbox PG32) \land $ \\ 
 $ ( \Rdiamond E3G21(X) \rightarrow  \Rbox E3G21(X)) \land $ \\ 
 $ ( \Rdiamond E2G3(X) \rightarrow  \Rbox E2G3(X)) \land $ \\ 
 $ ( \Rdiamond E2G16(X) \rightarrow  \Rbox E2G16(X)) \land $ \\ 
 $ ( \Rdiamond E1L39Inv(X) \rightarrow  \Rbox PinvL39) \land $ \\ 
 $ ( \Rdiamond E1L0Inv(X) \rightarrow  \Rbox PinvL0) \land $ \\ 
 $ ( \Rdiamond E2G37(X) \rightarrow  \Rbox E2G37(X)) \land $ \\ 
 $ ( \Rdiamond E1G23(X) \rightarrow  \Rbox E1G23(X)) \land $ \\ 
 $ ( \Rdiamond E2G48(X) \rightarrow  \Rbox E2G48(X))) \land $ \\ 
 $ (PL33 \rightarrow E1L33Inv(dL33Inv)) \land $ \\ 
 $ (PinvL16 \rightarrow E1L16(dL16)) \land $ \\ 
 $ (PinvL36 \rightarrow E1L36(dL36)) \land $ \\ 
 $ (PG39 \rightarrow E1G39Inv(dG39Inv)) \land $ \\ 
 $ (PinvL7 \rightarrow E1L7(dL7)) \land $ \\ 
 $ (PG43 \rightarrow E1G43Inv(dG43Inv)) \land $ \\ 
 $ (PinvL21 \rightarrow E1L21(dL21)) \land $ \\ 
 $ (PinvL9 \rightarrow E1L9(dL9)) \land $ \\ 
 $ (PinvG22 \rightarrow E1G22(dG22)) \land $ \\ 
 $ (PG31 \rightarrow E1G31Inv(dG31Inv)) \land $ \\ 
 $ (PinvG40 \rightarrow E1G40(dG40)) \land $ \\ 
 $ (PinvL42 \rightarrow E1L42(dL42)) \land $ \\ 
 $ (PinvL35 \rightarrow E1L35(dL35)) \land $ \\ 
 $ (PG45 \rightarrow E1G45Inv(dG45Inv)) \land $ \\ 
 $ (PG30 \rightarrow E1G30Inv(dG30Inv)) \land $ \\ 
 $ (PinvG39 \rightarrow E1G39(dG39)) \land $ \\ 
 $ (PinvG31 \rightarrow E1G31(dG31)) \land $ \\ 
 $ (PinvL28 \rightarrow E1L28(dL28)) \land $ \\ 
 $ (PinvL0 \rightarrow E1L0(dL0)) \land $ \\ 
 $ (PG8 \rightarrow E1G8Inv(dG8Inv)) \land $ \\ 
 $ (PinvG46 \rightarrow E1G46(dG46)) \land $ \\ 
 $ (PL22 \rightarrow E1L22Inv(dL22Inv)) \land $ \\ 
 $ (PinvG47 \rightarrow E1G47(dG47)) \land $ \\ 
 $ (PinvL45 \rightarrow E1L45(dL45)) \land $ \\ 
 $ (PL26 \rightarrow E1L26Inv(dL26Inv)) \land $ \\ 
 $ (PinvG36 \rightarrow E1G36(dG36)) \land $ \\ 
 $ (PinvG42 \rightarrow E1G42(dG42)) \land $ \\ 
 $ (PinvL3 \rightarrow E1L3(dL3)) \land $ \\ 
 $ (PinvG19 \rightarrow E1G19(dG19)) \land $ \\ 
 $ (PinvG15 \rightarrow E1G15(dG15)) \land $ \\ 
 $ (PinvL30 \rightarrow E1L30(dL30)) \land $ \\ 
 $ (PG3 \rightarrow E1G3Inv(dG3Inv)) \land $ \\ 
 $ (PL2 \rightarrow E1L2Inv(dL2Inv)) \land $ \\ 
 $ (PinvG12 \rightarrow E1G12(dG12)) \land $ \\ 
 $ (PinvG23 \rightarrow E1G23(dG23)) \land $ \\ 
 $ (PL15 \rightarrow E1L15Inv(dL15Inv)) \land $ \\ 
 $ (PinvG17 \rightarrow E1G17(dG17)) \land $ \\ 
 $ (PinvL20 \rightarrow E1L20(dL20)) \land $ \\ 
 $ (PinvL12 \rightarrow E1L12(dL12)) \land $ \\ 
 $ (PL0 \rightarrow E1L0Inv(dL0Inv)) \land $ \\ 
 $ (PL4 \rightarrow E1L4Inv(dL4Inv)) \land $ \\ 
 $ (PG0 \rightarrow E1G0Inv(dG0Inv)) \land $ \\ 
 $ (PG48 \rightarrow E1G48Inv(dG48Inv)) \land $ \\ 
 $ (PinvL41 \rightarrow E1L41(dL41)) \land $ \\ 
 $ (PinvG4 \rightarrow E1G4(dG4)) \land $ \\ 
 $ (PinvG25 \rightarrow E1G25(dG25)) \land $ \\ 
 $ (PinvG9 \rightarrow E1G9(dG9)) \land $ \\ 
 $ (PinvL22 \rightarrow E1L22(dL22)) \land $ \\ 
 $ (PG5 \rightarrow E1G5Inv(dG5Inv)) \land $ \\ 
 $ (PinvL33 \rightarrow E1L33(dL33)) \land $ \\ 
 $ (PG38 \rightarrow E1G38Inv(dG38Inv)) \land $ \\ 
 $ (PinvL11 \rightarrow E1L11(dL11)) \land $ \\ 
 $ (PG1 \rightarrow E1G1Inv(dG1Inv)) \land $ \\ 
 $ (PinvG41 \rightarrow E1G41(dG41)) \land $ \\ 
 $ (PinvG28 \rightarrow E1G28(dG28)) \land $ \\ 
 $ (PinvL46 \rightarrow E1L46(dL46)) \land $ \\ 
 $ (PinvL5 \rightarrow E1L5(dL5)) \land $ \\ 
 $ (PL49 \rightarrow E1L49Inv(dL49Inv)) \land $ \\ 
 $ (PinvL25 \rightarrow E1L25(dL25)) \land $ \\ 
 $ (PinvG20 \rightarrow E1G20(dG20)) \land $ \\ 
 $ (PinvL15 \rightarrow E1L15(dL15)) \land $ \\ 
 $ (PG27 \rightarrow E1G27Inv(dG27Inv)) \land $ \\ 
 $ (PG19 \rightarrow E1G19Inv(dG19Inv)) \land $ \\ 
 $ (PinvL44 \rightarrow E1L44(dL44)) \land $ \\ 
 $ (PinvL6 \rightarrow E1L6(dL6)) \land $ \\ 
 $ (PinvG32 \rightarrow E1G32(dG32)) \land $ \\ 
 $ (PL25 \rightarrow E1L25Inv(dL25Inv)) \land $ \\ 
 $ (PinvG18 \rightarrow E1G18(dG18)) \land $ \\ 
 $ (PinvG33 \rightarrow E1G33(dG33)) \land $ \\ 
 $ (PG12 \rightarrow E1G12Inv(dG12Inv)) \land $ \\ 
 $ (PinvG16 \rightarrow E1G16(dG16)) \land $ \\ 
 $ (PinvL49 \rightarrow E1L49(dL49)) \land $ \\ 
 $ (PinvL13 \rightarrow E1L13(dL13)) \land $ \\ 
 $ (PinvG35 \rightarrow E1G35(dG35)) \land $ \\ 
 $ (PL19 \rightarrow E1L19Inv(dL19Inv)) \land $ \\ 
 $ (PinvL27 \rightarrow E1L27(dL27)) \land $ \\ 
 $ (PG26 \rightarrow E1G26Inv(dG26Inv)) \land $ \\ 
 $ (PL43 \rightarrow E1L43Inv(dL43Inv)) \land $ \\ 
 $ (PG9 \rightarrow E1G9Inv(dG9Inv)) \land $ \\ 
 $ (PG46 \rightarrow E1G46Inv(dG46Inv)) \land $ \\ 
 $ (PL27 \rightarrow E1L27Inv(dL27Inv)) \land $ \\ 
 $ (PinvL32 \rightarrow E1L32(dL32)) \land $ \\ 
 $ (PG33 \rightarrow E1G33Inv(dG33Inv)) \land $ \\ 
 $ (PG41 \rightarrow E1G41Inv(dG41Inv)) \land $ \\ 
 $ (PinvG27 \rightarrow E1G27(dG27)) \land $ \\ 
 $ (PG34 \rightarrow E1G34Inv(dG34Inv)) \land $ \\ 
 $ (PL38 \rightarrow E1L38Inv(dL38Inv)) \land $ \\ 
 $ (PG22 \rightarrow E1G22Inv(dG22Inv)) \land $ \\ 
 $ (PinvL43 \rightarrow E1L43(dL43)) \land $ \\ 
 $ (PL42 \rightarrow E1L42Inv(dL42Inv)) \land $ \\ 
 $ (PG16 \rightarrow E1G16Inv(dG16Inv)) \land $ \\ 
 $ (PinvG26 \rightarrow E1G26(dG26)) \land $ \\ 
 $ (PG32 \rightarrow E1G32Inv(dG32Inv)) \land $ \\ 
 $ (PL18 \rightarrow E1L18Inv(dL18Inv)) \land $ \\ 
 $ (PG35 \rightarrow E1G35Inv(dG35Inv)) \land $ \\ 
 $ (PL36 \rightarrow E1L36Inv(dL36Inv)) \land $ \\ 
 $ (PinvL47 \rightarrow E1L47(dL47)) \land $ \\ 
 $ (PG7 \rightarrow E1G7Inv(dG7Inv)) \land $ \\ 
 $ (PinvL26 \rightarrow E1L26(dL26)) \land $ \\ 
 $ (PG15 \rightarrow E1G15Inv(dG15Inv)) \land $ \\ 
 $ (PL48 \rightarrow E1L48Inv(dL48Inv)) \land $ \\ 
 $ (PinvG3 \rightarrow E1G3(dG3)) \land $ \\ 
 $ (PG28 \rightarrow E1G28Inv(dG28Inv)) \land $ \\ 
 $ (PinvL29 \rightarrow E1L29(dL29)) \land $ \\ 
 $ (PL13 \rightarrow E1L13Inv(dL13Inv)) \land $ \\ 
 $ (PinvG5 \rightarrow E1G5(dG5)) \land $ \\ 
 $ (PinvL18 \rightarrow E1L18(dL18)) \land $ \\ 
 $ (PL3 \rightarrow E1L3Inv(dL3Inv)) \land $ \\ 
 $ (PL1 \rightarrow E1L1Inv(dL1Inv)) \land $ \\ 
 $ (PL24 \rightarrow E1L24Inv(dL24Inv)) \land $ \\ 
 $ (PL40 \rightarrow E1L40Inv(dL40Inv)) \land $ \\ 
 $ (PG17 \rightarrow E1G17Inv(dG17Inv)) \land $ \\ 
 $ (PinvG45 \rightarrow E1G45(dG45)) \land $ \\ 
 $ (PinvL39 \rightarrow E1L39(dL39)) \land $ \\ 
 $ (PinvG13 \rightarrow E1G13(dG13)) \land $ \\ 
 $ (PG47 \rightarrow E1G47Inv(dG47Inv)) \land $ \\ 
 $ (PG20 \rightarrow E1G20Inv(dG20Inv)) \land $ \\ 
 $ (PinvL19 \rightarrow E1L19(dL19)) \land $ \\ 
 $ (PL45 \rightarrow E1L45Inv(dL45Inv)) \land $ \\ 
 $ (PinvG8 \rightarrow E1G8(dG8)) \land $ \\ 
 $ (PinvG30 \rightarrow E1G30(dG30)) \land $ \\ 
 $ (PG18 \rightarrow E1G18Inv(dG18Inv)) \land $ \\ 
 $ (PinvL17 \rightarrow E1L17(dL17)) \land $ \\ 
 $ (PG4 \rightarrow E1G4Inv(dG4Inv)) \land $ \\ 
 $ (PL29 \rightarrow E1L29Inv(dL29Inv)) \land $ \\ 
 $ (PL46 \rightarrow E1L46Inv(dL46Inv)) \land $ \\ 
 $ (PinvL48 \rightarrow E1L48(dL48)) \land $ \\ 
 $ (PG25 \rightarrow E1G25Inv(dG25Inv)) \land $ \\ 
 $ (PL39 \rightarrow E1L39Inv(dL39Inv)) \land $ \\ 
 $ (PinvL24 \rightarrow E1L24(dL24)) \land $ \\ 
 $ (PinvG10 \rightarrow E1G10(dG10)) \land $ \\ 
 $ (PL17 \rightarrow E1L17Inv(dL17Inv)) \land $ \\ 
 $ (PL10 \rightarrow E1L10Inv(dL10Inv)) \land $ \\ 
 $ (PinvL31 \rightarrow E1L31(dL31)) \land $ \\ 
 $ (PL37 \rightarrow E1L37Inv(dL37Inv)) \land $ \\ 
 $ (PG36 \rightarrow E1G36Inv(dG36Inv)) \land $ \\ 
 $ (PinvG37 \rightarrow E1G37(dG37)) \land $ \\ 
 $ (PL11 \rightarrow E1L11Inv(dL11Inv)) \land $ \\ 
 $ (PinvL34 \rightarrow E1L34(dL34)) \land $ \\ 
 $ (PG42 \rightarrow E1G42Inv(dG42Inv)) \land $ \\ 
 $ (PG2 \rightarrow E1G2Inv(dG2Inv)) \land $ \\ 
 $ (PL5 \rightarrow E1L5Inv(dL5Inv)) \land $ \\ 
 $ (PinvL2 \rightarrow E1L2(dL2)) \land $ \\ 
 $ (PinvL37 \rightarrow E1L37(dL37)) \land $ \\ 
 $ (PL12 \rightarrow E1L12Inv(dL12Inv)) \land $ \\ 
 $ (PL20 \rightarrow E1L20Inv(dL20Inv)) \land $ \\ 
 $ (PL14 \rightarrow E1L14Inv(dL14Inv)) \land $ \\ 
 $ (PinvG38 \rightarrow E1G38(dG38)) \land $ \\ 
 $ (PL30 \rightarrow E1L30Inv(dL30Inv)) \land $ \\ 
 $ (PinvG21 \rightarrow E1G21(dG21)) \land $ \\ 
 $ (PinvG2 \rightarrow E1G2(dG2)) \land $ \\ 
 $ (PinvL1 \rightarrow E1L1(dL1)) \land $ \\ 
 $ (PinvG14 \rightarrow E1G14(dG14)) \land $ \\ 
 $ (PG14 \rightarrow E1G14Inv(dG14Inv)) \land $ \\ 
 $ (PL28 \rightarrow E1L28Inv(dL28Inv)) \land $ \\ 
 $ (PinvL38 \rightarrow E1L38(dL38)) \land $ \\ 
 $ (PinvG0 \rightarrow E1G0(dG0)) \land $ \\ 
 $ (PinvL10 \rightarrow E1L10(dL10)) \land $ \\ 
 $ (PL31 \rightarrow E1L31Inv(dL31Inv)) \land $ \\ 
 $ (PinvG43 \rightarrow E1G43(dG43)) \land $ \\ 
 $ (PinvG44 \rightarrow E1G44(dG44)) \land $ \\ 
 $ (PL7 \rightarrow E1L7Inv(dL7Inv)) \land $ \\ 
 $ (PG40 \rightarrow E1G40Inv(dG40Inv)) \land $ \\ 
 $ (PinvL40 \rightarrow E1L40(dL40)) \land $ \\ 
 $ (PL16 \rightarrow E1L16Inv(dL16Inv)) \land $ \\ 
 $ (PinvL23 \rightarrow E1L23(dL23)) \land $ \\ 
 $ (PL41 \rightarrow E1L41Inv(dL41Inv)) \land $ \\ 
 $ (PL44 \rightarrow E1L44Inv(dL44Inv)) \land $ \\ 
 $ (PinvL4 \rightarrow E1L4(dL4)) \land $ \\ 
 $ (PL47 \rightarrow E1L47Inv(dL47Inv)) \land $ \\ 
 $ (PL21 \rightarrow E1L21Inv(dL21Inv)) \land $ \\ 
 $ (PL34 \rightarrow E1L34Inv(dL34Inv)) \land $ \\ 
 $ (PinvG48 \rightarrow E1G48(dG48)) \land $ \\ 
 $ (PG13 \rightarrow E1G13Inv(dG13Inv)) \land $ \\ 
 $ (PL9 \rightarrow E1L9Inv(dL9Inv)) \land $ \\ 
 $ (PinvG1 \rightarrow E1G1(dG1)) \land $ \\ 
 $ (PinvG7 \rightarrow E1G7(dG7)) \land $ \\ 
 $ (PL32 \rightarrow E1L32Inv(dL32Inv)) \land $ \\ 
 $ (PL6 \rightarrow E1L6Inv(dL6Inv)) \land $ \\ 
 $ (PinvG29 \rightarrow E1G29(dG29)) \land $ \\ 
 $ (PL23 \rightarrow E1L23Inv(dL23Inv)) \land $ \\ 
 $ (PinvL14 \rightarrow E1L14(dL14)) \land $ \\ 
 $ (PG44 \rightarrow E1G44Inv(dG44Inv)) \land $ \\ 
 $ (PG21 \rightarrow E1G21Inv(dG21Inv)) \land $ \\ 
 $ (PG10 \rightarrow E1G10Inv(dG10Inv)) \land $ \\ 
 $ (PL35 \rightarrow E1L35Inv(dL35Inv)) \land $ \\ 
 $ (PG29 \rightarrow E1G29Inv(dG29Inv)) \land $ \\ 
 $ (PinvG34 \rightarrow E1G34(dG34)) \land $ \\ 
 $ (PG37 \rightarrow E1G37Inv(dG37Inv)) \land $ \\ 
 $ (PG23 \rightarrow E1G23Inv(dG23Inv)))$ 
\end{document}