\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. ((E2G5F(X) \rightarrow E1G5F(X)) \land $ \\ 
 $ (E3G28F(X) \rightarrow BOX76F(X)) \land $ \\ 
 $ (E1G11F(X) \rightarrow BOX71F(X)) \land $ \\ 
 $ (E1L29F(X) \rightarrow BOX114F(X)) \land $ \\ 
 $ (E1G9InvF(X) \rightarrow BOX128F(X)) \land $ \\ 
 $ (E3G25F(X) \rightarrow E1G25F(X)) \land $ \\ 
 $ (E1G18F(X) \rightarrow BOX3F(X)) \land $ \\ 
 $ (E2G29F(X) \rightarrow BOX40F(X)) \land $ \\ 
 $ (E1G27InvF(X) \rightarrow BOX94F(X)) \land $ \\ 
 $ (E3G14F(X) \rightarrow BOX38F(X)) \land $ \\ 
 $ (E2G29F(X) \rightarrow E1G29F(X)) \land $ \\ 
 $ (E3G11F(X) \rightarrow BOX11F(X)) \land $ \\ 
 $ (E4G25F(X) \rightarrow E3G25F(X)) \land $ \\ 
 $ ((BOX58F(X) \land $ \\ 
 $ DIAMOND59F(X)) \rightarrow BOX60F(X)) \land $ \\ 
 $ (E5L1F(X) \rightarrow E4L1F(X)) \land $ \\ 
 $ (E4G14F(X) \rightarrow BOX17F(X)) \land $ \\ 
 $ (E1G3InvF(X) \rightarrow BOX102F(X)) \land $ \\ 
 $ (BOX5F(X) \rightarrow (DIAMOND6F(X) \land $ \\ 
 $  \lnot C13F(X) \land $ \\ 
 $ C7F(X))) \land $ \\ 
 $ (E1G8F(X) \rightarrow BOX118F(X)) \land $ \\ 
 $ (E1G19F(X) \rightarrow BOX13F(X)) \land $ \\ 
 $ (E2G18F(X) \rightarrow E1G18F(X)) \land $ \\ 
 $ (E4G4F(X) \rightarrow BOX75F(X)) \land $ \\ 
 $ (E1G29F(X) \rightarrow BOX42F(X)) \land $ \\ 
 $ (E2G9F(X) \rightarrow BOX62F(X)) \land $ \\ 
 $ (E1G18F(X) \rightarrow BOX90F(X)) \land $ \\ 
 $ (E1G19F(X) \rightarrow BOX117F(X)) \land $ \\ 
 $ (E1G4F(X) \rightarrow BOX85F(X)) \land $ \\ 
 $ (E4G4F(X) \rightarrow E3G4F(X)) \land $ \\ 
 $ (E2G3F(X) \rightarrow E1G3F(X)) \land $ \\ 
 $ (E5G17F(X) \rightarrow E4G17F(X)) \land $ \\ 
 $ (E1G5InvF(X) \rightarrow BOX92F(X)) \land $ \\ 
 $ (E1G20F(X) \rightarrow BOX16F(X)) \land $ \\ 
 $ (E3G7F(X) \rightarrow E1G7F(X)) \land $ \\ 
 $ (E1G23F(X) \rightarrow BOX111F(X)) \land $ \\ 
 $ (E4G17F(X) \rightarrow BOX34F(X)) \land $ \\ 
 $ (BOX0F(X) \rightarrow BOX1F(X)) \land $ \\ 
 $ (DIAMOND14F(X) \rightarrow DIAMOND15F(X)) \land $ \\ 
 $ (E1G27F(X) \rightarrow BOX4F(X)) \land $ \\ 
 $ (E1G25F(X) \rightarrow BOX7F(X)) \land $ \\ 
 $ (E1G29InvF(X) \rightarrow BOX88F(X)) \land $ \\ 
 $ (E5G2F(X) \rightarrow E3G2F(X)) \land $ \\ 
 $ (BOX18F(X) \rightarrow BOX19F(X)) \land $ \\ 
 $ (E1G17F(X) \rightarrow BOX103F(X)) \land $ \\ 
 $ (E1G3F(X) \rightarrow BOX113F(X)) \land $ \\ 
 $ (DIAMOND65F(X) \rightarrow DIAMOND66F(X)) \land $ \\ 
 $ (E1G5F(X) \rightarrow BOX112F(X)) \land $ \\ 
 $ (E1G16F(X) \rightarrow BOX57F(X)) \land $ \\ 
 $ (E3G4F(X) \rightarrow E1G4F(X)) \land $ \\ 
 $ (E2G3F(X) \rightarrow BOX52F(X)) \land $ \\ 
 $ ((DIAMOND44F(X) \land $ \\ 
 $ BOX45F(X)) \rightarrow BOX46F(X)) \land $ \\ 
 $ (E1G8F(X) \rightarrow BOX32F(X)) \land $ \\ 
 $ (E2G20F(X) \rightarrow E1G20F(X)) \land $ \\ 
 $ (E1G14F(X) \rightarrow BOX56F(X)) \land $ \\ 
 $ (E1G7InvF(X) \rightarrow BOX126F(X)) \land $ \\ 
 $ (E1G14InvF(X) \rightarrow BOX100F(X)) \land $ \\ 
 $ (E4G14F(X) \rightarrow E3G14F(X)) \land $ \\ 
 $ (DIAMOND35F(X) \rightarrow BOX36F(X)) \land $ \\ 
 $ (E1L29InvF(X) \rightarrow BOX108F(X)) \land $ \\ 
 $ (E3G11F(X) \rightarrow E1G11F(X)) \land $ \\ 
 $ (E1L26F(X) \rightarrow BOX81F(X)) \land $ \\ 
 $ (E1G29F(X) \rightarrow BOX104F(X)) \land $ \\ 
 $ (E1G23F(X) \rightarrow BOX64F(X)) \land $ \\ 
 $ (E3G14F(X) \rightarrow E1G14F(X)) \land $ \\ 
 $ (E4G9F(X) \rightarrow BOX28F(X)) \land $ \\ 
 $ (E1G12InvF(X) \rightarrow BOX127F(X)) \land $ \\ 
 $ (E1G7F(X) \rightarrow BOX48F(X)) \land $ \\ 
 $ (E1G20InvF(X) \rightarrow BOX96F(X)) \land $ \\ 
 $ (E5G2F(X) \rightarrow BOX29F(X)) \land $ \\ 
 $ (E3G2F(X) \rightarrow E1G2F(X)) \land $ \\ 
 $ (E1G16F(X) \rightarrow BOX110F(X)) \land $ \\ 
 $ (E5G17F(X) \rightarrow BOX67F(X)) \land $ \\ 
 $ (E4G8F(X) \rightarrow E1G8F(X)) \land $ \\ 
 $ (E2G20F(X) \rightarrow BOX43F(X)) \land $ \\ 
 $ (E1G4InvF(X) \rightarrow BOX95F(X)) \land $ \\ 
 $ (E4G17F(X) \rightarrow E1G17F(X)) \land $ \\ 
 $ (E3G18F(X) \rightarrow BOX24F(X)) \land $ \\ 
 $ (E4L15F(X) \rightarrow E1L15F(X)) \land $ \\ 
 $ (E1G16InvF(X) \rightarrow BOX124F(X)) \land $ \\ 
 $ (BOX72F(X) \rightarrow DIAMOND73F(X)) \land $ \\ 
 $ (DIAMOND53F(X) \rightarrow (DIAMOND54F(X) \land $ \\ 
 $ BOX55F(X) \land $ \\ 
 $ E1G3F(X))) \land $ \\ 
 $ (E1G12F(X) \rightarrow BOX123F(X)) \land $ \\ 
 $ (DIAMOND21F(X) \rightarrow BOX22F(X)) \land $ \\ 
 $ (E2G18F(X) \rightarrow BOX39F(X)) \land $ \\ 
 $ (E1G17F(X) \rightarrow BOX10F(X)) \land $ \\ 
 $ (E1L26InvF(X) \rightarrow BOX122F(X)) \land $ \\ 
 $ (E1G8InvF(X) \rightarrow BOX86F(X)) \land $ \\ 
 $ (E1G14F(X) \rightarrow BOX105F(X)) \land $ \\ 
 $ (E3G25F(X) \rightarrow BOX74F(X)) \land $ \\ 
 $ (DIAMOND8F(X) \rightarrow DIAMOND9F(X)) \land $ \\ 
 $ (E3G27F(X) \rightarrow BOX20F(X)) \land $ \\ 
 $ (E1G9F(X) \rightarrow BOX93F(X)) \land $ \\ 
 $ (E1G5F(X) \rightarrow BOX30F(X)) \land $ \\ 
 $ (E3G4F(X) \rightarrow BOX26F(X)) \land $ \\ 
 $ (E1G20F(X) \rightarrow BOX87F(X)) \land $ \\ 
 $ ((BOX49F(X) \land $ \\ 
 $ BOX50F(X)) \rightarrow BOX51F(X)) \land $ \\ 
 $ (E1G7F(X) \rightarrow BOX97F(X)) \land $ \\ 
 $ (E1G25InvF(X) \rightarrow BOX120F(X)) \land $ \\ 
 $ (E2G5F(X) \rightarrow BOX27F(X)) \land $ \\ 
 $ (E1G17InvF(X) \rightarrow BOX106F(X)) \land $ \\ 
 $ (E1L15InvF(X) \rightarrow BOX119F(X)) \land $ \\ 
 $ (E1G19InvF(X) \rightarrow BOX82F(X)) \land $ \\ 
 $ (E5G4F(X) \rightarrow E4G4F(X)) \land $ \\ 
 $ (E4G8F(X) \rightarrow BOX80F(X)) \land $ \\ 
 $ (E3G18F(X) \rightarrow E2G18F(X)) \land $ \\ 
 $ (E1G28InvF(X) \rightarrow BOX116F(X)) \land $ \\ 
 $ (E1L1InvF(X) \rightarrow BOX109F(X)) \land $ \\ 
 $ (E3G2F(X) \rightarrow BOX12F(X)) \land $ \\ 
 $ ((BOX68F(X) \land $ \\ 
 $ BOX69F(X)) \rightarrow BOX70F(X)) \land $ \\ 
 $ (E5G29F(X) \rightarrow E2G29F(X)) \land $ \\ 
 $ (E1L15F(X) \rightarrow BOX98F(X)) \land $ \\ 
 $ (E1G25F(X) \rightarrow BOX121F(X)) \land $ \\ 
 $ (E1G9F(X) \rightarrow BOX47F(X)) \land $ \\ 
 $ (E3G7F(X) \rightarrow BOX61F(X)) \land $ \\ 
 $ (E4G12F(X) \rightarrow E1G12F(X)) \land $ \\ 
 $ (E2L29F(X) \rightarrow E1L29F(X)) \land $ \\ 
 $ (E1G2InvF(X) \rightarrow BOX89F(X)) \land $ \\ 
 $ (E4G9F(X) \rightarrow E2G9F(X)) \land $ \\ 
 $ (E1G11F(X) \rightarrow BOX99F(X)) \land $ \\ 
 $ (E5G29F(X) \rightarrow BOX33F(X)) \land $ \\ 
 $ (E3G28F(X) \rightarrow E1G28F(X)) \land $ \\ 
 $ (E1G28F(X) \rightarrow BOX91F(X)) \land $ \\ 
 $ (BOX78F(X) \rightarrow DIAMOND79F(X)) \land $ \\ 
 $ (E1G3F(X) \rightarrow BOX23F(X)) \land $ \\ 
 $ (E1G23InvF(X) \rightarrow BOX125F(X)) \land $ \\ 
 $ (E1G27F(X) \rightarrow BOX83F(X)) \land $ \\ 
 $ (E1G28F(X) \rightarrow BOX25F(X)) \land $ \\ 
 $ (E2G9F(X) \rightarrow E1G9F(X)) \land $ \\ 
 $ (E5G4F(X) \rightarrow BOX63F(X)) \land $ \\ 
 $ (E1G4F(X) \rightarrow BOX2F(X)) \land $ \\ 
 $ (E1G2F(X) \rightarrow BOX31F(X)) \land $ \\ 
 $ (E1G12F(X) \rightarrow BOX37F(X)) \land $ \\ 
 $ (E1G11InvF(X) \rightarrow BOX107F(X)) \land $ \\ 
 $ (E3G27F(X) \rightarrow E1G27F(X)) \land $ \\ 
 $ (E1L1F(X) \rightarrow BOX101F(X)) \land $ \\ 
 $ (E1G18InvF(X) \rightarrow BOX115F(X)) \land $ \\ 
 $ (E4G25F(X) \rightarrow BOX77F(X)) \land $ \\ 
 $ (E1G2F(X) \rightarrow BOX84F(X)) \land $ \\ 
 $ (E4L1F(X) \rightarrow E1L1F(X)) \land $ \\ 
 $ (E4G12F(X) \rightarrow BOX41F(X)) \land $ \\ 
 $  \Rbox ((DIAMOND195F(X) \leftrightarrow  \Rdiamond (C7F(X) \land $ \\ 
 $ BOX196F(X) \land $ \\ 
 $ C8F(X))) \land $ \\ 
 $ (DIAMOND297P(X) \leftrightarrow  \Rdiamond DIAMOND298P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND236F(X) \leftrightarrow (DIAMOND236F(X) \lor  \Rnext  \lnot C13F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND164P(X) \leftrightarrow (DIAMOND164P(X) \lor  \Rnext DIAMOND165P(X))) \land $ \\ 
 $ (DIAMOND298P(X) \leftrightarrow  \Rdiamond (C1P(X) \land $ \\ 
 $ E3G18P(X))) \land $ \\ 
 $ ( \Rnext DIAMOND15F(X) \leftrightarrow (DIAMOND15F(X) \lor  \Rnext BOX237F(X))) \land $ \\ 
 $ (DIAMOND201F(X) \leftrightarrow  \Rdiamond (C19F(X) \land $ \\ 
 $ E3G25F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND138P(X) \leftrightarrow (DIAMOND138P(X) \lor  \Rnext BOX139P(X))) \land $ \\ 
 $ ( \Rnext DIAMOND186F(X) \leftrightarrow (DIAMOND186F(X) \lor  \Rnext DIAMOND236F(X))) \land $ \\ 
 $ (DIAMOND279P(X) \leftrightarrow  \Rdiamond DIAMOND280P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND267F(X) \leftrightarrow (DIAMOND267F(X) \lor  \Rnext DIAMOND268F(X))) \land $ \\ 
 $ (DIAMOND293P(X) \leftrightarrow  \Rdiamond BOX294P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND160P(X) \leftrightarrow (DIAMOND160P(X) \lor  \Rnext (E5G29P(X) \land $ \\ 
 $ DIAMOND161P(X)))) \land $ \\ 
 $ ( \Rnext DIAMOND167P(X) \leftrightarrow (DIAMOND167P(X) \lor  \Rnext DIAMOND168P(X))) \land $ \\ 
 $ ( \Rnext DIAMOND153P(X) \leftrightarrow (DIAMOND153P(X) \lor  \Rnext (C19P(X) \land $ \\ 
 $ E3G25P(X)))) \land $ \\ 
 $ ( \Rnext DIAMOND66F(X) \leftrightarrow (DIAMOND66F(X) \lor  \Rnext (C25F(X) \land $ \\ 
 $ BOX260F(X)))) \land $ \\ 
 $ ( \Rnext DIAMOND142P(X) \leftrightarrow (DIAMOND142P(X) \lor  \Rnext BOX143P(X))) \land $ \\ 
 $ ( \Rnext DIAMOND245F(X) \leftrightarrow (DIAMOND245F(X) \lor  \Rnext E1G16F(X))) \land $ \\ 
 $ (DIAMOND182F(X) \leftrightarrow  \Rdiamond (DIAMOND183F(X) \land $ \\ 
 $ E4G9F(X) \land $ \\ 
 $ E3G2F(X) \land $ \\ 
 $ E1G7F(X))) \land $ \\ 
 $ (DIAMOND14F(X) \leftrightarrow  \Rdiamond (C11F(X) \land $ \\ 
 $ DIAMOND187F(X) \land $ \\ 
 $ DIAMOND188F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND229F(X) \leftrightarrow (DIAMOND229F(X) \lor  \Rnext C15F(X))) \land $ \\ 
 $ (DIAMOND306P(X) \leftrightarrow  \Rdiamond E2G3P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND242F(X) \leftrightarrow (DIAMOND242F(X) \lor  \Rnext DIAMOND243F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND162P(X) \leftrightarrow (DIAMOND162P(X) \lor  \Rnext DIAMOND163P(X))) \land $ \\ 
 $ (DIAMOND202F(X) \leftrightarrow  \Rdiamond (C23F(X) \land $ \\ 
 $ C24F(X))) \land $ \\ 
 $ (DIAMOND44F(X) \leftrightarrow  \Rdiamond E5G2F(X)) \land $ \\ 
 $ ( \Rnext DIAMOND169P(X) \leftrightarrow (DIAMOND169P(X) \lor  \Rnext DIAMOND170P(X))) \land $ \\ 
 $ (DIAMOND271P(X) \leftrightarrow  \Rdiamond C14P(X)) \land $ \\ 
 $ (DIAMOND73F(X) \leftrightarrow  \Rdiamond DIAMOND219F(X)) \land $ \\ 
 $ ( \Rnext DIAMOND197F(X) \leftrightarrow (DIAMOND197F(X) \lor  \Rnext BOX246F(X))) \land $ \\ 
 $ (DIAMOND304P(X) \leftrightarrow  \Rdiamond DIAMOND305P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND149P(X) \leftrightarrow (DIAMOND149P(X) \lor  \Rnext BOX150P(X))) \land $ \\ 
 $ ( \Rnext DIAMOND228F(X) \leftrightarrow (DIAMOND228F(X) \lor  \Rnext C14F(X))) \land $ \\ 
 $ (DIAMOND273P(X) \leftrightarrow  \Rdiamond C6P(X)) \land $ \\ 
 $ (DIAMOND163P(X) \leftrightarrow  \Rdiamond (E2L29P(X) \land $ \\ 
 $ BOX307P(X))) \land $ \\ 
 $ ( \Rnext DIAMOND266F(X) \leftrightarrow (DIAMOND266F(X) \lor  \Rnext DIAMOND267F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND247F(X) \leftrightarrow (DIAMOND247F(X) \lor  \Rnext BOX248F(X))) \land $ \\ 
 $ (DIAMOND134P(X) \leftrightarrow  \Rdiamond DIAMOND281P(X)) \land $ \\ 
 $ (DIAMOND200F(X) \leftrightarrow  \Rdiamond E4L15F(X)) \land $ \\ 
 $ ( \Rnext DIAMOND235F(X) \leftrightarrow (DIAMOND235F(X) \lor  \Rnext  \lnot C18F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND239F(X) \leftrightarrow (DIAMOND239F(X) \lor  \Rnext BOX241F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND177P(X) \leftrightarrow (DIAMOND177P(X) \lor  \Rnext BOX178P(X))) \land $ \\ 
 $ (DIAMOND9F(X) \leftrightarrow  \Rdiamond (BOX184F(X) \land $ \\ 
 $ DIAMOND185F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND216F(X) \leftrightarrow (DIAMOND216F(X) \lor  \Rnext E3G27F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND238F(X) \leftrightarrow (DIAMOND238F(X) \lor  \Rnext (E3G4F(X) \land $ \\ 
 $ DIAMOND239F(X) \land $ \\ 
 $ BOX240F(X)))) \land $ \\ 
 $ ( \Rnext DIAMOND155P(X) \leftrightarrow (DIAMOND155P(X) \lor  \Rnext (E4G12P(X) \land $ \\ 
 $ E3G7P(X)))) \land $ \\ 
 $ ( \Rnext DIAMOND253F(X) \leftrightarrow (DIAMOND253F(X) \lor  \Rnext BOX254F(X))) \land $ \\ 
 $ (DIAMOND284P(X) \leftrightarrow  \Rdiamond (E3G4P(X) \land $ \\ 
 $ DIAMOND285P(X) \land $ \\ 
 $ BOX286P(X))) \land $ \\ 
 $ (DIAMOND224F(X) \leftrightarrow  \Rdiamond E1G19F(X)) \land $ \\ 
 $ ( \Rnext DIAMOND6F(X) \leftrightarrow (DIAMOND6F(X) \lor  \Rnext BOX231F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND230F(X) \leftrightarrow (DIAMOND230F(X) \lor  \Rnext C6F(X))) \land $ \\ 
 $ (DIAMOND295P(X) \leftrightarrow  \Rdiamond DIAMOND151P(X)) \land $ \\ 
 $ (DIAMOND204F(X) \leftrightarrow  \Rdiamond DIAMOND205F(X)) \land $ \\ 
 $ (DIAMOND301P(X) \leftrightarrow  \Rdiamond C13P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND165P(X) \leftrightarrow (DIAMOND165P(X) \lor  \Rnext DIAMOND166P(X))) \land $ \\ 
 $ ( \Rnext DIAMOND171P(X) \leftrightarrow (DIAMOND171P(X) \lor  \Rnext C11P(X))) \land $ \\ 
 $ (DIAMOND276P(X) \leftrightarrow  \Rdiamond (E4G14P(X) \land $ \\ 
 $ BOX277P(X))) \land $ \\ 
 $ (DIAMOND288P(X) \leftrightarrow  \Rdiamond DIAMOND289P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND205F(X) \leftrightarrow (DIAMOND205F(X) \lor  \Rnext C12F(X))) \land $ \\ 
 $ (DIAMOND194F(X) \leftrightarrow  \Rdiamond DIAMOND195F(X)) \land $ \\ 
 $ ( \Rnext DIAMOND140P(X) \leftrightarrow (DIAMOND140P(X) \lor  \Rnext BOX141P(X))) \land $ \\ 
 $ (DIAMOND79F(X) \leftrightarrow  \Rdiamond BOX225F(X)) \land $ \\ 
 $ (DIAMOND166P(X) \leftrightarrow  \Rdiamond  \lnot E5L1P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND154P(X) \leftrightarrow (DIAMOND154P(X) \lor  \Rnext (C23P(X) \land $ \\ 
 $ C24P(X)))) \land $ \\ 
 $ ( \Rnext DIAMOND249F(X) \leftrightarrow (DIAMOND249F(X) \lor  \Rnext DIAMOND200F(X))) \land $ \\ 
 $ (DIAMOND189F(X) \leftrightarrow  \Rdiamond BOX190F(X)) \land $ \\ 
 $ (DIAMOND183F(X) \leftrightarrow  \Rdiamond C16F(X)) \land $ \\ 
 $ ( \Rnext DIAMOND251F(X) \leftrightarrow (DIAMOND251F(X) \lor  \Rnext DIAMOND252F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND168P(X) \leftrightarrow (DIAMOND168P(X) \lor  \Rnext DIAMOND169P(X))) \land $ \\ 
 $ (DIAMOND296P(X) \leftrightarrow  \Rdiamond DIAMOND153P(X)) \land $ \\ 
 $ (DIAMOND289P(X) \leftrightarrow  \Rdiamond C25P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND156P(X) \leftrightarrow (DIAMOND156P(X) \lor  \Rnext DIAMOND157P(X))) \land $ \\ 
 $ (DIAMOND282P(X) \leftrightarrow  \Rdiamond BOX283P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND234F(X) \leftrightarrow (DIAMOND234F(X) \lor  \Rnext DIAMOND235F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND263F(X) \leftrightarrow (DIAMOND263F(X) \lor  \Rnext (C16F(X) \land $ \\ 
 $ E2G5F(X) \land $ \\ 
 $ DIAMOND264F(X)))) \land $ \\ 
 $ (DIAMOND299P(X) \leftrightarrow  \Rdiamond BOX300P(X)) \land $ \\ 
 $ (DIAMOND308P(X) \leftrightarrow  \Rdiamond (C25P(X) \land $ \\ 
 $ BOX309P(X))) \land $ \\ 
 $ ( \Rnext DIAMOND179P(X) \leftrightarrow (DIAMOND179P(X) \lor  \Rnext E1G19P(X))) \land $ \\ 
 $ (DIAMOND203F(X) \leftrightarrow  \Rdiamond (E4G12F(X) \land $ \\ 
 $ E3G7F(X))) \land $ \\ 
 $ (DIAMOND291P(X) \leftrightarrow  \Rdiamond E1G16P(X)) \land $ \\ 
 $ (DIAMOND161P(X) \leftrightarrow  \Rdiamond C28P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND176P(X) \leftrightarrow (DIAMOND176P(X) \lor  \Rnext DIAMOND177P(X))) \land $ \\ 
 $ (DIAMOND317P(X) \leftrightarrow  \Rdiamond (DIAMOND273P(X) \land $ \\ 
 $  \lnot C25P(X))) \land $ \\ 
 $ (DIAMOND170P(X) \leftrightarrow  \Rdiamond E3G27P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND243F(X) \leftrightarrow (DIAMOND243F(X) \lor  \Rnext C25F(X))) \land $ \\ 
 $ (DIAMOND21F(X) \leftrightarrow  \Rdiamond BOX193F(X)) \land $ \\ 
 $ (DIAMOND217F(X) \leftrightarrow  \Rdiamond C11F(X)) \land $ \\ 
 $ (DIAMOND274P(X) \leftrightarrow  \Rdiamond BOX275P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND233F(X) \leftrightarrow (DIAMOND233F(X) \lor  \Rnext DIAMOND234F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND147P(X) \leftrightarrow (DIAMOND147P(X) \lor  \Rnext DIAMOND148P(X))) \land $ \\ 
 $ (DIAMOND280P(X) \leftrightarrow  \Rdiamond  \lnot C18P(X)) \land $ \\ 
 $ (DIAMOND191F(X) \leftrightarrow  \Rdiamond BOX192F(X)) \land $ \\ 
 $ (DIAMOND210F(X) \leftrightarrow  \Rdiamond DIAMOND211F(X)) \land $ \\ 
 $ (DIAMOND214F(X) \leftrightarrow  \Rdiamond DIAMOND215F(X)) \land $ \\ 
 $ ( \Rnext DIAMOND130P(X) \leftrightarrow (DIAMOND130P(X) \lor  \Rnext C16P(X))) \land $ \\ 
 $ ( \Rnext DIAMOND250F(X) \leftrightarrow (DIAMOND250F(X) \lor  \Rnext DIAMOND201F(X))) \land $ \\ 
 $ (DIAMOND285P(X) \leftrightarrow  \Rdiamond BOX287P(X)) \land $ \\ 
 $ (DIAMOND207F(X) \leftrightarrow  \Rdiamond (E5G29F(X) \land $ \\ 
 $ DIAMOND208F(X))) \land $ \\ 
 $ (DIAMOND137P(X) \leftrightarrow  \Rdiamond E5G4P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND136P(X) \leftrightarrow (DIAMOND136P(X) \lor  \Rnext (C18P(X) \land $ \\ 
 $ E3G25P(X)))) \land $ \\ 
 $ ( \Rnext DIAMOND208F(X) \leftrightarrow (DIAMOND208F(X) \lor  \Rnext C28F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND209F(X) \leftrightarrow (DIAMOND209F(X) \lor  \Rnext (E2L29F(X) \land $ \\ 
 $ BOX259F(X)))) \land $ \\ 
 $ (DIAMOND315P(X) \leftrightarrow  \Rdiamond DIAMOND316P(X)) \land $ \\ 
 $ (DIAMOND148P(X) \leftrightarrow  \Rdiamond BOX292P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND145P(X) \leftrightarrow (DIAMOND145P(X) \lor  \Rnext (C7P(X) \land $ \\ 
 $ BOX146P(X) \land $ \\ 
 $ C8P(X)))) \land $ \\ 
 $ (DIAMOND157P(X) \leftrightarrow  \Rdiamond C12P(X)) \land $ \\ 
 $ (DIAMOND305P(X) \leftrightarrow  \Rdiamond DIAMOND156P(X)) \land $ \\ 
 $ (DIAMOND272P(X) \leftrightarrow  \Rdiamond C15P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND255F(X) \leftrightarrow (DIAMOND255F(X) \lor  \Rnext C13F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND144P(X) \leftrightarrow (DIAMOND144P(X) \lor  \Rnext DIAMOND145P(X))) \land $ \\ 
 $ (DIAMOND290P(X) \leftrightarrow  \Rdiamond E2G29P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND135P(X) \leftrightarrow (DIAMOND135P(X) \lor  \Rnext (C11P(X) \land $ \\ 
 $ DIAMOND136P(X) \land $ \\ 
 $ DIAMOND137P(X)))) \land $ \\ 
 $ (DIAMOND312P(X) \leftrightarrow  \Rdiamond (C16P(X) \land $ \\ 
 $ E2G5P(X) \land $ \\ 
 $ DIAMOND313P(X))) \land $ \\ 
 $ (DIAMOND211F(X) \leftrightarrow  \Rdiamond DIAMOND212F(X)) \land $ \\ 
 $ ( \Rnext DIAMOND152P(X) \leftrightarrow (DIAMOND152P(X) \lor  \Rnext E5G2P(X))) \land $ \\ 
 $ ( \Rnext DIAMOND268F(X) \leftrightarrow (DIAMOND268F(X) \lor  \Rnext (DIAMOND230F(X) \land $ \\ 
 $  \lnot C25F(X)))) \land $ \\ 
 $ (DIAMOND35F(X) \leftrightarrow  \Rdiamond DIAMOND197F(X)) \land $ \\ 
 $ ( \Rnext DIAMOND244F(X) \leftrightarrow (DIAMOND244F(X) \lor  \Rnext E2G29F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND53F(X) \leftrightarrow (DIAMOND53F(X) \lor  \Rnext BOX256F(X))) \land $ \\ 
 $ (DIAMOND316P(X) \leftrightarrow  \Rdiamond DIAMOND317P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND173P(X) \leftrightarrow (DIAMOND173P(X) \lor  \Rnext DIAMOND174P(X))) \land $ \\ 
 $ (DIAMOND221F(X) \leftrightarrow  \Rdiamond DIAMOND222F(X)) \land $ \\ 
 $ ( \Rnext DIAMOND8F(X) \leftrightarrow (DIAMOND8F(X) \lor  \Rnext (E4G14F(X) \land $ \\ 
 $ BOX232F(X)))) \land $ \\ 
 $ ( \Rnext DIAMOND188F(X) \leftrightarrow (DIAMOND188F(X) \lor  \Rnext E5G4F(X))) \land $ \\ 
 $ (DIAMOND65F(X) \leftrightarrow  \Rdiamond DIAMOND209F(X)) \land $ \\ 
 $ (DIAMOND310P(X) \leftrightarrow  \Rdiamond DIAMOND167P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND258F(X) \leftrightarrow (DIAMOND258F(X) \lor  \Rnext E2G3F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND212F(X) \leftrightarrow (DIAMOND212F(X) \lor  \Rnext  \lnot E5L1F(X))) \land $ \\ 
 $ (DIAMOND281P(X) \leftrightarrow  \Rdiamond  \lnot C13P(X)) \land $ \\ 
 $ (DIAMOND198F(X) \leftrightarrow  \Rdiamond BOX199F(X)) \land $ \\ 
 $ ( \Rnext DIAMOND264F(X) \leftrightarrow (DIAMOND264F(X) \lor  \Rnext BOX265F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND151P(X) \leftrightarrow (DIAMOND151P(X) \lor  \Rnext E4L15P(X))) \land $ \\ 
 $ ( \Rnext DIAMOND252F(X) \leftrightarrow (DIAMOND252F(X) \lor  \Rnext (C1F(X) \land $ \\ 
 $ E3G18F(X)))) \land $ \\ 
 $ (DIAMOND218F(X) \leftrightarrow  \Rdiamond  \lnot E4G8F(X)) \land $ \\ 
 $ ( \Rnext DIAMOND261F(X) \leftrightarrow (DIAMOND261F(X) \lor  \Rnext DIAMOND213F(X))) \land $ \\ 
 $ (DIAMOND185F(X) \leftrightarrow  \Rdiamond DIAMOND186F(X)) \land $ \\ 
 $ (DIAMOND187F(X) \leftrightarrow  \Rdiamond (C18F(X) \land $ \\ 
 $ E3G25F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND54F(X) \leftrightarrow (DIAMOND54F(X) \lor  \Rnext DIAMOND257F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND180P(X) \leftrightarrow (DIAMOND180P(X) \lor  \Rnext BOX181P(X))) \land $ \\ 
 $ (DIAMOND313P(X) \leftrightarrow  \Rdiamond BOX314P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND133P(X) \leftrightarrow (DIAMOND133P(X) \lor  \Rnext DIAMOND134P(X))) \land $ \\ 
 $ ( \Rnext DIAMOND262F(X) \leftrightarrow (DIAMOND262F(X) \lor  \Rnext C23F(X))) \land $ \\ 
 $ (DIAMOND215F(X) \leftrightarrow  \Rdiamond DIAMOND216F(X)) \land $ \\ 
 $ (DIAMOND219F(X) \leftrightarrow  \Rdiamond BOX220F(X)) \land $ \\ 
 $ (DIAMOND302P(X) \leftrightarrow  \Rdiamond BOX303P(X)) \land $ \\ 
 $ (DIAMOND59F(X) \leftrightarrow  \Rdiamond BOX206F(X)) \land $ \\ 
 $ ( \Rnext DIAMOND129P(X) \leftrightarrow (DIAMOND129P(X) \lor  \Rnext (DIAMOND130P(X) \land $ \\ 
 $ E4G9P(X) \land $ \\ 
 $ E3G2P(X) \land $ \\ 
 $ E1G7P(X)))) \land $ \\ 
 $ (DIAMOND222F(X) \leftrightarrow  \Rdiamond BOX223F(X)) \land $ \\ 
 $ ( \Rnext DIAMOND172P(X) \leftrightarrow (DIAMOND172P(X) \lor  \Rnext  \lnot E4G8P(X))) \land $ \\ 
 $ (DIAMOND311P(X) \leftrightarrow  \Rdiamond C23P(X)) \land $ \\ 
 $ ( \Rnext DIAMOND131P(X) \leftrightarrow (DIAMOND131P(X) \lor  \Rnext (BOX132P(X) \land $ \\ 
 $ DIAMOND133P(X)))) \land $ \\ 
 $ ( \Rnext DIAMOND174P(X) \leftrightarrow (DIAMOND174P(X) \lor  \Rnext BOX175P(X))) \land $ \\ 
 $ ( \Rnext DIAMOND226F(X) \leftrightarrow (DIAMOND226F(X) \lor  \Rnext BOX227F(X))) \land $ \\ 
 $ ( \Rnext DIAMOND158P(X) \leftrightarrow (DIAMOND158P(X) \lor  \Rnext BOX159P(X))) \land $ \\ 
 $ (DIAMOND213F(X) \leftrightarrow  \Rdiamond DIAMOND214F(X)) \land $ \\ 
 $ ( \Rnext DIAMOND257F(X) \leftrightarrow (DIAMOND257F(X) \lor  \Rnext DIAMOND204F(X))) \land $ \\ 
 $ (DIAMOND278P(X) \leftrightarrow  \Rdiamond DIAMOND279P(X)) \land $ \\ 
 $ (DIAMOND269P(X) \leftrightarrow  \Rdiamond BOX270P(X)) \land $ \\ 
 $ (BOX34F(X) \leftrightarrow  \Rbox BOX524F(X)) \land $ \\ 
 $ (BOX199F(X) \leftrightarrow  \Rbox  \lnot C4F(X)) \land $ \\ 
 $ (BOX665P(X) \leftrightarrow  \Rbox BOX482P(X)) \land $ \\ 
 $ ( \Rnext BOX327P(X) \leftrightarrow (BOX327P(X) \land $ \\ 
 $  \Rnext (E4G4P(X) \land $ \\ 
 $ DIAMOND272P(X) \land $ \\ 
 $ DIAMOND273P(X)))) \land $ \\ 
 $ ( \Rnext BOX332P(X) \leftrightarrow (BOX332P(X) \land $ \\ 
 $  \Rnext BOX333P(X))) \land $ \\ 
 $ (BOX655P(X) \leftrightarrow  \Rbox BOX472P(X)) \land $ \\ 
 $ (BOX642P(X) \leftrightarrow  \Rbox BOX459P(X)) \land $ \\ 
 $ ( \Rnext BOX108F(X) \leftrightarrow (BOX108F(X) \land $ \\ 
 $  \Rnext BOX587F(X))) \land $ \\ 
 $ (BOX437P(X) \leftrightarrow  \Rbox E3G28P(X)) \land $ \\ 
 $ (BOX634P(X) \leftrightarrow  \Rbox BOX451P(X)) \land $ \\ 
 $ ( \Rnext BOX426P(X) \leftrightarrow (BOX426P(X) \land $ \\ 
 $  \Rnext (C24P(X) \land $ \\ 
 $ BOX427P(X) \land $ \\ 
 $ E4G17P(X) \land $ \\ 
 $ DIAMOND311P(X)))) \land $ \\ 
 $ ( \Rnext BOX516F(X) \leftrightarrow (BOX516F(X) \land $ \\ 
 $  \Rnext E1G28F(X))) \land $ \\ 
 $ ( \Rnext BOX292P(X) \leftrightarrow (BOX292P(X) \land $ \\ 
 $  \Rnext BOX379P(X))) \land $ \\ 
 $ (BOX32F(X) \leftrightarrow  \Rbox BOX522F(X)) \land $ \\ 
 $ (BOX616P(X) \leftrightarrow  \Rbox (BOX617P(X) \land $ \\ 
 $ DIAMOND297P(X))) \land $ \\ 
 $ (BOX553F(X) \leftrightarrow  \Rbox DIAMOND224F(X)) \land $ \\ 
 $ (BOX27F(X) \leftrightarrow  \Rbox BOX518F(X)) \land $ \\ 
 $ (BOX307P(X) \leftrightarrow  \Rbox DIAMOND164P(X)) \land $ \\ 
 $ ( \Rnext BOX431P(X) \leftrightarrow (BOX431P(X) \land $ \\ 
 $  \Rnext DIAMOND179P(X))) \land $ \\ 
 $ ( \Rnext BOX477P(X) \leftrightarrow (BOX477P(X) \land $ \\ 
 $  \Rnext PinvG18P)) \land $ \\ 
 $ (BOX650P(X) \leftrightarrow  \Rbox BOX467P(X)) \land $ \\ 
 $ (BOX260F(X) \leftrightarrow  \Rbox DIAMOND261F(X)) \land $ \\ 
 $ ( \Rnext BOX455P(X) \leftrightarrow (BOX455P(X) \land $ \\ 
 $  \Rnext PG9P)) \land $ \\ 
 $ ( \Rnext BOX321P(X) \leftrightarrow (BOX321P(X) \land $ \\ 
 $  \Rnext BOX322P(X))) \land $ \\ 
 $ ( \Rnext BOX196F(X) \leftrightarrow (BOX196F(X) \land $ \\ 
 $  \Rnext E1L26F(X))) \land $ \\ 
 $ ( \Rnext BOX88F(X) \leftrightarrow (BOX88F(X) \land $ \\ 
 $  \Rnext BOX567F(X))) \land $ \\ 
 $ (BOX572F(X) \leftrightarrow  \Rbox PG9F) \land $ \\ 
 $ ( \Rnext BOX488P(X) \leftrightarrow (BOX488P(X) \land $ \\ 
 $  \Rnext PinvG7P)) \land $ \\ 
 $ (BOX277P(X) \leftrightarrow  \Rbox BOX330P(X)) \land $ \\ 
 $ (BOX421P(X) \leftrightarrow  \Rbox E5G4P(X)) \land $ \\ 
 $ (BOX4F(X) \leftrightarrow  \Rbox BOX495F(X)) \land $ \\ 
 $ ( \Rnext BOX336P(X) \leftrightarrow (BOX336P(X) \land $ \\ 
 $  \Rnext BOX337P(X))) \land $ \\ 
 $ ( \Rnext BOX464P(X) \leftrightarrow (BOX464P(X) \land $ \\ 
 $  \Rnext PinvG3P)) \land $ \\ 
 $ ( \Rnext BOX463P(X) \leftrightarrow (BOX463P(X) \land $ \\ 
 $  \Rnext PL1P)) \land $ \\ 
 $ (BOX50F(X) \leftrightarrow  \Rbox BOX537F(X)) \land $ \\ 
 $ ( \Rnext BOX514F(X) \leftrightarrow (BOX514F(X) \land $ \\ 
 $  \Rnext E1G3F(X))) \land $ \\ 
 $ ( \Rnext BOX83F(X) \leftrightarrow (BOX83F(X) \land $ \\ 
 $  \Rnext BOX562F(X))) \land $ \\ 
 $ (BOX192F(X) \leftrightarrow  \Rbox E1G23F(X)) \land $ \\ 
 $ (BOX617P(X) \leftrightarrow  \Rbox  \lnot E2G18P(X)) \land $ \\ 
 $ ( \Rnext BOX343P(X) \leftrightarrow (BOX343P(X) \land $ \\ 
 $  \Rnext BOX344P(X))) \land $ \\ 
 $ ( \Rnext BOX82F(X) \leftrightarrow (BOX82F(X) \land $ \\ 
 $  \Rnext BOX561F(X))) \land $ \\ 
 $ ( \Rnext BOX69F(X) \leftrightarrow (BOX69F(X) \land $ \\ 
 $  \Rnext C8F(X))) \land $ \\ 
 $ (BOX70F(X) \leftrightarrow  \Rbox (C24F(X) \land $ \\ 
 $ BOX550F(X) \land $ \\ 
 $ E4G17F(X) \land $ \\ 
 $ DIAMOND262F(X))) \land $ \\ 
 $ (BOX491F(X) \leftrightarrow  \Rbox DIAMOND226F(X)) \land $ \\ 
 $ ( \Rnext BOX348P(X) \leftrightarrow (BOX348P(X) \land $ \\ 
 $  \Rnext BOX349P(X))) \land $ \\ 
 $ (BOX583F(X) \leftrightarrow  \Rbox PG29F) \land $ \\ 
 $ ( \Rnext BOX531F(X) \leftrightarrow (BOX531F(X) \land $ \\ 
 $  \Rnext E2G29F(X))) \land $ \\ 
 $ (BOX374P(X) \leftrightarrow  \Rbox E1G8P(X)) \land $ \\ 
 $ ( \Rnext BOX319P(X) \leftrightarrow (BOX319P(X) \land $ \\ 
 $  \Rnext DIAMOND269P(X))) \land $ \\ 
 $ (BOX659P(X) \leftrightarrow  \Rbox BOX476P(X)) \land $ \\ 
 $ ( \Rnext BOX206F(X) \leftrightarrow (BOX206F(X) \land $ \\ 
 $  \Rnext C25F(X))) \land $ \\ 
 $ ( \Rnext BOX474P(X) \leftrightarrow (BOX474P(X) \land $ \\ 
 $  \Rnext PG5P)) \land $ \\ 
 $ ( \Rnext BOX81F(X) \leftrightarrow (BOX81F(X) \land $ \\ 
 $  \Rnext BOX560F(X))) \land $ \\ 
 $ ( \Rnext BOX507F(X) \leftrightarrow (BOX507F(X) \land $ \\ 
 $  \Rnext E1G20F(X))) \land $ \\ 
 $ (BOX28F(X) \leftrightarrow  \Rbox BOX519F(X)) \land $ \\ 
 $ ( \Rnext BOX462P(X) \leftrightarrow (BOX462P(X) \land $ \\ 
 $  \Rnext PinvG14P)) \land $ \\ 
 $ ( \Rnext BOX528F(X) \leftrightarrow (BOX528F(X) \land $ \\ 
 $  \Rnext E1G12F(X))) \land $ \\ 
 $ (BOX564F(X) \leftrightarrow  \Rbox PG4F) \land $ \\ 
 $ (BOX58F(X) \leftrightarrow  \Rbox BOX543F(X)) \land $ \\ 
 $ (BOX225F(X) \leftrightarrow  \Rbox DIAMOND266F(X)) \land $ \\ 
 $ (BOX584F(X) \leftrightarrow  \Rbox PG14F) \land $ \\ 
 $ (BOX613P(X) \leftrightarrow  \Rbox BOX614P(X)) \land $ \\ 
 $ (BOX409P(X) \leftrightarrow  \Rbox E1G14P(X)) \land $ \\ 
 $ (BOX537F(X) \leftrightarrow  \Rbox (E1G8F(X) \land $ \\ 
 $ E3G14F(X))) \land $ \\ 
 $ ( \Rnext BOX248F(X) \leftrightarrow (BOX248F(X) \land $ \\ 
 $  \Rnext (C12F(X) \land $ \\ 
 $ C10F(X) \land $ \\ 
 $ DIAMOND249F(X)))) \land $ \\ 
 $ ( \Rnext BOX259F(X) \leftrightarrow (BOX259F(X) \land $ \\ 
 $  \Rnext DIAMOND210F(X))) \land $ \\ 
 $ ( \Rnext BOX559F(X) \leftrightarrow (BOX559F(X) \land $ \\ 
 $  \Rnext E4G8F(X))) \land $ \\ 
 $ ( \Rnext BOX487P(X) \leftrightarrow (BOX487P(X) \land $ \\ 
 $  \Rnext PinvG23P)) \land $ \\ 
 $ (BOX80F(X) \leftrightarrow  \Rbox BOX559F(X)) \land $ \\ 
 $ (BOX320P(X) \leftrightarrow  \Rbox DIAMOND271P(X)) \land $ \\ 
 $ ( \Rnext BOX111F(X) \leftrightarrow (BOX111F(X) \land $ \\ 
 $  \Rnext BOX590F(X))) \land $ \\ 
 $ (BOX184F(X) \leftrightarrow  \Rbox BOX499F(X)) \land $ \\ 
 $ ( \Rnext BOX504F(X) \leftrightarrow (BOX504F(X) \land $ \\ 
 $  \Rnext DIAMOND189F(X))) \land $ \\ 
 $ (BOX146P(X) \leftrightarrow  \Rbox E1L26P(X)) \land $ \\ 
 $ (BOX329P(X) \leftrightarrow  \Rbox E1G25P(X)) \land $ \\ 
 $ (BOX337P(X) \leftrightarrow  \Rbox E3G2P(X)) \land $ \\ 
 $ ( \Rnext BOX325P(X) \leftrightarrow (BOX325P(X) \land $ \\ 
 $  \Rnext BOX326P(X))) \land $ \\ 
 $ ( \Rnext BOX451P(X) \leftrightarrow (BOX451P(X) \land $ \\ 
 $  \Rnext PinvG2P)) \land $ \\ 
 $ (BOX25F(X) \leftrightarrow  \Rbox BOX516F(X)) \land $ \\ 
 $ (BOX569F(X) \leftrightarrow  \Rbox PG18F) \land $ \\ 
 $ (BOX592F(X) \leftrightarrow  \Rbox PG3F) \land $ \\ 
 $ (BOX389P(X) \leftrightarrow  \Rbox E2G29P(X)) \land $ \\ 
 $ ( \Rnext BOX445P(X) \leftrightarrow (BOX445P(X) \land $ \\ 
 $  \Rnext PG27P)) \land $ \\ 
 $ ( \Rnext BOX459P(X) \leftrightarrow (BOX459P(X) \land $ \\ 
 $  \Rnext PG7P)) \land $ \\ 
 $ ( \Rnext BOX303P(X) \leftrightarrow (BOX303P(X) \land $ \\ 
 $  \Rnext (DIAMOND155P(X) \land $ \\ 
 $ BOX405P(X)))) \land $ \\ 
 $ ( \Rnext BOX500F(X) \leftrightarrow (BOX500F(X) \land $ \\ 
 $  \Rnext E1G17F(X))) \land $ \\ 
 $ (BOX265F(X) \leftrightarrow  \Rbox  \lnot C13F(X)) \land $ \\ 
 $ ( \Rnext BOX511F(X) \leftrightarrow (BOX511F(X) \land $ \\ 
 $  \Rnext E3G27F(X))) \land $ \\ 
 $ (BOX581F(X) \leftrightarrow  \Rbox PinvG3F) \land $ \\ 
 $ ( \Rnext BOX414P(X) \leftrightarrow (BOX414P(X) \land $ \\ 
 $  \Rnext BOX415P(X))) \land $ \\ 
 $ (BOX638P(X) \leftrightarrow  \Rbox BOX455P(X)) \land $ \\ 
 $ ( \Rnext BOX503F(X) \leftrightarrow (BOX503F(X) \land $ \\ 
 $  \Rnext E1G19F(X))) \land $ \\ 
 $ (BOX552F(X) \leftrightarrow  \Rbox BOX553F(X)) \land $ \\ 
 $ ( \Rnext BOX465P(X) \leftrightarrow (BOX465P(X) \land $ \\ 
 $  \Rnext PG17P)) \land $ \\ 
 $ (BOX540F(X) \leftrightarrow  \Rbox E3G25F(X)) \land $ \\ 
 $ ( \Rnext BOX87F(X) \leftrightarrow (BOX87F(X) \land $ \\ 
 $  \Rnext BOX566F(X))) \land $ \\ 
 $ ( \Rnext BOX408P(X) \leftrightarrow (BOX408P(X) \land $ \\ 
 $  \Rnext BOX409P(X))) \land $ \\ 
 $ (BOX601F(X) \leftrightarrow  \Rbox PinvL26F) \land $ \\ 
 $ (BOX582F(X) \leftrightarrow  \Rbox PG17F) \land $ \\ 
 $ ( \Rnext BOX541F(X) \leftrightarrow (BOX541F(X) \land $ \\ 
 $  \Rnext E1G14F(X))) \land $ \\ 
 $ ( \Rnext BOX358P(X) \leftrightarrow (BOX358P(X) \land $ \\ 
 $  \Rnext BOX359P(X))) \land $ \\ 
 $ (BOX287P(X) \leftrightarrow  \Rbox E5G2P(X)) \land $ \\ 
 $ ( \Rnext BOX508F(X) \leftrightarrow (BOX508F(X) \land $ \\ 
 $  \Rnext E4G14F(X))) \land $ \\ 
 $ ( \Rnext BOX454P(X) \leftrightarrow (BOX454P(X) \land $ \\ 
 $  \Rnext PinvG5P)) \land $ \\ 
 $ (BOX657P(X) \leftrightarrow  \Rbox BOX474P(X)) \land $ \\ 
 $ ( \Rnext BOX193F(X) \leftrightarrow (BOX193F(X) \land $ \\ 
 $  \Rnext DIAMOND194F(X))) \land $ \\ 
 $ (BOX404P(X) \leftrightarrow  \Rbox E2G3P(X)) \land $ \\ 
 $ (BOX664P(X) \leftrightarrow  \Rbox BOX481P(X)) \land $ \\ 
 $ ( \Rnext BOX428P(X) \leftrightarrow (BOX428P(X) \land $ \\ 
 $  \Rnext BOX429P(X))) \land $ \\ 
 $ (BOX357P(X) \leftrightarrow  \Rbox E1G3P(X)) \land $ \\ 
 $ ( \Rnext BOX175P(X) \leftrightarrow (BOX175P(X) \land $ \\ 
 $  \Rnext DIAMOND176P(X))) \land $ \\ 
 $ (BOX423P(X) \leftrightarrow  \Rbox E1G23P(X)) \land $ \\ 
 $ ( \Rnext BOX114F(X) \leftrightarrow (BOX114F(X) \land $ \\ 
 $  \Rnext BOX593F(X))) \land $ \\ 
 $ ( \Rnext BOX94F(X) \leftrightarrow (BOX94F(X) \land $ \\ 
 $  \Rnext BOX573F(X))) \land $ \\ 
 $ ( \Rnext BOX345P(X) \leftrightarrow (BOX345P(X) \land $ \\ 
 $  \Rnext BOX346P(X))) \land $ \\ 
 $ (BOX633P(X) \leftrightarrow  \Rbox BOX450P(X)) \land $ \\ 
 $ ( \Rnext BOX480P(X) \leftrightarrow (BOX480P(X) \land $ \\ 
 $  \Rnext PG8P)) \land $ \\ 
 $ (BOX43F(X) \leftrightarrow  \Rbox BOX534F(X)) \land $ \\ 
 $ (BOX651P(X) \leftrightarrow  \Rbox BOX468P(X)) \land $ \\ 
 $ ( \Rnext BOX424P(X) \leftrightarrow (BOX424P(X) \land $ \\ 
 $  \Rnext BOX425P(X))) \land $ \\ 
 $ (BOX231F(X) \leftrightarrow  \Rbox (E4G25F(X) \land $ \\ 
 $ C4F(X))) \land $ \\ 
 $ (BOX40F(X) \leftrightarrow  \Rbox BOX531F(X)) \land $ \\ 
 $ (BOX22F(X) \leftrightarrow  \Rbox (BOX512F(X) \land $ \\ 
 $ DIAMOND244F(X) \land $ \\ 
 $ BOX513F(X))) \land $ \\ 
 $ (BOX573F(X) \leftrightarrow  \Rbox PinvG27F) \land $ \\ 
 $ (BOX632P(X) \leftrightarrow  \Rbox BOX449P(X)) \land $ \\ 
 $ ( \Rnext BOX334P(X) \leftrightarrow (BOX334P(X) \land $ \\ 
 $  \Rnext BOX335P(X))) \land $ \\ 
 $ ( \Rnext BOX452P(X) \leftrightarrow (BOX452P(X) \land $ \\ 
 $  \Rnext PG18P)) \land $ \\ 
 $ (BOX379P(X) \leftrightarrow  \Rbox BOX380P(X)) \land $ \\ 
 $ ( \Rnext BOX362P(X) \leftrightarrow (BOX362P(X) \land $ \\ 
 $  \Rnext BOX363P(X))) \land $ \\ 
 $ (BOX509F(X) \leftrightarrow  \Rbox (BOX510F(X) \land $ \\ 
 $ DIAMOND242F(X))) \land $ \\ 
 $ ( \Rnext BOX91F(X) \leftrightarrow (BOX91F(X) \land $ \\ 
 $  \Rnext BOX570F(X))) \land $ \\ 
 $ (BOX603F(X) \leftrightarrow  \Rbox PinvG16F) \land $ \\ 
 $ ( \Rnext BOX432P(X) \leftrightarrow (BOX432P(X) \land $ \\ 
 $  \Rnext BOX433P(X))) \land $ \\ 
 $ ( \Rnext BOX517F(X) \leftrightarrow (BOX517F(X) \land $ \\ 
 $  \Rnext E3G4F(X))) \land $ \\ 
 $ ( \Rnext BOX481P(X) \leftrightarrow (BOX481P(X) \land $ \\ 
 $  \Rnext PinvL15P)) \land $ \\ 
 $ (BOX668P(X) \leftrightarrow  \Rbox BOX485P(X)) \land $ \\ 
 $ ( \Rnext BOX232F(X) \leftrightarrow (BOX232F(X) \land $ \\ 
 $  \Rnext BOX498F(X))) \land $ \\ 
 $ (BOX558F(X) \leftrightarrow  \Rbox (C21F(X) \land $ \\ 
 $ E3G28F(X) \land $ \\ 
 $  \lnot E5G17F(X) \land $ \\ 
 $ C15F(X))) \land $ \\ 
 $ (BOX223F(X) \leftrightarrow  \Rbox BOX552F(X)) \land $ \\ 
 $ (BOX16F(X) \leftrightarrow  \Rbox BOX507F(X)) \land $ \\ 
 $ ( \Rnext BOX72F(X) \leftrightarrow (BOX72F(X) \land $ \\ 
 $  \Rnext DIAMOND263F(X))) \land $ \\ 
 $ (BOX227F(X) \leftrightarrow  \Rbox  \lnot E3G11F(X)) \land $ \\ 
 $ (BOX76F(X) \leftrightarrow  \Rbox BOX556F(X)) \land $ \\ 
 $ (BOX591F(X) \leftrightarrow  \Rbox PG5F) \land $ \\ 
 $ (BOX606F(X) \leftrightarrow  \Rbox PinvG12F) \land $ \\ 
 $ (BOX10F(X) \leftrightarrow  \Rbox BOX500F(X)) \land $ \\ 
 $ ( \Rnext BOX557F(X) \leftrightarrow (BOX557F(X) \land $ \\ 
 $  \Rnext E4G25F(X))) \land $ \\ 
 $ ( \Rnext BOX447P(X) \leftrightarrow (BOX447P(X) \land $ \\ 
 $  \Rnext PG4P)) \land $ \\ 
 $ (BOX600F(X) \leftrightarrow  \Rbox PG25F) \land $ \\ 
 $ ( \Rnext BOX484P(X) \leftrightarrow (BOX484P(X) \land $ \\ 
 $  \Rnext PinvL26P)) \land $ \\ 
 $ (BOX566F(X) \leftrightarrow  \Rbox PG20F) \land $ \\ 
 $ (BOX405P(X) \leftrightarrow  \Rbox BOX406P(X)) \land $ \\ 
 $ (BOX339P(X) \leftrightarrow  \Rbox E1G19P(X)) \land $ \\ 
 $ (BOX561F(X) \leftrightarrow  \Rbox PinvG19F) \land $ \\ 
 $ ( \Rnext BOX283P(X) \leftrightarrow (BOX283P(X) \land $ \\ 
 $  \Rnext BOX340P(X))) \land $ \\ 
 $ (BOX352P(X) \leftrightarrow  \Rbox E3G27P(X)) \land $ \\ 
 $ ( \Rnext BOX550F(X) \leftrightarrow (BOX550F(X) \land $ \\ 
 $  \Rnext C11F(X))) \land $ \\ 
 $ ( \Rnext BOX103F(X) \leftrightarrow (BOX103F(X) \land $ \\ 
 $  \Rnext BOX582F(X))) \land $ \\ 
 $ (BOX673P(X) \leftrightarrow  \Rbox BOX490P(X)) \land $ \\ 
 $ (BOX641P(X) \leftrightarrow  \Rbox BOX458P(X)) \land $ \\ 
 $ ( \Rnext BOX416P(X) \leftrightarrow (BOX416P(X) \land $ \\ 
 $  \Rnext BOX417P(X))) \land $ \\ 
 $ ( \Rnext BOX380P(X) \leftrightarrow (BOX380P(X) \land $ \\ 
 $  \Rnext BOX381P(X))) \land $ \\ 
 $ ( \Rnext BOX116F(X) \leftrightarrow (BOX116F(X) \land $ \\ 
 $  \Rnext BOX595F(X))) \land $ \\ 
 $ (BOX624P(X) \leftrightarrow  \Rbox DIAMOND312P(X)) \land $ \\ 
 $ ( \Rnext BOX102F(X) \leftrightarrow (BOX102F(X) \land $ \\ 
 $  \Rnext BOX581F(X))) \land $ \\ 
 $ ( \Rnext BOX494F(X) \leftrightarrow (BOX494F(X) \land $ \\ 
 $  \Rnext E1G18F(X))) \land $ \\ 
 $ ( \Rnext BOX107F(X) \leftrightarrow (BOX107F(X) \land $ \\ 
 $  \Rnext BOX586F(X))) \land $ \\ 
 $ (BOX594F(X) \leftrightarrow  \Rbox PinvG18F) \land $ \\ 
 $ (BOX324P(X) \leftrightarrow  \Rbox E1G18P(X)) \land $ \\ 
 $ ( \Rnext BOX401P(X) \leftrightarrow (BOX401P(X) \land $ \\ 
 $  \Rnext BOX402P(X))) \land $ \\ 
 $ ( \Rnext BOX610F(X) \leftrightarrow (BOX610F(X) \land $ \\ 
 $  \Rnext BOX611F(X))) \land $ \\ 
 $ ( \Rnext BOX369P(X) \leftrightarrow (BOX369P(X) \land $ \\ 
 $  \Rnext BOX370P(X))) \land $ \\ 
 $ (BOX661P(X) \leftrightarrow  \Rbox BOX478P(X)) \land $ \\ 
 $ (BOX41F(X) \leftrightarrow  \Rbox BOX532F(X)) \land $ \\ 
 $ (BOX612P(X) \leftrightarrow  \Rbox DIAMOND129P(X)) \land $ \\ 
 $ (BOX42F(X) \leftrightarrow  \Rbox BOX533F(X)) \land $ \\ 
 $ (BOX442P(X) \leftrightarrow  \Rbox E4G8P(X)) \land $ \\ 
 $ (BOX575F(X) \leftrightarrow  \Rbox PinvG20F) \land $ \\ 
 $ (BOX654P(X) \leftrightarrow  \Rbox BOX471P(X)) \land $ \\ 
 $ (BOX586F(X) \leftrightarrow  \Rbox PinvG11F) \land $ \\ 
 $ ( \Rnext BOX119F(X) \leftrightarrow (BOX119F(X) \land $ \\ 
 $  \Rnext BOX598F(X))) \land $ \\ 
 $ ( \Rnext BOX364P(X) \leftrightarrow (BOX364P(X) \land $ \\ 
 $  \Rnext BOX365P(X))) \land $ \\ 
 $ (BOX256F(X) \leftrightarrow  \Rbox (DIAMOND203F(X) \land $ \\ 
 $ BOX539F(X))) \land $ \\ 
 $ (BOX393P(X) \leftrightarrow  \Rbox E1G29P(X)) \land $ \\ 
 $ ( \Rnext BOX328P(X) \leftrightarrow (BOX328P(X) \land $ \\ 
 $  \Rnext BOX329P(X))) \land $ \\ 
 $ ( \Rnext BOX392P(X) \leftrightarrow (BOX392P(X) \land $ \\ 
 $  \Rnext BOX393P(X))) \land $ \\ 
 $ ( \Rnext BOX331P(X) \leftrightarrow (BOX331P(X) \land $ \\ 
 $  \Rnext E2G20P(X))) \land $ \\ 
 $ (BOX385P(X) \leftrightarrow  \Rbox E3G14P(X)) \land $ \\ 
 $ (BOX376P(X) \leftrightarrow  \Rbox E5G29P(X)) \land $ \\ 
 $ (BOX648P(X) \leftrightarrow  \Rbox BOX465P(X)) \land $ \\ 
 $ (BOX74F(X) \leftrightarrow  \Rbox BOX554F(X)) \land $ \\ 
 $ ( \Rnext BOX543F(X) \leftrightarrow (BOX543F(X) \land $ \\ 
 $  \Rnext (E4G25F(X) \land $ \\ 
 $ DIAMOND258F(X)))) \land $ \\ 
 $ (BOX435P(X) \leftrightarrow  \Rbox E4G4P(X)) \land $ \\ 
 $ ( \Rnext BOX89F(X) \leftrightarrow (BOX89F(X) \land $ \\ 
 $  \Rnext BOX568F(X))) \land $ \\ 
 $ (BOX429P(X) \leftrightarrow  \Rbox E1G11P(X)) \land $ \\ 
 $ ( \Rnext BOX92F(X) \leftrightarrow (BOX92F(X) \land $ \\ 
 $  \Rnext BOX571F(X))) \land $ \\ 
 $ ( \Rnext BOX515F(X) \leftrightarrow (BOX515F(X) \land $ \\ 
 $  \Rnext E3G18F(X))) \land $ \\ 
 $ ( \Rnext BOX440P(X) \leftrightarrow (BOX440P(X) \land $ \\ 
 $  \Rnext (C21P(X) \land $ \\ 
 $ E3G28P(X) \land $ \\ 
 $  \lnot E5G17P(X) \land $ \\ 
 $ C15P(X)))) \land $ \\ 
 $ ( \Rnext BOX98F(X) \leftrightarrow (BOX98F(X) \land $ \\ 
 $  \Rnext BOX577F(X))) \land $ \\ 
 $ (BOX383P(X) \leftrightarrow  \Rbox E1G12P(X)) \land $ \\ 
 $ ( \Rnext BOX441P(X) \leftrightarrow (BOX441P(X) \land $ \\ 
 $  \Rnext BOX442P(X))) \land $ \\ 
 $ (BOX17F(X) \leftrightarrow  \Rbox BOX508F(X)) \land $ \\ 
 $ ( \Rnext BOX1F(X) \leftrightarrow (BOX1F(X) \land $ \\ 
 $  \Rnext DIAMOND182F(X))) \land $ \\ 
 $ (BOX626P(X) \leftrightarrow  \Rbox BOX443P(X)) \land $ \\ 
 $ (BOX614P(X) \leftrightarrow  \Rbox BOX327P(X)) \land $ \\ 
 $ ( \Rnext BOX101F(X) \leftrightarrow (BOX101F(X) \land $ \\ 
 $  \Rnext BOX580F(X))) \land $ \\ 
 $ ( \Rnext BOX178P(X) \leftrightarrow (BOX178P(X) \land $ \\ 
 $  \Rnext BOX430P(X))) \land $ \\ 
 $ ( \Rnext BOX611F(X) \leftrightarrow (BOX611F(X) \land $ \\ 
 $  \Rnext (DIAMOND202F(X) \land $ \\ 
 $ DIAMOND255F(X)))) \land $ \\ 
 $ ( \Rnext BOX128F(X) \leftrightarrow (BOX128F(X) \land $ \\ 
 $  \Rnext BOX607F(X))) \land $ \\ 
 $ (BOX370P(X) \leftrightarrow  \Rbox E1G5P(X)) \land $ \\ 
 $ ( \Rnext BOX444P(X) \leftrightarrow (BOX444P(X) \land $ \\ 
 $  \Rnext PinvG19P)) \land $ \\ 
 $ ( \Rnext BOX394P(X) \leftrightarrow (BOX394P(X) \land $ \\ 
 $  \Rnext BOX395P(X))) \land $ \\ 
 $ ( \Rnext BOX555F(X) \leftrightarrow (BOX555F(X) \land $ \\ 
 $  \Rnext E4G4F(X))) \land $ \\ 
 $ (BOX574F(X) \leftrightarrow  \Rbox PinvG4F) \land $ \\ 
 $ (BOX636P(X) \leftrightarrow  \Rbox BOX453P(X)) \land $ \\ 
 $ (BOX294P(X) \leftrightarrow  \Rbox (C12P(X) \land $ \\ 
 $ C10P(X) \land $ \\ 
 $ DIAMOND295P(X))) \land $ \\ 
 $ (BOX496F(X) \leftrightarrow  \Rbox (E4G4F(X) \land $ \\ 
 $ DIAMOND229F(X) \land $ \\ 
 $ DIAMOND230F(X))) \land $ \\ 
 $ ( \Rnext BOX523F(X) \leftrightarrow (BOX523F(X) \land $ \\ 
 $  \Rnext E5G29F(X))) \land $ \\ 
 $ ( \Rnext BOX122F(X) \leftrightarrow (BOX122F(X) \land $ \\ 
 $  \Rnext BOX601F(X))) \land $ \\ 
 $ (BOX671P(X) \leftrightarrow  \Rbox BOX488P(X)) \land $ \\ 
 $ (BOX254F(X) \leftrightarrow  \Rbox E2G9F(X)) \land $ \\ 
 $ (BOX590F(X) \leftrightarrow  \Rbox PG23F) \land $ \\ 
 $ (BOX220F(X) \leftrightarrow  \Rbox DIAMOND221F(X)) \land $ \\ 
 $ (BOX67F(X) \leftrightarrow  \Rbox BOX549F(X)) \land $ \\ 
 $ ( \Rnext BOX529F(X) \leftrightarrow (BOX529F(X) \land $ \\ 
 $  \Rnext E3G14F(X))) \land $ \\ 
 $ (BOX3F(X) \leftrightarrow  \Rbox BOX494F(X)) \land $ \\ 
 $ (BOX585F(X) \leftrightarrow  \Rbox PinvG17F) \land $ \\ 
 $ (BOX631P(X) \leftrightarrow  \Rbox BOX448P(X)) \land $ \\ 
 $ (BOX391P(X) \leftrightarrow  \Rbox E4G12P(X)) \land $ \\ 
 $ ( \Rnext BOX460P(X) \leftrightarrow (BOX460P(X) \land $ \\ 
 $  \Rnext PL15P)) \land $ \\ 
 $ (BOX565F(X) \leftrightarrow  \Rbox PinvG8F) \land $ \\ 
 $ (BOX579F(X) \leftrightarrow  \Rbox PinvG14F) \land $ \\ 
 $ ( \Rnext BOX536F(X) \leftrightarrow (BOX536F(X) \land $ \\ 
 $  \Rnext E1G9F(X))) \land $ \\ 
 $ ( \Rnext BOX373P(X) \leftrightarrow (BOX373P(X) \land $ \\ 
 $  \Rnext BOX374P(X))) \land $ \\ 
 $ (BOX30F(X) \leftrightarrow  \Rbox BOX520F(X)) \land $ \\ 
 $ ( \Rnext BOX457P(X) \leftrightarrow (BOX457P(X) \land $ \\ 
 $  \Rnext PinvG4P)) \land $ \\ 
 $ (BOX439P(X) \leftrightarrow  \Rbox E4G25P(X)) \land $ \\ 
 $ ( \Rnext BOX112F(X) \leftrightarrow (BOX112F(X) \land $ \\ 
 $  \Rnext BOX591F(X))) \land $ \\ 
 $ (BOX598F(X) \leftrightarrow  \Rbox PinvL15F) \land $ \\ 
 $ (BOX672P(X) \leftrightarrow  \Rbox BOX489P(X)) \land $ \\ 
 $ ( \Rnext BOX402P(X) \leftrightarrow (BOX402P(X) \land $ \\ 
 $  \Rnext (E1G8P(X) \land $ \\ 
 $ E3G14P(X)))) \land $ \\ 
 $ (BOX237F(X) \leftrightarrow  \Rbox BOX504F(X)) \land $ \\ 
 $ ( \Rnext BOX95F(X) \leftrightarrow (BOX95F(X) \land $ \\ 
 $  \Rnext BOX574F(X))) \land $ \\ 
 $ ( \Rnext BOX430P(X) \leftrightarrow (BOX430P(X) \land $ \\ 
 $  \Rnext BOX431P(X))) \land $ \\ 
 $ (BOX159P(X) \leftrightarrow  \Rbox C25P(X)) \land $ \\ 
 $ (BOX395P(X) \leftrightarrow  \Rbox E2G20P(X)) \land $ \\ 
 $ ( \Rnext BOX556F(X) \leftrightarrow (BOX556F(X) \land $ \\ 
 $  \Rnext E3G28F(X))) \land $ \\ 
 $ (BOX527F(X) \leftrightarrow  \Rbox DIAMOND198F(X)) \land $ \\ 
 $ (BOX568F(X) \leftrightarrow  \Rbox PinvG2F) \land $ \\ 
 $ (BOX413P(X) \leftrightarrow  \Rbox (E4G25P(X) \land $ \\ 
 $ DIAMOND306P(X))) \land $ \\ 
 $ ( \Rnext BOX532F(X) \leftrightarrow (BOX532F(X) \land $ \\ 
 $  \Rnext E4G12F(X))) \land $ \\ 
 $ (BOX618P(X) \leftrightarrow  \Rbox DIAMOND299P(X)) \land $ \\ 
 $ ( \Rnext BOX300P(X) \leftrightarrow (BOX300P(X) \land $ \\ 
 $  \Rnext E2G9P(X))) \land $ \\ 
 $ (BOX597F(X) \leftrightarrow  \Rbox PG8F) \land $ \\ 
 $ (BOX499F(X) \leftrightarrow  \Rbox E2G20F(X)) \land $ \\ 
 $ (BOX629P(X) \leftrightarrow  \Rbox BOX446P(X)) \land $ \\ 
 $ (BOX12F(X) \leftrightarrow  \Rbox BOX502F(X)) \land $ \\ 
 $ ( \Rnext BOX420P(X) \leftrightarrow (BOX420P(X) \land $ \\ 
 $  \Rnext BOX421P(X))) \land $ \\ 
 $ ( \Rnext BOX51F(X) \leftrightarrow (BOX51F(X) \land $ \\ 
 $  \Rnext BOX610F(X))) \land $ \\ 
 $ ( \Rnext BOX371P(X) \leftrightarrow (BOX371P(X) \land $ \\ 
 $  \Rnext BOX372P(X))) \land $ \\ 
 $ ( \Rnext BOX476P(X) \leftrightarrow (BOX476P(X) \land $ \\ 
 $  \Rnext PL29P)) \land $ \\ 
 $ ( \Rnext BOX353P(X) \leftrightarrow (BOX353P(X) \land $ \\ 
 $  \Rnext (BOX354P(X) \land $ \\ 
 $ DIAMOND290P(X) \land $ \\ 
 $ BOX355P(X)))) \land $ \\ 
 $ ( \Rnext BOX360P(X) \leftrightarrow (BOX360P(X) \land $ \\ 
 $  \Rnext BOX361P(X))) \land $ \\ 
 $ ( \Rnext BOX473P(X) \leftrightarrow (BOX473P(X) \land $ \\ 
 $  \Rnext PG23P)) \land $ \\ 
 $ ( \Rnext BOX415P(X) \leftrightarrow (BOX415P(X) \land $ \\ 
 $  \Rnext ( \lnot C1P(X) \land $ \\ 
 $ DIAMOND160P(X)))) \land $ \\ 
 $ ( \Rnext BOX493F(X) \leftrightarrow (BOX493F(X) \land $ \\ 
 $  \Rnext E1G4F(X))) \land $ \\ 
 $ ( \Rnext BOX118F(X) \leftrightarrow (BOX118F(X) \land $ \\ 
 $  \Rnext BOX597F(X))) \land $ \\ 
 $ (BOX658P(X) \leftrightarrow  \Rbox BOX475P(X)) \land $ \\ 
 $ ( \Rnext BOX489P(X) \leftrightarrow (BOX489P(X) \land $ \\ 
 $  \Rnext PinvG12P)) \land $ \\ 
 $ (BOX589F(X) \leftrightarrow  \Rbox PG16F) \land $ \\ 
 $ (BOX607F(X) \leftrightarrow  \Rbox PinvG9F) \land $ \\ 
 $ ( \Rnext BOX434P(X) \leftrightarrow (BOX434P(X) \land $ \\ 
 $  \Rnext BOX435P(X))) \land $ \\ 
 $ ( \Rnext BOX125F(X) \leftrightarrow (BOX125F(X) \land $ \\ 
 $  \Rnext BOX604F(X))) \land $ \\ 
 $ ( \Rnext BOX388P(X) \leftrightarrow (BOX388P(X) \land $ \\ 
 $  \Rnext BOX389P(X))) \land $ \\ 
 $ ( \Rnext BOX522F(X) \leftrightarrow (BOX522F(X) \land $ \\ 
 $  \Rnext E1G8F(X))) \land $ \\ 
 $ (BOX587F(X) \leftrightarrow  \Rbox PinvL29F) \land $ \\ 
 $ ( \Rnext BOX46F(X) \leftrightarrow (BOX46F(X) \land $ \\ 
 $  \Rnext (BOX609F(X) \land $ \\ 
 $ DIAMOND251F(X)))) \land $ \\ 
 $ ( \Rnext BOX123F(X) \leftrightarrow (BOX123F(X) \land $ \\ 
 $  \Rnext BOX602F(X))) \land $ \\ 
 $ (BOX367P(X) \leftrightarrow  \Rbox E4G9P(X)) \land $ \\ 
 $ (BOX346P(X) \leftrightarrow  \Rbox E4G14P(X)) \land $ \\ 
 $ (BOX344P(X) \leftrightarrow  \Rbox E1G20P(X)) \land $ \\ 
 $ ( \Rnext BOX521F(X) \leftrightarrow (BOX521F(X) \land $ \\ 
 $  \Rnext E1G2F(X))) \land $ \\ 
 $ ( \Rnext BOX106F(X) \leftrightarrow (BOX106F(X) \land $ \\ 
 $  \Rnext BOX585F(X))) \land $ \\ 
 $ ( \Rnext BOX350P(X) \leftrightarrow (BOX350P(X) \land $ \\ 
 $  \Rnext (C17P(X) \land $ \\ 
 $ E4L1P(X)))) \land $ \\ 
 $ (BOX56F(X) \leftrightarrow  \Rbox BOX541F(X)) \land $ \\ 
 $ (BOX498F(X) \leftrightarrow  \Rbox DIAMOND233F(X)) \land $ \\ 
 $ ( \Rnext BOX398P(X) \leftrightarrow (BOX398P(X) \land $ \\ 
 $  \Rnext BOX399P(X))) \land $ \\ 
 $ (BOX669P(X) \leftrightarrow  \Rbox BOX486P(X)) \land $ \\ 
 $ (BOX26F(X) \leftrightarrow  \Rbox BOX517F(X)) \land $ \\ 
 $ (BOX139P(X) \leftrightarrow  \Rbox BOX341P(X)) \land $ \\ 
 $ ( \Rnext BOX347P(X) \leftrightarrow (BOX347P(X) \land $ \\ 
 $  \Rnext DIAMOND284P(X))) \land $ \\ 
 $ (BOX361P(X) \leftrightarrow  \Rbox E1G28P(X)) \land $ \\ 
 $ (BOX644P(X) \leftrightarrow  \Rbox BOX461P(X)) \land $ \\ 
 $ ( \Rnext BOX382P(X) \leftrightarrow (BOX382P(X) \land $ \\ 
 $  \Rnext BOX383P(X))) \land $ \\ 
 $ (BOX571F(X) \leftrightarrow  \Rbox PinvG5F) \land $ \\ 
 $ ( \Rnext BOX492F(X) \leftrightarrow (BOX492F(X) \land $ \\ 
 $  \Rnext DIAMOND228F(X))) \land $ \\ 
 $ (BOX667P(X) \leftrightarrow  \Rbox BOX484P(X)) \land $ \\ 
 $ ( \Rnext BOX461P(X) \leftrightarrow (BOX461P(X) \land $ \\ 
 $  \Rnext PG11P)) \land $ \\ 
 $ (BOX615P(X) \leftrightarrow  \Rbox DIAMOND293P(X)) \land $ \\ 
 $ (BOX29F(X) \leftrightarrow  \Rbox BOX241F(X)) \land $ \\ 
 $ (BOX580F(X) \leftrightarrow  \Rbox PL1F) \land $ \\ 
 $ (BOX593F(X) \leftrightarrow  \Rbox PL29F) \land $ \\ 
 $ ( \Rnext BOX141P(X) \leftrightarrow (BOX141P(X) \land $ \\ 
 $  \Rnext E1G23P(X))) \land $ \\ 
 $ ( \Rnext BOX386P(X) \leftrightarrow (BOX386P(X) \land $ \\ 
 $  \Rnext BOX387P(X))) \land $ \\ 
 $ (BOX604F(X) \leftrightarrow  \Rbox PinvG23F) \land $ \\ 
 $ ( \Rnext BOX609F(X) \leftrightarrow (BOX609F(X) \land $ \\ 
 $  \Rnext  \lnot E2G18F(X))) \land $ \\ 
 $ (BOX663P(X) \leftrightarrow  \Rbox BOX480P(X)) \land $ \\ 
 $ ( \Rnext BOX121F(X) \leftrightarrow (BOX121F(X) \land $ \\ 
 $  \Rnext BOX600F(X))) \land $ \\ 
 $ (BOX630P(X) \leftrightarrow  \Rbox BOX447P(X)) \land $ \\ 
 $ ( \Rnext BOX497F(X) \leftrightarrow (BOX497F(X) \land $ \\ 
 $  \Rnext E1G25F(X))) \land $ \\ 
 $ (BOX39F(X) \leftrightarrow  \Rbox BOX530F(X)) \land $ \\ 
 $ ( \Rnext BOX349P(X) \leftrightarrow (BOX349P(X) \land $ \\ 
 $  \Rnext (BOX350P(X) \land $ \\ 
 $ DIAMOND288P(X)))) \land $ \\ 
 $ ( \Rnext BOX486P(X) \leftrightarrow (BOX486P(X) \land $ \\ 
 $  \Rnext PinvG16P)) \land $ \\ 
 $ (BOX31F(X) \leftrightarrow  \Rbox BOX521F(X)) \land $ \\ 
 $ (BOX649P(X) \leftrightarrow  \Rbox BOX466P(X)) \land $ \\ 
 $ (BOX322P(X) \leftrightarrow  \Rbox E1G4P(X)) \land $ \\ 
 $ (BOX660P(X) \leftrightarrow  \Rbox BOX477P(X)) \land $ \\ 
 $ ( \Rnext BOX407P(X) \leftrightarrow (BOX407P(X) \land $ \\ 
 $  \Rnext C28P(X))) \land $ \\ 
 $ (BOX577F(X) \leftrightarrow  \Rbox PL15F) \land $ \\ 
 $ ( \Rnext BOX84F(X) \leftrightarrow (BOX84F(X) \land $ \\ 
 $  \Rnext BOX563F(X))) \land $ \\ 
 $ ( \Rnext BOX275P(X) \leftrightarrow (BOX275P(X) \land $ \\ 
 $  \Rnext (E4G25P(X) \land $ \\ 
 $ C4P(X)))) \land $ \\ 
 $ (BOX47F(X) \leftrightarrow  \Rbox BOX536F(X)) \land $ \\ 
 $ (BOX0F(X) \leftrightarrow  \Rbox (BOX491F(X) \land $ \\ 
 $ BOX492F(X))) \land $ \\ 
 $ (BOX13F(X) \leftrightarrow  \Rbox BOX503F(X)) \land $ \\ 
 $ ( \Rnext BOX190F(X) \leftrightarrow (BOX190F(X) \land $ \\ 
 $  \Rnext BOX505F(X))) \land $ \\ 
 $ (BOX20F(X) \leftrightarrow  \Rbox BOX511F(X)) \land $ \\ 
 $ (BOX562F(X) \leftrightarrow  \Rbox PG27F) \land $ \\ 
 $ ( \Rnext BOX466P(X) \leftrightarrow (BOX466P(X) \land $ \\ 
 $  \Rnext PG29P)) \land $ \\ 
 $ ( \Rnext BOX113F(X) \leftrightarrow (BOX113F(X) \land $ \\ 
 $  \Rnext BOX592F(X))) \land $ \\ 
 $ (BOX599F(X) \leftrightarrow  \Rbox PinvG25F) \land $ \\ 
 $ ( \Rnext BOX453P(X) \leftrightarrow (BOX453P(X) \land $ \\ 
 $  \Rnext PG28P)) \land $ \\ 
 $ (BOX57F(X) \leftrightarrow  \Rbox BOX542F(X)) \land $ \\ 
 $ ( \Rnext BOX549F(X) \leftrightarrow (BOX549F(X) \land $ \\ 
 $  \Rnext E5G17F(X))) \land $ \\ 
 $ ( \Rnext BOX318P(X) \leftrightarrow (BOX318P(X) \land $ \\ 
 $  \Rnext (BOX319P(X) \land $ \\ 
 $ BOX320P(X)))) \land $ \\ 
 $ (BOX33F(X) \leftrightarrow  \Rbox BOX523F(X)) \land $ \\ 
 $ (BOX567F(X) \leftrightarrow  \Rbox PinvG29F) \land $ \\ 
 $ ( \Rnext BOX100F(X) \leftrightarrow (BOX100F(X) \land $ \\ 
 $  \Rnext BOX579F(X))) \land $ \\ 
 $ (BOX646P(X) \leftrightarrow  \Rbox BOX463P(X)) \land $ \\ 
 $ ( \Rnext BOX470P(X) \leftrightarrow (BOX470P(X) \land $ \\ 
 $  \Rnext PinvL29P)) \land $ \\ 
 $ (BOX38F(X) \leftrightarrow  \Rbox BOX529F(X)) \land $ \\ 
 $ ( \Rnext BOX397P(X) \leftrightarrow (BOX397P(X) \land $ \\ 
 $  \Rnext DIAMOND296P(X))) \land $ \\ 
 $ ( \Rnext BOX448P(X) \leftrightarrow (BOX448P(X) \land $ \\ 
 $  \Rnext PinvG8P)) \land $ \\ 
 $ (BOX576F(X) \leftrightarrow  \Rbox PG7F) \land $ \\ 
 $ ( \Rnext BOX36F(X) \leftrightarrow (BOX36F(X) \land $ \\ 
 $  \Rnext DIAMOND247F(X))) \land $ \\ 
 $ (BOX619P(X) \leftrightarrow  \Rbox BOX620P(X)) \land $ \\ 
 $ ( \Rnext BOX458P(X) \leftrightarrow (BOX458P(X) \land $ \\ 
 $  \Rnext PinvG20P)) \land $ \\ 
 $ ( \Rnext BOX240F(X) \leftrightarrow (BOX240F(X) \land $ \\ 
 $  \Rnext E1G7F(X))) \land $ \\ 
 $ ( \Rnext BOX449P(X) \leftrightarrow (BOX449P(X) \land $ \\ 
 $  \Rnext PG20P)) \land $ \\ 
 $ (BOX670P(X) \leftrightarrow  \Rbox BOX487P(X)) \land $ \\ 
 $ ( \Rnext BOX547F(X) \leftrightarrow (BOX547F(X) \land $ \\ 
 $  \Rnext E5G4F(X))) \land $ \\ 
 $ (BOX666P(X) \leftrightarrow  \Rbox BOX483P(X)) \land $ \\ 
 $ (BOX342P(X) \leftrightarrow  \Rbox DIAMOND140P(X)) \land $ \\ 
 $ ( \Rnext BOX495F(X) \leftrightarrow (BOX495F(X) \land $ \\ 
 $  \Rnext E1G27F(X))) \land $ \\ 
 $ ( \Rnext BOX548F(X) \leftrightarrow (BOX548F(X) \land $ \\ 
 $  \Rnext E1G23F(X))) \land $ \\ 
 $ (BOX510F(X) \leftrightarrow  \Rbox (C17F(X) \land $ \\ 
 $ E4L1F(X))) \land $ \\ 
 $ ( \Rnext BOX471P(X) \leftrightarrow (BOX471P(X) \land $ \\ 
 $  \Rnext PinvL1P)) \land $ \\ 
 $ (BOX544F(X) \leftrightarrow  \Rbox ( \lnot C1F(X) \land $ \\ 
 $ DIAMOND207F(X))) \land $ \\ 
 $ ( \Rnext BOX438P(X) \leftrightarrow (BOX438P(X) \land $ \\ 
 $  \Rnext BOX439P(X))) \land $ \\ 
 $ (BOX662P(X) \leftrightarrow  \Rbox BOX479P(X)) \land $ \\ 
 $ (BOX378P(X) \leftrightarrow  \Rbox E4G17P(X)) \land $ \\ 
 $ ( \Rnext BOX241F(X) \leftrightarrow (BOX241F(X) \land $ \\ 
 $  \Rnext E5G2F(X))) \land $ \\ 
 $ ( \Rnext BOX126F(X) \leftrightarrow (BOX126F(X) \land $ \\ 
 $  \Rnext BOX605F(X))) \land $ \\ 
 $ (BOX18F(X) \leftrightarrow  \Rbox DIAMOND238F(X)) \land $ \\ 
 $ (BOX399P(X) \leftrightarrow  \Rbox E1G9P(X)) \land $ \\ 
 $ ( \Rnext BOX78F(X) \leftrightarrow (BOX78F(X) \land $ \\ 
 $  \Rnext BOX558F(X))) \land $ \\ 
 $ (BOX656P(X) \leftrightarrow  \Rbox BOX473P(X)) \land $ \\ 
 $ (BOX62F(X) \leftrightarrow  \Rbox BOX546F(X)) \land $ \\ 
 $ (BOX595F(X) \leftrightarrow  \Rbox PinvG28F) \land $ \\ 
 $ (BOX643P(X) \leftrightarrow  \Rbox BOX460P(X)) \land $ \\ 
 $ ( \Rnext BOX443P(X) \leftrightarrow (BOX443P(X) \land $ \\ 
 $  \Rnext PL26P)) \land $ \\ 
 $ ( \Rnext BOX115F(X) \leftrightarrow (BOX115F(X) \land $ \\ 
 $  \Rnext BOX594F(X))) \land $ \\ 
 $ (BOX628P(X) \leftrightarrow  \Rbox BOX445P(X)) \land $ \\ 
 $ ( \Rnext BOX150P(X) \leftrightarrow (BOX150P(X) \land $ \\ 
 $  \Rnext  \lnot C4P(X))) \land $ \\ 
 $ (BOX335P(X) \leftrightarrow  \Rbox E3G11P(X)) \land $ \\ 
 $ (BOX55F(X) \leftrightarrow  \Rbox C28F(X)) \land $ \\ 
 $ ( \Rnext BOX506F(X) \leftrightarrow (BOX506F(X) \land $ \\ 
 $  \Rnext DIAMOND191F(X))) \land $ \\ 
 $ ( \Rnext BOX400P(X) \leftrightarrow (BOX400P(X) \land $ \\ 
 $  \Rnext BOX286P(X))) \land $ \\ 
 $ (BOX602F(X) \leftrightarrow  \Rbox PG12F) \land $ \\ 
 $ ( \Rnext BOX5F(X) \leftrightarrow (BOX5F(X) \land $ \\ 
 $  \Rnext BOX608F(X))) \land $ \\ 
 $ (BOX622P(X) \leftrightarrow  \Rbox (DIAMOND171P(X) \land $ \\ 
 $ DIAMOND172P(X))) \land $ \\ 
 $ ( \Rnext BOX105F(X) \leftrightarrow (BOX105F(X) \land $ \\ 
 $  \Rnext BOX584F(X))) \land $ \\ 
 $ ( \Rnext BOX551F(X) \leftrightarrow (BOX551F(X) \land $ \\ 
 $  \Rnext E1G11F(X))) \land $ \\ 
 $ (BOX359P(X) \leftrightarrow  \Rbox E3G18P(X)) \land $ \\ 
 $ (BOX505F(X) \leftrightarrow  \Rbox BOX506F(X)) \land $ \\ 
 $ ( \Rnext BOX410P(X) \leftrightarrow (BOX410P(X) \land $ \\ 
 $  \Rnext BOX411P(X))) \land $ \\ 
 $ (BOX11F(X) \leftrightarrow  \Rbox BOX501F(X)) \land $ \\ 
 $ ( \Rnext BOX85F(X) \leftrightarrow (BOX85F(X) \land $ \\ 
 $  \Rnext BOX564F(X))) \land $ \\ 
 $ ( \Rnext BOX418P(X) \leftrightarrow (BOX418P(X) \land $ \\ 
 $  \Rnext BOX419P(X))) \land $ \\ 
 $ ( \Rnext BOX309P(X) \leftrightarrow (BOX309P(X) \land $ \\ 
 $  \Rnext DIAMOND310P(X))) \land $ \\ 
 $ ( \Rnext BOX533F(X) \leftrightarrow (BOX533F(X) \land $ \\ 
 $  \Rnext E1G29F(X))) \land $ \\ 
 $ ( \Rnext BOX446P(X) \leftrightarrow (BOX446P(X) \land $ \\ 
 $  \Rnext PG2P)) \land $ \\ 
 $ ( \Rnext BOX467P(X) \leftrightarrow (BOX467P(X) \land $ \\ 
 $  \Rnext PG14P)) \land $ \\ 
 $ ( \Rnext BOX127F(X) \leftrightarrow (BOX127F(X) \land $ \\ 
 $  \Rnext BOX606F(X))) \land $ \\ 
 $ ( \Rnext BOX132P(X) \leftrightarrow (BOX132P(X) \land $ \\ 
 $  \Rnext BOX331P(X))) \land $ \\ 
 $ (BOX419P(X) \leftrightarrow  \Rbox E2G9P(X)) \land $ \\ 
 $ ( \Rnext BOX490P(X) \leftrightarrow (BOX490P(X) \land $ \\ 
 $  \Rnext PinvG9P)) \land $ \\ 
 $ ( \Rnext BOX546F(X) \leftrightarrow (BOX546F(X) \land $ \\ 
 $  \Rnext E2G9F(X))) \land $ \\ 
 $ ( \Rnext BOX608F(X) \leftrightarrow (BOX608F(X) \land $ \\ 
 $  \Rnext BOX496F(X))) \land $ \\ 
 $ (BOX578F(X) \leftrightarrow  \Rbox PG11F) \land $ \\ 
 $ ( \Rnext BOX330P(X) \leftrightarrow (BOX330P(X) \land $ \\ 
 $  \Rnext DIAMOND278P(X))) \land $ \\ 
 $ ( \Rnext BOX375P(X) \leftrightarrow (BOX375P(X) \land $ \\ 
 $  \Rnext BOX376P(X))) \land $ \\ 
 $ (BOX596F(X) \leftrightarrow  \Rbox PG19F) \land $ \\ 
 $ ( \Rnext BOX538F(X) \leftrightarrow (BOX538F(X) \land $ \\ 
 $  \Rnext E2G3F(X))) \land $ \\ 
 $ (BOX526F(X) \leftrightarrow  \Rbox BOX527F(X)) \land $ \\ 
 $ (BOX653P(X) \leftrightarrow  \Rbox BOX470P(X)) \land $ \\ 
 $ (BOX620P(X) \leftrightarrow  \Rbox BOX621P(X)) \land $ \\ 
 $ ( \Rnext BOX456P(X) \leftrightarrow (BOX456P(X) \land $ \\ 
 $  \Rnext PinvG27P)) \land $ \\ 
 $ ( \Rnext BOX68F(X) \leftrightarrow (BOX68F(X) \land $ \\ 
 $  \Rnext (DIAMOND217F(X) \land $ \\ 
 $ DIAMOND218F(X)))) \land $ \\ 
 $ ( \Rnext BOX354P(X) \leftrightarrow (BOX354P(X) \land $ \\ 
 $  \Rnext C13P(X))) \land $ \\ 
 $ ( \Rnext BOX390P(X) \leftrightarrow (BOX390P(X) \land $ \\ 
 $  \Rnext BOX391P(X))) \land $ \\ 
 $ ( \Rnext BOX412P(X) \leftrightarrow (BOX412P(X) \land $ \\ 
 $  \Rnext BOX413P(X))) \land $ \\ 
 $ ( \Rnext BOX554F(X) \leftrightarrow (BOX554F(X) \land $ \\ 
 $  \Rnext E3G25F(X))) \land $ \\ 
 $ ( \Rnext BOX406P(X) \leftrightarrow (BOX406P(X) \land $ \\ 
 $  \Rnext E3G25P(X))) \land $ \\ 
 $ (BOX246F(X) \leftrightarrow  \Rbox BOX525F(X)) \land $ \\ 
 $ ( \Rnext BOX482P(X) \leftrightarrow (BOX482P(X) \land $ \\ 
 $  \Rnext PinvG25P)) \land $ \\ 
 $ ( \Rnext BOX110F(X) \leftrightarrow (BOX110F(X) \land $ \\ 
 $  \Rnext BOX589F(X))) \land $ \\ 
 $ ( \Rnext BOX478P(X) \leftrightarrow (BOX478P(X) \land $ \\ 
 $  \Rnext PinvG28P)) \land $ \\ 
 $ (BOX326P(X) \leftrightarrow  \Rbox E1G27P(X)) \land $ \\ 
 $ (BOX417P(X) \leftrightarrow  \Rbox E3G7P(X)) \land $ \\ 
 $ ( \Rnext BOX323P(X) \leftrightarrow (BOX323P(X) \land $ \\ 
 $  \Rnext BOX324P(X))) \land $ \\ 
 $ (BOX625P(X) \leftrightarrow  \Rbox BOX440P(X)) \land $ \\ 
 $ ( \Rnext BOX518F(X) \leftrightarrow (BOX518F(X) \land $ \\ 
 $  \Rnext E2G5F(X))) \land $ \\ 
 $ (BOX433P(X) \leftrightarrow  \Rbox E3G25P(X)) \land $ \\ 
 $ ( \Rnext BOX366P(X) \leftrightarrow (BOX366P(X) \land $ \\ 
 $  \Rnext BOX367P(X))) \land $ \\ 
 $ ( \Rnext BOX479P(X) \leftrightarrow (BOX479P(X) \land $ \\ 
 $  \Rnext PG19P)) \land $ \\ 
 $ ( \Rnext BOX124F(X) \leftrightarrow (BOX124F(X) \land $ \\ 
 $  \Rnext BOX603F(X))) \land $ \\ 
 $ ( \Rnext BOX181P(X) \leftrightarrow (BOX181P(X) \land $ \\ 
 $  \Rnext DIAMOND315P(X))) \land $ \\ 
 $ ( \Rnext BOX450P(X) \leftrightarrow (BOX450P(X) \land $ \\ 
 $  \Rnext PinvG29P)) \land $ \\ 
 $ (BOX71F(X) \leftrightarrow  \Rbox BOX551F(X)) \land $ \\ 
 $ (BOX340P(X) \leftrightarrow  \Rbox DIAMOND138P(X)) \land $ \\ 
 $ ( \Rnext BOX396P(X) \leftrightarrow (BOX396P(X) \land $ \\ 
 $  \Rnext BOX397P(X))) \land $ \\ 
 $ (BOX427P(X) \leftrightarrow  \Rbox C11P(X)) \land $ \\ 
 $ ( \Rnext BOX96F(X) \leftrightarrow (BOX96F(X) \land $ \\ 
 $  \Rnext BOX575F(X))) \land $ \\ 
 $ ( \Rnext BOX351P(X) \leftrightarrow (BOX351P(X) \land $ \\ 
 $  \Rnext BOX352P(X))) \land $ \\ 
 $ (BOX637P(X) \leftrightarrow  \Rbox BOX454P(X)) \land $ \\ 
 $ (BOX333P(X) \leftrightarrow  \Rbox E1G17P(X)) \land $ \\ 
 $ ( \Rnext BOX542F(X) \leftrightarrow (BOX542F(X) \land $ \\ 
 $  \Rnext E1G16F(X))) \land $ \\ 
 $ (BOX286P(X) \leftrightarrow  \Rbox E1G7P(X)) \land $ \\ 
 $ ( \Rnext BOX97F(X) \leftrightarrow (BOX97F(X) \land $ \\ 
 $  \Rnext BOX576F(X))) \land $ \\ 
 $ ( \Rnext BOX469P(X) \leftrightarrow (BOX469P(X) \land $ \\ 
 $  \Rnext PinvG11P)) \land $ \\ 
 $ (BOX355P(X) \leftrightarrow  \Rbox DIAMOND291P(X)) \land $ \\ 
 $ (BOX588F(X) \leftrightarrow  \Rbox PinvL1F) \land $ \\ 
 $ (BOX24F(X) \leftrightarrow  \Rbox BOX515F(X)) \land $ \\ 
 $ (BOX623P(X) \leftrightarrow  \Rbox C8P(X)) \land $ \\ 
 $ ( \Rnext BOX384P(X) \leftrightarrow (BOX384P(X) \land $ \\ 
 $  \Rnext BOX385P(X))) \land $ \\ 
 $ (BOX7F(X) \leftrightarrow  \Rbox BOX497F(X)) \land $ \\ 
 $ ( \Rnext BOX314P(X) \leftrightarrow (BOX314P(X) \land $ \\ 
 $  \Rnext  \lnot C13P(X))) \land $ \\ 
 $ ( \Rnext BOX524F(X) \leftrightarrow (BOX524F(X) \land $ \\ 
 $  \Rnext E4G17F(X))) \land $ \\ 
 $ (BOX365P(X) \leftrightarrow  \Rbox E2G5P(X)) \land $ \\ 
 $ (BOX627P(X) \leftrightarrow  \Rbox BOX444P(X)) \land $ \\ 
 $ (BOX640P(X) \leftrightarrow  \Rbox BOX457P(X)) \land $ \\ 
 $ ( \Rnext BOX403P(X) \leftrightarrow (BOX403P(X) \land $ \\ 
 $  \Rnext BOX404P(X))) \land $ \\ 
 $ (BOX2F(X) \leftrightarrow  \Rbox BOX493F(X)) \land $ \\ 
 $ (BOX64F(X) \leftrightarrow  \Rbox BOX548F(X)) \land $ \\ 
 $ (BOX425P(X) \leftrightarrow  \Rbox E5G17P(X)) \land $ \\ 
 $ ( \Rnext BOX501F(X) \leftrightarrow (BOX501F(X) \land $ \\ 
 $  \Rnext E3G11F(X))) \land $ \\ 
 $ (BOX75F(X) \leftrightarrow  \Rbox BOX555F(X)) \land $ \\ 
 $ (BOX23F(X) \leftrightarrow  \Rbox BOX514F(X)) \land $ \\ 
 $ (BOX605F(X) \leftrightarrow  \Rbox PinvG7F) \land $ \\ 
 $ ( \Rnext BOX475P(X) \leftrightarrow (BOX475P(X) \land $ \\ 
 $  \Rnext PG3P)) \land $ \\ 
 $ (BOX143P(X) \leftrightarrow  \Rbox DIAMOND144P(X)) \land $ \\ 
 $ (BOX535F(X) \leftrightarrow  \Rbox DIAMOND250F(X)) \land $ \\ 
 $ (BOX63F(X) \leftrightarrow  \Rbox BOX547F(X)) \land $ \\ 
 $ ( \Rnext BOX90F(X) \leftrightarrow (BOX90F(X) \land $ \\ 
 $  \Rnext BOX569F(X))) \land $ \\ 
 $ ( \Rnext BOX338P(X) \leftrightarrow (BOX338P(X) \land $ \\ 
 $  \Rnext BOX339P(X))) \land $ \\ 
 $ (BOX512F(X) \leftrightarrow  \Rbox C13F(X)) \land $ \\ 
 $ (BOX37F(X) \leftrightarrow  \Rbox BOX528F(X)) \land $ \\ 
 $ ( \Rnext BOX422P(X) \leftrightarrow (BOX422P(X) \land $ \\ 
 $  \Rnext BOX423P(X))) \land $ \\ 
 $ ( \Rnext BOX341P(X) \leftrightarrow (BOX341P(X) \land $ \\ 
 $  \Rnext BOX342P(X))) \land $ \\ 
 $ ( \Rnext BOX483P(X) \leftrightarrow (BOX483P(X) \land $ \\ 
 $  \Rnext PG25P)) \land $ \\ 
 $ (BOX411P(X) \leftrightarrow  \Rbox E1G16P(X)) \land $ \\ 
 $ (BOX61F(X) \leftrightarrow  \Rbox BOX545F(X)) \land $ \\ 
 $ ( \Rnext BOX377P(X) \leftrightarrow (BOX377P(X) \land $ \\ 
 $  \Rnext BOX378P(X))) \land $ \\ 
 $ (BOX19F(X) \leftrightarrow  \Rbox BOX509F(X)) \land $ \\ 
 $ (BOX635P(X) \leftrightarrow  \Rbox BOX452P(X)) \land $ \\ 
 $ ( \Rnext BOX468P(X) \leftrightarrow (BOX468P(X) \land $ \\ 
 $  \Rnext PinvG17P)) \land $ \\ 
 $ ( \Rnext BOX270P(X) \leftrightarrow (BOX270P(X) \land $ \\ 
 $  \Rnext  \lnot E3G11P(X))) \land $ \\ 
 $ ( \Rnext BOX502F(X) \leftrightarrow (BOX502F(X) \land $ \\ 
 $  \Rnext E3G2F(X))) \land $ \\ 
 $ (BOX621P(X) \leftrightarrow  \Rbox (DIAMOND154P(X) \land $ \\ 
 $ DIAMOND301P(X))) \land $ \\ 
 $ ( \Rnext BOX513F(X) \leftrightarrow (BOX513F(X) \land $ \\ 
 $  \Rnext DIAMOND245F(X))) \land $ \\ 
 $ ( \Rnext BOX520F(X) \leftrightarrow (BOX520F(X) \land $ \\ 
 $  \Rnext E1G5F(X))) \land $ \\ 
 $ ( \Rnext BOX368P(X) \leftrightarrow (BOX368P(X) \land $ \\ 
 $  \Rnext BOX287P(X))) \land $ \\ 
 $ (BOX563F(X) \leftrightarrow  \Rbox PG2F) \land $ \\ 
 $ ( \Rnext BOX534F(X) \leftrightarrow (BOX534F(X) \land $ \\ 
 $  \Rnext E2G20F(X))) \land $ \\ 
 $ ( \Rnext BOX120F(X) \leftrightarrow (BOX120F(X) \land $ \\ 
 $  \Rnext BOX599F(X))) \land $ \\ 
 $ ( \Rnext BOX86F(X) \leftrightarrow (BOX86F(X) \land $ \\ 
 $  \Rnext BOX565F(X))) \land $ \\ 
 $ (BOX647P(X) \leftrightarrow  \Rbox BOX464P(X)) \land $ \\ 
 $ ( \Rnext BOX519F(X) \leftrightarrow (BOX519F(X) \land $ \\ 
 $  \Rnext E4G9F(X))) \land $ \\ 
 $ (BOX48F(X) \leftrightarrow  \Rbox BOX240F(X)) \land $ \\ 
 $ (BOX387P(X) \leftrightarrow  \Rbox E2G18P(X)) \land $ \\ 
 $ (BOX77F(X) \leftrightarrow  \Rbox BOX557F(X)) \land $ \\ 
 $ ( \Rnext BOX545F(X) \leftrightarrow (BOX545F(X) \land $ \\ 
 $  \Rnext E3G7F(X))) \land $ \\ 
 $ ( \Rnext BOX99F(X) \leftrightarrow (BOX99F(X) \land $ \\ 
 $  \Rnext BOX578F(X))) \land $ \\ 
 $ ( \Rnext BOX472P(X) \leftrightarrow (BOX472P(X) \land $ \\ 
 $  \Rnext PG16P)) \land $ \\ 
 $ ( \Rnext BOX436P(X) \leftrightarrow (BOX436P(X) \land $ \\ 
 $  \Rnext BOX437P(X))) \land $ \\ 
 $ (BOX570F(X) \leftrightarrow  \Rbox PG28F) \land $ \\ 
 $ ( \Rnext BOX525F(X) \leftrightarrow (BOX525F(X) \land $ \\ 
 $  \Rnext BOX526F(X))) \land $ \\ 
 $ ( \Rnext BOX356P(X) \leftrightarrow (BOX356P(X) \land $ \\ 
 $  \Rnext BOX357P(X))) \land $ \\ 
 $ ( \Rnext BOX539F(X) \leftrightarrow (BOX539F(X) \land $ \\ 
 $  \Rnext BOX540F(X))) \land $ \\ 
 $ (BOX45F(X) \leftrightarrow  \Rbox BOX535F(X)) \land $ \\ 
 $ (BOX60F(X) \leftrightarrow  \Rbox BOX544F(X)) \land $ \\ 
 $ (BOX560F(X) \leftrightarrow  \Rbox PL26F) \land $ \\ 
 $ ( \Rnext BOX104F(X) \leftrightarrow (BOX104F(X) \land $ \\ 
 $  \Rnext BOX583F(X))) \land $ \\ 
 $ ( \Rnext BOX49F(X) \leftrightarrow (BOX49F(X) \land $ \\ 
 $  \Rnext DIAMOND253F(X))) \land $ \\ 
 $ ( \Rnext BOX381P(X) \leftrightarrow (BOX381P(X) \land $ \\ 
 $  \Rnext DIAMOND149P(X))) \land $ \\ 
 $ ( \Rnext BOX109F(X) \leftrightarrow (BOX109F(X) \land $ \\ 
 $  \Rnext BOX588F(X))) \land $ \\ 
 $ ( \Rnext BOX485P(X) \leftrightarrow (BOX485P(X) \land $ \\ 
 $  \Rnext PG12P)) \land $ \\ 
 $ ( \Rnext BOX530F(X) \leftrightarrow (BOX530F(X) \land $ \\ 
 $  \Rnext E2G18F(X))) \land $ \\ 
 $ (BOX52F(X) \leftrightarrow  \Rbox BOX538F(X)) \land $ \\ 
 $ (BOX363P(X) \leftrightarrow  \Rbox E3G4P(X)) \land $ \\ 
 $ (BOX639P(X) \leftrightarrow  \Rbox BOX456P(X)) \land $ \\ 
 $ (BOX652P(X) \leftrightarrow  \Rbox BOX469P(X)) \land $ \\ 
 $ ( \Rnext BOX93F(X) \leftrightarrow (BOX93F(X) \land $ \\ 
 $  \Rnext BOX572F(X))) \land $ \\ 
 $ ( \Rnext BOX117F(X) \leftrightarrow (BOX117F(X) \land $ \\ 
 $  \Rnext BOX596F(X))) \land $ \\ 
 $ (BOX372P(X) \leftrightarrow  \Rbox E1G2P(X)) \land $ \\ 
 $ (BOX645P(X) \leftrightarrow  \Rbox BOX462P(X))) \land $ \\ 
 $ (BOX113F(X) \leftrightarrow BOX658P(X)) \land $ \\ 
 $ (E1G4F(X) \leftrightarrow E1G4P(X)) \land $ \\ 
 $ (DIAMOND195F(X) \leftrightarrow DIAMOND145P(X)) \land $ \\ 
 $ (PinvG14F \leftrightarrow PinvG14P) \land $ \\ 
 $ (E1L1InvF(X) \leftrightarrow E1L1InvP(X)) \land $ \\ 
 $ (PG18F \leftrightarrow PG18P) \land $ \\ 
 $ (BOX592F(X) \leftrightarrow BOX475P(X)) \land $ \\ 
 $ (BOX506F(X) \leftrightarrow BOX342P(X)) \land $ \\ 
 $ (E1G16InvF(X) \leftrightarrow E1G16InvP(X)) \land $ \\ 
 $ (E1G20F(X) \leftrightarrow E1G20P(X)) \land $ \\ 
 $ (BOX563F(X) \leftrightarrow BOX446P(X)) \land $ \\ 
 $ (BOX547F(X) \leftrightarrow BOX421P(X)) \land $ \\ 
 $ (BOX231F(X) \leftrightarrow BOX275P(X)) \land $ \\ 
 $ (BOX603F(X) \leftrightarrow BOX486P(X)) \land $ \\ 
 $ (DIAMOND197F(X) \leftrightarrow DIAMOND148P(X)) \land $ \\ 
 $ (PinvG5F \leftrightarrow PinvG5P) \land $ \\ 
 $ (BOX582F(X) \leftrightarrow BOX465P(X)) \land $ \\ 
 $ (BOX573F(X) \leftrightarrow BOX456P(X)) \land $ \\ 
 $ (BOX5F(X) \leftrightarrow BOX613P(X)) \land $ \\ 
 $ (BOX533F(X) \leftrightarrow BOX393P(X)) \land $ \\ 
 $ (E1L26InvF(X) \leftrightarrow E1L26InvP(X)) \land $ \\ 
 $ (BOX518F(X) \leftrightarrow BOX365P(X)) \land $ \\ 
 $ (PinvG28F \leftrightarrow PinvG28P) \land $ \\ 
 $ (BOX117F(X) \leftrightarrow BOX662P(X)) \land $ \\ 
 $ (PinvG12F \leftrightarrow PinvG12P) \land $ \\ 
 $ (BOX576F(X) \leftrightarrow BOX459P(X)) \land $ \\ 
 $ (E4G12F(X) \leftrightarrow E4G12P(X)) \land $ \\ 
 $ (DIAMOND66F(X) \leftrightarrow DIAMOND308P(X)) \land $ \\ 
 $ (BOX70F(X) \leftrightarrow BOX426P(X)) \land $ \\ 
 $ (BOX586F(X) \leftrightarrow BOX469P(X)) \land $ \\ 
 $ (BOX101F(X) \leftrightarrow BOX646P(X)) \land $ \\ 
 $ (BOX254F(X) \leftrightarrow BOX300P(X)) \land $ \\ 
 $ (E1G5InvF(X) \leftrightarrow E1G5InvP(X)) \land $ \\ 
 $ (BOX599F(X) \leftrightarrow BOX482P(X)) \land $ \\ 
 $ (PinvG8F \leftrightarrow PinvG8F) \land $ \\ 
 $ (PG4F \leftrightarrow PG4F) \land $ \\ 
 $ (BOX600F(X) \leftrightarrow BOX483P(X)) \land $ \\ 
 $ (C14F(X) \leftrightarrow C14P(X)) \land $ \\ 
 $ (C10F(X) \leftrightarrow C10P(X)) \land $ \\ 
 $ (BOX72F(X) \leftrightarrow BOX624P(X)) \land $ \\ 
 $ (BOX55F(X) \leftrightarrow BOX407P(X)) \land $ \\ 
 $ (BOX90F(X) \leftrightarrow BOX635P(X)) \land $ \\ 
 $ (BOX565F(X) \leftrightarrow BOX448P(X)) \land $ \\ 
 $ (BOX607F(X) \leftrightarrow BOX490P(X)) \land $ \\ 
 $ (DIAMOND210F(X) \leftrightarrow DIAMOND164P(X)) \land $ \\ 
 $ (BOX499F(X) \leftrightarrow BOX331P(X)) \land $ \\ 
 $ (DIAMOND229F(X) \leftrightarrow DIAMOND272P(X)) \land $ \\ 
 $ (BOX76F(X) \leftrightarrow BOX436P(X)) \land $ \\ 
 $ (BOX108F(X) \leftrightarrow BOX653P(X)) \land $ \\ 
 $ (BOX260F(X) \leftrightarrow BOX309P(X)) \land $ \\ 
 $ (BOX99F(X) \leftrightarrow BOX644P(X)) \land $ \\ 
 $ (E1G28InvF(X) \leftrightarrow E1G28InvP(X)) \land $ \\ 
 $ (BOX557F(X) \leftrightarrow BOX439P(X)) \land $ \\ 
 $ (BOX532F(X) \leftrightarrow BOX391P(X)) \land $ \\ 
 $ (PinvG2F \leftrightarrow PinvG2F) \land $ \\ 
 $ (BOX114F(X) \leftrightarrow BOX659P(X)) \land $ \\ 
 $ (DIAMOND53F(X) \leftrightarrow DIAMOND302P(X)) \land $ \\ 
 $ (PG3F \leftrightarrow PG3F) \land $ \\ 
 $ (BOX606F(X) \leftrightarrow BOX489P(X)) \land $ \\ 
 $ (C17F(X) \leftrightarrow C17P(X)) \land $ \\ 
 $ (BOX109F(X) \leftrightarrow BOX654P(X)) \land $ \\ 
 $ (PG11F \leftrightarrow PG11P) \land $ \\ 
 $ (DIAMOND245F(X) \leftrightarrow DIAMOND291P(X)) \land $ \\ 
 $ (E3G27F(X) \leftrightarrow E3G27P(X)) \land $ \\ 
 $ (DIAMOND65F(X) \leftrightarrow DIAMOND162P(X)) \land $ \\ 
 $ (C21F(X) \leftrightarrow C21P(X)) \land $ \\ 
 $ (C13F(X) \leftrightarrow C13P(X)) \land $ \\ 
 $ (BOX42F(X) \leftrightarrow BOX392P(X)) \land $ \\ 
 $ (E4G9F(X) \leftrightarrow E4G9P(X)) \land $ \\ 
 $ (BOX602F(X) \leftrightarrow BOX485P(X)) \land $ \\ 
 $ (PG17F \leftrightarrow PG17P) \land $ \\ 
 $ (E2G20F(X) \leftrightarrow E2G20P(X)) \land $ \\ 
 $ (E3G25F(X) \leftrightarrow E3G25P(X)) \land $ \\ 
 $ (PinvG3F \leftrightarrow PinvG3F) \land $ \\ 
 $ (E1L29InvF(X) \leftrightarrow E1L29InvP(X)) \land $ \\ 
 $ (E1G14F(X) \leftrightarrow E1G14P(X)) \land $ \\ 
 $ (BOX579F(X) \leftrightarrow BOX462P(X)) \land $ \\ 
 $ (BOX546F(X) \leftrightarrow BOX419P(X)) \land $ \\ 
 $ (PinvG4F \leftrightarrow PinvG4P) \land $ \\ 
 $ (BOX16F(X) \leftrightarrow BOX343P(X)) \land $ \\ 
 $ (E3G18F(X) \leftrightarrow E3G18P(X)) \land $ \\ 
 $ (BOX47F(X) \leftrightarrow BOX398P(X)) \land $ \\ 
 $ (BOX34F(X) \leftrightarrow BOX377P(X)) \land $ \\ 
 $ (BOX541F(X) \leftrightarrow BOX409P(X)) \land $ \\ 
 $ (C6F(X) \leftrightarrow C6P(X)) \land $ \\ 
 $ (DIAMOND187F(X) \leftrightarrow DIAMOND136P(X)) \land $ \\ 
 $ (PinvL1F \leftrightarrow PinvL1P) \land $ \\ 
 $ (PG2F \leftrightarrow PG2F) \land $ \\ 
 $ (E1G3InvF(X) \leftrightarrow E1G3InvP(X)) \land $ \\ 
 $ (BOX121F(X) \leftrightarrow BOX666P(X)) \land $ \\ 
 $ (BOX92F(X) \leftrightarrow BOX637P(X)) \land $ \\ 
 $ (PG9F \leftrightarrow PG9P) \land $ \\ 
 $ (PinvG27F \leftrightarrow PinvG27P) \land $ \\ 
 $ (BOX220F(X) \leftrightarrow BOX175P(X)) \land $ \\ 
 $ (BOX237F(X) \leftrightarrow BOX283P(X)) \land $ \\ 
 $ (BOX577F(X) \leftrightarrow BOX460P(X)) \land $ \\ 
 $ (BOX552F(X) \leftrightarrow BOX430P(X)) \land $ \\ 
 $ (DIAMOND198F(X) \leftrightarrow DIAMOND149P(X)) \land $ \\ 
 $ (BOX491F(X) \leftrightarrow BOX319P(X)) \land $ \\ 
 $ (PinvG25F \leftrightarrow PinvG25F) \land $ \\ 
 $ (BOX572F(X) \leftrightarrow BOX455P(X)) \land $ \\ 
 $ (BOX598F(X) \leftrightarrow BOX481P(X)) \land $ \\ 
 $ (C16F(X) \leftrightarrow C16P(X)) \land $ \\ 
 $ (BOX93F(X) \leftrightarrow BOX638P(X)) \land $ \\ 
 $ (DIAMOND205F(X) \leftrightarrow DIAMOND157P(X)) \land $ \\ 
 $ (DIAMOND257F(X) \leftrightarrow DIAMOND305P(X)) \land $ \\ 
 $ (PG12F \leftrightarrow PG12P) \land $ \\ 
 $ (E4G4F(X) \leftrightarrow E4G4P(X)) \land $ \\ 
 $ (PinvG27F \leftrightarrow PinvG27F) \land $ \\ 
 $ (BOX246F(X) \leftrightarrow BOX292P(X)) \land $ \\ 
 $ (BOX69F(X) \leftrightarrow BOX623P(X)) \land $ \\ 
 $ (BOX118F(X) \leftrightarrow BOX663P(X)) \land $ \\ 
 $ (E1L1F(X) \leftrightarrow E1L1P(X)) \land $ \\ 
 $ (BOX495F(X) \leftrightarrow BOX326P(X)) \land $ \\ 
 $ (E1G12F(X) \leftrightarrow E1G12P(X)) \land $ \\ 
 $ (BOX593F(X) \leftrightarrow BOX476P(X)) \land $ \\ 
 $ (PinvG29F \leftrightarrow PinvG29F) \land $ \\ 
 $ (BOX492F(X) \leftrightarrow BOX320P(X)) \land $ \\ 
 $ (BOX584F(X) \leftrightarrow BOX467P(X)) \land $ \\ 
 $ (DIAMOND211F(X) \leftrightarrow DIAMOND165P(X)) \land $ \\ 
 $ (BOX184F(X) \leftrightarrow BOX132P(X)) \land $ \\ 
 $ (BOX265F(X) \leftrightarrow BOX314P(X)) \land $ \\ 
 $ (DIAMOND250F(X) \leftrightarrow DIAMOND296P(X)) \land $ \\ 
 $ (E1G27InvF(X) \leftrightarrow E1G27InvP(X)) \land $ \\ 
 $ (BOX29F(X) \leftrightarrow BOX368P(X)) \land $ \\ 
 $ (PinvG16F \leftrightarrow PinvG16P) \land $ \\ 
 $ (BOX57F(X) \leftrightarrow BOX410P(X)) \land $ \\ 
 $ (DIAMOND261F(X) \leftrightarrow DIAMOND310P(X)) \land $ \\ 
 $ (BOX61F(X) \leftrightarrow BOX416P(X)) \land $ \\ 
 $ (BOX501F(X) \leftrightarrow BOX335P(X)) \land $ \\ 
 $ (PinvL29F \leftrightarrow PinvL29F) \land $ \\ 
 $ (DIAMOND217F(X) \leftrightarrow DIAMOND171P(X)) \land $ \\ 
 $ (BOX192F(X) \leftrightarrow BOX141P(X)) \land $ \\ 
 $ (BOX107F(X) \leftrightarrow BOX652P(X)) \land $ \\ 
 $ (BOX98F(X) \leftrightarrow BOX643P(X)) \land $ \\ 
 $ (C25F(X) \leftrightarrow C25P(X)) \land $ \\ 
 $ (BOX569F(X) \leftrightarrow BOX452P(X)) \land $ \\ 
 $ (PinvG23F \leftrightarrow PinvG23P) \land $ \\ 
 $ (BOX33F(X) \leftrightarrow BOX375P(X)) \land $ \\ 
 $ (C1F(X) \leftrightarrow C1P(X)) \land $ \\ 
 $ (BOX609F(X) \leftrightarrow BOX617P(X)) \land $ \\ 
 $ (DIAMOND8F(X) \leftrightarrow DIAMOND276P(X)) \land $ \\ 
 $ (BOX126F(X) \leftrightarrow BOX671P(X)) \land $ \\ 
 $ (BOX12F(X) \leftrightarrow BOX336P(X)) \land $ \\ 
 $ (BOX536F(X) \leftrightarrow BOX399P(X)) \land $ \\ 
 $ (BOX19F(X) \leftrightarrow BOX348P(X)) \land $ \\ 
 $ (E1G4InvF(X) \leftrightarrow E1G4InvP(X)) \land $ \\ 
 $ (BOX575F(X) \leftrightarrow BOX458P(X)) \land $ \\ 
 $ (PG25F \leftrightarrow PG25F) \land $ \\ 
 $ (BOX71F(X) \leftrightarrow BOX428P(X)) \land $ \\ 
 $ (E2G5F(X) \leftrightarrow E2G5P(X)) \land $ \\ 
 $ (BOX610F(X) \leftrightarrow BOX620P(X)) \land $ \\ 
 $ (BOX39F(X) \leftrightarrow BOX386P(X)) \land $ \\ 
 $ (DIAMOND244F(X) \leftrightarrow DIAMOND290P(X)) \land $ \\ 
 $ (E2G18F(X) \leftrightarrow E2G18P(X)) \land $ \\ 
 $ (BOX583F(X) \leftrightarrow BOX466P(X)) \land $ \\ 
 $ (PG11F \leftrightarrow PG11F) \land $ \\ 
 $ (DIAMOND9F(X) \leftrightarrow DIAMOND131P(X)) \land $ \\ 
 $ (PinvG4F \leftrightarrow PinvG4F) \land $ \\ 
 $ (DIAMOND236F(X) \leftrightarrow DIAMOND281P(X)) \land $ \\ 
 $ (DIAMOND258F(X) \leftrightarrow DIAMOND306P(X)) \land $ \\ 
 $ (DIAMOND212F(X) \leftrightarrow DIAMOND166P(X)) \land $ \\ 
 $ (PG20F \leftrightarrow PG20F) \land $ \\ 
 $ (BOX56F(X) \leftrightarrow BOX408P(X)) \land $ \\ 
 $ (E3G11F(X) \leftrightarrow E3G11P(X)) \land $ \\ 
 $ (PinvG7F \leftrightarrow PinvG7F) \land $ \\ 
 $ (BOX196F(X) \leftrightarrow BOX146P(X)) \land $ \\ 
 $ (BOX601F(X) \leftrightarrow BOX484P(X)) \land $ \\ 
 $ (BOX497F(X) \leftrightarrow BOX329P(X)) \land $ \\ 
 $ (PG23F \leftrightarrow PG23P) \land $ \\ 
 $ (PinvG19F \leftrightarrow PinvG19P) \land $ \\ 
 $ (BOX591F(X) \leftrightarrow BOX474P(X)) \land $ \\ 
 $ (DIAMOND208F(X) \leftrightarrow DIAMOND161P(X)) \land $ \\ 
 $ (BOX199F(X) \leftrightarrow BOX150P(X)) \land $ \\ 
 $ (E5G17F(X) \leftrightarrow E5G17P(X)) \land $ \\ 
 $ (BOX500F(X) \leftrightarrow BOX333P(X)) \land $ \\ 
 $ (BOX64F(X) \leftrightarrow BOX422P(X)) \land $ \\ 
 $ (BOX504F(X) \leftrightarrow BOX340P(X)) \land $ \\ 
 $ (BOX23F(X) \leftrightarrow BOX356P(X)) \land $ \\ 
 $ (BOX32F(X) \leftrightarrow BOX373P(X)) \land $ \\ 
 $ (BOX544F(X) \leftrightarrow BOX415P(X)) \land $ \\ 
 $ (C19F(X) \leftrightarrow C19P(X)) \land $ \\ 
 $ (E1G2InvF(X) \leftrightarrow E1G2InvP(X)) \land $ \\ 
 $ (DIAMOND234F(X) \leftrightarrow DIAMOND279P(X)) \land $ \\ 
 $ (BOX551F(X) \leftrightarrow BOX429P(X)) \land $ \\ 
 $ (BOX241F(X) \leftrightarrow BOX287P(X)) \land $ \\ 
 $ (DIAMOND255F(X) \leftrightarrow DIAMOND301P(X)) \land $ \\ 
 $ (BOX590F(X) \leftrightarrow BOX473P(X)) \land $ \\ 
 $ (DIAMOND219F(X) \leftrightarrow DIAMOND174P(X)) \land $ \\ 
 $ (DIAMOND209F(X) \leftrightarrow DIAMOND163P(X)) \land $ \\ 
 $ (BOX531F(X) \leftrightarrow BOX389P(X)) \land $ \\ 
 $ (DIAMOND21F(X) \leftrightarrow DIAMOND142P(X)) \land $ \\ 
 $ (DIAMOND35F(X) \leftrightarrow DIAMOND147P(X)) \land $ \\ 
 $ (BOX124F(X) \leftrightarrow BOX669P(X)) \land $ \\ 
 $ (BOX26F(X) \leftrightarrow BOX362P(X)) \land $ \\ 
 $ (C23F(X) \leftrightarrow C23P(X)) \land $ \\ 
 $ (BOX41F(X) \leftrightarrow BOX390P(X)) \land $ \\ 
 $ (PG14F \leftrightarrow PG14F) \land $ \\ 
 $ (BOX604F(X) \leftrightarrow BOX487P(X)) \land $ \\ 
 $ (PinvG2F \leftrightarrow PinvG2P) \land $ \\ 
 $ (C4F(X) \leftrightarrow C4P(X)) \land $ \\ 
 $ (E1G9F(X) \leftrightarrow E1G9P(X)) \land $ \\ 
 $ (PinvG5F \leftrightarrow PinvG5F) \land $ \\ 
 $ (PG5F \leftrightarrow PG5F) \land $ \\ 
 $ (PG7F \leftrightarrow PG7P) \land $ \\ 
 $ (E1G28F(X) \leftrightarrow E1G28P(X)) \land $ \\ 
 $ (PinvG25F \leftrightarrow PinvG25P) \land $ \\ 
 $ (DIAMOND203F(X) \leftrightarrow DIAMOND155P(X)) \land $ \\ 
 $ (BOX560F(X) \leftrightarrow BOX443P(X)) \land $ \\ 
 $ (DIAMOND200F(X) \leftrightarrow DIAMOND151P(X)) \land $ \\ 
 $ (BOX510F(X) \leftrightarrow BOX350P(X)) \land $ \\ 
 $ (DIAMOND267F(X) \leftrightarrow DIAMOND316P(X)) \land $ \\ 
 $ (C28F(X) \leftrightarrow C28P(X)) \land $ \\ 
 $ (BOX519F(X) \leftrightarrow BOX367P(X)) \land $ \\ 
 $ (BOX122F(X) \leftrightarrow BOX667P(X)) \land $ \\ 
 $ (BOX11F(X) \leftrightarrow BOX334P(X)) \land $ \\ 
 $ (BOX91F(X) \leftrightarrow BOX636P(X)) \land $ \\ 
 $ (C8F(X) \leftrightarrow C8P(X)) \land $ \\ 
 $ (C11F(X) \leftrightarrow C11P(X)) \land $ \\ 
 $ (PinvG9F \leftrightarrow PinvG9P) \land $ \\ 
 $ (PG12F \leftrightarrow PG12F) \land $ \\ 
 $ (BOX1F(X) \leftrightarrow BOX612P(X)) \land $ \\ 
 $ (PinvG7F \leftrightarrow PinvG7P) \land $ \\ 
 $ (DIAMOND230F(X) \leftrightarrow DIAMOND273P(X)) \land $ \\ 
 $ (DIAMOND263F(X) \leftrightarrow DIAMOND312P(X)) \land $ \\ 
 $ (E2G29F(X) \leftrightarrow E2G29P(X)) \land $ \\ 
 $ (BOX89F(X) \leftrightarrow BOX634P(X)) \land $ \\ 
 $ (DIAMOND191F(X) \leftrightarrow DIAMOND140P(X)) \land $ \\ 
 $ (BOX558F(X) \leftrightarrow BOX440P(X)) \land $ \\ 
 $ (E4G14F(X) \leftrightarrow E4G14P(X)) \land $ \\ 
 $ (PG16F \leftrightarrow PG16F) \land $ \\ 
 $ (BOX4F(X) \leftrightarrow BOX325P(X)) \land $ \\ 
 $ (BOX190F(X) \leftrightarrow BOX139P(X)) \land $ \\ 
 $ (BOX125F(X) \leftrightarrow BOX670P(X)) \land $ \\ 
 $ (PG9F \leftrightarrow PG9F) \land $ \\ 
 $ (PinvG17F \leftrightarrow PinvG17P) \land $ \\ 
 $ (BOX95F(X) \leftrightarrow BOX640P(X)) \land $ \\ 
 $ (BOX38F(X) \leftrightarrow BOX384P(X)) \land $ \\ 
 $ (BOX119F(X) \leftrightarrow BOX664P(X)) \land $ \\ 
 $ (E1G25F(X) \leftrightarrow E1G25P(X)) \land $ \\ 
 $ (BOX508F(X) \leftrightarrow BOX346P(X)) \land $ \\ 
 $ (BOX106F(X) \leftrightarrow BOX651P(X)) \land $ \\ 
 $ (BOX88F(X) \leftrightarrow BOX633P(X)) \land $ \\ 
 $ (DIAMOND204F(X) \leftrightarrow DIAMOND156P(X)) \land $ \\ 
 $ (BOX49F(X) \leftrightarrow BOX618P(X)) \land $ \\ 
 $ (BOX585F(X) \leftrightarrow BOX468P(X)) \land $ \\ 
 $ (BOX67F(X) \leftrightarrow BOX424P(X)) \land $ \\ 
 $ (BOX77F(X) \leftrightarrow BOX438P(X)) \land $ \\ 
 $ (BOX13F(X) \leftrightarrow BOX338P(X)) \land $ \\ 
 $ (BOX529F(X) \leftrightarrow BOX385P(X)) \land $ \\ 
 $ (BOX535F(X) \leftrightarrow BOX397P(X)) \land $ \\ 
 $ (BOX248F(X) \leftrightarrow BOX294P(X)) \land $ \\ 
 $ (E1G18F(X) \leftrightarrow E1G18P(X)) \land $ \\ 
 $ (PG23F \leftrightarrow PG23F) \land $ \\ 
 $ (BOX571F(X) \leftrightarrow BOX454P(X)) \land $ \\ 
 $ (PinvG20F \leftrightarrow PinvG20F) \land $ \\ 
 $ (PG20F \leftrightarrow PG20P) \land $ \\ 
 $ (BOX63F(X) \leftrightarrow BOX420P(X)) \land $ \\ 
 $ (BOX102F(X) \leftrightarrow BOX647P(X)) \land $ \\ 
 $ (DIAMOND14F(X) \leftrightarrow DIAMOND135P(X)) \land $ \\ 
 $ (BOX43F(X) \leftrightarrow BOX394P(X)) \land $ \\ 
 $ (BOX80F(X) \leftrightarrow BOX441P(X)) \land $ \\ 
 $ (BOX580F(X) \leftrightarrow BOX463P(X)) \land $ \\ 
 $ (BOX581F(X) \leftrightarrow BOX464P(X)) \land $ \\ 
 $ (PG27F \leftrightarrow PG27P) \land $ \\ 
 $ (BOX517F(X) \leftrightarrow BOX363P(X)) \land $ \\ 
 $ (BOX112F(X) \leftrightarrow BOX657P(X)) \land $ \\ 
 $ (BOX45F(X) \leftrightarrow BOX396P(X)) \land $ \\ 
 $ (PG29F \leftrightarrow PG29P) \land $ \\ 
 $ (DIAMOND242F(X) \leftrightarrow DIAMOND288P(X)) \land $ \\ 
 $ (E1G23F(X) \leftrightarrow E1G23P(X)) \land $ \\ 
 $ (PinvG16F \leftrightarrow PinvG16F) \land $ \\ 
 $ (PinvG14F \leftrightarrow PinvG14F) \land $ \\ 
 $ (BOX116F(X) \leftrightarrow BOX661P(X)) \land $ \\ 
 $ (PinvG17F \leftrightarrow PinvG17F) \land $ \\ 
 $ (BOX554F(X) \leftrightarrow BOX433P(X)) \land $ \\ 
 $ (PG7F \leftrightarrow PG7F) \land $ \\ 
 $ (E2G9F(X) \leftrightarrow E2G9P(X)) \land $ \\ 
 $ (PG25F \leftrightarrow PG25P) \land $ \\ 
 $ (BOX110F(X) \leftrightarrow BOX655P(X)) \land $ \\ 
 $ (PG8F \leftrightarrow PG8P) \land $ \\ 
 $ (E1L15F(X) \leftrightarrow E1L15P(X)) \land $ \\ 
 $ (BOX515F(X) \leftrightarrow BOX359P(X)) \land $ \\ 
 $ (DIAMOND224F(X) \leftrightarrow DIAMOND179P(X)) \land $ \\ 
 $ (PinvG11F \leftrightarrow PinvG11P) \land $ \\ 
 $ (BOX556F(X) \leftrightarrow BOX437P(X)) \land $ \\ 
 $ (BOX105F(X) \leftrightarrow BOX650P(X)) \land $ \\ 
 $ (BOX74F(X) \leftrightarrow BOX432P(X)) \land $ \\ 
 $ (PinvG9F \leftrightarrow PinvG9F) \land $ \\ 
 $ (PinvL15F \leftrightarrow PinvL15F) \land $ \\ 
 $ (PinvG19F \leftrightarrow PinvG19F) \land $ \\ 
 $ (PL15F \leftrightarrow PL15F) \land $ \\ 
 $ (PG14F \leftrightarrow PG14P) \land $ \\ 
 $ (BOX225F(X) \leftrightarrow BOX181P(X)) \land $ \\ 
 $ (BOX259F(X) \leftrightarrow BOX307P(X)) \land $ \\ 
 $ (BOX97F(X) \leftrightarrow BOX642P(X)) \land $ \\ 
 $ (PL29F \leftrightarrow PL29P) \land $ \\ 
 $ (BOX2F(X) \leftrightarrow BOX321P(X)) \land $ \\ 
 $ (BOX539F(X) \leftrightarrow BOX405P(X)) \land $ \\ 
 $ (BOX227F(X) \leftrightarrow BOX270P(X)) \land $ \\ 
 $ (BOX31F(X) \leftrightarrow BOX371P(X)) \land $ \\ 
 $ (BOX507F(X) \leftrightarrow BOX344P(X)) \land $ \\ 
 $ (BOX594F(X) \leftrightarrow BOX477P(X)) \land $ \\ 
 $ (E1G8F(X) \leftrightarrow E1G8P(X)) \land $ \\ 
 $ (PG3F \leftrightarrow PG3P) \land $ \\ 
 $ (BOX20F(X) \leftrightarrow BOX351P(X)) \land $ \\ 
 $ (PinvG3F \leftrightarrow PinvG3P) \land $ \\ 
 $ (BOX100F(X) \leftrightarrow BOX645P(X)) \land $ \\ 
 $ (BOX553F(X) \leftrightarrow BOX431P(X)) \land $ \\ 
 $ (DIAMOND252F(X) \leftrightarrow DIAMOND298P(X)) \land $ \\ 
 $ (E1G11F(X) \leftrightarrow E1G11P(X)) \land $ \\ 
 $ (E1G27F(X) \leftrightarrow E1G27P(X)) \land $ \\ 
 $ (BOX549F(X) \leftrightarrow BOX425P(X)) \land $ \\ 
 $ (DIAMOND253F(X) \leftrightarrow DIAMOND299P(X)) \land $ \\ 
 $ (E5G4F(X) \leftrightarrow E5G4P(X)) \land $ \\ 
 $ (BOX524F(X) \leftrightarrow BOX378P(X)) \land $ \\ 
 $ (BOX104F(X) \leftrightarrow BOX649P(X)) \land $ \\ 
 $ (BOX123F(X) \leftrightarrow BOX668P(X)) \land $ \\ 
 $ (DIAMOND188F(X) \leftrightarrow DIAMOND137P(X)) \land $ \\ 
 $ (E1G29InvF(X) \leftrightarrow E1G29InvP(X)) \land $ \\ 
 $ (BOX567F(X) \leftrightarrow BOX450P(X)) \land $ \\ 
 $ (BOX578F(X) \leftrightarrow BOX461P(X)) \land $ \\ 
 $ (BOX128F(X) \leftrightarrow BOX673P(X)) \land $ \\ 
 $ (DIAMOND251F(X) \leftrightarrow DIAMOND297P(X)) \land $ \\ 
 $ (E1G7F(X) \leftrightarrow E1G7P(X)) \land $ \\ 
 $ (BOX40F(X) \leftrightarrow BOX388P(X)) \land $ \\ 
 $ (BOX81F(X) \leftrightarrow BOX626P(X)) \land $ \\ 
 $ (E5G2F(X) \leftrightarrow E5G2P(X)) \land $ \\ 
 $ (BOX103F(X) \leftrightarrow BOX648P(X)) \land $ \\ 
 $ (PinvL29F \leftrightarrow PinvL29P) \land $ \\ 
 $ (DIAMOND235F(X) \leftrightarrow DIAMOND280P(X)) \land $ \\ 
 $ (DIAMOND228F(X) \leftrightarrow DIAMOND271P(X)) \land $ \\ 
 $ (BOX543F(X) \leftrightarrow BOX413P(X)) \land $ \\ 
 $ (BOX232F(X) \leftrightarrow BOX277P(X)) \land $ \\ 
 $ (E1G29F(X) \leftrightarrow E1G29P(X)) \land $ \\ 
 $ (BOX94F(X) \leftrightarrow BOX639P(X)) \land $ \\ 
 $ (PG29F \leftrightarrow PG29F) \land $ \\ 
 $ (E2L29F(X) \leftrightarrow E2L29P(X)) \land $ \\ 
 $ (DIAMOND216F(X) \leftrightarrow DIAMOND170P(X)) \land $ \\ 
 $ (BOX25F(X) \leftrightarrow BOX360P(X)) \land $ \\ 
 $ (BOX568F(X) \leftrightarrow BOX451P(X)) \land $ \\ 
 $ (C12F(X) \leftrightarrow C12P(X)) \land $ \\ 
 $ (BOX570F(X) \leftrightarrow BOX453P(X)) \land $ \\ 
 $ (BOX522F(X) \leftrightarrow BOX374P(X)) \land $ \\ 
 $ (BOX587F(X) \leftrightarrow BOX470P(X)) \land $ \\ 
 $ (BOX60F(X) \leftrightarrow BOX414P(X)) \land $ \\ 
 $ (DIAMOND15F(X) \leftrightarrow DIAMOND282P(X)) \land $ \\ 
 $ (BOX240F(X) \leftrightarrow BOX286P(X)) \land $ \\ 
 $ (DIAMOND207F(X) \leftrightarrow DIAMOND160P(X)) \land $ \\ 
 $ (PG19F \leftrightarrow PG19F) \land $ \\ 
 $ (E1L15InvF(X) \leftrightarrow E1L15InvP(X)) \land $ \\ 
 $ (E1G17F(X) \leftrightarrow E1G17P(X)) \land $ \\ 
 $ (BOX498F(X) \leftrightarrow BOX330P(X)) \land $ \\ 
 $ (DIAMOND268F(X) \leftrightarrow DIAMOND317P(X)) \land $ \\ 
 $ (DIAMOND243F(X) \leftrightarrow DIAMOND289P(X)) \land $ \\ 
 $ (DIAMOND226F(X) \leftrightarrow DIAMOND269P(X)) \land $ \\ 
 $ (BOX564F(X) \leftrightarrow BOX447P(X)) \land $ \\ 
 $ (BOX22F(X) \leftrightarrow BOX353P(X)) \land $ \\ 
 $ (BOX3F(X) \leftrightarrow BOX323P(X)) \land $ \\ 
 $ (BOX494F(X) \leftrightarrow BOX324P(X)) \land $ \\ 
 $ (BOX534F(X) \leftrightarrow BOX395P(X)) \land $ \\ 
 $ (E1G17InvF(X) \leftrightarrow E1G17InvP(X)) \land $ \\ 
 $ (E1G3F(X) \leftrightarrow E1G3P(X)) \land $ \\ 
 $ (PinvL15F \leftrightarrow PinvL15P) \land $ \\ 
 $ (E1G18InvF(X) \leftrightarrow E1G18InvP(X)) \land $ \\ 
 $ (BOX537F(X) \leftrightarrow BOX402P(X)) \land $ \\ 
 $ (PL26F \leftrightarrow PL26P) \land $ \\ 
 $ (E5G29F(X) \leftrightarrow E5G29P(X)) \land $ \\ 
 $ (E1G14InvF(X) \leftrightarrow E1G14InvP(X)) \land $ \\ 
 $ (PinvG23F \leftrightarrow PinvG23F) \land $ \\ 
 $ (DIAMOND54F(X) \leftrightarrow DIAMOND304P(X)) \land $ \\ 
 $ (DIAMOND73F(X) \leftrightarrow DIAMOND173P(X)) \land $ \\ 
 $ (BOX589F(X) \leftrightarrow BOX472P(X)) \land $ \\ 
 $ (PL26F \leftrightarrow PL26F) \land $ \\ 
 $ (PG2F \leftrightarrow PG2P) \land $ \\ 
 $ (DIAMOND183F(X) \leftrightarrow DIAMOND130P(X)) \land $ \\ 
 $ (BOX512F(X) \leftrightarrow BOX354P(X)) \land $ \\ 
 $ (E4G17F(X) \leftrightarrow E4G17P(X)) \land $ \\ 
 $ (DIAMOND194F(X) \leftrightarrow DIAMOND144P(X)) \land $ \\ 
 $ (E1G23InvF(X) \leftrightarrow E1G23InvP(X)) \land $ \\ 
 $ (BOX48F(X) \leftrightarrow BOX400P(X)) \land $ \\ 
 $ (E1G8InvF(X) \leftrightarrow E1G8InvP(X)) \land $ \\ 
 $ (BOX96F(X) \leftrightarrow BOX641P(X)) \land $ \\ 
 $ (PinvG20F \leftrightarrow PinvG20P) \land $ \\ 
 $ (E1G11InvF(X) \leftrightarrow E1G11InvP(X)) \land $ \\ 
 $ (DIAMOND213F(X) \leftrightarrow DIAMOND167P(X)) \land $ \\ 
 $ (E1G9InvF(X) \leftrightarrow E1G9InvP(X)) \land $ \\ 
 $ (DIAMOND44F(X) \leftrightarrow DIAMOND152P(X)) \land $ \\ 
 $ (E1G19InvF(X) \leftrightarrow E1G19InvP(X)) \land $ \\ 
 $ (BOX24F(X) \leftrightarrow BOX358P(X)) \land $ \\ 
 $ (BOX525F(X) \leftrightarrow BOX379P(X)) \land $ \\ 
 $ (BOX52F(X) \leftrightarrow BOX403P(X)) \land $ \\ 
 $ (BOX561F(X) \leftrightarrow BOX444P(X)) \land $ \\ 
 $ (DIAMOND247F(X) \leftrightarrow DIAMOND293P(X)) \land $ \\ 
 $ (E4L1F(X) \leftrightarrow E4L1P(X)) \land $ \\ 
 $ (PinvG29F \leftrightarrow PinvG29P) \land $ \\ 
 $ (C18F(X) \leftrightarrow C18P(X)) \land $ \\ 
 $ (BOX550F(X) \leftrightarrow BOX427P(X)) \land $ \\ 
 $ (BOX516F(X) \leftrightarrow BOX361P(X)) \land $ \\ 
 $ (BOX545F(X) \leftrightarrow BOX417P(X)) \land $ \\ 
 $ (DIAMOND266F(X) \leftrightarrow DIAMOND315P(X)) \land $ \\ 
 $ (E1G25InvF(X) \leftrightarrow E1G25InvP(X)) \land $ \\ 
 $ (DIAMOND185F(X) \leftrightarrow DIAMOND133P(X)) \land $ \\ 
 $ (BOX68F(X) \leftrightarrow BOX622P(X)) \land $ \\ 
 $ (DIAMOND233F(X) \leftrightarrow DIAMOND278P(X)) \land $ \\ 
 $ (PinvG18F \leftrightarrow PinvG18P) \land $ \\ 
 $ (PinvL26F \leftrightarrow PinvL26P) \land $ \\ 
 $ (BOX528F(X) \leftrightarrow BOX383P(X)) \land $ \\ 
 $ (BOX530F(X) \leftrightarrow BOX387P(X)) \land $ \\ 
 $ (PinvG28F \leftrightarrow PinvG28F) \land $ \\ 
 $ (BOX78F(X) \leftrightarrow BOX625P(X)) \land $ \\ 
 $ (BOX62F(X) \leftrightarrow BOX418P(X)) \land $ \\ 
 $ (BOX595F(X) \leftrightarrow BOX478P(X)) \land $ \\ 
 $ (BOX605F(X) \leftrightarrow BOX488P(X)) \land $ \\ 
 $ (BOX28F(X) \leftrightarrow BOX366P(X)) \land $ \\ 
 $ (PinvG11F \leftrightarrow PinvG11F) \land $ \\ 
 $ (BOX7F(X) \leftrightarrow BOX328P(X)) \land $ \\ 
 $ (BOX36F(X) \leftrightarrow BOX615P(X)) \land $ \\ 
 $ (BOX18F(X) \leftrightarrow BOX347P(X)) \land $ \\ 
 $ (E1G5F(X) \leftrightarrow E1G5P(X)) \land $ \\ 
 $ (PinvL1F \leftrightarrow PinvL1F) \land $ \\ 
 $ (BOX526F(X) \leftrightarrow BOX380P(X)) \land $ \\ 
 $ (E1G12InvF(X) \leftrightarrow E1G12InvP(X)) \land $ \\ 
 $ (PG19F \leftrightarrow PG19P) \land $ \\ 
 $ (PG8F \leftrightarrow PG8F) \land $ \\ 
 $ (BOX548F(X) \leftrightarrow BOX423P(X)) \land $ \\ 
 $ (PL1F \leftrightarrow PL1F) \land $ \\ 
 $ (BOX0F(X) \leftrightarrow BOX318P(X)) \land $ \\ 
 $ (C24F(X) \leftrightarrow C24P(X)) \land $ \\ 
 $ (E1L29F(X) \leftrightarrow E1L29P(X)) \land $ \\ 
 $ (BOX84F(X) \leftrightarrow BOX629P(X)) \land $ \\ 
 $ (BOX46F(X) \leftrightarrow BOX616P(X)) \land $ \\ 
 $ (BOX87F(X) \leftrightarrow BOX632P(X)) \land $ \\ 
 $ (PinvG18F \leftrightarrow PinvG18F) \land $ \\ 
 $ (E3G14F(X) \leftrightarrow E3G14P(X)) \land $ \\ 
 $ (E1G2F(X) \leftrightarrow E1G2P(X)) \land $ \\ 
 $ (PG5F \leftrightarrow PG5P) \land $ \\ 
 $ (DIAMOND182F(X) \leftrightarrow DIAMOND129P(X)) \land $ \\ 
 $ (BOX523F(X) \leftrightarrow BOX376P(X)) \land $ \\ 
 $ (BOX86F(X) \leftrightarrow BOX631P(X)) \land $ \\ 
 $ (E1L26F(X) \leftrightarrow E1L26P(X)) \land $ \\ 
 $ (BOX608F(X) \leftrightarrow BOX614P(X)) \land $ \\ 
 $ (DIAMOND239F(X) \leftrightarrow DIAMOND285P(X)) \land $ \\ 
 $ (DIAMOND202F(X) \leftrightarrow DIAMOND154P(X)) \land $ \\ 
 $ (PG4F \leftrightarrow PG4P) \land $ \\ 
 $ (BOX256F(X) \leftrightarrow BOX303P(X)) \land $ \\ 
 $ (BOX206F(X) \leftrightarrow BOX159P(X)) \land $ \\ 
 $ (BOX597F(X) \leftrightarrow BOX480P(X)) \land $ \\ 
 $ (DIAMOND262F(X) \leftrightarrow DIAMOND311P(X)) \land $ \\ 
 $ (BOX193F(X) \leftrightarrow BOX143P(X)) \land $ \\ 
 $ (E4G25F(X) \leftrightarrow E4G25P(X)) \land $ \\ 
 $ (BOX596F(X) \leftrightarrow BOX479P(X)) \land $ \\ 
 $ (PG17F \leftrightarrow PG17F) \land $ \\ 
 $ (BOX37F(X) \leftrightarrow BOX382P(X)) \land $ \\ 
 $ (E1G19F(X) \leftrightarrow E1G19P(X)) \land $ \\ 
 $ (PinvG12F \leftrightarrow PinvG12F) \land $ \\ 
 $ (BOX559F(X) \leftrightarrow BOX442P(X)) \land $ \\ 
 $ (BOX527F(X) \leftrightarrow BOX381P(X)) \land $ \\ 
 $ (BOX75F(X) \leftrightarrow BOX434P(X)) \land $ \\ 
 $ (E3G2F(X) \leftrightarrow E3G2P(X)) \land $ \\ 
 $ (DIAMOND222F(X) \leftrightarrow DIAMOND177P(X)) \land $ \\ 
 $ (DIAMOND214F(X) \leftrightarrow DIAMOND168P(X)) \land $ \\ 
 $ (BOX521F(X) \leftrightarrow BOX372P(X)) \land $ \\ 
 $ (BOX50F(X) \leftrightarrow BOX401P(X)) \land $ \\ 
 $ (E5L1F(X) \leftrightarrow E5L1P(X)) \land $ \\ 
 $ (BOX562F(X) \leftrightarrow BOX445P(X)) \land $ \\ 
 $ (PinvG8F \leftrightarrow PinvG8P) \land $ \\ 
 $ (E4G8F(X) \leftrightarrow E4G8P(X)) \land $ \\ 
 $ (E1G20InvF(X) \leftrightarrow E1G20InvP(X)) \land $ \\ 
 $ (BOX85F(X) \leftrightarrow BOX630P(X)) \land $ \\ 
 $ (BOX111F(X) \leftrightarrow BOX656P(X)) \land $ \\ 
 $ (C7F(X) \leftrightarrow C7P(X)) \land $ \\ 
 $ (BOX82F(X) \leftrightarrow BOX627P(X)) \land $ \\ 
 $ (BOX520F(X) \leftrightarrow BOX370P(X)) \land $ \\ 
 $ (E2G3F(X) \leftrightarrow E2G3P(X)) \land $ \\ 
 $ (BOX574F(X) \leftrightarrow BOX457P(X)) \land $ \\ 
 $ (BOX509F(X) \leftrightarrow BOX349P(X)) \land $ \\ 
 $ (BOX513F(X) \leftrightarrow BOX355P(X)) \land $ \\ 
 $ (PG27F \leftrightarrow PG27F) \land $ \\ 
 $ (DIAMOND264F(X) \leftrightarrow DIAMOND313P(X)) \land $ \\ 
 $ (PG16F \leftrightarrow PG16P) \land $ \\ 
 $ (DIAMOND59F(X) \leftrightarrow DIAMOND158P(X)) \land $ \\ 
 $ (DIAMOND249F(X) \leftrightarrow DIAMOND295P(X)) \land $ \\ 
 $ (BOX30F(X) \leftrightarrow BOX369P(X)) \land $ \\ 
 $ (E3G28F(X) \leftrightarrow E3G28P(X)) \land $ \\ 
 $ (E3G4F(X) \leftrightarrow E3G4P(X)) \land $ \\ 
 $ (PL29F \leftrightarrow PL29F) \land $ \\ 
 $ (DIAMOND186F(X) \leftrightarrow DIAMOND134P(X)) \land $ \\ 
 $ (C15F(X) \leftrightarrow C15P(X)) \land $ \\ 
 $ (BOX115F(X) \leftrightarrow BOX660P(X)) \land $ \\ 
 $ (BOX542F(X) \leftrightarrow BOX411P(X)) \land $ \\ 
 $ (BOX17F(X) \leftrightarrow BOX345P(X)) \land $ \\ 
 $ (BOX120F(X) \leftrightarrow BOX665P(X)) \land $ \\ 
 $ (BOX496F(X) \leftrightarrow BOX327P(X)) \land $ \\ 
 $ (PG28F \leftrightarrow PG28P) \land $ \\ 
 $ (BOX493F(X) \leftrightarrow BOX322P(X)) \land $ \\ 
 $ (DIAMOND215F(X) \leftrightarrow DIAMOND169P(X)) \land $ \\ 
 $ (BOX588F(X) \leftrightarrow BOX471P(X)) \land $ \\ 
 $ (BOX555F(X) \leftrightarrow BOX435P(X)) \land $ \\ 
 $ (BOX51F(X) \leftrightarrow BOX619P(X)) \land $ \\ 
 $ (DIAMOND79F(X) \leftrightarrow DIAMOND180P(X)) \land $ \\ 
 $ (BOX511F(X) \leftrightarrow BOX352P(X)) \land $ \\ 
 $ (PL1F \leftrightarrow PL1P) \land $ \\ 
 $ (PG28F \leftrightarrow PG28F) \land $ \\ 
 $ (BOX10F(X) \leftrightarrow BOX332P(X)) \land $ \\ 
 $ (E4L15F(X) \leftrightarrow E4L15P(X)) \land $ \\ 
 $ (PinvL26F \leftrightarrow PinvL26F) \land $ \\ 
 $ (BOX505F(X) \leftrightarrow BOX341P(X)) \land $ \\ 
 $ (BOX502F(X) \leftrightarrow BOX337P(X)) \land $ \\ 
 $ (DIAMOND238F(X) \leftrightarrow DIAMOND284P(X)) \land $ \\ 
 $ (BOX127F(X) \leftrightarrow BOX672P(X)) \land $ \\ 
 $ (BOX83F(X) \leftrightarrow BOX628P(X)) \land $ \\ 
 $ (DIAMOND6F(X) \leftrightarrow DIAMOND274P(X)) \land $ \\ 
 $ (BOX58F(X) \leftrightarrow BOX412P(X)) \land $ \\ 
 $ (BOX540F(X) \leftrightarrow BOX406P(X)) \land $ \\ 
 $ (BOX566F(X) \leftrightarrow BOX449P(X)) \land $ \\ 
 $ (PL15F \leftrightarrow PL15P) \land $ \\ 
 $ (BOX538F(X) \leftrightarrow BOX404P(X)) \land $ \\ 
 $ (PG18F \leftrightarrow PG18F) \land $ \\ 
 $ (BOX27F(X) \leftrightarrow BOX364P(X)) \land $ \\ 
 $ (DIAMOND201F(X) \leftrightarrow DIAMOND153P(X)) \land $ \\ 
 $ (BOX503F(X) \leftrightarrow BOX339P(X)) \land $ \\ 
 $ (E3G7F(X) \leftrightarrow E3G7P(X)) \land $ \\ 
 $ (E1G16F(X) \leftrightarrow E1G16P(X)) \land $ \\ 
 $ (DIAMOND218F(X) \leftrightarrow DIAMOND172P(X)) \land $ \\ 
 $ (BOX223F(X) \leftrightarrow BOX178P(X)) \land $ \\ 
 $ (BOX514F(X) \leftrightarrow BOX357P(X)) \land $ \\ 
 $ (E1G7InvF(X) \leftrightarrow E1G7InvP(X)) \land $ \\ 
 $ (DIAMOND221F(X) \leftrightarrow DIAMOND176P(X)) \land $ \\ 
 $ (DIAMOND189F(X) \leftrightarrow DIAMOND138P(X)) \land $ \\ 
 $ (BOX611F(X) \leftrightarrow BOX621P(X))) \land $ \\ 
 $ (PG7 \rightarrow E1G7Inv(dG7Inv)) \land $ \\ 
 $ (PL1 \rightarrow E1L1Inv(dL1Inv)) \land $ \\ 
 $ (PinvG27 \rightarrow E1G27(dG27)) \land $ \\ 
 $ (PinvG11 \rightarrow E1G11(dG11)) \land $ \\ 
 $ (PinvL1 \rightarrow E1L1(dL1)) \land $ \\ 
 $ (PG25 \rightarrow E1G25Inv(dG25Inv)) \land $ \\ 
 $ (PinvG19 \rightarrow E1G19(dG19)) \land $ \\ 
 $ (PinvG28 \rightarrow E1G28(dG28)) \land $ \\ 
 $ (PG20 \rightarrow E1G20Inv(dG20Inv)) \land $ \\ 
 $ (PG14 \rightarrow E1G14Inv(dG14Inv)) \land $ \\ 
 $ (PinvG29 \rightarrow E1G29(dG29)) \land $ \\ 
 $ (PG2 \rightarrow E1G2Inv(dG2Inv)) \land $ \\ 
 $ (PG23 \rightarrow E1G23Inv(dG23Inv)) \land $ \\ 
 $ (PinvG3 \rightarrow E1G3(dG3)) \land $ \\ 
 $ (PinvG7 \rightarrow E1G7(dG7)) \land $ \\ 
 $ (PL15 \rightarrow E1L15Inv(dL15Inv)) \land $ \\ 
 $ (PG16 \rightarrow E1G16Inv(dG16Inv)) \land $ \\ 
 $ (PinvG25 \rightarrow E1G25(dG25)) \land $ \\ 
 $ (PinvL15 \rightarrow E1L15(dL15)) \land $ \\ 
 $ (PinvG4 \rightarrow E1G4(dG4)) \land $ \\ 
 $ (PL26 \rightarrow E1L26Inv(dL26Inv)) \land $ \\ 
 $ (PG8 \rightarrow E1G8Inv(dG8Inv)) \land $ \\ 
 $ (PG12 \rightarrow E1G12Inv(dG12Inv)) \land $ \\ 
 $ (PG17 \rightarrow E1G17Inv(dG17Inv)) \land $ \\ 
 $ (PinvG16 \rightarrow E1G16(dG16)) \land $ \\ 
 $ (PG28 \rightarrow E1G28Inv(dG28Inv)) \land $ \\ 
 $ (PL29 \rightarrow E1L29Inv(dL29Inv)) \land $ \\ 
 $ (PinvG17 \rightarrow E1G17(dG17)) \land $ \\ 
 $ (PinvL26 \rightarrow E1L26(dL26)) \land $ \\ 
 $ (PG19 \rightarrow E1G19Inv(dG19Inv)) \land $ \\ 
 $ (PinvG18 \rightarrow E1G18(dG18)) \land $ \\ 
 $ (PG9 \rightarrow E1G9Inv(dG9Inv)) \land $ \\ 
 $ (PinvG14 \rightarrow E1G14(dG14)) \land $ \\ 
 $ (PG18 \rightarrow E1G18Inv(dG18Inv)) \land $ \\ 
 $ (PG5 \rightarrow E1G5Inv(dG5Inv)) \land $ \\ 
 $ (PinvG5 \rightarrow E1G5(dG5)) \land $ \\ 
 $ (PG4 \rightarrow E1G4Inv(dG4Inv)) \land $ \\ 
 $ (PG11 \rightarrow E1G11Inv(dG11Inv)) \land $ \\ 
 $ (PinvG8 \rightarrow E1G8(dG8)) \land $ \\ 
 $ (PinvG2 \rightarrow E1G2(dG2)) \land $ \\ 
 $ (PinvG9 \rightarrow E1G9(dG9)) \land $ \\ 
 $ (PinvG20 \rightarrow E1G20(dG20)) \land $ \\ 
 $ (PinvG23 \rightarrow E1G23(dG23)) \land $ \\ 
 $ (PG3 \rightarrow E1G3Inv(dG3Inv)) \land $ \\ 
 $ (PG29 \rightarrow E1G29Inv(dG29Inv)) \land $ \\ 
 $ (PinvL29 \rightarrow E1L29(dL29)) \land $ \\ 
 $ (PinvG12 \rightarrow E1G12(dG12)) \land $ \\ 
 $ (PG27 \rightarrow E1G27Inv(dG27Inv)))$ 
\end{document}