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


$((PG0 \rightarrow E1G0Inv(dG0Inv)) \land $ \\ 
 $  \forall X. ( \Rbox (((E2L1(X) \land $ \\ 
 $ E2G0(X) \land $ \\ 
 $ E1G1(X)) \rightarrow (C0(X) \land $ \\ 
 $ E3L0(X) \land $ \\ 
 $ C1(X))) \land $ \\ 
 $ ( \Rdiamond (E1L1(X) \land $ \\ 
 $  \Rbox C0(X)) \rightarrow  \Rbox (C0(X) \land $ \\ 
 $  \Rnext C1(X))) \land $ \\ 
 $ ((C1(X) \land $ \\ 
 $ E2L0(X) \land $ \\ 
 $ E3L0(X)) \rightarrow ( \Rnext C1(X) \land $ \\ 
 $  \Rbox E1G0(X))) \land $ \\ 
 $ (( \Rbox E2L0(X) \land $ \\ 
 $  \Rnext C1(X)) \rightarrow  \Rdiamond (E3L1(X) \land $ \\ 
 $  \Rnext E3L0(X))) \land $ \\ 
 $ ( \Rbox (E2G0(X) \land $ \\ 
 $  \Rbox E2G1(X)) \rightarrow  \Rbox (C0(X) \land $ \\ 
 $  \Rnext E2G0(X))) \land $ \\ 
 $ ( \Rbox  \Rbox (E3L1(X) \land $ \\ 
 $ C0(X)) \rightarrow ( \Rdiamond E2L0(X) \land $ \\ 
 $  \Rnext C0(X))) \land $ \\ 
 $ (( \Rnext C1(X) \land $ \\ 
 $  \Rdiamond E3G1(X)) \rightarrow (C1(X) \land $ \\ 
 $ E1L0(X))) \land $ \\ 
 $ ( \Rdiamond (C0(X) \land $ \\ 
 $  \Rnext E3L0(X)) \rightarrow  \Rdiamond (C0(X) \land $ \\ 
 $  \Rnext E2G1(X))) \land $ \\ 
 $ ((C0(X) \land $ \\ 
 $ C0(X) \land $ \\ 
 $ E3G0(X)) \rightarrow ( \Rdiamond E3L1(X) \land $ \\ 
 $  \Rdiamond E3G1(X))) \land $ \\ 
 $ (( \Rnext E2G1(X) \land $ \\ 
 $  \Rbox E3L1(X)) \rightarrow  \Rbox (E3G1(X) \land $ \\ 
 $  \Rnext C0(X))) \land $ \\ 
 $ (E3L1(X) \rightarrow E2L1(X)) \land $ \\ 
 $ (E2G1(X) \rightarrow E1G1(X)) \land $ \\ 
 $ (E2G0(X) \rightarrow E1G0(X)) \land $ \\ 
 $ (E3G1(X) \rightarrow E2G1(X)) \land $ \\ 
 $ (E3L0(X) \rightarrow E2L0(X)) \land $ \\ 
 $ (E2L0(X) \rightarrow E1L0(X)) \land $ \\ 
 $ (E3G0(X) \rightarrow E2G0(X)) \land $ \\ 
 $ (E2L1(X) \rightarrow E1L1(X))) \land $ \\ 
 $ ( \Rdiamond E1G1Inv(X) \rightarrow  \Rbox E1G1Inv(X)) \land $ \\ 
 $ ( \Rdiamond E1G0(X) \rightarrow  \Rbox PG0) \land $ \\ 
 $ ( \Rdiamond E2G1(X) \rightarrow  \Rbox E2G1(X)) \land $ \\ 
 $ ( \Rdiamond E1G1Inv(X) \rightarrow  \Rbox PinvG1) \land $ \\ 
 $ ( \Rdiamond E1G0(X) \rightarrow  \Rbox E1G0(X)) \land $ \\ 
 $ ( \Rdiamond E1L0Inv(X) \rightarrow  \Rbox PinvL0) \land $ \\ 
 $ ( \Rdiamond E1G0Inv(X) \rightarrow  \Rbox PinvG0) \land $ \\ 
 $ ( \Rdiamond E2G0(X) \rightarrow  \Rbox E2G0(X)) \land $ \\ 
 $ ( \Rdiamond E1G1(X) \rightarrow  \Rbox E1G1(X)) \land $ \\ 
 $ ( \Rdiamond E1G1(X) \rightarrow  \Rbox PG1) \land $ \\ 
 $ ( \Rdiamond E1L0(X) \rightarrow  \Rbox PL0) \land $ \\ 
 $ ( \Rdiamond E1L1Inv(X) \rightarrow  \Rbox PinvL1) \land $ \\ 
 $ ( \Rdiamond E1L1(X) \rightarrow  \Rbox PL1) \land $ \\ 
 $ ( \Rdiamond E3G0(X) \rightarrow  \Rbox E3G0(X)) \land $ \\ 
 $ ( \Rdiamond E3G1(X) \rightarrow  \Rbox E3G1(X)) \land $ \\ 
 $ ( \Rdiamond E1G0Inv(X) \rightarrow  \Rbox E1G0Inv(X))) \land $ \\ 
 $ (PL0 \rightarrow E1L0Inv(dL0Inv)) \land $ \\ 
 $ (PinvL1 \rightarrow E1L1(dL1)) \land $ \\ 
 $ (PinvG1 \rightarrow E1G1(dG1)) \land $ \\ 
 $ (PinvG0 \rightarrow E1G0(dG0)) \land $ \\ 
 $ (PG1 \rightarrow E1G1Inv(dG1Inv)) \land $ \\ 
 $ (PinvL0 \rightarrow E1L0(dL0)) \land $ \\ 
 $ (PL1 \rightarrow E1L1Inv(dL1Inv)) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a45) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a98_a26_a28_a19_a70) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a5) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a10_a81_a92) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a21_a79_a47_a82_a51) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a46) \land $ \\ 
 $  \Rnext  \Rnext C1(a11_a33_a76_a32_a13_a35_a57_a78_a12_a34_a15_a37_a14_a58_a38_a80_a60_a84_a40_a100_a62_a63_a88_a43_a23_a67_a69_a49_a2_a3_a4_a6_a90_a94_a50_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a22) \land $ \\ 
 $  \Rnext C0(a45) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a98_a26_a28_a19_a70) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a44) \land $ \\ 
 $  \Rnext  \Rnext C0(a24) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a10_a81_a92) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a46) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a61) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a11_a33_a76_a32_a13_a35_a57_a78_a12_a34_a15_a37_a14_a58_a38_a80_a60_a84_a40_a100_a62_a63_a88_a43_a23_a67_a69_a49_a2_a3_a4_a6_a90_a94_a50_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a10_a81_a92) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a8_a18_a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a99_a72) \land $ \\ 
 $  \Rnext  \Rnext C1(a89_a36_a29_a42_a52) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a71) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a11_a33_a76_a32_a13_a35_a57_a78_a12_a34_a15_a37_a14_a58_a38_a80_a60_a84_a40_a100_a62_a63_a88_a43_a23_a67_a69_a49_a2_a3_a4_a6_a90_a94_a50_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a16_a96) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a24) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a54) \land $ \\ 
 $  \Rnext E3L1Inv(a98_a26_a28_a19_a70) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a5) \land $ \\ 
 $  \Rnext C0(a24) \land $ \\ 
 $  \Rnext  \Rnext C1(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a16_a96) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a16_a96) \land $ \\ 
 $  \Rnext E3L0(a39_a20) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a46) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a77) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a99_a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a99_a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a21_a79_a47_a82_a51) \land $ \\ 
 $  \Rnext E3L1(a22) \land $ \\ 
 $  \Rnext C1(a46) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a39_a20) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a9_a86_a97_a41) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a54) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a66_a1_a48_a93) \land $ \\ 
 $  \Rnext C1(a45) \land $ \\ 
 $  \Rnext C1(a9_a86_a97_a41) \land $ \\ 
 $  \Rnext E3L0(a7_a64) \land $ \\ 
 $  \Rnext  \Rnext C1(a59_a25_a17_a91_a83) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a22) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a85) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a61) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a45) \land $ \\ 
 $  \Rnext  \Rnext C1(a68_a56) \land $ \\ 
 $  \Rnext E3L0(a55) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a27) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a27) \land $ \\ 
 $  \Rnext  \Rnext C1(a66_a1_a48_a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a10_a81_a92) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a5) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a59_a25_a17_a91_a83) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a54) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a22) \land $ \\ 
 $  \Rnext E3L0Inv(a53) \land $ \\ 
 $  \Rnext E3L1Inv(a10_a81_a92) \land $ \\ 
 $  \Rnext  \Rnext C0(a45) \land $ \\ 
 $  \Rnext C1(a24) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a46) \land $ \\ 
 $  \Rnext E3L0Inv(a45) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a77) \land $ \\ 
 $  \Rnext C1(a89_a36_a29_a42_a52) \land $ \\ 
 $  \Rnext  \Rnext C0(a98_a26_a28_a19_a70) \land $ \\ 
 $  \Rnext E3L1Inv(a59_a25_a17_a91_a83) \land $ \\ 
 $  \Rnext  \Rnext C1(a5) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a8_a18_a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a98_a26_a28_a19_a70) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a9_a86_a97_a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a59_a25_a17_a91_a83) \land $ \\ 
 $  \Rnext E3L0Inv(a54) \land $ \\ 
 $  \Rnext E3L0Inv(a22) \land $ \\ 
 $  \Rnext E3L1(a68_a56) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a85) \land $ \\ 
 $  \Rnext E3L0Inv(a87) \land $ \\ 
 $ E1G1Inv(a71) \land $ \\ 
 $ E1G1Inv(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a65) \land $ \\ 
 $ E1G1Inv(a21_a79_a47_a82_a51) \land $ \\ 
 $ E1G1Inv(a5) \land $ \\ 
 $ E1G1Inv(a8_a18_a73) \land $ \\ 
 $ E1G1Inv(a27) \land $ \\ 
 $ E1G1Inv(a66_a1_a48_a93) \land $ \\ 
 $ E1G1Inv(a55) \land $ \\ 
 $ E1G1Inv(a54) \land $ \\ 
 $ E1G1Inv(a16_a96) \land $ \\ 
 $ E1G1Inv(a10_a81_a92) \land $ \\ 
 $ E1G1Inv(a53) \land $ \\ 
 $ E1G1Inv(a61) \land $ \\ 
 $ E1G1Inv(a89_a36_a29_a42_a52) \land $ \\ 
 $ E1G1Inv(a7_a64) \land $ \\ 
 $ E1G1Inv(a65) \land $ \\ 
 $ E1G1Inv(a98_a26_a28_a19_a70) \land $ \\ 
 $ E1G1Inv(a45) \land $ \\ 
 $ E1G1Inv(a11_a33_a76_a32_a13_a35_a57_a78_a12_a34_a15_a37_a14_a58_a38_a80_a60_a84_a40_a100_a62_a63_a88_a43_a23_a67_a69_a49_a2_a3_a4_a6_a90_a94_a50_a31_a75_a74) \land $ \\ 
 $ E1G1Inv(a99_a72) \land $ \\ 
 $ E1G1Inv(a24) \land $ \\ 
 $ E1G1Inv(a59_a25_a17_a91_a83) \land $ \\ 
 $ E1G1Inv(a46) \land $ \\ 
 $ E1G1Inv(a77) \land $ \\ 
 $ E1G1Inv(a9_a86_a97_a41) \land $ \\ 
 $ E1G1Inv(a68_a56) \land $ \\ 
 $ E1G1Inv(a22) \land $ \\ 
 $ E1G1Inv(a95) \land $ \\ 
 $ E1G1Inv(a30) \land $ \\ 
 $ E1G1Inv(a85) \land $ \\ 
 $ E1G1Inv(a44) \land $ \\ 
 $ E1G1Inv(a39_a20) \land $ \\ 
 $  \Rnext  \Rnext C0(a99_a72) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a16_a96) \land $ \\ 
 $  \Rnext C0(a10_a81_a92) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a45) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a65) \land $ \\ 
 $  \Rnext  \Rnext C0(a66_a1_a48_a93) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a68_a56) \land $ \\ 
 $  \Rnext  \Rnext C1(a53) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a53) \land $ \\ 
 $  \Rnext E3L0(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a8_a18_a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a7_a64) \land $ \\ 
 $  \Rnext E3L0Inv(a85) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a95) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a21_a79_a47_a82_a51) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a99_a72) \land $ \\ 
 $  \Rnext E3L1(a66_a1_a48_a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a55) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a10_a81_a92) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a89_a36_a29_a42_a52) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a8_a18_a73) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a21_a79_a47_a82_a51) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a8_a18_a73) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a45) \land $ \\ 
 $  \Rnext E3L1(a65) \land $ \\ 
 $  \Rnext C1(a68_a56) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a89_a36_a29_a42_a52) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a55) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a66_a1_a48_a93) \land $ \\ 
 $  \Rnext C1(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a55) \land $ \\ 
 $  \Rnext E3L0(a5) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a89_a36_a29_a42_a52) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a45) \land $ \\ 
 $  \Rnext  \Rnext C0(a21_a79_a47_a82_a51) \land $ \\ 
 $  \Rnext C1(a77) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a11_a33_a76_a32_a13_a35_a57_a78_a12_a34_a15_a37_a14_a58_a38_a80_a60_a84_a40_a100_a62_a63_a88_a43_a23_a67_a69_a49_a2_a3_a4_a6_a90_a94_a50_a31_a75_a74) \land $ \\ 
 $ E3G0(a10_a81_a92) \land $ \\ 
 $ E3G0(a27) \land $ \\ 
 $ E3G0(a66_a1_a48_a93) \land $ \\ 
 $ E3G0(a9_a86_a97_a41) \land $ \\ 
 $ E3G0(a61) \land $ \\ 
 $ E3G0(a39_a20) \land $ \\ 
 $ E3G0(a7_a64) \land $ \\ 
 $ E3G0(a24) \land $ \\ 
 $ E3G0(a98_a26_a28_a19_a70) \land $ \\ 
 $ E3G0(a71) \land $ \\ 
 $ E3G0(a65) \land $ \\ 
 $ E3G0(a85) \land $ \\ 
 $ E3G0(a55) \land $ \\ 
 $ E3G0(a46) \land $ \\ 
 $ E3G0(a54) \land $ \\ 
 $ E3G0(a11_a33_a76_a32_a13_a35_a57_a78_a12_a34_a15_a37_a14_a58_a38_a80_a60_a84_a40_a100_a62_a63_a88_a43_a23_a67_a69_a49_a2_a3_a4_a6_a90_a94_a50_a31_a75_a74) \land $ \\ 
 $ E3G0(a30) \land $ \\ 
 $ E3G0(a22) \land $ \\ 
 $ E3G0(a21_a79_a47_a82_a51) \land $ \\ 
 $ E3G0(a87) \land $ \\ 
 $ E3G0(a5) \land $ \\ 
 $ E3G0(a95) \land $ \\ 
 $ E3G0(a16_a96) \land $ \\ 
 $ E3G0(a8_a18_a73) \land $ \\ 
 $ E3G0(a99_a72) \land $ \\ 
 $ E3G0(a53) \land $ \\ 
 $ E3G0(a59_a25_a17_a91_a83) \land $ \\ 
 $ E3G0(a45) \land $ \\ 
 $ E3G0(a77) \land $ \\ 
 $ E3G0(a44) \land $ \\ 
 $ E3G0(a68_a56) \land $ \\ 
 $ E3G0(a89_a36_a29_a42_a52) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a39_a20) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a95) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a22) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a77) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a55) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a10_a81_a92) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a24) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a87) \land $ \\ 
 $  \Rnext C1(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a98_a26_a28_a19_a70) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a53) \land $ \\ 
 $  \Rnext E3L1Inv(a27) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a24) \land $ \\ 
 $  \Rnext E3L0Inv(a7_a64) \land $ \\ 
 $  \Rnext E3L0Inv(a61) \land $ \\ 
 $  \Rnext E3L0Inv(a77) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a21_a79_a47_a82_a51) \land $ \\ 
 $  \Rnext E3L1Inv(a11_a33_a76_a32_a13_a35_a57_a78_a12_a34_a15_a37_a14_a58_a38_a80_a60_a84_a40_a100_a62_a63_a88_a43_a23_a67_a69_a49_a2_a3_a4_a6_a90_a94_a50_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a27) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a95) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a46) \land $ \\ 
 $  \Rnext C0(a9_a86_a97_a41) \land $ \\ 
 $  \Rnext E3L1(a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a9_a86_a97_a41) \land $ \\ 
 $  \Rnext C0(a53) \land $ \\ 
 $  \Rnext E3L1(a87) \land $ \\ 
 $  \Rnext E3L1(a59_a25_a17_a91_a83) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a89_a36_a29_a42_a52) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a95) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a59_a25_a17_a91_a83) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a68_a56) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a8_a18_a73) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a87) \land $ \\ 
 $  \Rnext E3L1Inv(a39_a20) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a8_a18_a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a71) \land $ \\ 
 $  \Rnext E3L1(a10_a81_a92) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a61) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a61) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a9_a86_a97_a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a61) \land $ \\ 
 $  \Rnext  \Rnext C1(a98_a26_a28_a19_a70) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a89_a36_a29_a42_a52) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a5) \land $ \\ 
 $  \Rnext E3L0(a16_a96) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a8_a18_a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a45) \land $ \\ 
 $  \Rnext C1(a59_a25_a17_a91_a83) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a9_a86_a97_a41) \land $ \\ 
 $  \Rnext  \Rnext C0(a9_a86_a97_a41) \land $ \\ 
 $  \Rnext  \Rnext C0(a10_a81_a92) \land $ \\ 
 $  \Rnext E3L1(a54) \land $ \\ 
 $  \Rnext C0(a5) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a53) \land $ \\ 
 $  \Rnext C0(a7_a64) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a21_a79_a47_a82_a51) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a61) \land $ \\ 
 $  \Rnext  \Rnext C1(a21_a79_a47_a82_a51) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a77) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a16_a96) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a24) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a22) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a55) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a39_a20) \land $ \\ 
 $  \Rnext E3L0Inv(a27) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a39_a20) \land $ \\ 
 $  \Rnext E3L1Inv(a53) \land $ \\ 
 $  \Rnext E3L0(a46) \land $ \\ 
 $  \Rnext E3L0(a65) \land $ \\ 
 $  \Rnext E3L1(a89_a36_a29_a42_a52) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a89_a36_a29_a42_a52) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a89_a36_a29_a42_a52) \land $ \\ 
 $  \Rnext E3L1Inv(a54) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a89_a36_a29_a42_a52) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a66_a1_a48_a93) \land $ \\ 
 $  \Rnext E3L0(a44) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a21_a79_a47_a82_a51) \land $ \\ 
 $  \Rnext  \Rnext C1(a27) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a59_a25_a17_a91_a83) \land $ \\ 
 $  \Rnext E3L1(a7_a64) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a16_a96) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a59_a25_a17_a91_a83) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a85) \land $ \\ 
 $  \Rnext E3L0(a21_a79_a47_a82_a51) \land $ \\ 
 $  \Rnext C1(a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a39_a20) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a59_a25_a17_a91_a83) \land $ \\ 
 $  \Rnext E3L1(a11_a33_a76_a32_a13_a35_a57_a78_a12_a34_a15_a37_a14_a58_a38_a80_a60_a84_a40_a100_a62_a63_a88_a43_a23_a67_a69_a49_a2_a3_a4_a6_a90_a94_a50_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a7_a64) \land $ \\ 
 $  \Rnext E3L0Inv(a99_a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a22) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a66_a1_a48_a93) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a71) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a39_a20) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a22) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a68_a56) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a99_a72) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a21_a79_a47_a82_a51) \land $ \\ 
 $  \Rnext E3L1(a27) \land $ \\ 
 $  \Rnext E3L1(a8_a18_a73) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a87) \land $ \\ 
 $  \Rnext E3L1Inv(a9_a86_a97_a41) \land $ \\ 
 $  \Rnext  \Rnext C1(a55) \land $ \\ 
 $  \Rnext E3L0Inv(a5) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a21_a79_a47_a82_a51) \land $ \\ 
 $  \Rnext E3L0(a98_a26_a28_a19_a70) \land $ \\ 
 $  \Rnext E3L0(a66_a1_a48_a93) \land $ \\ 
 $  \Rnext E3L1Inv(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a5) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a5) \land $ \\ 
 $  \Rnext E3L0(a89_a36_a29_a42_a52) \land $ \\ 
 $  \Rnext E3L1(a53) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a59_a25_a17_a91_a83) \land $ \\ 
 $ E3L1Inv(a66_a1_a48_a93) \land $ \\ 
 $ E3L1Inv(a71) \land $ \\ 
 $ E3L1Inv(a21_a79_a47_a82_a51) \land $ \\ 
 $ E3L1Inv(a45) \land $ \\ 
 $ E3L1Inv(a16_a96) \land $ \\ 
 $ E3L1Inv(a95) \land $ \\ 
 $ E3L1Inv(a98_a26_a28_a19_a70) \land $ \\ 
 $ E3L1Inv(a87) \land $ \\ 
 $ E3L1Inv(a27) \land $ \\ 
 $ E3L1Inv(a59_a25_a17_a91_a83) \land $ \\ 
 $  \Rnext E3L0Inv(a8_a18_a73) \land $ \\ 
 $ E3L1Inv(a55) \land $ \\ 
 $ E3L1Inv(a8_a18_a73) \land $ \\ 
 $ E3L1Inv(a77) \land $ \\ 
 $ E3L1Inv(a10_a81_a92) \land $ \\ 
 $ E3L1Inv(a68_a56) \land $ \\ 
 $ E3L1Inv(a5) \land $ \\ 
 $ E3L1Inv(a89_a36_a29_a42_a52) \land $ \\ 
 $ E3L1Inv(a54) \land $ \\ 
 $ E3L1Inv(a11_a33_a76_a32_a13_a35_a57_a78_a12_a34_a15_a37_a14_a58_a38_a80_a60_a84_a40_a100_a62_a63_a88_a43_a23_a67_a69_a49_a2_a3_a4_a6_a90_a94_a50_a31_a75_a74) \land $ \\ 
 $ E3L1Inv(a39_a20) \land $ \\ 
 $ E3L1Inv(a85) \land $ \\ 
 $ E3L1Inv(a24) \land $ \\ 
 $ E3L1Inv(a7_a64) \land $ \\ 
 $ E3L1Inv(a99_a72) \land $ \\ 
 $ E3L1Inv(a53) \land $ \\ 
 $ E3L1Inv(a9_a86_a97_a41) \land $ \\ 
 $ E3L1Inv(a46) \land $ \\ 
 $ E3L1Inv(a22) \land $ \\ 
 $ E3L1Inv(a44) \land $ \\ 
 $ E3L1Inv(a61) \land $ \\ 
 $ E3L1Inv(a30) \land $ \\ 
 $ E3L1Inv(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a10_a81_a92) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a53) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a8_a18_a73) \land $ \\ 
 $  \Rnext E3L1(a55) \land $ \\ 
 $ C1(a27) \land $ \\ 
 $ C1(a61) \land $ \\ 
 $ C1(a66_a1_a48_a93) \land $ \\ 
 $ C1(a65) \land $ \\ 
 $ C1(a8_a18_a73) \land $ \\ 
 $ C1(a5) \land $ \\ 
 $ C1(a10_a81_a92) \land $ \\ 
 $ C1(a30) \land $ \\ 
 $ C1(a99_a72) \land $ \\ 
 $ C1(a89_a36_a29_a42_a52) \land $ \\ 
 $ C1(a39_a20) \land $ \\ 
 $ C1(a85) \land $ \\ 
 $ C1(a59_a25_a17_a91_a83) \land $ \\ 
 $ C1(a16_a96) \land $ \\ 
 $ C1(a9_a86_a97_a41) \land $ \\ 
 $ C1(a68_a56) \land $ \\ 
 $ C1(a7_a64) \land $ \\ 
 $ C1(a87) \land $ \\ 
 $ C1(a98_a26_a28_a19_a70) \land $ \\ 
 $ C1(a44) \land $ \\ 
 $ C1(a22) \land $ \\ 
 $ C1(a71) \land $ \\ 
 $ C1(a46) \land $ \\ 
 $ C1(a11_a33_a76_a32_a13_a35_a57_a78_a12_a34_a15_a37_a14_a58_a38_a80_a60_a84_a40_a100_a62_a63_a88_a43_a23_a67_a69_a49_a2_a3_a4_a6_a90_a94_a50_a31_a75_a74) \land $ \\ 
 $ C1(a53) \land $ \\ 
 $ C1(a55) \land $ \\ 
 $ C1(a95) \land $ \\ 
 $ C1(a24) \land $ \\ 
 $ C1(a54) \land $ \\ 
 $  \Rnext C0(a46) \land $ \\ 
 $  \Rnext  \Rnext C1(a99_a72) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a65) \land $ \\ 
 $  \Rnext  \Rnext C1(a7_a64) \land $ \\ 
 $  \Rnext E3L1Inv(a65) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a22) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a7_a64) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a87) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a59_a25_a17_a91_a83) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a55) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a27) \land $ \\ 
 $  \Rnext E3L0Inv(a9_a86_a97_a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a7_a64) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a46) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a66_a1_a48_a93) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a5) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a65) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a16_a96) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a30) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a5) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a8_a18_a73) \land $ \\ 
 $  \Rnext C0(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a77) \land $ \\ 
 $  \Rnext C1(a11_a33_a76_a32_a13_a35_a57_a78_a12_a34_a15_a37_a14_a58_a38_a80_a60_a84_a40_a100_a62_a63_a88_a43_a23_a67_a69_a49_a2_a3_a4_a6_a90_a94_a50_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a55) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a39_a20) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a68_a56) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a99_a72) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a65) \land $ \\ 
 $  \Rnext E3L0(a68_a56) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a98_a26_a28_a19_a70) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a68_a56) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a9_a86_a97_a41) \land $ \\ 
 $  \Rnext  \Rnext C0(a16_a96) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a22) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a10_a81_a92) \land $ \\ 
 $ E3L1(a99_a72) \land $ \\ 
 $ E3L1(a16_a96) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a39_a20) \land $ \\ 
 $ E3L1(a68_a56) \land $ \\ 
 $ E3L1(a87) \land $ \\ 
 $ E3L1(a71) \land $ \\ 
 $ E3L1(a27) \land $ \\ 
 $ E3L1(a98_a26_a28_a19_a70) \land $ \\ 
 $ E3L1(a45) \land $ \\ 
 $ E3L1(a7_a64) \land $ \\ 
 $ E3L1(a46) \land $ \\ 
 $ E3L1(a77) \land $ \\ 
 $ E3L1(a5) \land $ \\ 
 $ E3L1(a66_a1_a48_a93) \land $ \\ 
 $ E3L1(a24) \land $ \\ 
 $ E3L1(a53) \land $ \\ 
 $ E3L1(a22) \land $ \\ 
 $ E3L1(a30) \land $ \\ 
 $ E3L1(a85) \land $ \\ 
 $ E3L1(a21_a79_a47_a82_a51) \land $ \\ 
 $ E3L1(a89_a36_a29_a42_a52) \land $ \\ 
 $ E3L1(a44) \land $ \\ 
 $ E3L1(a61) \land $ \\ 
 $ E3L1(a55) \land $ \\ 
 $ E3L1(a8_a18_a73) \land $ \\ 
 $ E3L1(a95) \land $ \\ 
 $ E3L1(a11_a33_a76_a32_a13_a35_a57_a78_a12_a34_a15_a37_a14_a58_a38_a80_a60_a84_a40_a100_a62_a63_a88_a43_a23_a67_a69_a49_a2_a3_a4_a6_a90_a94_a50_a31_a75_a74) \land $ \\ 
 $ E3L1(a54) \land $ \\ 
 $ E3L1(a39_a20) \land $ \\ 
 $ E3L1(a65) \land $ \\ 
 $ E3L1(a59_a25_a17_a91_a83) \land $ \\ 
 $ E3L1(a10_a81_a92) \land $ \\ 
 $ E3L1(a9_a86_a97_a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a55) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a98_a26_a28_a19_a70) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a95) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a22) \land $ \\ 
 $  \Rnext E3L0(a9_a86_a97_a41) \land $ \\ 
 $  \Rnext  \Rnext C1(a10_a81_a92) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a44) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a66_a1_a48_a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a11_a33_a76_a32_a13_a35_a57_a78_a12_a34_a15_a37_a14_a58_a38_a80_a60_a84_a40_a100_a62_a63_a88_a43_a23_a67_a69_a49_a2_a3_a4_a6_a90_a94_a50_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a77) \land $ \\ 
 $  \Rnext E3L0Inv(a55) \land $ \\ 
 $  \Rnext E3L0(a99_a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a27) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a61) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a54) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a46) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a7_a64) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a46) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a21_a79_a47_a82_a51) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a11_a33_a76_a32_a13_a35_a57_a78_a12_a34_a15_a37_a14_a58_a38_a80_a60_a84_a40_a100_a62_a63_a88_a43_a23_a67_a69_a49_a2_a3_a4_a6_a90_a94_a50_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a55) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a99_a72) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a77) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a89_a36_a29_a42_a52) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a85) \land $ \\ 
 $  \Rnext E3L1(a46) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a61) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a98_a26_a28_a19_a70) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a22) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a77) \land $ \\ 
 $  \Rnext C1(a7_a64) \land $ \\ 
 $  \Rnext E3L0(a87) \land $ \\ 
 $  \Rnext E3L1Inv(a99_a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a24) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a7_a64) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a61) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a5) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a55) \land $ \\ 
 $  \Rnext E3L0Inv(a59_a25_a17_a91_a83) \land $ \\ 
 $  \Rnext E3L0(a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a45) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a68_a56) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a10_a81_a92) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a53) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a39_a20) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a59_a25_a17_a91_a83) \land $ \\ 
 $  \Rnext  \Rnext C0(a46) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a77) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a7_a64) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a5) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a87) \land $ \\ 
 $  \Rnext  \Rnext C1(a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a27) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a10_a81_a92) \land $ \\ 
 $  \Rnext E3L0Inv(a44) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a5) \land $ \\ 
 $  \Rnext  \Rnext C0(a11_a33_a76_a32_a13_a35_a57_a78_a12_a34_a15_a37_a14_a58_a38_a80_a60_a84_a40_a100_a62_a63_a88_a43_a23_a67_a69_a49_a2_a3_a4_a6_a90_a94_a50_a31_a75_a74) \land $ \\ 
 $  \Rnext E3L0Inv(a46) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a66_a1_a48_a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a11_a33_a76_a32_a13_a35_a57_a78_a12_a34_a15_a37_a14_a58_a38_a80_a60_a84_a40_a100_a62_a63_a88_a43_a23_a67_a69_a49_a2_a3_a4_a6_a90_a94_a50_a31_a75_a74) \land $ \\ 
 $  \Rnext E3L0(a8_a18_a73) \land $ \\ 
 $  \Rnext C0(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a99_a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a8_a18_a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a65) \land $ \\ 
 $  \Rnext E3L0Inv(a89_a36_a29_a42_a52) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a99_a72) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a8_a18_a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a27) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a99_a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a66_a1_a48_a93) \land $ \\ 
 $  \Rnext C0(a68_a56) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a66_a1_a48_a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a68_a56) \land $ \\ 
 $  \Rnext  \Rnext C1(a39_a20) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a65) \land $ \\ 
 $  \Rnext C1(a39_a20) \land $ \\ 
 $  \Rnext C0(a30) \land $ \\ 
 $  \Rnext  \Rnext C0(a87) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a9_a86_a97_a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a44) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a99_a72) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a21_a79_a47_a82_a51) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a5) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a59_a25_a17_a91_a83) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a44) \land $ \\ 
 $  \Rnext C1(a98_a26_a28_a19_a70) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a59_a25_a17_a91_a83) \land $ \\ 
 $  \Rnext E3L0Inv(a24) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a89_a36_a29_a42_a52) \land $ \\ 
 $  \Rnext E3L1Inv(a8_a18_a73) \land $ \\ 
 $  \Rnext E3L1Inv(a85) \land $ \\ 
 $  \Rnext E3L1Inv(a44) \land $ \\ 
 $  \Rnext E3L1(a95) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a10_a81_a92) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a87) \land $ \\ 
 $  \Rnext E3L1(a5) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a68_a56) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a45) \land $ \\ 
 $ E3L0Inv(a9_a86_a97_a41) \land $ \\ 
 $ E3L0Inv(a21_a79_a47_a82_a51) \land $ \\ 
 $ E3L0Inv(a44) \land $ \\ 
 $ E3L0Inv(a30) \land $ \\ 
 $ E3L0Inv(a71) \land $ \\ 
 $ E3L0Inv(a24) \land $ \\ 
 $ E3L0Inv(a8_a18_a73) \land $ \\ 
 $ E3L0Inv(a27) \land $ \\ 
 $ E3L0Inv(a66_a1_a48_a93) \land $ \\ 
 $ E3L0Inv(a45) \land $ \\ 
 $ E3L0Inv(a95) \land $ \\ 
 $ E3L0Inv(a39_a20) \land $ \\ 
 $ E3L0Inv(a77) \land $ \\ 
 $ E3L0Inv(a61) \land $ \\ 
 $ E3L0Inv(a22) \land $ \\ 
 $ E3L0Inv(a54) \land $ \\ 
 $ E3L0Inv(a55) \land $ \\ 
 $ E3L0Inv(a99_a72) \land $ \\ 
 $ E3L0Inv(a98_a26_a28_a19_a70) \land $ \\ 
 $ E3L0Inv(a10_a81_a92) \land $ \\ 
 $ E3L0Inv(a89_a36_a29_a42_a52) \land $ \\ 
 $ E3L0Inv(a7_a64) \land $ \\ 
 $ E3L0Inv(a59_a25_a17_a91_a83) \land $ \\ 
 $ E3L0Inv(a46) \land $ \\ 
 $ E3L0Inv(a16_a96) \land $ \\ 
 $ E3L0Inv(a87) \land $ \\ 
 $ E3L0Inv(a53) \land $ \\ 
 $ E3L0Inv(a65) \land $ \\ 
 $ E3L0Inv(a5) \land $ \\ 
 $ E3L0Inv(a85) \land $ \\ 
 $ E3L0Inv(a68_a56) \land $ \\ 
 $ E3L0Inv(a11_a33_a76_a32_a13_a35_a57_a78_a12_a34_a15_a37_a14_a58_a38_a80_a60_a84_a40_a100_a62_a63_a88_a43_a23_a67_a69_a49_a2_a3_a4_a6_a90_a94_a50_a31_a75_a74) \land $ \\ 
 $  \Rnext E3L0Inv(a65) \land $ \\ 
 $  \Rnext  \Rnext C1(a16_a96) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a68_a56) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a10_a81_a92) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a89_a36_a29_a42_a52) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a54) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a9_a86_a97_a41) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a10_a81_a92) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a98_a26_a28_a19_a70) \land $ \\ 
 $  \Rnext E3L0(a27) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a7_a64) \land $ \\ 
 $  \Rnext E3L0(a11_a33_a76_a32_a13_a35_a57_a78_a12_a34_a15_a37_a14_a58_a38_a80_a60_a84_a40_a100_a62_a63_a88_a43_a23_a67_a69_a49_a2_a3_a4_a6_a90_a94_a50_a31_a75_a74) \land $ \\ 
 $  \Rnext E3L1(a98_a26_a28_a19_a70) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a5) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a54) \land $ \\ 
 $  \Rnext C0(a21_a79_a47_a82_a51) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a46) \land $ \\ 
 $  \Rnext C0(a98_a26_a28_a19_a70) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a54) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a7_a64) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a9_a86_a97_a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a54) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a30) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a11_a33_a76_a32_a13_a35_a57_a78_a12_a34_a15_a37_a14_a58_a38_a80_a60_a84_a40_a100_a62_a63_a88_a43_a23_a67_a69_a49_a2_a3_a4_a6_a90_a94_a50_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a61) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a9_a86_a97_a41) \land $ \\ 
 $  \Rnext E3L0(a59_a25_a17_a91_a83) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a61) \land $ \\ 
 $  \Rnext C0(a99_a72) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a77) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a87) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a7_a64) \land $ \\ 
 $  \Rnext C1(a27) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a68_a56) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a5) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a53) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a16_a96) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a24) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a10_a81_a92) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a46) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a9_a86_a97_a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a89_a36_a29_a42_a52) \land $ \\ 
 $  \Rnext E3L1Inv(a7_a64) \land $ \\ 
 $  \Rnext C0(a77) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a89_a36_a29_a42_a52) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a30) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a10_a81_a92) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a9_a86_a97_a41) \land $ \\ 
 $  \Rnext C1(a55) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a27) \land $ \\ 
 $  \Rnext E3L0Inv(a10_a81_a92) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a24) \land $ \\ 
 $ E3G1(a66_a1_a48_a93) \land $ \\ 
 $ E3G1(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a24) \land $ \\ 
 $ E3G1(a59_a25_a17_a91_a83) \land $ \\ 
 $ E3G1(a16_a96) \land $ \\ 
 $ E3G1(a61) \land $ \\ 
 $ E3G1(a87) \land $ \\ 
 $ E3G1(a27) \land $ \\ 
 $ E3G1(a95) \land $ \\ 
 $ E3G1(a99_a72) \land $ \\ 
 $ E3G1(a98_a26_a28_a19_a70) \land $ \\ 
 $ E3G1(a30) \land $ \\ 
 $ E3G1(a21_a79_a47_a82_a51) \land $ \\ 
 $ E3G1(a22) \land $ \\ 
 $ E3G1(a46) \land $ \\ 
 $ E3G1(a85) \land $ \\ 
 $ E3G1(a89_a36_a29_a42_a52) \land $ \\ 
 $ E3G1(a44) \land $ \\ 
 $ E3G1(a55) \land $ \\ 
 $ E3G1(a54) \land $ \\ 
 $ E3G1(a11_a33_a76_a32_a13_a35_a57_a78_a12_a34_a15_a37_a14_a58_a38_a80_a60_a84_a40_a100_a62_a63_a88_a43_a23_a67_a69_a49_a2_a3_a4_a6_a90_a94_a50_a31_a75_a74) \land $ \\ 
 $ E3G1(a7_a64) \land $ \\ 
 $ E3G1(a77) \land $ \\ 
 $ E3G1(a9_a86_a97_a41) \land $ \\ 
 $ E3G1(a68_a56) \land $ \\ 
 $ E3G1(a5) \land $ \\ 
 $ E3G1(a65) \land $ \\ 
 $ E3G1(a8_a18_a73) \land $ \\ 
 $ E3G1(a45) \land $ \\ 
 $ E3G1(a39_a20) \land $ \\ 
 $ E3G1(a10_a81_a92) \land $ \\ 
 $ E3G1(a24) \land $ \\ 
 $ E3G1(a53) \land $ \\ 
 $  \Rnext E3L1Inv(a89_a36_a29_a42_a52) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a54) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a44) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a45) \land $ \\ 
 $  \Rnext E3L0Inv(a21_a79_a47_a82_a51) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a7_a64) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a77) \land $ \\ 
 $  \Rnext C1(a66_a1_a48_a93) \land $ \\ 
 $  \Rnext E3L0Inv(a30) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a77) \land $ \\ 
 $  \Rnext C0(a22) \land $ \\ 
 $  \Rnext  \Rnext C0(a30) \land $ \\ 
 $  \Rnext E3L0Inv(a16_a96) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a68_a56) \land $ \\ 
 $  \Rnext  \Rnext C0(a8_a18_a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a98_a26_a28_a19_a70) \land $ \\ 
 $  \Rnext  \Rnext C0(a95) \land $ \\ 
 $  \Rnext E3L1Inv(a30) \land $ \\ 
 $  \Rnext E3L1Inv(a5) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a55) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a11_a33_a76_a32_a13_a35_a57_a78_a12_a34_a15_a37_a14_a58_a38_a80_a60_a84_a40_a100_a62_a63_a88_a43_a23_a67_a69_a49_a2_a3_a4_a6_a90_a94_a50_a31_a75_a74) \land $ \\ 
 $  \Rnext C0(a11_a33_a76_a32_a13_a35_a57_a78_a12_a34_a15_a37_a14_a58_a38_a80_a60_a84_a40_a100_a62_a63_a88_a43_a23_a67_a69_a49_a2_a3_a4_a6_a90_a94_a50_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a89_a36_a29_a42_a52) \land $ \\ 
 $  \Rnext E3L0Inv(a95) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a53) \land $ \\ 
 $  \Rnext E3L1(a99_a72) \land $ \\ 
 $  \Rnext E3L0(a95) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a53) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a45) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a95) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a7_a64) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a95) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a66_a1_a48_a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a27) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a24) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a55) \land $ \\ 
 $  \Rnext  \Rnext C0(a44) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a71) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a59_a25_a17_a91_a83) \land $ \\ 
 $  \Rnext E3L0(a61) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a30) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a46) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a5) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a21_a79_a47_a82_a51) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a53) \land $ \\ 
 $  \Rnext E3L1Inv(a77) \land $ \\ 
 $  \Rnext C1(a16_a96) \land $ \\ 
 $  \Rnext E3L1Inv(a22) \land $ \\ 
 $  \Rnext E3L1Inv(a21_a79_a47_a82_a51) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a54) \land $ \\ 
 $  \Rnext E3L1Inv(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a16_a96) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a24) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a45) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a46) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a85) \land $ \\ 
 $  \Rnext  \Rnext C1(a61) \land $ \\ 
 $  \Rnext  \Rnext C0(a77) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a46) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a45) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a99_a72) \land $ \\ 
 $  \Rnext C1(a21_a79_a47_a82_a51) \land $ \\ 
 $  \Rnext C0(a59_a25_a17_a91_a83) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a39_a20) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a61) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a27) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a95) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a55) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a68_a56) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a59_a25_a17_a91_a83) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a45) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a30) \land $ \\ 
 $  \Rnext E3L0Inv(a71) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a66_a1_a48_a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a22) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a16_a96) \land $ \\ 
 $  \Rnext  \Rnext C1(a54) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a27) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a21_a79_a47_a82_a51) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a11_a33_a76_a32_a13_a35_a57_a78_a12_a34_a15_a37_a14_a58_a38_a80_a60_a84_a40_a100_a62_a63_a88_a43_a23_a67_a69_a49_a2_a3_a4_a6_a90_a94_a50_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a5) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a89_a36_a29_a42_a52) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a98_a26_a28_a19_a70) \land $ \\ 
 $  \Rnext E3L1(a30) \land $ \\ 
 $  \Rnext C0(a85) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a68_a56) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a87) \land $ \\ 
 $  \Rnext C0(a61) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a11_a33_a76_a32_a13_a35_a57_a78_a12_a34_a15_a37_a14_a58_a38_a80_a60_a84_a40_a100_a62_a63_a88_a43_a23_a67_a69_a49_a2_a3_a4_a6_a90_a94_a50_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a8_a18_a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a99_a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a44) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a8_a18_a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a85) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a55) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a11_a33_a76_a32_a13_a35_a57_a78_a12_a34_a15_a37_a14_a58_a38_a80_a60_a84_a40_a100_a62_a63_a88_a43_a23_a67_a69_a49_a2_a3_a4_a6_a90_a94_a50_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a98_a26_a28_a19_a70) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a66_a1_a48_a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a59_a25_a17_a91_a83) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a22) \land $ \\ 
 $  \Rnext  \Rnext C0(a68_a56) \land $ \\ 
 $  \Rnext E3L0(a85) \land $ \\ 
 $  \Rnext  \Rnext C1(a71) \land $ \\ 
 $  \Rnext  \Rnext C1(a77) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a39_a20) \land $ \\ 
 $  \Rnext E3L1Inv(a66_a1_a48_a93) \land $ \\ 
 $  \Rnext E3L0(a77) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a9_a86_a97_a41) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a87) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a66_a1_a48_a93) \land $ \\ 
 $  \Rnext E3L1Inv(a95) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a66_a1_a48_a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a55) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a44) \land $ \\ 
 $  \Rnext  \Rnext C1(a8_a18_a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a44) \land $ \\ 
 $  \Rnext E3L1(a45) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a46) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a8_a18_a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a61) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a71) \land $ \\ 
 $  \Rnext C1(a61) \land $ \\ 
 $  \Rnext C1(a22) \land $ \\ 
 $  \Rnext C1(a44) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a24) \land $ \\ 
 $  \Rnext  \Rnext C1(a95) \land $ \\ 
 $  \Rnext E3L0(a54) \land $ \\ 
 $  \Rnext E3L0(a53) \land $ \\ 
 $  \Rnext E3L1(a21_a79_a47_a82_a51) \land $ \\ 
 $  \Rnext E3L1(a44) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a98_a26_a28_a19_a70) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a27) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a59_a25_a17_a91_a83) \land $ \\ 
 $  \Rnext E3L1(a9_a86_a97_a41) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a24) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a45) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a27) \land $ \\ 
 $  \Rnext C1(a10_a81_a92) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a99_a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a53) \land $ \\ 
 $  \Rnext E3L0(a45) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a24) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a44) \land $ \\ 
 $ E1G0Inv(a16_a96) \land $ \\ 
 $ E1G0Inv(a21_a79_a47_a82_a51) \land $ \\ 
 $ E1G0Inv(a27) \land $ \\ 
 $ E1G0Inv(a22) \land $ \\ 
 $ E1G0Inv(a66_a1_a48_a93) \land $ \\ 
 $ E1G0Inv(a99_a72) \land $ \\ 
 $ E1G0Inv(a39_a20) \land $ \\ 
 $ E1G0Inv(a54) \land $ \\ 
 $ E1G0Inv(a24) \land $ \\ 
 $ E1G0Inv(a53) \land $ \\ 
 $ E1G0Inv(a5) \land $ \\ 
 $ E1G0Inv(a45) \land $ \\ 
 $ E1G0Inv(a68_a56) \land $ \\ 
 $ E1G0Inv(a95) \land $ \\ 
 $ E1G0Inv(a55) \land $ \\ 
 $ E1G0Inv(a46) \land $ \\ 
 $ E1G0Inv(a8_a18_a73) \land $ \\ 
 $ E1G0Inv(a10_a81_a92) \land $ \\ 
 $ E1G0Inv(a59_a25_a17_a91_a83) \land $ \\ 
 $ E1G0Inv(a65) \land $ \\ 
 $ E1G0Inv(a61) \land $ \\ 
 $ E1G0Inv(a30) \land $ \\ 
 $ E1G0Inv(a11_a33_a76_a32_a13_a35_a57_a78_a12_a34_a15_a37_a14_a58_a38_a80_a60_a84_a40_a100_a62_a63_a88_a43_a23_a67_a69_a49_a2_a3_a4_a6_a90_a94_a50_a31_a75_a74) \land $ \\ 
 $ E1G0Inv(a71) \land $ \\ 
 $ E1G0Inv(a87) \land $ \\ 
 $ E1G0Inv(a44) \land $ \\ 
 $ E1G0Inv(a89_a36_a29_a42_a52) \land $ \\ 
 $ E1G0Inv(a98_a26_a28_a19_a70) \land $ \\ 
 $ E1G0Inv(a77) \land $ \\ 
 $ E1G0Inv(a85) \land $ \\ 
 $ E1G0Inv(a9_a86_a97_a41) \land $ \\ 
 $ E1G0Inv(a7_a64) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a39_a20) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a53) \land $ \\ 
 $  \Rnext E3L0(a10_a81_a92) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a98_a26_a28_a19_a70) \land $ \\ 
 $  \Rnext E3L0(a24) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a44) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a55) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a77) \land $ \\ 
 $  \Rnext C0(a66_a1_a48_a93) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a9_a86_a97_a41) \land $ \\ 
 $  \Rnext E3L0Inv(a39_a20) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a98_a26_a28_a19_a70) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a22) \land $ \\ 
 $  \Rnext E3L1Inv(a16_a96) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a71) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a68_a56) \land $ \\ 
 $ C0(a21_a79_a47_a82_a51) \land $ \\ 
 $ C0(a27) \land $ \\ 
 $ C0(a16_a96) \land $ \\ 
 $ C0(a24) \land $ \\ 
 $ C0(a8_a18_a73) \land $ \\ 
 $ C0(a98_a26_a28_a19_a70) \land $ \\ 
 $ C0(a99_a72) \land $ \\ 
 $ C0(a59_a25_a17_a91_a83) \land $ \\ 
 $ C0(a7_a64) \land $ \\ 
 $ C0(a71) \land $ \\ 
 $ C0(a9_a86_a97_a41) \land $ \\ 
 $ C0(a11_a33_a76_a32_a13_a35_a57_a78_a12_a34_a15_a37_a14_a58_a38_a80_a60_a84_a40_a100_a62_a63_a88_a43_a23_a67_a69_a49_a2_a3_a4_a6_a90_a94_a50_a31_a75_a74) \land $ \\ 
 $ C0(a10_a81_a92) \land $ \\ 
 $ C0(a39_a20) \land $ \\ 
 $ C0(a55) \land $ \\ 
 $ C0(a61) \land $ \\ 
 $ C0(a5) \land $ \\ 
 $ C0(a89_a36_a29_a42_a52) \land $ \\ 
 $ C0(a45) \land $ \\ 
 $ C0(a46) \land $ \\ 
 $ C0(a65) \land $ \\ 
 $ C0(a44) \land $ \\ 
 $ C0(a87) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a61) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a7_a64) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a95) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a53) \land $ \\ 
 $  \Rnext  \Rnext C0(a54) \land $ \\ 
 $  \Rnext  \Rnext C1(a22) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a27) \land $ \\ 
 $  \Rnext  \Rnext C1(a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a77) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a39_a20) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a85) \land $ \\ 
 $  \Rnext E3L0Inv(a66_a1_a48_a93) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a46) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a68_a56) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a95) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a11_a33_a76_a32_a13_a35_a57_a78_a12_a34_a15_a37_a14_a58_a38_a80_a60_a84_a40_a100_a62_a63_a88_a43_a23_a67_a69_a49_a2_a3_a4_a6_a90_a94_a50_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a22) \land $ \\ 
 $  \Rnext E3L1Inv(a45) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a59_a25_a17_a91_a83) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a54) \land $ \\ 
 $  \Rnext E3L1(a77) \land $ \\ 
 $  \Rnext E3L1Inv(a24) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a7_a64) \land $ \\ 
 $  \Rnext E3L1Inv(a61) \land $ \\ 
 $  \Rnext E3L0Inv(a11_a33_a76_a32_a13_a35_a57_a78_a12_a34_a15_a37_a14_a58_a38_a80_a60_a84_a40_a100_a62_a63_a88_a43_a23_a67_a69_a49_a2_a3_a4_a6_a90_a94_a50_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a21_a79_a47_a82_a51) \land $ \\ 
 $  \Rnext  \Rnext C1(a46) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a53) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a66_a1_a48_a93) \land $ \\ 
 $  \Rnext E3L0Inv(a68_a56) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1Inv(a85) \land $ \\ 
 $  \Rnext C1(a99_a72) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a66_a1_a48_a93) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a65) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a45) \land $ \\ 
 $  \Rnext E3L1Inv(a68_a56) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a89_a36_a29_a42_a52) \land $ \\ 
 $  \Rnext C0(a44) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a21_a79_a47_a82_a51) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a95) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a11_a33_a76_a32_a13_a35_a57_a78_a12_a34_a15_a37_a14_a58_a38_a80_a60_a84_a40_a100_a62_a63_a88_a43_a23_a67_a69_a49_a2_a3_a4_a6_a90_a94_a50_a31_a75_a74) \land $ \\ 
 $  \Rnext E3L1Inv(a55) \land $ \\ 
 $  \Rnext  \Rnext C1(a87) \land $ \\ 
 $  \Rnext  \Rnext C0(a27) \land $ \\ 
 $  \Rnext E3L0Inv(a98_a26_a28_a19_a70) \land $ \\ 
 $ E3L0(a27) \land $ \\ 
 $ E3L0(a66_a1_a48_a93) \land $ \\ 
 $ E3L0(a71) \land $ \\ 
 $ E3L0(a22) \land $ \\ 
 $ E3L0(a99_a72) \land $ \\ 
 $ E3L0(a10_a81_a92) \land $ \\ 
 $ E3L0(a85) \land $ \\ 
 $ E3L0(a54) \land $ \\ 
 $ E3L0(a44) \land $ \\ 
 $ E3L0(a46) \land $ \\ 
 $ E3L0(a77) \land $ \\ 
 $ E3L0(a39_a20) \land $ \\ 
 $ E3L0(a9_a86_a97_a41) \land $ \\ 
 $ E3L0(a45) \land $ \\ 
 $ E3L0(a7_a64) \land $ \\ 
 $ E3L0(a8_a18_a73) \land $ \\ 
 $ E3L0(a24) \land $ \\ 
 $ E3L0(a98_a26_a28_a19_a70) \land $ \\ 
 $ E3L0(a68_a56) \land $ \\ 
 $ E3L0(a11_a33_a76_a32_a13_a35_a57_a78_a12_a34_a15_a37_a14_a58_a38_a80_a60_a84_a40_a100_a62_a63_a88_a43_a23_a67_a69_a49_a2_a3_a4_a6_a90_a94_a50_a31_a75_a74) \land $ \\ 
 $ E3L0(a89_a36_a29_a42_a52) \land $ \\ 
 $ E3L0(a87) \land $ \\ 
 $ E3L0(a59_a25_a17_a91_a83) \land $ \\ 
 $ E3L0(a5) \land $ \\ 
 $ E3L0(a61) \land $ \\ 
 $ E3L0(a16_a96) \land $ \\ 
 $ E3L0(a65) \land $ \\ 
 $ E3L0(a55) \land $ \\ 
 $ E3L0(a53) \land $ \\ 
 $ E3L0(a21_a79_a47_a82_a51) \land $ \\ 
 $ E3L0(a95) \land $ \\ 
 $ E3L0(a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a95) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a54) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a77) \land $ \\ 
 $  \Rnext  \Rnext C0(a89_a36_a29_a42_a52) \land $ \\ 
 $  \Rnext E3L1Inv(a46) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a44) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a27) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a11_a33_a76_a32_a13_a35_a57_a78_a12_a34_a15_a37_a14_a58_a38_a80_a60_a84_a40_a100_a62_a63_a88_a43_a23_a67_a69_a49_a2_a3_a4_a6_a90_a94_a50_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a98_a26_a28_a19_a70) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a65) \land $ \\ 
 $  \Rnext E3L1(a16_a96) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a95) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a44) \land $ \\ 
 $  \Rnext  \Rnext C0(a39_a20) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a21_a79_a47_a82_a51) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a11_a33_a76_a32_a13_a35_a57_a78_a12_a34_a15_a37_a14_a58_a38_a80_a60_a84_a40_a100_a62_a63_a88_a43_a23_a67_a69_a49_a2_a3_a4_a6_a90_a94_a50_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a30) \land $ \\ 
 $  \Rnext C0(a54) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a16_a96) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a30) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a53) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a44) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a95) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a8_a18_a73) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a61) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a54) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0(a54) \land $ \\ 
 $  \Rnext  \Rnext E3L0Inv(a11_a33_a76_a32_a13_a35_a57_a78_a12_a34_a15_a37_a14_a58_a38_a80_a60_a84_a40_a100_a62_a63_a88_a43_a23_a67_a69_a49_a2_a3_a4_a6_a90_a94_a50_a31_a75_a74) \land $ \\ 
 $  \Rnext  \Rnext C1(a24) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a53) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a16_a96) \land $ \\ 
 $  \Rnext  \Rnext E3L0(a95) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a24) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C0(a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0Inv(a77) \land $ \\ 
 $  \Rnext  \Rnext C0(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L0Inv(a30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a87) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext C1(a22) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a54) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a44) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a16_a96) \land $ \\ 
 $  \Rnext E3L1(a39_a20) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a9_a86_a97_a41) \land $ \\ 
 $  \Rnext C0(a8_a18_a73) \land $ \\ 
 $  \Rnext E3L1(a61) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a7_a64) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a39_a20) \land $ \\ 
 $  \Rnext  \Rnext E3L1(a39_a20) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1(a16_a96) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L1Inv(a95) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a71) \land $ \\ 
 $  \Rnext E3L0(a22) \land $ \\ 
 $  \Rnext  \Rnext E3L1Inv(a44) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C1(a53) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E3L1(a54) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a16_a96) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E3L0(a9_a86_a97_a41) \land $ \\ 
 $  \Rnext E3L1(a24) \land $ \\ 
 $  \Rnext E3L1(a71) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext C0(a99_a72))$ 
\end{document}