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


$( \forall X. ((E1G6InvF(X) \rightarrow BOX87F(X)) \land $ \\ 
 $ (E1G13F(X) \rightarrow BOX13F(X)) \land $ \\ 
 $ (E1G5F(X) \rightarrow BOX56F(X)) \land $ \\ 
 $ (E4G13F(X) \rightarrow E3G13F(X)) \land $ \\ 
 $ (E1G4InvF(X) \rightarrow BOX75F(X)) \land $ \\ 
 $ (E1G1F(X) \rightarrow BOX115F(X)) \land $ \\ 
 $ (E1G1InvF(X) \rightarrow BOX113F(X)) \land $ \\ 
 $ (E3G10F(X) \rightarrow E1G10F(X)) \land $ \\ 
 $ (E1G17F(X) \rightarrow BOX34F(X)) \land $ \\ 
 $ (E1G28InvF(X) \rightarrow BOX84F(X)) \land $ \\ 
 $ (E5G18F(X) \rightarrow E1G18F(X)) \land $ \\ 
 $ (E1G8InvF(X) \rightarrow BOX92F(X)) \land $ \\ 
 $ (E1G9F(X) \rightarrow BOX77F(X)) \land $ \\ 
 $ (E1G9InvF(X) \rightarrow BOX89F(X)) \land $ \\ 
 $ (E5G11F(X) \rightarrow BOX30F(X)) \land $ \\ 
 $ (E5G5F(X) \rightarrow BOX44F(X)) \land $ \\ 
 $ (E1G14F(X) \rightarrow BOX47F(X)) \land $ \\ 
 $ (E3G13F(X) \rightarrow BOX27F(X)) \land $ \\ 
 $ (E4G0F(X) \rightarrow BOX66F(X)) \land $ \\ 
 $ (E1G11InvF(X) \rightarrow BOX91F(X)) \land $ \\ 
 $ (DIAMOND1F(X) \rightarrow DIAMOND2F(X)) \land $ \\ 
 $ (E1G21InvF(X) \rightarrow BOX109F(X)) \land $ \\ 
 $ (E3G9F(X) \rightarrow E1G9F(X)) \land $ \\ 
 $ (E1G8F(X) \rightarrow BOX90F(X)) \land $ \\ 
 $ (E1G18InvF(X) \rightarrow BOX76F(X)) \land $ \\ 
 $ (E1G27F(X) \rightarrow BOX7F(X)) \land $ \\ 
 $ (E1G9F(X) \rightarrow BOX4F(X)) \land $ \\ 
 $ (E5G18F(X) \rightarrow BOX36F(X)) \land $ \\ 
 $ (E1G28F(X) \rightarrow BOX81F(X)) \land $ \\ 
 $ (BOX25F(X) \rightarrow BOX26F(X)) \land $ \\ 
 $ (E4G10F(X) \rightarrow BOX0F(X)) \land $ \\ 
 $ (E1G18F(X) \rightarrow BOX78F(X)) \land $ \\ 
 $ (E1G0F(X) \rightarrow BOX93F(X)) \land $ \\ 
 $ (E1G8F(X) \rightarrow BOX51F(X)) \land $ \\ 
 $ (E5G27F(X) \rightarrow E1G27F(X)) \land $ \\ 
 $ (E5G17F(X) \rightarrow BOX46F(X)) \land $ \\ 
 $ (E1G20F(X) \rightarrow BOX79F(X)) \land $ \\ 
 $ (E3G8F(X) \rightarrow BOX60F(X)) \land $ \\ 
 $ (DIAMOND21F(X) \rightarrow BOX22F(X)) \land $ \\ 
 $ (E1G10InvF(X) \rightarrow BOX107F(X)) \land $ \\ 
 $ (E1G17InvF(X) \rightarrow BOX88F(X)) \land $ \\ 
 $ (E1G16F(X) \rightarrow BOX12F(X)) \land $ \\ 
 $ (E5G27F(X) \rightarrow BOX17F(X)) \land $ \\ 
 $ (E1G17F(X) \rightarrow BOX97F(X)) \land $ \\ 
 $ (E1L6InvF(X) \rightarrow BOX111F(X)) \land $ \\ 
 $ (E1G28F(X) \rightarrow BOX24F(X)) \land $ \\ 
 $ ((DIAMOND31F(X) \land $ \\ 
 $ DIAMOND32F(X)) \rightarrow DIAMOND33F(X)) \land $ \\ 
 $ (E4G10F(X) \rightarrow E3G10F(X)) \land $ \\ 
 $ (BOX42F(X) \rightarrow BOX43F(X)) \land $ \\ 
 $ (E1G4F(X) \rightarrow BOX103F(X)) \land $ \\ 
 $ (E4G7F(X) \rightarrow BOX45F(X)) \land $ \\ 
 $ (E1G16InvF(X) \rightarrow BOX104F(X)) \land $ \\ 
 $ (E5G5F(X) \rightarrow E1G5F(X)) \land $ \\ 
 $ (E1G7InvF(X) \rightarrow BOX74F(X)) \land $ \\ 
 $ (E4G13F(X) \rightarrow BOX29F(X)) \land $ \\ 
 $ (E5G28F(X) \rightarrow E1G28F(X)) \land $ \\ 
 $ (E1G27F(X) \rightarrow BOX98F(X)) \land $ \\ 
 $ (E3G13F(X) \rightarrow E2G13F(X)) \land $ \\ 
 $ (E3G8F(X) \rightarrow E1G8F(X)) \land $ \\ 
 $ (BOX57F(X) \rightarrow DIAMOND58F(X)) \land $ \\ 
 $ (E1G7F(X) \rightarrow BOX40F(X)) \land $ \\ 
 $ (BOX14F(X) \rightarrow DIAMOND15F(X)) \land $ \\ 
 $ (E1G2InvF(X) \rightarrow BOX95F(X)) \land $ \\ 
 $ (E1G14InvF(X) \rightarrow BOX114F(X)) \land $ \\ 
 $ (E1G20F(X) \rightarrow BOX20F(X)) \land $ \\ 
 $ (E1G4F(X) \rightarrow BOX37F(X)) \land $ \\ 
 $ (E1G13F(X) \rightarrow BOX83F(X)) \land $ \\ 
 $ (BOX54F(X) \rightarrow BOX55F(X)) \land $ \\ 
 $ (E1G27InvF(X) \rightarrow BOX82F(X)) \land $ \\ 
 $ (E2G21F(X) \rightarrow E1G21F(X)) \land $ \\ 
 $ (E4L6F(X) \rightarrow E1L6F(X)) \land $ \\ 
 $ (E1G1F(X) \rightarrow BOX28F(X)) \land $ \\ 
 $ (E1G13InvF(X) \rightarrow BOX94F(X)) \land $ \\ 
 $ (E1G21F(X) \rightarrow BOX105F(X)) \land $ \\ 
 $ (E4G7F(X) \rightarrow E1G7F(X)) \land $ \\ 
 $ (E5G14F(X) \rightarrow BOX53F(X)) \land $ \\ 
 $ (E1G11F(X) \rightarrow BOX101F(X)) \land $ \\ 
 $ (E3G1F(X) \rightarrow BOX35F(X)) \land $ \\ 
 $ (E1G6F(X) \rightarrow BOX65F(X)) \land $ \\ 
 $ (E2G13F(X) \rightarrow BOX62F(X)) \land $ \\ 
 $ (E2G20F(X) \rightarrow BOX59F(X)) \land $ \\ 
 $ (E1G10F(X) \rightarrow BOX102F(X)) \land $ \\ 
 $ (E4G0F(X) \rightarrow E1G0F(X)) \land $ \\ 
 $ (E1G0F(X) \rightarrow BOX38F(X)) \land $ \\ 
 $ (BOX5F(X) \rightarrow BOX6F(X)) \land $ \\ 
 $ (E4G4F(X) \rightarrow E1G4F(X)) \land $ \\ 
 $ (E1G14F(X) \rightarrow BOX110F(X)) \land $ \\ 
 $ (BOX71F(X) \rightarrow (DIAMOND72F(X) \land $ \\ 
 $ DIAMOND73F(X))) \land $ \\ 
 $ (E1G10F(X) \rightarrow BOX39F(X)) \land $ \\ 
 $ (E2G13F(X) \rightarrow E1G13F(X)) \land $ \\ 
 $ (E2G21F(X) \rightarrow BOX8F(X)) \land $ \\ 
 $ (E1G16F(X) \rightarrow BOX85F(X)) \land $ \\ 
 $ (E2G20F(X) \rightarrow E1G20F(X)) \land $ \\ 
 $ (E1G21F(X) \rightarrow BOX48F(X)) \land $ \\ 
 $ (E5G28F(X) \rightarrow BOX69F(X)) \land $ \\ 
 $ (E1G5InvF(X) \rightarrow BOX80F(X)) \land $ \\ 
 $ (E1G2F(X) \rightarrow BOX70F(X)) \land $ \\ 
 $ (E3G9F(X) \rightarrow BOX16F(X)) \land $ \\ 
 $ (E5G14F(X) \rightarrow E1G14F(X)) \land $ \\ 
 $ (E5G17F(X) \rightarrow E1G17F(X)) \land $ \\ 
 $ (E5G11F(X) \rightarrow E1G11F(X)) \land $ \\ 
 $ (E1G20InvF(X) \rightarrow BOX108F(X)) \land $ \\ 
 $ (E1G7F(X) \rightarrow BOX100F(X)) \land $ \\ 
 $ (E1G11F(X) \rightarrow BOX23F(X)) \land $ \\ 
 $ (BOX18F(X) \rightarrow DIAMOND19F(X)) \land $ \\ 
 $ (E1G6F(X) \rightarrow BOX96F(X)) \land $ \\ 
 $ (E1L6F(X) \rightarrow BOX99F(X)) \land $ \\ 
 $ (DIAMOND63F(X) \rightarrow BOX64F(X)) \land $ \\ 
 $ (E5G2F(X) \rightarrow E1G2F(X)) \land $ \\ 
 $ (E1G5F(X) \rightarrow BOX106F(X)) \land $ \\ 
 $ (E1G0InvF(X) \rightarrow BOX112F(X)) \land $ \\ 
 $ (E3G10F(X) \rightarrow BOX3F(X)) \land $ \\ 
 $ ((BOX9F(X) \land $ \\ 
 $ DIAMOND10F(X)) \rightarrow BOX11F(X)) \land $ \\ 
 $ (DIAMOND49F(X) \rightarrow BOX50F(X)) \land $ \\ 
 $ (DIAMOND67F(X) \rightarrow BOX68F(X)) \land $ \\ 
 $ (E3G1F(X) \rightarrow E1G1F(X)) \land $ \\ 
 $ (E5G2F(X) \rightarrow BOX41F(X)) \land $ \\ 
 $ (E1G18F(X) \rightarrow BOX52F(X)) \land $ \\ 
 $ (E4G4F(X) \rightarrow BOX61F(X)) \land $ \\ 
 $ (E1G2F(X) \rightarrow BOX86F(X)) \land $ \\ 
 $  \Rbox (( \Rnext DIAMOND310F(X) \leftrightarrow (DIAMOND310F(X) \lor  \Rnext DIAMOND247F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND152P(X) \leftrightarrow (DIAMOND152P(X) \lor  \Rnext DIAMOND153P(X))) \land $ \\ 
 $ (DIAMOND58F(X) \leftrightarrow  \Rdiamond DIAMOND251F(X)) \land $ \\ 
 $ ( \Rnext DIAMOND285F(X) \leftrightarrow (DIAMOND285F(X) \lor  \Rnext DIAMOND286F(X))) \land $ \\ 
 $ (DIAMOND267F(X) \leftrightarrow  \Rdiamond BOX268F(X)) \land $ \\ 
 $ (DIAMOND388P(X) \leftrightarrow  \Rdiamond DIAMOND179P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND133P(X) \leftrightarrow (DIAMOND133P(X) \lor  \Rnext DIAMOND134P(X))) \land $ \\ 
 $ ( \Rnext DIAMOND216F(X) \leftrightarrow (DIAMOND216F(X) \lor  \Rnext BOX284F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND287F(X) \leftrightarrow (DIAMOND287F(X) \lor  \Rnext BOX288F(X))) \land $ \\ 
 $ (DIAMOND210F(X) \leftrightarrow  \Rdiamond (E4G10F(X) \land $ \\ 
 $ DIAMOND211F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND278F(X) \leftrightarrow (DIAMOND278F(X) \lor  \Rnext BOX279F(X))) \land $ \\ 
 $ (DIAMOND33F(X) \leftrightarrow  \Rdiamond (BOX234F(X) \land $ \\ 
 $  \lnot E3G10F(X))) \land $ \\ 
 $ (DIAMOND379P(X) \leftrightarrow  \Rdiamond  \lnot C9P(X)) \land $ \\ 
 $ (DIAMOND149P(X) \leftrightarrow  \Rdiamond E2G21P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND300F(X) \leftrightarrow (DIAMOND300F(X) \lor  \Rnext E5G5F(X))) \land $ \\ 
 $ (DIAMOND339P(X) \leftrightarrow  \Rdiamond BOX340P(X)) \land $ \\ 
 $ (DIAMOND356P(X) \leftrightarrow  \Rdiamond BOX357P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND195P(X) \leftrightarrow (DIAMOND195P(X) \lor  \Rnext C2P(X))) \land $ \\ 
 $ (DIAMOND32F(X) \leftrightarrow  \Rdiamond E2G20F(X)) \land $ \\ 
 $ ( \Rnext DIAMOND166P(X) \leftrightarrow (DIAMOND166P(X) \lor  \Rnext (BOX167P(X) \land $ \\ 
 $ DIAMOND168P(X)))) \land $ \\ 
 $ ( \Rnext DIAMOND147P(X) \leftrightarrow (DIAMOND147P(X) \lor  \Rnext DIAMOND148P(X))) \land $ \\ 
 $ (DIAMOND224F(X) \leftrightarrow  \Rdiamond BOX225F(X)) \land $ \\ 
 $ ( \Rnext DIAMOND73F(X) \leftrightarrow (DIAMOND73F(X) \lor  \Rnext DIAMOND330F(X))) \land $ \\ 
 $ (DIAMOND337P(X) \leftrightarrow  \Rdiamond BOX338P(X)) \land $ \\ 
 $ (DIAMOND347P(X) \leftrightarrow  \Rdiamond DIAMOND348P(X)) \land $ \\ 
 $ (DIAMOND355P(X) \leftrightarrow  \Rdiamond DIAMOND356P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND297F(X) \leftrightarrow (DIAMOND297F(X) \lor  \Rnext BOX298F(X))) \land $ \\ 
 $ (DIAMOND212F(X) \leftrightarrow  \Rdiamond DIAMOND213F(X)) \land $ \\ 
 $ (DIAMOND226F(X) \leftrightarrow  \Rdiamond DIAMOND227F(X)) \land $ \\ 
 $ ( \Rnext DIAMOND211F(X) \leftrightarrow (DIAMOND211F(X) \lor  \Rnext C29F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND126P(X) \leftrightarrow (DIAMOND126P(X) \lor  \Rnext C9P(X))) \land $ \\ 
 $ (DIAMOND334P(X) \leftrightarrow  \Rdiamond DIAMOND116P(X)) \land $ \\ 
 $ (DIAMOND132P(X) \leftrightarrow  \Rdiamond C29P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND318F(X) \leftrightarrow (DIAMOND318F(X) \lor  \Rnext E5G2F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND286F(X) \leftrightarrow (DIAMOND286F(X) \lor  \Rnext DIAMOND287F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND128P(X) \leftrightarrow (DIAMOND128P(X) \lor  \Rnext BOX129P(X))) \land $ \\ 
 $ ( \Rnext DIAMOND19F(X) \leftrightarrow (DIAMOND19F(X) \lor  \Rnext DIAMOND292F(X))) \land $ \\ 
 $ (DIAMOND207F(X) \leftrightarrow  \Rdiamond BOX208F(X)) \land $ \\ 
 $ (DIAMOND219F(X) \leftrightarrow  \Rdiamond DIAMOND220F(X)) \land $ \\ 
 $ ( \Rnext DIAMOND168P(X) \leftrightarrow (DIAMOND168P(X) \lor  \Rnext DIAMOND169P(X))) \land $ \\ 
 $ (DIAMOND213F(X) \leftrightarrow  \Rdiamond DIAMOND214F(X)) \land $ \\ 
 $ ( \Rnext DIAMOND307F(X) \leftrightarrow (DIAMOND307F(X) \lor  \Rnext BOX308F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND122P(X) \leftrightarrow (DIAMOND122P(X) \lor  \Rnext BOX123P(X))) \land $ \\ 
 $ (DIAMOND203F(X) \leftrightarrow  \Rdiamond DIAMOND204F(X)) \land $ \\ 
 $ (DIAMOND366P(X) \leftrightarrow  \Rdiamond DIAMOND367P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND289F(X) \leftrightarrow (DIAMOND289F(X) \lor  \Rnext DIAMOND290F(X))) \land $ \\ 
 $ (DIAMOND222F(X) \leftrightarrow  \Rdiamond BOX223F(X)) \land $ \\ 
 $ ( \Rnext DIAMOND148P(X) \leftrightarrow (DIAMOND148P(X) \lor  \Rnext DIAMOND149P(X))) \land $ \\ 
 $ ( \Rnext DIAMOND214F(X) \leftrightarrow (DIAMOND214F(X) \lor  \Rnext (BOX281F(X) \land $ \\ 
 $ DIAMOND282F(X)))) \land $ \\ 
 $ (DIAMOND137P(X) \leftrightarrow  \Rdiamond BOX346P(X)) \land $ \\ 
 $ (DIAMOND175P(X) \leftrightarrow  \Rdiamond DIAMOND176P(X)) \land $ \\ 
 $ (DIAMOND201F(X) \leftrightarrow  \Rdiamond BOX202F(X)) \land $ \\ 
 $ ( \Rnext DIAMOND228F(X) \leftrightarrow (DIAMOND228F(X) \lor  \Rnext E2G21F(X))) \land $ \\ 
 $ (DIAMOND358P(X) \leftrightarrow  \Rdiamond (E5G28P(X) \land $ \\ 
 $ BOX359P(X))) \land $ \\ 
 $ ( \Rnext DIAMOND242F(X) \leftrightarrow (DIAMOND242F(X) \lor  \Rnext DIAMOND243F(X))) \land $ \\ 
 $ (DIAMOND241F(X) \leftrightarrow  \Rdiamond DIAMOND242F(X)) \land $ \\ 
 $ (DIAMOND239F(X) \leftrightarrow  \Rdiamond ( \lnot C28F(X) \land $ \\ 
 $ BOX240F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND49F(X) \leftrightarrow (DIAMOND49F(X) \lor  \Rnext BOX309F(X))) \land $ \\ 
 $ (DIAMOND258F(X) \leftrightarrow  \Rdiamond DIAMOND259F(X)) \land $ \\ 
 $ (DIAMOND365P(X) \leftrightarrow  \Rdiamond E5G5P(X)) \land $ \\ 
 $ (DIAMOND2F(X) \leftrightarrow  \Rdiamond DIAMOND199F(X)) \land $ \\ 
 $ ( \Rnext DIAMOND320F(X) \leftrightarrow (DIAMOND320F(X) \lor  \Rnext DIAMOND255F(X))) \land $ \\ 
 $ (DIAMOND377P(X) \leftrightarrow  \Rdiamond DIAMOND170P(X)) \land $ \\ 
 $ (DIAMOND171P(X) \leftrightarrow  \Rdiamond (C1P(X) \land $ \\ 
 $ DIAMOND378P(X))) \land $ \\ 
 $ ( \Rnext DIAMOND190P(X) \leftrightarrow (DIAMOND190P(X) \lor  \Rnext DIAMOND191P(X))) \land $ \\ 
 $ ( \Rnext DIAMOND124P(X) \leftrightarrow (DIAMOND124P(X) \lor  \Rnext DIAMOND125P(X))) \land $ \\ 
 $ (DIAMOND217F(X) \leftrightarrow  \Rdiamond E3G1F(X)) \land $ \\ 
 $ (DIAMOND235F(X) \leftrightarrow  \Rdiamond E1G5F(X)) \land $ \\ 
 $ (DIAMOND183P(X) \leftrightarrow  \Rdiamond (DIAMOND184P(X) \land $ \\ 
 $ BOX394P(X))) \land $ \\ 
 $ (DIAMOND370P(X) \leftrightarrow  \Rdiamond BOX371P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND1F(X) \leftrightarrow (DIAMOND1F(X) \lor  \Rnext BOX271F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND174P(X) \leftrightarrow (DIAMOND174P(X) \lor  \Rnext DIAMOND175P(X))) \land $ \\ 
 $ ( \Rnext DIAMOND67F(X) \leftrightarrow (DIAMOND67F(X) \lor  \Rnext DIAMOND258F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND150P(X) \leftrightarrow (DIAMOND150P(X) \lor  \Rnext DIAMOND151P(X))) \land $ \\ 
 $ (DIAMOND372P(X) \leftrightarrow  \Rdiamond C27P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND294F(X) \leftrightarrow (DIAMOND294F(X) \lor  \Rnext (E5G28F(X) \land $ \\ 
 $ BOX295F(X)))) \land $ \\ 
 $ ( \Rnext DIAMOND158P(X) \leftrightarrow (DIAMOND158P(X) \lor  \Rnext E1G5P(X))) \land $ \\ 
 $ (DIAMOND238F(X) \leftrightarrow  \Rdiamond DIAMOND239F(X)) \land $ \\ 
 $ ( \Rnext DIAMOND321F(X) \leftrightarrow (DIAMOND321F(X) \lor  \Rnext (BOX322F(X) \land $ \\ 
 $ DIAMOND323F(X)))) \land $ \\ 
 $ ( \Rnext DIAMOND120P(X) \leftrightarrow (DIAMOND120P(X) \lor  \Rnext BOX121P(X))) \land $ \\ 
 $ (DIAMOND169P(X) \leftrightarrow  \Rdiamond C5P(X)) \land $ \\ 
 $ (DIAMOND378P(X) \leftrightarrow  \Rdiamond DIAMOND379P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND329F(X) \leftrightarrow (DIAMOND329F(X) \lor  \Rnext DIAMOND266F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND302F(X) \leftrightarrow (DIAMOND302F(X) \lor  \Rnext BOX303F(X))) \land $ \\ 
 $ (DIAMOND196F(X) \leftrightarrow  \Rdiamond DIAMOND197F(X)) \land $ \\ 
 $ ( \Rnext DIAMOND306F(X) \leftrightarrow (DIAMOND306F(X) \lor  \Rnext C27F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND182P(X) \leftrightarrow (DIAMOND182P(X) \lor  \Rnext DIAMOND183P(X))) \land $ \\ 
 $ (DIAMOND262F(X) \leftrightarrow  \Rdiamond DIAMOND263F(X)) \land $ \\ 
 $ ( \Rnext DIAMOND138P(X) \leftrightarrow (DIAMOND138P(X) \lor  \Rnext E3G1P(X))) \land $ \\ 
 $ ( \Rnext DIAMOND330F(X) \leftrightarrow (DIAMOND330F(X) \lor  \Rnext E5G27F(X))) \land $ \\ 
 $ (DIAMOND218F(X) \leftrightarrow  \Rdiamond DIAMOND219F(X)) \land $ \\ 
 $ ( \Rnext DIAMOND63F(X) \leftrightarrow (DIAMOND63F(X) \lor  \Rnext BOX319F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND176P(X) \leftrightarrow (DIAMOND176P(X) \lor  \Rnext BOX177P(X))) \land $ \\ 
 $ (DIAMOND260F(X) \leftrightarrow  \Rdiamond BOX261F(X)) \land $ \\ 
 $ ( \Rnext DIAMOND21F(X) \leftrightarrow (DIAMOND21F(X) \lor  \Rnext BOX296F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND170P(X) \leftrightarrow (DIAMOND170P(X) \lor  \Rnext DIAMOND171P(X))) \land $ \\ 
 $ ( \Rnext DIAMOND164P(X) \leftrightarrow (DIAMOND164P(X) \lor  \Rnext DIAMOND165P(X))) \land $ \\ 
 $ (DIAMOND229F(X) \leftrightarrow  \Rdiamond DIAMOND230F(X)) \land $ \\ 
 $ ( \Rnext DIAMOND117P(X) \leftrightarrow (DIAMOND117P(X) \lor  \Rnext DIAMOND118P(X))) \land $ \\ 
 $ (DIAMOND349P(X) \leftrightarrow  \Rdiamond DIAMOND350P(X)) \land $ \\ 
 $ (DIAMOND352P(X) \leftrightarrow  \Rdiamond DIAMOND353P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND315F(X) \leftrightarrow (DIAMOND315F(X) \lor  \Rnext BOX316F(X))) \land $ \\ 
 $ (DIAMOND199F(X) \leftrightarrow  \Rdiamond BOX200F(X)) \land $ \\ 
 $ (DIAMOND348P(X) \leftrightarrow  \Rdiamond DIAMOND349P(X)) \land $ \\ 
 $ (DIAMOND399P(X) \leftrightarrow  \Rdiamond DIAMOND400P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND139P(X) \leftrightarrow (DIAMOND139P(X) \lor  \Rnext DIAMOND140P(X))) \land $ \\ 
 $ ( \Rnext DIAMOND159P(X) \leftrightarrow (DIAMOND159P(X) \lor  \Rnext BOX160P(X))) \land $ \\ 
 $ ( \Rnext DIAMOND125P(X) \leftrightarrow (DIAMOND125P(X) \lor  \Rnext C25P(X))) \land $ \\ 
 $ (DIAMOND270F(X) \leftrightarrow  \Rdiamond C2F(X)) \land $ \\ 
 $ ( \Rnext DIAMOND156P(X) \leftrightarrow (DIAMOND156P(X) \lor  \Rnext (BOX157P(X) \land $ \\ 
 $  \lnot E3G10P(X)))) \land $ \\ 
 $ ( \Rnext DIAMOND304F(X) \leftrightarrow (DIAMOND304F(X) \lor  \Rnext BOX305F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND136P(X) \leftrightarrow (DIAMOND136P(X) \lor  \Rnext DIAMOND137P(X))) \land $ \\ 
 $ ( \Rnext DIAMOND186P(X) \leftrightarrow (DIAMOND186P(X) \lor  \Rnext DIAMOND187P(X))) \land $ \\ 
 $ ( \Rnext DIAMOND15F(X) \leftrightarrow (DIAMOND15F(X) \lor  \Rnext DIAMOND285F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND178P(X) \leftrightarrow (DIAMOND178P(X) \lor  \Rnext E1G4P(X))) \land $ \\ 
 $ ( \Rnext DIAMOND250F(X) \leftrightarrow (DIAMOND250F(X) \lor  \Rnext BOX317F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND131P(X) \leftrightarrow (DIAMOND131P(X) \lor  \Rnext (E4G10P(X) \land $ \\ 
 $ DIAMOND132P(X)))) \land $ \\ 
 $ (DIAMOND197F(X) \leftrightarrow  \Rdiamond DIAMOND198F(X)) \land $ \\ 
 $ ( \Rnext DIAMOND313F(X) \leftrightarrow (DIAMOND313F(X) \lor  \Rnext BOX314F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND290F(X) \leftrightarrow (DIAMOND290F(X) \lor  \Rnext BOX291F(X))) \land $ \\ 
 $ (DIAMOND393P(X) \leftrightarrow  \Rdiamond DIAMOND182P(X)) \land $ \\ 
 $ (DIAMOND362P(X) \leftrightarrow  \Rdiamond BOX363P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND198F(X) \leftrightarrow (DIAMOND198F(X) \lor  \Rnext BOX274F(X))) \land $ \\ 
 $ (DIAMOND395P(X) \leftrightarrow  \Rdiamond DIAMOND186P(X)) \land $ \\ 
 $ (DIAMOND386P(X) \leftrightarrow  \Rdiamond BOX387P(X)) \land $ \\ 
 $ (DIAMOND364P(X) \leftrightarrow  \Rdiamond C12P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND312F(X) \leftrightarrow (DIAMOND312F(X) \lor  \Rnext  \lnot C9F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND191P(X) \leftrightarrow (DIAMOND191P(X) \lor  \Rnext BOX192P(X))) \land $ \\ 
 $ ( \Rnext DIAMOND301F(X) \leftrightarrow (DIAMOND301F(X) \lor  \Rnext DIAMOND302F(X))) \land $ \\ 
 $ (DIAMOND382P(X) \leftrightarrow  \Rdiamond BOX383P(X)) \land $ \\ 
 $ (DIAMOND353P(X) \leftrightarrow  \Rdiamond BOX354P(X)) \land $ \\ 
 $ (DIAMOND227F(X) \leftrightarrow  \Rdiamond DIAMOND228F(X)) \land $ \\ 
 $ ( \Rnext DIAMOND143P(X) \leftrightarrow (DIAMOND143P(X) \lor  \Rnext BOX144P(X))) \land $ \\ 
 $ ( \Rnext DIAMOND130P(X) \leftrightarrow (DIAMOND130P(X) \lor  \Rnext E2G13P(X))) \land $ \\ 
 $ (DIAMOND368P(X) \leftrightarrow  \Rdiamond BOX369P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND116P(X) \leftrightarrow (DIAMOND116P(X) \lor  \Rnext DIAMOND117P(X))) \land $ \\ 
 $ (DIAMOND341P(X) \leftrightarrow  \Rdiamond BOX342P(X)) \land $ \\ 
 $ (DIAMOND247F(X) \leftrightarrow  \Rdiamond DIAMOND248F(X)) \land $ \\ 
 $ (DIAMOND397P(X) \leftrightarrow  \Rdiamond C11P(X)) \land $ \\ 
 $ (DIAMOND165P(X) \leftrightarrow  \Rdiamond DIAMOND166P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND246F(X) \leftrightarrow (DIAMOND246F(X) \lor  \Rnext C5F(X))) \land $ \\ 
 $ (DIAMOND72F(X) \leftrightarrow  \Rdiamond (BOX269F(X) \land $ \\ 
 $ DIAMOND270F(X))) \land $ \\ 
 $ (DIAMOND118P(X) \leftrightarrow  \Rdiamond BOX335P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND179P(X) \leftrightarrow (DIAMOND179P(X) \lor  \Rnext BOX180P(X))) \land $ \\ 
 $ ( \Rnext DIAMOND10F(X) \leftrightarrow (DIAMOND10F(X) \lor  \Rnext BOX280F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND141P(X) \leftrightarrow (DIAMOND141P(X) \lor  \Rnext BOX142P(X))) \land $ \\ 
 $ (DIAMOND151P(X) \leftrightarrow  \Rdiamond DIAMOND365P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND145P(X) \leftrightarrow (DIAMOND145P(X) \lor  \Rnext BOX146P(X))) \land $ \\ 
 $ (DIAMOND249F(X) \leftrightarrow  \Rdiamond (E3G13F(X) \land $ \\ 
 $ DIAMOND250F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND31F(X) \leftrightarrow (DIAMOND31F(X) \lor  \Rnext DIAMOND301F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND119P(X) \leftrightarrow (DIAMOND119P(X) \lor  \Rnext DIAMOND120P(X))) \land $ \\ 
 $ ( \Rnext DIAMOND299F(X) \leftrightarrow (DIAMOND299F(X) \lor  \Rnext C12F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND251F(X) \leftrightarrow (DIAMOND251F(X) \lor  \Rnext DIAMOND252F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND161P(X) \leftrightarrow (DIAMOND161P(X) \lor  \Rnext DIAMOND162P(X))) \land $ \\ 
 $ ( \Rnext DIAMOND162P(X) \leftrightarrow (DIAMOND162P(X) \lor  \Rnext ( \lnot C28P(X) \land $ \\ 
 $ BOX163P(X)))) \land $ \\ 
 $ (DIAMOND243F(X) \leftrightarrow  \Rdiamond (BOX244F(X) \land $ \\ 
 $ DIAMOND245F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND153P(X) \leftrightarrow (DIAMOND153P(X) \lor  \Rnext BOX154P(X))) \land $ \\ 
 $ ( \Rnext DIAMOND127P(X) \leftrightarrow (DIAMOND127P(X) \lor  \Rnext DIAMOND128P(X))) \land $ \\ 
 $ ( \Rnext DIAMOND328F(X) \leftrightarrow (DIAMOND328F(X) \lor  \Rnext C11F(X))) \land $ \\ 
 $ (DIAMOND187P(X) \leftrightarrow  \Rdiamond BOX396P(X)) \land $ \\ 
 $ (DIAMOND344P(X) \leftrightarrow  \Rdiamond BOX345P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND273F(X) \leftrightarrow (DIAMOND273F(X) \lor  \Rnext DIAMOND196F(X))) \land $ \\ 
 $ (DIAMOND400P(X) \leftrightarrow  \Rdiamond E5G27P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND323F(X) \leftrightarrow (DIAMOND323F(X) \lor  \Rnext BOX324F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND326F(X) \leftrightarrow (DIAMOND326F(X) \lor  \Rnext DIAMOND262F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND188P(X) \leftrightarrow (DIAMOND188P(X) \lor  \Rnext BOX189P(X))) \land $ \\ 
 $ (DIAMOND215F(X) \leftrightarrow  \Rdiamond DIAMOND216F(X)) \land $ \\ 
 $ ( \Rnext DIAMOND155P(X) \leftrightarrow (DIAMOND155P(X) \lor  \Rnext E2G20P(X))) \land $ \\ 
 $ (DIAMOND266F(X) \leftrightarrow  \Rdiamond DIAMOND267F(X)) \land $ \\ 
 $ ( \Rnext DIAMOND272F(X) \leftrightarrow (DIAMOND272F(X) \lor  \Rnext DIAMOND273F(X))) \land $ \\ 
 $ (DIAMOND204F(X) \leftrightarrow  \Rdiamond C25F(X)) \land $ \\ 
 $ (DIAMOND236F(X) \leftrightarrow  \Rdiamond BOX237F(X)) \land $ \\ 
 $ ( \Rnext DIAMOND181P(X) \leftrightarrow (DIAMOND181P(X) \lor  \Rnext E5G14P(X))) \land $ \\ 
 $ (DIAMOND264F(X) \leftrightarrow  \Rdiamond BOX265F(X)) \land $ \\ 
 $ (DIAMOND252F(X) \leftrightarrow  \Rdiamond BOX253F(X)) \land $ \\ 
 $ (DIAMOND232F(X) \leftrightarrow  \Rdiamond BOX233F(X)) \land $ \\ 
 $ ( \Rnext DIAMOND276F(X) \leftrightarrow (DIAMOND276F(X) \lor  \Rnext BOX277F(X))) \land $ \\ 
 $ (DIAMOND389P(X) \leftrightarrow  \Rdiamond (BOX390P(X) \land $ \\ 
 $ DIAMOND391P(X))) \land $ \\ 
 $ ( \Rnext DIAMOND248F(X) \leftrightarrow (DIAMOND248F(X) \lor  \Rnext (C1F(X) \land $ \\ 
 $ DIAMOND311F(X)))) \land $ \\ 
 $ (DIAMOND360P(X) \leftrightarrow  \Rdiamond BOX361P(X)) \land $ \\ 
 $ (DIAMOND220F(X) \leftrightarrow  \Rdiamond BOX221F(X)) \land $ \\ 
 $ (DIAMOND331P(X) \leftrightarrow  \Rdiamond BOX332P(X)) \land $ \\ 
 $ (DIAMOND135P(X) \leftrightarrow  \Rdiamond (BOX343P(X) \land $ \\ 
 $ DIAMOND344P(X))) \land $ \\ 
 $ (DIAMOND350P(X) \leftrightarrow  \Rdiamond BOX351P(X)) \land $ \\ 
 $ (DIAMOND205F(X) \leftrightarrow  \Rdiamond C9F(X)) \land $ \\ 
 $ ( \Rnext DIAMOND134P(X) \leftrightarrow (DIAMOND134P(X) \lor  \Rnext DIAMOND135P(X))) \land $ \\ 
 $ ( \Rnext DIAMOND193P(X) \leftrightarrow (DIAMOND193P(X) \lor  \Rnext (BOX194P(X) \land $ \\ 
 $ DIAMOND195P(X)))) \land $ \\ 
 $ (DIAMOND206F(X) \leftrightarrow  \Rdiamond DIAMOND207F(X)) \land $ \\ 
 $ (DIAMOND254F(X) \leftrightarrow  \Rdiamond E1G4F(X)) \land $ \\ 
 $ ( \Rnext DIAMOND311F(X) \leftrightarrow (DIAMOND311F(X) \lor  \Rnext DIAMOND312F(X))) \land $ \\ 
 $ (DIAMOND385P(X) \leftrightarrow  \Rdiamond E5G2P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND275F(X) \leftrightarrow (DIAMOND275F(X) \lor  \Rnext E4G13F(X))) \land $ \\ 
 $ (DIAMOND367P(X) \leftrightarrow  \Rdiamond DIAMOND368P(X)) \land $ \\ 
 $ (DIAMOND380P(X) \leftrightarrow  \Rdiamond BOX381P(X)) \land $ \\ 
 $ (DIAMOND373P(X) \leftrightarrow  \Rdiamond BOX374P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND172P(X) \leftrightarrow (DIAMOND172P(X) \lor  \Rnext (E3G13P(X) \land $ \\ 
 $ DIAMOND173P(X)))) \land $ \\ 
 $ ( \Rnext DIAMOND230F(X) \leftrightarrow (DIAMOND230F(X) \lor  \Rnext DIAMOND300F(X))) \land $ \\ 
 $ (DIAMOND245F(X) \leftrightarrow  \Rdiamond DIAMOND246F(X)) \land $ \\ 
 $ (DIAMOND173P(X) \leftrightarrow  \Rdiamond BOX384P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND140P(X) \leftrightarrow (DIAMOND140P(X) \lor  \Rnext DIAMOND141P(X))) \land $ \\ 
 $ ( \Rnext DIAMOND263F(X) \leftrightarrow (DIAMOND263F(X) \lor  \Rnext BOX327F(X))) \land $ \\ 
 $ (DIAMOND257F(X) \leftrightarrow  \Rdiamond E5G14F(X)) \land $ \\ 
 $ (DIAMOND333P(X) \leftrightarrow  \Rdiamond DIAMOND334P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND292F(X) \leftrightarrow (DIAMOND292F(X) \lor  \Rnext BOX293F(X))) \land $ \\ 
 $ (DIAMOND336P(X) \leftrightarrow  \Rdiamond E4G13P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND282F(X) \leftrightarrow (DIAMOND282F(X) \lor  \Rnext BOX283F(X))) \land $ \\ 
 $ (DIAMOND209F(X) \leftrightarrow  \Rdiamond E2G13F(X)) \land $ \\ 
 $ (DIAMOND231F(X) \leftrightarrow  \Rdiamond DIAMOND232F(X)) \land $ \\ 
 $ ( \Rnext DIAMOND259F(X) \leftrightarrow (DIAMOND259F(X) \lor  \Rnext (DIAMOND260F(X) \land $ \\ 
 $ BOX325F(X)))) \land $ \\ 
 $ (DIAMOND375P(X) \leftrightarrow  \Rdiamond BOX376P(X)) \land $ \\ 
 $ (DIAMOND255F(X) \leftrightarrow  \Rdiamond BOX256F(X)) \land $ \\ 
 $ (DIAMOND398P(X) \leftrightarrow  \Rdiamond DIAMOND190P(X)) \land $ \\ 
 $ (DIAMOND391P(X) \leftrightarrow  \Rdiamond BOX392P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND184P(X) \leftrightarrow (DIAMOND184P(X) \lor  \Rnext BOX185P(X))) \land $ \\ 
 $ (BOX253F(X) \leftrightarrow  \Rbox (BOX619F(X) \land $ \\ 
 $ DIAMOND254F(X))) \land $ \\ 
 $ (BOX61F(X) \leftrightarrow  \Rbox BOX622F(X)) \land $ \\ 
 $ ( \Rnext BOX449P(X) \leftrightarrow (BOX449P(X) \land $ \\ 
 $  \Rnext BOX450P(X))) \land $ \\ 
 $ ( \Rnext BOX458P(X) \leftrightarrow (BOX458P(X) \land $ \\ 
 $  \Rnext BOX459P(X))) \land $ \\ 
 $ (BOX733P(X) \leftrightarrow  \Rbox BOX549P(X)) \land $ \\ 
 $ (BOX129P(X) \leftrightarrow  \Rbox BOX414P(X)) \land $ \\ 
 $ (BOX713P(X) \leftrightarrow  \Rbox BOX529P(X)) \land $ \\ 
 $ (BOX725P(X) \leftrightarrow  \Rbox BOX541P(X)) \land $ \\ 
 $ ( \Rnext BOX535P(X) \leftrightarrow (BOX535P(X) \land $ \\ 
 $  \Rnext PinvG9P)) \land $ \\ 
 $ ( \Rnext BOX244F(X) \leftrightarrow (BOX244F(X) \land $ \\ 
 $  \Rnext E5G28F(X))) \land $ \\ 
 $ ( \Rnext BOX499P(X) \leftrightarrow (BOX499P(X) \land $ \\ 
 $  \Rnext DIAMOND385P(X))) \land $ \\ 
 $ (BOX618F(X) \leftrightarrow  \Rbox (C21F(X) \land $ \\ 
 $ C17F(X))) \land $ \\ 
 $ (BOX505P(X) \leftrightarrow  \Rbox E4G4P(X)) \land $ \\ 
 $ (BOX652F(X) \leftrightarrow  \Rbox PinvG2F) \land $ \\ 
 $ (BOX55F(X) \leftrightarrow  \Rbox BOX615F(X)) \land $ \\ 
 $ (BOX704P(X) \leftrightarrow  \Rbox BOX520P(X)) \land $ \\ 
 $ ( \Rnext BOX541P(X) \leftrightarrow (BOX541P(X) \land $ \\ 
 $  \Rnext PinvG2P)) \land $ \\ 
 $ (BOX284F(X) \leftrightarrow  \Rbox C20F(X)) \land $ \\ 
 $ (BOX741P(X) \leftrightarrow  \Rbox BOX557P(X)) \land $ \\ 
 $ (BOX644F(X) \leftrightarrow  \Rbox PinvG6F) \land $ \\ 
 $ ( \Rnext BOX561P(X) \leftrightarrow (BOX561P(X) \land $ \\ 
 $  \Rnext PG1P)) \land $ \\ 
 $ ( \Rnext BOX446P(X) \leftrightarrow (BOX446P(X) \land $ \\ 
 $  \Rnext (DIAMOND150P(X) \land $ \\ 
 $ DIAMOND152P(X)))) \land $ \\ 
 $ ( \Rnext BOX610F(X) \leftrightarrow (BOX610F(X) \land $ \\ 
 $  \Rnext E1G21F(X))) \land $ \\ 
 $ ( \Rnext BOX102F(X) \leftrightarrow (BOX102F(X) \land $ \\ 
 $  \Rnext BOX659F(X))) \land $ \\ 
 $ (BOX672F(X) \leftrightarrow  \Rbox PG1F) \land $ \\ 
 $ (BOX23F(X) \leftrightarrow  \Rbox BOX585F(X)) \land $ \\ 
 $ (BOX450P(X) \leftrightarrow  \Rbox E1G1P(X)) \land $ \\ 
 $ (BOX703P(X) \leftrightarrow  \Rbox BOX517P(X)) \land $ \\ 
 $ ( \Rnext BOX425P(X) \leftrightarrow (BOX425P(X) \land $ \\ 
 $  \Rnext (BOX426P(X) \land $ \\ 
 $ DIAMOND138P(X)))) \land $ \\ 
 $ (BOX27F(X) \leftrightarrow  \Rbox BOX591F(X)) \land $ \\ 
 $ ( \Rnext BOX401P(X) \leftrightarrow (BOX401P(X) \land $ \\ 
 $  \Rnext BOX402P(X))) \land $ \\ 
 $ ( \Rnext BOX461P(X) \leftrightarrow (BOX461P(X) \land $ \\ 
 $  \Rnext BOX462P(X))) \land $ \\ 
 $ (BOX566F(X) \leftrightarrow  \Rbox BOX568F(X)) \land $ \\ 
 $ (BOX565F(X) \leftrightarrow  \Rbox (BOX566F(X) \land $ \\ 
 $ BOX567F(X))) \land $ \\ 
 $ (BOX268F(X) \leftrightarrow  \Rbox  \lnot E4G0F(X)) \land $ \\ 
 $ ( \Rnext BOX240F(X) \leftrightarrow (BOX240F(X) \land $ \\ 
 $  \Rnext C6F(X))) \land $ \\ 
 $ ( \Rnext BOX97F(X) \leftrightarrow (BOX97F(X) \land $ \\ 
 $  \Rnext BOX654F(X))) \land $ \\ 
 $ (BOX41F(X) \leftrightarrow  \Rbox BOX602F(X)) \land $ \\ 
 $ (BOX507P(X) \leftrightarrow  \Rbox E2G13P(X)) \land $ \\ 
 $ ( \Rnext BOX471P(X) \leftrightarrow (BOX471P(X) \land $ \\ 
 $  \Rnext BOX472P(X))) \land $ \\ 
 $ ( \Rnext BOX96F(X) \leftrightarrow (BOX96F(X) \land $ \\ 
 $  \Rnext BOX653F(X))) \land $ \\ 
 $ ( \Rnext BOX85F(X) \leftrightarrow (BOX85F(X) \land $ \\ 
 $  \Rnext BOX642F(X))) \land $ \\ 
 $ (BOX646F(X) \leftrightarrow  \Rbox PinvG9F) \land $ \\ 
 $ (BOX589F(X) \leftrightarrow  \Rbox E1G6F(X)) \land $ \\ 
 $ ( \Rnext BOX407P(X) \leftrightarrow (BOX407P(X) \land $ \\ 
 $  \Rnext BOX408P(X))) \land $ \\ 
 $ ( \Rnext BOX477P(X) \leftrightarrow (BOX477P(X) \land $ \\ 
 $  \Rnext BOX478P(X))) \land $ \\ 
 $ ( \Rnext BOX280F(X) \leftrightarrow (BOX280F(X) \land $ \\ 
 $  \Rnext DIAMOND210F(X))) \land $ \\ 
 $ ( \Rnext BOX681F(X) \leftrightarrow (BOX681F(X) \land $ \\ 
 $  \Rnext DIAMOND320F(X))) \land $ \\ 
 $ (BOX163P(X) \leftrightarrow  \Rbox C6P(X)) \land $ \\ 
 $ ( \Rnext BOX444P(X) \leftrightarrow (BOX444P(X) \land $ \\ 
 $  \Rnext E1G6P(X))) \land $ \\ 
 $ ( \Rnext BOX77F(X) \leftrightarrow (BOX77F(X) \land $ \\ 
 $  \Rnext BOX634F(X))) \land $ \\ 
 $ (BOX13F(X) \leftrightarrow  \Rbox BOX575F(X)) \land $ \\ 
 $ ( \Rnext BOX95F(X) \leftrightarrow (BOX95F(X) \land $ \\ 
 $  \Rnext BOX652F(X))) \land $ \\ 
 $ ( \Rnext BOX676F(X) \leftrightarrow (BOX676F(X) \land $ \\ 
 $  \Rnext BOX607F(X))) \land $ \\ 
 $ (BOX615F(X) \leftrightarrow  \Rbox BOX616F(X)) \land $ \\ 
 $ (BOX5F(X) \leftrightarrow  \Rbox BOX565F(X)) \land $ \\ 
 $ ( \Rnext BOX623F(X) \leftrightarrow (BOX623F(X) \land $ \\ 
 $  \Rnext E2G13F(X))) \land $ \\ 
 $ ( \Rnext BOX408P(X) \leftrightarrow (BOX408P(X) \land $ \\ 
 $  \Rnext (BOX409P(X) \land $ \\ 
 $ BOX410P(X)))) \land $ \\ 
 $ (BOX664F(X) \leftrightarrow  \Rbox PinvG10F) \land $ \\ 
 $ (BOX637F(X) \leftrightarrow  \Rbox PinvG5F) \land $ \\ 
 $ (BOX658F(X) \leftrightarrow  \Rbox PG11F) \land $ \\ 
 $ ( \Rnext BOX11F(X) \leftrightarrow (BOX11F(X) \land $ \\ 
 $  \Rnext DIAMOND212F(X))) \land $ \\ 
 $ ( \Rnext BOX338P(X) \leftrightarrow (BOX338P(X) \land $ \\ 
 $  \Rnext DIAMOND124P(X))) \land $ \\ 
 $ (BOX440P(X) \leftrightarrow  \Rbox E1G28P(X)) \land $ \\ 
 $ (BOX510P(X) \leftrightarrow  \Rbox E1G6P(X)) \land $ \\ 
 $ (BOX269F(X) \leftrightarrow  \Rbox E1G16F(X)) \land $ \\ 
 $ ( \Rnext BOX622F(X) \leftrightarrow (BOX622F(X) \land $ \\ 
 $  \Rnext E4G4F(X))) \land $ \\ 
 $ ( \Rnext BOX82F(X) \leftrightarrow (BOX82F(X) \land $ \\ 
 $  \Rnext BOX639F(X))) \land $ \\ 
 $ ( \Rnext BOX412P(X) \leftrightarrow (BOX412P(X) \land $ \\ 
 $  \Rnext C26P(X))) \land $ \\ 
 $ ( \Rnext BOX94F(X) \leftrightarrow (BOX94F(X) \land $ \\ 
 $  \Rnext BOX651F(X))) \land $ \\ 
 $ (BOX584F(X) \leftrightarrow  \Rbox DIAMOND299F(X)) \land $ \\ 
 $ (BOX659F(X) \leftrightarrow  \Rbox PG10F) \land $ \\ 
 $ (BOX433P(X) \leftrightarrow  \Rbox E1G20P(X)) \land $ \\ 
 $ (BOX419P(X) \leftrightarrow  \Rbox E2G21P(X)) \land $ \\ 
 $ ( \Rnext BOX434P(X) \leftrightarrow (BOX434P(X) \land $ \\ 
 $  \Rnext BOX435P(X))) \land $ \\ 
 $ (BOX595F(X) \leftrightarrow  \Rbox (E5G11F(X) \land $ \\ 
 $ DIAMOND235F(X))) \land $ \\ 
 $ ( \Rnext BOX604F(X) \leftrightarrow (BOX604F(X) \land $ \\ 
 $  \Rnext DIAMOND306F(X))) \land $ \\ 
 $ (BOX474P(X) \leftrightarrow  \Rbox DIAMOND159P(X)) \land $ \\ 
 $ (BOX448P(X) \leftrightarrow  \Rbox E3G13P(X)) \land $ \\ 
 $ (BOX369P(X) \leftrightarrow  \Rbox DIAMOND370P(X)) \land $ \\ 
 $ ( \Rnext BOX447P(X) \leftrightarrow (BOX447P(X) \land $ \\ 
 $  \Rnext BOX448P(X))) \land $ \\ 
 $ ( \Rnext BOX557P(X) \leftrightarrow (BOX557P(X) \land $ \\ 
 $  \Rnext PinvL6P)) \land $ \\ 
 $ (BOX52F(X) \leftrightarrow  \Rbox BOX613F(X)) \land $ \\ 
 $ (BOX669F(X) \leftrightarrow  \Rbox PinvG0F) \land $ \\ 
 $ ( \Rnext BOX579F(X) \leftrightarrow (BOX579F(X) \land $ \\ 
 $  \Rnext E3G9F(X))) \land $ \\ 
 $ (BOX383P(X) \leftrightarrow  \Rbox DIAMOND172P(X)) \land $ \\ 
 $ ( \Rnext BOX551P(X) \leftrightarrow (BOX551P(X) \land $ \\ 
 $  \Rnext PG21P)) \land $ \\ 
 $ ( \Rnext BOX121P(X) \leftrightarrow (BOX121P(X) \land $ \\ 
 $  \Rnext DIAMOND122P(X))) \land $ \\ 
 $ (BOX277F(X) \leftrightarrow  \Rbox DIAMOND203F(X)) \land $ \\ 
 $ ( \Rnext BOX521P(X) \leftrightarrow (BOX521P(X) \land $ \\ 
 $  \Rnext PinvG4P)) \land $ \\ 
 $ ( \Rnext BOX346P(X) \leftrightarrow (BOX346P(X) \land $ \\ 
 $  \Rnext C20P(X))) \land $ \\ 
 $ ( \Rnext BOX599F(X) \leftrightarrow (BOX599F(X) \land $ \\ 
 $  \Rnext E1G0F(X))) \land $ \\ 
 $ (BOX648F(X) \leftrightarrow  \Rbox PinvG11F) \land $ \\ 
 $ ( \Rnext BOX308F(X) \leftrightarrow (BOX308F(X) \land $ \\ 
 $  \Rnext E1G5F(X))) \land $ \\ 
 $ ( \Rnext BOX572F(X) \leftrightarrow (BOX572F(X) \land $ \\ 
 $  \Rnext E1G27F(X))) \land $ \\ 
 $ ( \Rnext BOX409P(X) \leftrightarrow (BOX409P(X) \land $ \\ 
 $  \Rnext BOX411P(X))) \land $ \\ 
 $ ( \Rnext BOX527P(X) \leftrightarrow (BOX527P(X) \land $ \\ 
 $  \Rnext PG28P)) \land $ \\ 
 $ (BOX729P(X) \leftrightarrow  \Rbox BOX545P(X)) \land $ \\ 
 $ ( \Rnext BOX602F(X) \leftrightarrow (BOX602F(X) \land $ \\ 
 $  \Rnext E5G2F(X))) \land $ \\ 
 $ (BOX651F(X) \leftrightarrow  \Rbox PinvG13F) \land $ \\ 
 $ (BOX569F(X) \leftrightarrow  \Rbox C26F(X)) \land $ \\ 
 $ (BOX633F(X) \leftrightarrow  \Rbox PinvG18F) \land $ \\ 
 $ ( \Rnext BOX101F(X) \leftrightarrow (BOX101F(X) \land $ \\ 
 $  \Rnext BOX658F(X))) \land $ \\ 
 $ ( \Rnext BOX524P(X) \leftrightarrow (BOX524P(X) \land $ \\ 
 $  \Rnext PG18P)) \land $ \\ 
 $ ( \Rnext BOX22F(X) \leftrightarrow (BOX22F(X) \land $ \\ 
 $  \Rnext DIAMOND297F(X))) \land $ \\ 
 $ ( \Rnext BOX573F(X) \leftrightarrow (BOX573F(X) \land $ \\ 
 $  \Rnext E2G21F(X))) \land $ \\ 
 $ ( \Rnext BOX74F(X) \leftrightarrow (BOX74F(X) \land $ \\ 
 $  \Rnext BOX631F(X))) \land $ \\ 
 $ ( \Rnext BOX439P(X) \leftrightarrow (BOX439P(X) \land $ \\ 
 $  \Rnext BOX440P(X))) \land $ \\ 
 $ ( \Rnext BOX487P(X) \leftrightarrow (BOX487P(X) \land $ \\ 
 $  \Rnext BOX488P(X))) \land $ \\ 
 $ (BOX466P(X) \leftrightarrow  \Rbox E1G10P(X)) \land $ \\ 
 $ ( \Rnext BOX608F(X) \leftrightarrow (BOX608F(X) \land $ \\ 
 $  \Rnext BOX677F(X))) \land $ \\ 
 $ ( \Rnext BOX560P(X) \leftrightarrow (BOX560P(X) \land $ \\ 
 $  \Rnext PinvG14P)) \land $ \\ 
 $ ( \Rnext BOX609F(X) \leftrightarrow (BOX609F(X) \land $ \\ 
 $  \Rnext E5G5F(X))) \land $ \\ 
 $ (BOX392P(X) \leftrightarrow  \Rbox BOX701P(X)) \land $ \\ 
 $ ( \Rnext BOX536P(X) \leftrightarrow (BOX536P(X) \land $ \\ 
 $  \Rnext PG8P)) \land $ \\ 
 $ ( \Rnext BOX332P(X) \leftrightarrow (BOX332P(X) \land $ \\ 
 $  \Rnext DIAMOND333P(X))) \land $ \\ 
 $ (BOX691P(X) \leftrightarrow  \Rbox BOX477P(X)) \land $ \\ 
 $ ( \Rnext BOX538P(X) \leftrightarrow (BOX538P(X) \land $ \\ 
 $  \Rnext PinvG8P)) \land $ \\ 
 $ (BOX519P(X) \leftrightarrow  \Rbox DIAMOND398P(X)) \land $ \\ 
 $ (BOX343P(X) \leftrightarrow  \Rbox E4G7P(X)) \land $ \\ 
 $ ( \Rnext BOX436P(X) \leftrightarrow (BOX436P(X) \land $ \\ 
 $  \Rnext DIAMOND364P(X))) \land $ \\ 
 $ ( \Rnext BOX108F(X) \leftrightarrow (BOX108F(X) \land $ \\ 
 $  \Rnext BOX665F(X))) \land $ \\ 
 $ ( \Rnext BOX472P(X) \leftrightarrow (BOX472P(X) \land $ \\ 
 $  \Rnext (BOX473P(X) \land $ \\ 
 $ BOX474P(X)))) \land $ \\ 
 $ (BOX724P(X) \leftrightarrow  \Rbox BOX540P(X)) \land $ \\ 
 $ (BOX17F(X) \leftrightarrow  \Rbox BOX580F(X)) \land $ \\ 
 $ (BOX327F(X) \leftrightarrow  \Rbox DIAMOND264F(X)) \land $ \\ 
 $ (BOX742P(X) \leftrightarrow  \Rbox BOX558P(X)) \land $ \\ 
 $ ( \Rnext BOX534P(X) \leftrightarrow (BOX534P(X) \land $ \\ 
 $  \Rnext PinvG17P)) \land $ \\ 
 $ (BOX29F(X) \leftrightarrow  \Rbox BOX593F(X)) \land $ \\ 
 $ (BOX65F(X) \leftrightarrow  \Rbox BOX624F(X)) \land $ \\ 
 $ (BOX47F(X) \leftrightarrow  \Rbox BOX283F(X)) \land $ \\ 
 $ ( \Rnext BOX562F(X) \leftrightarrow (BOX562F(X) \land $ \\ 
 $  \Rnext E4G10F(X))) \land $ \\ 
 $ (BOX723P(X) \leftrightarrow  \Rbox BOX539P(X)) \land $ \\ 
 $ ( \Rnext BOX460P(X) \leftrightarrow (BOX460P(X) \land $ \\ 
 $  \Rnext BOX160P(X))) \land $ \\ 
 $ ( \Rnext BOX558P(X) \leftrightarrow (BOX558P(X) \land $ \\ 
 $  \Rnext PinvG0P)) \land $ \\ 
 $ (BOX488P(X) \leftrightarrow  \Rbox E1G8P(X)) \land $ \\ 
 $ ( \Rnext BOX491P(X) \leftrightarrow (BOX491P(X) \land $ \\ 
 $  \Rnext BOX492P(X))) \land $ \\ 
 $ (BOX44F(X) \leftrightarrow  \Rbox BOX609F(X)) \land $ \\ 
 $ ( \Rnext BOX105F(X) \leftrightarrow (BOX105F(X) \land $ \\ 
 $  \Rnext BOX662F(X))) \land $ \\ 
 $ ( \Rnext BOX675F(X) \leftrightarrow (BOX675F(X) \land $ \\ 
 $  \Rnext BOX584F(X))) \land $ \\ 
 $ ( \Rnext BOX542P(X) \leftrightarrow (BOX542P(X) \land $ \\ 
 $  \Rnext PG6P)) \land $ \\ 
 $ ( \Rnext BOX612F(X) \leftrightarrow (BOX612F(X) \land $ \\ 
 $  \Rnext E1G8F(X))) \land $ \\ 
 $ (BOX295F(X) \leftrightarrow  \Rbox  \lnot E3G9F(X)) \land $ \\ 
 $ ( \Rnext BOX416P(X) \leftrightarrow (BOX416P(X) \land $ \\ 
 $  \Rnext BOX417P(X))) \land $ \\ 
 $ ( \Rnext BOX598F(X) \leftrightarrow (BOX598F(X) \land $ \\ 
 $  \Rnext E1G4F(X))) \land $ \\ 
 $ ( \Rnext BOX418P(X) \leftrightarrow (BOX418P(X) \land $ \\ 
 $  \Rnext BOX419P(X))) \land $ \\ 
 $ (BOX657F(X) \leftrightarrow  \Rbox PG7F) \land $ \\ 
 $ (BOX650F(X) \leftrightarrow  \Rbox PG0F) \land $ \\ 
 $ (BOX42F(X) \leftrightarrow  \Rbox BOX603F(X)) \land $ \\ 
 $ ( \Rnext BOX88F(X) \leftrightarrow (BOX88F(X) \land $ \\ 
 $  \Rnext BOX645F(X))) \land $ \\ 
 $ (BOX588F(X) \leftrightarrow  \Rbox (C7F(X) \land $ \\ 
 $ BOX590F(X))) \land $ \\ 
 $ (BOX655F(X) \leftrightarrow  \Rbox PG27F) \land $ \\ 
 $ ( \Rnext BOX291F(X) \leftrightarrow (BOX291F(X) \land $ \\ 
 $  \Rnext C0F(X))) \land $ \\ 
 $ ( \Rnext BOX590F(X) \leftrightarrow (BOX590F(X) \land $ \\ 
 $  \Rnext E5G17F(X))) \land $ \\ 
 $ (BOX35F(X) \leftrightarrow  \Rbox BOX597F(X)) \land $ \\ 
 $ ( \Rnext BOX92F(X) \leftrightarrow (BOX92F(X) \land $ \\ 
 $  \Rnext BOX649F(X))) \land $ \\ 
 $ ( \Rnext BOX553P(X) \leftrightarrow (BOX553P(X) \land $ \\ 
 $  \Rnext PinvG10P)) \land $ \\ 
 $ ( \Rnext BOX581F(X) \leftrightarrow (BOX581F(X) \land $ \\ 
 $  \Rnext E1G20F(X))) \land $ \\ 
 $ (BOX582F(X) \leftrightarrow  \Rbox BOX583F(X)) \land $ \\ 
 $ (BOX666F(X) \leftrightarrow  \Rbox PinvG21F) \land $ \\ 
 $ (BOX701P(X) \leftrightarrow  \Rbox DIAMOND181P(X)) \land $ \\ 
 $ (BOX157P(X) \leftrightarrow  \Rbox BOX455P(X)) \land $ \\ 
 $ (BOX661F(X) \leftrightarrow  \Rbox PinvG16F) \land $ \\ 
 $ ( \Rnext BOX465P(X) \leftrightarrow (BOX465P(X) \land $ \\ 
 $  \Rnext BOX466P(X))) \land $ \\ 
 $ ( \Rnext BOX427P(X) \leftrightarrow (BOX427P(X) \land $ \\ 
 $  \Rnext DIAMOND352P(X))) \land $ \\ 
 $ (BOX470P(X) \leftrightarrow  \Rbox E5G2P(X)) \land $ \\ 
 $ ( \Rnext BOX86F(X) \leftrightarrow (BOX86F(X) \land $ \\ 
 $  \Rnext BOX643F(X))) \land $ \\ 
 $ (BOX335P(X) \leftrightarrow  \Rbox DIAMOND336P(X)) \land $ \\ 
 $ (BOX732P(X) \leftrightarrow  \Rbox BOX548P(X)) \land $ \\ 
 $ ( \Rnext BOX529P(X) \leftrightarrow (BOX529P(X) \land $ \\ 
 $  \Rnext PG13P)) \land $ \\ 
 $ ( \Rnext BOX500P(X) \leftrightarrow (BOX500P(X) \land $ \\ 
 $  \Rnext BOX501P(X))) \land $ \\ 
 $ (BOX422P(X) \leftrightarrow  \Rbox E1G16P(X)) \land $ \\ 
 $ (BOX710P(X) \leftrightarrow  \Rbox BOX526P(X)) \land $ \\ 
 $ (BOX402P(X) \leftrightarrow  \Rbox E4G10P(X)) \land $ \\ 
 $ ( \Rnext BOX303F(X) \leftrightarrow (BOX303F(X) \land $ \\ 
 $  \Rnext DIAMOND304F(X))) \land $ \\ 
 $ (BOX411P(X) \leftrightarrow  \Rbox BOX412P(X)) \land $ \\ 
 $ ( \Rnext BOX18F(X) \leftrightarrow (BOX18F(X) \land $ \\ 
 $  \Rnext DIAMOND218F(X))) \land $ \\ 
 $ (BOX690P(X) \leftrightarrow  \Rbox BOX436P(X)) \land $ \\ 
 $ ( \Rnext BOX192P(X) \leftrightarrow (BOX192P(X) \land $ \\ 
 $  \Rnext  \lnot E4G0P(X))) \land $ \\ 
 $ ( \Rnext BOX68F(X) \leftrightarrow (BOX68F(X) \land $ \\ 
 $  \Rnext BOX626F(X))) \land $ \\ 
 $ ( \Rnext BOX496P(X) \leftrightarrow (BOX496P(X) \land $ \\ 
 $  \Rnext DIAMOND380P(X))) \land $ \\ 
 $ (BOX66F(X) \leftrightarrow  \Rbox BOX625F(X)) \land $ \\ 
 $ (BOX689P(X) \leftrightarrow  \Rbox DIAMOND362P(X)) \land $ \\ 
 $ (BOX626F(X) \leftrightarrow  \Rbox DIAMOND326F(X)) \land $ \\ 
 $ (BOX716P(X) \leftrightarrow  \Rbox BOX532P(X)) \land $ \\ 
 $ ( \Rnext BOX403P(X) \leftrightarrow (BOX403P(X) \land $ \\ 
 $  \Rnext BOX404P(X))) \land $ \\ 
 $ ( \Rnext BOX202F(X) \leftrightarrow (BOX202F(X) \land $ \\ 
 $  \Rnext DIAMOND276F(X))) \land $ \\ 
 $ (BOX745P(X) \leftrightarrow  \Rbox BOX561P(X)) \land $ \\ 
 $ ( \Rnext BOX421P(X) \leftrightarrow (BOX421P(X) \land $ \\ 
 $  \Rnext BOX422P(X))) \land $ \\ 
 $ ( \Rnext BOX283F(X) \leftrightarrow (BOX283F(X) \land $ \\ 
 $  \Rnext E1G14F(X))) \land $ \\ 
 $ (BOX351P(X) \leftrightarrow  \Rbox BOX427P(X)) \land $ \\ 
 $ ( \Rnext BOX493P(X) \leftrightarrow (BOX493P(X) \land $ \\ 
 $  \Rnext BOX494P(X))) \land $ \\ 
 $ (BOX632F(X) \leftrightarrow  \Rbox PinvG4F) \land $ \\ 
 $ (BOX501P(X) \leftrightarrow  \Rbox E2G20P(X)) \land $ \\ 
 $ ( \Rnext BOX453P(X) \leftrightarrow (BOX453P(X) \land $ \\ 
 $  \Rnext BOX454P(X))) \land $ \\ 
 $ ( \Rnext BOX513P(X) \leftrightarrow (BOX513P(X) \land $ \\ 
 $  \Rnext DIAMOND395P(X))) \land $ \\ 
 $ ( \Rnext BOX456P(X) \leftrightarrow (BOX456P(X) \land $ \\ 
 $  \Rnext BOX457P(X))) \land $ \\ 
 $ (BOX696P(X) \leftrightarrow  \Rbox BOX697P(X)) \land $ \\ 
 $ (BOX694P(X) \leftrightarrow  \Rbox DIAMOND164P(X)) \land $ \\ 
 $ ( \Rnext BOX359P(X) \leftrightarrow (BOX359P(X) \land $ \\ 
 $  \Rnext  \lnot E3G9P(X))) \land $ \\ 
 $ (BOX739P(X) \leftrightarrow  \Rbox BOX555P(X)) \land $ \\ 
 $ (BOX653F(X) \leftrightarrow  \Rbox PG6F) \land $ \\ 
 $ ( \Rnext BOX76F(X) \leftrightarrow (BOX76F(X) \land $ \\ 
 $  \Rnext BOX633F(X))) \land $ \\ 
 $ (BOX712P(X) \leftrightarrow  \Rbox BOX528P(X)) \land $ \\ 
 $ ( \Rnext BOX103F(X) \leftrightarrow (BOX103F(X) \land $ \\ 
 $  \Rnext BOX660F(X))) \land $ \\ 
 $ (BOX709P(X) \leftrightarrow  \Rbox BOX525P(X)) \land $ \\ 
 $ ( \Rnext BOX106F(X) \leftrightarrow (BOX106F(X) \land $ \\ 
 $  \Rnext BOX663F(X))) \land $ \\ 
 $ ( \Rnext BOX340P(X) \leftrightarrow (BOX340P(X) \land $ \\ 
 $  \Rnext DIAMOND130P(X))) \land $ \\ 
 $ ( \Rnext BOX50F(X) \leftrightarrow (BOX50F(X) \land $ \\ 
 $  \Rnext DIAMOND241F(X))) \land $ \\ 
 $ ( \Rnext BOX546P(X) \leftrightarrow (BOX546P(X) \land $ \\ 
 $  \Rnext PG7P)) \land $ \\ 
 $ ( \Rnext BOX112F(X) \leftrightarrow (BOX112F(X) \land $ \\ 
 $  \Rnext BOX669F(X))) \land $ \\ 
 $ (BOX695P(X) \leftrightarrow  \Rbox DIAMOND377P(X)) \land $ \\ 
 $ ( \Rnext BOX548P(X) \leftrightarrow (BOX548P(X) \land $ \\ 
 $  \Rnext PG10P)) \land $ \\ 
 $ (BOX603F(X) \leftrightarrow  \Rbox (BOX604F(X) \land $ \\ 
 $ BOX605F(X))) \land $ \\ 
 $ ( \Rnext BOX593F(X) \leftrightarrow (BOX593F(X) \land $ \\ 
 $  \Rnext E4G13F(X))) \land $ \\ 
 $ (BOX717P(X) \leftrightarrow  \Rbox BOX533P(X)) \land $ \\ 
 $ (BOX445P(X) \leftrightarrow  \Rbox E5G17P(X)) \land $ \\ 
 $ ( \Rnext BOX115F(X) \leftrightarrow (BOX115F(X) \land $ \\ 
 $  \Rnext BOX672F(X))) \land $ \\ 
 $ ( \Rnext BOX539P(X) \leftrightarrow (BOX539P(X) \land $ \\ 
 $  \Rnext PG0P)) \land $ \\ 
 $ ( \Rnext BOX627F(X) \leftrightarrow (BOX627F(X) \land $ \\ 
 $  \Rnext E1G2F(X))) \land $ \\ 
 $ (BOX688P(X) \leftrightarrow  \Rbox DIAMOND358P(X)) \land $ \\ 
 $ (BOX485P(X) \leftrightarrow  \Rbox E1G21P(X)) \land $ \\ 
 $ ( \Rnext BOX441P(X) \leftrightarrow (BOX441P(X) \land $ \\ 
 $  \Rnext (BOX442P(X) \land $ \\ 
 $ BOX443P(X)))) \land $ \\ 
 $ ( \Rnext BOX550P(X) \leftrightarrow (BOX550P(X) \land $ \\ 
 $  \Rnext PinvG16P)) \land $ \\ 
 $ ( \Rnext BOX396P(X) \leftrightarrow (BOX396P(X) \land $ \\ 
 $  \Rnext DIAMOND188P(X))) \land $ \\ 
 $ ( \Rnext BOX90F(X) \leftrightarrow (BOX90F(X) \land $ \\ 
 $  \Rnext BOX647F(X))) \land $ \\ 
 $ ( \Rnext BOX437P(X) \leftrightarrow (BOX437P(X) \land $ \\ 
 $  \Rnext BOX438P(X))) \land $ \\ 
 $ ( \Rnext BOX274F(X) \leftrightarrow (BOX274F(X) \land $ \\ 
 $  \Rnext DIAMOND275F(X))) \land $ \\ 
 $ ( \Rnext BOX410P(X) \leftrightarrow (BOX410P(X) \land $ \\ 
 $  \Rnext DIAMOND126P(X))) \land $ \\ 
 $ (BOX727P(X) \leftrightarrow  \Rbox BOX543P(X)) \land $ \\ 
 $ ( \Rnext BOX426P(X) \leftrightarrow (BOX426P(X) \land $ \\ 
 $  \Rnext DIAMOND136P(X))) \land $ \\ 
 $ (BOX492P(X) \leftrightarrow  \Rbox E5G14P(X)) \land $ \\ 
 $ (BOX28F(X) \leftrightarrow  \Rbox BOX592F(X)) \land $ \\ 
 $ ( \Rnext BOX316F(X) \leftrightarrow (BOX316F(X) \land $ \\ 
 $  \Rnext DIAMOND249F(X))) \land $ \\ 
 $ (BOX431P(X) \leftrightarrow  \Rbox E5G27P(X)) \land $ \\ 
 $ (BOX629F(X) \leftrightarrow  \Rbox BOX630F(X)) \land $ \\ 
 $ ( \Rnext BOX288F(X) \leftrightarrow (BOX288F(X) \land $ \\ 
 $  \Rnext BOX578F(X))) \land $ \\ 
 $ (BOX649F(X) \leftrightarrow  \Rbox PinvG8F) \land $ \\ 
 $ (BOX645F(X) \leftrightarrow  \Rbox PinvG17F) \land $ \\ 
 $ ( \Rnext BOX319F(X) \leftrightarrow (BOX319F(X) \land $ \\ 
 $  \Rnext BOX680F(X))) \land $ \\ 
 $ (BOX233F(X) \leftrightarrow  \Rbox C7F(X)) \land $ \\ 
 $ ( \Rnext BOX281F(X) \leftrightarrow (BOX281F(X) \land $ \\ 
 $  \Rnext E4G7F(X))) \land $ \\ 
 $ (BOX722P(X) \leftrightarrow  \Rbox BOX538P(X)) \land $ \\ 
 $ (BOX384P(X) \leftrightarrow  \Rbox C12P(X)) \land $ \\ 
 $ (BOX3F(X) \leftrightarrow  \Rbox BOX563F(X)) \land $ \\ 
 $ (BOX665F(X) \leftrightarrow  \Rbox PinvG20F) \land $ \\ 
 $ ( \Rnext BOX208F(X) \leftrightarrow (BOX208F(X) \land $ \\ 
 $  \Rnext BOX570F(X))) \land $ \\ 
 $ ( \Rnext BOX625F(X) \leftrightarrow (BOX625F(X) \land $ \\ 
 $  \Rnext E4G0F(X))) \land $ \\ 
 $ ( \Rnext BOX435P(X) \leftrightarrow (BOX435P(X) \land $ \\ 
 $  \Rnext DIAMOND145P(X))) \land $ \\ 
 $ ( \Rnext BOX497P(X) \leftrightarrow (BOX497P(X) \land $ \\ 
 $  \Rnext (C21P(X) \land $ \\ 
 $ C17P(X)))) \land $ \\ 
 $ (BOX617F(X) \leftrightarrow  \Rbox DIAMOND313F(X)) \land $ \\ 
 $ (BOX271F(X) \leftrightarrow  \Rbox DIAMOND272F(X)) \land $ \\ 
 $ (BOX714P(X) \leftrightarrow  \Rbox BOX530P(X)) \land $ \\ 
 $ (BOX342P(X) \leftrightarrow  \Rbox DIAMOND131P(X)) \land $ \\ 
 $ ( \Rnext BOX293F(X) \leftrightarrow (BOX293F(X) \land $ \\ 
 $  \Rnext BOX674F(X))) \land $ \\ 
 $ ( \Rnext BOX194P(X) \leftrightarrow (BOX194P(X) \land $ \\ 
 $  \Rnext E1G16P(X))) \land $ \\ 
 $ (BOX39F(X) \leftrightarrow  \Rbox BOX600F(X)) \land $ \\ 
 $ ( \Rnext BOX109F(X) \leftrightarrow (BOX109F(X) \land $ \\ 
 $  \Rnext BOX666F(X))) \land $ \\ 
 $ ( \Rnext BOX540P(X) \leftrightarrow (BOX540P(X) \land $ \\ 
 $  \Rnext PinvG13P)) \land $ \\ 
 $ (BOX394P(X) \leftrightarrow  \Rbox E4L6P(X)) \land $ \\ 
 $ (BOX503P(X) \leftrightarrow  \Rbox E3G8P(X)) \land $ \\ 
 $ ( \Rnext BOX413P(X) \leftrightarrow (BOX413P(X) \land $ \\ 
 $  \Rnext DIAMOND127P(X))) \land $ \\ 
 $ ( \Rnext BOX91F(X) \leftrightarrow (BOX91F(X) \land $ \\ 
 $  \Rnext BOX648F(X))) \land $ \\ 
 $ (BOX60F(X) \leftrightarrow  \Rbox BOX621F(X)) \land $ \\ 
 $ (BOX668F(X) \leftrightarrow  \Rbox PinvL6F) \land $ \\ 
 $ (BOX185P(X) \leftrightarrow  \Rbox DIAMOND149P(X)) \land $ \\ 
 $ ( \Rnext BOX256F(X) \leftrightarrow (BOX256F(X) \land $ \\ 
 $  \Rnext BOX682F(X))) \land $ \\ 
 $ (BOX698P(X) \leftrightarrow  \Rbox BOX699P(X)) \land $ \\ 
 $ ( \Rnext BOX518P(X) \leftrightarrow (BOX518P(X) \land $ \\ 
 $  \Rnext BOX519P(X))) \land $ \\ 
 $ ( \Rnext BOX673F(X) \leftrightarrow (BOX673F(X) \land $ \\ 
 $  \Rnext  \lnot C26F(X))) \land $ \\ 
 $ (BOX34F(X) \leftrightarrow  \Rbox BOX596F(X)) \land $ \\ 
 $ (BOX720P(X) \leftrightarrow  \Rbox BOX536P(X)) \land $ \\ 
 $ (BOX37F(X) \leftrightarrow  \Rbox BOX598F(X)) \land $ \\ 
 $ ( \Rnext BOX531P(X) \leftrightarrow (BOX531P(X) \land $ \\ 
 $  \Rnext PG16P)) \land $ \\ 
 $ ( \Rnext BOX325F(X) \leftrightarrow (BOX325F(X) \land $ \\ 
 $  \Rnext E4L6F(X))) \land $ \\ 
 $ ( \Rnext BOX381P(X) \leftrightarrow (BOX381P(X) \land $ \\ 
 $  \Rnext BOX497P(X))) \land $ \\ 
 $ (BOX577F(X) \leftrightarrow  \Rbox DIAMOND215F(X)) \land $ \\ 
 $ ( \Rnext BOX483P(X) \leftrightarrow (BOX483P(X) \land $ \\ 
 $  \Rnext BOX345P(X))) \land $ \\ 
 $ ( \Rnext BOX489P(X) \leftrightarrow (BOX489P(X) \land $ \\ 
 $  \Rnext BOX490P(X))) \land $ \\ 
 $ (BOX12F(X) \leftrightarrow  \Rbox BOX574F(X)) \land $ \\ 
 $ ( \Rnext BOX528P(X) \leftrightarrow (BOX528P(X) \land $ \\ 
 $  \Rnext PinvG27P)) \land $ \\ 
 $ ( \Rnext BOX594F(X) \leftrightarrow (BOX594F(X) \land $ \\ 
 $  \Rnext E5G11F(X))) \land $ \\ 
 $ (BOX685P(X) \leftrightarrow  \Rbox BOX425P(X)) \land $ \\ 
 $ (BOX24F(X) \leftrightarrow  \Rbox BOX586F(X)) \land $ \\ 
 $ ( \Rnext BOX14F(X) \leftrightarrow (BOX14F(X) \land $ \\ 
 $  \Rnext BOX576F(X))) \land $ \\ 
 $ ( \Rnext BOX591F(X) \leftrightarrow (BOX591F(X) \land $ \\ 
 $  \Rnext E3G13F(X))) \land $ \\ 
 $ ( \Rnext BOX543P(X) \leftrightarrow (BOX543P(X) \land $ \\ 
 $  \Rnext PG17P)) \land $ \\ 
 $ ( \Rnext BOX430P(X) \leftrightarrow (BOX430P(X) \land $ \\ 
 $  \Rnext BOX431P(X))) \land $ \\ 
 $ (BOX144P(X) \leftrightarrow  \Rbox BOX687P(X)) \land $ \\ 
 $ ( \Rnext BOX509P(X) \leftrightarrow (BOX509P(X) \land $ \\ 
 $  \Rnext BOX510P(X))) \land $ \\ 
 $ ( \Rnext BOX679F(X) \leftrightarrow (BOX679F(X) \land $ \\ 
 $  \Rnext DIAMOND315F(X))) \land $ \\ 
 $ ( \Rnext BOX574F(X) \leftrightarrow (BOX574F(X) \land $ \\ 
 $  \Rnext E1G16F(X))) \land $ \\ 
 $ ( \Rnext BOX683F(X) \leftrightarrow (BOX683F(X) \land $ \\ 
 $  \Rnext DIAMOND257F(X))) \land $ \\ 
 $ (BOX686P(X) \leftrightarrow  \Rbox DIAMOND139P(X)) \land $ \\ 
 $ (BOX480P(X) \leftrightarrow  \Rbox E5G5P(X)) \land $ \\ 
 $ (BOX464P(X) \leftrightarrow  \Rbox E1G0P(X)) \land $ \\ 
 $ (BOX462P(X) \leftrightarrow  \Rbox E1G4P(X)) \land $ \\ 
 $ ( \Rnext BOX57F(X) \leftrightarrow (BOX57F(X) \land $ \\ 
 $  \Rnext BOX679F(X))) \land $ \\ 
 $ (BOX406P(X) \leftrightarrow  \Rbox E1G9P(X)) \land $ \\ 
 $ ( \Rnext BOX481P(X) \leftrightarrow (BOX481P(X) \land $ \\ 
 $  \Rnext BOX343P(X))) \land $ \\ 
 $ (BOX635F(X) \leftrightarrow  \Rbox PG18F) \land $ \\ 
 $ (BOX305F(X) \leftrightarrow  \Rbox C27F(X)) \land $ \\ 
 $ ( \Rnext BOX515P(X) \leftrightarrow (BOX515P(X) \land $ \\ 
 $  \Rnext BOX516P(X))) \land $ \\ 
 $ (BOX53F(X) \leftrightarrow  \Rbox BOX614F(X)) \land $ \\ 
 $ (BOX459P(X) \leftrightarrow  \Rbox E3G1P(X)) \land $ \\ 
 $ ( \Rnext BOX414P(X) \leftrightarrow (BOX414P(X) \land $ \\ 
 $  \Rnext BOX415P(X))) \land $ \\ 
 $ ( \Rnext BOX475P(X) \leftrightarrow (BOX475P(X) \land $ \\ 
 $  \Rnext BOX476P(X))) \land $ \\ 
 $ (BOX692P(X) \leftrightarrow  \Rbox BOX693P(X)) \land $ \\ 
 $ (BOX735P(X) \leftrightarrow  \Rbox BOX551P(X)) \land $ \\ 
 $ ( \Rnext BOX506P(X) \leftrightarrow (BOX506P(X) \land $ \\ 
 $  \Rnext BOX507P(X))) \land $ \\ 
 $ (BOX671F(X) \leftrightarrow  \Rbox PinvG14F) \land $ \\ 
 $ ( \Rnext BOX592F(X) \leftrightarrow (BOX592F(X) \land $ \\ 
 $  \Rnext E1G1F(X))) \land $ \\ 
 $ (BOX4F(X) \leftrightarrow  \Rbox BOX564F(X)) \land $ \\ 
 $ (BOX490P(X) \leftrightarrow  \Rbox E1G18P(X)) \land $ \\ 
 $ (BOX616F(X) \leftrightarrow  \Rbox BOX617F(X)) \land $ \\ 
 $ ( \Rnext BOX571F(X) \leftrightarrow (BOX571F(X) \land $ \\ 
 $  \Rnext DIAMOND278F(X))) \land $ \\ 
 $ ( \Rnext BOX580F(X) \leftrightarrow (BOX580F(X) \land $ \\ 
 $  \Rnext E5G27F(X))) \land $ \\ 
 $ ( \Rnext BOX469P(X) \leftrightarrow (BOX469P(X) \land $ \\ 
 $  \Rnext BOX470P(X))) \land $ \\ 
 $ ( \Rnext BOX390P(X) \leftrightarrow (BOX390P(X) \land $ \\ 
 $  \Rnext E1G21P(X))) \land $ \\ 
 $ ( \Rnext BOX585F(X) \leftrightarrow (BOX585F(X) \land $ \\ 
 $  \Rnext E1G11F(X))) \land $ \\ 
 $ ( \Rnext BOX624F(X) \leftrightarrow (BOX624F(X) \land $ \\ 
 $  \Rnext E1G6F(X))) \land $ \\ 
 $ (BOX429P(X) \leftrightarrow  \Rbox E3G9P(X)) \land $ \\ 
 $ (BOX721P(X) \leftrightarrow  \Rbox BOX537P(X)) \land $ \\ 
 $ ( \Rnext BOX237F(X) \leftrightarrow (BOX237F(X) \land $ \\ 
 $  \Rnext E5G18F(X))) \land $ \\ 
 $ (BOX322F(X) \leftrightarrow  \Rbox E1G21F(X)) \land $ \\ 
 $ ( \Rnext BOX479P(X) \leftrightarrow (BOX479P(X) \land $ \\ 
 $  \Rnext BOX480P(X))) \land $ \\ 
 $ (BOX225F(X) \leftrightarrow  \Rbox DIAMOND226F(X)) \land $ \\ 
 $ (BOX314F(X) \leftrightarrow  \Rbox BOX618F(X)) \land $ \\ 
 $ (BOX740P(X) \leftrightarrow  \Rbox BOX556P(X)) \land $ \\ 
 $ (BOX363P(X) \leftrightarrow  \Rbox (BOX690P(X) \land $ \\ 
 $  \lnot E3G8P(X))) \land $ \\ 
 $ ( \Rnext BOX523P(X) \leftrightarrow (BOX523P(X) \land $ \\ 
 $  \Rnext PG9P)) \land $ \\ 
 $ ( \Rnext BOX564F(X) \leftrightarrow (BOX564F(X) \land $ \\ 
 $  \Rnext E1G9F(X))) \land $ \\ 
 $ ( \Rnext BOX98F(X) \leftrightarrow (BOX98F(X) \land $ \\ 
 $  \Rnext BOX655F(X))) \land $ \\ 
 $ ( \Rnext BOX451P(X) \leftrightarrow (BOX451P(X) \land $ \\ 
 $  \Rnext BOX452P(X))) \land $ \\ 
 $ (BOX70F(X) \leftrightarrow  \Rbox BOX627F(X)) \land $ \\ 
 $ (BOX587F(X) \leftrightarrow  \Rbox BOX589F(X)) \land $ \\ 
 $ (BOX38F(X) \leftrightarrow  \Rbox BOX599F(X)) \land $ \\ 
 $ ( \Rnext BOX605F(X) \leftrightarrow (BOX605F(X) \land $ \\ 
 $  \Rnext DIAMOND236F(X))) \land $ \\ 
 $ ( \Rnext BOX428P(X) \leftrightarrow (BOX428P(X) \land $ \\ 
 $  \Rnext BOX429P(X))) \land $ \\ 
 $ (BOX46F(X) \leftrightarrow  \Rbox BOX590F(X)) \land $ \\ 
 $ (BOX662F(X) \leftrightarrow  \Rbox PG21F) \land $ \\ 
 $ (BOX567F(X) \leftrightarrow  \Rbox DIAMOND205F(X)) \land $ \\ 
 $ (BOX684P(X) \leftrightarrow  \Rbox DIAMOND133P(X)) \land $ \\ 
 $ ( \Rnext BOX674F(X) \leftrightarrow (BOX674F(X) \land $ \\ 
 $  \Rnext DIAMOND294F(X))) \land $ \\ 
 $ ( \Rnext BOX559P(X) \leftrightarrow (BOX559P(X) \land $ \\ 
 $  \Rnext PinvG1P)) \land $ \\ 
 $ (BOX636F(X) \leftrightarrow  \Rbox PG20F) \land $ \\ 
 $ ( \Rnext BOX83F(X) \leftrightarrow (BOX83F(X) \land $ \\ 
 $  \Rnext BOX640F(X))) \land $ \\ 
 $ ( \Rnext BOX442P(X) \leftrightarrow (BOX442P(X) \land $ \\ 
 $  \Rnext BOX444P(X))) \land $ \\ 
 $ (BOX56F(X) \leftrightarrow  \Rbox BOX308F(X)) \land $ \\ 
 $ (BOX667F(X) \leftrightarrow  \Rbox PG14F) \land $ \\ 
 $ ( \Rnext BOX114F(X) \leftrightarrow (BOX114F(X) \land $ \\ 
 $  \Rnext BOX671F(X))) \land $ \\ 
 $ (BOX737P(X) \leftrightarrow  \Rbox BOX553P(X)) \land $ \\ 
 $ (BOX7F(X) \leftrightarrow  \Rbox BOX572F(X)) \land $ \\ 
 $ (BOX64F(X) \leftrightarrow  \Rbox DIAMOND321F(X)) \land $ \\ 
 $ ( \Rnext BOX514P(X) \leftrightarrow (BOX514P(X) \land $ \\ 
 $  \Rnext BOX167P(X))) \land $ \\ 
 $ ( \Rnext BOX554P(X) \leftrightarrow (BOX554P(X) \land $ \\ 
 $  \Rnext PinvG20P)) \land $ \\ 
 $ ( \Rnext BOX563F(X) \leftrightarrow (BOX563F(X) \land $ \\ 
 $  \Rnext E3G10F(X))) \land $ \\ 
 $ ( \Rnext BOX621F(X) \leftrightarrow (BOX621F(X) \land $ \\ 
 $  \Rnext E3G8F(X))) \land $ \\ 
 $ (BOX699P(X) \leftrightarrow  \Rbox DIAMOND388P(X)) \land $ \\ 
 $ (BOX200F(X) \leftrightarrow  \Rbox DIAMOND201F(X)) \land $ \\ 
 $ ( \Rnext BOX678F(X) \leftrightarrow (BOX678F(X) \land $ \\ 
 $  \Rnext DIAMOND307F(X))) \land $ \\ 
 $ ( \Rnext BOX555P(X) \leftrightarrow (BOX555P(X) \land $ \\ 
 $  \Rnext PinvG21P)) \land $ \\ 
 $ ( \Rnext BOX80F(X) \leftrightarrow (BOX80F(X) \land $ \\ 
 $  \Rnext BOX637F(X))) \land $ \\ 
 $ (BOX160P(X) \leftrightarrow  \Rbox E5G18P(X)) \land $ \\ 
 $ ( \Rnext BOX234F(X) \leftrightarrow (BOX234F(X) \land $ \\ 
 $  \Rnext BOX595F(X))) \land $ \\ 
 $ ( \Rnext BOX81F(X) \leftrightarrow (BOX81F(X) \land $ \\ 
 $  \Rnext BOX638F(X))) \land $ \\ 
 $ (BOX45F(X) \leftrightarrow  \Rbox BOX281F(X)) \land $ \\ 
 $ ( \Rnext BOX361P(X) \leftrightarrow (BOX361P(X) \land $ \\ 
 $  \Rnext BOX434P(X))) \land $ \\ 
 $ (BOX8F(X) \leftrightarrow  \Rbox BOX573F(X)) \land $ \\ 
 $ (BOX639F(X) \leftrightarrow  \Rbox PinvG27F) \land $ \\ 
 $ ( \Rnext BOX545P(X) \leftrightarrow (BOX545P(X) \land $ \\ 
 $  \Rnext PL6P)) \land $ \\ 
 $ (BOX167P(X) \leftrightarrow  \Rbox E5G28P(X)) \land $ \\ 
 $ ( \Rnext BOX677F(X) \leftrightarrow (BOX677F(X) \land $ \\ 
 $  \Rnext BOX678F(X))) \land $ \\ 
 $ (BOX687P(X) \leftrightarrow  \Rbox  \lnot C26P(X)) \land $ \\ 
 $ (BOX43F(X) \leftrightarrow  \Rbox BOX606F(X)) \land $ \\ 
 $ (BOX387P(X) \leftrightarrow  \Rbox BOX698P(X)) \land $ \\ 
 $ ( \Rnext BOX93F(X) \leftrightarrow (BOX93F(X) \land $ \\ 
 $  \Rnext BOX650F(X))) \land $ \\ 
 $ (BOX641F(X) \leftrightarrow  \Rbox PinvG28F) \land $ \\ 
 $ ( \Rnext BOX221F(X) \leftrightarrow (BOX221F(X) \land $ \\ 
 $  \Rnext DIAMOND222F(X))) \land $ \\ 
 $ (BOX734P(X) \leftrightarrow  \Rbox BOX550P(X)) \land $ \\ 
 $ ( \Rnext BOX549P(X) \leftrightarrow (BOX549P(X) \land $ \\ 
 $  \Rnext PG4P)) \land $ \\ 
 $ (BOX345P(X) \leftrightarrow  \Rbox E1G14P(X)) \land $ \\ 
 $ (BOX719P(X) \leftrightarrow  \Rbox BOX535P(X)) \land $ \\ 
 $ ( \Rnext BOX504P(X) \leftrightarrow (BOX504P(X) \land $ \\ 
 $  \Rnext BOX505P(X))) \land $ \\ 
 $ (BOX454P(X) \leftrightarrow  \Rbox E5G11P(X)) \land $ \\ 
 $ (BOX634F(X) \leftrightarrow  \Rbox PG9F) \land $ \\ 
 $ ( \Rnext BOX606F(X) \leftrightarrow (BOX606F(X) \land $ \\ 
 $  \Rnext BOX676F(X))) \land $ \\ 
 $ ( \Rnext BOX517P(X) \leftrightarrow (BOX517P(X) \land $ \\ 
 $  \Rnext BOX518P(X))) \land $ \\ 
 $ ( \Rnext BOX298F(X) \leftrightarrow (BOX298F(X) \land $ \\ 
 $  \Rnext (BOX675F(X) \land $ \\ 
 $  \lnot E3G8F(X)))) \land $ \\ 
 $ ( \Rnext BOX596F(X) \leftrightarrow (BOX596F(X) \land $ \\ 
 $  \Rnext E1G17F(X))) \land $ \\ 
 $ (BOX706P(X) \leftrightarrow  \Rbox BOX522P(X)) \land $ \\ 
 $ (BOX404P(X) \leftrightarrow  \Rbox E3G10P(X)) \land $ \\ 
 $ ( \Rnext BOX87F(X) \leftrightarrow (BOX87F(X) \land $ \\ 
 $  \Rnext BOX644F(X))) \land $ \\ 
 $ (BOX478P(X) \leftrightarrow  \Rbox BOX692P(X)) \land $ \\ 
 $ (BOX40F(X) \leftrightarrow  \Rbox BOX601F(X)) \land $ \\ 
 $ ( \Rnext BOX525P(X) \leftrightarrow (BOX525P(X) \land $ \\ 
 $  \Rnext PG20P)) \land $ \\ 
 $ (BOX36F(X) \leftrightarrow  \Rbox BOX237F(X)) \land $ \\ 
 $ ( \Rnext BOX99F(X) \leftrightarrow (BOX99F(X) \land $ \\ 
 $  \Rnext BOX656F(X))) \land $ \\ 
 $ ( \Rnext BOX530P(X) \leftrightarrow (BOX530P(X) \land $ \\ 
 $  \Rnext PinvG28P)) \land $ \\ 
 $ ( \Rnext BOX533P(X) \leftrightarrow (BOX533P(X) \land $ \\ 
 $  \Rnext PinvG6P)) \land $ \\ 
 $ ( \Rnext BOX682F(X) \leftrightarrow (BOX682F(X) \land $ \\ 
 $  \Rnext BOX562F(X))) \land $ \\ 
 $ ( \Rnext BOX552P(X) \leftrightarrow (BOX552P(X) \land $ \\ 
 $  \Rnext PG5P)) \land $ \\ 
 $ (BOX6F(X) \leftrightarrow  \Rbox DIAMOND206F(X)) \land $ \\ 
 $ (BOX357P(X) \leftrightarrow  \Rbox BOX688P(X)) \land $ \\ 
 $ ( \Rnext BOX455P(X) \leftrightarrow (BOX455P(X) \land $ \\ 
 $  \Rnext (E5G11P(X) \land $ \\ 
 $ DIAMOND158P(X)))) \land $ \\ 
 $ (BOX516P(X) \leftrightarrow  \Rbox E1G2P(X)) \land $ \\ 
 $ (BOX25F(X) \leftrightarrow  \Rbox (BOX587F(X) \land $ \\ 
 $ BOX588F(X))) \land $ \\ 
 $ ( \Rnext BOX79F(X) \leftrightarrow (BOX79F(X) \land $ \\ 
 $  \Rnext BOX636F(X))) \land $ \\ 
 $ ( \Rnext BOX597F(X) \leftrightarrow (BOX597F(X) \land $ \\ 
 $  \Rnext E3G1F(X))) \land $ \\ 
 $ ( \Rnext BOX568F(X) \leftrightarrow (BOX568F(X) \land $ \\ 
 $  \Rnext BOX569F(X))) \land $ \\ 
 $ ( \Rnext BOX371P(X) \leftrightarrow (BOX371P(X) \land $ \\ 
 $  \Rnext C27P(X))) \land $ \\ 
 $ ( \Rnext BOX498P(X) \leftrightarrow (BOX498P(X) \land $ \\ 
 $  \Rnext BOX374P(X))) \land $ \\ 
 $ ( \Rnext BOX223F(X) \leftrightarrow (BOX223F(X) \land $ \\ 
 $  \Rnext BOX673F(X))) \land $ \\ 
 $ ( \Rnext BOX71F(X) \leftrightarrow (BOX71F(X) \land $ \\ 
 $  \Rnext BOX628F(X))) \land $ \\ 
 $ (BOX59F(X) \leftrightarrow  \Rbox BOX620F(X)) \land $ \\ 
 $ (BOX744P(X) \leftrightarrow  \Rbox BOX560P(X)) \land $ \\ 
 $ (BOX180P(X) \leftrightarrow  \Rbox BOX700P(X)) \land $ \\ 
 $ (BOX0F(X) \leftrightarrow  \Rbox BOX562F(X)) \land $ \\ 
 $ ( \Rnext BOX84F(X) \leftrightarrow (BOX84F(X) \land $ \\ 
 $  \Rnext BOX641F(X))) \land $ \\ 
 $ ( \Rnext BOX484P(X) \leftrightarrow (BOX484P(X) \land $ \\ 
 $  \Rnext BOX485P(X))) \land $ \\ 
 $ ( \Rnext BOX511P(X) \leftrightarrow (BOX511P(X) \land $ \\ 
 $  \Rnext BOX512P(X))) \land $ \\ 
 $ ( \Rnext BOX526P(X) \leftrightarrow (BOX526P(X) \land $ \\ 
 $  \Rnext PinvG5P)) \land $ \\ 
 $ ( \Rnext BOX89F(X) \leftrightarrow (BOX89F(X) \land $ \\ 
 $  \Rnext BOX646F(X))) \land $ \\ 
 $ ( \Rnext BOX522P(X) \leftrightarrow (BOX522P(X) \land $ \\ 
 $  \Rnext PinvG18P)) \land $ \\ 
 $ (BOX619F(X) \leftrightarrow  \Rbox DIAMOND318F(X)) \land $ \\ 
 $ (BOX20F(X) \leftrightarrow  \Rbox BOX581F(X)) \land $ \\ 
 $ (BOX417P(X) \leftrightarrow  \Rbox E1G27P(X)) \land $ \\ 
 $ (BOX578F(X) \leftrightarrow  \Rbox DIAMOND289F(X)) \land $ \\ 
 $ (BOX438P(X) \leftrightarrow  \Rbox E1G11P(X)) \land $ \\ 
 $ (BOX702P(X) \leftrightarrow  \Rbox BOX513P(X)) \land $ \\ 
 $ ( \Rnext BOX154P(X) \leftrightarrow (BOX154P(X) \land $ \\ 
 $  \Rnext C7P(X))) \land $ \\ 
 $ (BOX715P(X) \leftrightarrow  \Rbox BOX531P(X)) \land $ \\ 
 $ ( \Rnext BOX613F(X) \leftrightarrow (BOX613F(X) \land $ \\ 
 $  \Rnext E1G18F(X))) \land $ \\ 
 $ (BOX711P(X) \leftrightarrow  \Rbox BOX527P(X)) \land $ \\ 
 $ ( \Rnext BOX494P(X) \leftrightarrow (BOX494P(X) \land $ \\ 
 $  \Rnext BOX495P(X))) \land $ \\ 
 $ (BOX16F(X) \leftrightarrow  \Rbox BOX579F(X)) \land $ \\ 
 $ (BOX142P(X) \leftrightarrow  \Rbox DIAMOND143P(X)) \land $ \\ 
 $ ( \Rnext BOX547P(X) \leftrightarrow (BOX547P(X) \land $ \\ 
 $  \Rnext PG11P)) \land $ \\ 
 $ ( \Rnext BOX556P(X) \leftrightarrow (BOX556P(X) \land $ \\ 
 $  \Rnext PG14P)) \land $ \\ 
 $ (BOX647F(X) \leftrightarrow  \Rbox PG8F) \land $ \\ 
 $ (BOX457P(X) \leftrightarrow  \Rbox E1G17P(X)) \land $ \\ 
 $ ( \Rnext BOX189P(X) \leftrightarrow (BOX189P(X) \land $ \\ 
 $  \Rnext DIAMOND397P(X))) \land $ \\ 
 $ (BOX708P(X) \leftrightarrow  \Rbox BOX524P(X)) \land $ \\ 
 $ ( \Rnext BOX110F(X) \leftrightarrow (BOX110F(X) \land $ \\ 
 $  \Rnext BOX667F(X))) \land $ \\ 
 $ ( \Rnext BOX482P(X) \leftrightarrow (BOX482P(X) \land $ \\ 
 $  \Rnext BOX445P(X))) \land $ \\ 
 $ (BOX728P(X) \leftrightarrow  \Rbox BOX544P(X)) \land $ \\ 
 $ (BOX452P(X) \leftrightarrow  \Rbox E4G13P(X)) \land $ \\ 
 $ ( \Rnext BOX75F(X) \leftrightarrow (BOX75F(X) \land $ \\ 
 $  \Rnext BOX632F(X))) \land $ \\ 
 $ (BOX468P(X) \leftrightarrow  \Rbox E1G7P(X)) \land $ \\ 
 $ ( \Rnext BOX111F(X) \leftrightarrow (BOX111F(X) \land $ \\ 
 $  \Rnext BOX668F(X))) \land $ \\ 
 $ (BOX279F(X) \leftrightarrow  \Rbox DIAMOND209F(X)) \land $ \\ 
 $ (BOX476P(X) \leftrightarrow  \Rbox BOX691P(X)) \land $ \\ 
 $ ( \Rnext BOX575F(X) \leftrightarrow (BOX575F(X) \land $ \\ 
 $  \Rnext E1G13F(X))) \land $ \\ 
 $ (BOX51F(X) \leftrightarrow  \Rbox BOX612F(X)) \land $ \\ 
 $ (BOX707P(X) \leftrightarrow  \Rbox BOX523P(X)) \land $ \\ 
 $ ( \Rnext BOX508P(X) \leftrightarrow (BOX508P(X) \land $ \\ 
 $  \Rnext DIAMOND389P(X))) \land $ \\ 
 $ (BOX30F(X) \leftrightarrow  \Rbox BOX594F(X)) \land $ \\ 
 $ ( \Rnext BOX537P(X) \leftrightarrow (BOX537P(X) \land $ \\ 
 $  \Rnext PinvG11P)) \land $ \\ 
 $ ( \Rnext BOX317F(X) \leftrightarrow (BOX317F(X) \land $ \\ 
 $  \Rnext C12F(X))) \land $ \\ 
 $ (BOX374P(X) \leftrightarrow  \Rbox E1G5P(X)) \land $ \\ 
 $ (BOX718P(X) \leftrightarrow  \Rbox BOX534P(X)) \land $ \\ 
 $ (BOX731P(X) \leftrightarrow  \Rbox BOX547P(X)) \land $ \\ 
 $ ( \Rnext BOX520P(X) \leftrightarrow (BOX520P(X) \land $ \\ 
 $  \Rnext PinvG7P)) \land $ \\ 
 $ (BOX26F(X) \leftrightarrow  \Rbox (DIAMOND229F(X) \land $ \\ 
 $ DIAMOND231F(X))) \land $ \\ 
 $ (BOX643F(X) \leftrightarrow  \Rbox PG2F) \land $ \\ 
 $ (BOX705P(X) \leftrightarrow  \Rbox BOX521P(X)) \land $ \\ 
 $ ( \Rnext BOX600F(X) \leftrightarrow (BOX600F(X) \land $ \\ 
 $  \Rnext E1G10F(X))) \land $ \\ 
 $ ( \Rnext BOX420P(X) \leftrightarrow (BOX420P(X) \land $ \\ 
 $  \Rnext E4G4P(X))) \land $ \\ 
 $ ( \Rnext BOX432P(X) \leftrightarrow (BOX432P(X) \land $ \\ 
 $  \Rnext BOX433P(X))) \land $ \\ 
 $ (BOX654F(X) \leftrightarrow  \Rbox PG17F) \land $ \\ 
 $ (BOX309F(X) \leftrightarrow  \Rbox BOX611F(X)) \land $ \\ 
 $ ( \Rnext BOX586F(X) \leftrightarrow (BOX586F(X) \land $ \\ 
 $  \Rnext E1G28F(X))) \land $ \\ 
 $ (BOX576F(X) \leftrightarrow  \Rbox (BOX577F(X) \land $ \\ 
 $ DIAMOND217F(X))) \land $ \\ 
 $ (BOX473P(X) \leftrightarrow  \Rbox DIAMOND372P(X)) \land $ \\ 
 $ (BOX69F(X) \leftrightarrow  \Rbox BOX244F(X)) \land $ \\ 
 $ (BOX642F(X) \leftrightarrow  \Rbox PG16F) \land $ \\ 
 $ ( \Rnext BOX104F(X) \leftrightarrow (BOX104F(X) \land $ \\ 
 $  \Rnext BOX661F(X))) \land $ \\ 
 $ ( \Rnext BOX463P(X) \leftrightarrow (BOX463P(X) \land $ \\ 
 $  \Rnext BOX464P(X))) \land $ \\ 
 $ (BOX48F(X) \leftrightarrow  \Rbox BOX610F(X)) \land $ \\ 
 $ (BOX62F(X) \leftrightarrow  \Rbox BOX623F(X)) \land $ \\ 
 $ ( \Rnext BOX532P(X) \leftrightarrow (BOX532P(X) \land $ \\ 
 $  \Rnext PG2P)) \land $ \\ 
 $ ( \Rnext BOX467P(X) \leftrightarrow (BOX467P(X) \land $ \\ 
 $  \Rnext BOX468P(X))) \land $ \\ 
 $ ( \Rnext BOX405P(X) \leftrightarrow (BOX405P(X) \land $ \\ 
 $  \Rnext BOX406P(X))) \land $ \\ 
 $ (BOX296F(X) \leftrightarrow  \Rbox BOX582F(X)) \land $ \\ 
 $ (BOX512P(X) \leftrightarrow  \Rbox E4G0P(X)) \land $ \\ 
 $ (BOX640F(X) \leftrightarrow  \Rbox PG13F) \land $ \\ 
 $ ( \Rnext BOX177P(X) \leftrightarrow (BOX177P(X) \land $ \\ 
 $  \Rnext (BOX499P(X) \land $ \\ 
 $ DIAMOND178P(X)))) \land $ \\ 
 $ (BOX607F(X) \leftrightarrow  \Rbox BOX608F(X)) \land $ \\ 
 $ (BOX726P(X) \leftrightarrow  \Rbox BOX542P(X)) \land $ \\ 
 $ (BOX570F(X) \leftrightarrow  \Rbox BOX571F(X)) \land $ \\ 
 $ ( \Rnext BOX443P(X) \leftrightarrow (BOX443P(X) \land $ \\ 
 $  \Rnext (C7P(X) \land $ \\ 
 $ BOX445P(X)))) \land $ \\ 
 $ ( \Rnext BOX601F(X) \leftrightarrow (BOX601F(X) \land $ \\ 
 $  \Rnext E1G7F(X))) \land $ \\ 
 $ (BOX700P(X) \leftrightarrow  \Rbox BOX402P(X)) \land $ \\ 
 $ ( \Rnext BOX611F(X) \leftrightarrow (BOX611F(X) \land $ \\ 
 $  \Rnext DIAMOND238F(X))) \land $ \\ 
 $ ( \Rnext BOX146P(X) \leftrightarrow (BOX146P(X) \land $ \\ 
 $  \Rnext DIAMOND147P(X))) \land $ \\ 
 $ ( \Rnext BOX54F(X) \leftrightarrow (BOX54F(X) \land $ \\ 
 $  \Rnext DIAMOND310F(X))) \land $ \\ 
 $ ( \Rnext BOX495P(X) \leftrightarrow (BOX495P(X) \land $ \\ 
 $  \Rnext BOX496P(X))) \land $ \\ 
 $ (BOX663F(X) \leftrightarrow  \Rbox PG5F) \land $ \\ 
 $ ( \Rnext BOX324F(X) \leftrightarrow (BOX324F(X) \land $ \\ 
 $  \Rnext BOX683F(X))) \land $ \\ 
 $ (BOX354P(X) \leftrightarrow  \Rbox C0P(X)) \land $ \\ 
 $ ( \Rnext BOX100F(X) \leftrightarrow (BOX100F(X) \land $ \\ 
 $  \Rnext BOX657F(X))) \land $ \\ 
 $ (BOX738P(X) \leftrightarrow  \Rbox BOX554P(X)) \land $ \\ 
 $ ( \Rnext BOX614F(X) \leftrightarrow (BOX614F(X) \land $ \\ 
 $  \Rnext E5G14F(X))) \land $ \\ 
 $ (BOX628F(X) \leftrightarrow  \Rbox BOX629F(X)) \land $ \\ 
 $ (BOX697P(X) \leftrightarrow  \Rbox DIAMOND382P(X)) \land $ \\ 
 $ (BOX656F(X) \leftrightarrow  \Rbox PL6F) \land $ \\ 
 $ ( \Rnext BOX78F(X) \leftrightarrow (BOX78F(X) \land $ \\ 
 $  \Rnext BOX635F(X))) \land $ \\ 
 $ ( \Rnext BOX113F(X) \leftrightarrow (BOX113F(X) \land $ \\ 
 $  \Rnext BOX670F(X))) \land $ \\ 
 $ (BOX9F(X) \leftrightarrow  \Rbox E4G4F(X)) \land $ \\ 
 $ ( \Rnext BOX544P(X) \leftrightarrow (BOX544P(X) \land $ \\ 
 $  \Rnext PG27P)) \land $ \\ 
 $ (BOX670F(X) \leftrightarrow  \Rbox PinvG1F) \land $ \\ 
 $ ( \Rnext BOX620F(X) \leftrightarrow (BOX620F(X) \land $ \\ 
 $  \Rnext E2G20F(X))) \land $ \\ 
 $ ( \Rnext BOX376P(X) \leftrightarrow (BOX376P(X) \land $ \\ 
 $  \Rnext BOX486P(X))) \land $ \\ 
 $ ( \Rnext BOX630F(X) \leftrightarrow (BOX630F(X) \land $ \\ 
 $  \Rnext DIAMOND329F(X))) \land $ \\ 
 $ (BOX265F(X) \leftrightarrow  \Rbox DIAMOND328F(X)) \land $ \\ 
 $ (BOX638F(X) \leftrightarrow  \Rbox PG28F) \land $ \\ 
 $ (BOX660F(X) \leftrightarrow  \Rbox PG4F) \land $ \\ 
 $ (BOX123P(X) \leftrightarrow  \Rbox DIAMOND337P(X)) \land $ \\ 
 $ ( \Rnext BOX423P(X) \leftrightarrow (BOX423P(X) \land $ \\ 
 $  \Rnext BOX424P(X))) \land $ \\ 
 $ ( \Rnext BOX261F(X) \leftrightarrow (BOX261F(X) \land $ \\ 
 $  \Rnext DIAMOND228F(X))) \land $ \\ 
 $ ( \Rnext BOX502P(X) \leftrightarrow (BOX502P(X) \land $ \\ 
 $  \Rnext BOX503P(X))) \land $ \\ 
 $ (BOX415P(X) \leftrightarrow  \Rbox DIAMOND339P(X)) \land $ \\ 
 $ (BOX583F(X) \leftrightarrow  \Rbox DIAMOND224F(X)) \land $ \\ 
 $ ( \Rnext BOX680F(X) \leftrightarrow (BOX680F(X) \land $ \\ 
 $  \Rnext BOX681F(X))) \land $ \\ 
 $ (BOX631F(X) \leftrightarrow  \Rbox PinvG7F) \land $ \\ 
 $ (BOX693P(X) \leftrightarrow  \Rbox DIAMOND373P(X)) \land $ \\ 
 $ (BOX730P(X) \leftrightarrow  \Rbox BOX546P(X)) \land $ \\ 
 $ (BOX743P(X) \leftrightarrow  \Rbox BOX559P(X)) \land $ \\ 
 $ ( \Rnext BOX107F(X) \leftrightarrow (BOX107F(X) \land $ \\ 
 $  \Rnext BOX664F(X))) \land $ \\ 
 $ (BOX424P(X) \leftrightarrow  \Rbox E1G13P(X)) \land $ \\ 
 $ (BOX486P(X) \leftrightarrow  \Rbox DIAMOND161P(X)) \land $ \\ 
 $ (BOX736P(X) \leftrightarrow  \Rbox BOX552P(X))) \land $ \\ 
 $ (BOX613F(X) \leftrightarrow BOX490P(X)) \land $ \\ 
 $ (DIAMOND313F(X) \leftrightarrow DIAMOND380P(X)) \land $ \\ 
 $ (PG20F \leftrightarrow PG20F) \land $ \\ 
 $ (BOX303F(X) \leftrightarrow BOX369P(X)) \land $ \\ 
 $ (PG28F \leftrightarrow PG28F) \land $ \\ 
 $ (E1G6F(X) \leftrightarrow E1G6P(X)) \land $ \\ 
 $ (BOX92F(X) \leftrightarrow BOX722P(X)) \land $ \\ 
 $ (BOX296F(X) \leftrightarrow BOX361P(X)) \land $ \\ 
 $ (BOX641F(X) \leftrightarrow BOX530P(X)) \land $ \\ 
 $ (C21F(X) \leftrightarrow C21P(X)) \land $ \\ 
 $ (DIAMOND285F(X) \leftrightarrow DIAMOND348P(X)) \land $ \\ 
 $ (BOX582F(X) \leftrightarrow BOX434P(X)) \land $ \\ 
 $ (BOX670F(X) \leftrightarrow BOX559P(X)) \land $ \\ 
 $ (BOX52F(X) \leftrightarrow BOX489P(X)) \land $ \\ 
 $ (BOX91F(X) \leftrightarrow BOX721P(X)) \land $ \\ 
 $ (DIAMOND306F(X) \leftrightarrow DIAMOND372P(X)) \land $ \\ 
 $ (BOX225F(X) \leftrightarrow BOX146P(X)) \land $ \\ 
 $ (BOX56F(X) \leftrightarrow BOX498P(X)) \land $ \\ 
 $ (BOX280F(X) \leftrightarrow BOX342P(X)) \land $ \\ 
 $ (BOX626F(X) \leftrightarrow BOX513P(X)) \land $ \\ 
 $ (C5F(X) \leftrightarrow C5P(X)) \land $ \\ 
 $ (BOX672F(X) \leftrightarrow BOX561P(X)) \land $ \\ 
 $ (DIAMOND259F(X) \leftrightarrow DIAMOND183P(X)) \land $ \\ 
 $ (BOX599F(X) \leftrightarrow BOX464P(X)) \land $ \\ 
 $ (BOX54F(X) \leftrightarrow BOX695P(X)) \land $ \\ 
 $ (E1G20InvF(X) \leftrightarrow E1G20InvP(X)) \land $ \\ 
 $ (BOX628F(X) \leftrightarrow BOX517P(X)) \land $ \\ 
 $ (DIAMOND242F(X) \leftrightarrow DIAMOND165P(X)) \land $ \\ 
 $ (BOX676F(X) \leftrightarrow BOX691P(X)) \land $ \\ 
 $ (BOX47F(X) \leftrightarrow BOX483P(X)) \land $ \\ 
 $ (BOX308F(X) \leftrightarrow BOX374P(X)) \land $ \\ 
 $ (DIAMOND239F(X) \leftrightarrow DIAMOND162P(X)) \land $ \\ 
 $ (E3G1F(X) \leftrightarrow E3G1P(X)) \land $ \\ 
 $ (BOX37F(X) \leftrightarrow BOX461P(X)) \land $ \\ 
 $ (PinvG9F \leftrightarrow PinvG9P) \land $ \\ 
 $ (PinvG7F \leftrightarrow PinvG7P) \land $ \\ 
 $ (BOX314F(X) \leftrightarrow BOX381P(X)) \land $ \\ 
 $ (DIAMOND310F(X) \leftrightarrow DIAMOND377P(X)) \land $ \\ 
 $ (PG7F \leftrightarrow PG7P) \land $ \\ 
 $ (PinvG14F \leftrightarrow PinvG14F) \land $ \\ 
 $ (BOX611F(X) \leftrightarrow BOX486P(X)) \land $ \\ 
 $ (BOX240F(X) \leftrightarrow BOX163P(X)) \land $ \\ 
 $ (PG5F \leftrightarrow PG5F) \land $ \\ 
 $ (BOX35F(X) \leftrightarrow BOX458P(X)) \land $ \\ 
 $ (BOX3F(X) \leftrightarrow BOX403P(X)) \land $ \\ 
 $ (E1G1InvF(X) \leftrightarrow E1G1InvP(X)) \land $ \\ 
 $ (BOX83F(X) \leftrightarrow BOX713P(X)) \land $ \\ 
 $ (DIAMOND215F(X) \leftrightarrow DIAMOND136P(X)) \land $ \\ 
 $ (BOX609F(X) \leftrightarrow BOX480P(X)) \land $ \\ 
 $ (E1G21InvF(X) \leftrightarrow E1G21InvP(X)) \land $ \\ 
 $ (BOX269F(X) \leftrightarrow BOX194P(X)) \land $ \\ 
 $ (BOX668F(X) \leftrightarrow BOX557P(X)) \land $ \\ 
 $ (E5G18F(X) \leftrightarrow E5G18P(X)) \land $ \\ 
 $ (BOX664F(X) \leftrightarrow BOX553P(X)) \land $ \\ 
 $ (BOX634F(X) \leftrightarrow BOX523P(X)) \land $ \\ 
 $ (E2G20F(X) \leftrightarrow E2G20P(X)) \land $ \\ 
 $ (BOX601F(X) \leftrightarrow BOX468P(X)) \land $ \\ 
 $ (BOX99F(X) \leftrightarrow BOX729P(X)) \land $ \\ 
 $ (PG13F \leftrightarrow PG13F) \land $ \\ 
 $ (E1G5F(X) \leftrightarrow E1G5P(X)) \land $ \\ 
 $ (BOX12F(X) \leftrightarrow BOX421P(X)) \land $ \\ 
 $ (PG13F \leftrightarrow PG13P) \land $ \\ 
 $ (BOX580F(X) \leftrightarrow BOX431P(X)) \land $ \\ 
 $ (BOX95F(X) \leftrightarrow BOX725P(X)) \land $ \\ 
 $ (BOX115F(X) \leftrightarrow BOX745P(X)) \land $ \\ 
 $ (PG16F \leftrightarrow PG16P) \land $ \\ 
 $ (PinvG9F \leftrightarrow PinvG9F) \land $ \\ 
 $ (PinvG27F \leftrightarrow PinvG27P) \land $ \\ 
 $ (DIAMOND10F(X) \leftrightarrow DIAMOND341P(X)) \land $ \\ 
 $ (DIAMOND252F(X) \leftrightarrow DIAMOND176P(X)) \land $ \\ 
 $ (DIAMOND326F(X) \leftrightarrow DIAMOND395P(X)) \land $ \\ 
 $ (BOX279F(X) \leftrightarrow BOX340P(X)) \land $ \\ 
 $ (BOX74F(X) \leftrightarrow BOX704P(X)) \land $ \\ 
 $ (DIAMOND230F(X) \leftrightarrow DIAMOND151P(X)) \land $ \\ 
 $ (PinvG27F \leftrightarrow PinvG27F) \land $ \\ 
 $ (E1G9InvF(X) \leftrightarrow E1G9InvP(X)) \land $ \\ 
 $ (PG0F \leftrightarrow PG0P) \land $ \\ 
 $ (C0F(X) \leftrightarrow C0P(X)) \land $ \\ 
 $ (E3G8F(X) \leftrightarrow E3G8P(X)) \land $ \\ 
 $ (PinvG17F \leftrightarrow PinvG17P) \land $ \\ 
 $ (BOX34F(X) \leftrightarrow BOX456P(X)) \land $ \\ 
 $ (BOX636F(X) \leftrightarrow BOX525P(X)) \land $ \\ 
 $ (DIAMOND299F(X) \leftrightarrow DIAMOND364P(X)) \land $ \\ 
 $ (DIAMOND206F(X) \leftrightarrow DIAMOND127P(X)) \land $ \\ 
 $ (DIAMOND276F(X) \leftrightarrow DIAMOND337P(X)) \land $ \\ 
 $ (DIAMOND220F(X) \leftrightarrow DIAMOND141P(X)) \land $ \\ 
 $ (BOX268F(X) \leftrightarrow BOX192P(X)) \land $ \\ 
 $ (BOX44F(X) \leftrightarrow BOX479P(X)) \land $ \\ 
 $ (DIAMOND282F(X) \leftrightarrow DIAMOND344P(X)) \land $ \\ 
 $ (DIAMOND318F(X) \leftrightarrow DIAMOND385P(X)) \land $ \\ 
 $ (PinvG6F \leftrightarrow PinvG6P) \land $ \\ 
 $ (C20F(X) \leftrightarrow C20P(X)) \land $ \\ 
 $ (BOX585F(X) \leftrightarrow BOX438P(X)) \land $ \\ 
 $ (PG4F \leftrightarrow PG4F) \land $ \\ 
 $ (BOX594F(X) \leftrightarrow BOX454P(X)) \land $ \\ 
 $ (BOX674F(X) \leftrightarrow BOX688P(X)) \land $ \\ 
 $ (DIAMOND294F(X) \leftrightarrow DIAMOND358P(X)) \land $ \\ 
 $ (DIAMOND72F(X) \leftrightarrow DIAMOND193P(X)) \land $ \\ 
 $ (BOX284F(X) \leftrightarrow BOX346P(X)) \land $ \\ 
 $ (BOX28F(X) \leftrightarrow BOX449P(X)) \land $ \\ 
 $ (DIAMOND254F(X) \leftrightarrow DIAMOND178P(X)) \land $ \\ 
 $ (BOX322F(X) \leftrightarrow BOX390P(X)) \land $ \\ 
 $ (C28F(X) \leftrightarrow C28P(X)) \land $ \\ 
 $ (BOX38F(X) \leftrightarrow BOX463P(X)) \land $ \\ 
 $ (BOX27F(X) \leftrightarrow BOX447P(X)) \land $ \\ 
 $ (DIAMOND67F(X) \leftrightarrow DIAMOND393P(X)) \land $ \\ 
 $ (BOX586F(X) \leftrightarrow BOX440P(X)) \land $ \\ 
 $ (BOX93F(X) \leftrightarrow BOX723P(X)) \land $ \\ 
 $ (BOX96F(X) \leftrightarrow BOX726P(X)) \land $ \\ 
 $ (BOX75F(X) \leftrightarrow BOX705P(X)) \land $ \\ 
 $ (DIAMOND290F(X) \leftrightarrow DIAMOND353P(X)) \land $ \\ 
 $ (C9F(X) \leftrightarrow C9P(X)) \land $ \\ 
 $ (BOX569F(X) \leftrightarrow BOX412P(X)) \land $ \\ 
 $ (BOX41F(X) \leftrightarrow BOX469P(X)) \land $ \\ 
 $ (BOX572F(X) \leftrightarrow BOX417P(X)) \land $ \\ 
 $ (DIAMOND286F(X) \leftrightarrow DIAMOND349P(X)) \land $ \\ 
 $ (BOX584F(X) \leftrightarrow BOX436P(X)) \land $ \\ 
 $ (DIAMOND329F(X) \leftrightarrow DIAMOND398P(X)) \land $ \\ 
 $ (BOX13F(X) \leftrightarrow BOX423P(X)) \land $ \\ 
 $ (E4G13F(X) \leftrightarrow E4G13P(X)) \land $ \\ 
 $ (BOX18F(X) \leftrightarrow BOX686P(X)) \land $ \\ 
 $ (BOX277F(X) \leftrightarrow BOX338P(X)) \land $ \\ 
 $ (DIAMOND205F(X) \leftrightarrow DIAMOND126P(X)) \land $ \\ 
 $ (PinvG17F \leftrightarrow PinvG17F) \land $ \\ 
 $ (BOX86F(X) \leftrightarrow BOX716P(X)) \land $ \\ 
 $ (C26F(X) \leftrightarrow C26P(X)) \land $ \\ 
 $ (BOX25F(X) \leftrightarrow BOX441P(X)) \land $ \\ 
 $ (BOX571F(X) \leftrightarrow BOX415P(X)) \land $ \\ 
 $ (DIAMOND218F(X) \leftrightarrow DIAMOND139P(X)) \land $ \\ 
 $ (BOX106F(X) \leftrightarrow BOX736P(X)) \land $ \\ 
 $ (DIAMOND197F(X) \leftrightarrow DIAMOND117P(X)) \land $ \\ 
 $ (PinvG2F \leftrightarrow PinvG2F) \land $ \\ 
 $ (PG6F \leftrightarrow PG6F) \land $ \\ 
 $ (BOX662F(X) \leftrightarrow BOX551P(X)) \land $ \\ 
 $ (E1G28F(X) \leftrightarrow E1G28P(X)) \land $ \\ 
 $ (BOX612F(X) \leftrightarrow BOX488P(X)) \land $ \\ 
 $ (BOX598F(X) \leftrightarrow BOX462P(X)) \land $ \\ 
 $ (PG14F \leftrightarrow PG14P) \land $ \\ 
 $ (E1G18InvF(X) \leftrightarrow E1G18InvP(X)) \land $ \\ 
 $ (BOX583F(X) \leftrightarrow BOX435P(X)) \land $ \\ 
 $ (PG11F \leftrightarrow PG11F) \land $ \\ 
 $ (DIAMOND312F(X) \leftrightarrow DIAMOND379P(X)) \land $ \\ 
 $ (BOX565F(X) \leftrightarrow BOX408P(X)) \land $ \\ 
 $ (PL6F \leftrightarrow PL6P) \land $ \\ 
 $ (BOX0F(X) \leftrightarrow BOX401P(X)) \land $ \\ 
 $ (BOX68F(X) \leftrightarrow BOX702P(X)) \land $ \\ 
 $ (BOX614F(X) \leftrightarrow BOX492P(X)) \land $ \\ 
 $ (DIAMOND227F(X) \leftrightarrow DIAMOND148P(X)) \land $ \\ 
 $ (BOX658F(X) \leftrightarrow BOX547P(X)) \land $ \\ 
 $ (DIAMOND204F(X) \leftrightarrow DIAMOND125P(X)) \land $ \\ 
 $ (E2G13F(X) \leftrightarrow E2G13P(X)) \land $ \\ 
 $ (BOX7F(X) \leftrightarrow BOX416P(X)) \land $ \\ 
 $ (C6F(X) \leftrightarrow C6P(X)) \land $ \\ 
 $ (DIAMOND257F(X) \leftrightarrow DIAMOND181P(X)) \land $ \\ 
 $ (DIAMOND19F(X) \leftrightarrow DIAMOND355P(X)) \land $ \\ 
 $ (E1G11InvF(X) \leftrightarrow E1G11InvP(X)) \land $ \\ 
 $ (BOX316F(X) \leftrightarrow BOX383P(X)) \land $ \\ 
 $ (PL6F \leftrightarrow PL6F) \land $ \\ 
 $ (DIAMOND207F(X) \leftrightarrow DIAMOND128P(X)) \land $ \\ 
 $ (BOX79F(X) \leftrightarrow BOX709P(X)) \land $ \\ 
 $ (DIAMOND263F(X) \leftrightarrow DIAMOND187P(X)) \land $ \\ 
 $ (BOX587F(X) \leftrightarrow BOX442P(X)) \land $ \\ 
 $ (E4G7F(X) \leftrightarrow E4G7P(X)) \land $ \\ 
 $ (E1G27F(X) \leftrightarrow E1G27P(X)) \land $ \\ 
 $ (E1G27InvF(X) \leftrightarrow E1G27InvP(X)) \land $ \\ 
 $ (BOX50F(X) \leftrightarrow BOX694P(X)) \land $ \\ 
 $ (BOX105F(X) \leftrightarrow BOX735P(X)) \land $ \\ 
 $ (BOX14F(X) \leftrightarrow BOX685P(X)) \land $ \\ 
 $ (PinvL6F \leftrightarrow PinvL6P) \land $ \\ 
 $ (DIAMOND203F(X) \leftrightarrow DIAMOND124P(X)) \land $ \\ 
 $ (DIAMOND320F(X) \leftrightarrow DIAMOND388P(X)) \land $ \\ 
 $ (PG10F \leftrightarrow PG10F) \land $ \\ 
 $ (E1G2F(X) \leftrightarrow E1G2P(X)) \land $ \\ 
 $ (E1G14InvF(X) \leftrightarrow E1G14InvP(X)) \land $ \\ 
 $ (BOX640F(X) \leftrightarrow BOX529P(X)) \land $ \\ 
 $ (BOX16F(X) \leftrightarrow BOX428P(X)) \land $ \\ 
 $ (BOX265F(X) \leftrightarrow BOX189P(X)) \land $ \\ 
 $ (BOX223F(X) \leftrightarrow BOX144P(X)) \land $ \\ 
 $ (BOX678F(X) \leftrightarrow BOX693P(X)) \land $ \\ 
 $ (PinvG0F \leftrightarrow PinvG0F) \land $ \\ 
 $ (BOX615F(X) \leftrightarrow BOX494P(X)) \land $ \\ 
 $ (BOX97F(X) \leftrightarrow BOX727P(X)) \land $ \\ 
 $ (PinvG1F \leftrightarrow PinvG1P) \land $ \\ 
 $ (BOX566F(X) \leftrightarrow BOX409P(X)) \land $ \\ 
 $ (DIAMOND212F(X) \leftrightarrow DIAMOND133P(X)) \land $ \\ 
 $ (BOX652F(X) \leftrightarrow BOX541P(X)) \land $ \\ 
 $ (E1G5InvF(X) \leftrightarrow E1G5InvP(X)) \land $ \\ 
 $ (DIAMOND232F(X) \leftrightarrow DIAMOND153P(X)) \land $ \\ 
 $ (DIAMOND236F(X) \leftrightarrow DIAMOND159P(X)) \land $ \\ 
 $ (PG9F \leftrightarrow PG9P) \land $ \\ 
 $ (C25F(X) \leftrightarrow C25P(X)) \land $ \\ 
 $ (PinvG4F \leftrightarrow PinvG4F) \land $ \\ 
 $ (BOX88F(X) \leftrightarrow BOX718P(X)) \land $ \\ 
 $ (BOX17F(X) \leftrightarrow BOX430P(X)) \land $ \\ 
 $ (BOX645F(X) \leftrightarrow BOX534P(X)) \land $ \\ 
 $ (BOX102F(X) \leftrightarrow BOX732P(X)) \land $ \\ 
 $ (BOX577F(X) \leftrightarrow BOX426P(X)) \land $ \\ 
 $ (BOX208F(X) \leftrightarrow BOX129P(X)) \land $ \\ 
 $ (BOX654F(X) \leftrightarrow BOX543P(X)) \land $ \\ 
 $ (PG14F \leftrightarrow PG14F) \land $ \\ 
 $ (PG1F \leftrightarrow PG1F) \land $ \\ 
 $ (BOX620F(X) \leftrightarrow BOX501P(X)) \land $ \\ 
 $ (DIAMOND262F(X) \leftrightarrow DIAMOND186P(X)) \land $ \\ 
 $ (PinvG10F \leftrightarrow PinvG10P) \land $ \\ 
 $ (DIAMOND229F(X) \leftrightarrow DIAMOND150P(X)) \land $ \\ 
 $ (E1G0F(X) \leftrightarrow E1G0P(X)) \land $ \\ 
 $ (PinvG28F \leftrightarrow PinvG28F) \land $ \\ 
 $ (BOX24F(X) \leftrightarrow BOX439P(X)) \land $ \\ 
 $ (DIAMOND214F(X) \leftrightarrow DIAMOND135P(X)) \land $ \\ 
 $ (DIAMOND315F(X) \leftrightarrow DIAMOND382P(X)) \land $ \\ 
 $ (PinvG0F \leftrightarrow PinvG0P) \land $ \\ 
 $ (E1G1F(X) \leftrightarrow E1G1P(X)) \land $ \\ 
 $ (E3G13F(X) \leftrightarrow E3G13P(X)) \land $ \\ 
 $ (BOX677F(X) \leftrightarrow BOX692P(X)) \land $ \\ 
 $ (PG27F \leftrightarrow PG27P) \land $ \\ 
 $ (DIAMOND248F(X) \leftrightarrow DIAMOND171P(X)) \land $ \\ 
 $ (BOX23F(X) \leftrightarrow BOX437P(X)) \land $ \\ 
 $ (BOX113F(X) \leftrightarrow BOX743P(X)) \land $ \\ 
 $ (PinvG16F \leftrightarrow PinvG16P) \land $ \\ 
 $ (BOX671F(X) \leftrightarrow BOX560P(X)) \land $ \\ 
 $ (BOX244F(X) \leftrightarrow BOX167P(X)) \land $ \\ 
 $ (DIAMOND258F(X) \leftrightarrow DIAMOND182P(X)) \land $ \\ 
 $ (BOX283F(X) \leftrightarrow BOX345P(X)) \land $ \\ 
 $ (PG18F \leftrightarrow PG18P) \land $ \\ 
 $ (DIAMOND15F(X) \leftrightarrow DIAMOND347P(X)) \land $ \\ 
 $ (DIAMOND228F(X) \leftrightarrow DIAMOND149P(X)) \land $ \\ 
 $ (C1F(X) \leftrightarrow C1P(X)) \land $ \\ 
 $ (BOX665F(X) \leftrightarrow BOX554P(X)) \land $ \\ 
 $ (DIAMOND211F(X) \leftrightarrow DIAMOND132P(X)) \land $ \\ 
 $ (BOX78F(X) \leftrightarrow BOX708P(X)) \land $ \\ 
 $ (BOX71F(X) \leftrightarrow BOX703P(X)) \land $ \\ 
 $ (DIAMOND273F(X) \leftrightarrow DIAMOND334P(X)) \land $ \\ 
 $ (BOX622F(X) \leftrightarrow BOX505P(X)) \land $ \\ 
 $ (DIAMOND311F(X) \leftrightarrow DIAMOND378P(X)) \land $ \\ 
 $ (E5G17F(X) \leftrightarrow E5G17P(X)) \land $ \\ 
 $ (DIAMOND196F(X) \leftrightarrow DIAMOND116P(X)) \land $ \\ 
 $ (BOX649F(X) \leftrightarrow BOX538P(X)) \land $ \\ 
 $ (BOX621F(X) \leftrightarrow BOX503P(X)) \land $ \\ 
 $ (E1G9F(X) \leftrightarrow E1G9P(X)) \land $ \\ 
 $ (BOX202F(X) \leftrightarrow BOX123P(X)) \land $ \\ 
 $ (BOX325F(X) \leftrightarrow BOX394P(X)) \land $ \\ 
 $ (DIAMOND213F(X) \leftrightarrow DIAMOND134P(X)) \land $ \\ 
 $ (BOX602F(X) \leftrightarrow BOX470P(X)) \land $ \\ 
 $ (DIAMOND302F(X) \leftrightarrow DIAMOND368P(X)) \land $ \\ 
 $ (BOX656F(X) \leftrightarrow BOX545P(X)) \land $ \\ 
 $ (BOX573F(X) \leftrightarrow BOX419P(X)) \land $ \\ 
 $ (BOX593F(X) \leftrightarrow BOX452P(X)) \land $ \\ 
 $ (BOX605F(X) \leftrightarrow BOX474P(X)) \land $ \\ 
 $ (BOX70F(X) \leftrightarrow BOX515P(X)) \land $ \\ 
 $ (BOX576F(X) \leftrightarrow BOX425P(X)) \land $ \\ 
 $ (BOX618F(X) \leftrightarrow BOX497P(X)) \land $ \\ 
 $ (DIAMOND2F(X) \leftrightarrow DIAMOND119P(X)) \land $ \\ 
 $ (BOX655F(X) \leftrightarrow BOX544P(X)) \land $ \\ 
 $ (BOX233F(X) \leftrightarrow BOX154P(X)) \land $ \\ 
 $ (BOX29F(X) \leftrightarrow BOX451P(X)) \land $ \\ 
 $ (DIAMOND1F(X) \leftrightarrow DIAMOND331P(X)) \land $ \\ 
 $ (E5G5F(X) \leftrightarrow E5G5P(X)) \land $ \\ 
 $ (BOX59F(X) \leftrightarrow BOX500P(X)) \land $ \\ 
 $ (E5G27F(X) \leftrightarrow E5G27P(X)) \land $ \\ 
 $ (BOX111F(X) \leftrightarrow BOX741P(X)) \land $ \\ 
 $ (BOX253F(X) \leftrightarrow BOX177P(X)) \land $ \\ 
 $ (BOX281F(X) \leftrightarrow BOX343P(X)) \land $ \\ 
 $ (DIAMOND222F(X) \leftrightarrow DIAMOND143P(X)) \land $ \\ 
 $ (BOX595F(X) \leftrightarrow BOX455P(X)) \land $ \\ 
 $ (BOX39F(X) \leftrightarrow BOX465P(X)) \land $ \\ 
 $ (BOX4F(X) \leftrightarrow BOX405P(X)) \land $ \\ 
 $ (BOX324F(X) \leftrightarrow BOX392P(X)) \land $ \\ 
 $ (E1G28InvF(X) \leftrightarrow E1G28InvP(X)) \land $ \\ 
 $ (BOX657F(X) \leftrightarrow BOX546P(X)) \land $ \\ 
 $ (BOX581F(X) \leftrightarrow BOX433P(X)) \land $ \\ 
 $ (DIAMOND32F(X) \leftrightarrow DIAMOND155P(X)) \land $ \\ 
 $ (BOX256F(X) \leftrightarrow BOX180P(X)) \land $ \\ 
 $ (BOX108F(X) \leftrightarrow BOX738P(X)) \land $ \\ 
 $ (PG11F \leftrightarrow PG11P) \land $ \\ 
 $ (C17F(X) \leftrightarrow C17P(X)) \land $ \\ 
 $ (E1G16F(X) \leftrightarrow E1G16P(X)) \land $ \\ 
 $ (BOX562F(X) \leftrightarrow BOX402P(X)) \land $ \\ 
 $ (E5G11F(X) \leftrightarrow E5G11P(X)) \land $ \\ 
 $ (BOX660F(X) \leftrightarrow BOX549P(X)) \land $ \\ 
 $ (E4G4F(X) \leftrightarrow E4G4P(X)) \land $ \\ 
 $ (DIAMOND278F(X) \leftrightarrow DIAMOND339P(X)) \land $ \\ 
 $ (BOX682F(X) \leftrightarrow BOX700P(X)) \land $ \\ 
 $ (E1G17InvF(X) \leftrightarrow E1G17InvP(X)) \land $ \\ 
 $ (BOX291F(X) \leftrightarrow BOX354P(X)) \land $ \\ 
 $ (BOX57F(X) \leftrightarrow BOX696P(X)) \land $ \\ 
 $ (PinvG21F \leftrightarrow PinvG21P) \land $ \\ 
 $ (BOX638F(X) \leftrightarrow BOX527P(X)) \land $ \\ 
 $ (BOX681F(X) \leftrightarrow BOX699P(X)) \land $ \\ 
 $ (BOX653F(X) \leftrightarrow BOX542P(X)) \land $ \\ 
 $ (PinvG20F \leftrightarrow PinvG20F) \land $ \\ 
 $ (BOX298F(X) \leftrightarrow BOX363P(X)) \land $ \\ 
 $ (PG18F \leftrightarrow PG18F) \land $ \\ 
 $ (DIAMOND241F(X) \leftrightarrow DIAMOND164P(X)) \land $ \\ 
 $ (E1G4InvF(X) \leftrightarrow E1G4InvP(X)) \land $ \\ 
 $ (E5G2F(X) \leftrightarrow E5G2P(X)) \land $ \\ 
 $ (PinvG4F \leftrightarrow PinvG4P) \land $ \\ 
 $ (C29F(X) \leftrightarrow C29P(X)) \land $ \\ 
 $ (BOX80F(X) \leftrightarrow BOX710P(X)) \land $ \\ 
 $ (BOX9F(X) \leftrightarrow BOX420P(X)) \land $ \\ 
 $ (BOX639F(X) \leftrightarrow BOX528P(X)) \land $ \\ 
 $ (BOX610F(X) \leftrightarrow BOX485P(X)) \land $ \\ 
 $ (BOX630F(X) \leftrightarrow BOX519P(X)) \land $ \\ 
 $ (DIAMOND224F(X) \leftrightarrow DIAMOND145P(X)) \land $ \\ 
 $ (BOX644F(X) \leftrightarrow BOX533P(X)) \land $ \\ 
 $ (DIAMOND219F(X) \leftrightarrow DIAMOND140P(X)) \land $ \\ 
 $ (BOX570F(X) \leftrightarrow BOX414P(X)) \land $ \\ 
 $ (BOX20F(X) \leftrightarrow BOX432P(X)) \land $ \\ 
 $ (DIAMOND49F(X) \leftrightarrow DIAMOND375P(X)) \land $ \\ 
 $ (BOX608F(X) \leftrightarrow BOX478P(X)) \land $ \\ 
 $ (PinvG13F \leftrightarrow PinvG13F) \land $ \\ 
 $ (DIAMOND58F(X) \leftrightarrow DIAMOND174P(X)) \land $ \\ 
 $ (PinvG10F \leftrightarrow PinvG10F) \land $ \\ 
 $ (PinvG6F \leftrightarrow PinvG6F) \land $ \\ 
 $ (DIAMOND328F(X) \leftrightarrow DIAMOND397P(X)) \land $ \\ 
 $ (BOX623F(X) \leftrightarrow BOX507P(X)) \land $ \\ 
 $ (E1G6InvF(X) \leftrightarrow E1G6InvP(X)) \land $ \\ 
 $ (DIAMOND210F(X) \leftrightarrow DIAMOND131P(X)) \land $ \\ 
 $ (BOX568F(X) \leftrightarrow BOX411P(X)) \land $ \\ 
 $ (PinvG20F \leftrightarrow PinvG20P) \land $ \\ 
 $ (E1L6InvF(X) \leftrightarrow E1L6InvP(X)) \land $ \\ 
 $ (DIAMOND297F(X) \leftrightarrow DIAMOND362P(X)) \land $ \\ 
 $ (BOX661F(X) \leftrightarrow BOX550P(X)) \land $ \\ 
 $ (BOX112F(X) \leftrightarrow BOX742P(X)) \land $ \\ 
 $ (PG8F \leftrightarrow PG8F) \land $ \\ 
 $ (PG10F \leftrightarrow PG10P) \land $ \\ 
 $ (BOX669F(X) \leftrightarrow BOX558P(X)) \land $ \\ 
 $ (E1G13InvF(X) \leftrightarrow E1G13InvP(X)) \land $ \\ 
 $ (BOX574F(X) \leftrightarrow BOX422P(X)) \land $ \\ 
 $ (BOX673F(X) \leftrightarrow BOX687P(X)) \land $ \\ 
 $ (BOX81F(X) \leftrightarrow BOX711P(X)) \land $ \\ 
 $ (E4G10F(X) \leftrightarrow E4G10P(X)) \land $ \\ 
 $ (BOX40F(X) \leftrightarrow BOX467P(X)) \land $ \\ 
 $ (BOX567F(X) \leftrightarrow BOX410P(X)) \land $ \\ 
 $ (BOX237F(X) \leftrightarrow BOX160P(X)) \land $ \\ 
 $ (BOX76F(X) \leftrightarrow BOX706P(X)) \land $ \\ 
 $ (DIAMOND304F(X) \leftrightarrow DIAMOND370P(X)) \land $ \\ 
 $ (DIAMOND255F(X) \leftrightarrow DIAMOND179P(X)) \land $ \\ 
 $ (BOX624F(X) \leftrightarrow BOX510P(X)) \land $ \\ 
 $ (DIAMOND323F(X) \leftrightarrow DIAMOND391P(X)) \land $ \\ 
 $ (BOX317F(X) \leftrightarrow BOX384P(X)) \land $ \\ 
 $ (DIAMOND300F(X) \leftrightarrow DIAMOND365P(X)) \land $ \\ 
 $ (BOX234F(X) \leftrightarrow BOX157P(X)) \land $ \\ 
 $ (BOX101F(X) \leftrightarrow BOX731P(X)) \land $ \\ 
 $ (BOX61F(X) \leftrightarrow BOX504P(X)) \land $ \\ 
 $ (BOX646F(X) \leftrightarrow BOX535P(X)) \land $ \\ 
 $ (PG27F \leftrightarrow PG27F) \land $ \\ 
 $ (DIAMOND251F(X) \leftrightarrow DIAMOND175P(X)) \land $ \\ 
 $ (BOX625F(X) \leftrightarrow BOX512P(X)) \land $ \\ 
 $ (E4G0F(X) \leftrightarrow E4G0P(X)) \land $ \\ 
 $ (DIAMOND292F(X) \leftrightarrow DIAMOND356P(X)) \land $ \\ 
 $ (BOX98F(X) \leftrightarrow BOX728P(X)) \land $ \\ 
 $ (DIAMOND267F(X) \leftrightarrow DIAMOND191P(X)) \land $ \\ 
 $ (BOX51F(X) \leftrightarrow BOX487P(X)) \land $ \\ 
 $ (PG6F \leftrightarrow PG6P) \land $ \\ 
 $ (BOX42F(X) \leftrightarrow BOX471P(X)) \land $ \\ 
 $ (BOX659F(X) \leftrightarrow BOX548P(X)) \land $ \\ 
 $ (BOX66F(X) \leftrightarrow BOX511P(X)) \land $ \\ 
 $ (DIAMOND33F(X) \leftrightarrow DIAMOND156P(X)) \land $ \\ 
 $ (BOX107F(X) \leftrightarrow BOX737P(X)) \land $ \\ 
 $ (PinvG5F \leftrightarrow PinvG5F) \land $ \\ 
 $ (BOX650F(X) \leftrightarrow BOX539P(X)) \land $ \\ 
 $ (E1G10F(X) \leftrightarrow E1G10P(X)) \land $ \\ 
 $ (E1G21F(X) \leftrightarrow E1G21P(X)) \land $ \\ 
 $ (DIAMOND272F(X) \leftrightarrow DIAMOND333P(X)) \land $ \\ 
 $ (BOX589F(X) \leftrightarrow BOX444P(X)) \land $ \\ 
 $ (PinvG1F \leftrightarrow PinvG1F) \land $ \\ 
 $ (BOX288F(X) \leftrightarrow BOX351P(X)) \land $ \\ 
 $ (BOX85F(X) \leftrightarrow BOX715P(X)) \land $ \\ 
 $ (BOX90F(X) \leftrightarrow BOX720P(X)) \land $ \\ 
 $ (BOX55F(X) \leftrightarrow BOX493P(X)) \land $ \\ 
 $ (DIAMOND231F(X) \leftrightarrow DIAMOND152P(X)) \land $ \\ 
 $ (BOX43F(X) \leftrightarrow BOX475P(X)) \land $ \\ 
 $ (BOX642F(X) \leftrightarrow BOX531P(X)) \land $ \\ 
 $ (E5G28F(X) \leftrightarrow E5G28P(X)) \land $ \\ 
 $ (PG20F \leftrightarrow PG20P) \land $ \\ 
 $ (DIAMOND275F(X) \leftrightarrow DIAMOND336P(X)) \land $ \\ 
 $ (E1G17F(X) \leftrightarrow E1G17P(X)) \land $ \\ 
 $ (PG0F \leftrightarrow PG0F) \land $ \\ 
 $ (BOX274F(X) \leftrightarrow BOX335P(X)) \land $ \\ 
 $ (PG4F \leftrightarrow PG4P) \land $ \\ 
 $ (E1G14F(X) \leftrightarrow E1G14P(X)) \land $ \\ 
 $ (E1L6F(X) \leftrightarrow E1L6P(X)) \land $ \\ 
 $ (BOX109F(X) \leftrightarrow BOX739P(X)) \land $ \\ 
 $ (E1G10InvF(X) \leftrightarrow E1G10InvP(X)) \land $ \\ 
 $ (BOX6F(X) \leftrightarrow BOX413P(X)) \land $ \\ 
 $ (PinvG28F \leftrightarrow PinvG28P) \land $ \\ 
 $ (BOX319F(X) \leftrightarrow BOX387P(X)) \land $ \\ 
 $ (PG5F \leftrightarrow PG5P) \land $ \\ 
 $ (E4L6F(X) \leftrightarrow E4L6P(X)) \land $ \\ 
 $ (DIAMOND264F(X) \leftrightarrow DIAMOND188P(X)) \land $ \\ 
 $ (PinvG8F \leftrightarrow PinvG8P) \land $ \\ 
 $ (BOX591F(X) \leftrightarrow BOX448P(X)) \land $ \\ 
 $ (BOX679F(X) \leftrightarrow BOX697P(X)) \land $ \\ 
 $ (E1G11F(X) \leftrightarrow E1G11P(X)) \land $ \\ 
 $ (PinvG7F \leftrightarrow PinvG7F) \land $ \\ 
 $ (PinvG2F \leftrightarrow PinvG2P) \land $ \\ 
 $ (DIAMOND245F(X) \leftrightarrow DIAMOND168P(X)) \land $ \\ 
 $ (BOX631F(X) \leftrightarrow BOX520P(X)) \land $ \\ 
 $ (DIAMOND260F(X) \leftrightarrow DIAMOND184P(X)) \land $ \\ 
 $ (BOX48F(X) \leftrightarrow BOX484P(X)) \land $ \\ 
 $ (BOX94F(X) \leftrightarrow BOX724P(X)) \land $ \\ 
 $ (DIAMOND289F(X) \leftrightarrow DIAMOND352P(X)) \land $ \\ 
 $ (DIAMOND321F(X) \leftrightarrow DIAMOND389P(X)) \land $ \\ 
 $ (DIAMOND73F(X) \leftrightarrow DIAMOND399P(X)) \land $ \\ 
 $ (BOX46F(X) \leftrightarrow BOX482P(X)) \land $ \\ 
 $ (BOX619F(X) \leftrightarrow BOX499P(X)) \land $ \\ 
 $ (BOX647F(X) \leftrightarrow BOX536P(X)) \land $ \\ 
 $ (BOX84F(X) \leftrightarrow BOX714P(X)) \land $ \\ 
 $ (E1G18F(X) \leftrightarrow E1G18P(X)) \land $ \\ 
 $ (BOX30F(X) \leftrightarrow BOX453P(X)) \land $ \\ 
 $ (BOX82F(X) \leftrightarrow BOX712P(X)) \land $ \\ 
 $ (E1G2InvF(X) \leftrightarrow E1G2InvP(X)) \land $ \\ 
 $ (PG21F \leftrightarrow PG21F) \land $ \\ 
 $ (BOX22F(X) \leftrightarrow BOX689P(X)) \land $ \\ 
 $ (DIAMOND330F(X) \leftrightarrow DIAMOND400P(X)) \land $ \\ 
 $ (BOX69F(X) \leftrightarrow BOX514P(X)) \land $ \\ 
 $ (BOX667F(X) \leftrightarrow BOX556P(X)) \land $ \\ 
 $ (E5G14F(X) \leftrightarrow E5G14P(X)) \land $ \\ 
 $ (BOX632F(X) \leftrightarrow BOX521P(X)) \land $ \\ 
 $ (DIAMOND247F(X) \leftrightarrow DIAMOND170P(X)) \land $ \\ 
 $ (BOX65F(X) \leftrightarrow BOX509P(X)) \land $ \\ 
 $ (BOX8F(X) \leftrightarrow BOX418P(X)) \land $ \\ 
 $ (BOX26F(X) \leftrightarrow BOX446P(X)) \land $ \\ 
 $ (C12F(X) \leftrightarrow C12P(X)) \land $ \\ 
 $ (DIAMOND226F(X) \leftrightarrow DIAMOND147P(X)) \land $ \\ 
 $ (BOX221F(X) \leftrightarrow BOX142P(X)) \land $ \\ 
 $ (BOX305F(X) \leftrightarrow BOX371P(X)) \land $ \\ 
 $ (DIAMOND301F(X) \leftrightarrow DIAMOND367P(X)) \land $ \\ 
 $ (C7F(X) \leftrightarrow C7P(X)) \land $ \\ 
 $ (DIAMOND235F(X) \leftrightarrow DIAMOND158P(X)) \land $ \\ 
 $ (C2F(X) \leftrightarrow C2P(X)) \land $ \\ 
 $ (BOX89F(X) \leftrightarrow BOX719P(X)) \land $ \\ 
 $ (E1G7F(X) \leftrightarrow E1G7P(X)) \land $ \\ 
 $ (BOX64F(X) \leftrightarrow BOX508P(X)) \land $ \\ 
 $ (E1G13F(X) \leftrightarrow E1G13P(X)) \land $ \\ 
 $ (PinvG11F \leftrightarrow PinvG11P) \land $ \\ 
 $ (DIAMOND198F(X) \leftrightarrow DIAMOND118P(X)) \land $ \\ 
 $ (BOX596F(X) \leftrightarrow BOX457P(X)) \land $ \\ 
 $ (BOX53F(X) \leftrightarrow BOX491P(X)) \land $ \\ 
 $ (BOX592F(X) \leftrightarrow BOX450P(X)) \land $ \\ 
 $ (E1G4F(X) \leftrightarrow E1G4P(X)) \land $ \\ 
 $ (PG21F \leftrightarrow PG21P) \land $ \\ 
 $ (PG2F \leftrightarrow PG2P) \land $ \\ 
 $ (BOX680F(X) \leftrightarrow BOX698P(X)) \land $ \\ 
 $ (BOX633F(X) \leftrightarrow BOX522P(X)) \land $ \\ 
 $ (BOX590F(X) \leftrightarrow BOX445P(X)) \land $ \\ 
 $ (PG17F \leftrightarrow PG17P) \land $ \\ 
 $ (BOX637F(X) \leftrightarrow BOX526P(X)) \land $ \\ 
 $ (BOX114F(X) \leftrightarrow BOX744P(X)) \land $ \\ 
 $ (PinvL6F \leftrightarrow PinvL6F) \land $ \\ 
 $ (BOX293F(X) \leftrightarrow BOX357P(X)) \land $ \\ 
 $ (BOX36F(X) \leftrightarrow BOX460P(X)) \land $ \\ 
 $ (BOX616F(X) \leftrightarrow BOX495P(X)) \land $ \\ 
 $ (PinvG11F \leftrightarrow PinvG11F) \land $ \\ 
 $ (BOX110F(X) \leftrightarrow BOX740P(X)) \land $ \\ 
 $ (BOX666F(X) \leftrightarrow BOX555P(X)) \land $ \\ 
 $ (DIAMOND307F(X) \leftrightarrow DIAMOND373P(X)) \land $ \\ 
 $ (PG7F \leftrightarrow PG7F) \land $ \\ 
 $ (BOX327F(X) \leftrightarrow BOX396P(X)) \land $ \\ 
 $ (E3G9F(X) \leftrightarrow E3G9P(X)) \land $ \\ 
 $ (DIAMOND238F(X) \leftrightarrow DIAMOND161P(X)) \land $ \\ 
 $ (DIAMOND31F(X) \leftrightarrow DIAMOND366P(X)) \land $ \\ 
 $ (E1G7InvF(X) \leftrightarrow E1G7InvP(X)) \land $ \\ 
 $ (PG2F \leftrightarrow PG2F) \land $ \\ 
 $ (BOX651F(X) \leftrightarrow BOX540P(X)) \land $ \\ 
 $ (DIAMOND243F(X) \leftrightarrow DIAMOND166P(X)) \land $ \\ 
 $ (BOX588F(X) \leftrightarrow BOX443P(X)) \land $ \\ 
 $ (DIAMOND216F(X) \leftrightarrow DIAMOND137P(X)) \land $ \\ 
 $ (BOX629F(X) \leftrightarrow BOX518P(X)) \land $ \\ 
 $ (DIAMOND270F(X) \leftrightarrow DIAMOND195P(X)) \land $ \\ 
 $ (PinvG18F \leftrightarrow PinvG18P) \land $ \\ 
 $ (BOX5F(X) \leftrightarrow BOX407P(X)) \land $ \\ 
 $ (DIAMOND246F(X) \leftrightarrow DIAMOND169P(X)) \land $ \\ 
 $ (DIAMOND21F(X) \leftrightarrow DIAMOND360P(X)) \land $ \\ 
 $ (E2G21F(X) \leftrightarrow E2G21P(X)) \land $ \\ 
 $ (BOX627F(X) \leftrightarrow BOX516P(X)) \land $ \\ 
 $ (BOX600F(X) \leftrightarrow BOX466P(X)) \land $ \\ 
 $ (DIAMOND287F(X) \leftrightarrow DIAMOND350P(X)) \land $ \\ 
 $ (BOX563F(X) \leftrightarrow BOX404P(X)) \land $ \\ 
 $ (BOX578F(X) \leftrightarrow BOX427P(X)) \land $ \\ 
 $ (PinvG13F \leftrightarrow PinvG13P) \land $ \\ 
 $ (BOX62F(X) \leftrightarrow BOX506P(X)) \land $ \\ 
 $ (BOX11F(X) \leftrightarrow BOX684P(X)) \land $ \\ 
 $ (PinvG5F \leftrightarrow PinvG5P) \land $ \\ 
 $ (BOX100F(X) \leftrightarrow BOX730P(X)) \land $ \\ 
 $ (PG9F \leftrightarrow PG9F) \land $ \\ 
 $ (BOX87F(X) \leftrightarrow BOX717P(X)) \land $ \\ 
 $ (BOX103F(X) \leftrightarrow BOX733P(X)) \land $ \\ 
 $ (DIAMOND199F(X) \leftrightarrow DIAMOND120P(X)) \land $ \\ 
 $ (PG28F \leftrightarrow PG28P) \land $ \\ 
 $ (PinvG16F \leftrightarrow PinvG16F) \land $ \\ 
 $ (DIAMOND63F(X) \leftrightarrow DIAMOND386P(X)) \land $ \\ 
 $ (C27F(X) \leftrightarrow C27P(X)) \land $ \\ 
 $ (BOX104F(X) \leftrightarrow BOX734P(X)) \land $ \\ 
 $ (DIAMOND250F(X) \leftrightarrow DIAMOND173P(X)) \land $ \\ 
 $ (BOX597F(X) \leftrightarrow BOX459P(X)) \land $ \\ 
 $ (BOX309F(X) \leftrightarrow BOX376P(X)) \land $ \\ 
 $ (PG16F \leftrightarrow PG16F) \land $ \\ 
 $ (BOX295F(X) \leftrightarrow BOX359P(X)) \land $ \\ 
 $ (BOX579F(X) \leftrightarrow BOX429P(X)) \land $ \\ 
 $ (E1G8InvF(X) \leftrightarrow E1G8InvP(X)) \land $ \\ 
 $ (BOX606F(X) \leftrightarrow BOX476P(X)) \land $ \\ 
 $ (BOX271F(X) \leftrightarrow BOX332P(X)) \land $ \\ 
 $ (BOX60F(X) \leftrightarrow BOX502P(X)) \land $ \\ 
 $ (BOX648F(X) \leftrightarrow BOX537P(X)) \land $ \\ 
 $ (E1G16InvF(X) \leftrightarrow E1G16InvP(X)) \land $ \\ 
 $ (BOX683F(X) \leftrightarrow BOX701P(X)) \land $ \\ 
 $ (BOX663F(X) \leftrightarrow BOX552P(X)) \land $ \\ 
 $ (BOX261F(X) \leftrightarrow BOX185P(X)) \land $ \\ 
 $ (E3G10F(X) \leftrightarrow E3G10P(X)) \land $ \\ 
 $ (DIAMOND266F(X) \leftrightarrow DIAMOND190P(X)) \land $ \\ 
 $ (PG8F \leftrightarrow PG8P) \land $ \\ 
 $ (E1G8F(X) \leftrightarrow E1G8P(X)) \land $ \\ 
 $ (BOX603F(X) \leftrightarrow BOX472P(X)) \land $ \\ 
 $ (BOX643F(X) \leftrightarrow BOX532P(X)) \land $ \\ 
 $ (BOX675F(X) \leftrightarrow BOX690P(X)) \land $ \\ 
 $ (BOX564F(X) \leftrightarrow BOX406P(X)) \land $ \\ 
 $ (BOX575F(X) \leftrightarrow BOX424P(X)) \land $ \\ 
 $ (BOX77F(X) \leftrightarrow BOX707P(X)) \land $ \\ 
 $ (PG17F \leftrightarrow PG17F) \land $ \\ 
 $ (DIAMOND217F(X) \leftrightarrow DIAMOND138P(X)) \land $ \\ 
 $ (DIAMOND249F(X) \leftrightarrow DIAMOND172P(X)) \land $ \\ 
 $ (BOX200F(X) \leftrightarrow BOX121P(X)) \land $ \\ 
 $ (BOX604F(X) \leftrightarrow BOX473P(X)) \land $ \\ 
 $ (E1G0InvF(X) \leftrightarrow E1G0InvP(X)) \land $ \\ 
 $ (PinvG18F \leftrightarrow PinvG18F) \land $ \\ 
 $ (BOX635F(X) \leftrightarrow BOX524P(X)) \land $ \\ 
 $ (E1G20F(X) \leftrightarrow E1G20P(X)) \land $ \\ 
 $ (DIAMOND201F(X) \leftrightarrow DIAMOND122P(X)) \land $ \\ 
 $ (PinvG8F \leftrightarrow PinvG8F) \land $ \\ 
 $ (PinvG21F \leftrightarrow PinvG21F) \land $ \\ 
 $ (BOX607F(X) \leftrightarrow BOX477P(X)) \land $ \\ 
 $ (PinvG14F \leftrightarrow PinvG14P) \land $ \\ 
 $ (PG1F \leftrightarrow PG1P) \land $ \\ 
 $ (DIAMOND209F(X) \leftrightarrow DIAMOND130P(X)) \land $ \\ 
 $ (BOX617F(X) \leftrightarrow BOX496P(X)) \land $ \\ 
 $ (C11F(X) \leftrightarrow C11P(X)) \land $ \\ 
 $ (BOX45F(X) \leftrightarrow BOX481P(X))) \land $ \\ 
 $ (PG14 \rightarrow E1G14Inv(dG14Inv)) \land $ \\ 
 $ (PG21 \rightarrow E1G21Inv(dG21Inv)) \land $ \\ 
 $ (PinvG16 \rightarrow E1G16(dG16)) \land $ \\ 
 $ (PG20 \rightarrow E1G20Inv(dG20Inv)) \land $ \\ 
 $ (PinvG1 \rightarrow E1G1(dG1)) \land $ \\ 
 $ (PinvG2 \rightarrow E1G2(dG2)) \land $ \\ 
 $ (PG7 \rightarrow E1G7Inv(dG7Inv)) \land $ \\ 
 $ (PL6 \rightarrow E1L6Inv(dL6Inv)) \land $ \\ 
 $ (PinvG14 \rightarrow E1G14(dG14)) \land $ \\ 
 $ (PinvG11 \rightarrow E1G11(dG11)) \land $ \\ 
 $ (PinvG5 \rightarrow E1G5(dG5)) \land $ \\ 
 $ (PinvG20 \rightarrow E1G20(dG20)) \land $ \\ 
 $ (PinvG7 \rightarrow E1G7(dG7)) \land $ \\ 
 $ (PinvG8 \rightarrow E1G8(dG8)) \land $ \\ 
 $ (PG18 \rightarrow E1G18Inv(dG18Inv)) \land $ \\ 
 $ (PG13 \rightarrow E1G13Inv(dG13Inv)) \land $ \\ 
 $ (PinvG27 \rightarrow E1G27(dG27)) \land $ \\ 
 $ (PinvG21 \rightarrow E1G21(dG21)) \land $ \\ 
 $ (PG10 \rightarrow E1G10Inv(dG10Inv)) \land $ \\ 
 $ (PinvG10 \rightarrow E1G10(dG10)) \land $ \\ 
 $ (PG11 \rightarrow E1G11Inv(dG11Inv)) \land $ \\ 
 $ (PinvG18 \rightarrow E1G18(dG18)) \land $ \\ 
 $ (PinvG13 \rightarrow E1G13(dG13)) \land $ \\ 
 $ (PinvG9 \rightarrow E1G9(dG9)) \land $ \\ 
 $ (PG28 \rightarrow E1G28Inv(dG28Inv)) \land $ \\ 
 $ (PG5 \rightarrow E1G5Inv(dG5Inv)) \land $ \\ 
 $ (PinvG0 \rightarrow E1G0(dG0)) \land $ \\ 
 $ (PG0 \rightarrow E1G0Inv(dG0Inv)) \land $ \\ 
 $ (PG9 \rightarrow E1G9Inv(dG9Inv)) \land $ \\ 
 $ (PinvG4 \rightarrow E1G4(dG4)) \land $ \\ 
 $ (PG27 \rightarrow E1G27Inv(dG27Inv)) \land $ \\ 
 $ (PinvG6 \rightarrow E1G6(dG6)) \land $ \\ 
 $ (PinvG28 \rightarrow E1G28(dG28)) \land $ \\ 
 $ (PG4 \rightarrow E1G4Inv(dG4Inv)) \land $ \\ 
 $ (PinvG17 \rightarrow E1G17(dG17)) \land $ \\ 
 $ (PG6 \rightarrow E1G6Inv(dG6Inv)) \land $ \\ 
 $ (PG16 \rightarrow E1G16Inv(dG16Inv)) \land $ \\ 
 $ (PG1 \rightarrow E1G1Inv(dG1Inv)) \land $ \\ 
 $ (PG17 \rightarrow E1G17Inv(dG17Inv)) \land $ \\ 
 $ (PG2 \rightarrow E1G2Inv(dG2Inv)) \land $ \\ 
 $ (PG8 \rightarrow E1G8Inv(dG8Inv)) \land $ \\ 
 $ (PinvL6 \rightarrow E1L6(dL6)))$ 
\end{document}