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


$((PinvL5 \rightarrow E1L5(dL5)) \land $ \\ 
 $ (PinvL4 \rightarrow E1L4(dL4)) \land $ \\ 
 $ (PG0 \rightarrow E1G0Inv(dG0Inv)) \land $ \\ 
 $ (PinvL0 \rightarrow E1L0(dL0)) \land $ \\ 
 $ (PinvL2 \rightarrow E1L2(dL2)) \land $ \\ 
 $ (PG2 \rightarrow E1G2Inv(dG2Inv)) \land $ \\ 
 $ (PinvG1 \rightarrow E1G1(dG1)) \land $ \\ 
 $ (PL0 \rightarrow E1L0Inv(dL0Inv)) \land $ \\ 
 $ (PL2 \rightarrow E1L2Inv(dL2Inv)) \land $ \\ 
 $ (PL4 \rightarrow E1L4Inv(dL4Inv)) \land $ \\ 
 $  \forall X. ( \Rbox ((( \Rbox C1(X) \land $ \\ 
 $  \Rdiamond C5(X)) \rightarrow  \Rdiamond  \Rbox (E2G4(X) \land $ \\ 
 $ C1(X))) \land $ \\ 
 $ (( \Rbox C2(X) \land $ \\ 
 $  \Rbox E3L0(X)) \rightarrow (E2G1(X) \land $ \\ 
 $ E1L4(X) \land $ \\ 
 $ C1(X))) \land $ \\ 
 $ ( \Rbox  \Rbox  \Rdiamond  \Rdiamond C5(X) \rightarrow ( \Rdiamond C3(X) \land $ \\ 
 $  \Rnext E3L2(X))) \land $ \\ 
 $ ((C2(X) \land $ \\ 
 $  \Rdiamond  \Rnext C5(X)) \rightarrow (E1L2(X) \land $ \\ 
 $ C4(X) \land $ \\ 
 $ C3(X))) \land $ \\ 
 $ ( \Rbox  \Rbox  \Rdiamond  \Rbox E1L1(X) \rightarrow  \Rdiamond  \Rbox  \Rbox  \Rdiamond C4(X)) \land $ \\ 
 $ ((C3(X) \land $ \\ 
 $ E3G1(X) \land $ \\ 
 $ E2L4(X)) \rightarrow ( \Rdiamond C2(X) \land $ \\ 
 $  \Rnext C3(X))) \land $ \\ 
 $ ((E1L5(X) \land $ \\ 
 $ C0(X) \land $ \\ 
 $ C4(X)) \rightarrow ( \Rnext C4(X) \land $ \\ 
 $  \Rnext E1G1(X))) \land $ \\ 
 $ ( \Rbox (C0(X) \land $ \\ 
 $  \Rnext E2L5(X)) \rightarrow  \Rdiamond (E2L5(X) \land $ \\ 
 $  \Rdiamond E1G1(X))) \land $ \\ 
 $ ( \Rbox  \Rbox (C5(X) \land $ \\ 
 $ C0(X)) \rightarrow  \Rbox  \Rbox (E3G2(X) \land $ \\ 
 $ C2(X))) \land $ \\ 
 $ ( \Rbox  \Rbox  \Rbox  \Rnext C3(X) \rightarrow  \Rdiamond (E3L2(X) \land $ \\ 
 $  \Rnext E1G2(X))) \land $ \\ 
 $ ( \Rbox  \Rbox (E2L1(X) \land $ \\ 
 $ C3(X)) \rightarrow ( \Rdiamond E1G5(X) \land $ \\ 
 $  \Rnext C1(X))) \land $ \\ 
 $ (( \Rdiamond E3L1(X) \land $ \\ 
 $  \Rdiamond C2(X)) \rightarrow (E2G4(X) \land $ \\ 
 $ E2L4(X) \land $ \\ 
 $ E1G2(X))) \land $ \\ 
 $ ( \Rbox  \Rdiamond  \Rdiamond  \Rdiamond E3G2(X) \rightarrow (C2(X) \land $ \\ 
 $  \Rbox  \Rdiamond C0(X))) \land $ \\ 
 $ ( \Rbox (C0(X) \land $ \\ 
 $  \Rbox E3G2(X)) \rightarrow (E2G3(X) \land $ \\ 
 $ E1L4(X) \land $ \\ 
 $ E3G1(X))) \land $ \\ 
 $ (( \Rdiamond C4(X) \land $ \\ 
 $  \Rnext C4(X)) \rightarrow (E1L3(X) \land $ \\ 
 $ E2L1(X) \land $ \\ 
 $ C5(X))) \land $ \\ 
 $ ((E2G0(X) \land $ \\ 
 $  \Rbox  \Rbox C4(X)) \rightarrow  \Rbox (C5(X) \land $ \\ 
 $  \Rbox C1(X))) \land $ \\ 
 $ (( \Rbox E3L2(X) \land $ \\ 
 $  \Rnext E1G5(X)) \rightarrow ( \Rnext E2G2(X) \land $ \\ 
 $  \Rbox E2L3(X))) \land $ \\ 
 $ (( \Rdiamond E1L5(X) \land $ \\ 
 $  \Rbox E2L4(X)) \rightarrow  \Rdiamond (C5(X) \land $ \\ 
 $  \Rdiamond C1(X))) \land $ \\ 
 $ ( \Rbox (E1G0(X) \land $ \\ 
 $  \Rnext C0(X)) \rightarrow ( \Rdiamond C5(X) \land $ \\ 
 $  \Rbox E1L4(X))) \land $ \\ 
 $ ( \Rdiamond (C0(X) \land $ \\ 
 $  \Rnext E2G4(X)) \rightarrow  \Rbox  \Rdiamond  \Rbox  \Rbox E2G5(X)) \land $ \\ 
 $ (E3L0(X) \rightarrow E1L0(X)) \land $ \\ 
 $ (E2G2(X) \rightarrow E1G2(X)) \land $ \\ 
 $ (E3G1(X) \rightarrow E2G1(X)) \land $ \\ 
 $ (E3G2(X) \rightarrow E2G2(X)) \land $ \\ 
 $ (E3L1(X) \rightarrow E2L1(X)) \land $ \\ 
 $ (E2G1(X) \rightarrow E1G1(X)) \land $ \\ 
 $ (E2L4(X) \rightarrow E1L4(X)) \land $ \\ 
 $ (E2G0(X) \rightarrow E1G0(X)) \land $ \\ 
 $ (E2L3(X) \rightarrow E1L3(X)) \land $ \\ 
 $ (E2L1(X) \rightarrow E1L1(X)) \land $ \\ 
 $ (E2G3(X) \rightarrow E1G3(X)) \land $ \\ 
 $ (E2G4(X) \rightarrow E1G4(X)) \land $ \\ 
 $ (E3L2(X) \rightarrow E1L2(X)) \land $ \\ 
 $ (E2G5(X) \rightarrow E1G5(X)) \land $ \\ 
 $ (E2L5(X) \rightarrow E1L5(X))) \land $ \\ 
 $ ( \Rdiamond E1L0Inv(X) \rightarrow  \Rbox PinvL0) \land $ \\ 
 $ ( \Rdiamond E3G2(X) \rightarrow  \Rbox E3G2(X)) \land $ \\ 
 $ ( \Rdiamond E1G1(X) \rightarrow  \Rbox E1G1(X)) \land $ \\ 
 $ ( \Rdiamond E1G0Inv(X) \rightarrow  \Rbox PinvG0) \land $ \\ 
 $ ( \Rdiamond E1G2Inv(X) \rightarrow  \Rbox E1G2Inv(X)) \land $ \\ 
 $ ( \Rdiamond E2G3(X) \rightarrow  \Rbox E2G3(X)) \land $ \\ 
 $ ( \Rdiamond E1L1(X) \rightarrow  \Rbox PL1) \land $ \\ 
 $ ( \Rdiamond E1G3Inv(X) \rightarrow  \Rbox PinvG3) \land $ \\ 
 $ ( \Rdiamond E1G4(X) \rightarrow  \Rbox E1G4(X)) \land $ \\ 
 $ ( \Rdiamond E1G4(X) \rightarrow  \Rbox PG4) \land $ \\ 
 $ ( \Rdiamond E1L4(X) \rightarrow  \Rbox PL4) \land $ \\ 
 $ ( \Rdiamond E2G0(X) \rightarrow  \Rbox E2G0(X)) \land $ \\ 
 $ ( \Rdiamond E1L2(X) \rightarrow  \Rbox PL2) \land $ \\ 
 $ ( \Rdiamond E1L3(X) \rightarrow  \Rbox PL3) \land $ \\ 
 $ ( \Rdiamond E1G3(X) \rightarrow  \Rbox PG3) \land $ \\ 
 $ ( \Rdiamond E1G5Inv(X) \rightarrow  \Rbox E1G5Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1L3Inv(X) \rightarrow  \Rbox PinvL3) \land $ \\ 
 $ ( \Rdiamond E1G0(X) \rightarrow  \Rbox PG0) \land $ \\ 
 $ ( \Rdiamond E1G5Inv(X) \rightarrow  \Rbox PinvG5) \land $ \\ 
 $ ( \Rdiamond E1G0Inv(X) \rightarrow  \Rbox E1G0Inv(X)) \land $ \\ 
 $ ( \Rdiamond E2G5(X) \rightarrow  \Rbox E2G5(X)) \land $ \\ 
 $ ( \Rdiamond E1G5(X) \rightarrow  \Rbox PG5) \land $ \\ 
 $ ( \Rdiamond E1L5(X) \rightarrow  \Rbox PL5) \land $ \\ 
 $ ( \Rdiamond E1G2(X) \rightarrow  \Rbox E1G2(X)) \land $ \\ 
 $ ( \Rdiamond E1L0(X) \rightarrow  \Rbox PL0) \land $ \\ 
 $ ( \Rdiamond E1G5(X) \rightarrow  \Rbox E1G5(X)) \land $ \\ 
 $ ( \Rdiamond E1L4Inv(X) \rightarrow  \Rbox PinvL4) \land $ \\ 
 $ ( \Rdiamond E1G4Inv(X) \rightarrow  \Rbox PinvG4) \land $ \\ 
 $ ( \Rdiamond E3G1(X) \rightarrow  \Rbox E3G1(X)) \land $ \\ 
 $ ( \Rdiamond E1G4Inv(X) \rightarrow  \Rbox E1G4Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1G3(X) \rightarrow  \Rbox E1G3(X)) \land $ \\ 
 $ ( \Rdiamond E1G0(X) \rightarrow  \Rbox E1G0(X)) \land $ \\ 
 $ ( \Rdiamond E1L5Inv(X) \rightarrow  \Rbox PinvL5) \land $ \\ 
 $ ( \Rdiamond E1G3Inv(X) \rightarrow  \Rbox E1G3Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1G1(X) \rightarrow  \Rbox PG1) \land $ \\ 
 $ ( \Rdiamond E2G2(X) \rightarrow  \Rbox E2G2(X)) \land $ \\ 
 $ ( \Rdiamond E1G2(X) \rightarrow  \Rbox PG2) \land $ \\ 
 $ ( \Rdiamond E1G2Inv(X) \rightarrow  \Rbox PinvG2) \land $ \\ 
 $ ( \Rdiamond E1G1Inv(X) \rightarrow  \Rbox E1G1Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1G1Inv(X) \rightarrow  \Rbox PinvG1) \land $ \\ 
 $ ( \Rdiamond E2G4(X) \rightarrow  \Rbox E2G4(X)) \land $ \\ 
 $ ( \Rdiamond E1L2Inv(X) \rightarrow  \Rbox PinvL2) \land $ \\ 
 $ ( \Rdiamond E2G1(X) \rightarrow  \Rbox E2G1(X)) \land $ \\ 
 $ ( \Rdiamond E1L1Inv(X) \rightarrow  \Rbox PinvL1)) \land $ \\ 
 $ (PinvL1 \rightarrow E1L1(dL1)) \land $ \\ 
 $ (PL3 \rightarrow E1L3Inv(dL3Inv)) \land $ \\ 
 $ (PinvG5 \rightarrow E1G5(dG5)) \land $ \\ 
 $ (PinvL3 \rightarrow E1L3(dL3)) \land $ \\ 
 $ (PG4 \rightarrow E1G4Inv(dG4Inv)) \land $ \\ 
 $ (PinvG2 \rightarrow E1G2(dG2)) \land $ \\ 
 $ (PG1 \rightarrow E1G1Inv(dG1Inv)) \land $ \\ 
 $ (PinvG0 \rightarrow E1G0(dG0)) \land $ \\ 
 $ (PG5 \rightarrow E1G5Inv(dG5Inv)) \land $ \\ 
 $ (PinvG4 \rightarrow E1G4(dG4)) \land $ \\ 
 $ (PL1 \rightarrow E1L1Inv(dL1Inv)) \land $ \\ 
 $ (PG3 \rightarrow E1G3Inv(dG3Inv)) \land $ \\ 
 $ (PinvG3 \rightarrow E1G3(dG3)) \land $ \\ 
 $ (PL5 \rightarrow E1L5Inv(dL5Inv)) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4Inv(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2Inv(a91) \land $ \\ 
 $  \Rnext  \Rnext E3L2(a50) \land $ \\ 
 $  \Rnext  \Rnext E2L4(a38) \land $ \\ 
 $  \Rnext  \Rnext E2L3Inv(a89_a29) \land $ \\ 
 $  \Rnext E2L5(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a7) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a63) \land $ \\ 
 $  \Rnext  \Rnext C4(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2Inv(a41) \land $ \\ 
 $  \Rnext  \Rnext C5(a91) \land $ \\ 
 $  \Rnext C1(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a3) \land $ \\ 
 $  \Rnext E2L5(a87) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a60) \land $ \\ 
 $  \Rnext C1(a37) \land $ \\ 
 $  \Rnext  \Rnext E3L2Inv(a40) \land $ \\ 
 $  \Rnext E2L5Inv(a10) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C4(a98) \land $ \\ 
 $  \Rnext  \Rnext E2L4(a60) \land $ \\ 
 $  \Rnext C0(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3Inv(a7) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a41) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a37) \land $ \\ 
 $  \Rnext E3L2(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a40) \land $ \\ 
 $  \Rnext  \Rnext E2L3(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C5(a91) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3Inv(a98) \land $ \\ 
 $  \Rnext E3L0(a31) \land $ \\ 
 $  \Rnext C4(a98) \land $ \\ 
 $  \Rnext E2L4(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a89_a29) \land $ \\ 
 $  \Rnext C2(a91) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a14) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a71) \land $ \\ 
 $  \Rnext C0(a7) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5(a91) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a40) \land $ \\ 
 $  \Rnext E3L2(a7) \land $ \\ 
 $  \Rnext C5(a14) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3Inv(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a98) \land $ \\ 
 $  \Rnext  \Rnext C5(a86_a85) \land $ \\ 
 $  \Rnext C1(a86_a85) \land $ \\ 
 $  \Rnext E3L1(a14) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a50) \land $ \\ 
 $  \Rnext E2L4Inv(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2Inv(a3) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3Inv(a3) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a90) \land $ \\ 
 $  \Rnext  \Rnext E2L5Inv(a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext C1(a11) \land $ \\ 
 $  \Rnext  \Rnext E2L4Inv(a53_a30) \land $ \\ 
 $  \Rnext E2L3(a3) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a3) \land $ \\ 
 $  \Rnext  \Rnext E2L3(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a90) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a37) \land $ \\ 
 $  \Rnext E2L3(a91) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2(a10) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5(a82) \land $ \\ 
 $  \Rnext E3L1(a89_a29) \land $ \\ 
 $  \Rnext E3L1Inv(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a41) \land $ \\ 
 $  \Rnext C5(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4(a3) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a11) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext C3(a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a63) \land $ \\ 
 $  \Rnext  \Rnext E2L4Inv(a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a31) \land $ \\ 
 $  \Rnext  \Rnext C4(a7) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5Inv(a31) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a10) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a87) \land $ \\ 
 $  \Rnext C1(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2Inv(a89_a29) \land $ \\ 
 $ E1G1Inv(a89_a29) \land $ \\ 
 $ E1G1Inv(a53_a30) \land $ \\ 
 $ E1G1Inv(a41) \land $ \\ 
 $ E1G1Inv(a86_a85) \land $ \\ 
 $ E1G1Inv(a14) \land $ \\ 
 $ E1G1Inv(a31) \land $ \\ 
 $ E1G1Inv(a98) \land $ \\ 
 $ E1G1Inv(a7) \land $ \\ 
 $ E1G1Inv(a38) \land $ \\ 
 $ E1G1Inv(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $ E1G1Inv(a3) \land $ \\ 
 $ E1G1Inv(a91) \land $ \\ 
 $ E1G1Inv(a87) \land $ \\ 
 $ E1G1Inv(a40) \land $ \\ 
 $ E1G1Inv(a50) \land $ \\ 
 $ E1G1Inv(a82) \land $ \\ 
 $ E1G1Inv(a60) \land $ \\ 
 $ E1G1Inv(a71) \land $ \\ 
 $ E1G1Inv(a37) \land $ \\ 
 $ E1G1Inv(a11) \land $ \\ 
 $ E1G1Inv(a63) \land $ \\ 
 $ E1G1Inv(a90) \land $ \\ 
 $ E1G1Inv(a10) \land $ \\ 
 $  \Rnext E3L0Inv(a87) \land $ \\ 
 $  \Rnext  \Rnext C4(a37) \land $ \\ 
 $  \Rnext E2L5Inv(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5Inv(a14) \land $ \\ 
 $  \Rnext  \Rnext E2L4(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext C3(a10) \land $ \\ 
 $  \Rnext  \Rnext E2L3Inv(a41) \land $ \\ 
 $  \Rnext E3L0(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5Inv(a91) \land $ \\ 
 $  \Rnext E2L5(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a50) \land $ \\ 
 $  \Rnext E3L0(a3) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C4(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C5(a40) \land $ \\ 
 $  \Rnext E3L0(a7) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4Inv(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext E3L1(a41) \land $ \\ 
 $  \Rnext  \Rnext E3L2Inv(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5Inv(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C4(a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext E2L4(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext C4(a14) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a91) \land $ \\ 
 $  \Rnext  \Rnext C5(a41) \land $ \\ 
 $  \Rnext  \Rnext E2L3(a41) \land $ \\ 
 $  \Rnext  \Rnext C4(a91) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4(a7) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a31) \land $ \\ 
 $  \Rnext  \Rnext E2L5Inv(a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a71) \land $ \\ 
 $  \Rnext C2(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a3) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3(a7) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a50) \land $ \\ 
 $  \Rnext  \Rnext C4(a50) \land $ \\ 
 $  \Rnext E2L5Inv(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C5(a37) \land $ \\ 
 $  \Rnext E2L5Inv(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a71) \land $ \\ 
 $  \Rnext  \Rnext E2L4Inv(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a7) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a37) \land $ \\ 
 $  \Rnext C3(a63) \land $ \\ 
 $ E3L2Inv(a53_a30) \land $ \\ 
 $ E3L2Inv(a41) \land $ \\ 
 $ E3L2Inv(a89_a29) \land $ \\ 
 $ E3L2Inv(a98) \land $ \\ 
 $ E3L2Inv(a40) \land $ \\ 
 $ E3L2Inv(a14) \land $ \\ 
 $ E3L2Inv(a11) \land $ \\ 
 $ E3L2Inv(a50) \land $ \\ 
 $ E3L2Inv(a91) \land $ \\ 
 $ E3L2Inv(a7) \land $ \\ 
 $ E3L2Inv(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $ E3L2Inv(a86_a85) \land $ \\ 
 $ E3L2Inv(a82) \land $ \\ 
 $ E3L2Inv(a60) \land $ \\ 
 $ E3L2Inv(a87) \land $ \\ 
 $ E3L2Inv(a90) \land $ \\ 
 $ E3L2Inv(a37) \land $ \\ 
 $ E3L2Inv(a38) \land $ \\ 
 $ E3L2Inv(a10) \land $ \\ 
 $ E3L2Inv(a3) \land $ \\ 
 $ E3L2Inv(a71) \land $ \\ 
 $ E3L2Inv(a63) \land $ \\ 
 $ E3L2Inv(a31) \land $ \\ 
 $  \Rnext C2(a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3Inv(a90) \land $ \\ 
 $  \Rnext C0(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext E2L5(a50) \land $ \\ 
 $  \Rnext E2L4(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4(a10) \land $ \\ 
 $  \Rnext E3L2(a38) \land $ \\ 
 $  \Rnext  \Rnext E2L4(a11) \land $ \\ 
 $  \Rnext E3L0(a10) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a98) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a91) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a31) \land $ \\ 
 $  \Rnext  \Rnext E2L4Inv(a7) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C4(a90) \land $ \\ 
 $  \Rnext E3L2Inv(a90) \land $ \\ 
 $  \Rnext C0(a3) \land $ \\ 
 $  \Rnext  \Rnext E3L2(a60) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a10) \land $ \\ 
 $  \Rnext  \Rnext C1(a7) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3(a91) \land $ \\ 
 $  \Rnext E2L3(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C4(a10) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3(a87) \land $ \\ 
 $  \Rnext  \Rnext E2L5(a91) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a37) \land $ \\ 
 $  \Rnext  \Rnext C0(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4(a71) \land $ \\ 
 $  \Rnext E3L0Inv(a82) \land $ \\ 
 $  \Rnext E2L4(a60) \land $ \\ 
 $  \Rnext E2L5(a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2Inv(a11) \land $ \\ 
 $  \Rnext C0(a37) \land $ \\ 
 $  \Rnext  \Rnext E2L5Inv(a14) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3(a53_a30) \land $ \\ 
 $  \Rnext E2L3Inv(a7) \land $ \\ 
 $ C5(a86_a85) \land $ \\ 
 $ C5(a87) \land $ \\ 
 $ C5(a89_a29) \land $ \\ 
 $ C5(a37) \land $ \\ 
 $ C5(a63) \land $ \\ 
 $ C5(a98) \land $ \\ 
 $ C5(a38) \land $ \\ 
 $ C5(a3) \land $ \\ 
 $ C5(a11) \land $ \\ 
 $ C5(a71) \land $ \\ 
 $ C5(a41) \land $ \\ 
 $ C5(a40) \land $ \\ 
 $ C5(a10) \land $ \\ 
 $ C5(a91) \land $ \\ 
 $ C5(a53_a30) \land $ \\ 
 $ C5(a60) \land $ \\ 
 $ C5(a7) \land $ \\ 
 $ C5(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $ C5(a82) \land $ \\ 
 $ C5(a31) \land $ \\ 
 $ C5(a14) \land $ \\ 
 $ C5(a50) \land $ \\ 
 $ C5(a90) \land $ \\ 
 $  \Rnext E2L3Inv(a63) \land $ \\ 
 $  \Rnext E2L3Inv(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5(a86_a85) \land $ \\ 
 $  \Rnext C2(a37) \land $ \\ 
 $  \Rnext  \Rnext E2L3Inv(a50) \land $ \\ 
 $ E1G3Inv(a90) \land $ \\ 
 $ E1G3Inv(a40) \land $ \\ 
 $ E1G3Inv(a41) \land $ \\ 
 $ E1G3Inv(a53_a30) \land $ \\ 
 $ E1G3Inv(a89_a29) \land $ \\ 
 $ E1G3Inv(a91) \land $ \\ 
 $ E1G3Inv(a50) \land $ \\ 
 $ E1G3Inv(a63) \land $ \\ 
 $ E1G3Inv(a71) \land $ \\ 
 $ E1G3Inv(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $ E1G3Inv(a37) \land $ \\ 
 $ E1G3Inv(a14) \land $ \\ 
 $ E1G3Inv(a60) \land $ \\ 
 $ E1G3Inv(a82) \land $ \\ 
 $ E1G3Inv(a11) \land $ \\ 
 $ E1G3Inv(a38) \land $ \\ 
 $ E1G3Inv(a3) \land $ \\ 
 $ E1G3Inv(a98) \land $ \\ 
 $ E1G3Inv(a7) \land $ \\ 
 $ E1G3Inv(a31) \land $ \\ 
 $ E1G3Inv(a86_a85) \land $ \\ 
 $ E1G3Inv(a10) \land $ \\ 
 $ E1G3Inv(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5(a91) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a10) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a10) \land $ \\ 
 $  \Rnext E2L3(a14) \land $ \\ 
 $  \Rnext  \Rnext E2L3Inv(a38) \land $ \\ 
 $  \Rnext  \Rnext C3(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a11) \land $ \\ 
 $  \Rnext C0(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5(a3) \land $ \\ 
 $ E3G2(a87) \land $ \\ 
 $ E3G2(a89_a29) \land $ \\ 
 $ E3G2(a41) \land $ \\ 
 $ E3G2(a86_a85) \land $ \\ 
 $ E3G2(a53_a30) \land $ \\ 
 $ E3G2(a91) \land $ \\ 
 $ E3G2(a98) \land $ \\ 
 $ E3G2(a90) \land $ \\ 
 $ E3G2(a7) \land $ \\ 
 $ E3G2(a82) \land $ \\ 
 $ E3G2(a11) \land $ \\ 
 $ E3G2(a63) \land $ \\ 
 $ E3G2(a37) \land $ \\ 
 $ E3G2(a60) \land $ \\ 
 $ E3G2(a31) \land $ \\ 
 $ E3G2(a71) \land $ \\ 
 $ E3G2(a38) \land $ \\ 
 $ E3G2(a40) \land $ \\ 
 $ E3G2(a50) \land $ \\ 
 $ E3G2(a14) \land $ \\ 
 $ E3G2(a3) \land $ \\ 
 $ E3G2(a10) \land $ \\ 
 $ E3G2(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3Inv(a14) \land $ \\ 
 $  \Rnext E2L4(a82) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a60) \land $ \\ 
 $ E2G4(a89_a29) \land $ \\ 
 $  \Rnext E2L4(a31) \land $ \\ 
 $ E2G4(a41) \land $ \\ 
 $ E2G4(a40) \land $ \\ 
 $ E2G4(a31) \land $ \\ 
 $ E2G4(a11) \land $ \\ 
 $ E2G4(a50) \land $ \\ 
 $ E2G4(a7) \land $ \\ 
 $ E2G4(a91) \land $ \\ 
 $ E2G4(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $ E2G4(a90) \land $ \\ 
 $ E2G4(a37) \land $ \\ 
 $ E2G4(a38) \land $ \\ 
 $ E2G4(a87) \land $ \\ 
 $ E2G4(a3) \land $ \\ 
 $ E2G4(a98) \land $ \\ 
 $ E2G4(a10) \land $ \\ 
 $ E2G4(a63) \land $ \\ 
 $ E2G4(a86_a85) \land $ \\ 
 $ E2G4(a82) \land $ \\ 
 $ E2G4(a71) \land $ \\ 
 $ E2G4(a14) \land $ \\ 
 $ E2G4(a60) \land $ \\ 
 $ E2G4(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext C0(a40) \land $ \\ 
 $  \Rnext E2L4Inv(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3(a7) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5Inv(a87) \land $ \\ 
 $  \Rnext E3L2Inv(a7) \land $ \\ 
 $  \Rnext C1(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a10) \land $ \\ 
 $  \Rnext  \Rnext C5(a10) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5(a63) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a7) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2(a91) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a86_a85) \land $ \\ 
 $  \Rnext C0(a82) \land $ \\ 
 $  \Rnext C2(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2Inv(a90) \land $ \\ 
 $  \Rnext  \Rnext E2L5Inv(a90) \land $ \\ 
 $  \Rnext C0(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C5(a87) \land $ \\ 
 $  \Rnext E2L3Inv(a3) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C5(a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5Inv(a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3Inv(a11) \land $ \\ 
 $  \Rnext E2L3Inv(a14) \land $ \\ 
 $  \Rnext C0(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a11) \land $ \\ 
 $  \Rnext E2L4(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3(a90) \land $ \\ 
 $  \Rnext C3(a10) \land $ \\ 
 $  \Rnext  \Rnext C3(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext C4(a53_a30) \land $ \\ 
 $  \Rnext C2(a7) \land $ \\ 
 $  \Rnext  \Rnext E3L2Inv(a91) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C5(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a14) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a60) \land $ \\ 
 $  \Rnext  \Rnext E3L2Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext E3L2Inv(a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a91) \land $ \\ 
 $  \Rnext  \Rnext C4(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a71) \land $ \\ 
 $  \Rnext E2L3(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C4(a31) \land $ \\ 
 $  \Rnext E2L3Inv(a60) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a87) \land $ \\ 
 $  \Rnext E3L2Inv(a14) \land $ \\ 
 $  \Rnext E2L4Inv(a90) \land $ \\ 
 $  \Rnext E3L2Inv(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext E3L2Inv(a63) \land $ \\ 
 $  \Rnext  \Rnext C3(a90) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a91) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2(a87) \land $ \\ 
 $  \Rnext E2L3Inv(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C5(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4Inv(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4Inv(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a91) \land $ \\ 
 $ C1(a37) \land $ \\ 
 $ C1(a89_a29) \land $ \\ 
 $ C1(a53_a30) \land $ \\ 
 $ C1(a40) \land $ \\ 
 $ C1(a87) \land $ \\ 
 $ C1(a91) \land $ \\ 
 $ C1(a14) \land $ \\ 
 $ C1(a71) \land $ \\ 
 $ C1(a90) \land $ \\ 
 $ C1(a38) \land $ \\ 
 $ C1(a41) \land $ \\ 
 $ C1(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $ C1(a50) \land $ \\ 
 $ C1(a82) \land $ \\ 
 $ C1(a60) \land $ \\ 
 $ C1(a10) \land $ \\ 
 $ C1(a63) \land $ \\ 
 $ C1(a3) \land $ \\ 
 $ C1(a86_a85) \land $ \\ 
 $ C1(a11) \land $ \\ 
 $ C1(a7) \land $ \\ 
 $ C1(a98) \land $ \\ 
 $ C1(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4Inv(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3Inv(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5Inv(a71) \land $ \\ 
 $  \Rnext E3L2(a82) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext C3(a91) \land $ \\ 
 $  \Rnext  \Rnext C3(a31) \land $ \\ 
 $  \Rnext  \Rnext E3L2(a10) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C4(a37) \land $ \\ 
 $  \Rnext  \Rnext E3L2Inv(a14) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2Inv(a82) \land $ \\ 
 $  \Rnext E2L5Inv(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2Inv(a38) \land $ \\ 
 $  \Rnext  \Rnext C4(a10) \land $ \\ 
 $  \Rnext  \Rnext C0(a53_a30) \land $ \\ 
 $  \Rnext E3L0Inv(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a71) \land $ \\ 
 $  \Rnext E2L3(a60) \land $ \\ 
 $  \Rnext E3L0Inv(a53_a30) \land $ \\ 
 $ E2G0(a41) \land $ \\ 
 $ E2G0(a89_a29) \land $ \\ 
 $ E2G0(a40) \land $ \\ 
 $ E2G0(a14) \land $ \\ 
 $ E2G0(a86_a85) \land $ \\ 
 $ E2G0(a63) \land $ \\ 
 $ E2G0(a60) \land $ \\ 
 $ E2G0(a87) \land $ \\ 
 $ E2G0(a10) \land $ \\ 
 $ E2G0(a90) \land $ \\ 
 $ E2G0(a31) \land $ \\ 
 $ E2G0(a71) \land $ \\ 
 $ E2G0(a91) \land $ \\ 
 $ E2G0(a98) \land $ \\ 
 $ E2G0(a7) \land $ \\ 
 $ E2G0(a53_a30) \land $ \\ 
 $ E2G0(a82) \land $ \\ 
 $ E2G0(a11) \land $ \\ 
 $ E2G0(a3) \land $ \\ 
 $ E2G0(a38) \land $ \\ 
 $ E2G0(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $ E2G0(a50) \land $ \\ 
 $ E2G0(a37) \land $ \\ 
 $  \Rnext  \Rnext E2L4Inv(a90) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4(a50) \land $ \\ 
 $  \Rnext E3L2Inv(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C4(a82) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a82) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a7) \land $ \\ 
 $  \Rnext C4(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C4(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C4(a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a63) \land $ \\ 
 $  \Rnext  \Rnext E2L4Inv(a86_a85) \land $ \\ 
 $  \Rnext E2L5Inv(a90) \land $ \\ 
 $  \Rnext  \Rnext C2(a10) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a11) \land $ \\ 
 $  \Rnext  \Rnext E2L4Inv(a3) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2Inv(a37) \land $ \\ 
 $  \Rnext E2L4(a7) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4Inv(a86_a85) \land $ \\ 
 $  \Rnext C5(a89_a29) \land $ \\ 
 $  \Rnext E2L4(a90) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a31) \land $ \\ 
 $  \Rnext E2L5Inv(a50) \land $ \\ 
 $ E3L1(a10) \land $ \\ 
 $ E3L1(a40) \land $ \\ 
 $ E3L1(a89_a29) \land $ \\ 
 $ E3L1(a41) \land $ \\ 
 $ E3L1(a87) \land $ \\ 
 $ E3L1(a11) \land $ \\ 
 $ E3L1(a91) \land $ \\ 
 $ E3L1(a90) \land $ \\ 
 $ E3L1(a14) \land $ \\ 
 $ E3L1(a3) \land $ \\ 
 $ E3L1(a60) \land $ \\ 
 $ E3L1(a31) \land $ \\ 
 $ E3L1(a82) \land $ \\ 
 $ E3L1(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $ E3L1(a7) \land $ \\ 
 $ E3L1(a53_a30) \land $ \\ 
 $ E3L1(a38) \land $ \\ 
 $ E3L1(a71) \land $ \\ 
 $ E3L1(a86_a85) \land $ \\ 
 $ E3L1(a50) \land $ \\ 
 $ E3L1(a37) \land $ \\ 
 $ E3L1(a98) \land $ \\ 
 $ E3L1(a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext E2L3Inv(a91) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2(a38) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a91) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C4(a11) \land $ \\ 
 $ E2L3(a86_a85) \land $ \\ 
 $ E2L3(a89_a29) \land $ \\ 
 $ E2L3(a41) \land $ \\ 
 $ E2L3(a63) \land $ \\ 
 $ E2L3(a98) \land $ \\ 
 $ E2L3(a3) \land $ \\ 
 $ E2L3(a37) \land $ \\ 
 $ E2L3(a87) \land $ \\ 
 $ E2L3(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $ E2L3(a31) \land $ \\ 
 $  \Rnext E2L5Inv(a14) \land $ \\ 
 $ E2L3(a91) \land $ \\ 
 $ E2L3(a7) \land $ \\ 
 $ E2L3(a38) \land $ \\ 
 $ E2L3(a90) \land $ \\ 
 $ E2L3(a53_a30) \land $ \\ 
 $ E2L3(a11) \land $ \\ 
 $ E2L3(a82) \land $ \\ 
 $ E2L3(a10) \land $ \\ 
 $ E2L3(a60) \land $ \\ 
 $ E2L3(a40) \land $ \\ 
 $ E2L3(a14) \land $ \\ 
 $ E2L3(a50) \land $ \\ 
 $ E2L3(a71) \land $ \\ 
 $  \Rnext C1(a60) \land $ \\ 
 $  \Rnext C4(a87) \land $ \\ 
 $ E2L3Inv(a71) \land $ \\ 
 $ E2L3Inv(a89_a29) \land $ \\ 
 $ E2L3Inv(a98) \land $ \\ 
 $ E2L3Inv(a86_a85) \land $ \\ 
 $ E2L3Inv(a14) \land $ \\ 
 $ E2L3Inv(a10) \land $ \\ 
 $ E2L3Inv(a3) \land $ \\ 
 $ E2L3Inv(a31) \land $ \\ 
 $ E2L3Inv(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $ E2L3Inv(a40) \land $ \\ 
 $ E2L3Inv(a41) \land $ \\ 
 $ E2L3Inv(a60) \land $ \\ 
 $ E2L3Inv(a90) \land $ \\ 
 $ E2L3Inv(a11) \land $ \\ 
 $ E2L3Inv(a53_a30) \land $ \\ 
 $ E2L3Inv(a91) \land $ \\ 
 $ E2L3Inv(a38) \land $ \\ 
 $ E2L3Inv(a87) \land $ \\ 
 $ E2L3Inv(a63) \land $ \\ 
 $ E2L3Inv(a37) \land $ \\ 
 $ E2L3Inv(a50) \land $ \\ 
 $ E2L3Inv(a82) \land $ \\ 
 $ E2L3Inv(a7) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a63) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a90) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3Inv(a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4(a91) \land $ \\ 
 $  \Rnext  \Rnext C1(a3) \land $ \\ 
 $  \Rnext E2L3(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext C2(a60) \land $ \\ 
 $  \Rnext  \Rnext C3(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5Inv(a89_a29) \land $ \\ 
 $  \Rnext E3L2(a40) \land $ \\ 
 $  \Rnext E3L2Inv(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2Inv(a82) \land $ \\ 
 $  \Rnext E3L1Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a10) \land $ \\ 
 $  \Rnext C3(a14) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C5(a7) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2(a41) \land $ \\ 
 $  \Rnext E3L0(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3(a14) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a53_a30) \land $ \\ 
 $  \Rnext C0(a10) \land $ \\ 
 $  \Rnext E3L1(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5(a7) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2Inv(a53_a30) \land $ \\ 
 $  \Rnext C1(a90) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a41) \land $ \\ 
 $  \Rnext  \Rnext C4(a63) \land $ \\ 
 $  \Rnext C1(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3(a63) \land $ \\ 
 $  \Rnext  \Rnext E2L4Inv(a91) \land $ \\ 
 $  \Rnext  \Rnext C1(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a41) \land $ \\ 
 $  \Rnext E3L2Inv(a60) \land $ \\ 
 $  \Rnext  \Rnext C5(a3) \land $ \\ 
 $  \Rnext  \Rnext E2L3Inv(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C5(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a7) \land $ \\ 
 $  \Rnext  \Rnext E2L5Inv(a11) \land $ \\ 
 $  \Rnext  \Rnext E2L3Inv(a71) \land $ \\ 
 $  \Rnext E2L4Inv(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3Inv(a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext E2L3Inv(a11) \land $ \\ 
 $  \Rnext C1(a7) \land $ \\ 
 $  \Rnext  \Rnext C0(a7) \land $ \\ 
 $  \Rnext C1(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext C4(a11) \land $ \\ 
 $  \Rnext  \Rnext C5(a90) \land $ \\ 
 $  \Rnext E2L5(a7) \land $ \\ 
 $  \Rnext  \Rnext E2L5Inv(a7) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5Inv(a98) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a98) \land $ \\ 
 $  \Rnext E3L0(a91) \land $ \\ 
 $  \Rnext E3L1(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4Inv(a3) \land $ \\ 
 $  \Rnext E3L0Inv(a40) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext E2L3Inv(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a90) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext E3L2(a10) \land $ \\ 
 $  \Rnext  \Rnext C1(a37) \land $ \\ 
 $  \Rnext C3(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext E2L3Inv(a7) \land $ \\ 
 $  \Rnext  \Rnext E2L3(a53_a30) \land $ \\ 
 $  \Rnext E3L2(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5Inv(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext E2L4(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a90) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a7) \land $ \\ 
 $  \Rnext  \Rnext E2L5(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a37) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a31) \land $ \\ 
 $  \Rnext  \Rnext E2L4(a50) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4(a91) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a90) \land $ \\ 
 $  \Rnext  \Rnext C5(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a14) \land $ \\ 
 $  \Rnext  \Rnext C4(a71) \land $ \\ 
 $  \Rnext C5(a91) \land $ \\ 
 $  \Rnext  \Rnext E3L2(a14) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C5(a82) \land $ \\ 
 $  \Rnext C3(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2(a14) \land $ \\ 
 $  \Rnext  \Rnext E2L5Inv(a91) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a7) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a50) \land $ \\ 
 $  \Rnext C5(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C4(a38) \land $ \\ 
 $  \Rnext  \Rnext C3(a3) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3(a38) \land $ \\ 
 $ E3L0Inv(a60) \land $ \\ 
 $ E3L0Inv(a40) \land $ \\ 
 $ E3L0Inv(a86_a85) \land $ \\ 
 $ E3L0Inv(a14) \land $ \\ 
 $ E3L0Inv(a89_a29) \land $ \\ 
 $ E3L0Inv(a91) \land $ \\ 
 $ E3L0Inv(a63) \land $ \\ 
 $ E3L0Inv(a41) \land $ \\ 
 $ E3L0Inv(a87) \land $ \\ 
 $ E3L0Inv(a37) \land $ \\ 
 $ E3L0Inv(a98) \land $ \\ 
 $ E3L0Inv(a11) \land $ \\ 
 $ E3L0Inv(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $ E3L0Inv(a3) \land $ \\ 
 $ E3L0Inv(a90) \land $ \\ 
 $ E3L0Inv(a7) \land $ \\ 
 $ E3L0Inv(a31) \land $ \\ 
 $ E3L0Inv(a10) \land $ \\ 
 $ E3L0Inv(a53_a30) \land $ \\ 
 $ E3L0Inv(a82) \land $ \\ 
 $ E3L0Inv(a38) \land $ \\ 
 $ E3L0Inv(a71) \land $ \\ 
 $ E3L0Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a91) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a82) \land $ \\ 
 $  \Rnext  \Rnext E2L5(a90) \land $ \\ 
 $  \Rnext  \Rnext C0(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a63) \land $ \\ 
 $  \Rnext C4(a3) \land $ \\ 
 $  \Rnext E2L4Inv(a87) \land $ \\ 
 $  \Rnext  \Rnext E2L3Inv(a60) \land $ \\ 
 $  \Rnext  \Rnext E2L5(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a40) \land $ \\ 
 $  \Rnext E3L1(a10) \land $ \\ 
 $  \Rnext E2L5(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3Inv(a50) \land $ \\ 
 $  \Rnext E2L3Inv(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4Inv(a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3(a10) \land $ \\ 
 $  \Rnext  \Rnext E2L4Inv(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext C4(a82) \land $ \\ 
 $  \Rnext C5(a71) \land $ \\ 
 $  \Rnext  \Rnext E3L2(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a14) \land $ \\ 
 $  \Rnext E3L2(a71) \land $ \\ 
 $  \Rnext E3L1Inv(a90) \land $ \\ 
 $  \Rnext  \Rnext E2L5(a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5Inv(a3) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3Inv(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2(a41) \land $ \\ 
 $  \Rnext  \Rnext C5(a40) \land $ \\ 
 $  \Rnext  \Rnext E2L4(a82) \land $ \\ 
 $  \Rnext E2L4Inv(a10) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C4(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext C4(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3Inv(a3) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5(a89_a29) \land $ \\ 
 $  \Rnext C4(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a71) \land $ \\ 
 $  \Rnext E3L1Inv(a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2Inv(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a41) \land $ \\ 
 $  \Rnext E3L2(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2(a10) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2Inv(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3Inv(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2Inv(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a7) \land $ \\ 
 $  \Rnext E2L4Inv(a82) \land $ \\ 
 $  \Rnext E2L3(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4(a63) \land $ \\ 
 $  \Rnext  \Rnext E2L4Inv(a38) \land $ \\ 
 $  \Rnext E2L5(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2(a82) \land $ \\ 
 $  \Rnext E2L3Inv(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a37) \land $ \\ 
 $  \Rnext E2L3(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a11) \land $ \\ 
 $  \Rnext  \Rnext E3L2Inv(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3Inv(a90) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C5(a7) \land $ \\ 
 $  \Rnext E2L3(a40) \land $ \\ 
 $  \Rnext C3(a86_a85) \land $ \\ 
 $  \Rnext E2L5(a40) \land $ \\ 
 $  \Rnext C0(a14) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3(a87) \land $ \\ 
 $  \Rnext  \Rnext C1(a90) \land $ \\ 
 $  \Rnext E3L2(a41) \land $ \\ 
 $  \Rnext C1(a14) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a86_a85) \land $ \\ 
 $  \Rnext E2L4(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C4(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext C5(a31) \land $ \\ 
 $  \Rnext  \Rnext C0(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4Inv(a87) \land $ \\ 
 $  \Rnext E3L2Inv(a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C5(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a71) \land $ \\ 
 $  \Rnext  \Rnext E2L5Inv(a71) \land $ \\ 
 $  \Rnext  \Rnext C5(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext E2L4(a50) \land $ \\ 
 $  \Rnext  \Rnext E2L3(a87) \land $ \\ 
 $  \Rnext  \Rnext E2L4Inv(a41) \land $ \\ 
 $  \Rnext E2L5(a90) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a71) \land $ \\ 
 $  \Rnext E2L5(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext C0(a90) \land $ \\ 
 $  \Rnext E2L4Inv(a3) \land $ \\ 
 $  \Rnext C4(a38) \land $ \\ 
 $  \Rnext E3L0Inv(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext E2L5Inv(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a41) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a37) \land $ \\ 
 $  \Rnext E3L2Inv(a37) \land $ \\ 
 $  \Rnext E3L1(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C5(a90) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3(a37) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $ E2G5(a89_a29) \land $ \\ 
 $ E2G5(a90) \land $ \\ 
 $ E2G5(a41) \land $ \\ 
 $ E2G5(a82) \land $ \\ 
 $ E2G5(a40) \land $ \\ 
 $ E2G5(a60) \land $ \\ 
 $ E2G5(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $ E2G5(a98) \land $ \\ 
 $ E2G5(a37) \land $ \\ 
 $ E2G5(a10) \land $ \\ 
 $ E2G5(a14) \land $ \\ 
 $ E2G5(a3) \land $ \\ 
 $ E2G5(a87) \land $ \\ 
 $ E2G5(a63) \land $ \\ 
 $ E2G5(a53_a30) \land $ \\ 
 $ E2G5(a38) \land $ \\ 
 $ E2G5(a71) \land $ \\ 
 $ E2G5(a50) \land $ \\ 
 $ E2G5(a91) \land $ \\ 
 $ E2G5(a86_a85) \land $ \\ 
 $ E2G5(a11) \land $ \\ 
 $ E2G5(a31) \land $ \\ 
 $ E2G5(a7) \land $ \\ 
 $  \Rnext  \Rnext E3L2Inv(a89_a29) \land $ \\ 
 $  \Rnext E2L5(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a38) \land $ \\ 
 $  \Rnext C2(a3) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a3) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C5(a98) \land $ \\ 
 $  \Rnext  \Rnext E3L2(a87) \land $ \\ 
 $  \Rnext E2L3Inv(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a86_a85) \land $ \\ 
 $  \Rnext C3(a82) \land $ \\ 
 $  \Rnext  \Rnext E2L5Inv(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3Inv(a91) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C4(a50) \land $ \\ 
 $  \Rnext C1(a91) \land $ \\ 
 $  \Rnext E2L4Inv(a63) \land $ \\ 
 $  \Rnext  \Rnext E3L2(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5(a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C4(a40) \land $ \\ 
 $  \Rnext  \Rnext E2L5Inv(a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5Inv(a11) \land $ \\ 
 $  \Rnext  \Rnext C0(a63) \land $ \\ 
 $  \Rnext C0(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2Inv(a3) \land $ \\ 
 $  \Rnext  \Rnext C4(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext C4(a31) \land $ \\ 
 $  \Rnext E2L3Inv(a10) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3Inv(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C5(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a91) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a60) \land $ \\ 
 $  \Rnext C3(a53_a30) \land $ \\ 
 $  \Rnext E2L4(a3) \land $ \\ 
 $  \Rnext  \Rnext E2L4Inv(a40) \land $ \\ 
 $  \Rnext C5(a90) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a87) \land $ \\ 
 $  \Rnext E3L2(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C5(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C4(a91) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3(a50) \land $ \\ 
 $  \Rnext E3L1(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2(a87) \land $ \\ 
 $  \Rnext E3L0Inv(a11) \land $ \\ 
 $  \Rnext  \Rnext E2L3Inv(a91) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a50) \land $ \\ 
 $  \Rnext E3L0Inv(a86_a85) \land $ \\ 
 $  \Rnext E2L5Inv(a91) \land $ \\ 
 $  \Rnext  \Rnext C4(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2Inv(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C5(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a11) \land $ \\ 
 $  \Rnext E3L1(a38) \land $ \\ 
 $  \Rnext  \Rnext E3L2Inv(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a90) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C4(a60) \land $ \\ 
 $  \Rnext  \Rnext C1(a53_a30) \land $ \\ 
 $  \Rnext E2L3(a90) \land $ \\ 
 $  \Rnext C0(a41) \land $ \\ 
 $  \Rnext  \Rnext C3(a37) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a40) \land $ \\ 
 $  \Rnext  \Rnext C5(a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5Inv(a14) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a91) \land $ \\ 
 $  \Rnext C2(a90) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a3) \land $ \\ 
 $  \Rnext  \Rnext E2L5(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4(a89_a29) \land $ \\ 
 $  \Rnext E3L0Inv(a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C4(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a11) \land $ \\ 
 $  \Rnext  \Rnext E2L3Inv(a10) \land $ \\ 
 $  \Rnext E3L0(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C4(a14) \land $ \\ 
 $ C2(a89_a29) \land $ \\ 
 $  \Rnext E2L3(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $ C2(a40) \land $ \\ 
 $ C2(a41) \land $ \\ 
 $ C2(a14) \land $ \\ 
 $ C2(a63) \land $ \\ 
 $ C2(a3) \land $ \\ 
 $ C2(a87) \land $ \\ 
 $ C2(a90) \land $ \\ 
 $ C2(a7) \land $ \\ 
 $ C2(a10) \land $ \\ 
 $ C2(a60) \land $ \\ 
 $ C2(a86_a85) \land $ \\ 
 $ C2(a38) \land $ \\ 
 $ C2(a11) \land $ \\ 
 $ C2(a37) \land $ \\ 
 $ C2(a82) \land $ \\ 
 $ C2(a31) \land $ \\ 
 $ C2(a91) \land $ \\ 
 $ C2(a71) \land $ \\ 
 $ C2(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $ C2(a98) \land $ \\ 
 $ C2(a53_a30) \land $ \\ 
 $ C2(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5(a14) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3Inv(a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2(a11) \land $ \\ 
 $  \Rnext C1(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4Inv(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C5(a3) \land $ \\ 
 $  \Rnext  \Rnext C2(a71) \land $ \\ 
 $  \Rnext  \Rnext C2(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext C3(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a10) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a38) \land $ \\ 
 $  \Rnext  \Rnext C0(a60) \land $ \\ 
 $  \Rnext  \Rnext C2(a38) \land $ \\ 
 $  \Rnext  \Rnext C0(a98) \land $ \\ 
 $  \Rnext  \Rnext C2(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a86_a85) \land $ \\ 
 $  \Rnext E2L3Inv(a90) \land $ \\ 
 $  \Rnext E2L5Inv(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a60) \land $ \\ 
 $  \Rnext E2L5(a10) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a50) \land $ \\ 
 $  \Rnext  \Rnext E2L3(a90) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext E3L2Inv(a7) \land $ \\ 
 $  \Rnext  \Rnext C2(a7) \land $ \\ 
 $  \Rnext  \Rnext E3L2Inv(a3) \land $ \\ 
 $  \Rnext  \Rnext C4(a41) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext C0(a10) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a82) \land $ \\ 
 $  \Rnext E3L2Inv(a38) \land $ \\ 
 $  \Rnext E3L2Inv(a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a40) \land $ \\ 
 $  \Rnext E3L1(a7) \land $ \\ 
 $  \Rnext E3L2(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3Inv(a14) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3Inv(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext E2L4(a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5(a14) \land $ \\ 
 $  \Rnext  \Rnext E2L5(a14) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a3) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext E3L2Inv(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext E2L5Inv(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3Inv(a37) \land $ \\ 
 $  \Rnext E2L3Inv(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a82) \land $ \\ 
 $  \Rnext  \Rnext E2L4Inv(a14) \land $ \\ 
 $  \Rnext E2L5Inv(a37) \land $ \\ 
 $  \Rnext C4(a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a10) \land $ \\ 
 $  \Rnext C3(a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3(a3) \land $ \\ 
 $  \Rnext  \Rnext E2L3Inv(a3) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5(a10) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4Inv(a90) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5Inv(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5Inv(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a98) \land $ \\ 
 $  \Rnext  \Rnext C3(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4Inv(a10) \land $ \\ 
 $  \Rnext E2L4Inv(a14) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3(a90) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a14) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5Inv(a10) \land $ \\ 
 $  \Rnext E3L1Inv(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5Inv(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext C1(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext C0(a41) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a60) \land $ \\ 
 $ E2L5Inv(a86_a85) \land $ \\ 
 $ E2L5Inv(a41) \land $ \\ 
 $ E2L5Inv(a91) \land $ \\ 
 $ E2L5Inv(a89_a29) \land $ \\ 
 $ E2L5Inv(a63) \land $ \\ 
 $ E2L5Inv(a90) \land $ \\ 
 $ E2L5Inv(a53_a30) \land $ \\ 
 $ E2L5Inv(a60) \land $ \\ 
 $ E2L5Inv(a3) \land $ \\ 
 $ E2L5Inv(a38) \land $ \\ 
 $ E2L5Inv(a37) \land $ \\ 
 $ E2L5Inv(a50) \land $ \\ 
 $ E2L5Inv(a98) \land $ \\ 
 $ E2L5Inv(a40) \land $ \\ 
 $ E2L5Inv(a7) \land $ \\ 
 $ E2L5Inv(a10) \land $ \\ 
 $ E2L5Inv(a14) \land $ \\ 
 $ E2L5Inv(a87) \land $ \\ 
 $ E2L5Inv(a71) \land $ \\ 
 $ E2L5Inv(a82) \land $ \\ 
 $ E2L5Inv(a11) \land $ \\ 
 $ E2L5Inv(a31) \land $ \\ 
 $ E2L5Inv(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5Inv(a10) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext E3L0(a98) \land $ \\ 
 $  \Rnext E2L5Inv(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5(a40) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4Inv(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5(a90) \land $ \\ 
 $  \Rnext  \Rnext E2L4(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5(a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2(a3) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5Inv(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3Inv(a71) \land $ \\ 
 $  \Rnext E3L2Inv(a10) \land $ \\ 
 $  \Rnext E3L0(a87) \land $ \\ 
 $  \Rnext E3L0(a63) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a14) \land $ \\ 
 $  \Rnext  \Rnext C1(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4Inv(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2Inv(a14) \land $ \\ 
 $  \Rnext  \Rnext C2(a50) \land $ \\ 
 $  \Rnext E3L1Inv(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a7) \land $ \\ 
 $  \Rnext C3(a60) \land $ \\ 
 $  \Rnext  \Rnext E3L2Inv(a38) \land $ \\ 
 $  \Rnext  \Rnext E3L2(a91) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a14) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2Inv(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5Inv(a90) \land $ \\ 
 $  \Rnext E2L4Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3Inv(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C4(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a91) \land $ \\ 
 $  \Rnext  \Rnext E2L3(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a86_a85) \land $ \\ 
 $  \Rnext E2L3Inv(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a11) \land $ \\ 
 $  \Rnext E2L4(a10) \land $ \\ 
 $  \Rnext E3L2(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext E2L3Inv(a37) \land $ \\ 
 $  \Rnext  \Rnext E2L4Inv(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a90) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3Inv(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a7) \land $ \\ 
 $  \Rnext  \Rnext E2L4(a10) \land $ \\ 
 $  \Rnext E2L3(a87) \land $ \\ 
 $  \Rnext  \Rnext E3L2Inv(a60) \land $ \\ 
 $  \Rnext C2(a10) \land $ \\ 
 $  \Rnext  \Rnext C2(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2Inv(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C5(a11) \land $ \\ 
 $  \Rnext C0(a60) \land $ \\ 
 $  \Rnext  \Rnext E2L4(a41) \land $ \\ 
 $  \Rnext  \Rnext C3(a91) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext C0(a14) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a60) \land $ \\ 
 $  \Rnext E2L4Inv(a11) \land $ \\ 
 $  \Rnext E3L0Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5Inv(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4(a3) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a3) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a40) \land $ \\ 
 $  \Rnext  \Rnext E2L4Inv(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a11) \land $ \\ 
 $  \Rnext  \Rnext C5(a14) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2(a14) \land $ \\ 
 $ E1G4Inv(a90) \land $ \\ 
 $ E1G4Inv(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a60) \land $ \\ 
 $ E1G4Inv(a31) \land $ \\ 
 $ E1G4Inv(a71) \land $ \\ 
 $ E1G4Inv(a63) \land $ \\ 
 $ E1G4Inv(a11) \land $ \\ 
 $ E1G4Inv(a40) \land $ \\ 
 $ E1G4Inv(a7) \land $ \\ 
 $ E1G4Inv(a91) \land $ \\ 
 $ E1G4Inv(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $ E1G4Inv(a60) \land $ \\ 
 $ E1G4Inv(a87) \land $ \\ 
 $ E1G4Inv(a3) \land $ \\ 
 $ E1G4Inv(a41) \land $ \\ 
 $ E1G4Inv(a86_a85) \land $ \\ 
 $ E1G4Inv(a98) \land $ \\ 
 $ E1G4Inv(a37) \land $ \\ 
 $ E1G4Inv(a38) \land $ \\ 
 $ E1G4Inv(a53_a30) \land $ \\ 
 $ E1G4Inv(a10) \land $ \\ 
 $ E1G4Inv(a50) \land $ \\ 
 $ E1G4Inv(a14) \land $ \\ 
 $ E1G4Inv(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext E2L3(a11) \land $ \\ 
 $ E3L2(a40) \land $ \\ 
 $ E3L2(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext E2L3(a82) \land $ \\ 
 $ E3L2(a41) \land $ \\ 
 $ E3L2(a31) \land $ \\ 
 $ E3L2(a10) \land $ \\ 
 $ E3L2(a37) \land $ \\ 
 $ E3L2(a50) \land $ \\ 
 $ E3L2(a90) \land $ \\ 
 $ E3L2(a7) \land $ \\ 
 $ E3L2(a63) \land $ \\ 
 $ E3L2(a14) \land $ \\ 
 $ E3L2(a82) \land $ \\ 
 $ E3L2(a87) \land $ \\ 
 $ E3L2(a3) \land $ \\ 
 $ E3L2(a53_a30) \land $ \\ 
 $ E3L2(a71) \land $ \\ 
 $ E3L2(a91) \land $ \\ 
 $ E3L2(a38) \land $ \\ 
 $ E3L2(a60) \land $ \\ 
 $ E3L2(a11) \land $ \\ 
 $ E3L2(a98) \land $ \\ 
 $ E3L2(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $ E3L2(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4Inv(a82) \land $ \\ 
 $  \Rnext  \Rnext C2(a31) \land $ \\ 
 $  \Rnext  \Rnext E2L5Inv(a10) \land $ \\ 
 $  \Rnext C2(a63) \land $ \\ 
 $ E2L4(a41) \land $ \\ 
 $ E2L4(a91) \land $ \\ 
 $ E2L4(a89_a29) \land $ \\ 
 $ E2L4(a87) \land $ \\ 
 $ E2L4(a90) \land $ \\ 
 $ E2L4(a10) \land $ \\ 
 $ E2L4(a38) \land $ \\ 
 $ E2L4(a82) \land $ \\ 
 $ E2L4(a53_a30) \land $ \\ 
 $ E2L4(a40) \land $ \\ 
 $ E2L4(a86_a85) \land $ \\ 
 $ E2L4(a7) \land $ \\ 
 $ E2L4(a3) \land $ \\ 
 $ E2L4(a50) \land $ \\ 
 $ E2L4(a11) \land $ \\ 
 $ E2L4(a14) \land $ \\ 
 $ E2L4(a37) \land $ \\ 
 $ E2L4(a98) \land $ \\ 
 $ E2L4(a63) \land $ \\ 
 $ E2L4(a60) \land $ \\ 
 $ E2L4(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $ E2L4(a31) \land $ \\ 
 $ E2L4(a71) \land $ \\ 
 $  \Rnext E2L3(a41) \land $ \\ 
 $  \Rnext E3L1(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4Inv(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2Inv(a10) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a98) \land $ \\ 
 $  \Rnext  \Rnext E3L2Inv(a10) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a38) \land $ \\ 
 $  \Rnext E3L1Inv(a60) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5Inv(a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4Inv(a3) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a63) \land $ \\ 
 $  \Rnext C5(a7) \land $ \\ 
 $  \Rnext E3L1Inv(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a40) \land $ \\ 
 $  \Rnext  \Rnext E3L2(a41) \land $ \\ 
 $  \Rnext  \Rnext C3(a86_a85) \land $ \\ 
 $  \Rnext C3(a90) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a40) \land $ \\ 
 $  \Rnext  \Rnext E2L5Inv(a98) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C4(a63) \land $ \\ 
 $  \Rnext  \Rnext E2L5Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C4(a71) \land $ \\ 
 $  \Rnext  \Rnext C1(a14) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a37) \land $ \\ 
 $  \Rnext E2L4Inv(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3(a3) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a53_a30) \land $ \\ 
 $  \Rnext E3L0(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C5(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C4(a90) \land $ \\ 
 $  \Rnext E2L5Inv(a40) \land $ \\ 
 $  \Rnext E3L1(a50) \land $ \\ 
 $  \Rnext  \Rnext C5(a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4Inv(a91) \land $ \\ 
 $  \Rnext E3L1Inv(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C4(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3(a14) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext C5(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C5(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a11) \land $ \\ 
 $  \Rnext C5(a50) \land $ \\ 
 $  \Rnext  \Rnext E2L5Inv(a53_a30) \land $ \\ 
 $  \Rnext E2L4(a37) \land $ \\ 
 $  \Rnext E2L4Inv(a41) \land $ \\ 
 $  \Rnext E2L4Inv(a91) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2Inv(a14) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C5(a14) \land $ \\ 
 $  \Rnext E2L5(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5Inv(a82) \land $ \\ 
 $  \Rnext E2L4(a14) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a90) \land $ \\ 
 $  \Rnext  \Rnext C4(a98) \land $ \\ 
 $  \Rnext E2L4Inv(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a63) \land $ \\ 
 $  \Rnext E3L0(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2(a3) \land $ \\ 
 $ E1G2Inv(a40) \land $ \\ 
 $ E1G2Inv(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C5(a3) \land $ \\ 
 $ E1G2Inv(a63) \land $ \\ 
 $ E1G2Inv(a60) \land $ \\ 
 $ E1G2Inv(a38) \land $ \\ 
 $ E1G2Inv(a41) \land $ \\ 
 $ E1G2Inv(a14) \land $ \\ 
 $ E1G2Inv(a50) \land $ \\ 
 $ E1G2Inv(a31) \land $ \\ 
 $ E1G2Inv(a11) \land $ \\ 
 $ E1G2Inv(a37) \land $ \\ 
 $ E1G2Inv(a91) \land $ \\ 
 $ E1G2Inv(a82) \land $ \\ 
 $ E1G2Inv(a71) \land $ \\ 
 $ E1G2Inv(a3) \land $ \\ 
 $ E1G2Inv(a87) \land $ \\ 
 $ E1G2Inv(a53_a30) \land $ \\ 
 $ E1G2Inv(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $ E1G2Inv(a7) \land $ \\ 
 $ E1G2Inv(a90) \land $ \\ 
 $ E1G2Inv(a10) \land $ \\ 
 $ E1G2Inv(a86_a85) \land $ \\ 
 $ E1G2Inv(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a7) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4Inv(a14) \land $ \\ 
 $  \Rnext E3L0Inv(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2Inv(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext E2L3Inv(a87) \land $ \\ 
 $  \Rnext  \Rnext E2L4Inv(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext C0(a71) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a91) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a98) \land $ \\ 
 $  \Rnext E3L0(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a3) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4Inv(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C4(a91) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2Inv(a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a14) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5(a10) \land $ \\ 
 $  \Rnext C4(a7) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3Inv(a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a90) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4(a14) \land $ \\ 
 $  \Rnext C0(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a14) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a37) \land $ \\ 
 $  \Rnext  \Rnext E2L3(a3) \land $ \\ 
 $  \Rnext  \Rnext E3L2Inv(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5Inv(a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3(a10) \land $ \\ 
 $  \Rnext E3L1Inv(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a38) \land $ \\ 
 $  \Rnext E3L2Inv(a3) \land $ \\ 
 $  \Rnext C1(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a7) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a14) \land $ \\ 
 $  \Rnext  \Rnext E2L5(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2Inv(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2(a90) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a31) \land $ \\ 
 $  \Rnext  \Rnext E2L3Inv(a40) \land $ \\ 
 $  \Rnext E2L3(a82) \land $ \\ 
 $  \Rnext  \Rnext E3L2(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext C3(a82) \land $ \\ 
 $  \Rnext C2(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3Inv(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C4(a71) \land $ \\ 
 $  \Rnext  \Rnext E3L2Inv(a90) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a82) \land $ \\ 
 $  \Rnext  \Rnext E2L3Inv(a14) \land $ \\ 
 $  \Rnext E3L0Inv(a91) \land $ \\ 
 $  \Rnext E3L1Inv(a7) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a38) \land $ \\ 
 $  \Rnext  \Rnext C3(a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2Inv(a87) \land $ \\ 
 $  \Rnext C4(a37) \land $ \\ 
 $  \Rnext  \Rnext E2L3(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4Inv(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C4(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2Inv(a53_a30) \land $ \\ 
 $  \Rnext E3L0(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C4(a38) \land $ \\ 
 $  \Rnext E2L3(a50) \land $ \\ 
 $  \Rnext E3L0(a90) \land $ \\ 
 $  \Rnext E2L3Inv(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C5(a38) \land $ \\ 
 $  \Rnext  \Rnext C0(a3) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a89_a29) \land $ \\ 
 $  \Rnext E2L5(a38) \land $ \\ 
 $  \Rnext  \Rnext C5(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2Inv(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext C4(a31) \land $ \\ 
 $  \Rnext  \Rnext C5(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5Inv(a7) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5Inv(a7) \land $ \\ 
 $  \Rnext C2(a87) \land $ \\ 
 $  \Rnext  \Rnext E2L3(a86_a85) \land $ \\ 
 $  \Rnext E3L1Inv(a14) \land $ \\ 
 $  \Rnext E2L4Inv(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext E3L2Inv(a31) \land $ \\ 
 $  \Rnext E3L0(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a14) \land $ \\ 
 $  \Rnext C4(a91) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3Inv(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5Inv(a38) \land $ \\ 
 $  \Rnext  \Rnext E2L5(a71) \land $ \\ 
 $  \Rnext E3L2(a31) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3(a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3(a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a41) \land $ \\ 
 $  \Rnext C5(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext E2L5(a3) \land $ \\ 
 $  \Rnext E3L1(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a50) \land $ \\ 
 $  \Rnext C4(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3Inv(a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a10) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5(a98) \land $ \\ 
 $  \Rnext E3L1(a87) \land $ \\ 
 $  \Rnext  \Rnext C5(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5Inv(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext C1(a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a50) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a87) \land $ \\ 
 $  \Rnext  \Rnext C2(a14) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a91) \land $ \\ 
 $  \Rnext  \Rnext E2L5Inv(a89_a29) \land $ \\ 
 $  \Rnext C5(a10) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C5(a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a89_a29) \land $ \\ 
 $  \Rnext C5(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext C1(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C4(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext E2L5(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext E2L3(a40) \land $ \\ 
 $  \Rnext E3L0(a38) \land $ \\ 
 $  \Rnext E3L1(a40) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a91) \land $ \\ 
 $  \Rnext C2(a31) \land $ \\ 
 $  \Rnext  \Rnext C4(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4Inv(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2Inv(a7) \land $ \\ 
 $  \Rnext E3L1(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a41) \land $ \\ 
 $  \Rnext  \Rnext E2L4Inv(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4(a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a87) \land $ \\ 
 $  \Rnext E3L2Inv(a53_a30) \land $ \\ 
 $  \Rnext E3L0(a41) \land $ \\ 
 $  \Rnext E3L1(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext E2L3Inv(a31) \land $ \\ 
 $  \Rnext  \Rnext E2L4Inv(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3Inv(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2Inv(a7) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext E3L2Inv(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a10) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a90) \land $ \\ 
 $  \Rnext  \Rnext E2L3(a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5Inv(a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a60) \land $ \\ 
 $  \Rnext E2L4(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5(a90) \land $ \\ 
 $  \Rnext E3L2(a14) \land $ \\ 
 $  \Rnext  \Rnext E3L2Inv(a53_a30) \land $ \\ 
 $  \Rnext E3L2(a91) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3Inv(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4Inv(a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5Inv(a89_a29) \land $ \\ 
 $  \Rnext E3L2Inv(a71) \land $ \\ 
 $ C3(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $ C3(a53_a30) \land $ \\ 
 $ C3(a89_a29) \land $ \\ 
 $ C3(a11) \land $ \\ 
 $ C3(a71) \land $ \\ 
 $ C3(a31) \land $ \\ 
 $ C3(a98) \land $ \\ 
 $ C3(a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5Inv(a40) \land $ \\ 
 $ C3(a86_a85) \land $ \\ 
 $ C3(a7) \land $ \\ 
 $ C3(a63) \land $ \\ 
 $ C3(a40) \land $ \\ 
 $ C3(a50) \land $ \\ 
 $ C3(a87) \land $ \\ 
 $ C3(a91) \land $ \\ 
 $ C3(a90) \land $ \\ 
 $ C3(a37) \land $ \\ 
 $ C3(a38) \land $ \\ 
 $ C3(a60) \land $ \\ 
 $ C3(a14) \land $ \\ 
 $ C3(a3) \land $ \\ 
 $ C3(a10) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2Inv(a63) \land $ \\ 
 $  \Rnext C4(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a10) \land $ \\ 
 $  \Rnext C3(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a90) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a71) \land $ \\ 
 $  \Rnext  \Rnext C5(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C4(a3) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2(a11) \land $ \\ 
 $  \Rnext E2L5Inv(a3) \land $ \\ 
 $  \Rnext E3L0Inv(a10) \land $ \\ 
 $  \Rnext  \Rnext E2L4(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a31) \land $ \\ 
 $  \Rnext  \Rnext C5(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a3) \land $ \\ 
 $  \Rnext  \Rnext E3L2(a98) \land $ \\ 
 $  \Rnext C0(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext E2L5(a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2Inv(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C5(a38) \land $ \\ 
 $ E2L4Inv(a90) \land $ \\ 
 $ E2L4Inv(a53_a30) \land $ \\ 
 $ E2L4Inv(a38) \land $ \\ 
 $ E2L4Inv(a10) \land $ \\ 
 $ E2L4Inv(a11) \land $ \\ 
 $ E2L4Inv(a7) \land $ \\ 
 $ E2L4Inv(a89_a29) \land $ \\ 
 $ E2L4Inv(a71) \land $ \\ 
 $ E2L4Inv(a82) \land $ \\ 
 $ E2L4Inv(a14) \land $ \\ 
 $ E2L4Inv(a63) \land $ \\ 
 $ E2L4Inv(a41) \land $ \\ 
 $ E2L4Inv(a40) \land $ \\ 
 $ E2L4Inv(a50) \land $ \\ 
 $ E2L4Inv(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $ E2L4Inv(a98) \land $ \\ 
 $ E2L4Inv(a37) \land $ \\ 
 $ E2L4Inv(a91) \land $ \\ 
 $ E2L4Inv(a87) \land $ \\ 
 $ E2L4Inv(a86_a85) \land $ \\ 
 $ E2L4Inv(a31) \land $ \\ 
 $ E2L4Inv(a60) \land $ \\ 
 $ E2L4Inv(a3) \land $ \\ 
 $  \Rnext  \Rnext C5(a87) \land $ \\ 
 $  \Rnext E2L4(a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a14) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3Inv(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C5(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4Inv(a63) \land $ \\ 
 $  \Rnext E2L5Inv(a82) \land $ \\ 
 $  \Rnext E3L1Inv(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext C2(a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3Inv(a10) \land $ \\ 
 $  \Rnext C4(a40) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a10) \land $ \\ 
 $  \Rnext E3L0(a86_a85) \land $ \\ 
 $  \Rnext C1(a10) \land $ \\ 
 $  \Rnext  \Rnext E2L4(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3(a98) \land $ \\ 
 $  \Rnext  \Rnext E2L4(a90) \land $ \\ 
 $  \Rnext  \Rnext C4(a14) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a90) \land $ \\ 
 $  \Rnext E2L4(a91) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2Inv(a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a98) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a91) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5(a82) \land $ \\ 
 $  \Rnext E2L5(a63) \land $ \\ 
 $  \Rnext E2L5(a14) \land $ \\ 
 $ E3L1Inv(a89_a29) \land $ \\ 
 $ E3L1Inv(a38) \land $ \\ 
 $ E3L1Inv(a86_a85) \land $ \\ 
 $ E3L1Inv(a71) \land $ \\ 
 $ E3L1Inv(a98) \land $ \\ 
 $  \Rnext E3L1(a60) \land $ \\ 
 $ E3L1Inv(a41) \land $ \\ 
 $ E3L1Inv(a40) \land $ \\ 
 $ E3L1Inv(a63) \land $ \\ 
 $ E3L1Inv(a14) \land $ \\ 
 $ E3L1Inv(a90) \land $ \\ 
 $ E3L1Inv(a3) \land $ \\ 
 $ E3L1Inv(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $ E3L1Inv(a87) \land $ \\ 
 $ E3L1Inv(a10) \land $ \\ 
 $ E3L1Inv(a7) \land $ \\ 
 $ E3L1Inv(a91) \land $ \\ 
 $ E3L1Inv(a53_a30) \land $ \\ 
 $ E3L1Inv(a82) \land $ \\ 
 $ E3L1Inv(a50) \land $ \\ 
 $ E3L1Inv(a31) \land $ \\ 
 $ E3L1Inv(a11) \land $ \\ 
 $ E3L1Inv(a60) \land $ \\ 
 $ E3L1Inv(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C4(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5Inv(a50) \land $ \\ 
 $  \Rnext C3(a71) \land $ \\ 
 $  \Rnext E3L1(a3) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a7) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3Inv(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext C1(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4(a86_a85) \land $ \\ 
 $  \Rnext E3L2(a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a40) \land $ \\ 
 $  \Rnext  \Rnext E3L2Inv(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C5(a71) \land $ \\ 
 $  \Rnext C3(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C4(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext E2L4Inv(a10) \land $ \\ 
 $  \Rnext  \Rnext C1(a40) \land $ \\ 
 $  \Rnext  \Rnext E2L4Inv(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a60) \land $ \\ 
 $  \Rnext E2L3Inv(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a10) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5(a41) \land $ \\ 
 $  \Rnext C3(a7) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5Inv(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5(a7) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a91) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C4(a60) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a41) \land $ \\ 
 $  \Rnext E2L4Inv(a7) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a89_a29) \land $ \\ 
 $  \Rnext E2L5(a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a71) \land $ \\ 
 $  \Rnext E2L4Inv(a60) \land $ \\ 
 $  \Rnext E3L0Inv(a3) \land $ \\ 
 $  \Rnext  \Rnext C3(a50) \land $ \\ 
 $  \Rnext E2L4Inv(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext E3L2(a7) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a7) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3(a98) \land $ \\ 
 $  \Rnext E3L2Inv(a50) \land $ \\ 
 $  \Rnext E2L4(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4Inv(a7) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext E2L5(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4(a87) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3(a11) \land $ \\ 
 $  \Rnext E3L2(a50) \land $ \\ 
 $  \Rnext C4(a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a41) \land $ \\ 
 $  \Rnext E3L2Inv(a11) \land $ \\ 
 $  \Rnext E2L5Inv(a7) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5Inv(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext C1(a31) \land $ \\ 
 $  \Rnext  \Rnext E2L5Inv(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5(a11) \land $ \\ 
 $  \Rnext E3L2(a3) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a3) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C5(a10) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4Inv(a14) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4Inv(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2Inv(a38) \land $ \\ 
 $  \Rnext E3L2Inv(a91) \land $ \\ 
 $  \Rnext E3L2(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext E2L4(a3) \land $ \\ 
 $  \Rnext  \Rnext E3L2(a37) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5(a87) \land $ \\ 
 $  \Rnext  \Rnext E2L4(a14) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a14) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a37) \land $ \\ 
 $  \Rnext E3L0Inv(a31) \land $ \\ 
 $  \Rnext  \Rnext C2(a90) \land $ \\ 
 $  \Rnext C0(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2Inv(a10) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C4(a3) \land $ \\ 
 $  \Rnext  \Rnext C2(a86_a85) \land $ \\ 
 $  \Rnext C2(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext E3L2(a40) \land $ \\ 
 $  \Rnext E3L2(a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4Inv(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a53_a30) \land $ \\ 
 $  \Rnext E3L0Inv(a7) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a98) \land $ \\ 
 $ E2L5(a53_a30) \land $ \\ 
 $ E2L5(a90) \land $ \\ 
 $ E2L5(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext E2L4(a89_a29) \land $ \\ 
 $ E2L5(a7) \land $ \\ 
 $ E2L5(a87) \land $ \\ 
 $ E2L5(a14) \land $ \\ 
 $ E2L5(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $ E2L5(a3) \land $ \\ 
 $ E2L5(a98) \land $ \\ 
 $ E2L5(a41) \land $ \\ 
 $ E2L5(a10) \land $ \\ 
 $ E2L5(a60) \land $ \\ 
 $ E2L5(a71) \land $ \\ 
 $ E2L5(a50) \land $ \\ 
 $ E2L5(a40) \land $ \\ 
 $ E2L5(a37) \land $ \\ 
 $ E2L5(a38) \land $ \\ 
 $ E2L5(a63) \land $ \\ 
 $ E2L5(a91) \land $ \\ 
 $ E2L5(a31) \land $ \\ 
 $ E2L5(a82) \land $ \\ 
 $ E2L5(a11) \land $ \\ 
 $ E2L5(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3Inv(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a7) \land $ \\ 
 $  \Rnext  \Rnext E2L3(a91) \land $ \\ 
 $  \Rnext C5(a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a3) \land $ \\ 
 $  \Rnext E2L5Inv(a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2(a63) \land $ \\ 
 $  \Rnext C3(a3) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a89_a29) \land $ \\ 
 $  \Rnext C2(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2Inv(a98) \land $ \\ 
 $  \Rnext C3(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4Inv(a41) \land $ \\ 
 $  \Rnext  \Rnext E3L2Inv(a87) \land $ \\ 
 $  \Rnext E2L4(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext C2(a91) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3Inv(a91) \land $ \\ 
 $  \Rnext E3L2Inv(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2(a7) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4(a41) \land $ \\ 
 $  \Rnext C2(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4(a71) \land $ \\ 
 $  \Rnext  \Rnext E2L3(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3Inv(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a40) \land $ \\ 
 $  \Rnext C0(a63) \land $ \\ 
 $  \Rnext  \Rnext E2L3(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4Inv(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a10) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C5(a31) \land $ \\ 
 $  \Rnext E2L3Inv(a31) \land $ \\ 
 $  \Rnext C3(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4Inv(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4(a10) \land $ \\ 
 $  \Rnext  \Rnext C0(a89_a29) \land $ \\ 
 $  \Rnext E2L5Inv(a11) \land $ \\ 
 $  \Rnext  \Rnext E3L2(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5Inv(a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a90) \land $ \\ 
 $  \Rnext  \Rnext E2L4(a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a90) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3Inv(a89_a29) \land $ \\ 
 $  \Rnext E3L2(a90) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5Inv(a91) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2(a50) \land $ \\ 
 $  \Rnext  \Rnext C0(a50) \land $ \\ 
 $  \Rnext  \Rnext C2(a40) \land $ \\ 
 $  \Rnext C0(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5Inv(a3) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4Inv(a87) \land $ \\ 
 $  \Rnext  \Rnext E2L5(a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a82) \land $ \\ 
 $  \Rnext C5(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C4(a10) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3Inv(a10) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a31) \land $ \\ 
 $ E1G5Inv(a82) \land $ \\ 
 $ E1G5Inv(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4Inv(a38) \land $ \\ 
 $ E1G5Inv(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $ E1G5Inv(a63) \land $ \\ 
 $ E1G5Inv(a14) \land $ \\ 
 $ E1G5Inv(a11) \land $ \\ 
 $ E1G5Inv(a41) \land $ \\ 
 $ E1G5Inv(a40) \land $ \\ 
 $ E1G5Inv(a3) \land $ \\ 
 $ E1G5Inv(a87) \land $ \\ 
 $ E1G5Inv(a50) \land $ \\ 
 $ E1G5Inv(a71) \land $ \\ 
 $ E1G5Inv(a53_a30) \land $ \\ 
 $ E1G5Inv(a86_a85) \land $ \\ 
 $ E1G5Inv(a7) \land $ \\ 
 $ E1G5Inv(a38) \land $ \\ 
 $ E1G5Inv(a10) \land $ \\ 
 $ E1G5Inv(a98) \land $ \\ 
 $ E1G5Inv(a91) \land $ \\ 
 $ E1G5Inv(a31) \land $ \\ 
 $ E1G5Inv(a90) \land $ \\ 
 $ E1G5Inv(a37) \land $ \\ 
 $ E1G5Inv(a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a71) \land $ \\ 
 $  \Rnext  \Rnext C0(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext C5(a82) \land $ \\ 
 $  \Rnext E2L5Inv(a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C4(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C4(a14) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3(a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a53_a30) \land $ \\ 
 $  \Rnext E2L5Inv(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5Inv(a90) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3(a82) \land $ \\ 
 $  \Rnext  \Rnext E2L3(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4(a31) \land $ \\ 
 $  \Rnext E3L0(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C5(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4Inv(a31) \land $ \\ 
 $  \Rnext C0(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C5(a40) \land $ \\ 
 $  \Rnext  \Rnext E3L2Inv(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a91) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a98) \land $ \\ 
 $  \Rnext  \Rnext E3L2(a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext E2L3Inv(a11) \land $ \\ 
 $  \Rnext E2L4Inv(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a14) \land $ \\ 
 $  \Rnext  \Rnext C1(a10) \land $ \\ 
 $  \Rnext C1(a89_a29) \land $ \\ 
 $  \Rnext E2L4Inv(a71) \land $ \\ 
 $  \Rnext  \Rnext E2L3Inv(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext E2L5(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5Inv(a37) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3(a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a38) \land $ \\ 
 $  \Rnext  \Rnext E2L4(a91) \land $ \\ 
 $  \Rnext  \Rnext C4(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext E3L2(a38) \land $ \\ 
 $  \Rnext C3(a31) \land $ \\ 
 $  \Rnext  \Rnext E2L5Inv(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C4(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2(a7) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4Inv(a7) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a91) \land $ \\ 
 $  \Rnext C4(a10) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a7) \land $ \\ 
 $  \Rnext C5(a63) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a90) \land $ \\ 
 $  \Rnext E2L5Inv(a60) \land $ \\ 
 $  \Rnext  \Rnext C4(a90) \land $ \\ 
 $  \Rnext E2L3Inv(a87) \land $ \\ 
 $  \Rnext C1(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4Inv(a40) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a87) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a3) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3(a31) \land $ \\ 
 $  \Rnext E2L4(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a37) \land $ \\ 
 $  \Rnext E2L3(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C5(a60) \land $ \\ 
 $  \Rnext C2(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a11) \land $ \\ 
 $  \Rnext E2L3(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3(a38) \land $ \\ 
 $  \Rnext E2L5Inv(a71) \land $ \\ 
 $  \Rnext E3L0Inv(a41) \land $ \\ 
 $  \Rnext E2L3(a98) \land $ \\ 
 $ E3G1(a90) \land $ \\ 
 $ E3G1(a41) \land $ \\ 
 $ E3G1(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $ E3G1(a89_a29) \land $ \\ 
 $ E3G1(a82) \land $ \\ 
 $ E3G1(a7) \land $ \\ 
 $ E3G1(a37) \land $ \\ 
 $ E3G1(a31) \land $ \\ 
 $ E3G1(a91) \land $ \\ 
 $ E3G1(a3) \land $ \\ 
 $ E3G1(a10) \land $ \\ 
 $ E3G1(a98) \land $ \\ 
 $ E3G1(a60) \land $ \\ 
 $ E3G1(a40) \land $ \\ 
 $ E3G1(a14) \land $ \\ 
 $ E3G1(a86_a85) \land $ \\ 
 $ E3G1(a53_a30) \land $ \\ 
 $ E3G1(a50) \land $ \\ 
 $ E3G1(a63) \land $ \\ 
 $ E3G1(a87) \land $ \\ 
 $ E3G1(a38) \land $ \\ 
 $ E3G1(a11) \land $ \\ 
 $ E3G1(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext E2L5(a3) \land $ \\ 
 $  \Rnext  \Rnext C3(a11) \land $ \\ 
 $ E2G3(a40) \land $ \\ 
 $ E2G3(a89_a29) \land $ \\ 
 $ E2G3(a10) \land $ \\ 
 $ E2G3(a7) \land $ \\ 
 $ E2G3(a53_a30) \land $ \\ 
 $ E2G3(a63) \land $ \\ 
 $ E2G3(a38) \land $ \\ 
 $ E2G3(a31) \land $ \\ 
 $ E2G3(a82) \land $ \\ 
 $ E2G3(a98) \land $ \\ 
 $ E2G3(a50) \land $ \\ 
 $ E2G3(a60) \land $ \\ 
 $ E2G3(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $ E2G3(a41) \land $ \\ 
 $ E2G3(a90) \land $ \\ 
 $ E2G3(a3) \land $ \\ 
 $ E2G3(a87) \land $ \\ 
 $ E2G3(a71) \land $ \\ 
 $ E2G3(a11) \land $ \\ 
 $ E2G3(a14) \land $ \\ 
 $ E2G3(a37) \land $ \\ 
 $ E2G3(a86_a85) \land $ \\ 
 $ E2G3(a91) \land $ \\ 
 $  \Rnext  \Rnext E2L5(a98) \land $ \\ 
 $  \Rnext  \Rnext E3L2(a3) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4(a7) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a90) \land $ \\ 
 $  \Rnext E2L4(a38) \land $ \\ 
 $  \Rnext  \Rnext E2L5(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3Inv(a82) \land $ \\ 
 $  \Rnext  \Rnext E2L4Inv(a63) \land $ \\ 
 $  \Rnext E3L0(a14) \land $ \\ 
 $  \Rnext E2L3Inv(a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2(a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4(a38) \land $ \\ 
 $  \Rnext  \Rnext C5(a7) \land $ \\ 
 $  \Rnext  \Rnext E2L5(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a90) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5(a87) \land $ \\ 
 $  \Rnext  \Rnext E3L2(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a3) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4(a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a7) \land $ \\ 
 $  \Rnext  \Rnext C1(a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C5(a50) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a3) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2Inv(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2Inv(a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4Inv(a91) \land $ \\ 
 $  \Rnext  \Rnext E2L3(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext C1(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C5(a10) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a91) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2Inv(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2(a40) \land $ \\ 
 $  \Rnext  \Rnext C0(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a3) \land $ \\ 
 $  \Rnext E3L1Inv(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3(a86_a85) \land $ \\ 
 $  \Rnext C2(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext C1(a38) \land $ \\ 
 $  \Rnext  \Rnext E2L3Inv(a63) \land $ \\ 
 $  \Rnext C4(a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext E2L5(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext E3L0Inv(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext E2L5Inv(a3) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2(a40) \land $ \\ 
 $  \Rnext E3L1(a91) \land $ \\ 
 $  \Rnext C5(a3) \land $ \\ 
 $  \Rnext  \Rnext C2(a37) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a14) \land $ \\ 
 $  \Rnext E3L1Inv(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5(a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a11) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a14) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a50) \land $ \\ 
 $  \Rnext E3L1Inv(a10) \land $ \\ 
 $  \Rnext C0(a90) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4(a14) \land $ \\ 
 $  \Rnext  \Rnext E2L4(a31) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a63) \land $ \\ 
 $  \Rnext  \Rnext C4(a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4Inv(a50) \land $ \\ 
 $  \Rnext E3L1(a71) \land $ \\ 
 $  \Rnext  \Rnext C3(a7) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3Inv(a7) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a40) \land $ \\ 
 $  \Rnext E3L1Inv(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a98) \land $ \\ 
 $  \Rnext C4(a11) \land $ \\ 
 $  \Rnext  \Rnext C2(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a86_a85) \land $ \\ 
 $ C4(a3) \land $ \\ 
 $ C4(a41) \land $ \\ 
 $ C4(a38) \land $ \\ 
 $ C4(a89_a29) \land $ \\ 
 $ C4(a31) \land $ \\ 
 $ C4(a91) \land $ \\ 
 $ C4(a40) \land $ \\ 
 $ C4(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext C4(a3) \land $ \\ 
 $ C4(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $ C4(a63) \land $ \\ 
 $ C4(a60) \land $ \\ 
 $ C4(a87) \land $ \\ 
 $ C4(a86_a85) \land $ \\ 
 $ C4(a50) \land $ \\ 
 $ C4(a90) \land $ \\ 
 $ C4(a71) \land $ \\ 
 $ C4(a82) \land $ \\ 
 $ C4(a7) \land $ \\ 
 $ C4(a10) \land $ \\ 
 $ C4(a11) \land $ \\ 
 $ C4(a14) \land $ \\ 
 $ C4(a98) \land $ \\ 
 $ C4(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C4(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5Inv(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C5(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a11) \land $ \\ 
 $  \Rnext  \Rnext E2L5(a82) \land $ \\ 
 $  \Rnext  \Rnext E2L5Inv(a38) \land $ \\ 
 $  \Rnext C5(a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4(a53_a30) \land $ \\ 
 $  \Rnext E3L1Inv(a11) \land $ \\ 
 $  \Rnext C1(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a10) \land $ \\ 
 $  \Rnext E3L2Inv(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext E3L1(a63) \land $ \\ 
 $  \Rnext E3L0Inv(a14) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a7) \land $ \\ 
 $  \Rnext E3L2Inv(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2(a90) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5Inv(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a87) \land $ \\ 
 $  \Rnext  \Rnext C3(a14) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C4(a7) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5(a3) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a82) \land $ \\ 
 $  \Rnext  \Rnext E2L3Inv(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2Inv(a63) \land $ \\ 
 $  \Rnext C3(a50) \land $ \\ 
 $  \Rnext  \Rnext E2L4(a98) \land $ \\ 
 $  \Rnext E2L5(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4(a90) \land $ \\ 
 $  \Rnext C5(a31) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a7) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a3) \land $ \\ 
 $  \Rnext  \Rnext E2L3(a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4Inv(a10) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a98) \land $ \\ 
 $  \Rnext E2L4Inv(a31) \land $ \\ 
 $  \Rnext  \Rnext E3L2(a90) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4(a60) \land $ \\ 
 $  \Rnext E2L5(a91) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2(a60) \land $ \\ 
 $  \Rnext E2L3(a10) \land $ \\ 
 $  \Rnext C4(a90) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4Inv(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C3(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a53_a30) \land $ \\ 
 $  \Rnext E2L3(a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4Inv(a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4Inv(a82) \land $ \\ 
 $  \Rnext E2L5(a31) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext C2(a3) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2(a91) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4Inv(a90) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a87) \land $ \\ 
 $  \Rnext E3L0Inv(a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2(a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2Inv(a91) \land $ \\ 
 $  \Rnext E2L3Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a37) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a60) \land $ \\ 
 $  \Rnext E3L0Inv(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3(a91) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4(a41) \land $ \\ 
 $ E1G0Inv(a89_a29) \land $ \\ 
 $ E1G0Inv(a90) \land $ \\ 
 $ E1G0Inv(a60) \land $ \\ 
 $ E1G0Inv(a41) \land $ \\ 
 $ E1G0Inv(a7) \land $ \\ 
 $ E1G0Inv(a71) \land $ \\ 
 $ E1G0Inv(a63) \land $ \\ 
 $ E1G0Inv(a91) \land $ \\ 
 $ E1G0Inv(a31) \land $ \\ 
 $ E1G0Inv(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $ E1G0Inv(a82) \land $ \\ 
 $ E1G0Inv(a98) \land $ \\ 
 $ E1G0Inv(a40) \land $ \\ 
 $ E1G0Inv(a10) \land $ \\ 
 $ E1G0Inv(a3) \land $ \\ 
 $ E1G0Inv(a37) \land $ \\ 
 $ E1G0Inv(a87) \land $ \\ 
 $ E1G0Inv(a11) \land $ \\ 
 $ E1G0Inv(a50) \land $ \\ 
 $ E1G0Inv(a53_a30) \land $ \\ 
 $ E1G0Inv(a14) \land $ \\ 
 $ E1G0Inv(a38) \land $ \\ 
 $ E1G0Inv(a86_a85) \land $ \\ 
 $  \Rnext E3L0Inv(a90) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5(a60) \land $ \\ 
 $  \Rnext  \Rnext E2L3(a7) \land $ \\ 
 $  \Rnext  \Rnext E2L3Inv(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a98) \land $ \\ 
 $  \Rnext  \Rnext C3(a38) \land $ \\ 
 $  \Rnext C1(a63) \land $ \\ 
 $  \Rnext  \Rnext C1(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a60) \land $ \\ 
 $  \Rnext  \Rnext E2L4(a87) \land $ \\ 
 $  \Rnext C0(a91) \land $ \\ 
 $  \Rnext  \Rnext E2L3Inv(a90) \land $ \\ 
 $  \Rnext  \Rnext E2L4Inv(a98) \land $ \\ 
 $  \Rnext  \Rnext C0(a91) \land $ \\ 
 $  \Rnext  \Rnext C2(a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C5(a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2Inv(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a41) \land $ \\ 
 $  \Rnext  \Rnext E2L4(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3Inv(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5Inv(a11) \land $ \\ 
 $  \Rnext  \Rnext C2(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a82) \land $ \\ 
 $  \Rnext E2L3(a7) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a86_a85) \land $ \\ 
 $  \Rnext C3(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C4(a7) \land $ \\ 
 $ C0(a63) \land $ \\ 
 $ C0(a41) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a90) \land $ \\ 
 $ C0(a89_a29) \land $ \\ 
 $ C0(a10) \land $ \\ 
 $ C0(a91) \land $ \\ 
 $ C0(a98) \land $ \\ 
 $ C0(a40) \land $ \\ 
 $ C0(a82) \land $ \\ 
 $ C0(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $ C0(a3) \land $ \\ 
 $ C0(a53_a30) \land $ \\ 
 $ C0(a7) \land $ \\ 
 $ C0(a86_a85) \land $ \\ 
 $ C0(a11) \land $ \\ 
 $ C0(a71) \land $ \\ 
 $ C0(a31) \land $ \\ 
 $ C0(a87) \land $ \\ 
 $ C0(a60) \land $ \\ 
 $ C0(a37) \land $ \\ 
 $ C0(a50) \land $ \\ 
 $ C0(a14) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a14) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5Inv(a40) \land $ \\ 
 $  \Rnext C1(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C5(a98) \land $ \\ 
 $  \Rnext  \Rnext C2(a87) \land $ \\ 
 $  \Rnext  \Rnext E2L4(a7) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3(a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a87) \land $ \\ 
 $  \Rnext  \Rnext E3L2(a11) \land $ \\ 
 $  \Rnext  \Rnext C3(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext C1(a91) \land $ \\ 
 $  \Rnext  \Rnext E2L3(a14) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a87) \land $ \\ 
 $  \Rnext  \Rnext C5(a38) \land $ \\ 
 $  \Rnext  \Rnext E2L4Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a38) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a89_a29) \land $ \\ 
 $  \Rnext C2(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext E2L5(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3Inv(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a3) \land $ \\ 
 $  \Rnext C2(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2(a71) \land $ \\ 
 $  \Rnext E3L0(a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3Inv(a40) \land $ \\ 
 $  \Rnext C1(a98) \land $ \\ 
 $  \Rnext C2(a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a10) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3Inv(a60) \land $ \\ 
 $  \Rnext E3L1(a90) \land $ \\ 
 $  \Rnext E2L3Inv(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2Inv(a90) \land $ \\ 
 $  \Rnext  \Rnext E2L5(a10) \land $ \\ 
 $  \Rnext  \Rnext E3L2(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L4Inv(a71) \land $ \\ 
 $  \Rnext E3L2(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext C1(a87) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a10) \land $ \\ 
 $  \Rnext  \Rnext E2L3(a10) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a91) \land $ \\ 
 $  \Rnext  \Rnext E2L5Inv(a82) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L2Inv(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a53_a30) \land $ \\ 
 $ E3L0(a89_a29) \land $ \\ 
 $ E3L0(a41) \land $ \\ 
 $ E3L0(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $ E3L0(a91) \land $ \\ 
 $ E3L0(a50) \land $ \\ 
 $ E3L0(a31) \land $ \\ 
 $ E3L0(a40) \land $ \\ 
 $ E3L0(a7) \land $ \\ 
 $ E3L0(a90) \land $ \\ 
 $ E3L0(a37) \land $ \\ 
 $ E3L0(a53_a30) \land $ \\ 
 $ E3L0(a14) \land $ \\ 
 $ E3L0(a86_a85) \land $ \\ 
 $ E3L0(a82) \land $ \\ 
 $ E3L0(a10) \land $ \\ 
 $ E3L0(a3) \land $ \\ 
 $ E3L0(a98) \land $ \\ 
 $ E3L0(a11) \land $ \\ 
 $ E3L0(a71) \land $ \\ 
 $ E3L0(a38) \land $ \\ 
 $ E3L0(a63) \land $ \\ 
 $ E3L0(a87) \land $ \\ 
 $ E3L0(a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C5(a14) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C5(a90) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4(a90) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5Inv(a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C2(a14) \land $ \\ 
 $  \Rnext  \Rnext C0(a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a87) \land $ \\ 
 $  \Rnext E3L2Inv(a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a91) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5(a40) \land $ \\ 
 $  \Rnext E3L1Inv(a91) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a14) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3(a71) \land $ \\ 
 $  \Rnext E3L1Inv(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C5(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a31) \land $ \\ 
 $  \Rnext E3L0Inv(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a90) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C4(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C2(a3) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L5Inv(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C5(a53_a30) \land $ \\ 
 $  \Rnext E3L1Inv(a86_a85) \land $ \\ 
 $  \Rnext C2(a14) \land $ \\ 
 $  \Rnext  \Rnext E2L5Inv(a86_a85) \land $ \\ 
 $  \Rnext  \Rnext E2L5Inv(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L2Inv(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C4(a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C5(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a71) \land $ \\ 
 $  \Rnext  \Rnext C5(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a3) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C4(a11) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2L3Inv(a86_a85) \land $ \\ 
 $  \Rnext C1(a41) \land $ \\ 
 $  \Rnext E2L3(a89_a29) \land $ \\ 
 $  \Rnext  \Rnext E2L5(a7) \land $ \\ 
 $  \Rnext E3L1Inv(a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a63) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a82) \land $ \\ 
 $  \Rnext  \Rnext C0(a82) \land $ \\ 
 $  \Rnext  \Rnext E3L2(a77_a33_a76_a32_a79_a35_a78_a34_a36_a39_a80_a81_a84_a83_a42_a88_a44_a43_a46_a45_a48_a47_a49_a93_a92_a95_a51_a94_a97_a96_a52_a99_a55_a54_a13_a57_a12_a56_a15_a59_a58_a17_a16_a19_a18_a100_a62_a61_a20_a64_a22_a66_a21_a65_a24_a68_a23_a67_a26_a25_a69_a28_a27_a1_a2_a4_a5_a6_a8_a9_a70_a73_a72_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L3(a53_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C3(a3) \land $ \\ 
 $  \Rnext E2L5(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a10) \land $ \\ 
 $  \Rnext C4(a82) \land $ \\ 
 $  \Rnext C0(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L4Inv(a63) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a10) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2L5(a53_a30) \land $ \\ 
 $  \Rnext E3L1Inv(a3))$ 
\end{document}