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