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


$((PL1 \rightarrow E1L1Inv(dL1Inv)) \land $ \\ 
 $ (PinvG0 \rightarrow E1G0(dG0)) \land $ \\ 
 $ (PinvL0 \rightarrow E1L0(dL0)) \land $ \\ 
 $ (PinvL2 \rightarrow E1L2(dL2)) \land $ \\ 
 $ (PL2 \rightarrow E1L2Inv(dL2Inv)) \land $ \\ 
 $ (PinvG2 \rightarrow E1G2(dG2)) \land $ \\ 
 $ (PG2 \rightarrow E1G2Inv(dG2Inv)) \land $ \\ 
 $ (PG0 \rightarrow E1G0Inv(dG0Inv)) \land $ \\ 
 $ (PinvG3 \rightarrow E1G3(dG3)) \land $ \\ 
 $ (PG3 \rightarrow E1G3Inv(dG3Inv)) \land $ \\ 
 $ (PinvL1 \rightarrow E1L1(dL1)) \land $ \\ 
 $  \forall X. ( \Rbox (((C0(X) \land $ \\ 
 $ E1L2(X) \land $ \\ 
 $ E1L1(X)) \rightarrow ( \Rnext C1(X) \land $ \\ 
 $  \Rnext E1G0(X))) \land $ \\ 
 $ ( \Rbox  \Rbox C1(X) \rightarrow  \Rbox  \Rdiamond (E1L2(X) \land $ \\ 
 $ C2(X))) \land $ \\ 
 $ ( \Rdiamond (E2L2(X) \land $ \\ 
 $  \Rdiamond C0(X)) \rightarrow  \Rbox  \Rdiamond (C3(X) \land $ \\ 
 $ E1G2(X))) \land $ \\ 
 $ ( \Rbox  \Rdiamond  \Rbox  \Rnext C2(X) \rightarrow (C1(X) \land $ \\ 
 $ E2L0(X) \land $ \\ 
 $ E2G2(X))) \land $ \\ 
 $ ( \Rbox  \Rdiamond  \Rdiamond  \Rnext E2L0(X) \rightarrow ( \Rnext E3L0(X) \land $ \\ 
 $  \Rbox E2G3(X))) \land $ \\ 
 $ ( \Rbox (C2(X) \land $ \\ 
 $  \Rnext E3L1(X)) \rightarrow ( \Rnext C3(X) \land $ \\ 
 $  \Rdiamond C1(X))) \land $ \\ 
 $ ( \Rbox (C1(X) \land $ \\ 
 $  \Rnext C3(X)) \rightarrow ( \Rdiamond C1(X) \land $ \\ 
 $  \Rbox C2(X))) \land $ \\ 
 $ (( \Rnext C0(X) \land $ \\ 
 $  \Rnext C1(X)) \rightarrow ( \Rnext E1L2(X) \land $ \\ 
 $  \Rnext E2G3(X))) \land $ \\ 
 $ (( \Rbox C1(X) \land $ \\ 
 $  \Rdiamond C1(X)) \rightarrow  \Rdiamond  \Rbox  \Rdiamond  \Rnext E2L0(X)) \land $ \\ 
 $ ((C1(X) \land $ \\ 
 $  \Rdiamond  \Rnext E3L0(X)) \rightarrow (C0(X) \land $ \\ 
 $  \Rdiamond  \Rbox C1(X))) \land $ \\ 
 $ ( \Rbox  \Rdiamond  \Rbox  \Rnext E3G2(X) \rightarrow  \Rbox  \Rdiamond (C0(X) \land $ \\ 
 $ C2(X))) \land $ \\ 
 $ ((C0(X) \land $ \\ 
 $ E1L0(X) \land $ \\ 
 $ C3(X)) \rightarrow (C1(X) \land $ \\ 
 $  \Rdiamond  \Rnext C2(X))) \land $ \\ 
 $ ( \Rbox (C3(X) \land $ \\ 
 $  \Rnext C0(X)) \rightarrow  \Rdiamond (C3(X) \land $ \\ 
 $  \Rnext C0(X))) \land $ \\ 
 $ ((E2L0(X) \land $ \\ 
 $  \Rdiamond  \Rbox E1G2(X)) \rightarrow  \Rdiamond  \Rdiamond  \Rdiamond  \Rnext C2(X)) \land $ \\ 
 $ (( \Rnext C0(X) \land $ \\ 
 $  \Rnext C2(X)) \rightarrow  \Rdiamond (C3(X) \land $ \\ 
 $  \Rdiamond C1(X))) \land $ \\ 
 $ (E2L2(X) \rightarrow E1L2(X)) \land $ \\ 
 $ (E2G2(X) \rightarrow E1G2(X)) \land $ \\ 
 $ (E3L0(X) \rightarrow E2L0(X)) \land $ \\ 
 $ (E3G2(X) \rightarrow E2G2(X)) \land $ \\ 
 $ (E2G3(X) \rightarrow E1G3(X)) \land $ \\ 
 $ (E2L0(X) \rightarrow E1L0(X)) \land $ \\ 
 $ (E3L1(X) \rightarrow E1L1(X))) \land $ \\ 
 $ ( \Rdiamond E1G0Inv(X) \rightarrow  \Rbox PinvG0) \land $ \\ 
 $ ( \Rdiamond E1G0(X) \rightarrow  \Rbox PG0) \land $ \\ 
 $ ( \Rdiamond E1L0(X) \rightarrow  \Rbox PL0) \land $ \\ 
 $ ( \Rdiamond E1L2(X) \rightarrow  \Rbox PL2) \land $ \\ 
 $ ( \Rdiamond E1G2(X) \rightarrow  \Rbox PG2) \land $ \\ 
 $ ( \Rdiamond E1G2Inv(X) \rightarrow  \Rbox PinvG2) \land $ \\ 
 $ ( \Rdiamond E1G2Inv(X) \rightarrow  \Rbox E1G2Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1L0Inv(X) \rightarrow  \Rbox PinvL0) \land $ \\ 
 $ ( \Rdiamond E3G2(X) \rightarrow  \Rbox E3G2(X)) \land $ \\ 
 $ ( \Rdiamond E1G3(X) \rightarrow  \Rbox E1G3(X)) \land $ \\ 
 $ ( \Rdiamond E1G0Inv(X) \rightarrow  \Rbox E1G0Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1L1(X) \rightarrow  \Rbox PL1) \land $ \\ 
 $ ( \Rdiamond E1G3Inv(X) \rightarrow  \Rbox PinvG3) \land $ \\ 
 $ ( \Rdiamond E1G3(X) \rightarrow  \Rbox PG3) \land $ \\ 
 $ ( \Rdiamond E1L2Inv(X) \rightarrow  \Rbox PinvL2) \land $ \\ 
 $ ( \Rdiamond E1G2(X) \rightarrow  \Rbox E1G2(X)) \land $ \\ 
 $ ( \Rdiamond E1G0(X) \rightarrow  \Rbox E1G0(X)) \land $ \\ 
 $ ( \Rdiamond E1L1Inv(X) \rightarrow  \Rbox PinvL1) \land $ \\ 
 $ ( \Rdiamond E1G3Inv(X) \rightarrow  \Rbox E1G3Inv(X)) \land $ \\ 
 $ ( \Rdiamond E2G2(X) \rightarrow  \Rbox E2G2(X)) \land $ \\ 
 $ ( \Rdiamond E2G3(X) \rightarrow  \Rbox E2G3(X))) \land $ \\ 
 $ (PL0 \rightarrow E1L0Inv(dL0Inv)) \land $ \\ 
 $  \Rnext E2L2(a95) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a66_a7_a71) \land $ \\ 
 $  \Rnext  \Rnext C1(a5_a69) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a15) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a19) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a19) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a78) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a25_a9) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a19) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a99) \land $ \\ 
 $  \Rnext  \Rnext C3(a19) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $  \Rnext E2L2(a25_a9) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a54_a67_a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a100) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a25_a9) \land $ \\ 
 $  \Rnext  \Rnext C1(a76) \land $ \\ 
 $  \Rnext E2L2(a21) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a76) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a25_a9) \land $ \\ 
 $  \Rnext  \Rnext C3(a56_a31) \land $ \\ 
 $  \Rnext C2(a55) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a54_a67_a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a58) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a45) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a29) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a35_a49_a97) \land $ \\ 
 $  \Rnext E3L0Inv(a77) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a66_a7_a71) \land $ \\ 
 $  \Rnext E2L2(a79_a81) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a76) \land $ \\ 
 $  \Rnext E3L0Inv(a58) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a33_a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a89) \land $ \\ 
 $  \Rnext  \Rnext C3(a17) \land $ \\ 
 $  \Rnext E2L2(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a21) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a29) \land $ \\ 
 $  \Rnext  \Rnext C2(a17) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a66_a7_a71) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $  \Rnext E3L1(a12_a62) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a82) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a19) \land $ \\ 
 $  \Rnext C0(a51) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a87) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a95) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a87) \land $ \\ 
 $  \Rnext  \Rnext C3(a32_a80_a70_a94) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a78) \land $ \\ 
 $  \Rnext E2L2(a100) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a25_a9) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a2) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a12_a62) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a76) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a8_a86) \land $ \\ 
 $  \Rnext E3L0(a50) \land $ \\ 
 $  \Rnext E2L2(a37) \land $ \\ 
 $  \Rnext E2L2(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a65) \land $ \\ 
 $  \Rnext  \Rnext C3(a76) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a79_a81) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $  \Rnext E3L0(a23) \land $ \\ 
 $  \Rnext E3L1(a58) \land $ \\ 
 $  \Rnext C3(a12_a62) \land $ \\ 
 $  \Rnext  \Rnext C0(a99) \land $ \\ 
 $  \Rnext E3L0Inv(a25_a9) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a2) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a17) \land $ \\ 
 $  \Rnext  \Rnext C2(a14_a60_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a78) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a33_a36) \land $ \\ 
 $  \Rnext E2L2Inv(a32_a80_a70_a94) \land $ \\ 
 $  \Rnext  \Rnext C3(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $  \Rnext C3(a37) \land $ \\ 
 $  \Rnext  \Rnext C3(a58) \land $ \\ 
 $  \Rnext  \Rnext C0(a51) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a17) \land $ \\ 
 $  \Rnext C1(a61) \land $ \\ 
 $  \Rnext C1(a35_a49_a97) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a32_a80_a70_a94) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a14_a60_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a2) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a61) \land $ \\ 
 $  \Rnext C0(a37) \land $ \\ 
 $  \Rnext E2L2(a17) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a23) \land $ \\ 
 $  \Rnext E3L0(a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a2) \land $ \\ 
 $  \Rnext C3(a40) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a78) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a100) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a14_a60_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a45) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a99) \land $ \\ 
 $  \Rnext C3(a82) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a56_a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a66_a7_a71) \land $ \\ 
 $  \Rnext C1(a79_a81) \land $ \\ 
 $  \Rnext E2L2Inv(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a61) \land $ \\ 
 $  \Rnext E2L2Inv(a40) \land $ \\ 
 $  \Rnext E3L0(a76) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a51) \land $ \\ 
 $  \Rnext E3L0Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a51) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a55) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a51) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a45) \land $ \\ 
 $  \Rnext E3L1Inv(a89) \land $ \\ 
 $  \Rnext E2L2(a33_a36) \land $ \\ 
 $  \Rnext E3L1(a79_a81) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a45) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a19) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a95) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a37) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a35_a49_a97) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a65) \land $ \\ 
 $  \Rnext  \Rnext C1(a100) \land $ \\ 
 $  \Rnext E3L0Inv(a33_a36) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a23) \land $ \\ 
 $  \Rnext C0(a45) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a17) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a15) \land $ \\ 
 $  \Rnext  \Rnext C2(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a100) \land $ \\ 
 $  \Rnext  \Rnext C2(a78) \land $ \\ 
 $  \Rnext  \Rnext C2(a77) \land $ \\ 
 $  \Rnext E3L0(a65) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a54_a67_a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a14_a60_a63) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a35_a49_a97) \land $ \\ 
 $  \Rnext E3L0(a15) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a66_a7_a71) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a95) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a73) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a95) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a82) \land $ \\ 
 $  \Rnext E3L0Inv(a100) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a95) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a56_a31) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a57) \land $ \\ 
 $  \Rnext E2L2(a55) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a54_a67_a72) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a45) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a50) \land $ \\ 
 $  \Rnext E3L1Inv(a57) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a21) \land $ \\ 
 $ E1G3Inv(a78) \land $ \\ 
 $ E1G3Inv(a51) \land $ \\ 
 $ E1G3Inv(a17) \land $ \\ 
 $ E1G3Inv(a2) \land $ \\ 
 $ E1G3Inv(a61) \land $ \\ 
 $ E1G3Inv(a100) \land $ \\ 
 $ E1G3Inv(a58) \land $ \\ 
 $ E1G3Inv(a32_a80_a70_a94) \land $ \\ 
 $ E1G3Inv(a73) \land $ \\ 
 $ E1G3Inv(a55) \land $ \\ 
 $ E1G3Inv(a45) \land $ \\ 
 $ E1G3Inv(a12_a62) \land $ \\ 
 $ E1G3Inv(a66_a7_a71) \land $ \\ 
 $ E1G3Inv(a99) \land $ \\ 
 $ E1G3Inv(a21) \land $ \\ 
 $ E1G3Inv(a14_a60_a63) \land $ \\ 
 $ E1G3Inv(a89) \land $ \\ 
 $ E1G3Inv(a19) \land $ \\ 
 $ E1G3Inv(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $ E1G3Inv(a79_a81) \land $ \\ 
 $ E1G3Inv(a40) \land $ \\ 
 $ E1G3Inv(a82) \land $ \\ 
 $ E1G3Inv(a29) \land $ \\ 
 $ E1G3Inv(a56_a31) \land $ \\ 
 $ E1G3Inv(a87) \land $ \\ 
 $ E1G3Inv(a23) \land $ \\ 
 $ E1G3Inv(a57) \land $ \\ 
 $ E1G3Inv(a33_a36) \land $ \\ 
 $ E1G3Inv(a37) \land $ \\ 
 $ E1G3Inv(a5_a69) \land $ \\ 
 $ E1G3Inv(a76) \land $ \\ 
 $ E1G3Inv(a50) \land $ \\ 
 $ E1G3Inv(a95) \land $ \\ 
 $ E1G3Inv(a8_a86) \land $ \\ 
 $ E1G3Inv(a35_a49_a97) \land $ \\ 
 $ E1G3Inv(a65) \land $ \\ 
 $ E1G3Inv(a25_a9) \land $ \\ 
 $ E1G3Inv(a54_a67_a72) \land $ \\ 
 $ E1G3Inv(a77) \land $ \\ 
 $ E1G3Inv(a15) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a32_a80_a70_a94) \land $ \\ 
 $  \Rnext  \Rnext C3(a78) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a56_a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a78) \land $ \\ 
 $  \Rnext  \Rnext C2(a51) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a21) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a35_a49_a97) \land $ \\ 
 $  \Rnext  \Rnext C1(a37) \land $ \\ 
 $ E3G2(a95) \land $ \\ 
 $ E3G2(a51) \land $ \\ 
 $ E3G2(a29) \land $ \\ 
 $ E3G2(a37) \land $ \\ 
 $ E3G2(a57) \land $ \\ 
 $ E3G2(a45) \land $ \\ 
 $ E3G2(a65) \land $ \\ 
 $ E3G2(a100) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a19) \land $ \\ 
 $ E3G2(a79_a81) \land $ \\ 
 $ E3G2(a8_a86) \land $ \\ 
 $ E3G2(a61) \land $ \\ 
 $ E3G2(a33_a36) \land $ \\ 
 $ E3G2(a15) \land $ \\ 
 $ E3G2(a19) \land $ \\ 
 $ E3G2(a66_a7_a71) \land $ \\ 
 $ E3G2(a77) \land $ \\ 
 $ E3G2(a17) \land $ \\ 
 $ E3G2(a12_a62) \land $ \\ 
 $ E3G2(a32_a80_a70_a94) \land $ \\ 
 $ E3G2(a78) \land $ \\ 
 $ E3G2(a40) \land $ \\ 
 $ E3G2(a35_a49_a97) \land $ \\ 
 $ E3G2(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $ E3G2(a25_a9) \land $ \\ 
 $ E3G2(a58) \land $ \\ 
 $ E3G2(a99) \land $ \\ 
 $ E3G2(a54_a67_a72) \land $ \\ 
 $ E3G2(a23) \land $ \\ 
 $ E3G2(a2) \land $ \\ 
 $ E3G2(a56_a31) \land $ \\ 
 $ E3G2(a55) \land $ \\ 
 $ E3G2(a5_a69) \land $ \\ 
 $ E3G2(a76) \land $ \\ 
 $ E3G2(a82) \land $ \\ 
 $ E3G2(a87) \land $ \\ 
 $ E3G2(a50) \land $ \\ 
 $ E3G2(a14_a60_a63) \land $ \\ 
 $ E3G2(a21) \land $ \\ 
 $ E3G2(a89) \land $ \\ 
 $ E3G2(a73) \land $ \\ 
 $  \Rnext E3L1(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a40) \land $ \\ 
 $  \Rnext C2(a95) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a45) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a40) \land $ \\ 
 $  \Rnext E3L1Inv(a76) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a66_a7_a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a12_a62) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a55) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a51) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a23) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a32_a80_a70_a94) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a100) \land $ \\ 
 $  \Rnext C2(a19) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a12_a62) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a5_a69) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a51) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a79_a81) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a35_a49_a97) \land $ \\ 
 $  \Rnext E3L0Inv(a87) \land $ \\ 
 $  \Rnext  \Rnext C0(a76) \land $ \\ 
 $  \Rnext E3L1(a82) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a51) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a61) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a5_a69) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a32_a80_a70_a94) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a89) \land $ \\ 
 $  \Rnext C2(a66_a7_a71) \land $ \\ 
 $  \Rnext E3L1(a51) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a21) \land $ \\ 
 $  \Rnext E3L1Inv(a45) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a19) \land $ \\ 
 $  \Rnext  \Rnext C3(a2) \land $ \\ 
 $  \Rnext E3L0(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a32_a80_a70_a94) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a79_a81) \land $ \\ 
 $  \Rnext  \Rnext C3(a12_a62) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a12_a62) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a56_a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a78) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a100) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a32_a80_a70_a94) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a79_a81) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a58) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a17) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a40) \land $ \\ 
 $  \Rnext E3L0(a2) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a17) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a95) \land $ \\ 
 $  \Rnext C1(a2) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a55) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a76) \land $ \\ 
 $  \Rnext C3(a2) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a33_a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a8_a86) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a77) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a57) \land $ \\ 
 $  \Rnext E3L1(a40) \land $ \\ 
 $  \Rnext  \Rnext C1(a55) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a12_a62) \land $ \\ 
 $  \Rnext  \Rnext C2(a45) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a76) \land $ \\ 
 $  \Rnext C1(a19) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a57) \land $ \\ 
 $  \Rnext E2L2Inv(a66_a7_a71) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a87) \land $ \\ 
 $  \Rnext E2L2(a51) \land $ \\ 
 $  \Rnext E2L2Inv(a33_a36) \land $ \\ 
 $ C1(a51) \land $ \\ 
 $ C1(a29) \land $ \\ 
 $ C1(a2) \land $ \\ 
 $ C1(a65) \land $ \\ 
 $ C1(a82) \land $ \\ 
 $ C1(a87) \land $ \\ 
 $ C1(a17) \land $ \\ 
 $ C1(a5_a69) \land $ \\ 
 $ C1(a89) \land $ \\ 
 $ C1(a33_a36) \land $ \\ 
 $ C1(a77) \land $ \\ 
 $ C1(a14_a60_a63) \land $ \\ 
 $ C1(a54_a67_a72) \land $ \\ 
 $ C1(a15) \land $ \\ 
 $ C1(a61) \land $ \\ 
 $ C1(a37) \land $ \\ 
 $ C1(a58) \land $ \\ 
 $ C1(a50) \land $ \\ 
 $ C1(a45) \land $ \\ 
 $ C1(a12_a62) \land $ \\ 
 $ C1(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $ C1(a57) \land $ \\ 
 $ C1(a25_a9) \land $ \\ 
 $ C1(a8_a86) \land $ \\ 
 $ C1(a73) \land $ \\ 
 $ C1(a66_a7_a71) \land $ \\ 
 $ C1(a40) \land $ \\ 
 $ C1(a55) \land $ \\ 
 $ C1(a78) \land $ \\ 
 $ C1(a56_a31) \land $ \\ 
 $ C1(a23) \land $ \\ 
 $ C1(a19) \land $ \\ 
 $ C1(a100) \land $ \\ 
 $ C1(a99) \land $ \\ 
 $ C1(a79_a81) \land $ \\ 
 $ C1(a35_a49_a97) \land $ \\ 
 $ C1(a21) \land $ \\ 
 $  \Rnext E3L0(a55) \land $ \\ 
 $  \Rnext C0(a76) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a17) \land $ \\ 
 $  \Rnext E3L0(a51) \land $ \\ 
 $  \Rnext  \Rnext C0(a56_a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a35_a49_a97) \land $ \\ 
 $  \Rnext  \Rnext C2(a19) \land $ \\ 
 $  \Rnext C0(a77) \land $ \\ 
 $  \Rnext C2(a35_a49_a97) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a5_a69) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a57) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a40) \land $ \\ 
 $  \Rnext C3(a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a25_a9) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a100) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $  \Rnext C0(a17) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a79_a81) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a15) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a95) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a76) \land $ \\ 
 $  \Rnext C3(a56_a31) \land $ \\ 
 $  \Rnext C0(a73) \land $ \\ 
 $  \Rnext  \Rnext C1(a17) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a8_a86) \land $ \\ 
 $  \Rnext  \Rnext C2(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a23) \land $ \\ 
 $  \Rnext E3L1(a23) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a57) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a14_a60_a63) \land $ \\ 
 $  \Rnext E3L0Inv(a37) \land $ \\ 
 $ E3L1(a5_a69) \land $ \\ 
 $ E3L1(a8_a86) \land $ \\ 
 $ E3L1(a32_a80_a70_a94) \land $ \\ 
 $ E3L1(a65) \land $ \\ 
 $ E3L1(a61) \land $ \\ 
 $ E3L1(a14_a60_a63) \land $ \\ 
 $ E3L1(a17) \land $ \\ 
 $ E3L1(a57) \land $ \\ 
 $ E3L1(a45) \land $ \\ 
 $ E3L1(a66_a7_a71) \land $ \\ 
 $ E3L1(a58) \land $ \\ 
 $ E3L1(a73) \land $ \\ 
 $ E3L1(a51) \land $ \\ 
 $ E3L1(a21) \land $ \\ 
 $ E3L1(a54_a67_a72) \land $ \\ 
 $ E3L1(a89) \land $ \\ 
 $ E3L1(a50) \land $ \\ 
 $ E3L1(a40) \land $ \\ 
 $ E3L1(a19) \land $ \\ 
 $ E3L1(a79_a81) \land $ \\ 
 $ E3L1(a95) \land $ \\ 
 $ E3L1(a76) \land $ \\ 
 $ E3L1(a87) \land $ \\ 
 $ E3L1(a82) \land $ \\ 
 $ E3L1(a25_a9) \land $ \\ 
 $ E3L1(a15) \land $ \\ 
 $ E3L1(a33_a36) \land $ \\ 
 $ E3L1(a23) \land $ \\ 
 $ E3L1(a29) \land $ \\ 
 $ E3L1(a37) \land $ \\ 
 $ E3L1(a12_a62) \land $ \\ 
 $ E3L1(a2) \land $ \\ 
 $ E3L1(a100) \land $ \\ 
 $ E3L1(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $ E3L1(a78) \land $ \\ 
 $ E3L1(a35_a49_a97) \land $ \\ 
 $ E3L1(a99) \land $ \\ 
 $ E3L1(a55) \land $ \\ 
 $ E3L1(a56_a31) \land $ \\ 
 $ E3L1(a77) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a99) \land $ \\ 
 $  \Rnext E3L0(a73) \land $ \\ 
 $  \Rnext E3L0Inv(a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a65) \land $ \\ 
 $  \Rnext  \Rnext C1(a61) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a54_a67_a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a45) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a89) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a76) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a55) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a51) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a15) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a95) \land $ \\ 
 $  \Rnext E3L1(a87) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a19) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a56_a31) \land $ \\ 
 $  \Rnext E3L1(a19) \land $ \\ 
 $  \Rnext E3L1(a8_a86) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a8_a86) \land $ \\ 
 $  \Rnext E3L1(a45) \land $ \\ 
 $  \Rnext E2L2(a56_a31) \land $ \\ 
 $  \Rnext  \Rnext C0(a87) \land $ \\ 
 $  \Rnext C2(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a51) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a79_a81) \land $ \\ 
 $  \Rnext E3L0Inv(a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a100) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a23) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a8_a86) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a14_a60_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a37) \land $ \\ 
 $  \Rnext E2L2(a57) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a78) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a12_a62) \land $ \\ 
 $  \Rnext C1(a12_a62) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a14_a60_a63) \land $ \\ 
 $  \Rnext  \Rnext C1(a66_a7_a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a73) \land $ \\ 
 $  \Rnext E3L0Inv(a57) \land $ \\ 
 $  \Rnext E2L2Inv(a2) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a89) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a50) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a15) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a25_a9) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a14_a60_a63) \land $ \\ 
 $  \Rnext C2(a54_a67_a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a29) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a17) \land $ \\ 
 $  \Rnext E3L0(a8_a86) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a55) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a87) \land $ \\ 
 $  \Rnext  \Rnext C0(a23) \land $ \\ 
 $  \Rnext E2L2Inv(a14_a60_a63) \land $ \\ 
 $  \Rnext E2L2(a66_a7_a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a14_a60_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a33_a36) \land $ \\ 
 $  \Rnext E3L1Inv(a21) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a33_a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a51) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a33_a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a51) \land $ \\ 
 $  \Rnext C0(a32_a80_a70_a94) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a76) \land $ \\ 
 $  \Rnext E3L1(a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a33_a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a54_a67_a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a79_a81) \land $ \\ 
 $  \Rnext E3L0Inv(a32_a80_a70_a94) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a95) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a56_a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a87) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a89) \land $ \\ 
 $  \Rnext C0(a66_a7_a71) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a100) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a89) \land $ \\ 
 $  \Rnext  \Rnext C2(a57) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a56_a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a35_a49_a97) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a100) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a12_a62) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a99) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a12_a62) \land $ \\ 
 $  \Rnext C0(a56_a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a79_a81) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a32_a80_a70_a94) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a25_a9) \land $ \\ 
 $  \Rnext C0(a79_a81) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a76) \land $ \\ 
 $  \Rnext E3L1Inv(a66_a7_a71) \land $ \\ 
 $  \Rnext E2L2(a77) \land $ \\ 
 $  \Rnext E3L1(a55) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a87) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a77) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a25_a9) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a8_a86) \land $ \\ 
 $  \Rnext E2L2(a78) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a32_a80_a70_a94) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a32_a80_a70_a94) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a40) \land $ \\ 
 $  \Rnext C1(a66_a7_a71) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a55) \land $ \\ 
 $  \Rnext E2L2Inv(a45) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a21) \land $ \\ 
 $  \Rnext  \Rnext C2(a76) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a15) \land $ \\ 
 $  \Rnext  \Rnext C0(a8_a86) \land $ \\ 
 $  \Rnext C1(a76) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a32_a80_a70_a94) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a55) \land $ \\ 
 $  \Rnext  \Rnext C0(a5_a69) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a21) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a54_a67_a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a21) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a35_a49_a97) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a66_a7_a71) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a79_a81) \land $ \\ 
 $  \Rnext C2(a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a45) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a19) \land $ \\ 
 $  \Rnext  \Rnext C2(a25_a9) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a79_a81) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a15) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a2) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a95) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a15) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a19) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a8_a86) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a82) \land $ \\ 
 $ E3L0Inv(a56_a31) \land $ \\ 
 $ E3L0Inv(a21) \land $ \\ 
 $ E3L0Inv(a32_a80_a70_a94) \land $ \\ 
 $ E3L0Inv(a51) \land $ \\ 
 $ E3L0Inv(a50) \land $ \\ 
 $ E3L0Inv(a58) \land $ \\ 
 $ E3L0Inv(a55) \land $ \\ 
 $ E3L0Inv(a2) \land $ \\ 
 $ E3L0Inv(a12_a62) \land $ \\ 
 $ E3L0Inv(a29) \land $ \\ 
 $ E3L0Inv(a23) \land $ \\ 
 $ E3L0Inv(a73) \land $ \\ 
 $ E3L0Inv(a87) \land $ \\ 
 $ E3L0Inv(a14_a60_a63) \land $ \\ 
 $ E3L0Inv(a5_a69) \land $ \\ 
 $ E3L0Inv(a33_a36) \land $ \\ 
 $ E3L0Inv(a79_a81) \land $ \\ 
 $ E3L0Inv(a25_a9) \land $ \\ 
 $ E3L0Inv(a82) \land $ \\ 
 $ E3L0Inv(a76) \land $ \\ 
 $ E3L0Inv(a15) \land $ \\ 
 $ E3L0Inv(a100) \land $ \\ 
 $ E3L0Inv(a8_a86) \land $ \\ 
 $ E3L0Inv(a61) \land $ \\ 
 $ E3L0Inv(a35_a49_a97) \land $ \\ 
 $ E3L0Inv(a89) \land $ \\ 
 $ E3L0Inv(a37) \land $ \\ 
 $ E3L0Inv(a95) \land $ \\ 
 $ E3L0Inv(a66_a7_a71) \land $ \\ 
 $ E3L0Inv(a45) \land $ \\ 
 $ E3L0Inv(a57) \land $ \\ 
 $ E3L0Inv(a77) \land $ \\ 
 $ E3L0Inv(a78) \land $ \\ 
 $ E3L0Inv(a65) \land $ \\ 
 $ E3L0Inv(a99) \land $ \\ 
 $ E3L0Inv(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $ E3L0Inv(a54_a67_a72) \land $ \\ 
 $ E3L0Inv(a17) \land $ \\ 
 $ E3L0Inv(a19) \land $ \\ 
 $ E3L0Inv(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a100) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a17) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a95) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a21) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a57) \land $ \\ 
 $  \Rnext C2(a78) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a25_a9) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a61) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a37) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a8_a86) \land $ \\ 
 $  \Rnext E2L2(a89) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a56_a31) \land $ \\ 
 $  \Rnext C0(a35_a49_a97) \land $ \\ 
 $  \Rnext C1(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a5_a69) \land $ \\ 
 $  \Rnext E3L0Inv(a23) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a61) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a45) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a51) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a76) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a12_a62) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a58) \land $ \\ 
 $  \Rnext C3(a17) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a21) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a14_a60_a63) \land $ \\ 
 $  \Rnext E2L2Inv(a58) \land $ \\ 
 $  \Rnext E3L1(a61) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a78) \land $ \\ 
 $  \Rnext  \Rnext C0(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a77) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a2) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a35_a49_a97) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a66_a7_a71) \land $ \\ 
 $  \Rnext C3(a32_a80_a70_a94) \land $ \\ 
 $  \Rnext E3L1Inv(a8_a86) \land $ \\ 
 $  \Rnext E2L2(a12_a62) \land $ \\ 
 $ E2L2Inv(a56_a31) \land $ \\ 
 $ E2L2Inv(a61) \land $ \\ 
 $  \Rnext C2(a14_a60_a63) \land $ \\ 
 $ E2L2Inv(a54_a67_a72) \land $ \\ 
 $ E2L2Inv(a95) \land $ \\ 
 $ E2L2Inv(a21) \land $ \\ 
 $ E2L2Inv(a51) \land $ \\ 
 $ E2L2Inv(a15) \land $ \\ 
 $ E2L2Inv(a25_a9) \land $ \\ 
 $ E2L2Inv(a17) \land $ \\ 
 $ E2L2Inv(a8_a86) \land $ \\ 
 $ E2L2Inv(a2) \land $ \\ 
 $ E2L2Inv(a57) \land $ \\ 
 $ E2L2Inv(a40) \land $ \\ 
 $ E2L2Inv(a33_a36) \land $ \\ 
 $ E2L2Inv(a50) \land $ \\ 
 $ E2L2Inv(a78) \land $ \\ 
 $ E2L2Inv(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $ E2L2Inv(a87) \land $ \\ 
 $ E2L2Inv(a45) \land $ \\ 
 $ E2L2Inv(a5_a69) \land $ \\ 
 $ E2L2Inv(a32_a80_a70_a94) \land $ \\ 
 $ E2L2Inv(a19) \land $ \\ 
 $ E2L2Inv(a29) \land $ \\ 
 $ E2L2Inv(a14_a60_a63) \land $ \\ 
 $ E2L2Inv(a99) \land $ \\ 
 $ E2L2Inv(a65) \land $ \\ 
 $ E2L2Inv(a82) \land $ \\ 
 $ E2L2Inv(a100) \land $ \\ 
 $ E2L2Inv(a23) \land $ \\ 
 $ E2L2Inv(a76) \land $ \\ 
 $ E2L2Inv(a73) \land $ \\ 
 $ E2L2Inv(a12_a62) \land $ \\ 
 $ E2L2Inv(a37) \land $ \\ 
 $ E2L2Inv(a89) \land $ \\ 
 $ E2L2Inv(a58) \land $ \\ 
 $ E2L2Inv(a55) \land $ \\ 
 $ E2L2Inv(a77) \land $ \\ 
 $ E2L2Inv(a35_a49_a97) \land $ \\ 
 $ E2L2Inv(a79_a81) \land $ \\ 
 $ E2L2Inv(a66_a7_a71) \land $ \\ 
 $  \Rnext  \Rnext C2(a12_a62) \land $ \\ 
 $  \Rnext  \Rnext C2(a56_a31) \land $ \\ 
 $  \Rnext  \Rnext C3(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a56_a31) \land $ \\ 
 $  \Rnext  \Rnext C2(a55) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a17) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a14_a60_a63) \land $ \\ 
 $  \Rnext E3L1(a66_a7_a71) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a15) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a29) \land $ \\ 
 $  \Rnext C0(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a37) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a21) \land $ \\ 
 $  \Rnext  \Rnext C3(a37) \land $ \\ 
 $  \Rnext C0(a57) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a23) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a61) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a15) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a95) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a32_a80_a70_a94) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a79_a81) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a8_a86) \land $ \\ 
 $  \Rnext C2(a57) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a95) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a82) \land $ \\ 
 $  \Rnext  \Rnext C0(a45) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a35_a49_a97) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a15) \land $ \\ 
 $  \Rnext E2L2(a45) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a58) \land $ \\ 
 $  \Rnext  \Rnext C0(a65) \land $ \\ 
 $  \Rnext C3(a19) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a56_a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a8_a86) \land $ \\ 
 $  \Rnext C0(a58) \land $ \\ 
 $  \Rnext C2(a56_a31) \land $ \\ 
 $  \Rnext  \Rnext C0(a55) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a12_a62) \land $ \\ 
 $  \Rnext E3L1(a99) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a5_a69) \land $ \\ 
 $  \Rnext  \Rnext C0(a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a55) \land $ \\ 
 $  \Rnext E2L2Inv(a82) \land $ \\ 
 $  \Rnext E3L1Inv(a58) \land $ \\ 
 $  \Rnext C2(a5_a69) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a15) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a21) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a66_a7_a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a76) \land $ \\ 
 $  \Rnext E2L2Inv(a35_a49_a97) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a35_a49_a97) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a19) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a5_a69) \land $ \\ 
 $  \Rnext  \Rnext C0(a15) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a33_a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a2) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a15) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a78) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a77) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a5_a69) \land $ \\ 
 $  \Rnext  \Rnext C2(a21) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a17) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a21) \land $ \\ 
 $  \Rnext  \Rnext C0(a25_a9) \land $ \\ 
 $  \Rnext  \Rnext C1(a2) \land $ \\ 
 $  \Rnext  \Rnext C3(a55) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a77) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a15) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a25_a9) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a35_a49_a97) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a54_a67_a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a2) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a8_a86) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a76) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a5_a69) \land $ \\ 
 $  \Rnext C3(a45) \land $ \\ 
 $  \Rnext C3(a78) \land $ \\ 
 $  \Rnext C1(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a37) \land $ \\ 
 $  \Rnext  \Rnext C3(a35_a49_a97) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a8_a86) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a19) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a51) \land $ \\ 
 $  \Rnext  \Rnext C3(a33_a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a78) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a25_a9) \land $ \\ 
 $  \Rnext C1(a65) \land $ \\ 
 $  \Rnext C1(a17) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a100) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a61) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a32_a80_a70_a94) \land $ \\ 
 $  \Rnext  \Rnext C2(a79_a81) \land $ \\ 
 $  \Rnext E3L0Inv(a95) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a35_a49_a97) \land $ \\ 
 $  \Rnext  \Rnext C3(a21) \land $ \\ 
 $  \Rnext E3L1(a54_a67_a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a95) \land $ \\ 
 $  \Rnext  \Rnext C1(a57) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a57) \land $ \\ 
 $  \Rnext C1(a51) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a15) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a8_a86) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a78) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a15) \land $ \\ 
 $  \Rnext C3(a66_a7_a71) \land $ \\ 
 $  \Rnext  \Rnext C0(a17) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a82) \land $ \\ 
 $  \Rnext C0(a2) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a33_a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a76) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $  \Rnext  \Rnext C2(a58) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext C3(a5_a69) \land $ \\ 
 $  \Rnext  \Rnext C1(a14_a60_a63) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a61) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a50) \land $ \\ 
 $  \Rnext E2L2(a50) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a32_a80_a70_a94) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a66_a7_a71) \land $ \\ 
 $  \Rnext E2L2(a58) \land $ \\ 
 $  \Rnext C3(a61) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a56_a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a8_a86) \land $ \\ 
 $  \Rnext E2L2(a32_a80_a70_a94) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a87) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a65) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a54_a67_a72) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a78) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a21) \land $ \\ 
 $  \Rnext C0(a15) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a54_a67_a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a17) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a23) \land $ \\ 
 $  \Rnext  \Rnext C0(a32_a80_a70_a94) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $  \Rnext  \Rnext C3(a66_a7_a71) \land $ \\ 
 $  \Rnext C2(a21) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a61) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a23) \land $ \\ 
 $ C2(a79_a81) \land $ \\ 
 $ C2(a17) \land $ \\ 
 $  \Rnext C2(a87) \land $ \\ 
 $ C2(a12_a62) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a89) \land $ \\ 
 $ C2(a51) \land $ \\ 
 $ C2(a21) \land $ \\ 
 $ C2(a58) \land $ \\ 
 $ C2(a76) \land $ \\ 
 $ C2(a73) \land $ \\ 
 $ C2(a45) \land $ \\ 
 $ C2(a77) \land $ \\ 
 $ C2(a95) \land $ \\ 
 $ C2(a15) \land $ \\ 
 $ C2(a89) \land $ \\ 
 $ C2(a78) \land $ \\ 
 $ C2(a40) \land $ \\ 
 $ C2(a87) \land $ \\ 
 $ C2(a25_a9) \land $ \\ 
 $ C2(a55) \land $ \\ 
 $ C2(a2) \land $ \\ 
 $ C2(a32_a80_a70_a94) \land $ \\ 
 $ C2(a14_a60_a63) \land $ \\ 
 $ C2(a82) \land $ \\ 
 $ C2(a61) \land $ \\ 
 $ C2(a5_a69) \land $ \\ 
 $ C2(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $ C2(a8_a86) \land $ \\ 
 $ C2(a54_a67_a72) \land $ \\ 
 $ C2(a33_a36) \land $ \\ 
 $ C2(a99) \land $ \\ 
 $ C2(a23) \land $ \\ 
 $ C2(a65) \land $ \\ 
 $ C2(a19) \land $ \\ 
 $ C2(a50) \land $ \\ 
 $ C2(a56_a31) \land $ \\ 
 $ C2(a66_a7_a71) \land $ \\ 
 $ C2(a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a45) \land $ \\ 
 $  \Rnext C2(a17) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a17) \land $ \\ 
 $  \Rnext E2L2Inv(a21) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a79_a81) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a32_a80_a70_a94) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a33_a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a61) \land $ \\ 
 $  \Rnext E3L1(a17) \land $ \\ 
 $  \Rnext E3L1Inv(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a56_a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a61) \land $ \\ 
 $  \Rnext E3L0Inv(a15) \land $ \\ 
 $  \Rnext  \Rnext C3(a15) \land $ \\ 
 $  \Rnext E3L0Inv(a65) \land $ \\ 
 $  \Rnext  \Rnext C1(a51) \land $ \\ 
 $  \Rnext E3L0Inv(a76) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a19) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a89) \land $ \\ 
 $  \Rnext E3L0(a78) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a2) \land $ \\ 
 $  \Rnext E2L2(a82) \land $ \\ 
 $  \Rnext  \Rnext C1(a40) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a12_a62) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a5_a69) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a15) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a29) \land $ \\ 
 $  \Rnext E3L1(a35_a49_a97) \land $ \\ 
 $  \Rnext E3L1Inv(a79_a81) \land $ \\ 
 $  \Rnext  \Rnext C1(a73) \land $ \\ 
 $  \Rnext  \Rnext C3(a79_a81) \land $ \\ 
 $  \Rnext C3(a35_a49_a97) \land $ \\ 
 $  \Rnext  \Rnext C0(a57) \land $ \\ 
 $  \Rnext E3L0Inv(a35_a49_a97) \land $ \\ 
 $  \Rnext E3L1Inv(a5_a69) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a5_a69) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a57) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a33_a36) \land $ \\ 
 $  \Rnext C3(a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a77) \land $ \\ 
 $  \Rnext E3L1Inv(a55) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a56_a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a2) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a58) \land $ \\ 
 $  \Rnext  \Rnext C1(a35_a49_a97) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a25_a9) \land $ \\ 
 $  \Rnext E3L0(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a29) \land $ \\ 
 $  \Rnext  \Rnext C3(a77) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a66_a7_a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a95) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a77) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a12_a62) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a65) \land $ \\ 
 $  \Rnext E3L0Inv(a61) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a76) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a45) \land $ \\ 
 $  \Rnext E2L2Inv(a54_a67_a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a23) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a78) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a15) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a12_a62) \land $ \\ 
 $  \Rnext E2L2(a35_a49_a97) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a23) \land $ \\ 
 $  \Rnext  \Rnext C2(a95) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a19) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a29) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a100) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a58) \land $ \\ 
 $  \Rnext C2(a89) \land $ \\ 
 $  \Rnext E3L0Inv(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a78) \land $ \\ 
 $  \Rnext  \Rnext C1(a21) \land $ \\ 
 $  \Rnext  \Rnext C2(a54_a67_a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a19) \land $ \\ 
 $  \Rnext C0(a25_a9) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a14_a60_a63) \land $ \\ 
 $  \Rnext E3L1Inv(a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a54_a67_a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a76) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a45) \land $ \\ 
 $  \Rnext C1(a15) \land $ \\ 
 $  \Rnext  \Rnext C0(a50) \land $ \\ 
 $  \Rnext E3L1Inv(a15) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a15) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a87) \land $ \\ 
 $  \Rnext E2L2Inv(a100) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a40) \land $ \\ 
 $  \Rnext E3L0(a79_a81) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a33_a36) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a87) \land $ \\ 
 $  \Rnext C2(a76) \land $ \\ 
 $  \Rnext E2L2(a61) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a66_a7_a71) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a8_a86) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a25_a9) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a25_a9) \land $ \\ 
 $  \Rnext  \Rnext C3(a95) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a99) \land $ \\ 
 $  \Rnext  \Rnext C2(a66_a7_a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a35_a49_a97) \land $ \\ 
 $  \Rnext E2L2Inv(a77) \land $ \\ 
 $  \Rnext E3L0(a54_a67_a72) \land $ \\ 
 $  \Rnext  \Rnext C2(a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a45) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a19) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a65) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a29) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a12_a62) \land $ \\ 
 $  \Rnext C2(a2) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a25_a9) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a35_a49_a97) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a100) \land $ \\ 
 $  \Rnext E3L1(a15) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a12_a62) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a15) \land $ \\ 
 $  \Rnext C1(a54_a67_a72) \land $ \\ 
 $  \Rnext E3L0Inv(a21) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a66_a7_a71) \land $ \\ 
 $  \Rnext E2L2Inv(a23) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a23) \land $ \\ 
 $  \Rnext E3L1Inv(a100) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a23) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a65) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a95) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a35_a49_a97) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a17) \land $ \\ 
 $  \Rnext  \Rnext C0(a78) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a61) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a5_a69) \land $ \\ 
 $  \Rnext E3L1Inv(a54_a67_a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a99) \land $ \\ 
 $  \Rnext C2(a100) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a19) \land $ \\ 
 $  \Rnext C2(a65) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a100) \land $ \\ 
 $  \Rnext C2(a32_a80_a70_a94) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a95) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a56_a31) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a45) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a56_a31) \land $ \\ 
 $  \Rnext E3L0Inv(a54_a67_a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a32_a80_a70_a94) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a2) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a45) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a61) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a32_a80_a70_a94) \land $ \\ 
 $  \Rnext E3L1Inv(a23) \land $ \\ 
 $  \Rnext C3(a89) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a95) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a33_a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a2) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a73) \land $ \\ 
 $  \Rnext C2(a23) \land $ \\ 
 $  \Rnext C1(a50) \land $ \\ 
 $  \Rnext  \Rnext C2(a35_a49_a97) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a12_a62) \land $ \\ 
 $  \Rnext E3L1Inv(a17) \land $ \\ 
 $  \Rnext E3L1Inv(a12_a62) \land $ \\ 
 $  \Rnext C1(a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a25_a9) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a5_a69) \land $ \\ 
 $  \Rnext E2L2Inv(a5_a69) \land $ \\ 
 $  \Rnext  \Rnext C0(a77) \land $ \\ 
 $  \Rnext  \Rnext C1(a78) \land $ \\ 
 $  \Rnext C1(a56_a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a32_a80_a70_a94) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a23) \land $ \\ 
 $  \Rnext E2L2Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a87) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a57) \land $ \\ 
 $  \Rnext C3(a55) \land $ \\ 
 $  \Rnext E3L0(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a23) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a73) \land $ \\ 
 $  \Rnext E3L1(a56_a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a14_a60_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a21) \land $ \\ 
 $  \Rnext  \Rnext C0(a61) \land $ \\ 
 $  \Rnext E3L1Inv(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $  \Rnext C3(a14_a60_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a79_a81) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a61) \land $ \\ 
 $  \Rnext  \Rnext C2(a50) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a99) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a25_a9) \land $ \\ 
 $  \Rnext E3L1(a32_a80_a70_a94) \land $ \\ 
 $  \Rnext  \Rnext C2(a100) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a100) \land $ \\ 
 $  \Rnext E3L0Inv(a14_a60_a63) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a32_a80_a70_a94) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a56_a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a12_a62) \land $ \\ 
 $  \Rnext E3L1(a21) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a55) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a57) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a33_a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a5_a69) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a65) \land $ \\ 
 $  \Rnext E2L2Inv(a76) \land $ \\ 
 $ E1G2Inv(a33_a36) \land $ \\ 
 $ E1G2Inv(a29) \land $ \\ 
 $ E1G2Inv(a51) \land $ \\ 
 $ E1G2Inv(a21) \land $ \\ 
 $ E1G2Inv(a25_a9) \land $ \\ 
 $ E1G2Inv(a56_a31) \land $ \\ 
 $ E1G2Inv(a15) \land $ \\ 
 $ E1G2Inv(a99) \land $ \\ 
 $ E1G2Inv(a73) \land $ \\ 
 $ E1G2Inv(a58) \land $ \\ 
 $ E1G2Inv(a54_a67_a72) \land $ \\ 
 $ E1G2Inv(a40) \land $ \\ 
 $ E1G2Inv(a78) \land $ \\ 
 $ E1G2Inv(a66_a7_a71) \land $ \\ 
 $ E1G2Inv(a57) \land $ \\ 
 $ E1G2Inv(a19) \land $ \\ 
 $ E1G2Inv(a45) \land $ \\ 
 $ E1G2Inv(a5_a69) \land $ \\ 
 $ E1G2Inv(a14_a60_a63) \land $ \\ 
 $ E1G2Inv(a76) \land $ \\ 
 $ E1G2Inv(a82) \land $ \\ 
 $ E1G2Inv(a100) \land $ \\ 
 $ E1G2Inv(a89) \land $ \\ 
 $ E1G2Inv(a12_a62) \land $ \\ 
 $ E1G2Inv(a32_a80_a70_a94) \land $ \\ 
 $ E1G2Inv(a8_a86) \land $ \\ 
 $ E1G2Inv(a37) \land $ \\ 
 $ E1G2Inv(a55) \land $ \\ 
 $ E1G2Inv(a77) \land $ \\ 
 $ E1G2Inv(a35_a49_a97) \land $ \\ 
 $ E1G2Inv(a95) \land $ \\ 
 $ E1G2Inv(a50) \land $ \\ 
 $ E1G2Inv(a79_a81) \land $ \\ 
 $ E1G2Inv(a17) \land $ \\ 
 $ E1G2Inv(a23) \land $ \\ 
 $ E1G2Inv(a65) \land $ \\ 
 $ E1G2Inv(a2) \land $ \\ 
 $ E1G2Inv(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $ E1G2Inv(a61) \land $ \\ 
 $ E1G2Inv(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $  \Rnext E3L0(a45) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a37) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a89) \land $ \\ 
 $  \Rnext E3L0(a12_a62) \land $ \\ 
 $  \Rnext  \Rnext C3(a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a79_a81) \land $ \\ 
 $  \Rnext E3L0Inv(a40) \land $ \\ 
 $  \Rnext C3(a99) \land $ \\ 
 $  \Rnext C0(a82) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a2) \land $ \\ 
 $  \Rnext E3L1Inv(a33_a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a21) \land $ \\ 
 $  \Rnext E3L1Inv(a78) \land $ \\ 
 $  \Rnext C0(a61) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a100) \land $ \\ 
 $  \Rnext E2L2Inv(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a33_a36) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a15) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a5_a69) \land $ \\ 
 $  \Rnext  \Rnext C0(a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a66_a7_a71) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a5_a69) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a77) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a8_a86) \land $ \\ 
 $  \Rnext C0(a54_a67_a72) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a61) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a37) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a50) \land $ \\ 
 $  \Rnext E3L0(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $  \Rnext C3(a76) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a99) \land $ \\ 
 $  \Rnext  \Rnext C1(a25_a9) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a65) \land $ \\ 
 $  \Rnext E3L0Inv(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a65) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a76) \land $ \\ 
 $  \Rnext E3L0(a77) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a78) \land $ \\ 
 $  \Rnext E3L1Inv(a19) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a79_a81) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a57) \land $ \\ 
 $  \Rnext  \Rnext C2(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a65) \land $ \\ 
 $  \Rnext E3L1Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a23) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a45) \land $ \\ 
 $  \Rnext E3L1(a78) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a2) \land $ \\ 
 $  \Rnext E3L1(a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a8_a86) \land $ \\ 
 $  \Rnext  \Rnext C2(a5_a69) \land $ \\ 
 $  \Rnext C1(a87) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a77) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a73) \land $ \\ 
 $  \Rnext  \Rnext C0(a100) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a73) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a32_a80_a70_a94) \land $ \\ 
 $  \Rnext  \Rnext C0(a95) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a25_a9) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a65) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a2) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a33_a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a19) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a57) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a95) \land $ \\ 
 $  \Rnext  \Rnext C3(a54_a67_a72) \land $ \\ 
 $  \Rnext E3L0Inv(a2) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a35_a49_a97) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a57) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a2) \land $ \\ 
 $  \Rnext E3L1(a77) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a76) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a99) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a66_a7_a71) \land $ \\ 
 $  \Rnext C1(a99) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $  \Rnext  \Rnext C2(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a12_a62) \land $ \\ 
 $  \Rnext E3L0Inv(a19) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a76) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a54_a67_a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a66_a7_a71) \land $ \\ 
 $  \Rnext  \Rnext C2(a61) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a99) \land $ \\ 
 $  \Rnext E3L0(a100) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a23) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a56_a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a66_a7_a71) \land $ \\ 
 $  \Rnext  \Rnext C1(a79_a81) \land $ \\ 
 $  \Rnext C0(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a57) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a56_a31) \land $ \\ 
 $  \Rnext E2L2(a2) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a73) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a8_a86) \land $ \\ 
 $  \Rnext E2L2Inv(a57) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a35_a49_a97) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a12_a62) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a58) \land $ \\ 
 $  \Rnext E2L2(a5_a69) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $  \Rnext C3(a25_a9) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a57) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a55) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a61) \land $ \\ 
 $  \Rnext E3L1(a100) \land $ \\ 
 $  \Rnext  \Rnext C3(a87) \land $ \\ 
 $  \Rnext C2(a37) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a79_a81) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a21) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a45) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a56_a31) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a51) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a51) \land $ \\ 
 $  \Rnext  \Rnext C1(a12_a62) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a100) \land $ \\ 
 $  \Rnext E3L0Inv(a8_a86) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a54_a67_a72) \land $ \\ 
 $  \Rnext C3(a100) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a58) \land $ \\ 
 $  \Rnext E2L2Inv(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a57) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a14_a60_a63) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a51) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a65) \land $ \\ 
 $  \Rnext C0(a5_a69) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a25_a9) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a66_a7_a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a99) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a21) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a54_a67_a72) \land $ \\ 
 $  \Rnext C0(a95) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a79_a81) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a78) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a77) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a82) \land $ \\ 
 $  \Rnext E3L1Inv(a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a35_a49_a97) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a14_a60_a63) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a35_a49_a97) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a40) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a37) \land $ \\ 
 $  \Rnext E3L1Inv(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a55) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a21) \land $ \\ 
 $  \Rnext C2(a79_a81) \land $ \\ 
 $  \Rnext E3L1Inv(a61) \land $ \\ 
 $  \Rnext E3L1(a14_a60_a63) \land $ \\ 
 $  \Rnext C2(a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a5_a69) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a56_a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a35_a49_a97) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a51) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a89) \land $ \\ 
 $  \Rnext E2L2(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a2) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a23) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a5_a69) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a40) \land $ \\ 
 $  \Rnext  \Rnext C1(a56_a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $ C3(a51) \land $ \\ 
 $ C3(a2) \land $ \\ 
 $ C3(a29) \land $ \\ 
 $ C3(a8_a86) \land $ \\ 
 $ C3(a99) \land $ \\ 
 $ C3(a21) \land $ \\ 
 $ C3(a12_a62) \land $ \\ 
 $ C3(a5_a69) \land $ \\ 
 $ C3(a58) \land $ \\ 
 $ C3(a100) \land $ \\ 
 $ C3(a45) \land $ \\ 
 $ C3(a33_a36) \land $ \\ 
 $ C3(a61) \land $ \\ 
 $ C3(a57) \land $ \\ 
 $ C3(a66_a7_a71) \land $ \\ 
 $ C3(a95) \land $ \\ 
 $ C3(a87) \land $ \\ 
 $ C3(a15) \land $ \\ 
 $ C3(a19) \land $ \\ 
 $ C3(a76) \land $ \\ 
 $ C3(a78) \land $ \\ 
 $ C3(a50) \land $ \\ 
 $ C3(a73) \land $ \\ 
 $ C3(a17) \land $ \\ 
 $ C3(a35_a49_a97) \land $ \\ 
 $ C3(a65) \land $ \\ 
 $ C3(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $ C3(a89) \land $ \\ 
 $ C3(a14_a60_a63) \land $ \\ 
 $ C3(a77) \land $ \\ 
 $ C3(a37) \land $ \\ 
 $ C3(a79_a81) \land $ \\ 
 $ C3(a40) \land $ \\ 
 $ C3(a25_a9) \land $ \\ 
 $ C3(a82) \land $ \\ 
 $ C3(a54_a67_a72) \land $ \\ 
 $ C3(a32_a80_a70_a94) \land $ \\ 
 $ C3(a56_a31) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a17) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a21) \land $ \\ 
 $  \Rnext C0(a50) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a54_a67_a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a61) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a51) \land $ \\ 
 $  \Rnext C1(a55) \land $ \\ 
 $  \Rnext E2L2Inv(a73) \land $ \\ 
 $  \Rnext C2(a12_a62) \land $ \\ 
 $  \Rnext  \Rnext C1(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $  \Rnext E3L0Inv(a5_a69) \land $ \\ 
 $  \Rnext  \Rnext C3(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a99) \land $ \\ 
 $  \Rnext  \Rnext C0(a79_a81) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a14_a60_a63) \land $ \\ 
 $ E1G0(a82) \land $ \\ 
 $ E1G0(a21) \land $ \\ 
 $ E1G0(a51) \land $ \\ 
 $ E1G0(a35_a49_a97) \land $ \\ 
 $ E1G0(a66_a7_a71) \land $ \\ 
 $ E1G0(a37) \land $ \\ 
 $ E1G0(a32_a80_a70_a94) \land $ \\ 
 $ E1G0(a8_a86) \land $ \\ 
 $ E1G0(a78) \land $ \\ 
 $ E1G0(a54_a67_a72) \land $ \\ 
 $ E1G0(a77) \land $ \\ 
 $ E1G0(a29) \land $ \\ 
 $ E1G0(a57) \land $ \\ 
 $ E1G0(a19) \land $ \\ 
 $ E1G0(a45) \land $ \\ 
 $ E1G0(a50) \land $ \\ 
 $ E1G0(a33_a36) \land $ \\ 
 $ E1G0(a100) \land $ \\ 
 $ E1G0(a23) \land $ \\ 
 $ E1G0(a17) \land $ \\ 
 $ E1G0(a40) \land $ \\ 
 $ E1G0(a76) \land $ \\ 
 $ E1G0(a15) \land $ \\ 
 $ E1G0(a5_a69) \land $ \\ 
 $ E1G0(a58) \land $ \\ 
 $ E1G0(a12_a62) \land $ \\ 
 $ E1G0(a25_a9) \land $ \\ 
 $ E1G0(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $ E1G0(a56_a31) \land $ \\ 
 $ E1G0(a99) \land $ \\ 
 $ E1G0(a55) \land $ \\ 
 $ E1G0(a95) \land $ \\ 
 $ E1G0(a65) \land $ \\ 
 $ E1G0(a61) \land $ \\ 
 $ E1G0(a89) \land $ \\ 
 $ E1G0(a73) \land $ \\ 
 $ E1G0(a87) \land $ \\ 
 $ E1G0(a2) \land $ \\ 
 $ E1G0(a14_a60_a63) \land $ \\ 
 $ E1G0(a79_a81) \land $ \\ 
 $  \Rnext  \Rnext C2(a8_a86) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a8_a86) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a77) \land $ \\ 
 $  \Rnext C3(a95) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a77) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a54_a67_a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a55) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a77) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a76) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a23) \land $ \\ 
 $  \Rnext  \Rnext C0(a73) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a89) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a55) \land $ \\ 
 $ E3L1Inv(a29) \land $ \\ 
 $ E3L1Inv(a51) \land $ \\ 
 $ E3L1Inv(a21) \land $ \\ 
 $ E3L1Inv(a57) \land $ \\ 
 $ E3L1Inv(a23) \land $ \\ 
 $ E3L1Inv(a76) \land $ \\ 
 $ E3L1Inv(a19) \land $ \\ 
 $ E3L1Inv(a50) \land $ \\ 
 $ E3L1Inv(a87) \land $ \\ 
 $ E3L1Inv(a32_a80_a70_a94) \land $ \\ 
 $ E3L1Inv(a82) \land $ \\ 
 $ E3L1Inv(a14_a60_a63) \land $ \\ 
 $ E3L1Inv(a56_a31) \land $ \\ 
 $ E3L1Inv(a8_a86) \land $ \\ 
 $ E3L1Inv(a73) \land $ \\ 
 $ E3L1Inv(a89) \land $ \\ 
 $ E3L1Inv(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $ E3L1Inv(a95) \land $ \\ 
 $ E3L1Inv(a58) \land $ \\ 
 $ E3L1Inv(a33_a36) \land $ \\ 
 $ E3L1Inv(a55) \land $ \\ 
 $ E3L1Inv(a61) \land $ \\ 
 $ E3L1Inv(a54_a67_a72) \land $ \\ 
 $ E3L1Inv(a100) \land $ \\ 
 $ E3L1Inv(a12_a62) \land $ \\ 
 $ E3L1Inv(a37) \land $ \\ 
 $ E3L1Inv(a40) \land $ \\ 
 $ E3L1Inv(a78) \land $ \\ 
 $ E3L1Inv(a5_a69) \land $ \\ 
 $ E3L1Inv(a77) \land $ \\ 
 $ E3L1Inv(a25_a9) \land $ \\ 
 $ E3L1Inv(a79_a81) \land $ \\ 
 $ E3L1Inv(a17) \land $ \\ 
 $ E3L1Inv(a35_a49_a97) \land $ \\ 
 $ E3L1Inv(a2) \land $ \\ 
 $ E3L1Inv(a99) \land $ \\ 
 $ E3L1Inv(a65) \land $ \\ 
 $ E3L1Inv(a15) \land $ \\ 
 $ E3L1Inv(a66_a7_a71) \land $ \\ 
 $ E3L1Inv(a45) \land $ \\ 
 $  \Rnext C1(a25_a9) \land $ \\ 
 $  \Rnext  \Rnext C2(a23) \land $ \\ 
 $  \Rnext E2L2Inv(a78) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a2) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a82) \land $ \\ 
 $  \Rnext E3L0(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a57) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a8_a86) \land $ \\ 
 $  \Rnext E2L2Inv(a29) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a5_a69) \land $ \\ 
 $  \Rnext C1(a95) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a25_a9) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a32_a80_a70_a94) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a56_a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a78) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a17) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a51) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $  \Rnext  \Rnext C0(a40) \land $ \\ 
 $  \Rnext  \Rnext C3(a45) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a17) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a55) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a25_a9) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a99) \land $ \\ 
 $  \Rnext C0(a89) \land $ \\ 
 $  \Rnext C3(a21) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a95) \land $ \\ 
 $  \Rnext E2L2Inv(a95) \land $ \\ 
 $  \Rnext C3(a15) \land $ \\ 
 $  \Rnext  \Rnext C1(a82) \land $ \\ 
 $  \Rnext E2L2(a15) \land $ \\ 
 $  \Rnext C1(a32_a80_a70_a94) \land $ \\ 
 $  \Rnext C0(a29) \land $ \\ 
 $  \Rnext E2L2Inv(a55) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a99) \land $ \\ 
 $  \Rnext  \Rnext C0(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a56_a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a33_a36) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a29) \land $ \\ 
 $  \Rnext E3L1(a5_a69) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a58) \land $ \\ 
 $  \Rnext C0(a33_a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a79_a81) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a29) \land $ \\ 
 $  \Rnext C1(a77) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a77) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a73) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a33_a36) \land $ \\ 
 $  \Rnext C0(a21) \land $ \\ 
 $  \Rnext  \Rnext C0(a54_a67_a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a40) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a99) \land $ \\ 
 $  \Rnext E3L0(a33_a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a95) \land $ \\ 
 $  \Rnext C0(a14_a60_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a8_a86) \land $ \\ 
 $  \Rnext C2(a25_a9) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a40) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a33_a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a19) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a50) \land $ \\ 
 $  \Rnext E3L1Inv(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a14_a60_a63) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a29) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a56_a31) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a19) \land $ \\ 
 $  \Rnext E2L2Inv(a51) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a55) \land $ \\ 
 $  \Rnext E2L2Inv(a61) \land $ \\ 
 $  \Rnext E3L1Inv(a95) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a33_a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a54_a67_a72) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a78) \land $ \\ 
 $  \Rnext E3L1(a50) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a61) \land $ \\ 
 $  \Rnext C3(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $  \Rnext E3L1Inv(a87) \land $ \\ 
 $  \Rnext E3L0Inv(a79_a81) \land $ \\ 
 $  \Rnext E3L0(a14_a60_a63) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a78) \land $ \\ 
 $  \Rnext E3L0Inv(a51) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a37) \land $ \\ 
 $  \Rnext E3L0(a17) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a82) \land $ \\ 
 $  \Rnext E2L2Inv(a17) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a5_a69) \land $ \\ 
 $  \Rnext E3L1Inv(a2) \land $ \\ 
 $  \Rnext E3L0(a56_a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a51) \land $ \\ 
 $  \Rnext C2(a33_a36) \land $ \\ 
 $  \Rnext E2L2Inv(a25_a9) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a79_a81) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a23) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a61) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a95) \land $ \\ 
 $  \Rnext  \Rnext C2(a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a21) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a66_a7_a71) \land $ \\ 
 $  \Rnext C0(a12_a62) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a5_a69) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a35_a49_a97) \land $ \\ 
 $  \Rnext E2L2(a54_a67_a72) \land $ \\ 
 $  \Rnext  \Rnext C3(a61) \land $ \\ 
 $  \Rnext C1(a57) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a15) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a57) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a23) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a95) \land $ \\ 
 $  \Rnext E3L1(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a66_a7_a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a58) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a12_a62) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $  \Rnext  \Rnext C0(a35_a49_a97) \land $ \\ 
 $  \Rnext E2L2Inv(a19) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a55) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a40) \land $ \\ 
 $  \Rnext E3L1(a57) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a45) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a61) \land $ \\ 
 $  \Rnext  \Rnext C3(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a45) \land $ \\ 
 $  \Rnext C0(a8_a86) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a23) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a56_a31) \land $ \\ 
 $  \Rnext E2L2(a8_a86) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a61) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a19) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a17) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a79_a81) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a37) \land $ \\ 
 $  \Rnext E3L0(a21) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a100) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a2) \land $ \\ 
 $  \Rnext E3L1Inv(a14_a60_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a35_a49_a97) \land $ \\ 
 $  \Rnext E3L1(a89) \land $ \\ 
 $  \Rnext E2L2Inv(a79_a81) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a55) \land $ \\ 
 $  \Rnext E2L2(a19) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a57) \land $ \\ 
 $  \Rnext C1(a23) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a8_a86) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a89) \land $ \\ 
 $  \Rnext  \Rnext C1(a95) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a79_a81) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a25_a9) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a32_a80_a70_a94) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a50) \land $ \\ 
 $  \Rnext E2L2(a87) \land $ \\ 
 $  \Rnext C2(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $  \Rnext  \Rnext C1(a15) \land $ \\ 
 $  \Rnext  \Rnext C3(a23) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a33_a36) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a66_a7_a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a78) \land $ \\ 
 $  \Rnext  \Rnext C3(a89) \land $ \\ 
 $  \Rnext  \Rnext C3(a25_a9) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a51) \land $ \\ 
 $  \Rnext C1(a100) \land $ \\ 
 $  \Rnext  \Rnext C1(a77) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a21) \land $ \\ 
 $  \Rnext C3(a51) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a14_a60_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a14_a60_a63) \land $ \\ 
 $  \Rnext E3L0(a61) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a14_a60_a63) \land $ \\ 
 $  \Rnext E3L0(a25_a9) \land $ \\ 
 $  \Rnext C2(a82) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a87) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a54_a67_a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a87) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a35_a49_a97) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a35_a49_a97) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a58) \land $ \\ 
 $  \Rnext  \Rnext C0(a2) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a65) \land $ \\ 
 $  \Rnext E3L0Inv(a99) \land $ \\ 
 $  \Rnext  \Rnext C3(a8_a86) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a45) \land $ \\ 
 $  \Rnext E3L0(a40) \land $ \\ 
 $  \Rnext  \Rnext C3(a40) \land $ \\ 
 $  \Rnext C1(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a32_a80_a70_a94) \land $ \\ 
 $  \Rnext E3L0Inv(a55) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a33_a36) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a100) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a55) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a12_a62) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a55) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a5_a69) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a54_a67_a72) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext C1(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a40) \land $ \\ 
 $  \Rnext E3L0(a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a100) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a77) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a57) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a2) \land $ \\ 
 $  \Rnext  \Rnext C0(a19) \land $ \\ 
 $  \Rnext C2(a45) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a19) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a77) \land $ \\ 
 $  \Rnext  \Rnext C2(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a25_a9) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a23) \land $ \\ 
 $ E2G3(a29) \land $ \\ 
 $ E2G3(a51) \land $ \\ 
 $ E2G3(a57) \land $ \\ 
 $ E2G3(a17) \land $ \\ 
 $ E2G3(a50) \land $ \\ 
 $ E2G3(a76) \land $ \\ 
 $ E2G3(a35_a49_a97) \land $ \\ 
 $ E2G3(a2) \land $ \\ 
 $ E2G3(a65) \land $ \\ 
 $ E2G3(a61) \land $ \\ 
 $ E2G3(a8_a86) \land $ \\ 
 $ E2G3(a95) \land $ \\ 
 $ E2G3(a89) \land $ \\ 
 $ E2G3(a12_a62) \land $ \\ 
 $ E2G3(a77) \land $ \\ 
 $ E2G3(a58) \land $ \\ 
 $ E2G3(a87) \land $ \\ 
 $ E2G3(a79_a81) \land $ \\ 
 $ E2G3(a32_a80_a70_a94) \land $ \\ 
 $ E2G3(a19) \land $ \\ 
 $ E2G3(a45) \land $ \\ 
 $ E2G3(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $ E2G3(a25_a9) \land $ \\ 
 $ E2G3(a21) \land $ \\ 
 $ E2G3(a78) \land $ \\ 
 $ E2G3(a100) \land $ \\ 
 $ E2G3(a14_a60_a63) \land $ \\ 
 $ E2G3(a33_a36) \land $ \\ 
 $ E2G3(a66_a7_a71) \land $ \\ 
 $ E2G3(a82) \land $ \\ 
 $ E2G3(a54_a67_a72) \land $ \\ 
 $ E2G3(a55) \land $ \\ 
 $ E2G3(a5_a69) \land $ \\ 
 $ E2G3(a37) \land $ \\ 
 $ E2G3(a73) \land $ \\ 
 $ E2G3(a99) \land $ \\ 
 $ E2G3(a40) \land $ \\ 
 $ E2G3(a56_a31) \land $ \\ 
 $ E2G3(a23) \land $ \\ 
 $ E2G3(a15) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a95) \land $ \\ 
 $  \Rnext C1(a45) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a5_a69) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a19) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a50) \land $ \\ 
 $  \Rnext E2L2Inv(a99) \land $ \\ 
 $  \Rnext C1(a33_a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a57) \land $ \\ 
 $  \Rnext C2(a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a100) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a32_a80_a70_a94) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a37) \land $ \\ 
 $  \Rnext C1(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $  \Rnext C2(a50) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a82) \land $ \\ 
 $  \Rnext E3L1Inv(a56_a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a66_a7_a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a15) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a77) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a19) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a78) \land $ \\ 
 $  \Rnext  \Rnext C1(a54_a67_a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a76) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a29) \land $ \\ 
 $  \Rnext  \Rnext C3(a14_a60_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a45) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a19) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a55) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a21) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a35_a49_a97) \land $ \\ 
 $  \Rnext E2L2Inv(a15) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a61) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a17) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a5_a69) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a32_a80_a70_a94) \land $ \\ 
 $  \Rnext  \Rnext C0(a66_a7_a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a5_a69) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a29) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a99) \land $ \\ 
 $  \Rnext  \Rnext C3(a57) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a45) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a65) \land $ \\ 
 $  \Rnext E3L1(a25_a9) \land $ \\ 
 $  \Rnext  \Rnext C2(a33_a36) \land $ \\ 
 $  \Rnext C2(a77) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a8_a86) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a33_a36) \land $ \\ 
 $  \Rnext E3L1(a95) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $  \Rnext C3(a5_a69) \land $ \\ 
 $  \Rnext E3L0Inv(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a79_a81) \land $ \\ 
 $  \Rnext  \Rnext C1(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a61) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a54_a67_a72) \land $ \\ 
 $  \Rnext C2(a8_a86) \land $ \\ 
 $  \Rnext E3L0Inv(a66_a7_a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a76) \land $ \\ 
 $  \Rnext C1(a21) \land $ \\ 
 $  \Rnext  \Rnext C2(a32_a80_a70_a94) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a29) \land $ \\ 
 $  \Rnext E3L0(a5_a69) \land $ \\ 
 $  \Rnext C3(a77) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a15) \land $ \\ 
 $  \Rnext C3(a65) \land $ \\ 
 $  \Rnext C0(a55) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a14_a60_a63) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a19) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a51) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a40) \land $ \\ 
 $  \Rnext  \Rnext C0(a33_a36) \land $ \\ 
 $  \Rnext E3L1Inv(a32_a80_a70_a94) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a51) \land $ \\ 
 $  \Rnext  \Rnext C1(a32_a80_a70_a94) \land $ \\ 
 $  \Rnext  \Rnext C1(a29) \land $ \\ 
 $  \Rnext E3L0Inv(a78) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a17) \land $ \\ 
 $  \Rnext  \Rnext C2(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a17) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a55) \land $ \\ 
 $  \Rnext E3L1Inv(a35_a49_a97) \land $ \\ 
 $  \Rnext  \Rnext C3(a51) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a73) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a100) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a33_a36) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a14_a60_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a23) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a56_a31) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a82) \land $ \\ 
 $  \Rnext E2L2Inv(a8_a86) \land $ \\ 
 $  \Rnext E3L0(a95) \land $ \\ 
 $  \Rnext E3L0Inv(a17) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a21) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a50) \land $ \\ 
 $  \Rnext E2L2Inv(a65) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a100) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a77) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a21) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a55) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a66_a7_a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a61) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a89) \land $ \\ 
 $  \Rnext E3L1(a76) \land $ \\ 
 $  \Rnext C3(a57) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a33_a36) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a2) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a32_a80_a70_a94) \land $ \\ 
 $  \Rnext  \Rnext C3(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a100) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a23) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a21) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a78) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a89) \land $ \\ 
 $  \Rnext C0(a23) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a33_a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a66_a7_a71) \land $ \\ 
 $  \Rnext E3L0(a35_a49_a97) \land $ \\ 
 $  \Rnext E2L2(a23) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a23) \land $ \\ 
 $  \Rnext  \Rnext C2(a89) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a78) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a54_a67_a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a87) \land $ \\ 
 $  \Rnext E3L0(a19) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a89) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a54_a67_a72) \land $ \\ 
 $ E1G0Inv(a33_a36) \land $ \\ 
 $ E1G0Inv(a45) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a14_a60_a63) \land $ \\ 
 $ E1G0Inv(a17) \land $ \\ 
 $ E1G0Inv(a19) \land $ \\ 
 $ E1G0Inv(a65) \land $ \\ 
 $ E1G0Inv(a95) \land $ \\ 
 $ E1G0Inv(a25_a9) \land $ \\ 
 $ E1G0Inv(a51) \land $ \\ 
 $ E1G0Inv(a21) \land $ \\ 
 $ E1G0Inv(a66_a7_a71) \land $ \\ 
 $ E1G0Inv(a15) \land $ \\ 
 $ E1G0Inv(a61) \land $ \\ 
 $ E1G0Inv(a37) \land $ \\ 
 $ E1G0Inv(a5_a69) \land $ \\ 
 $ E1G0Inv(a14_a60_a63) \land $ \\ 
 $ E1G0Inv(a89) \land $ \\ 
 $ E1G0Inv(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $ E1G0Inv(a77) \land $ \\ 
 $ E1G0Inv(a73) \land $ \\ 
 $ E1G0Inv(a58) \land $ \\ 
 $ E1G0Inv(a76) \land $ \\ 
 $ E1G0Inv(a99) \land $ \\ 
 $ E1G0Inv(a55) \land $ \\ 
 $ E1G0Inv(a82) \land $ \\ 
 $ E1G0Inv(a29) \land $ \\ 
 $ E1G0Inv(a56_a31) \land $ \\ 
 $ E1G0Inv(a35_a49_a97) \land $ \\ 
 $ E1G0Inv(a12_a62) \land $ \\ 
 $ E1G0Inv(a57) \land $ \\ 
 $ E1G0Inv(a87) \land $ \\ 
 $ E1G0Inv(a23) \land $ \\ 
 $ E1G0Inv(a2) \land $ \\ 
 $ E1G0Inv(a78) \land $ \\ 
 $ E1G0Inv(a100) \land $ \\ 
 $ E1G0Inv(a79_a81) \land $ \\ 
 $ E1G0Inv(a32_a80_a70_a94) \land $ \\ 
 $ E1G0Inv(a40) \land $ \\ 
 $ E1G0Inv(a8_a86) \land $ \\ 
 $ E1G0Inv(a54_a67_a72) \land $ \\ 
 $ E1G0Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a77) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a25_a9) \land $ \\ 
 $  \Rnext E3L1(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $  \Rnext E3L1Inv(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a14_a60_a63) \land $ \\ 
 $  \Rnext E2L2Inv(a56_a31) \land $ \\ 
 $  \Rnext E3L1Inv(a77) \land $ \\ 
 $  \Rnext E2L2(a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a78) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a100) \land $ \\ 
 $  \Rnext E2L2(a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a23) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a54_a67_a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a66_a7_a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a79_a81) \land $ \\ 
 $  \Rnext E2L2(a14_a60_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a12_a62) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a95) \land $ \\ 
 $  \Rnext C1(a89) \land $ \\ 
 $  \Rnext  \Rnext C0(a12_a62) \land $ \\ 
 $ C0(a50) \land $ \\ 
 $ C0(a32_a80_a70_a94) \land $ \\ 
 $ C0(a29) \land $ \\ 
 $ C0(a33_a36) \land $ \\ 
 $ C0(a19) \land $ \\ 
 $ C0(a51) \land $ \\ 
 $ C0(a37) \land $ \\ 
 $ C0(a65) \land $ \\ 
 $ C0(a57) \land $ \\ 
 $ C0(a45) \land $ \\ 
 $ C0(a8_a86) \land $ \\ 
 $ C0(a89) \land $ \\ 
 $ C0(a25_a9) \land $ \\ 
 $ C0(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $ C0(a95) \land $ \\ 
 $ C0(a77) \land $ \\ 
 $ C0(a17) \land $ \\ 
 $ C0(a35_a49_a97) \land $ \\ 
 $ C0(a82) \land $ \\ 
 $ C0(a21) \land $ \\ 
 $ C0(a58) \land $ \\ 
 $ C0(a5_a69) \land $ \\ 
 $ C0(a14_a60_a63) \land $ \\ 
 $ C0(a15) \land $ \\ 
 $ C0(a99) \land $ \\ 
 $ C0(a100) \land $ \\ 
 $ C0(a54_a67_a72) \land $ \\ 
 $ C0(a79_a81) \land $ \\ 
 $ C0(a2) \land $ \\ 
 $ C0(a73) \land $ \\ 
 $ C0(a66_a7_a71) \land $ \\ 
 $ C0(a55) \land $ \\ 
 $ C0(a56_a31) \land $ \\ 
 $ C0(a87) \land $ \\ 
 $ C0(a78) \land $ \\ 
 $ C0(a40) \land $ \\ 
 $  \Rnext C1(a78) \land $ \\ 
 $  \Rnext E3L0Inv(a56_a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a12_a62) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a2) \land $ \\ 
 $  \Rnext  \Rnext E2L2Inv(a25_a9) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a77) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a51) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a17) \land $ \\ 
 $  \Rnext E3L1(a33_a36) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a14_a60_a63) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a55) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a82) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a17) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a57) \land $ \\ 
 $  \Rnext C1(a5_a69) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a77) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a77) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a76) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a82) \land $ \\ 
 $  \Rnext E2L2Inv(a12_a62) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a78) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a14_a60_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a21) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a55) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a79_a81) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a61) \land $ \\ 
 $  \Rnext C1(a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a58) \land $ \\ 
 $  \Rnext E2L2Inv(a37) \land $ \\ 
 $  \Rnext C3(a73) \land $ \\ 
 $  \Rnext C2(a51) \land $ \\ 
 $  \Rnext C3(a54_a67_a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a12_a62) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a73) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a45) \land $ \\ 
 $  \Rnext  \Rnext E2L2(a57) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a76) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a55) \land $ \\ 
 $  \Rnext C1(a8_a86) \land $ \\ 
 $ E3L0(a32_a80_a70_a94) \land $ \\ 
 $ E3L0(a15) \land $ \\ 
 $ E3L0(a51) \land $ \\ 
 $ E3L0(a8_a86) \land $ \\ 
 $ E3L0(a14_a60_a63) \land $ \\ 
 $ E3L0(a77) \land $ \\ 
 $ E3L0(a78) \land $ \\ 
 $ E3L0(a95) \land $ \\ 
 $ E3L0(a82) \land $ \\ 
 $ E3L0(a61) \land $ \\ 
 $ E3L0(a37) \land $ \\ 
 $ E3L0(a54_a67_a72) \land $ \\ 
 $ E3L0(a100) \land $ \\ 
 $ E3L0(a17) \land $ \\ 
 $ E3L0(a40) \land $ \\ 
 $ E3L0(a89) \land $ \\ 
 $ E3L0(a33_a36) \land $ \\ 
 $ E3L0(a21) \land $ \\ 
 $ E3L0(a19) \land $ \\ 
 $ E3L0(a23) \land $ \\ 
 $ E3L0(a65) \land $ \\ 
 $ E3L0(a35_a49_a97) \land $ \\ 
 $ E3L0(a45) \land $ \\ 
 $ E3L0(a57) \land $ \\ 
 $ E3L0(a99) \land $ \\ 
 $ E3L0(a58) \land $ \\ 
 $ E3L0(a73) \land $ \\ 
 $ E3L0(a87) \land $ \\ 
 $ E3L0(a2) \land $ \\ 
 $ E3L0(a76) \land $ \\ 
 $ E3L0(a50) \land $ \\ 
 $ E3L0(a25_a9) \land $ \\ 
 $ E3L0(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $ E3L0(a79_a81) \land $ \\ 
 $ E3L0(a29) \land $ \\ 
 $ E3L0(a55) \land $ \\ 
 $ E3L0(a66_a7_a71) \land $ \\ 
 $ E3L0(a56_a31) \land $ \\ 
 $ E3L0(a12_a62) \land $ \\ 
 $ E3L0(a5_a69) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a37) \land $ \\ 
 $  \Rnext E3L1Inv(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a76) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a77) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a8_a86) \land $ \\ 
 $ E2L2(a57) \land $ \\ 
 $ E2L2(a21) \land $ \\ 
 $ E2L2(a2) \land $ \\ 
 $ E2L2(a99) \land $ \\ 
 $ E2L2(a61) \land $ \\ 
 $ E2L2(a87) \land $ \\ 
 $ E2L2(a65) \land $ \\ 
 $ E2L2(a54_a67_a72) \land $ \\ 
 $ E2L2(a35_a49_a97) \land $ \\ 
 $ E2L2(a8_a86) \land $ \\ 
 $ E2L2(a45) \land $ \\ 
 $ E2L2(a51) \land $ \\ 
 $ E2L2(a50) \land $ \\ 
 $ E2L2(a89) \land $ \\ 
 $ E2L2(a78) \land $ \\ 
 $ E2L2(a17) \land $ \\ 
 $ E2L2(a12_a62) \land $ \\ 
 $ E2L2(a33_a36) \land $ \\ 
 $ E2L2(a25_a9) \land $ \\ 
 $ E2L2(a14_a60_a63) \land $ \\ 
 $ E2L2(a29) \land $ \\ 
 $ E2L2(a79_a81) \land $ \\ 
 $ E2L2(a37) \land $ \\ 
 $ E2L2(a82) \land $ \\ 
 $ E2L2(a66_a7_a71) \land $ \\ 
 $ E2L2(a5_a69) \land $ \\ 
 $ E2L2(a56_a31) \land $ \\ 
 $ E2L2(a58) \land $ \\ 
 $ E2L2(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $ E2L2(a40) \land $ \\ 
 $ E2L2(a23) \land $ \\ 
 $ E2L2(a77) \land $ \\ 
 $ E2L2(a76) \land $ \\ 
 $ E2L2(a55) \land $ \\ 
 $ E2L2(a15) \land $ \\ 
 $ E2L2(a32_a80_a70_a94) \land $ \\ 
 $ E2L2(a100) \land $ \\ 
 $ E2L2(a19) \land $ \\ 
 $ E2L2(a73) \land $ \\ 
 $ E2L2(a95) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a76) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a45) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a40) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a40) \land $ \\ 
 $  \Rnext E3L0(a57) \land $ \\ 
 $  \Rnext  \Rnext C0(a14_a60_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a61) \land $ \\ 
 $  \Rnext  \Rnext C1(a50) \land $ \\ 
 $  \Rnext E2L2(a76) \land $ \\ 
 $  \Rnext E3L1(a2) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a87) \land $ \\ 
 $  \Rnext C3(a23) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a17) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a32_a80_a70_a94) \land $ \\ 
 $  \Rnext  \Rnext C3(a100) \land $ \\ 
 $  \Rnext E3L0(a32_a80_a70_a94) \land $ \\ 
 $  \Rnext E3L0Inv(a45) \land $ \\ 
 $  \Rnext E3L0Inv(a12_a62) \land $ \\ 
 $  \Rnext  \Rnext C1(a33_a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a79_a81) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a8_a86) \land $ \\ 
 $  \Rnext  \Rnext C2(a37) \land $ \\ 
 $  \Rnext E3L0(a66_a7_a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a76) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a2) \land $ \\ 
 $  \Rnext  \Rnext C1(a58) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a45) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a82) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a57) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a12_a62) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a54_a67_a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a15) \land $ \\ 
 $  \Rnext E3L1Inv(a25_a9) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a77) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a2) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a12_a62) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a45) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a5_a69) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a51) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a57) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a14_a60_a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L2(a17) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a55) \land $ \\ 
 $  \Rnext C0(a11_a98_a10_a13_a34_a59_a39_a16_a38_a18_a84_a83_a20_a42_a64_a85_a41_a88_a22_a44_a43_a24_a46_a68_a26_a48_a47_a28_a27_a1_a3_a4_a6_a91_a90_a93_a92_a53_a75_a96_a30_a52_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a54_a67_a72) \land $ \\ 
 $  \Rnext E3L0(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L2Inv(a99) \land $ \\ 
 $  \Rnext  \Rnext C1(a8_a86) \land $ \\ 
 $  \Rnext E2L2(a65) \land $ \\ 
 $  \Rnext E3L1Inv(a51) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a77) \land $ \\ 
 $  \Rnext C0(a100))$ 
\end{document}