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


$((PinvL0 \rightarrow E1L0(dL0)) \land $ \\ 
 $ (PinvL1 \rightarrow E1L1(dL1)) \land $ \\ 
 $  \forall X. ( \Rbox ((( \Rnext E2L1(X) \land $ \\ 
 $  \Rdiamond C1(X)) \rightarrow  \Rdiamond (E3L1(X) \land $ \\ 
 $  \Rdiamond E2G0(X))) \land $ \\ 
 $ ( \Rbox (E2G0(X) \land $ \\ 
 $  \Rnext C1(X)) \rightarrow  \Rbox (C1(X) \land $ \\ 
 $  \Rbox E3G0(X))) \land $ \\ 
 $ ( \Rdiamond (E3G0(X) \land $ \\ 
 $  \Rnext C1(X)) \rightarrow  \Rbox  \Rdiamond (E3G0(X) \land $ \\ 
 $ C1(X))) \land $ \\ 
 $ ( \Rbox (C0(X) \land $ \\ 
 $  \Rbox E1G1(X)) \rightarrow (C0(X) \land $ \\ 
 $  \Rbox  \Rnext E3L1(X))) \land $ \\ 
 $ ((C1(X) \land $ \\ 
 $  \Rbox  \Rnext E2L0(X)) \rightarrow ( \Rbox C0(X) \land $ \\ 
 $  \Rnext E1G1(X))) \land $ \\ 
 $ ( \Rdiamond  \Rdiamond (C0(X) \land $ \\ 
 $ E2L0(X)) \rightarrow  \Rbox  \Rbox  \Rbox  \Rnext C1(X)) \land $ \\ 
 $ (( \Rbox E3G0(X) \land $ \\ 
 $  \Rbox E3G1(X)) \rightarrow  \Rdiamond (E3L0(X) \land $ \\ 
 $  \Rbox E1L0(X))) \land $ \\ 
 $ ( \Rdiamond  \Rdiamond  \Rdiamond  \Rdiamond E1L0(X) \rightarrow ( \Rnext E1L0(X) \land $ \\ 
 $  \Rbox E3G1(X))) \land $ \\ 
 $ ( \Rbox  \Rdiamond  \Rdiamond  \Rnext C1(X) \rightarrow  \Rbox  \Rdiamond (E2L1(X) \land $ \\ 
 $ C0(X))) \land $ \\ 
 $ (( \Rnext C0(X) \land $ \\ 
 $  \Rbox C0(X)) \rightarrow ( \Rbox C1(X) \land $ \\ 
 $  \Rdiamond E2G0(X))) \land $ \\ 
 $ (E2L0(X) \rightarrow E1L0(X)) \land $ \\ 
 $ (E3L1(X) \rightarrow E2L1(X)) \land $ \\ 
 $ (E3L0(X) \rightarrow E2L0(X)) \land $ \\ 
 $ (E3G1(X) \rightarrow E1G1(X)) \land $ \\ 
 $ (E2L1(X) \rightarrow E1L1(X)) \land $ \\ 
 $ (E3G0(X) \rightarrow E2G0(X)) \land $ \\ 
 $ (E2G0(X) \rightarrow E1G0(X))) \land $ \\ 
 $ ( \Rdiamond E1L0Inv(X) \rightarrow  \Rbox PinvL0) \land $ \\ 
 $ ( \Rdiamond E2G0(X) \rightarrow  \Rbox E2G0(X)) \land $ \\ 
 $ ( \Rdiamond E1G0(X) \rightarrow  \Rbox PG0) \land $ \\ 
 $ ( \Rdiamond E1G1Inv(X) \rightarrow  \Rbox PinvG1) \land $ \\ 
 $ ( \Rdiamond E1G1(X) \rightarrow  \Rbox E1G1(X)) \land $ \\ 
 $ ( \Rdiamond E1L1Inv(X) \rightarrow  \Rbox PinvL1) \land $ \\ 
 $ ( \Rdiamond E1G0(X) \rightarrow  \Rbox E1G0(X)) \land $ \\ 
 $ ( \Rdiamond E1G0Inv(X) \rightarrow  \Rbox E1G0Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1G1Inv(X) \rightarrow  \Rbox E1G1Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1L1(X) \rightarrow  \Rbox PL1) \land $ \\ 
 $ ( \Rdiamond E1G1(X) \rightarrow  \Rbox PG1) \land $ \\ 
 $ ( \Rdiamond E3G0(X) \rightarrow  \Rbox E3G0(X)) \land $ \\ 
 $ ( \Rdiamond E1L0(X) \rightarrow  \Rbox PL0) \land $ \\ 
 $ ( \Rdiamond E3G1(X) \rightarrow  \Rbox E3G1(X)) \land $ \\ 
 $ ( \Rdiamond E1G0Inv(X) \rightarrow  \Rbox PinvG0)) \land $ \\ 
 $ (PL1 \rightarrow E1L1Inv(dL1Inv)) \land $ \\ 
 $ (PinvG1 \rightarrow E1G1(dG1)) \land $ \\ 
 $ (PinvG0 \rightarrow E1G0(dG0)) \land $ \\ 
 $ (PL0 \rightarrow E1L0Inv(dL0Inv)) \land $ \\ 
 $ (PG1 \rightarrow E1G1Inv(dG1Inv)) \land $ \\ 
 $ (PG0 \rightarrow E1G0Inv(dG0Inv)) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a55_a45_a27_a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a88_a61) \land $ \\ 
 $  \Rnext C1(a55_a45_a27_a38) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a88_a61) \land $ \\ 
 $  \Rnext E3L0(a79_a34_a15_a69_a40) \land $ \\ 
 $  \Rnext  \Rnext C0(a83) \land $ \\ 
 $  \Rnext  \Rnext C1(a88_a61) \land $ \\ 
 $  \Rnext  \Rnext C1(a86) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a77_a22_a32_a54_a46_a68_a23_a67_a37_a16_a7_a8_a91_a9_a82_a81_a84_a100_a62_a20_a64_a41_a63_a74) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a87_a14_a49) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a26) \land $ \\ 
 $  \Rnext E3L0Inv(a65) \land $ \\ 
 $  \Rnext E3L1Inv(a11_a43) \land $ \\ 
 $  \Rnext C1(a11_a43) \land $ \\ 
 $  \Rnext E3L1(a25_a85_a30) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a17) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a66) \land $ \\ 
 $  \Rnext E3L0Inv(a4_a36) \land $ \\ 
 $  \Rnext E3L0(a12) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a80_a29_a95_a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a71) \land $ \\ 
 $  \Rnext C1(a57) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a58) \land $ \\ 
 $  \Rnext  \Rnext C1(a39) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a70) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a50) \land $ \\ 
 $  \Rnext  \Rnext C1(a89) \land $ \\ 
 $  \Rnext C1(a13) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a4_a36) \land $ \\ 
 $  \Rnext E3L0(a99) \land $ \\ 
 $  \Rnext  \Rnext C0(a88_a61) \land $ \\ 
 $  \Rnext E3L0(a13) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a2_a90) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a94_a53) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a59) \land $ \\ 
 $  \Rnext C1(a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a89) \land $ \\ 
 $  \Rnext E3L0(a39) \land $ \\ 
 $  \Rnext C0(a77_a22_a32_a54_a46_a68_a23_a67_a37_a16_a7_a8_a91_a9_a82_a81_a84_a100_a62_a20_a64_a41_a63_a74) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a94_a53) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a10_a52) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a72) \land $ \\ 
 $  \Rnext C1(a12) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a42) \land $ \\ 
 $  \Rnext E3L0Inv(a2_a90) \land $ \\ 
 $  \Rnext E3L0Inv(a39) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a57) \land $ \\ 
 $  \Rnext C1(a86) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a76_a6_a92) \land $ \\ 
 $  \Rnext E3L1(a66) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a98) \land $ \\ 
 $  \Rnext E3L1Inv(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a47) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a71) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a1) \land $ \\ 
 $  \Rnext C1(a47) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a17) \land $ \\ 
 $  \Rnext E3L0(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a10_a52) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a47) \land $ \\ 
 $  \Rnext E3L0(a42) \land $ \\ 
 $  \Rnext E3L1(a51) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a86) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a21) \land $ \\ 
 $  \Rnext C0(a13) \land $ \\ 
 $  \Rnext E3L0Inv(a35) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a2_a90) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a2_a90) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a51) \land $ \\ 
 $ E1G1Inv(a12) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a58) \land $ \\ 
 $ E1G1Inv(a88_a61) \land $ \\ 
 $ E1G1Inv(a89) \land $ \\ 
 $ E1G1Inv(a10_a52) \land $ \\ 
 $ E1G1Inv(a70) \land $ \\ 
 $ E1G1Inv(a66) \land $ \\ 
 $ E1G1Inv(a35) \land $ \\ 
 $ E1G1Inv(a39) \land $ \\ 
 $ E1G1Inv(a58) \land $ \\ 
 $ E1G1Inv(a4_a36) \land $ \\ 
 $ E1G1Inv(a18) \land $ \\ 
 $ E1G1Inv(a56) \land $ \\ 
 $ E1G1Inv(a76_a6_a92) \land $ \\ 
 $ E1G1Inv(a13) \land $ \\ 
 $ E1G1Inv(a98) \land $ \\ 
 $ E1G1Inv(a42) \land $ \\ 
 $ E1G1Inv(a1) \land $ \\ 
 $ E1G1Inv(a65) \land $ \\ 
 $ E1G1Inv(a48) \land $ \\ 
 $ E1G1Inv(a94_a53) \land $ \\ 
 $ E1G1Inv(a59) \land $ \\ 
 $ E1G1Inv(a17) \land $ \\ 
 $ E1G1Inv(a72) \land $ \\ 
 $ E1G1Inv(a78_a96) \land $ \\ 
 $ E1G1Inv(a11_a43) \land $ \\ 
 $ E1G1Inv(a99) \land $ \\ 
 $ E1G1Inv(a86) \land $ \\ 
 $ E1G1Inv(a87_a14_a49) \land $ \\ 
 $ E1G1Inv(a50) \land $ \\ 
 $ E1G1Inv(a28) \land $ \\ 
 $ E1G1Inv(a71) \land $ \\ 
 $ E1G1Inv(a26) \land $ \\ 
 $ E1G1Inv(a25_a85_a30) \land $ \\ 
 $ E1G1Inv(a77_a22_a32_a54_a46_a68_a23_a67_a37_a16_a7_a8_a91_a9_a82_a81_a84_a100_a62_a20_a64_a41_a63_a74) \land $ \\ 
 $ E1G1Inv(a24_a5) \land $ \\ 
 $ E1G1Inv(a79_a34_a15_a69_a40) \land $ \\ 
 $ E1G1Inv(a57) \land $ \\ 
 $ E1G1Inv(a51) \land $ \\ 
 $ E1G1Inv(a21) \land $ \\ 
 $ E1G1Inv(a3) \land $ \\ 
 $ E1G1Inv(a19_a97_a75) \land $ \\ 
 $ E1G1Inv(a55_a45_a27_a38) \land $ \\ 
 $ E1G1Inv(a2_a90) \land $ \\ 
 $ E1G1Inv(a83) \land $ \\ 
 $ E1G1Inv(a31) \land $ \\ 
 $ E1G1Inv(a93) \land $ \\ 
 $ E1G1Inv(a47) \land $ \\ 
 $ E1G1Inv(a80_a29_a95_a73) \land $ \\ 
 $ E1G1Inv(a33_a44_a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a80_a29_a95_a73) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a28) \land $ \\ 
 $  \Rnext  \Rnext C1(a25_a85_a30) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a4_a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a2_a90) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a99) \land $ \\ 
 $  \Rnext E3L0Inv(a88_a61) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a66) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a2_a90) \land $ \\ 
 $  \Rnext E3L0(a70) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a77_a22_a32_a54_a46_a68_a23_a67_a37_a16_a7_a8_a91_a9_a82_a81_a84_a100_a62_a20_a64_a41_a63_a74) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a56) \land $ \\ 
 $  \Rnext  \Rnext C0(a26) \land $ \\ 
 $  \Rnext E3L0(a11_a43) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a17) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a10_a52) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a65) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a21) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a78_a96) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a26) \land $ \\ 
 $  \Rnext E3L1Inv(a31) \land $ \\ 
 $  \Rnext  \Rnext C1(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a79_a34_a15_a69_a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a26) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a59) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a94_a53) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a70) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a80_a29_a95_a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a79_a34_a15_a69_a40) \land $ \\ 
 $  \Rnext  \Rnext C0(a4_a36) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a83) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a28) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a35) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a56) \land $ \\ 
 $  \Rnext E3L1(a72) \land $ \\ 
 $  \Rnext  \Rnext C1(a17) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a42) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a42) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a56) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a56) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a86) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a88_a61) \land $ \\ 
 $  \Rnext C1(a83) \land $ \\ 
 $  \Rnext  \Rnext C0(a25_a85_a30) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a80_a29_a95_a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a87_a14_a49) \land $ \\ 
 $  \Rnext E3L0Inv(a3) \land $ \\ 
 $  \Rnext E3L1(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a80_a29_a95_a73) \land $ \\ 
 $  \Rnext C0(a47) \land $ \\ 
 $  \Rnext C1(a98) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a3) \land $ \\ 
 $  \Rnext  \Rnext C1(a2_a90) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a1) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a13) \land $ \\ 
 $  \Rnext E3L0Inv(a21) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a21) \land $ \\ 
 $  \Rnext E3L0Inv(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a72) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a87_a14_a49) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a13) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a58) \land $ \\ 
 $  \Rnext E3L0(a94_a53) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a76_a6_a92) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a72) \land $ \\ 
 $  \Rnext E3L0Inv(a13) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a1) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a18) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a42) \land $ \\ 
 $  \Rnext E3L1Inv(a76_a6_a92) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a94_a53) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a24_a5) \land $ \\ 
 $  \Rnext E3L1(a1) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a18) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a25_a85_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a70) \land $ \\ 
 $  \Rnext E3L1(a21) \land $ \\ 
 $  \Rnext E3L1(a18) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a11_a43) \land $ \\ 
 $  \Rnext C1(a10_a52) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a66) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a48) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a87_a14_a49) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a99) \land $ \\ 
 $  \Rnext E3L0(a47) \land $ \\ 
 $  \Rnext E3L0Inv(a94_a53) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a59) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a58) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a70) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a66) \land $ \\ 
 $  \Rnext C1(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a24_a5) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a33_a44_a60) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a71) \land $ \\ 
 $  \Rnext E3L1Inv(a33_a44_a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a2_a90) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a80_a29_a95_a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a35) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a42) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a56) \land $ \\ 
 $  \Rnext C0(a26) \land $ \\ 
 $  \Rnext E3L0Inv(a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a76_a6_a92) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a24_a5) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a94_a53) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a80_a29_a95_a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a78_a96) \land $ \\ 
 $  \Rnext E3L1(a77_a22_a32_a54_a46_a68_a23_a67_a37_a16_a7_a8_a91_a9_a82_a81_a84_a100_a62_a20_a64_a41_a63_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a94_a53) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a4_a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a71) \land $ \\ 
 $  \Rnext C1(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a18) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a79_a34_a15_a69_a40) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a55_a45_a27_a38) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a42) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a77_a22_a32_a54_a46_a68_a23_a67_a37_a16_a7_a8_a91_a9_a82_a81_a84_a100_a62_a20_a64_a41_a63_a74) \land $ \\ 
 $  \Rnext E3L0(a3) \land $ \\ 
 $  \Rnext  \Rnext C1(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a33_a44_a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a33_a44_a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a56) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a79_a34_a15_a69_a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a88_a61) \land $ \\ 
 $ C1(a50) \land $ \\ 
 $ C1(a72) \land $ \\ 
 $ C1(a98) \land $ \\ 
 $ C1(a99) \land $ \\ 
 $ C1(a65) \land $ \\ 
 $ C1(a76_a6_a92) \land $ \\ 
 $ C1(a80_a29_a95_a73) \land $ \\ 
 $ C1(a4_a36) \land $ \\ 
 $ C1(a77_a22_a32_a54_a46_a68_a23_a67_a37_a16_a7_a8_a91_a9_a82_a81_a84_a100_a62_a20_a64_a41_a63_a74) \land $ \\ 
 $ C1(a11_a43) \land $ \\ 
 $ C1(a89) \land $ \\ 
 $ C1(a33_a44_a60) \land $ \\ 
 $ C1(a78_a96) \land $ \\ 
 $ C1(a47) \land $ \\ 
 $ C1(a55_a45_a27_a38) \land $ \\ 
 $ C1(a57) \land $ \\ 
 $ C1(a86) \land $ \\ 
 $ C1(a21) \land $ \\ 
 $ C1(a56) \land $ \\ 
 $ C1(a35) \land $ \\ 
 $ C1(a2_a90) \land $ \\ 
 $ C1(a13) \land $ \\ 
 $ C1(a12) \land $ \\ 
 $ C1(a70) \land $ \\ 
 $ C1(a87_a14_a49) \land $ \\ 
 $ C1(a93) \land $ \\ 
 $ C1(a83) \land $ \\ 
 $ C1(a39) \land $ \\ 
 $ C1(a17) \land $ \\ 
 $ C1(a3) \land $ \\ 
 $ C1(a24_a5) \land $ \\ 
 $ C1(a88_a61) \land $ \\ 
 $ C1(a10_a52) \land $ \\ 
 $ C1(a28) \land $ \\ 
 $ C1(a31) \land $ \\ 
 $ C1(a19_a97_a75) \land $ \\ 
 $ C1(a58) \land $ \\ 
 $ C1(a79_a34_a15_a69_a40) \land $ \\ 
 $ C1(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a83) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a4_a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a72) \land $ \\ 
 $  \Rnext E3L1Inv(a79_a34_a15_a69_a40) \land $ \\ 
 $  \Rnext  \Rnext C0(a87_a14_a49) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a26) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a70) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a65) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a4_a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a55_a45_a27_a38) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a21) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a26) \land $ \\ 
 $  \Rnext E3L1Inv(a57) \land $ \\ 
 $  \Rnext  \Rnext C1(a94_a53) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a72) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a11_a43) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a83) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a28) \land $ \\ 
 $  \Rnext  \Rnext C0(a93) \land $ \\ 
 $  \Rnext  \Rnext C1(a57) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a10_a52) \land $ \\ 
 $  \Rnext  \Rnext C1(a70) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a12) \land $ \\ 
 $  \Rnext  \Rnext C0(a99) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a88_a61) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a57) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a4_a36) \land $ \\ 
 $ E3L1(a12) \land $ \\ 
 $ E3L1(a42) \land $ \\ 
 $ E3L1(a11_a43) \land $ \\ 
 $ E3L1(a31) \land $ \\ 
 $ E3L1(a48) \land $ \\ 
 $ E3L1(a28) \land $ \\ 
 $ E3L1(a21) \land $ \\ 
 $ E3L1(a47) \land $ \\ 
 $ E3L1(a71) \land $ \\ 
 $ E3L1(a55_a45_a27_a38) \land $ \\ 
 $ E3L1(a77_a22_a32_a54_a46_a68_a23_a67_a37_a16_a7_a8_a91_a9_a82_a81_a84_a100_a62_a20_a64_a41_a63_a74) \land $ \\ 
 $ E3L1(a83) \land $ \\ 
 $ E3L1(a2_a90) \land $ \\ 
 $ E3L1(a24_a5) \land $ \\ 
 $ E3L1(a76_a6_a92) \land $ \\ 
 $ E3L1(a13) \land $ \\ 
 $ E3L1(a10_a52) \land $ \\ 
 $ E3L1(a79_a34_a15_a69_a40) \land $ \\ 
 $ E3L1(a99) \land $ \\ 
 $ E3L1(a50) \land $ \\ 
 $ E3L1(a56) \land $ \\ 
 $ E3L1(a98) \land $ \\ 
 $ E3L1(a25_a85_a30) \land $ \\ 
 $ E3L1(a26) \land $ \\ 
 $ E3L1(a1) \land $ \\ 
 $ E3L1(a65) \land $ \\ 
 $ E3L1(a80_a29_a95_a73) \land $ \\ 
 $ E3L1(a57) \land $ \\ 
 $ E3L1(a87_a14_a49) \land $ \\ 
 $ E3L1(a3) \land $ \\ 
 $ E3L1(a78_a96) \land $ \\ 
 $ E3L1(a70) \land $ \\ 
 $ E3L1(a72) \land $ \\ 
 $ E3L1(a93) \land $ \\ 
 $ E3L1(a19_a97_a75) \land $ \\ 
 $ E3L1(a88_a61) \land $ \\ 
 $ E3L1(a18) \land $ \\ 
 $ E3L1(a89) \land $ \\ 
 $ E3L1(a4_a36) \land $ \\ 
 $ E3L1(a86) \land $ \\ 
 $ E3L1(a39) \land $ \\ 
 $ E3L1(a58) \land $ \\ 
 $ E3L1(a59) \land $ \\ 
 $ E3L1(a94_a53) \land $ \\ 
 $ E3L1(a35) \land $ \\ 
 $ E3L1(a17) \land $ \\ 
 $ E3L1(a66) \land $ \\ 
 $ E3L1(a33_a44_a60) \land $ \\ 
 $ E3L1(a51) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a58) \land $ \\ 
 $  \Rnext E3L1(a88_a61) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a48) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a78_a96) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a13) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a88_a61) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a47) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a47) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a55_a45_a27_a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a19_a97_a75) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a86) \land $ \\ 
 $  \Rnext C1(a3) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a65) \land $ \\ 
 $  \Rnext E3L0Inv(a76_a6_a92) \land $ \\ 
 $  \Rnext E3L0Inv(a77_a22_a32_a54_a46_a68_a23_a67_a37_a16_a7_a8_a91_a9_a82_a81_a84_a100_a62_a20_a64_a41_a63_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a88_a61) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a25_a85_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a56) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a83) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a88_a61) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a1) \land $ \\ 
 $  \Rnext E3L1(a94_a53) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a51) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a13) \land $ \\ 
 $  \Rnext E3L0(a51) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a56) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a18) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a58) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a19_a97_a75) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a78_a96) \land $ \\ 
 $  \Rnext C1(a19_a97_a75) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a86) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a4_a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a24_a5) \land $ \\ 
 $  \Rnext C0(a17) \land $ \\ 
 $  \Rnext  \Rnext C0(a76_a6_a92) \land $ \\ 
 $  \Rnext E3L1Inv(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a83) \land $ \\ 
 $  \Rnext C0(a24_a5) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a39) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a94_a53) \land $ \\ 
 $  \Rnext E3L1Inv(a51) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a17) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a26) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a39) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a56) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a33_a44_a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a89) \land $ \\ 
 $  \Rnext C0(a35) \land $ \\ 
 $  \Rnext E3L0Inv(a17) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a77_a22_a32_a54_a46_a68_a23_a67_a37_a16_a7_a8_a91_a9_a82_a81_a84_a100_a62_a20_a64_a41_a63_a74) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a17) \land $ \\ 
 $  \Rnext C1(a51) \land $ \\ 
 $  \Rnext C1(a48) \land $ \\ 
 $  \Rnext  \Rnext C0(a28) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a57) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a47) \land $ \\ 
 $  \Rnext  \Rnext C1(a50) \land $ \\ 
 $  \Rnext  \Rnext C1(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a19_a97_a75) \land $ \\ 
 $  \Rnext C1(a76_a6_a92) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a11_a43) \land $ \\ 
 $  \Rnext C1(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a11_a43) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a65) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a71) \land $ \\ 
 $  \Rnext E3L1Inv(a4_a36) \land $ \\ 
 $  \Rnext E3L1Inv(a83) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a12) \land $ \\ 
 $  \Rnext E3L1Inv(a88_a61) \land $ \\ 
 $  \Rnext  \Rnext C0(a56) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a28) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a11_a43) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a12) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a28) \land $ \\ 
 $  \Rnext E3L0Inv(a72) \land $ \\ 
 $  \Rnext C0(a1) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a18) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a48) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a86) \land $ \\ 
 $  \Rnext E3L1(a57) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a28) \land $ \\ 
 $  \Rnext E3L0(a18) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a10_a52) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a72) \land $ \\ 
 $  \Rnext E3L1Inv(a55_a45_a27_a38) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a51) \land $ \\ 
 $ E3L0Inv(a35) \land $ \\ 
 $ E3L0Inv(a12) \land $ \\ 
 $ E3L0Inv(a42) \land $ \\ 
 $ E3L0Inv(a94_a53) \land $ \\ 
 $  \Rnext  \Rnext C1(a35) \land $ \\ 
 $ E3L0Inv(a24_a5) \land $ \\ 
 $ E3L0Inv(a10_a52) \land $ \\ 
 $ E3L0Inv(a50) \land $ \\ 
 $ E3L0Inv(a98) \land $ \\ 
 $ E3L0Inv(a17) \land $ \\ 
 $ E3L0Inv(a4_a36) \land $ \\ 
 $ E3L0Inv(a56) \land $ \\ 
 $ E3L0Inv(a66) \land $ \\ 
 $ E3L0Inv(a89) \land $ \\ 
 $ E3L0Inv(a70) \land $ \\ 
 $ E3L0Inv(a21) \land $ \\ 
 $ E3L0Inv(a55_a45_a27_a38) \land $ \\ 
 $ E3L0Inv(a31) \land $ \\ 
 $ E3L0Inv(a86) \land $ \\ 
 $ E3L0Inv(a59) \land $ \\ 
 $ E3L0Inv(a93) \land $ \\ 
 $ E3L0Inv(a1) \land $ \\ 
 $ E3L0Inv(a65) \land $ \\ 
 $ E3L0Inv(a51) \land $ \\ 
 $ E3L0Inv(a83) \land $ \\ 
 $ E3L0Inv(a19_a97_a75) \land $ \\ 
 $ E3L0Inv(a11_a43) \land $ \\ 
 $ E3L0Inv(a88_a61) \land $ \\ 
 $ E3L0Inv(a71) \land $ \\ 
 $ E3L0Inv(a78_a96) \land $ \\ 
 $ E3L0Inv(a76_a6_a92) \land $ \\ 
 $ E3L0Inv(a80_a29_a95_a73) \land $ \\ 
 $ E3L0Inv(a57) \land $ \\ 
 $ E3L0Inv(a47) \land $ \\ 
 $ E3L0Inv(a48) \land $ \\ 
 $ E3L0Inv(a13) \land $ \\ 
 $ E3L0Inv(a87_a14_a49) \land $ \\ 
 $ E3L0Inv(a33_a44_a60) \land $ \\ 
 $ E3L0Inv(a72) \land $ \\ 
 $ E3L0Inv(a28) \land $ \\ 
 $ E3L0Inv(a39) \land $ \\ 
 $ E3L0Inv(a25_a85_a30) \land $ \\ 
 $ E3L0Inv(a77_a22_a32_a54_a46_a68_a23_a67_a37_a16_a7_a8_a91_a9_a82_a81_a84_a100_a62_a20_a64_a41_a63_a74) \land $ \\ 
 $ E3L0Inv(a18) \land $ \\ 
 $ E3L0Inv(a26) \land $ \\ 
 $ E3L0Inv(a2_a90) \land $ \\ 
 $ E3L0Inv(a99) \land $ \\ 
 $ E3L0Inv(a79_a34_a15_a69_a40) \land $ \\ 
 $ E3L0Inv(a3) \land $ \\ 
 $ E3L0Inv(a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a11_a43) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a94_a53) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a79_a34_a15_a69_a40) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a35) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a71) \land $ \\ 
 $  \Rnext E3L1(a79_a34_a15_a69_a40) \land $ \\ 
 $  \Rnext C1(a59) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a19_a97_a75) \land $ \\ 
 $  \Rnext  \Rnext C1(a83) \land $ \\ 
 $  \Rnext  \Rnext C1(a10_a52) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a17) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a39) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a98) \land $ \\ 
 $  \Rnext E3L1(a76_a6_a92) \land $ \\ 
 $  \Rnext  \Rnext C0(a94_a53) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a70) \land $ \\ 
 $  \Rnext C1(a94_a53) \land $ \\ 
 $  \Rnext E3L0(a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a3) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a12) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a39) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a70) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a33_a44_a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a24_a5) \land $ \\ 
 $  \Rnext E3L1(a55_a45_a27_a38) \land $ \\ 
 $  \Rnext E3L0Inv(a99) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a11_a43) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a26) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a4_a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a87_a14_a49) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a78_a96) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a70) \land $ \\ 
 $  \Rnext C0(a80_a29_a95_a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a26) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a48) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a28) \land $ \\ 
 $  \Rnext  \Rnext C1(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a56) \land $ \\ 
 $  \Rnext C0(a25_a85_a30) \land $ \\ 
 $  \Rnext E3L1Inv(a42) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a77_a22_a32_a54_a46_a68_a23_a67_a37_a16_a7_a8_a91_a9_a82_a81_a84_a100_a62_a20_a64_a41_a63_a74) \land $ \\ 
 $  \Rnext E3L0(a98) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a39) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a57) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a3) \land $ \\ 
 $  \Rnext E3L1Inv(a17) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a88_a61) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a3) \land $ \\ 
 $  \Rnext E3L1Inv(a66) \land $ \\ 
 $  \Rnext C1(a17) \land $ \\ 
 $  \Rnext E3L1Inv(a3) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a78_a96) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a59) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a77_a22_a32_a54_a46_a68_a23_a67_a37_a16_a7_a8_a91_a9_a82_a81_a84_a100_a62_a20_a64_a41_a63_a74) \land $ \\ 
 $  \Rnext C1(a4_a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a57) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a28) \land $ \\ 
 $  \Rnext E3L1Inv(a10_a52) \land $ \\ 
 $  \Rnext E3L1Inv(a1) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a83) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a26) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a80_a29_a95_a73) \land $ \\ 
 $  \Rnext  \Rnext C0(a35) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a79_a34_a15_a69_a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a19_a97_a75) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a72) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a10_a52) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a94_a53) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a48) \land $ \\ 
 $  \Rnext E3L0(a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a78_a96) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a51) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a17) \land $ \\ 
 $  \Rnext E3L1(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a70) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a71) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a80_a29_a95_a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a48) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a55_a45_a27_a38) \land $ \\ 
 $  \Rnext E3L0(a57) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a12) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a76_a6_a92) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a88_a61) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a72) \land $ \\ 
 $  \Rnext C0(a2_a90) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a99) \land $ \\ 
 $  \Rnext  \Rnext C0(a18) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a26) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a35) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a59) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a76_a6_a92) \land $ \\ 
 $  \Rnext C0(a56) \land $ \\ 
 $  \Rnext E3L1(a39) \land $ \\ 
 $  \Rnext E3L1(a48) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a98) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a65) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a1) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a4_a36) \land $ \\ 
 $  \Rnext E3L0Inv(a66) \land $ \\ 
 $  \Rnext E3L0(a78_a96) \land $ \\ 
 $  \Rnext C0(a51) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a57) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a70) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a55_a45_a27_a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a11_a43) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a83) \land $ \\ 
 $  \Rnext E3L1Inv(a87_a14_a49) \land $ \\ 
 $  \Rnext E3L1(a19_a97_a75) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a87_a14_a49) \land $ \\ 
 $  \Rnext E3L1Inv(a2_a90) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a55_a45_a27_a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a17) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a47) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a51) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a83) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a24_a5) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a21) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a35) \land $ \\ 
 $  \Rnext E3L0Inv(a51) \land $ \\ 
 $  \Rnext  \Rnext C1(a48) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a66) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a50) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a47) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a21) \land $ \\ 
 $  \Rnext C0(a78_a96) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a78_a96) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a11_a43) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a66) \land $ \\ 
 $  \Rnext E3L1Inv(a13) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a1) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a83) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a98) \land $ \\ 
 $  \Rnext E3L0(a17) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a94_a53) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a51) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a1) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a51) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a12) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a89) \land $ \\ 
 $  \Rnext E3L1Inv(a94_a53) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a25_a85_a30) \land $ \\ 
 $  \Rnext E3L1(a59) \land $ \\ 
 $  \Rnext E3L1(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a39) \land $ \\ 
 $  \Rnext  \Rnext C0(a13) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a13) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a12) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a19_a97_a75) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a48) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a55_a45_a27_a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a2_a90) \land $ \\ 
 $  \Rnext E3L1(a2_a90) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a18) \land $ \\ 
 $  \Rnext E3L0Inv(a42) \land $ \\ 
 $  \Rnext E3L1Inv(a35) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a18) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a10_a52) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a24_a5) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a87_a14_a49) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a56) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a10_a52) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a59) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a24_a5) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a89) \land $ \\ 
 $  \Rnext E3L0(a65) \land $ \\ 
 $  \Rnext E3L0(a25_a85_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a21) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a31) \land $ \\ 
 $  \Rnext C0(a19_a97_a75) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a17) \land $ \\ 
 $  \Rnext E3L1Inv(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a50) \land $ \\ 
 $  \Rnext E3L1Inv(a59) \land $ \\ 
 $  \Rnext E3L0Inv(a33_a44_a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a88_a61) \land $ \\ 
 $  \Rnext C0(a3) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a66) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a86) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a4_a36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a10_a52) \land $ \\ 
 $  \Rnext  \Rnext C1(a4_a36) \land $ \\ 
 $  \Rnext  \Rnext C0(a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a11_a43) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a42) \land $ \\ 
 $  \Rnext E3L0(a86) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a2_a90) \land $ \\ 
 $  \Rnext E3L1Inv(a47) \land $ \\ 
 $  \Rnext  \Rnext C0(a65) \land $ \\ 
 $  \Rnext C1(a31) \land $ \\ 
 $  \Rnext E3L1Inv(a26) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a76_a6_a92) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a55_a45_a27_a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a11_a43) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a88_a61) \land $ \\ 
 $  \Rnext C1(a1) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a17) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a65) \land $ \\ 
 $  \Rnext C0(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a33_a44_a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a83) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a77_a22_a32_a54_a46_a68_a23_a67_a37_a16_a7_a8_a91_a9_a82_a81_a84_a100_a62_a20_a64_a41_a63_a74) \land $ \\ 
 $  \Rnext E3L1(a78_a96) \land $ \\ 
 $  \Rnext  \Rnext C0(a2_a90) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a4_a36) \land $ \\ 
 $  \Rnext  \Rnext C0(a79_a34_a15_a69_a40) \land $ \\ 
 $  \Rnext E3L0(a4_a36) \land $ \\ 
 $  \Rnext E3L0Inv(a87_a14_a49) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a99) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a25_a85_a30) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a86) \land $ \\ 
 $  \Rnext E3L1Inv(a19_a97_a75) \land $ \\ 
 $  \Rnext C1(a87_a14_a49) \land $ \\ 
 $  \Rnext E3L1(a11_a43) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a26) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a39) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a51) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a3) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a80_a29_a95_a73) \land $ \\ 
 $  \Rnext E3L1Inv(a99) \land $ \\ 
 $  \Rnext E3L1Inv(a25_a85_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a1) \land $ \\ 
 $  \Rnext E3L1(a87_a14_a49) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a2_a90) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a48) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a19_a97_a75) \land $ \\ 
 $  \Rnext C1(a39) \land $ \\ 
 $  \Rnext E3L0Inv(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a59) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a33_a44_a60) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a77_a22_a32_a54_a46_a68_a23_a67_a37_a16_a7_a8_a91_a9_a82_a81_a84_a100_a62_a20_a64_a41_a63_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a4_a36) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a47) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a77_a22_a32_a54_a46_a68_a23_a67_a37_a16_a7_a8_a91_a9_a82_a81_a84_a100_a62_a20_a64_a41_a63_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a79_a34_a15_a69_a40) \land $ \\ 
 $  \Rnext E3L1(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a10_a52) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a56) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a80_a29_a95_a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a24_a5) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a18) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a18) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a59) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a25_a85_a30) \land $ \\ 
 $  \Rnext E3L0Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a77_a22_a32_a54_a46_a68_a23_a67_a37_a16_a7_a8_a91_a9_a82_a81_a84_a100_a62_a20_a64_a41_a63_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a93) \land $ \\ 
 $  \Rnext E3L0Inv(a12) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a31) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a25_a85_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a26) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a39) \land $ \\ 
 $  \Rnext E3L0Inv(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a1) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a72) \land $ \\ 
 $  \Rnext C0(a18) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a78_a96) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a79_a34_a15_a69_a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a86) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a24_a5) \land $ \\ 
 $  \Rnext E3L0(a59) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a83) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a17) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a13) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a35) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a58) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a19_a97_a75) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a79_a34_a15_a69_a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a80_a29_a95_a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a11_a43) \land $ \\ 
 $  \Rnext  \Rnext C1(a12) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a78_a96) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a56) \land $ \\ 
 $  \Rnext E3L0Inv(a56) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a98) \land $ \\ 
 $  \Rnext E3L0(a10_a52) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a28) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a87_a14_a49) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a87_a14_a49) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a2_a90) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a51) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a89) \land $ \\ 
 $  \Rnext  \Rnext C0(a66) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a10_a52) \land $ \\ 
 $  \Rnext C0(a48) \land $ \\ 
 $  \Rnext  \Rnext C1(a26) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a51) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a79_a34_a15_a69_a40) \land $ \\ 
 $  \Rnext E3L0(a33_a44_a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a50) \land $ \\ 
 $  \Rnext C1(a25_a85_a30) \land $ \\ 
 $  \Rnext E3L1Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a3) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a10_a52) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a66) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a24_a5) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a26) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a58) \land $ \\ 
 $  \Rnext E3L1Inv(a24_a5) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a47) \land $ \\ 
 $  \Rnext C1(a66) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a79_a34_a15_a69_a40) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a80_a29_a95_a73) \land $ \\ 
 $  \Rnext E3L1(a86) \land $ \\ 
 $  \Rnext  \Rnext C1(a87_a14_a49) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a89) \land $ \\ 
 $  \Rnext C0(a4_a36) \land $ \\ 
 $  \Rnext E3L0Inv(a11_a43) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a79_a34_a15_a69_a40) \land $ \\ 
 $ E3G0(a77_a22_a32_a54_a46_a68_a23_a67_a37_a16_a7_a8_a91_a9_a82_a81_a84_a100_a62_a20_a64_a41_a63_a74) \land $ \\ 
 $ E3G0(a12) \land $ \\ 
 $ E3G0(a42) \land $ \\ 
 $ E3G0(a86) \land $ \\ 
 $ E3G0(a79_a34_a15_a69_a40) \land $ \\ 
 $ E3G0(a59) \land $ \\ 
 $ E3G0(a58) \land $ \\ 
 $ E3G0(a98) \land $ \\ 
 $ E3G0(a17) \land $ \\ 
 $ E3G0(a65) \land $ \\ 
 $ E3G0(a93) \land $ \\ 
 $ E3G0(a1) \land $ \\ 
 $ E3G0(a11_a43) \land $ \\ 
 $ E3G0(a80_a29_a95_a73) \land $ \\ 
 $ E3G0(a76_a6_a92) \land $ \\ 
 $ E3G0(a71) \land $ \\ 
 $ E3G0(a24_a5) \land $ \\ 
 $ E3G0(a66) \land $ \\ 
 $ E3G0(a70) \land $ \\ 
 $ E3G0(a33_a44_a60) \land $ \\ 
 $ E3G0(a56) \land $ \\ 
 $ E3G0(a94_a53) \land $ \\ 
 $ E3G0(a51) \land $ \\ 
 $ E3G0(a47) \land $ \\ 
 $ E3G0(a88_a61) \land $ \\ 
 $ E3G0(a21) \land $ \\ 
 $ E3G0(a89) \land $ \\ 
 $ E3G0(a2_a90) \land $ \\ 
 $ E3G0(a26) \land $ \\ 
 $ E3G0(a31) \land $ \\ 
 $ E3G0(a19_a97_a75) \land $ \\ 
 $ E3G0(a4_a36) \land $ \\ 
 $ E3G0(a28) \land $ \\ 
 $ E3G0(a3) \land $ \\ 
 $ E3G0(a10_a52) \land $ \\ 
 $ E3G0(a57) \land $ \\ 
 $ E3G0(a13) \land $ \\ 
 $ E3G0(a87_a14_a49) \land $ \\ 
 $ E3G0(a25_a85_a30) \land $ \\ 
 $ E3G0(a72) \land $ \\ 
 $ E3G0(a55_a45_a27_a38) \land $ \\ 
 $ E3G0(a50) \land $ \\ 
 $ E3G0(a48) \land $ \\ 
 $ E3G0(a39) \land $ \\ 
 $ E3G0(a83) \land $ \\ 
 $ E3G0(a35) \land $ \\ 
 $ E3G0(a99) \land $ \\ 
 $ E3G0(a18) \land $ \\ 
 $ E3G0(a78_a96) \land $ \\ 
 $  \Rnext C0(a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a59) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a86) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a25_a85_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a59) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a39) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a70) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a89) \land $ \\ 
 $  \Rnext  \Rnext C1(a42) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a51) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a87_a14_a49) \land $ \\ 
 $  \Rnext E3L1Inv(a77_a22_a32_a54_a46_a68_a23_a67_a37_a16_a7_a8_a91_a9_a82_a81_a84_a100_a62_a20_a64_a41_a63_a74) \land $ \\ 
 $  \Rnext E3L0(a26) \land $ \\ 
 $  \Rnext E3L0(a55_a45_a27_a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a17) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a88_a61) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a3) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a77_a22_a32_a54_a46_a68_a23_a67_a37_a16_a7_a8_a91_a9_a82_a81_a84_a100_a62_a20_a64_a41_a63_a74) \land $ \\ 
 $  \Rnext E3L0(a56) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a56) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a94_a53) \land $ \\ 
 $  \Rnext E3L0(a80_a29_a95_a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a13) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a25_a85_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a99) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a51) \land $ \\ 
 $  \Rnext E3L0Inv(a1) \land $ \\ 
 $  \Rnext E3L0Inv(a19_a97_a75) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a35) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a93) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a4_a36) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a28) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a47) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a3) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a12) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a13) \land $ \\ 
 $  \Rnext C0(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a42) \land $ \\ 
 $  \Rnext E3L1(a3) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a72) \land $ \\ 
 $  \Rnext E3L0Inv(a26) \land $ \\ 
 $  \Rnext E3L0Inv(a83) \land $ \\ 
 $  \Rnext E3L0(a31) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a66) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a33_a44_a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a21) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a94_a53) \land $ \\ 
 $  \Rnext E3L1(a99) \land $ \\ 
 $  \Rnext E3L1(a58) \land $ \\ 
 $  \Rnext E3L1(a56) \land $ \\ 
 $  \Rnext E3L1(a33_a44_a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a76_a6_a92) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a66) \land $ \\ 
 $  \Rnext E3L1Inv(a70) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a13) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a4_a36) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a4_a36) \land $ \\ 
 $  \Rnext E3L0(a77_a22_a32_a54_a46_a68_a23_a67_a37_a16_a7_a8_a91_a9_a82_a81_a84_a100_a62_a20_a64_a41_a63_a74) \land $ \\ 
 $  \Rnext  \Rnext C1(a79_a34_a15_a69_a40) \land $ \\ 
 $  \Rnext E3L1Inv(a48) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a51) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a18) \land $ \\ 
 $  \Rnext E3L0Inv(a18) \land $ \\ 
 $  \Rnext E3L0(a2_a90) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a76_a6_a92) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a78_a96) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a88_a61) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a50) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a65) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a3) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a98) \land $ \\ 
 $  \Rnext E3L0Inv(a79_a34_a15_a69_a40) \land $ \\ 
 $ E3L1Inv(a78_a96) \land $ \\ 
 $ E3L1Inv(a86) \land $ \\ 
 $ E3L1Inv(a77_a22_a32_a54_a46_a68_a23_a67_a37_a16_a7_a8_a91_a9_a82_a81_a84_a100_a62_a20_a64_a41_a63_a74) \land $ \\ 
 $ E3L1Inv(a98) \land $ \\ 
 $ E3L1Inv(a70) \land $ \\ 
 $ E3L1Inv(a11_a43) \land $ \\ 
 $ E3L1Inv(a89) \land $ \\ 
 $ E3L1Inv(a55_a45_a27_a38) \land $ \\ 
 $ E3L1Inv(a57) \land $ \\ 
 $ E3L1Inv(a56) \land $ \\ 
 $ E3L1Inv(a99) \land $ \\ 
 $ E3L1Inv(a76_a6_a92) \land $ \\ 
 $ E3L1Inv(a31) \land $ \\ 
 $ E3L1Inv(a47) \land $ \\ 
 $ E3L1Inv(a72) \land $ \\ 
 $ E3L1Inv(a39) \land $ \\ 
 $ E3L1Inv(a12) \land $ \\ 
 $ E3L1Inv(a42) \land $ \\ 
 $ E3L1Inv(a1) \land $ \\ 
 $ E3L1Inv(a25_a85_a30) \land $ \\ 
 $ E3L1Inv(a88_a61) \land $ \\ 
 $ E3L1Inv(a10_a52) \land $ \\ 
 $ E3L1Inv(a28) \land $ \\ 
 $ E3L1Inv(a87_a14_a49) \land $ \\ 
 $ E3L1Inv(a35) \land $ \\ 
 $ E3L1Inv(a80_a29_a95_a73) \land $ \\ 
 $ E3L1Inv(a58) \land $ \\ 
 $ E3L1Inv(a83) \land $ \\ 
 $ E3L1Inv(a51) \land $ \\ 
 $ E3L1Inv(a48) \land $ \\ 
 $ E3L1Inv(a21) \land $ \\ 
 $ E3L1Inv(a18) \land $ \\ 
 $ E3L1Inv(a26) \land $ \\ 
 $ E3L1Inv(a33_a44_a60) \land $ \\ 
 $ E3L1Inv(a24_a5) \land $ \\ 
 $ E3L1Inv(a50) \land $ \\ 
 $ E3L1Inv(a13) \land $ \\ 
 $ E3L1Inv(a4_a36) \land $ \\ 
 $ E3L1Inv(a17) \land $ \\ 
 $ E3L1Inv(a65) \land $ \\ 
 $ E3L1Inv(a3) \land $ \\ 
 $ E3L1Inv(a59) \land $ \\ 
 $ E3L1Inv(a19_a97_a75) \land $ \\ 
 $ E3L1Inv(a71) \land $ \\ 
 $ E3L1Inv(a66) \land $ \\ 
 $ E3L1Inv(a2_a90) \land $ \\ 
 $ E3L1Inv(a79_a34_a15_a69_a40) \land $ \\ 
 $ E3L1Inv(a94_a53) \land $ \\ 
 $ E3L1Inv(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a31) \land $ \\ 
 $  \Rnext E3L0(a71) \land $ \\ 
 $  \Rnext E3L1(a35) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a87_a14_a49) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a24_a5) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a11_a43) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a21) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a86) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a19_a97_a75) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a51) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a35) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a31) \land $ \\ 
 $  \Rnext E3L1(a12) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a77_a22_a32_a54_a46_a68_a23_a67_a37_a16_a7_a8_a91_a9_a82_a81_a84_a100_a62_a20_a64_a41_a63_a74) \land $ \\ 
 $  \Rnext E3L1Inv(a80_a29_a95_a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a19_a97_a75) \land $ \\ 
 $  \Rnext E3L0(a1) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a59) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a57) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a48) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a1) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a70) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a24_a5) \land $ \\ 
 $  \Rnext E3L1Inv(a21) \land $ \\ 
 $  \Rnext C0(a21) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a65) \land $ \\ 
 $  \Rnext E3L1Inv(a58) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a94_a53) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a70) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a78_a96) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a72) \land $ \\ 
 $  \Rnext E3L1(a80_a29_a95_a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a88_a61) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a76_a6_a92) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a21) \land $ \\ 
 $  \Rnext E3L1Inv(a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a47) \land $ \\ 
 $  \Rnext C1(a50) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a83) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a48) \land $ \\ 
 $  \Rnext E3L1(a13) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a98) \land $ \\ 
 $  \Rnext  \Rnext C0(a21) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a1) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a3) \land $ \\ 
 $  \Rnext  \Rnext C0(a24_a5) \land $ \\ 
 $  \Rnext C1(a18) \land $ \\ 
 $  \Rnext E3L0(a83) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a12) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a26) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a25_a85_a30) \land $ \\ 
 $  \Rnext C0(a55_a45_a27_a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a10_a52) \land $ \\ 
 $  \Rnext E3L1Inv(a78_a96) \land $ \\ 
 $  \Rnext E3L0(a50) \land $ \\ 
 $  \Rnext  \Rnext C1(a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a57) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a99) \land $ \\ 
 $  \Rnext E3L1Inv(a28) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a76_a6_a92) \land $ \\ 
 $  \Rnext  \Rnext C0(a19_a97_a75) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a94_a53) \land $ \\ 
 $  \Rnext E3L0(a88_a61) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a21) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a58) \land $ \\ 
 $  \Rnext E3L0Inv(a25_a85_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a31) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a12) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a83) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a59) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a51) \land $ \\ 
 $  \Rnext E3L1Inv(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a70) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a33_a44_a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a42) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a28) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a80_a29_a95_a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a87_a14_a49) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a19_a97_a75) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a86) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a79_a34_a15_a69_a40) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a35) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a24_a5) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a59) \land $ \\ 
 $  \Rnext E3L0Inv(a47) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a66) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a50) \land $ \\ 
 $  \Rnext C0(a57) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a13) \land $ \\ 
 $  \Rnext E3L0(a76_a6_a92) \land $ \\ 
 $  \Rnext E3L0Inv(a80_a29_a95_a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a87_a14_a49) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a72) \land $ \\ 
 $  \Rnext E3L1Inv(a39) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a56) \land $ \\ 
 $  \Rnext E3L1Inv(a56) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a55_a45_a27_a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a88_a61) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a47) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a24_a5) \land $ \\ 
 $  \Rnext C0(a66) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a99) \land $ \\ 
 $  \Rnext C1(a56) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a87_a14_a49) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a78_a96) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a98) \land $ \\ 
 $  \Rnext  \Rnext C0(a33_a44_a60) \land $ \\ 
 $  \Rnext E3L0Inv(a59) \land $ \\ 
 $  \Rnext E3L0Inv(a57) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a66) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a31) \land $ \\ 
 $  \Rnext C0(a94_a53) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a80_a29_a95_a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a39) \land $ \\ 
 $  \Rnext E3L1Inv(a12) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a39) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a89) \land $ \\ 
 $  \Rnext E3L0(a66) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a18) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a19_a97_a75) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a18) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a42) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a25_a85_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a77_a22_a32_a54_a46_a68_a23_a67_a37_a16_a7_a8_a91_a9_a82_a81_a84_a100_a62_a20_a64_a41_a63_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a65) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a57) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a12) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a47) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a25_a85_a30) \land $ \\ 
 $  \Rnext C0(a33_a44_a60) \land $ \\ 
 $  \Rnext  \Rnext C1(a21) \land $ \\ 
 $  \Rnext E3L0Inv(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a17) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a94_a53) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a55_a45_a27_a38) \land $ \\ 
 $  \Rnext C0(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a48) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a25_a85_a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a42) \land $ \\ 
 $  \Rnext  \Rnext C1(a80_a29_a95_a73) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a13) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a59) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a19_a97_a75) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a35) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a57) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a39) \land $ \\ 
 $  \Rnext  \Rnext C1(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a19_a97_a75) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a78_a96) \land $ \\ 
 $  \Rnext  \Rnext C0(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a11_a43) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a48) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a12) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a3) \land $ \\ 
 $ E3G1(a79_a34_a15_a69_a40) \land $ \\ 
 $ E3G1(a88_a61) \land $ \\ 
 $ E3G1(a42) \land $ \\ 
 $ E3G1(a12) \land $ \\ 
 $ E3G1(a48) \land $ \\ 
 $ E3G1(a72) \land $ \\ 
 $ E3G1(a31) \land $ \\ 
 $ E3G1(a51) \land $ \\ 
 $ E3G1(a58) \land $ \\ 
 $ E3G1(a33_a44_a60) \land $ \\ 
 $ E3G1(a98) \land $ \\ 
 $ E3G1(a19_a97_a75) \land $ \\ 
 $ E3G1(a10_a52) \land $ \\ 
 $ E3G1(a50) \land $ \\ 
 $ E3G1(a21) \land $ \\ 
 $ E3G1(a11_a43) \land $ \\ 
 $ E3G1(a24_a5) \land $ \\ 
 $ E3G1(a93) \land $ \\ 
 $ E3G1(a99) \land $ \\ 
 $ E3G1(a28) \land $ \\ 
 $ E3G1(a35) \land $ \\ 
 $ E3G1(a4_a36) \land $ \\ 
 $ E3G1(a17) \land $ \\ 
 $ E3G1(a66) \land $ \\ 
 $ E3G1(a86) \land $ \\ 
 $ E3G1(a25_a85_a30) \land $ \\ 
 $ E3G1(a13) \land $ \\ 
 $ E3G1(a71) \land $ \\ 
 $ E3G1(a76_a6_a92) \land $ \\ 
 $ E3G1(a78_a96) \land $ \\ 
 $ E3G1(a59) \land $ \\ 
 $ E3G1(a26) \land $ \\ 
 $ E3G1(a2_a90) \land $ \\ 
 $ E3G1(a56) \land $ \\ 
 $ E3G1(a65) \land $ \\ 
 $ E3G1(a83) \land $ \\ 
 $ E3G1(a57) \land $ \\ 
 $ E3G1(a94_a53) \land $ \\ 
 $ E3G1(a3) \land $ \\ 
 $ E3G1(a70) \land $ \\ 
 $ E3G1(a47) \land $ \\ 
 $ E3G1(a89) \land $ \\ 
 $ E3G1(a39) \land $ \\ 
 $ E3G1(a77_a22_a32_a54_a46_a68_a23_a67_a37_a16_a7_a8_a91_a9_a82_a81_a84_a100_a62_a20_a64_a41_a63_a74) \land $ \\ 
 $ E3G1(a87_a14_a49) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a39) \land $ \\ 
 $ E3G1(a55_a45_a27_a38) \land $ \\ 
 $ E3G1(a18) \land $ \\ 
 $ E3G1(a1) \land $ \\ 
 $ E3G1(a80_a29_a95_a73) \land $ \\ 
 $  \Rnext E3L1Inv(a86) \land $ \\ 
 $  \Rnext C0(a28) \land $ \\ 
 $  \Rnext  \Rnext C0(a80_a29_a95_a73) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a2_a90) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a12) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a17) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a66) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a18) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a10_a52) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a79_a34_a15_a69_a40) \land $ \\ 
 $  \Rnext E3L0Inv(a48) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a42) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a50) \land $ \\ 
 $  \Rnext  \Rnext C1(a78_a96) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a21) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a55_a45_a27_a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a71) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a71) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a76_a6_a92) \land $ \\ 
 $  \Rnext C0(a12) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a28) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a1) \land $ \\ 
 $  \Rnext C1(a35) \land $ \\ 
 $  \Rnext E3L1Inv(a18) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a35) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a19_a97_a75) \land $ \\ 
 $  \Rnext E3L1(a26) \land $ \\ 
 $  \Rnext E3L1(a47) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a87_a14_a49) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a39) \land $ \\ 
 $  \Rnext E3L1(a10_a52) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a57) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a42) \land $ \\ 
 $  \Rnext  \Rnext C0(a59) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a28) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a33_a44_a60) \land $ \\ 
 $  \Rnext E3L1(a42) \land $ \\ 
 $  \Rnext E3L0Inv(a28) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a18) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a76_a6_a92) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a86) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a47) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a21) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a1) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a66) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a13) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a50) \land $ \\ 
 $  \Rnext  \Rnext C1(a76_a6_a92) \land $ \\ 
 $  \Rnext E3L0Inv(a78_a96) \land $ \\ 
 $  \Rnext E3L0Inv(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a55_a45_a27_a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a33_a44_a60) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a33_a44_a60) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a3) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a10_a52) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a11_a43) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a35) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a18) \land $ \\ 
 $  \Rnext  \Rnext C0(a70) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a25_a85_a30) \land $ \\ 
 $  \Rnext E3L0(a19_a97_a75) \land $ \\ 
 $  \Rnext  \Rnext C0(a42) \land $ \\ 
 $  \Rnext  \Rnext C0(a51) \land $ \\ 
 $  \Rnext  \Rnext C1(a18) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a12) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a33_a44_a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a12) \land $ \\ 
 $  \Rnext E3L1(a71) \land $ \\ 
 $  \Rnext  \Rnext C0(a98) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a70) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a1) \land $ \\ 
 $  \Rnext C1(a33_a44_a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a48) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a66) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a2_a90) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a66) \land $ \\ 
 $  \Rnext E3L1(a24_a5) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a55_a45_a27_a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a94_a53) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a21) \land $ \\ 
 $  \Rnext C0(a76_a6_a92) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a12) \land $ \\ 
 $  \Rnext C1(a77_a22_a32_a54_a46_a68_a23_a67_a37_a16_a7_a8_a91_a9_a82_a81_a84_a100_a62_a20_a64_a41_a63_a74) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a83) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a86) \land $ \\ 
 $  \Rnext E3L0(a24_a5) \land $ \\ 
 $  \Rnext C1(a80_a29_a95_a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a57) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a79_a34_a15_a69_a40) \land $ \\ 
 $  \Rnext  \Rnext C1(a33_a44_a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a31) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a58) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a42) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a76_a6_a92) \land $ \\ 
 $  \Rnext E3L1(a65) \land $ \\ 
 $  \Rnext C0(a87_a14_a49) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a35) \land $ \\ 
 $  \Rnext E3L1(a4_a36) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a35) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a77_a22_a32_a54_a46_a68_a23_a67_a37_a16_a7_a8_a91_a9_a82_a81_a84_a100_a62_a20_a64_a41_a63_a74) \land $ \\ 
 $  \Rnext E3L0(a21) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a2_a90) \land $ \\ 
 $ E1G0Inv(a80_a29_a95_a73) \land $ \\ 
 $ E1G0Inv(a70) \land $ \\ 
 $ E1G0Inv(a87_a14_a49) \land $ \\ 
 $ E1G0Inv(a11_a43) \land $ \\ 
 $ E1G0Inv(a18) \land $ \\ 
 $ E1G0Inv(a76_a6_a92) \land $ \\ 
 $ E1G0Inv(a78_a96) \land $ \\ 
 $ E1G0Inv(a57) \land $ \\ 
 $ E1G0Inv(a65) \land $ \\ 
 $ E1G0Inv(a47) \land $ \\ 
 $ E1G0Inv(a59) \land $ \\ 
 $ E1G0Inv(a51) \land $ \\ 
 $ E1G0Inv(a58) \land $ \\ 
 $ E1G0Inv(a56) \land $ \\ 
 $ E1G0Inv(a66) \land $ \\ 
 $ E1G0Inv(a12) \land $ \\ 
 $ E1G0Inv(a42) \land $ \\ 
 $ E1G0Inv(a93) \land $ \\ 
 $ E1G0Inv(a89) \land $ \\ 
 $ E1G0Inv(a50) \land $ \\ 
 $ E1G0Inv(a13) \land $ \\ 
 $ E1G0Inv(a10_a52) \land $ \\ 
 $ E1G0Inv(a3) \land $ \\ 
 $ E1G0Inv(a77_a22_a32_a54_a46_a68_a23_a67_a37_a16_a7_a8_a91_a9_a82_a81_a84_a100_a62_a20_a64_a41_a63_a74) \land $ \\ 
 $ E1G0Inv(a19_a97_a75) \land $ \\ 
 $ E1G0Inv(a25_a85_a30) \land $ \\ 
 $ E1G0Inv(a28) \land $ \\ 
 $ E1G0Inv(a72) \land $ \\ 
 $ E1G0Inv(a17) \land $ \\ 
 $ E1G0Inv(a98) \land $ \\ 
 $ E1G0Inv(a4_a36) \land $ \\ 
 $ E1G0Inv(a71) \land $ \\ 
 $ E1G0Inv(a35) \land $ \\ 
 $ E1G0Inv(a1) \land $ \\ 
 $ E1G0Inv(a86) \land $ \\ 
 $ E1G0Inv(a99) \land $ \\ 
 $ E1G0Inv(a83) \land $ \\ 
 $ E1G0Inv(a24_a5) \land $ \\ 
 $ E1G0Inv(a55_a45_a27_a38) \land $ \\ 
 $ E1G0Inv(a26) \land $ \\ 
 $ E1G0Inv(a33_a44_a60) \land $ \\ 
 $ E1G0Inv(a79_a34_a15_a69_a40) \land $ \\ 
 $ E1G0Inv(a31) \land $ \\ 
 $ E1G0Inv(a39) \land $ \\ 
 $ E1G0Inv(a94_a53) \land $ \\ 
 $ E1G0Inv(a2_a90) \land $ \\ 
 $ E1G0Inv(a88_a61) \land $ \\ 
 $ E1G0Inv(a48) \land $ \\ 
 $ E1G0Inv(a21) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a59) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a31) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a57) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a79_a34_a15_a69_a40) \land $ \\ 
 $  \Rnext C1(a70) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a13) \land $ \\ 
 $  \Rnext E3L0Inv(a86) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a59) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a33_a44_a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a26) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a83) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a78_a96) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a77_a22_a32_a54_a46_a68_a23_a67_a37_a16_a7_a8_a91_a9_a82_a81_a84_a100_a62_a20_a64_a41_a63_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a25_a85_a30) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a77_a22_a32_a54_a46_a68_a23_a67_a37_a16_a7_a8_a91_a9_a82_a81_a84_a100_a62_a20_a64_a41_a63_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a99) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a55_a45_a27_a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a76_a6_a92) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a55_a45_a27_a38) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a2_a90) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a21) \land $ \\ 
 $  \Rnext E3L0(a28) \land $ \\ 
 $ C0(a76_a6_a92) \land $ \\ 
 $ C0(a26) \land $ \\ 
 $ C0(a42) \land $ \\ 
 $ C0(a77_a22_a32_a54_a46_a68_a23_a67_a37_a16_a7_a8_a91_a9_a82_a81_a84_a100_a62_a20_a64_a41_a63_a74) \land $ \\ 
 $ C0(a55_a45_a27_a38) \land $ \\ 
 $ C0(a88_a61) \land $ \\ 
 $ C0(a24_a5) \land $ \\ 
 $ C0(a66) \land $ \\ 
 $ C0(a2_a90) \land $ \\ 
 $ C0(a35) \land $ \\ 
 $ C0(a39) \land $ \\ 
 $ C0(a58) \land $ \\ 
 $ C0(a1) \land $ \\ 
 $ C0(a56) \land $ \\ 
 $ C0(a51) \land $ \\ 
 $ C0(a80_a29_a95_a73) \land $ \\ 
 $ C0(a11_a43) \land $ \\ 
 $ C0(a93) \land $ \\ 
 $ C0(a78_a96) \land $ \\ 
 $ C0(a3) \land $ \\ 
 $ C0(a94_a53) \land $ \\ 
 $ C0(a87_a14_a49) \land $ \\ 
 $ C0(a33_a44_a60) \land $ \\ 
 $ C0(a19_a97_a75) \land $ \\ 
 $ C0(a48) \land $ \\ 
 $ C0(a50) \land $ \\ 
 $ C0(a72) \land $ \\ 
 $ C0(a79_a34_a15_a69_a40) \land $ \\ 
 $ C0(a18) \land $ \\ 
 $ C0(a31) \land $ \\ 
 $ C0(a99) \land $ \\ 
 $ C0(a86) \land $ \\ 
 $ C0(a65) \land $ \\ 
 $ C0(a25_a85_a30) \land $ \\ 
 $ C0(a10_a52) \land $ \\ 
 $ C0(a70) \land $ \\ 
 $ C0(a21) \land $ \\ 
 $ C0(a17) \land $ \\ 
 $  \Rnext E3L0(a87_a14_a49) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a48) \land $ \\ 
 $  \Rnext C0(a88_a61) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a17) \land $ \\ 
 $  \Rnext E3L1(a17) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a3) \land $ \\ 
 $  \Rnext  \Rnext C0(a10_a52) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a3) \land $ \\ 
 $  \Rnext  \Rnext C0(a57) \land $ \\ 
 $  \Rnext E3L0Inv(a24_a5) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a86) \land $ \\ 
 $  \Rnext  \Rnext C1(a55_a45_a27_a38) \land $ \\ 
 $  \Rnext C0(a83) \land $ \\ 
 $  \Rnext E3L1Inv(a89) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a25_a85_a30) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a65) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a28) \land $ \\ 
 $ E3L0(a58) \land $ \\ 
 $ E3L0(a78_a96) \land $ \\ 
 $ E3L0(a93) \land $ \\ 
 $ E3L0(a42) \land $ \\ 
 $ E3L0(a71) \land $ \\ 
 $ E3L0(a66) \land $ \\ 
 $ E3L0(a87_a14_a49) \land $ \\ 
 $ E3L0(a25_a85_a30) \land $ \\ 
 $ E3L0(a12) \land $ \\ 
 $ E3L0(a47) \land $ \\ 
 $ E3L0(a31) \land $ \\ 
 $ E3L0(a21) \land $ \\ 
 $ E3L0(a24_a5) \land $ \\ 
 $ E3L0(a79_a34_a15_a69_a40) \land $ \\ 
 $ E3L0(a70) \land $ \\ 
 $ E3L0(a4_a36) \land $ \\ 
 $ E3L0(a39) \land $ \\ 
 $ E3L0(a80_a29_a95_a73) \land $ \\ 
 $ E3L0(a98) \land $ \\ 
 $ E3L0(a77_a22_a32_a54_a46_a68_a23_a67_a37_a16_a7_a8_a91_a9_a82_a81_a84_a100_a62_a20_a64_a41_a63_a74) \land $ \\ 
 $ E3L0(a56) \land $ \\ 
 $ E3L0(a1) \land $ \\ 
 $ E3L0(a11_a43) \land $ \\ 
 $ E3L0(a57) \land $ \\ 
 $ E3L0(a35) \land $ \\ 
 $ E3L0(a99) \land $ \\ 
 $ E3L0(a19_a97_a75) \land $ \\ 
 $ E3L0(a33_a44_a60) \land $ \\ 
 $ E3L0(a88_a61) \land $ \\ 
 $ E3L0(a13) \land $ \\ 
 $ E3L0(a26) \land $ \\ 
 $ E3L0(a86) \land $ \\ 
 $ E3L0(a76_a6_a92) \land $ \\ 
 $ E3L0(a89) \land $ \\ 
 $ E3L0(a55_a45_a27_a38) \land $ \\ 
 $ E3L0(a3) \land $ \\ 
 $  \Rnext E3L0(a48) \land $ \\ 
 $ E3L0(a17) \land $ \\ 
 $ E3L0(a10_a52) \land $ \\ 
 $ E3L0(a18) \land $ \\ 
 $ E3L0(a59) \land $ \\ 
 $ E3L0(a2_a90) \land $ \\ 
 $ E3L0(a72) \land $ \\ 
 $ E3L0(a65) \land $ \\ 
 $ E3L0(a83) \land $ \\ 
 $ E3L0(a51) \land $ \\ 
 $ E3L0(a28) \land $ \\ 
 $ E3L0(a94_a53) \land $ \\ 
 $ E3L0(a50) \land $ \\ 
 $ E3L0(a48) \land $ \\ 
 $  \Rnext C1(a79_a34_a15_a69_a40) \land $ \\ 
 $  \Rnext  \Rnext C1(a77_a22_a32_a54_a46_a68_a23_a67_a37_a16_a7_a8_a91_a9_a82_a81_a84_a100_a62_a20_a64_a41_a63_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a83) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a33_a44_a60) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a19_a97_a75) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a13) \land $ \\ 
 $  \Rnext E3L0(a35) \land $ \\ 
 $  \Rnext E3L0Inv(a55_a45_a27_a38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a57) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a86) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a28) \land $ \\ 
 $  \Rnext E3L0(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a1) \land $ \\ 
 $  \Rnext C0(a11_a43) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a78_a96) \land $ \\ 
 $  \Rnext E3L1(a83) \land $ \\ 
 $  \Rnext E3L1(a28) \land $ \\ 
 $  \Rnext E3L0Inv(a10_a52) \land $ \\ 
 $  \Rnext  \Rnext C0(a89) \land $ \\ 
 $  \Rnext E3L1(a98) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a42) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a3) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a48) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a2_a90) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a76_a6_a92) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a24_a5) \land $ \\ 
 $  \Rnext E3L1(a70) \land $ \\ 
 $  \Rnext E3L0Inv(a70) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a57) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a99) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a1) \land $ \\ 
 $  \Rnext  \Rnext C1(a11_a43) \land $ \\ 
 $  \Rnext  \Rnext C0(a77_a22_a32_a54_a46_a68_a23_a67_a37_a16_a7_a8_a91_a9_a82_a81_a84_a100_a62_a20_a64_a41_a63_a74))$ 
\end{document}