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


$((PG3 \rightarrow E1G3Inv(dG3Inv)) \land $ \\ 
 $ (PL1 \rightarrow E1L1Inv(dL1Inv)) \land $ \\ 
 $ (PinvG0 \rightarrow E1G0(dG0)) \land $ \\ 
 $ (PL2 \rightarrow E1L2Inv(dL2Inv)) \land $ \\ 
 $ (PG0 \rightarrow E1G0Inv(dG0Inv)) \land $ \\ 
 $ (PinvL3 \rightarrow E1L3(dL3)) \land $ \\ 
 $ (PinvG1 \rightarrow E1G1(dG1)) \land $ \\ 
 $ (PinvL2 \rightarrow E1L2(dL2)) \land $ \\ 
 $ (PinvL1 \rightarrow E1L1(dL1)) \land $ \\ 
 $ (PL0 \rightarrow E1L0Inv(dL0Inv)) \land $ \\ 
 $ (PG1 \rightarrow E1G1Inv(dG1Inv)) \land $ \\ 
 $ (PinvL0 \rightarrow E1L0(dL0)) \land $ \\ 
 $ (PL3 \rightarrow E1L3Inv(dL3Inv)) \land $ \\ 
 $ (PinvG2 \rightarrow E1G2(dG2)) \land $ \\ 
 $ (PinvG3 \rightarrow E1G3(dG3)) \land $ \\ 
 $  \forall X. ( \Rbox (( \Rdiamond  \Rbox  \Rbox  \Rbox E1L2(X) \rightarrow (C0(X) \land $ \\ 
 $ E2G3(X) \land $ \\ 
 $ C3(X))) \land $ \\ 
 $ ( \Rbox (E3L3(X) \land $ \\ 
 $  \Rnext E1L3(X)) \rightarrow  \Rbox (C2(X) \land $ \\ 
 $  \Rbox C2(X))) \land $ \\ 
 $ ( \Rbox (E1L3(X) \land $ \\ 
 $  \Rnext E1G0(X)) \rightarrow (E2G3(X) \land $ \\ 
 $  \Rdiamond  \Rdiamond C3(X))) \land $ \\ 
 $ (( \Rnext E1L0(X) \land $ \\ 
 $  \Rnext C0(X)) \rightarrow  \Rbox  \Rdiamond  \Rdiamond  \Rnext E3L0(X)) \land $ \\ 
 $ (( \Rnext C2(X) \land $ \\ 
 $  \Rnext E2L2(X)) \rightarrow  \Rbox  \Rbox (C0(X) \land $ \\ 
 $ E3L1(X))) \land $ \\ 
 $ (( \Rnext E1G2(X) \land $ \\ 
 $  \Rbox E2L3(X)) \rightarrow  \Rdiamond (C3(X) \land $ \\ 
 $  \Rnext C0(X))) \land $ \\ 
 $ ( \Rdiamond (E3G3(X) \land $ \\ 
 $  \Rdiamond E2G3(X)) \rightarrow (E3L0(X) \land $ \\ 
 $  \Rbox  \Rbox E3L1(X))) \land $ \\ 
 $ ((C0(X) \land $ \\ 
 $  \Rdiamond  \Rnext E1L3(X)) \rightarrow  \Rdiamond (E1L1(X) \land $ \\ 
 $  \Rnext C1(X))) \land $ \\ 
 $ (( \Rnext E3L0(X) \land $ \\ 
 $  \Rbox C2(X)) \rightarrow  \Rdiamond  \Rbox (C0(X) \land $ \\ 
 $ E1G2(X))) \land $ \\ 
 $ ((E1G2(X) \land $ \\ 
 $ E2G3(X) \land $ \\ 
 $ C1(X)) \rightarrow ( \Rdiamond E3L0(X) \land $ \\ 
 $  \Rbox E2L3(X))) \land $ \\ 
 $ ( \Rdiamond (E1G3(X) \land $ \\ 
 $  \Rnext C3(X)) \rightarrow  \Rbox  \Rdiamond  \Rdiamond  \Rnext C0(X)) \land $ \\ 
 $ ( \Rbox  \Rdiamond  \Rbox  \Rbox E2G0(X) \rightarrow  \Rbox (C3(X) \land $ \\ 
 $  \Rnext E2L0(X))) \land $ \\ 
 $ (( \Rbox C0(X) \land $ \\ 
 $  \Rdiamond C3(X)) \rightarrow  \Rbox  \Rbox  \Rbox  \Rbox C2(X)) \land $ \\ 
 $ ((E3G3(X) \land $ \\ 
 $  \Rbox  \Rdiamond E1G1(X)) \rightarrow  \Rbox  \Rbox (C0(X) \land $ \\ 
 $ E1L3(X))) \land $ \\ 
 $ ( \Rdiamond  \Rbox (E3L1(X) \land $ \\ 
 $ E2L0(X)) \rightarrow ( \Rdiamond C1(X) \land $ \\ 
 $  \Rbox E2L0(X))) \land $ \\ 
 $ (E2L3(X) \rightarrow E1L3(X)) \land $ \\ 
 $ (E3L3(X) \rightarrow E2L3(X)) \land $ \\ 
 $ (E2G3(X) \rightarrow E1G3(X)) \land $ \\ 
 $ (E2L0(X) \rightarrow E1L0(X)) \land $ \\ 
 $ (E3G3(X) \rightarrow E2G3(X)) \land $ \\ 
 $ (E3L0(X) \rightarrow E2L0(X)) \land $ \\ 
 $ (E2G0(X) \rightarrow E1G0(X)) \land $ \\ 
 $ (E2L2(X) \rightarrow E1L2(X)) \land $ \\ 
 $ (E3L1(X) \rightarrow E1L1(X))) \land $ \\ 
 $ ( \Rdiamond E1L0(X) \rightarrow  \Rbox PL0) \land $ \\ 
 $ ( \Rdiamond E1L2Inv(X) \rightarrow  \Rbox PinvL2) \land $ \\ 
 $ ( \Rdiamond E2G0(X) \rightarrow  \Rbox E2G0(X)) \land $ \\ 
 $ ( \Rdiamond E1G2(X) \rightarrow  \Rbox E1G2(X)) \land $ \\ 
 $ ( \Rdiamond E1L1Inv(X) \rightarrow  \Rbox PinvL1) \land $ \\ 
 $ ( \Rdiamond E1G1(X) \rightarrow  \Rbox PG1) \land $ \\ 
 $ ( \Rdiamond E1G2(X) \rightarrow  \Rbox PG2) \land $ \\ 
 $ ( \Rdiamond E1L3(X) \rightarrow  \Rbox PL3) \land $ \\ 
 $ ( \Rdiamond E1G3(X) \rightarrow  \Rbox E1G3(X)) \land $ \\ 
 $ ( \Rdiamond E1G2Inv(X) \rightarrow  \Rbox E1G2Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1G2Inv(X) \rightarrow  \Rbox PinvG2) \land $ \\ 
 $ ( \Rdiamond E3G3(X) \rightarrow  \Rbox E3G3(X)) \land $ \\ 
 $ ( \Rdiamond E1L1(X) \rightarrow  \Rbox PL1) \land $ \\ 
 $ ( \Rdiamond E1G0Inv(X) \rightarrow  \Rbox PinvG0) \land $ \\ 
 $ ( \Rdiamond E1G1Inv(X) \rightarrow  \Rbox PinvG1) \land $ \\ 
 $ ( \Rdiamond E1G3Inv(X) \rightarrow  \Rbox PinvG3) \land $ \\ 
 $ ( \Rdiamond E1G3(X) \rightarrow  \Rbox PG3) \land $ \\ 
 $ ( \Rdiamond E1L2(X) \rightarrow  \Rbox PL2) \land $ \\ 
 $ ( \Rdiamond E1L3Inv(X) \rightarrow  \Rbox PinvL3) \land $ \\ 
 $ ( \Rdiamond E1G0Inv(X) \rightarrow  \Rbox E1G0Inv(X)) \land $ \\ 
 $ ( \Rdiamond E2G3(X) \rightarrow  \Rbox E2G3(X)) \land $ \\ 
 $ ( \Rdiamond E1G0(X) \rightarrow  \Rbox PG0) \land $ \\ 
 $ ( \Rdiamond E1G1Inv(X) \rightarrow  \Rbox E1G1Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1G0(X) \rightarrow  \Rbox E1G0(X)) \land $ \\ 
 $ ( \Rdiamond E1G1(X) \rightarrow  \Rbox E1G1(X)) \land $ \\ 
 $ ( \Rdiamond E1L0Inv(X) \rightarrow  \Rbox PinvL0) \land $ \\ 
 $ ( \Rdiamond E1G3Inv(X) \rightarrow  \Rbox E1G3Inv(X))) \land $ \\ 
 $ (PG2 \rightarrow E1G2Inv(dG2Inv)) \land $ \\ 
 $  \Rnext  \Rnext C1(a85) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a42_a64) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a65) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a88_a49) \land $ \\ 
 $  \Rnext  \Rnext C2(a36) \land $ \\ 
 $  \Rnext C3(a26_a84) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a24) \land $ \\ 
 $  \Rnext  \Rnext C1(a12_a58) \land $ \\ 
 $  \Rnext E3L3Inv(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a38) \land $ \\ 
 $  \Rnext E3L0Inv(a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a12_a58) \land $ \\ 
 $  \Rnext  \Rnext C0(a11) \land $ \\ 
 $  \Rnext  \Rnext E3L3(a30) \land $ \\ 
 $  \Rnext  \Rnext C0(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a42_a64) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a36) \land $ \\ 
 $  \Rnext E3L0(a72) \land $ \\ 
 $  \Rnext E3L1(a42_a64) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L3(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a88_a49) \land $ \\ 
 $  \Rnext E3L1(a38) \land $ \\ 
 $  \Rnext E3L3Inv(a11) \land $ \\ 
 $  \Rnext C2(a85) \land $ \\ 
 $  \Rnext C3(a88_a49) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a42_a64) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a11) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a72) \land $ \\ 
 $  \Rnext E3L3Inv(a97_a63) \land $ \\ 
 $  \Rnext E2L2Inv(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L3(a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a42_a64) \land $ \\ 
 $  \Rnext E3L1Inv(a38) \land $ \\ 
 $  \Rnext E3L3(a89) \land $ \\ 
 $  \Rnext E3L3Inv(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a42_a64) \land $ \\ 
 $  \Rnext  \Rnext C2(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a88_a49) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L3(a12_a58) \land $ \\ 
 $  \Rnext  \Rnext C2(a26_a84) \land $ \\ 
 $  \Rnext E3L3Inv(a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a97_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L3Inv(a11) \land $ \\ 
 $  \Rnext E3L1(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a42_a64) \land $ \\ 
 $  \Rnext C0(a24) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L3Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a88_a49) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a72) \land $ \\ 
 $  \Rnext E2L2Inv(a42_a64) \land $ \\ 
 $  \Rnext  \Rnext C3(a93) \land $ \\ 
 $  \Rnext E2L2(a30) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a88_a49) \land $ \\ 
 $  \Rnext E2L2Inv(a88_a49) \land $ \\ 
 $  \Rnext E2L2Inv(a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L3(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a42_a64) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a99) \land $ \\ 
 $  \Rnext E3L3(a42_a64) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a93) \land $ \\ 
 $  \Rnext  \Rnext C2(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a42_a64) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a30) \land $ \\ 
 $ E1G2Inv(a26_a84) \land $ \\ 
 $ E1G2Inv(a36) \land $ \\ 
 $ E1G2Inv(a85) \land $ \\ 
 $ E1G2Inv(a11) \land $ \\ 
 $ E1G2Inv(a50) \land $ \\ 
 $ E1G2Inv(a72) \land $ \\ 
 $ E1G2Inv(a71) \land $ \\ 
 $ E1G2Inv(a12_a58) \land $ \\ 
 $ E1G2Inv(a97_a63) \land $ \\ 
 $ E1G2Inv(a88_a49) \land $ \\ 
 $ E1G2Inv(a89) \land $ \\ 
 $ E1G2Inv(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $ E1G2Inv(a93) \land $ \\ 
 $ E1G2Inv(a30) \land $ \\ 
 $ E1G2Inv(a24) \land $ \\ 
 $ E1G2Inv(a65) \land $ \\ 
 $ E1G2Inv(a42_a64) \land $ \\ 
 $ E1G2Inv(a99) \land $ \\ 
 $ E1G2Inv(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a30) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a93) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a85) \land $ \\ 
 $  \Rnext E2L2Inv(a26_a84) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a11) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a89) \land $ \\ 
 $  \Rnext C1(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a38) \land $ \\ 
 $  \Rnext  \Rnext C1(a88_a49) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L3(a72) \land $ \\ 
 $  \Rnext  \Rnext C1(a89) \land $ \\ 
 $  \Rnext E3L0Inv(a38) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a12_a58) \land $ \\ 
 $  \Rnext  \Rnext E3L3(a24) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a89) \land $ \\ 
 $  \Rnext E3L3(a99) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a12_a58) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a85) \land $ \\ 
 $  \Rnext C3(a71) \land $ \\ 
 $  \Rnext E3L1(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a50) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a12_a58) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a93) \land $ \\ 
 $  \Rnext E3L3Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a89) \land $ \\ 
 $  \Rnext E2L2Inv(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a11) \land $ \\ 
 $  \Rnext E3L0(a89) \land $ \\ 
 $  \Rnext C1(a89) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a42_a64) \land $ \\ 
 $  \Rnext C2(a24) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a88_a49) \land $ \\ 
 $  \Rnext E3L0Inv(a97_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a65) \land $ \\ 
 $ E1G1Inv(a42_a64) \land $ \\ 
 $ E1G1Inv(a11) \land $ \\ 
 $ E1G1Inv(a36) \land $ \\ 
 $ E1G1Inv(a26_a84) \land $ \\ 
 $ E1G1Inv(a50) \land $ \\ 
 $ E1G1Inv(a89) \land $ \\ 
 $ E1G1Inv(a38) \land $ \\ 
 $ E1G1Inv(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $ E1G1Inv(a93) \land $ \\ 
 $ E1G1Inv(a72) \land $ \\ 
 $ E1G1Inv(a85) \land $ \\ 
 $ E1G1Inv(a99) \land $ \\ 
 $ E1G1Inv(a12_a58) \land $ \\ 
 $ E1G1Inv(a24) \land $ \\ 
 $ E1G1Inv(a71) \land $ \\ 
 $ E1G1Inv(a88_a49) \land $ \\ 
 $ E1G1Inv(a65) \land $ \\ 
 $ E1G1Inv(a30) \land $ \\ 
 $ E1G1Inv(a97_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L3(a88_a49) \land $ \\ 
 $  \Rnext C1(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a42_a64) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a85) \land $ \\ 
 $  \Rnext  \Rnext C3(a38) \land $ \\ 
 $  \Rnext E2L2(a99) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a24) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L3(a42_a64) \land $ \\ 
 $  \Rnext  \Rnext C2(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L3Inv(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L3Inv(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a65) \land $ \\ 
 $  \Rnext  \Rnext E3L3(a42_a64) \land $ \\ 
 $  \Rnext  \Rnext C1(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a65) \land $ \\ 
 $  \Rnext E3L0Inv(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L3(a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext E3L3(a26_a84) \land $ \\ 
 $  \Rnext E3L1(a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a89) \land $ \\ 
 $  \Rnext C0(a93) \land $ \\ 
 $  \Rnext C3(a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L3Inv(a26_a84) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a72) \land $ \\ 
 $  \Rnext  \Rnext E3L3Inv(a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a26_a84) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L3(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a99) \land $ \\ 
 $  \Rnext  \Rnext E3L3(a88_a49) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L3Inv(a99) \land $ \\ 
 $  \Rnext E3L0Inv(a11) \land $ \\ 
 $  \Rnext  \Rnext C2(a97_a63) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L3Inv(a38) \land $ \\ 
 $  \Rnext E3L1(a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a24) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a30) \land $ \\ 
 $  \Rnext  \Rnext E3L3Inv(a97_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a71) \land $ \\ 
 $  \Rnext  \Rnext C1(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a26_a84) \land $ \\ 
 $  \Rnext E3L3Inv(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext E3L1Inv(a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a72) \land $ \\ 
 $  \Rnext C1(a12_a58) \land $ \\ 
 $  \Rnext  \Rnext E3L3Inv(a26_a84) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a99) \land $ \\ 
 $  \Rnext C3(a30) \land $ \\ 
 $  \Rnext E3L0Inv(a24) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a71) \land $ \\ 
 $  \Rnext C2(a71) \land $ \\ 
 $  \Rnext  \Rnext C0(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a24) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a93) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a72) \land $ \\ 
 $  \Rnext  \Rnext C3(a85) \land $ \\ 
 $  \Rnext C0(a97_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L3(a89) \land $ \\ 
 $  \Rnext E2L2(a38) \land $ \\ 
 $  \Rnext  \Rnext E3L3(a97_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L3Inv(a36) \land $ \\ 
 $  \Rnext  \Rnext C1(a42_a64) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext C0(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a26_a84) \land $ \\ 
 $  \Rnext C1(a26_a84) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L3Inv(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext E3L1(a36) \land $ \\ 
 $ E1G3Inv(a97_a63) \land $ \\ 
 $ E1G3Inv(a26_a84) \land $ \\ 
 $ E1G3Inv(a11) \land $ \\ 
 $ E1G3Inv(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $ E1G3Inv(a93) \land $ \\ 
 $ E1G3Inv(a85) \land $ \\ 
 $ E1G3Inv(a99) \land $ \\ 
 $ E1G3Inv(a65) \land $ \\ 
 $ E1G3Inv(a30) \land $ \\ 
 $ E1G3Inv(a42_a64) \land $ \\ 
 $ E1G3Inv(a88_a49) \land $ \\ 
 $ E1G3Inv(a50) \land $ \\ 
 $ E1G3Inv(a36) \land $ \\ 
 $ E1G3Inv(a89) \land $ \\ 
 $ E1G3Inv(a71) \land $ \\ 
 $ E1G3Inv(a24) \land $ \\ 
 $ E1G3Inv(a38) \land $ \\ 
 $ E1G3Inv(a12_a58) \land $ \\ 
 $ E1G3Inv(a72) \land $ \\ 
 $  \Rnext E2L2Inv(a71) \land $ \\ 
 $  \Rnext  \Rnext E3L3Inv(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a30) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a71) \land $ \\ 
 $  \Rnext C2(a36) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a24) \land $ \\ 
 $  \Rnext  \Rnext C3(a11) \land $ \\ 
 $  \Rnext C2(a65) \land $ \\ 
 $  \Rnext E2L2(a85) \land $ \\ 
 $  \Rnext E3L3(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a26_a84) \land $ \\ 
 $  \Rnext C1(a93) \land $ \\ 
 $  \Rnext E3L0Inv(a36) \land $ \\ 
 $  \Rnext E3L3Inv(a71) \land $ \\ 
 $  \Rnext E3L3(a71) \land $ \\ 
 $  \Rnext E3L1(a12_a58) \land $ \\ 
 $  \Rnext  \Rnext C0(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a42_a64) \land $ \\ 
 $  \Rnext  \Rnext E3L3Inv(a38) \land $ \\ 
 $  \Rnext E2L2(a71) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a42_a64) \land $ \\ 
 $  \Rnext  \Rnext C3(a65) \land $ \\ 
 $  \Rnext E3L1Inv(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a30) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a11) \land $ \\ 
 $  \Rnext E3L0(a97_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a26_a84) \land $ \\ 
 $  \Rnext C2(a99) \land $ \\ 
 $  \Rnext C0(a42_a64) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L3(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a24) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a26_a84) \land $ \\ 
 $  \Rnext E2L2Inv(a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a89) \land $ \\ 
 $  \Rnext  \Rnext E3L3Inv(a12_a58) \land $ \\ 
 $  \Rnext E3L0Inv(a89) \land $ \\ 
 $  \Rnext  \Rnext C2(a24) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a24) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a88_a49) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L3Inv(a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a97_a63) \land $ \\ 
 $  \Rnext  \Rnext C1(a71) \land $ \\ 
 $ C3(a38) \land $ \\ 
 $ C3(a50) \land $ \\ 
 $ C3(a36) \land $ \\ 
 $ C3(a11) \land $ \\ 
 $  \Rnext E2L2(a65) \land $ \\ 
 $  \Rnext  \Rnext C0(a12_a58) \land $ \\ 
 $ C3(a71) \land $ \\ 
 $ C3(a26_a84) \land $ \\ 
 $ C3(a99) \land $ \\ 
 $ C3(a89) \land $ \\ 
 $ C3(a30) \land $ \\ 
 $ C3(a42_a64) \land $ \\ 
 $ C3(a85) \land $ \\ 
 $ C3(a12_a58) \land $ \\ 
 $ C3(a72) \land $ \\ 
 $ C3(a97_a63) \land $ \\ 
 $ C3(a65) \land $ \\ 
 $ C3(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $ C3(a24) \land $ \\ 
 $ C3(a88_a49) \land $ \\ 
 $ C3(a93) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a72) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a12_a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L3(a24) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a24) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a24) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L3Inv(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a30) \land $ \\ 
 $  \Rnext C0(a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a93) \land $ \\ 
 $  \Rnext C1(a42_a64) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a24) \land $ \\ 
 $  \Rnext  \Rnext C3(a24) \land $ \\ 
 $  \Rnext E2L2Inv(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a71) \land $ \\ 
 $  \Rnext E3L3(a65) \land $ \\ 
 $  \Rnext C3(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a12_a58) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a65) \land $ \\ 
 $  \Rnext E3L0Inv(a42_a64) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a30) \land $ \\ 
 $  \Rnext  \Rnext C3(a99) \land $ \\ 
 $  \Rnext E3L3(a85) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a42_a64) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a30) \land $ \\ 
 $  \Rnext E3L3(a50) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L3Inv(a97_a63) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a24) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L3(a30) \land $ \\ 
 $  \Rnext  \Rnext C1(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a24) \land $ \\ 
 $  \Rnext  \Rnext E3L3Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L3(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a65) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L3Inv(a88_a49) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a50) \land $ \\ 
 $  \Rnext E2L2(a12_a58) \land $ \\ 
 $ E3L1Inv(a11) \land $ \\ 
 $ E3L1Inv(a30) \land $ \\ 
 $ E3L1Inv(a89) \land $ \\ 
 $ E3L1Inv(a85) \land $ \\ 
 $ E3L1Inv(a24) \land $ \\ 
 $ E3L1Inv(a26_a84) \land $ \\ 
 $ E3L1Inv(a97_a63) \land $ \\ 
 $ E3L1Inv(a93) \land $ \\ 
 $ E3L1Inv(a36) \land $ \\ 
 $ E3L1Inv(a72) \land $ \\ 
 $ E3L1Inv(a12_a58) \land $ \\ 
 $ E3L1Inv(a42_a64) \land $ \\ 
 $ E3L1Inv(a88_a49) \land $ \\ 
 $ E3L1Inv(a99) \land $ \\ 
 $ E3L1Inv(a71) \land $ \\ 
 $ E3L1Inv(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $ E3L1Inv(a38) \land $ \\ 
 $ E3L1Inv(a65) \land $ \\ 
 $ E3L1Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a97_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a99) \land $ \\ 
 $  \Rnext E2L2Inv(a24) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L3(a12_a58) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a38) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a50) \land $ \\ 
 $  \Rnext  \Rnext C2(a88_a49) \land $ \\ 
 $ C1(a30) \land $ \\ 
 $ C1(a50) \land $ \\ 
 $ C1(a36) \land $ \\ 
 $ C1(a12_a58) \land $ \\ 
 $ C1(a65) \land $ \\ 
 $ C1(a11) \land $ \\ 
 $ C1(a93) \land $ \\ 
 $ C1(a38) \land $ \\ 
 $ C1(a89) \land $ \\ 
 $ C1(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $ C1(a99) \land $ \\ 
 $ C1(a72) \land $ \\ 
 $ C1(a71) \land $ \\ 
 $ C1(a24) \land $ \\ 
 $ C1(a88_a49) \land $ \\ 
 $ C1(a42_a64) \land $ \\ 
 $ C1(a97_a63) \land $ \\ 
 $ C1(a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a36) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a97_a63) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a42_a64) \land $ \\ 
 $  \Rnext  \Rnext C0(a24) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a12_a58) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext E3L1Inv(a88_a49) \land $ \\ 
 $  \Rnext E3L3(a72) \land $ \\ 
 $  \Rnext E2L2Inv(a85) \land $ \\ 
 $  \Rnext C1(a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a36) \land $ \\ 
 $  \Rnext  \Rnext E3L3(a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a89) \land $ \\ 
 $  \Rnext E3L1Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L3(a38) \land $ \\ 
 $ E2G0(a26_a84) \land $ \\ 
 $ E2G0(a30) \land $ \\ 
 $ E2G0(a65) \land $ \\ 
 $ E2G0(a99) \land $ \\ 
 $ E2G0(a11) \land $ \\ 
 $ E2G0(a93) \land $ \\ 
 $ E2G0(a50) \land $ \\ 
 $ E2G0(a36) \land $ \\ 
 $ E2G0(a71) \land $ \\ 
 $ E2G0(a97_a63) \land $ \\ 
 $ E2G0(a88_a49) \land $ \\ 
 $ E2G0(a12_a58) \land $ \\ 
 $ E2G0(a72) \land $ \\ 
 $ E2G0(a85) \land $ \\ 
 $ E2G0(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $ E2G0(a89) \land $ \\ 
 $ E2G0(a38) \land $ \\ 
 $ E2G0(a42_a64) \land $ \\ 
 $ E2G0(a24) \land $ \\ 
 $ E1G2(a26_a84) \land $ \\ 
 $ E1G2(a11) \land $ \\ 
 $ E1G2(a38) \land $ \\ 
 $ E1G2(a89) \land $ \\ 
 $ E1G2(a50) \land $ \\ 
 $ E1G2(a36) \land $ \\ 
 $ E1G2(a97_a63) \land $ \\ 
 $ E1G2(a12_a58) \land $ \\ 
 $ E1G2(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $ E1G2(a99) \land $ \\ 
 $ E1G2(a85) \land $ \\ 
 $ E1G2(a65) \land $ \\ 
 $ E1G2(a88_a49) \land $ \\ 
 $ E1G2(a71) \land $ \\ 
 $ E1G2(a72) \land $ \\ 
 $ E1G2(a30) \land $ \\ 
 $ E1G2(a93) \land $ \\ 
 $ E1G2(a42_a64) \land $ \\ 
 $ E1G2(a24) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L3(a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a93) \land $ \\ 
 $  \Rnext  \Rnext C3(a12_a58) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a36) \land $ \\ 
 $  \Rnext E3L3Inv(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a85) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a65) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a88_a49) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a24) \land $ \\ 
 $  \Rnext  \Rnext C3(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a24) \land $ \\ 
 $  \Rnext  \Rnext C3(a36) \land $ \\ 
 $  \Rnext E2L2Inv(a12_a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a88_a49) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a97_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a12_a58) \land $ \\ 
 $  \Rnext E3L1(a50) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a97_a63) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a93) \land $ \\ 
 $ E3L1(a26_a84) \land $ \\ 
 $  \Rnext  \Rnext E3L3(a65) \land $ \\ 
 $ E3L1(a85) \land $ \\ 
 $ E3L1(a11) \land $ \\ 
 $ E3L1(a65) \land $ \\ 
 $ E3L1(a88_a49) \land $ \\ 
 $ E3L1(a42_a64) \land $ \\ 
 $ E3L1(a97_a63) \land $ \\ 
 $ E3L1(a50) \land $ \\ 
 $ E3L1(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $ E3L1(a99) \land $ \\ 
 $ E3L1(a36) \land $ \\ 
 $ E3L1(a71) \land $ \\ 
 $ E3L1(a72) \land $ \\ 
 $ E3L1(a38) \land $ \\ 
 $ E3L1(a12_a58) \land $ \\ 
 $ E3L1(a89) \land $ \\ 
 $ E3L1(a93) \land $ \\ 
 $ E3L1(a30) \land $ \\ 
 $ E3L1(a24) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a88_a49) \land $ \\ 
 $  \Rnext E3L0Inv(a30) \land $ \\ 
 $  \Rnext  \Rnext C0(a85) \land $ \\ 
 $  \Rnext E3L0(a50) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a71) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a97_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L3(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a71) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a88_a49) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a88_a49) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a97_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a11) \land $ \\ 
 $  \Rnext C3(a85) \land $ \\ 
 $  \Rnext E3L3Inv(a88_a49) \land $ \\ 
 $  \Rnext  \Rnext E3L3(a71) \land $ \\ 
 $  \Rnext  \Rnext C1(a97_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a38) \land $ \\ 
 $  \Rnext E3L1(a99) \land $ \\ 
 $  \Rnext  \Rnext C0(a72) \land $ \\ 
 $  \Rnext E3L0(a71) \land $ \\ 
 $  \Rnext E2L2(a24) \land $ \\ 
 $  \Rnext C1(a88_a49) \land $ \\ 
 $  \Rnext E3L0(a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a26_a84) \land $ \\ 
 $  \Rnext C2(a50) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext E3L3Inv(a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a72) \land $ \\ 
 $  \Rnext E2L2(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a36) \land $ \\ 
 $  \Rnext E3L3(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext E2L2(a42_a64) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a99) \land $ \\ 
 $  \Rnext C0(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a50) \land $ \\ 
 $  \Rnext C2(a12_a58) \land $ \\ 
 $  \Rnext E3L0Inv(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a93) \land $ \\ 
 $  \Rnext C2(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L3Inv(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a71) \land $ \\ 
 $  \Rnext E3L1(a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a24) \land $ \\ 
 $  \Rnext  \Rnext C1(a24) \land $ \\ 
 $  \Rnext E2L2Inv(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a85) \land $ \\ 
 $  \Rnext E3L1Inv(a12_a58) \land $ \\ 
 $ E3L3(a85) \land $ \\ 
 $ E3L3(a26_a84) \land $ \\ 
 $ E3L3(a11) \land $ \\ 
 $ E3L3(a24) \land $ \\ 
 $ E3L3(a97_a63) \land $ \\ 
 $ E3L3(a71) \land $ \\ 
 $ E3L3(a42_a64) \land $ \\ 
 $ E3L3(a50) \land $ \\ 
 $ E3L3(a93) \land $ \\ 
 $ E3L3(a88_a49) \land $ \\ 
 $ E3L3(a89) \land $ \\ 
 $ E3L3(a36) \land $ \\ 
 $ E3L3(a65) \land $ \\ 
 $ E3L3(a30) \land $ \\ 
 $ E3L3(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $ E3L3(a99) \land $ \\ 
 $ E3L3(a12_a58) \land $ \\ 
 $ E3L3(a72) \land $ \\ 
 $ E3L3(a38) \land $ \\ 
 $  \Rnext C2(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a97_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a38) \land $ \\ 
 $  \Rnext E3L1Inv(a24) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a42_a64) \land $ \\ 
 $  \Rnext E2L2(a89) \land $ \\ 
 $  \Rnext E3L0(a93) \land $ \\ 
 $  \Rnext  \Rnext C3(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a12_a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a85) \land $ \\ 
 $  \Rnext E3L0(a11) \land $ \\ 
 $  \Rnext E3L0Inv(a50) \land $ \\ 
 $  \Rnext E3L1Inv(a72) \land $ \\ 
 $  \Rnext E2L2Inv(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a97_a63) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L3Inv(a36) \land $ \\ 
 $  \Rnext C2(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a85) \land $ \\ 
 $  \Rnext E3L3(a38) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a24) \land $ \\ 
 $  \Rnext C3(a12_a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a89) \land $ \\ 
 $  \Rnext E2L2(a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a93) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L3(a97_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a26_a84) \land $ \\ 
 $  \Rnext E3L3(a26_a84) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L3Inv(a26_a84) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a97_a63) \land $ \\ 
 $  \Rnext E3L3(a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a89) \land $ \\ 
 $  \Rnext E3L1Inv(a42_a64) \land $ \\ 
 $  \Rnext  \Rnext E3L3Inv(a99) \land $ \\ 
 $  \Rnext C0(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a89) \land $ \\ 
 $  \Rnext E3L3(a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a26_a84) \land $ \\ 
 $  \Rnext C2(a88_a49) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a42_a64) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a97_a63) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a42_a64) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a65) \land $ \\ 
 $  \Rnext  \Rnext E3L3Inv(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a12_a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a93) \land $ \\ 
 $  \Rnext E3L3(a88_a49) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a24) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a72) \land $ \\ 
 $  \Rnext E3L1Inv(a30) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a88_a49) \land $ \\ 
 $  \Rnext E3L0(a88_a49) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a42_a64) \land $ \\ 
 $  \Rnext E3L0(a42_a64) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L3(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a65) \land $ \\ 
 $  \Rnext E3L3Inv(a12_a58) \land $ \\ 
 $  \Rnext E3L0(a65) \land $ \\ 
 $  \Rnext  \Rnext E3L3(a50) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a24) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L3Inv(a42_a64) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a93) \land $ \\ 
 $  \Rnext E3L3Inv(a93) \land $ \\ 
 $  \Rnext E3L1Inv(a36) \land $ \\ 
 $  \Rnext C1(a36) \land $ \\ 
 $  \Rnext C2(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a42_a64) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a11) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a97_a63) \land $ \\ 
 $  \Rnext  \Rnext C2(a99) \land $ \\ 
 $  \Rnext E3L3Inv(a42_a64) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a99) \land $ \\ 
 $  \Rnext C3(a50) \land $ \\ 
 $  \Rnext E3L1Inv(a99) \land $ \\ 
 $ E3L0Inv(a42_a64) \land $ \\ 
 $ E3L0Inv(a11) \land $ \\ 
 $ E3L0Inv(a12_a58) \land $ \\ 
 $ E3L0Inv(a85) \land $ \\ 
 $ E3L0Inv(a24) \land $ \\ 
 $ E3L0Inv(a71) \land $ \\ 
 $ E3L0Inv(a97_a63) \land $ \\ 
 $ E3L0Inv(a30) \land $ \\ 
 $ E3L0Inv(a26_a84) \land $ \\ 
 $ E3L0Inv(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $ E3L0Inv(a99) \land $ \\ 
 $ E3L0Inv(a50) \land $ \\ 
 $ E3L0Inv(a36) \land $ \\ 
 $ E3L0Inv(a93) \land $ \\ 
 $ E3L0Inv(a88_a49) \land $ \\ 
 $ E3L0Inv(a38) \land $ \\ 
 $ E3L0Inv(a65) \land $ \\ 
 $ E3L0Inv(a72) \land $ \\ 
 $ E3L0Inv(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a88_a49) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L3Inv(a65) \land $ \\ 
 $  \Rnext  \Rnext E3L3Inv(a89) \land $ \\ 
 $  \Rnext C0(a72) \land $ \\ 
 $  \Rnext  \Rnext C3(a42_a64) \land $ \\ 
 $  \Rnext  \Rnext C1(a26_a84) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a65) \land $ \\ 
 $  \Rnext  \Rnext C0(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L3Inv(a99) \land $ \\ 
 $  \Rnext E2L2Inv(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext E3L1(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L3(a26_a84) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a71) \land $ \\ 
 $  \Rnext  \Rnext C0(a30) \land $ \\ 
 $  \Rnext C3(a42_a64) \land $ \\ 
 $  \Rnext C3(a99) \land $ \\ 
 $  \Rnext E3L0(a12_a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L3Inv(a97_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext E3L3(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a97_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a72) \land $ \\ 
 $  \Rnext E2L2Inv(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a72) \land $ \\ 
 $  \Rnext E2L2Inv(a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a24) \land $ \\ 
 $  \Rnext E3L0(a99) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a26_a84) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a97_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a99) \land $ \\ 
 $  \Rnext C0(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a97_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a97_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a72) \land $ \\ 
 $ E2L2Inv(a36) \land $ \\ 
 $ E2L2Inv(a11) \land $ \\ 
 $ E2L2Inv(a89) \land $ \\ 
 $ E2L2Inv(a50) \land $ \\ 
 $ E2L2Inv(a30) \land $ \\ 
 $ E2L2Inv(a93) \land $ \\ 
 $ E2L2Inv(a97_a63) \land $ \\ 
 $ E2L2Inv(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $ E2L2Inv(a85) \land $ \\ 
 $ E2L2Inv(a26_a84) \land $ \\ 
 $ E2L2Inv(a42_a64) \land $ \\ 
 $ E2L2Inv(a24) \land $ \\ 
 $ E2L2Inv(a71) \land $ \\ 
 $ E2L2Inv(a12_a58) \land $ \\ 
 $ E2L2Inv(a88_a49) \land $ \\ 
 $ E2L2Inv(a99) \land $ \\ 
 $ E2L2Inv(a65) \land $ \\ 
 $ E2L2Inv(a38) \land $ \\ 
 $ E2L2Inv(a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L3Inv(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a26_a84) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a88_a49) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a12_a58) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a93) \land $ \\ 
 $  \Rnext E3L0(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L3Inv(a71) \land $ \\ 
 $  \Rnext  \Rnext C1(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a71) \land $ \\ 
 $  \Rnext E2L2Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a97_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a89) \land $ \\ 
 $  \Rnext C0(a88_a49) \land $ \\ 
 $  \Rnext E3L0(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a71) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a30) \land $ \\ 
 $  \Rnext E3L3Inv(a24) \land $ \\ 
 $  \Rnext E3L3(a12_a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L3(a26_a84) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a24) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L3(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a50) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a89) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a26_a84) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a11) \land $ \\ 
 $  \Rnext E3L1(a71) \land $ \\ 
 $  \Rnext E3L0Inv(a26_a84) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a71) \land $ \\ 
 $  \Rnext  \Rnext E3L3(a38) \land $ \\ 
 $  \Rnext C0(a26_a84) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a26_a84) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a99) \land $ \\ 
 $  \Rnext E2L2(a36) \land $ \\ 
 $  \Rnext  \Rnext C0(a97_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L3(a85) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a65) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a12_a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a36) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a97_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L3(a93) \land $ \\ 
 $  \Rnext E2L2(a88_a49) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a50) \land $ \\ 
 $  \Rnext  \Rnext E3L3Inv(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L3Inv(a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L3(a24) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L3Inv(a12_a58) \land $ \\ 
 $  \Rnext  \Rnext E3L3Inv(a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a93) \land $ \\ 
 $  \Rnext  \Rnext C2(a71) \land $ \\ 
 $  \Rnext E3L3(a97_a63) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a93) \land $ \\ 
 $  \Rnext E3L3Inv(a72) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a12_a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a30) \land $ \\ 
 $  \Rnext  \Rnext C2(a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a88_a49) \land $ \\ 
 $  \Rnext  \Rnext C2(a12_a58) \land $ \\ 
 $  \Rnext C0(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a38) \land $ \\ 
 $ E3G3(a50) \land $ \\ 
 $ E3G3(a11) \land $ \\ 
 $ E3G3(a93) \land $ \\ 
 $ E3G3(a26_a84) \land $ \\ 
 $ E3G3(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $ E3G3(a38) \land $ \\ 
 $ E3G3(a65) \land $ \\ 
 $ E3G3(a97_a63) \land $ \\ 
 $ E3G3(a71) \land $ \\ 
 $ E3G3(a36) \land $ \\ 
 $ E3G3(a42_a64) \land $ \\ 
 $ E3G3(a99) \land $ \\ 
 $ E3G3(a12_a58) \land $ \\ 
 $ E3G3(a88_a49) \land $ \\ 
 $ E3G3(a72) \land $ \\ 
 $ E3G3(a89) \land $ \\ 
 $ E3G3(a30) \land $ \\ 
 $ E3G3(a24) \land $ \\ 
 $ E3G3(a85) \land $ \\ 
 $  \Rnext E3L1Inv(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L3Inv(a65) \land $ \\ 
 $  \Rnext E3L1Inv(a97_a63) \land $ \\ 
 $  \Rnext  \Rnext E3L3Inv(a42_a64) \land $ \\ 
 $  \Rnext E3L0Inv(a88_a49) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a65) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a24) \land $ \\ 
 $  \Rnext E3L1Inv(a11) \land $ \\ 
 $  \Rnext C1(a71) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a12_a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext C0(a99) \land $ \\ 
 $  \Rnext C2(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L3Inv(a88_a49) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a88_a49) \land $ \\ 
 $  \Rnext E2L2(a26_a84) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a97_a63) \land $ \\ 
 $  \Rnext E3L3Inv(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a42_a64) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a12_a58) \land $ \\ 
 $  \Rnext E2L2(a50) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a36) \land $ \\ 
 $  \Rnext E3L0Inv(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L3Inv(a12_a58) \land $ \\ 
 $  \Rnext C0(a65) \land $ \\ 
 $  \Rnext  \Rnext E3L3Inv(a36) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L3Inv(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext E3L3Inv(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a71) \land $ \\ 
 $  \Rnext E3L0Inv(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a12_a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a24) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L3Inv(a72) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a88_a49) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a99) \land $ \\ 
 $  \Rnext E3L0Inv(a65) \land $ \\ 
 $  \Rnext  \Rnext E3L3Inv(a24) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a26_a84) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a97_a63) \land $ \\ 
 $  \Rnext  \Rnext E3L3(a89) \land $ \\ 
 $  \Rnext C2(a26_a84) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a88_a49) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L3Inv(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L3Inv(a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L3(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a26_a84) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a24) \land $ \\ 
 $  \Rnext C0(a89) \land $ \\ 
 $  \Rnext E3L1Inv(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a72) \land $ \\ 
 $  \Rnext C0(a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a12_a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a11) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a38) \land $ \\ 
 $  \Rnext  \Rnext C2(a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L3(a42_a64) \land $ \\ 
 $ E1G1(a26_a84) \land $ \\ 
 $ E1G1(a85) \land $ \\ 
 $ E1G1(a11) \land $ \\ 
 $ E1G1(a72) \land $ \\ 
 $ E1G1(a12_a58) \land $ \\ 
 $ E1G1(a89) \land $ \\ 
 $ E1G1(a99) \land $ \\ 
 $ E1G1(a24) \land $ \\ 
 $ E1G1(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $ E1G1(a42_a64) \land $ \\ 
 $ E1G1(a50) \land $ \\ 
 $ E1G1(a38) \land $ \\ 
 $ E1G1(a65) \land $ \\ 
 $ E1G1(a97_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L3Inv(a85) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a99) \land $ \\ 
 $ E1G1(a30) \land $ \\ 
 $ E1G1(a71) \land $ \\ 
 $ E1G1(a36) \land $ \\ 
 $ E1G1(a93) \land $ \\ 
 $ E1G1(a88_a49) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L3Inv(a42_a64) \land $ \\ 
 $  \Rnext  \Rnext E3L3(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a85) \land $ \\ 
 $  \Rnext E3L0(a26_a84) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a42_a64) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a26_a84) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a24) \land $ \\ 
 $  \Rnext  \Rnext E3L3Inv(a88_a49) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a65) \land $ \\ 
 $  \Rnext E3L0(a36) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a97_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a99) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a26_a84) \land $ \\ 
 $  \Rnext  \Rnext C3(a97_a63) \land $ \\ 
 $  \Rnext E3L0(a85) \land $ \\ 
 $  \Rnext E3L3(a11) \land $ \\ 
 $  \Rnext E3L1(a97_a63) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a12_a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a88_a49) \land $ \\ 
 $  \Rnext E3L1(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext C2(a42_a64) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a97_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a26_a84) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a65) \land $ \\ 
 $  \Rnext  \Rnext E3L3(a12_a58) \land $ \\ 
 $  \Rnext  \Rnext C3(a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a11) \land $ \\ 
 $ C2(a88_a49) \land $ \\ 
 $ C2(a26_a84) \land $ \\ 
 $ C2(a11) \land $ \\ 
 $ C2(a42_a64) \land $ \\ 
 $ C2(a72) \land $ \\ 
 $ C2(a24) \land $ \\ 
 $ C2(a97_a63) \land $ \\ 
 $ C2(a50) \land $ \\ 
 $ C2(a85) \land $ \\ 
 $ C2(a93) \land $ \\ 
 $ C2(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $ C2(a12_a58) \land $ \\ 
 $ C2(a99) \land $ \\ 
 $ C2(a71) \land $ \\ 
 $ C2(a38) \land $ \\ 
 $ C2(a65) \land $ \\ 
 $ C2(a30) \land $ \\ 
 $ C2(a89) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a12_a58) \land $ \\ 
 $  \Rnext  \Rnext C3(a26_a84) \land $ \\ 
 $  \Rnext E3L1Inv(a89) \land $ \\ 
 $  \Rnext C1(a65) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a26_a84) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a12_a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L3(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a11) \land $ \\ 
 $  \Rnext  \Rnext C1(a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a50) \land $ \\ 
 $  \Rnext C3(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a72) \land $ \\ 
 $  \Rnext E3L1(a88_a49) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a93) \land $ \\ 
 $  \Rnext C1(a85) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a30) \land $ \\ 
 $  \Rnext  \Rnext C2(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a36) \land $ \\ 
 $  \Rnext  \Rnext C0(a26_a84) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a11) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L3(a97_a63) \land $ \\ 
 $  \Rnext E2L2Inv(a97_a63) \land $ \\ 
 $ E1G0Inv(a93) \land $ \\ 
 $ E1G0Inv(a26_a84) \land $ \\ 
 $ E1G0Inv(a11) \land $ \\ 
 $ E1G0Inv(a89) \land $ \\ 
 $ E1G0Inv(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $ E1G0Inv(a71) \land $ \\ 
 $ E1G0Inv(a97_a63) \land $ \\ 
 $ E1G0Inv(a99) \land $ \\ 
 $ E1G0Inv(a65) \land $ \\ 
 $ E1G0Inv(a38) \land $ \\ 
 $ E1G0Inv(a50) \land $ \\ 
 $ E1G0Inv(a36) \land $ \\ 
 $ E1G0Inv(a88_a49) \land $ \\ 
 $ E1G0Inv(a72) \land $ \\ 
 $ E1G0Inv(a85) \land $ \\ 
 $ E1G0Inv(a12_a58) \land $ \\ 
 $ E1G0Inv(a30) \land $ \\ 
 $ E1G0Inv(a24) \land $ \\ 
 $ E1G0Inv(a42_a64) \land $ \\ 
 $  \Rnext C2(a30) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a38) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a26_a84) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a93) \land $ \\ 
 $  \Rnext  \Rnext C3(a30) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a71) \land $ \\ 
 $  \Rnext C3(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a12_a58) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L3(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a99) \land $ \\ 
 $  \Rnext  \Rnext C3(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L3Inv(a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a50) \land $ \\ 
 $  \Rnext E3L3Inv(a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a88_a49) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a71) \land $ \\ 
 $ C0(a11) \land $ \\ 
 $ C0(a50) \land $ \\ 
 $ C0(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $ C0(a85) \land $ \\ 
 $ C0(a26_a84) \land $ \\ 
 $ C0(a24) \land $ \\ 
 $ C0(a89) \land $ \\ 
 $ C0(a99) \land $ \\ 
 $ C0(a65) \land $ \\ 
 $ C0(a36) \land $ \\ 
 $ C0(a12_a58) \land $ \\ 
 $ C0(a72) \land $ \\ 
 $ C0(a88_a49) \land $ \\ 
 $ C0(a93) \land $ \\ 
 $ C0(a42_a64) \land $ \\ 
 $ C0(a71) \land $ \\ 
 $ C0(a97_a63) \land $ \\ 
 $ C0(a38) \land $ \\ 
 $  \Rnext C2(a42_a64) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a89) \land $ \\ 
 $  \Rnext  \Rnext C0(a42_a64) \land $ \\ 
 $  \Rnext C1(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L3Inv(a50) \land $ \\ 
 $  \Rnext C1(a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a26_a84) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a12_a58) \land $ \\ 
 $  \Rnext E3L1(a24) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a30) \land $ \\ 
 $  \Rnext E3L1(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a88_a49) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a12_a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L3(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a88_a49) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L3(a36) \land $ \\ 
 $  \Rnext C3(a24) \land $ \\ 
 $  \Rnext E3L0Inv(a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a89) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a72) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a42_a64) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a97_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a65) \land $ \\ 
 $  \Rnext C0(a12_a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a42_a64) \land $ \\ 
 $  \Rnext E3L1Inv(a26_a84) \land $ \\ 
 $  \Rnext C3(a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a99) \land $ \\ 
 $  \Rnext E2L2(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a85) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a65) \land $ \\ 
 $  \Rnext  \Rnext C3(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext C0(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a30) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a88_a49) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L3(a89) \land $ \\ 
 $  \Rnext  \Rnext E3L3Inv(a11) \land $ \\ 
 $ E3L0(a11) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a30) \land $ \\ 
 $ E3L0(a89) \land $ \\ 
 $ E3L0(a42_a64) \land $ \\ 
 $ E3L0(a12_a58) \land $ \\ 
 $ E3L0(a85) \land $ \\ 
 $ E3L0(a26_a84) \land $ \\ 
 $ E3L0(a24) \land $ \\ 
 $ E3L0(a30) \land $ \\ 
 $ E3L0(a99) \land $ \\ 
 $ E3L0(a38) \land $ \\ 
 $ E3L0(a71) \land $ \\ 
 $ E3L0(a50) \land $ \\ 
 $ E3L0(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $ E3L0(a36) \land $ \\ 
 $ E3L0(a88_a49) \land $ \\ 
 $ E3L0(a97_a63) \land $ \\ 
 $ E3L0(a72) \land $ \\ 
 $ E3L0(a65) \land $ \\ 
 $ E3L0(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L3(a38) \land $ \\ 
 $  \Rnext E2L2(a11) \land $ \\ 
 $  \Rnext  \Rnext E3L3(a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L3(a30) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a50) \land $ \\ 
 $ E2L2(a88_a49) \land $ \\ 
 $ E2L2(a11) \land $ \\ 
 $ E2L2(a26_a84) \land $ \\ 
 $ E2L2(a71) \land $ \\ 
 $ E2L2(a12_a58) \land $ \\ 
 $ E2L2(a38) \land $ \\ 
 $ E2L2(a97_a63) \land $ \\ 
 $ E2L2(a50) \land $ \\ 
 $ E2L2(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $ E2L2(a89) \land $ \\ 
 $ E2L2(a24) \land $ \\ 
 $ E2L2(a36) \land $ \\ 
 $ E2L2(a85) \land $ \\ 
 $ E2L2(a99) \land $ \\ 
 $ E2L2(a65) \land $ \\ 
 $ E2L2(a30) \land $ \\ 
 $ E2L2(a42_a64) \land $ \\ 
 $ E2L2(a72) \land $ \\ 
 $ E2L2(a93) \land $ \\ 
 $  \Rnext  \Rnext C3(a88_a49) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a26_a84) \land $ \\ 
 $  \Rnext  \Rnext C1(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a12_a58) \land $ \\ 
 $  \Rnext C3(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L3Inv(a24) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a26_a84) \land $ \\ 
 $  \Rnext  \Rnext C2(a89) \land $ \\ 
 $  \Rnext E3L0Inv(a12_a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a36) \land $ \\ 
 $  \Rnext E2L2(a97_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a26_a84) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a12_a58) \land $ \\ 
 $  \Rnext C1(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a65) \land $ \\ 
 $  \Rnext E3L3Inv(a26_a84) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a50) \land $ \\ 
 $  \Rnext  \Rnext C1(a72) \land $ \\ 
 $  \Rnext  \Rnext C0(a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L3Inv(a89) \land $ \\ 
 $  \Rnext  \Rnext C0(a88_a49) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a42_a64) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a65) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a65) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a50) \land $ \\ 
 $  \Rnext E3L1Inv(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L3(a88_a49) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a24) \land $ \\ 
 $  \Rnext E3L0(a24) \land $ \\ 
 $  \Rnext E3L1(a26_a84) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L3Inv(a24) \land $ \\ 
 $  \Rnext  \Rnext C1(a30) \land $ \\ 
 $  \Rnext  \Rnext E3L3(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a88_a49) \land $ \\ 
 $  \Rnext C3(a97_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a30) \land $ \\ 
 $  \Rnext  \Rnext C1(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a42_a64) \land $ \\ 
 $  \Rnext C3(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L3(a11) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a26_a84) \land $ \\ 
 $  \Rnext E3L3(a24) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a38) \land $ \\ 
 $  \Rnext C1(a24) \land $ \\ 
 $  \Rnext  \Rnext E3L3(a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a26_a84) \land $ \\ 
 $  \Rnext  \Rnext C0(a50) \land $ \\ 
 $  \Rnext C1(a97_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a97_a63) \land $ \\ 
 $  \Rnext C2(a97_a63) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a89) \land $ \\ 
 $  \Rnext  \Rnext E3L3(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $ E3L3Inv(a11) \land $ \\ 
 $  \Rnext E3L3Inv(a36) \land $ \\ 
 $ E3L3Inv(a30) \land $ \\ 
 $ E3L3Inv(a93) \land $ \\ 
 $ E3L3Inv(a99) \land $ \\ 
 $ E3L3Inv(a26_a84) \land $ \\ 
 $ E3L3Inv(a42_a64) \land $ \\ 
 $ E3L3Inv(a72) \land $ \\ 
 $ E3L3Inv(a65) \land $ \\ 
 $ E3L3Inv(a38) \land $ \\ 
 $ E3L3Inv(a12_a58) \land $ \\ 
 $ E3L3Inv(a24) \land $ \\ 
 $ E3L3Inv(a71) \land $ \\ 
 $ E3L3Inv(a77_a33_a76_a32_a79_a35_a78_a34_a37_a39_a80_a82_a81_a40_a83_a86_a41_a44_a87_a43_a46_a45_a48_a47_a91_a90_a92_a95_a51_a94_a53_a96_a52_a55_a98_a10_a54_a13_a57_a56_a15_a59_a14_a17_a16_a19_a18_a60_a100_a62_a61_a20_a22_a66_a21_a68_a23_a67_a25_a69_a28_a27_a29_a1_a2_a3_a4_a5_a6_a7_a8_a9_a70_a73_a31_a75_a74) \land $ \\ 
 $ E3L3Inv(a88_a49) \land $ \\ 
 $ E3L3Inv(a50) \land $ \\ 
 $ E3L3Inv(a85) \land $ \\ 
 $ E3L3Inv(a36) \land $ \\ 
 $ E3L3Inv(a97_a63) \land $ \\ 
 $ E3L3Inv(a89) \land $ \\ 
 $  \Rnext C0(a38))$ 
\end{document}