Tbox: F O  ( >= 2.L29 /\ H F F O !>= 5.L1 )  << O  ( C25 /\ G O F F F O >= 3.G27 ) 
Tbox: H G  ( C21 /\  ( !>= 5.G17 /\  ( >= 3.G28 /\ C15 )  )  )  << F G O O O  ( O C6 /\ !C25 ) 
Tbox: O  ( >= 4.G14 /\ H G O O O !C18 )  << F  ( G G >= 2.G20 /\ F O O !C13 ) 
Tbox:  ( H  ( F C11 /\ F !>= 4.G8 )  /\ H C8 )  << G  (  ( C24 /\ H C11 )  /\  ( >= 4.G17 /\ O C23 )  ) 
Tbox: F H F F  ( C7 /\  ( C8 /\ H >= 1.L26 )  )  << G  (  ( G C13 /\ O >= 2.G29 )  /\ H O >= 1.G16 ) 
Tbox: O G  ( F  ( >= 4.G12 /\ >= 3.G7 )  /\ H G >= 3.G25 )  <<  ( O O F O C12 /\  ( >= 1.G3 /\ G C28 )  ) 
Tbox:  ( F >= 5.G2 /\ G G O F  ( C19 /\ >= 3.G25 )  )  << H  ( H !>= 2.G18 /\ O O  ( C1 /\ >= 3.G18 )  ) 
Tbox: F O G H G G F G !C4 << H O H  ( C12 /\  ( C10 /\ O F >= 4.L15 )  ) 
Tbox: H O  (  ( C16 /\ >= 2.G5 )  /\ O G !C13 )  << F F G F F G G G F >= 1.G19
Tbox:  ( G H  ( >= 4.G25 /\ O >= 2.G3 )  /\ F H C25 )  << G G  ( !C1 /\ F  ( >= 5.G29 /\ O C28 )  ) 
Tbox:  ( H O G >= 2.G9 /\ G G  ( >= 1.G8 /\ >= 3.G14 )  )  << H H H  ( F  ( C23 /\ C24 )  /\ O C13 ) 
Tbox: H H G  ( >= 4.G4 /\  ( O C15 /\ O C6 )  )  <<  ( O G  ( >= 4.G25 /\ C4 )  /\  ( C7 /\ !C13 )  ) 
Tbox: F  (  ( C11 /\ F  ( C18 /\ >= 3.G25 )  )  /\ O >= 5.G4 )  << O G H F H G H F G >= 1.G23
Tbox: G O  (  ( >= 3.G4 /\ O H >= 5.G2 )  /\ H >= 1.G7 )  << G G  ( G  ( C17 /\ >= 4.L1 )  /\ O O C25 ) 
Tbox: G  ( G O G !>= 3.G11 /\ H O C14 )  << H F  (  ( >= 4.G9 /\ F C16 )  /\  ( >= 3.G2 /\ >= 1.G7 )  ) 
Qrole:>= 1.G16
Qrole1:>= 1.G16
Qrole:>= 2.G18
Qrole1:>= 1.G18
Qrole:>= 3.G25
Qrole1:>= 1.G25
Qrole:>= 5.L1
Qrole1:>= 1.L1
Qrole:>= 5.G2
Qrole1:>= 1.G2
Qrole:>= 5.G4
Qrole1:>= 1.G4
Qrole:>= 3.G2
Qrole1:>= 1.G2
Qrole:>= 5.G17
Qrole1:>= 1.G17
Qrole:>= 3.G27
Qrole1:>= 1.G27
Qrole:>= 3.G28
Qrole1:>= 1.G28
Qrole:>= 4.L1
Qrole1:>= 1.L1
Qrole:>= 3.G7
Qrole1:>= 1.G7
Qrole:>= 1.G19
Qrole1:>= 1.G19
Qrole:>= 1.G3
Qrole1:>= 1.G3
Qrole:>= 1.G8
Qrole1:>= 1.G8
Qrole:>= 4.G25
Qrole1:>= 1.G25
Qrole:>= 3.G4
Qrole1:>= 1.G4
Qrole:>= 1.G7
Qrole1:>= 1.G7
Qrole:>= 4.G17
Qrole1:>= 1.G17
Qrole:>= 2.L29
Qrole1:>= 1.L29
Qrole:>= 1.G23
Qrole1:>= 1.G23
Qrole:>= 2.G29
Qrole1:>= 1.G29
Qrole:>= 4.L15
Qrole1:>= 1.L15
Qrole:>= 3.G14
Qrole1:>= 1.G14
Qrole:>= 3.G11
Qrole1:>= 1.G11
Qrole:>= 5.G29
Qrole1:>= 1.G29
Qrole:>= 3.G18
Qrole1:>= 1.G18
Qrole:>= 4.G9
Qrole1:>= 1.G9
Qrole:>= 4.G8
Qrole1:>= 1.G8
Qrole:>= 1.L26
Qrole1:>= 1.L26
Qrole:>= 2.G9
Qrole1:>= 1.G9
Qrole:>= 4.G14
Qrole1:>= 1.G14
Qrole:>= 4.G4
Qrole1:>= 1.G4
Qrole:>= 2.G3
Qrole1:>= 1.G3
Qrole:>= 2.G20
Qrole1:>= 1.G20
Qrole:>= 4.G12
Qrole1:>= 1.G12
Qrole:>= 2.G5
Qrole1:>= 1.G5
Rerformulation: ((E4G12F(X) -> E1G12F(X)) & (E2G29F(X) -> E1G29F(X)) & (BOX0F(X) -> BOX1F(X)) & (E4G9F(X) -> E2G9F(X)) & (E3G18F(X) -> E2G18F(X)) & (E1G4F(X) -> BOX2F(X)) & (E4G8F(X) -> E1G8F(X)) & (E1G18F(X) -> BOX3F(X)) & (E1G27F(X) -> BOX4F(X)) & (BOX5F(X) -> (DIAMOND6F(X) & !C13F(X) & C7F(X))) & (E5G2F(X) -> E3G2F(X)) & (E3G4F(X) -> E1G4F(X)) & (E2L29F(X) -> E1L29F(X)) & (E1G25F(X) -> BOX7F(X)) & (DIAMOND8F(X) -> DIAMOND9F(X)) & (E1G17F(X) -> BOX10F(X)) & (E3G11F(X) -> BOX11F(X)) & (E3G2F(X) -> BOX12F(X)) & (E4L1F(X) -> E1L1F(X)) & (E2G5F(X) -> E1G5F(X)) & (E2G20F(X) -> E1G20F(X)) & (E1G19F(X) -> BOX13F(X)) & (DIAMOND14F(X) -> DIAMOND15F(X)) & (E1G20F(X) -> BOX16F(X)) & (E4G14F(X) -> BOX17F(X)) & (BOX18F(X) -> BOX19F(X)) & (E3G27F(X) -> BOX20F(X)) & (DIAMOND21F(X) -> BOX22F(X)) & (E1G3F(X) -> BOX23F(X)) & (E4G14F(X) -> E3G14F(X)) & (E3G18F(X) -> BOX24F(X)) & (E1G28F(X) -> BOX25F(X)) & (E3G28F(X) -> E1G28F(X)) & (E3G4F(X) -> BOX26F(X)) & (E2G5F(X) -> BOX27F(X)) & (E4G9F(X) -> BOX28F(X)) & (E5G2F(X) -> BOX29F(X)) & (E1G5F(X) -> BOX30F(X)) & (E1G2F(X) -> BOX31F(X)) & (E1G8F(X) -> BOX32F(X)) & (E5G29F(X) -> BOX33F(X)) & (E4G17F(X) -> BOX34F(X)) & (E5G4F(X) -> E4G4F(X)) & (DIAMOND35F(X) -> BOX36F(X)) & (E1G12F(X) -> BOX37F(X)) & (E3G14F(X) -> BOX38F(X)) & (E2G18F(X) -> BOX39F(X)) & (E2G29F(X) -> BOX40F(X)) & (E4G12F(X) -> BOX41F(X)) & (E1G29F(X) -> BOX42F(X)) & (E2G20F(X) -> BOX43F(X)) & ((DIAMOND44F(X) & BOX45F(X)) -> BOX46F(X)) & (E3G25F(X) -> E1G25F(X)) & (E3G2F(X) -> E1G2F(X)) & (E1G9F(X) -> BOX47F(X)) & (E1G7F(X) -> BOX48F(X)) & ((BOX49F(X) & BOX50F(X)) -> BOX51F(X)) & (E2G18F(X) -> E1G18F(X)) & (E2G3F(X) -> BOX52F(X)) & (DIAMOND53F(X) -> (DIAMOND54F(X) & BOX55F(X) & E1G3F(X))) & (E1G14F(X) -> BOX56F(X)) & (E1G16F(X) -> BOX57F(X)) & (E2G3F(X) -> E1G3F(X)) & ((BOX58F(X) & DIAMOND59F(X)) -> BOX60F(X)) & (E3G7F(X) -> BOX61F(X)) & (E2G9F(X) -> BOX62F(X)) & (E5G4F(X) -> BOX63F(X)) & (E4G25F(X) -> E3G25F(X)) & (E2G9F(X) -> E1G9F(X)) & (E1G23F(X) -> BOX64F(X)) & (DIAMOND65F(X) -> DIAMOND66F(X)) & (E3G14F(X) -> E1G14F(X)) & (E3G7F(X) -> E1G7F(X)) & (E5G17F(X) -> BOX67F(X)) & ((BOX68F(X) & BOX69F(X)) -> BOX70F(X)) & (E1G11F(X) -> BOX71F(X)) & (BOX72F(X) -> DIAMOND73F(X)) & (E3G25F(X) -> BOX74F(X)) & (E4G4F(X) -> BOX75F(X)) & (E5G29F(X) -> E2G29F(X)) & (E5L1F(X) -> E4L1F(X)) & (E4G17F(X) -> E1G17F(X)) & (E4L15F(X) -> E1L15F(X)) & (E3G28F(X) -> BOX76F(X)) & (E5G17F(X) -> E4G17F(X)) & (E3G11F(X) -> E1G11F(X)) & (E4G25F(X) -> BOX77F(X)) & (BOX78F(X) -> DIAMOND79F(X)) & (E4G8F(X) -> BOX80F(X)) & (E3G27F(X) -> E1G27F(X)) & (E4G4F(X) -> E3G4F(X)) & (E1L26F(X) -> BOX81F(X)) & (E1G19InvF(X) -> BOX82F(X)) & (E1G27F(X) -> BOX83F(X)) & (E1G2F(X) -> BOX84F(X)) & (E1G4F(X) -> BOX85F(X)) & (E1G8InvF(X) -> BOX86F(X)) & (E1G20F(X) -> BOX87F(X)) & (E1G29InvF(X) -> BOX88F(X)) & (E1G2InvF(X) -> BOX89F(X)) & (E1G18F(X) -> BOX90F(X)) & (E1G28F(X) -> BOX91F(X)) & (E1G5InvF(X) -> BOX92F(X)) & (E1G9F(X) -> BOX93F(X)) & (E1G27InvF(X) -> BOX94F(X)) & (E1G4InvF(X) -> BOX95F(X)) & (E1G20InvF(X) -> BOX96F(X)) & (E1G7F(X) -> BOX97F(X)) & (E1L15F(X) -> BOX98F(X)) & (E1G11F(X) -> BOX99F(X)) & (E1G14InvF(X) -> BOX100F(X)) & (E1L1F(X) -> BOX101F(X)) & (E1G3InvF(X) -> BOX102F(X)) & (E1G17F(X) -> BOX103F(X)) & (E1G29F(X) -> BOX104F(X)) & (E1G14F(X) -> BOX105F(X)) & (E1G17InvF(X) -> BOX106F(X)) & (E1G11InvF(X) -> BOX107F(X)) & (E1L29InvF(X) -> BOX108F(X)) & (E1L1InvF(X) -> BOX109F(X)) & (E1G16F(X) -> BOX110F(X)) & (E1G23F(X) -> BOX111F(X)) & (E1G5F(X) -> BOX112F(X)) & (E1G3F(X) -> BOX113F(X)) & (E1L29F(X) -> BOX114F(X)) & (E1G18InvF(X) -> BOX115F(X)) & (E1G28InvF(X) -> BOX116F(X)) & (E1G19F(X) -> BOX117F(X)) & (E1G8F(X) -> BOX118F(X)) & (E1L15InvF(X) -> BOX119F(X)) & (E1G25InvF(X) -> BOX120F(X)) & (E1G25F(X) -> BOX121F(X)) & (E1L26InvF(X) -> BOX122F(X)) & (E1G12F(X) -> BOX123F(X)) & (E1G16InvF(X) -> BOX124F(X)) & (E1G23InvF(X) -> BOX125F(X)) & (E1G7InvF(X) -> BOX126F(X)) & (E1G12InvF(X) -> BOX127F(X)) & (E1G9InvF(X) -> BOX128F(X)))


Modal Equiv Pure Future: G((DIAMOND272P(X) <-> FC15P(X)) & (DIAMOND65F(X) <-> FDIAMOND209F(X)) & (XDIAMOND140P(X) <-> (DIAMOND140P(X) | XBOX141P(X))) & (XDIAMOND145P(X) <-> (DIAMOND145P(X) | X(C7P(X) & BOX146P(X) & C8P(X)))) & (DIAMOND198F(X) <-> FBOX199F(X)) & (XDIAMOND263F(X) <-> (DIAMOND263F(X) | X(C16F(X) & E2G5F(X) & DIAMOND264F(X)))) & (DIAMOND182F(X) <-> F(DIAMOND183F(X) & E4G9F(X) & E3G2F(X) & E1G7F(X))) & (DIAMOND195F(X) <-> F(C7F(X) & BOX196F(X) & C8F(X))) & (XDIAMOND142P(X) <-> (DIAMOND142P(X) | XBOX143P(X))) & (DIAMOND73F(X) <-> FDIAMOND219F(X)) & (XDIAMOND257F(X) <-> (DIAMOND257F(X) | XDIAMOND204F(X))) & (DIAMOND293P(X) <-> FBOX294P(X)) & (XDIAMOND209F(X) <-> (DIAMOND209F(X) | X(E2L29F(X) & BOX259F(X)))) & (DIAMOND211F(X) <-> FDIAMOND212F(X)) & (DIAMOND215F(X) <-> FDIAMOND216F(X)) & (XDIAMOND197F(X) <-> (DIAMOND197F(X) | XBOX246F(X))) & (DIAMOND295P(X) <-> FDIAMOND151P(X)) & (XDIAMOND239F(X) <-> (DIAMOND239F(X) | XBOX241F(X))) & (DIAMOND315P(X) <-> FDIAMOND316P(X)) & (XDIAMOND155P(X) <-> (DIAMOND155P(X) | X(E4G12P(X) & E3G7P(X)))) & (XDIAMOND156P(X) <-> (DIAMOND156P(X) | XDIAMOND157P(X))) & (XDIAMOND216F(X) <-> (DIAMOND216F(X) | XE3G27F(X))) & (XDIAMOND8F(X) <-> (DIAMOND8F(X) | X(E4G14F(X) & BOX232F(X)))) & (XDIAMOND168P(X) <-> (DIAMOND168P(X) | XDIAMOND169P(X))) & (DIAMOND217F(X) <-> FC11F(X)) & (DIAMOND316P(X) <-> FDIAMOND317P(X)) & (XDIAMOND172P(X) <-> (DIAMOND172P(X) | X!E4G8P(X))) & (XDIAMOND235F(X) <-> (DIAMOND235F(X) | X!C18F(X))) & (DIAMOND313P(X) <-> FBOX314P(X)) & (XDIAMOND262F(X) <-> (DIAMOND262F(X) | XC23F(X))) & (DIAMOND35F(X) <-> FDIAMOND197F(X)) & (DIAMOND44F(X) <-> FE5G2F(X)) & (DIAMOND284P(X) <-> F(E3G4P(X) & DIAMOND285P(X) & BOX286P(X))) & (DIAMOND269P(X) <-> FBOX270P(X)) & (XDIAMOND179P(X) <-> (DIAMOND179P(X) | XE1G19P(X))) & (XDIAMOND267F(X) <-> (DIAMOND267F(X) | XDIAMOND268F(X))) & (XDIAMOND162P(X) <-> (DIAMOND162P(X) | XDIAMOND163P(X))) & (DIAMOND204F(X) <-> FDIAMOND205F(X)) & (DIAMOND9F(X) <-> F(BOX184F(X) & DIAMOND185F(X))) & (DIAMOND79F(X) <-> FBOX225F(X)) & (XDIAMOND152P(X) <-> (DIAMOND152P(X) | XE5G2P(X))) & (DIAMOND191F(X) <-> FBOX192F(X)) & (XDIAMOND169P(X) <-> (DIAMOND169P(X) | XDIAMOND170P(X))) & (DIAMOND187F(X) <-> F(C18F(X) & E3G25F(X))) & (DIAMOND310P(X) <-> FDIAMOND167P(X)) & (DIAMOND288P(X) <-> FDIAMOND289P(X)) & (XDIAMOND177P(X) <-> (DIAMOND177P(X) | XBOX178P(X))) & (DIAMOND280P(X) <-> F!C18P(X)) & (DIAMOND200F(X) <-> FE4L15F(X)) & (XDIAMOND135P(X) <-> (DIAMOND135P(X) | X(C11P(X) & DIAMOND136P(X) & DIAMOND137P(X)))) & (XDIAMOND250F(X) <-> (DIAMOND250F(X) | XDIAMOND201F(X))) & (DIAMOND163P(X) <-> F(E2L29P(X) & BOX307P(X))) & (DIAMOND134P(X) <-> FDIAMOND281P(X)) & (DIAMOND276P(X) <-> F(E4G14P(X) & BOX277P(X))) & (XDIAMOND133P(X) <-> (DIAMOND133P(X) | XDIAMOND134P(X))) & (DIAMOND21F(X) <-> FBOX193F(X)) & (DIAMOND311P(X) <-> FC23P(X)) & (DIAMOND306P(X) <-> FE2G3P(X)) & (DIAMOND213F(X) <-> FDIAMOND214F(X)) & (DIAMOND218F(X) <-> F!E4G8F(X)) & (DIAMOND282P(X) <-> FBOX283P(X)) & (XDIAMOND149P(X) <-> (DIAMOND149P(X) | XBOX150P(X))) & (DIAMOND183F(X) <-> FC16F(X)) & (XDIAMOND243F(X) <-> (DIAMOND243F(X) | XC25F(X))) & (XDIAMOND264F(X) <-> (DIAMOND264F(X) | XBOX265F(X))) & (XDIAMOND138P(X) <-> (DIAMOND138P(X) | XBOX139P(X))) & (DIAMOND207F(X) <-> F(E5G29F(X) & DIAMOND208F(X))) & (DIAMOND273P(X) <-> FC6P(X)) & (XDIAMOND130P(X) <-> (DIAMOND130P(X) | XC16P(X))) & (XDIAMOND268F(X) <-> (DIAMOND268F(X) | X(DIAMOND230F(X) & !C25F(X)))) & (DIAMOND161P(X) <-> FC28P(X)) & (DIAMOND214F(X) <-> FDIAMOND215F(X)) & (XDIAMOND6F(X) <-> (DIAMOND6F(X) | XBOX231F(X))) & (XDIAMOND53F(X) <-> (DIAMOND53F(X) | XBOX256F(X))) & (DIAMOND185F(X) <-> FDIAMOND186F(X)) & (DIAMOND157P(X) <-> FC12P(X)) & (XDIAMOND236F(X) <-> (DIAMOND236F(X) | X!C13F(X))) & (DIAMOND59F(X) <-> FBOX206F(X)) & (DIAMOND278P(X) <-> FDIAMOND279P(X)) & (DIAMOND308P(X) <-> F(C25P(X) & BOX309P(X))) & (XDIAMOND258F(X) <-> (DIAMOND258F(X) | XE2G3F(X))) & (XDIAMOND208F(X) <-> (DIAMOND208F(X) | XC28F(X))) & (DIAMOND289P(X) <-> FC25P(X)) & (XDIAMOND158P(X) <-> (DIAMOND158P(X) | XBOX159P(X))) & (DIAMOND224F(X) <-> FE1G19F(X)) & (XDIAMOND188F(X) <-> (DIAMOND188F(X) | XE5G4F(X))) & (XDIAMOND244F(X) <-> (DIAMOND244F(X) | XE2G29F(X))) & (DIAMOND201F(X) <-> F(C19F(X) & E3G25F(X))) & (XDIAMOND251F(X) <-> (DIAMOND251F(X) | XDIAMOND252F(X))) & (DIAMOND14F(X) <-> F(C11F(X) & DIAMOND187F(X) & DIAMOND188F(X))) & (XDIAMOND144P(X) <-> (DIAMOND144P(X) | XDIAMOND145P(X))) & (XDIAMOND230F(X) <-> (DIAMOND230F(X) | XC6F(X))) & (DIAMOND291P(X) <-> FE1G16P(X)) & (XDIAMOND234F(X) <-> (DIAMOND234F(X) | XDIAMOND235F(X))) & (DIAMOND279P(X) <-> FDIAMOND280P(X)) & (XDIAMOND167P(X) <-> (DIAMOND167P(X) | XDIAMOND168P(X))) & (DIAMOND302P(X) <-> FBOX303P(X)) & (DIAMOND304P(X) <-> FDIAMOND305P(X)) & (XDIAMOND247F(X) <-> (DIAMOND247F(X) | XBOX248F(X))) & (XDIAMOND176P(X) <-> (DIAMOND176P(X) | XDIAMOND177P(X))) & (XDIAMOND226F(X) <-> (DIAMOND226F(X) | XBOX227F(X))) & (XDIAMOND266F(X) <-> (DIAMOND266F(X) | XDIAMOND267F(X))) & (XDIAMOND154P(X) <-> (DIAMOND154P(X) | X(C23P(X) & C24P(X)))) & (XDIAMOND66F(X) <-> (DIAMOND66F(X) | X(C25F(X) & BOX260F(X)))) & (XDIAMOND252F(X) <-> (DIAMOND252F(X) | X(C1F(X) & E3G18F(X)))) & (XDIAMOND151P(X) <-> (DIAMOND151P(X) | XE4L15P(X))) & (XDIAMOND205F(X) <-> (DIAMOND205F(X) | XC12F(X))) & (DIAMOND271P(X) <-> FC14P(X)) & (XDIAMOND136P(X) <-> (DIAMOND136P(X) | X(C18P(X) & E3G25P(X)))) & (DIAMOND189F(X) <-> FBOX190F(X)) & (XDIAMOND249F(X) <-> (DIAMOND249F(X) | XDIAMOND200F(X))) & (XDIAMOND171P(X) <-> (DIAMOND171P(X) | XC11P(X))) & (XDIAMOND261F(X) <-> (DIAMOND261F(X) | XDIAMOND213F(X))) & (XDIAMOND229F(X) <-> (DIAMOND229F(X) | XC15F(X))) & (DIAMOND290P(X) <-> FE2G29P(X)) & (DIAMOND312P(X) <-> F(C16P(X) & E2G5P(X) & DIAMOND313P(X))) & (DIAMOND317P(X) <-> F(DIAMOND273P(X) & !C25P(X))) & (XDIAMOND15F(X) <-> (DIAMOND15F(X) | XBOX237F(X))) & (DIAMOND137P(X) <-> FE5G4P(X)) & (XDIAMOND212F(X) <-> (DIAMOND212F(X) | X!E5L1F(X))) & (DIAMOND298P(X) <-> F(C1P(X) & E3G18P(X))) & (DIAMOND170P(X) <-> FE3G27P(X)) & (DIAMOND219F(X) <-> FBOX220F(X)) & (XDIAMOND253F(X) <-> (DIAMOND253F(X) | XBOX254F(X))) & (DIAMOND297P(X) <-> FDIAMOND298P(X)) & (DIAMOND301P(X) <-> FC13P(X)) & (DIAMOND148P(X) <-> FBOX292P(X)) & (XDIAMOND147P(X) <-> (DIAMOND147P(X) | XDIAMOND148P(X))) & (DIAMOND222F(X) <-> FBOX223F(X)) & (DIAMOND203F(X) <-> F(E4G12F(X) & E3G7F(X))) & (XDIAMOND186F(X) <-> (DIAMOND186F(X) | XDIAMOND236F(X))) & (XDIAMOND164P(X) <-> (DIAMOND164P(X) | XDIAMOND165P(X))) & (DIAMOND274P(X) <-> FBOX275P(X)) & (DIAMOND296P(X) <-> FDIAMOND153P(X)) & (XDIAMOND180P(X) <-> (DIAMOND180P(X) | XBOX181P(X))) & (DIAMOND210F(X) <-> FDIAMOND211F(X)) & (XDIAMOND173P(X) <-> (DIAMOND173P(X) | XDIAMOND174P(X))) & (XDIAMOND242F(X) <-> (DIAMOND242F(X) | XDIAMOND243F(X))) & (DIAMOND305P(X) <-> FDIAMOND156P(X)) & (XDIAMOND238F(X) <-> (DIAMOND238F(X) | X(E3G4F(X) & DIAMOND239F(X) & BOX240F(X)))) & (DIAMOND202F(X) <-> F(C23F(X) & C24F(X))) & (XDIAMOND165P(X) <-> (DIAMOND165P(X) | XDIAMOND166P(X))) & (XDIAMOND160P(X) <-> (DIAMOND160P(X) | X(E5G29P(X) & DIAMOND161P(X)))) & (XDIAMOND174P(X) <-> (DIAMOND174P(X) | XBOX175P(X))) & (DIAMOND166P(X) <-> F!E5L1P(X)) & (XDIAMOND54F(X) <-> (DIAMOND54F(X) | XDIAMOND257F(X))) & (DIAMOND281P(X) <-> F!C13P(X)) & (DIAMOND221F(X) <-> FDIAMOND222F(X)) & (DIAMOND285P(X) <-> FBOX287P(X)) & (XDIAMOND245F(X) <-> (DIAMOND245F(X) | XE1G16F(X))) & (XDIAMOND131P(X) <-> (DIAMOND131P(X) | X(BOX132P(X) & DIAMOND133P(X)))) & (XDIAMOND153P(X) <-> (DIAMOND153P(X) | X(C19P(X) & E3G25P(X)))) & (DIAMOND299P(X) <-> FBOX300P(X)) & (XDIAMOND129P(X) <-> (DIAMOND129P(X) | X(DIAMOND130P(X) & E4G9P(X) & E3G2P(X) & E1G7P(X)))) & (XDIAMOND228F(X) <-> (DIAMOND228F(X) | XC14F(X))) & (XDIAMOND255F(X) <-> (DIAMOND255F(X) | XC13F(X))) & (DIAMOND194F(X) <-> FDIAMOND195F(X)) & (XDIAMOND233F(X) <-> (DIAMOND233F(X) | XDIAMOND234F(X))) & (XBOX99F(X) <-> (BOX99F(X) & XBOX578F(X))) & (BOX352P(X) <-> GE3G27P(X)) & (XBOX72F(X) <-> (BOX72F(X) & XDIAMOND263F(X))) & (BOX439P(X) <-> GE4G25P(X)) & (XBOX397P(X) <-> (BOX397P(X) & XDIAMOND296P(X))) & (XBOX384P(X) <-> (BOX384P(X) & XBOX385P(X))) & (XBOX453P(X) <-> (BOX453P(X) & XPG28F)) & (BOX509F(X) <-> G(BOX510F(X) & DIAMOND242F(X))) & (BOX633P(X) <-> GBOX450P(X)) & (XBOX529F(X) <-> (BOX529F(X) & XE3G14F(X))) & (XBOX530F(X) <-> (BOX530F(X) & XE2G18F(X))) & (BOX357P(X) <-> GE1G3P(X)) & (BOX512F(X) <-> GC13F(X)) & (XBOX81F(X) <-> (BOX81F(X) & XBOX560F(X))) & (BOX329P(X) <-> GE1G25P(X)) & (XBOX418P(X) <-> (BOX418P(X) & XBOX419P(X))) & (BOX669P(X) <-> GBOX486P(X)) & (BOX650P(X) <-> GBOX467P(X)) & (XBOX240F(X) <-> (BOX240F(X) & XE1G7F(X))) & (XBOX520F(X) <-> (BOX520F(X) & XE1G5F(X))) & (XBOX438P(X) <-> (BOX438P(X) & XBOX439P(X))) & (BOX220F(X) <-> GDIAMOND221F(X)) & (XBOX503F(X) <-> (BOX503F(X) & XE1G19F(X))) & (XBOX97F(X) <-> (BOX97F(X) & XBOX576F(X))) & (BOX640P(X) <-> GBOX457P(X)) & (XBOX108F(X) <-> (BOX108F(X) & XBOX587F(X))) & (BOX585F(X) <-> GPinvG17F) & (XBOX388P(X) <-> (BOX388P(X) & XBOX389P(X))) & (XBOX483P(X) <-> (BOX483P(X) & XPG25F)) & (BOX621P(X) <-> G(DIAMOND154P(X) & DIAMOND301P(X))) & (BOX307P(X) <-> GDIAMOND164P(X)) & (XBOX85F(X) <-> (BOX85F(X) & XBOX564F(X))) & (XBOX507F(X) <-> (BOX507F(X) & XE1G20F(X))) & (BOX40F(X) <-> GBOX531F(X)) & (XBOX112F(X) <-> (BOX112F(X) & XBOX591F(X))) & (XBOX473P(X) <-> (BOX473P(X) & XPG23F)) & (XBOX111F(X) <-> (BOX111F(X) & XBOX590F(X))) & (BOX567F(X) <-> GPinvG29F) & (BOX429P(X) <-> GE1G11P(X)) & (XBOX348P(X) <-> (BOX348P(X) & XBOX349P(X))) & (XBOX436P(X) <-> (BOX436P(X) & XBOX437P(X))) & (BOX618P(X) <-> GDIAMOND299P(X)) & (XBOX377P(X) <-> (BOX377P(X) & XBOX378P(X))) & (BOX320P(X) <-> GDIAMOND271P(X)) & (BOX499F(X) <-> GE2G20F(X)) & (BOX563F(X) <-> GPG2F) & (BOX639P(X) <-> GBOX456P(X)) & (BOX22F(X) <-> G(BOX512F(X) & DIAMOND244F(X) & BOX513F(X))) & (BOX17F(X) <-> GBOX508F(X)) & (XBOX557F(X) <-> (BOX557F(X) & XE4G25F(X))) & (BOX579F(X) <-> GPinvG14F) & (XBOX107F(X) <-> (BOX107F(X) & XBOX586F(X))) & (BOX425P(X) <-> GE5G17P(X)) & (XBOX259F(X) <-> (BOX259F(X) & XDIAMOND210F(X))) & (BOX326P(X) <-> GE1G27P(X)) & (XBOX386P(X) <-> (BOX386P(X) & XBOX387P(X))) & (BOX653P(X) <-> GBOX470P(X)) & (BOX64F(X) <-> GBOX548F(X)) & (XBOX87F(X) <-> (BOX87F(X) & XBOX566F(X))) & (XBOX336P(X) <-> (BOX336P(X) & XBOX337P(X))) & (BOX18F(X) <-> GDIAMOND238F(X)) & (XBOX472P(X) <-> (BOX472P(X) & XPG16F)) & (BOX24F(X) <-> GBOX515F(X)) & (XBOX469P(X) <-> (BOX469P(X) & XPinvG11F)) & (BOX642P(X) <-> GBOX459P(X)) & (XBOX382P(X) <-> (BOX382P(X) & XBOX383P(X))) & (XBOX105F(X) <-> (BOX105F(X) & XBOX584F(X))) & (XBOX428P(X) <-> (BOX428P(X) & XBOX429P(X))) & (XBOX241F(X) <-> (BOX241F(X) & XE5G2F(X))) & (XBOX390P(X) <-> (BOX390P(X) & XBOX391P(X))) & (BOX340P(X) <-> GDIAMOND138P(X)) & (BOX552F(X) <-> GBOX553F(X)) & (BOX32F(X) <-> GBOX522F(X)) & (XBOX455P(X) <-> (BOX455P(X) & XPG9F)) & (XBOX545F(X) <-> (BOX545F(X) & XE3G7F(X))) & (BOX411P(X) <-> GE1G16P(X)) & (XBOX100F(X) <-> (BOX100F(X) & XBOX579F(X))) & (XBOX358P(X) <-> (BOX358P(X) & XBOX359P(X))) & (XBOX394P(X) <-> (BOX394P(X) & XBOX395P(X))) & (BOX646P(X) <-> GBOX463P(X)) & (BOX29F(X) <-> GBOX241F(X)) & (XBOX119F(X) <-> (BOX119F(X) & XBOX598F(X))) & (BOX286P(X) <-> GE1G7P(X)) & (XBOX476P(X) <-> (BOX476P(X) & XPL29F)) & (XBOX458P(X) <-> (BOX458P(X) & XPinvG20F)) & (BOX287P(X) <-> GE5G2P(X)) & (BOX577F(X) <-> GPL15F) & (XBOX193F(X) <-> (BOX193F(X) & XDIAMOND194F(X))) & (BOX333P(X) <-> GE1G17P(X)) & (BOX505F(X) <-> GBOX506F(X)) & (BOX673P(X) <-> GBOX490P(X)) & (XBOX444P(X) <-> (BOX444P(X) & XPinvG19F)) & (XBOX398P(X) <-> (BOX398P(X) & XBOX399P(X))) & (XBOX452P(X) <-> (BOX452P(X) & XPG18F)) & (XBOX325P(X) <-> (BOX325P(X) & XBOX326P(X))) & (XBOX349P(X) <-> (BOX349P(X) & X(BOX350P(X) & DIAMOND288P(X)))) & (BOX184F(X) <-> GBOX499F(X)) & (XBOX103F(X) <-> (BOX103F(X) & XBOX582F(X))) & (BOX80F(X) <-> GBOX559F(X)) & (XBOX206F(X) <-> (BOX206F(X) & XC25F(X))) & (BOX527F(X) <-> GDIAMOND198F(X)) & (BOX637P(X) <-> GBOX454P(X)) & (BOX586F(X) <-> GPinvG11F) & (BOX647P(X) <-> GBOX464P(X)) & (BOX627P(X) <-> GBOX444P(X)) & (XBOX412P(X) <-> (BOX412P(X) & XBOX413P(X))) & (XBOX321P(X) <-> (BOX321P(X) & XBOX322P(X))) & (XBOX559F(X) <-> (BOX559F(X) & XE4G8F(X))) & (XBOX609F(X) <-> (BOX609F(X) & X!E2G18F(X))) & (BOX427P(X) <-> GC11P(X)) & (BOX564F(X) <-> GPG4F) & (BOX419P(X) <-> GE2G9P(X)) & (BOX199F(X) <-> G!C4F(X)) & (XBOX175P(X) <-> (BOX175P(X) & XDIAMOND176P(X))) & (XBOX309P(X) <-> (BOX309P(X) & XDIAMOND310P(X))) & (BOX374P(X) <-> GE1G8P(X)) & (XBOX124F(X) <-> (BOX124F(X) & XBOX603F(X))) & (BOX385P(X) <-> GE3G14P(X)) & (XBOX410P(X) <-> (BOX410P(X) & XBOX411P(X))) & (XBOX78F(X) <-> (BOX78F(X) & XBOX558F(X))) & (XBOX141P(X) <-> (BOX141P(X) & XE1G23P(X))) & (BOX606F(X) <-> GPinvG12F) & (BOX146P(X) <-> GE1L26P(X)) & (BOX643P(X) <-> GBOX460P(X)) & (XBOX445P(X) <-> (BOX445P(X) & XPG27F)) & (BOX56F(X) <-> GBOX541F(X)) & (BOX71F(X) <-> GBOX551F(X)) & (BOX612P(X) <-> GDIAMOND129P(X)) & (BOX23F(X) <-> GBOX514F(X)) & (XBOX332P(X) <-> (BOX332P(X) & XBOX333P(X))) & (XBOX502F(X) <-> (BOX502F(X) & XE3G2F(X))) & (XBOX292P(X) <-> (BOX292P(X) & XBOX379P(X))) & (XBOX380P(X) <-> (BOX380P(X) & XBOX381P(X))) & (XBOX89F(X) <-> (BOX89F(X) & XBOX568F(X))) & (XBOX492F(X) <-> (BOX492F(X) & XDIAMOND228F(X))) & (BOX623P(X) <-> GC8P(X)) & (BOX580F(X) <-> GPL1F) & (BOX61F(X) <-> GBOX545F(X)) & (BOX614P(X) <-> GBOX327P(X)) & (XBOX408P(X) <-> (BOX408P(X) & XBOX409P(X))) & (BOX277P(X) <-> GBOX330P(X)) & (XBOX504F(X) <-> (BOX504F(X) & XDIAMOND189F(X))) & (BOX664P(X) <-> GBOX481P(X)) & (BOX4F(X) <-> GBOX495F(X)) & (BOX359P(X) <-> GE3G18P(X)) & (BOX365P(X) <-> GE2G5P(X)) & (BOX254F(X) <-> GE2G9F(X)) & (BOX617P(X) <-> G!E2G18P(X)) & (BOX634P(X) <-> GBOX451P(X)) & (XBOX430P(X) <-> (BOX430P(X) & XBOX431P(X))) & (BOX561F(X) <-> GPinvG19F) & (BOX613P(X) <-> GBOX614P(X)) & (XBOX232F(X) <-> (BOX232F(X) & XBOX498F(X))) & (XBOX471P(X) <-> (BOX471P(X) & XPinvL1F)) & (BOX592F(X) <-> GPG3F) & (BOX372P(X) <-> GE1G2P(X)) & (XBOX403P(X) <-> (BOX403P(X) & XBOX404P(X))) & (BOX378P(X) <-> GE4G17P(X)) & (BOX256F(X) <-> G(DIAMOND203F(X) & BOX539F(X))) & (XBOX525F(X) <-> (BOX525F(X) & XBOX526F(X))) & (XBOX101F(X) <-> (BOX101F(X) & XBOX580F(X))) & (XBOX468P(X) <-> (BOX468P(X) & XPinvG17F)) & (XBOX392P(X) <-> (BOX392P(X) & XBOX393P(X))) & (BOX657P(X) <-> GBOX474P(X)) & (XBOX486P(X) <-> (BOX486P(X) & XPinvG16F)) & (BOX395P(X) <-> GE2G20P(X)) & (XBOX495F(X) <-> (BOX495F(X) & XE1G27F(X))) & (BOX599F(X) <-> GPinvG25F) & (XBOX328P(X) <-> (BOX328P(X) & XBOX329P(X))) & (XBOX350P(X) <-> (BOX350P(X) & X(C17P(X) & E4L1P(X)))) & (XBOX96F(X) <-> (BOX96F(X) & XBOX575F(X))) & (XBOX368P(X) <-> (BOX368P(X) & XBOX287P(X))) & (BOX225F(X) <-> GDIAMOND266F(X)) & (XBOX608F(X) <-> (BOX608F(X) & XBOX496F(X))) & (BOX670P(X) <-> GBOX487P(X)) & (XBOX343P(X) <-> (BOX343P(X) & XBOX344P(X))) & (BOX635P(X) <-> GBOX452P(X)) & (XBOX432P(X) <-> (BOX432P(X) & XBOX433P(X))) & (XBOX330P(X) <-> (BOX330P(X) & XDIAMOND278P(X))) & (XBOX446P(X) <-> (BOX446P(X) & XPG2F)) & (XBOX5F(X) <-> (BOX5F(X) & XBOX608F(X))) & (BOX569F(X) <-> GPG18F) & (XBOX549F(X) <-> (BOX549F(X) & XE5G17F(X))) & (XBOX275P(X) <-> (BOX275P(X) & X(E4G25P(X) & C4P(X)))) & (XBOX360P(X) <-> (BOX360P(X) & XBOX361P(X))) & (BOX63F(X) <-> GBOX547F(X)) & (BOX663P(X) <-> GBOX480P(X)) & (XBOX431P(X) <-> (BOX431P(X) & XDIAMOND179P(X))) & (BOX41F(X) <-> GBOX532F(X)) & (XBOX362P(X) <-> (BOX362P(X) & XBOX363P(X))) & (BOX648P(X) <-> GBOX465P(X)) & (BOX666P(X) <-> GBOX483P(X)) & (XBOX448P(X) <-> (BOX448P(X) & XPinvG8F)) & (BOX570F(X) <-> GPG28F) & (XBOX501F(X) <-> (BOX501F(X) & XE3G11F(X))) & (BOX231F(X) <-> G(E4G25F(X) & C4F(X))) & (XBOX150P(X) <-> (BOX150P(X) & X!C4P(X))) & (XBOX531F(X) <-> (BOX531F(X) & XE2G29F(X))) & (BOX409P(X) <-> GE1G14P(X)) & (XBOX178P(X) <-> (BOX178P(X) & XBOX430P(X))) & (XBOX125F(X) <-> (BOX125F(X) & XBOX604F(X))) & (BOX560F(X) <-> GPL26F) & (BOX672P(X) <-> GBOX489P(X)) & (BOX11F(X) <-> GBOX501F(X)) & (XBOX547F(X) <-> (BOX547F(X) & XE5G4F(X))) & (XBOX443P(X) <-> (BOX443P(X) & XPL26F)) & (XBOX94F(X) <-> (BOX94F(X) & XBOX573F(X))) & (BOX335P(X) <-> GE3G11P(X)) & (XBOX341P(X) <-> (BOX341P(X) & XBOX342P(X))) & (XBOX514F(X) <-> (BOX514F(X) & XE1G3F(X))) & (BOX391P(X) <-> GE4G12P(X)) & (BOX587F(X) <-> GPinvL29F) & (XBOX115F(X) <-> (BOX115F(X) & XBOX594F(X))) & (BOX389P(X) <-> GE2G29P(X)) & (BOX566F(X) <-> GPG20F) & (XBOX493F(X) <-> (BOX493F(X) & XE1G4F(X))) & (BOX573F(X) <-> GPinvG27F) & (XBOX516F(X) <-> (BOX516F(X) & XE1G28F(X))) & (BOX339P(X) <-> GE1G19P(X)) & (XBOX334P(X) <-> (BOX334P(X) & XBOX335P(X))) & (XBOX528F(X) <-> (BOX528F(X) & XE1G12F(X))) & (XBOX92F(X) <-> (BOX92F(X) & XBOX571F(X))) & (XBOX338P(X) <-> (BOX338P(X) & XBOX339P(X))) & (XBOX454P(X) <-> (BOX454P(X) & XPinvG5F)) & (BOX588F(X) <-> GPinvL1F) & (BOX45F(X) <-> GBOX535F(X)) & (BOX383P(X) <-> GE1G12P(X)) & (BOX591F(X) <-> GPG5F) & (BOX344P(X) <-> GE1G20P(X)) & (XBOX538F(X) <-> (BOX538F(X) & XE2G3F(X))) & (BOX10F(X) <-> GBOX500F(X)) & (BOX576F(X) <-> GPG7F) & (XBOX396P(X) <-> (BOX396P(X) & XBOX397P(X))) & (BOX615P(X) <-> GDIAMOND293P(X)) & (BOX246F(X) <-> GBOX525F(X)) & (BOX417P(X) <-> GE3G7P(X)) & (XBOX550F(X) <-> (BOX550F(X) & XC11F(X))) & (BOX625P(X) <-> GBOX440P(X)) & (XBOX375P(X) <-> (BOX375P(X) & XBOX376P(X))) & (BOX12F(X) <-> GBOX502F(X)) & (XBOX113F(X) <-> (BOX113F(X) & XBOX592F(X))) & (XBOX487P(X) <-> (BOX487P(X) & XPinvG23F)) & (BOX667P(X) <-> GBOX484P(X)) & (BOX423P(X) <-> GE1G23P(X)) & (BOX39F(X) <-> GBOX530F(X)) & (XBOX482P(X) <-> (BOX482P(X) & XPinvG25F)) & (BOX626P(X) <-> GBOX443P(X)) & (BOX50F(X) <-> GBOX537F(X)) & (XBOX536F(X) <-> (BOX536F(X) & XE1G9F(X))) & (XBOX460P(X) <-> (BOX460P(X) & XPL15F)) & (BOX662P(X) <-> GBOX479P(X)) & (XBOX519F(X) <-> (BOX519F(X) & XE4G9F(X))) & (XBOX508F(X) <-> (BOX508F(X) & XE4G14F(X))) & (BOX370P(X) <-> GE1G5P(X)) & (XBOX494F(X) <-> (BOX494F(X) & XE1G18F(X))) & (BOX30F(X) <-> GBOX520F(X)) & (XBOX319P(X) <-> (BOX319P(X) & XDIAMOND269P(X))) & (XBOX462P(X) <-> (BOX462P(X) & XPinvG14F)) & (XBOX434P(X) <-> (BOX434P(X) & XBOX435P(X))) & (XBOX463P(X) <-> (BOX463P(X) & XPL1F)) & (XBOX88F(X) <-> (BOX88F(X) & XBOX567F(X))) & (XBOX314P(X) <-> (BOX314P(X) & X!C13P(X))) & (BOX602F(X) <-> GPG12F) & (BOX641P(X) <-> GBOX458P(X)) & (XBOX402P(X) <-> (BOX402P(X) & X(E1G8P(X) & E3G14P(X)))) & (XBOX511F(X) <-> (BOX511F(X) & XE3G27F(X))) & (XBOX366P(X) <-> (BOX366P(X) & XBOX367P(X))) & (XBOX354P(X) <-> (BOX354P(X) & XC13P(X))) & (XBOX327P(X) <-> (BOX327P(X) & X(E4G4P(X) & DIAMOND272P(X) & DIAMOND273P(X)))) & (BOX363P(X) <-> GE3G4P(X)) & (XBOX481P(X) <-> (BOX481P(X) & XPinvL15F)) & (BOX67F(X) <-> GBOX549F(X)) & (BOX379P(X) <-> GBOX380P(X)) & (BOX34F(X) <-> GBOX524F(X)) & (BOX2F(X) <-> GBOX493F(X)) & (BOX654P(X) <-> GBOX471P(X)) & (BOX58F(X) <-> GBOX543F(X)) & (BOX589F(X) <-> GPG16F) & (XBOX470P(X) <-> (BOX470P(X) & XPinvL29F)) & (BOX544F(X) <-> G(!C1F(X) & DIAMOND207F(X))) & (BOX33F(X) <-> GBOX523F(X)) & (BOX324P(X) <-> GE1G18P(X)) & (XBOX318P(X) <-> (BOX318P(X) & X(BOX319P(X) & BOX320P(X)))) & (BOX660P(X) <-> GBOX477P(X)) & (BOX605F(X) <-> GPinvG7F) & (BOX260F(X) <-> GDIAMOND261F(X)) & (XBOX449P(X) <-> (BOX449P(X) & XPG20F)) & (XBOX181P(X) <-> (BOX181P(X) & XDIAMOND315P(X))) & (BOX192F(X) <-> GE1G23F(X)) & (XBOX36F(X) <-> (BOX36F(X) & XDIAMOND247F(X))) & (BOX600F(X) <-> GPG25F) & (BOX604F(X) <-> GPinvG23F) & (BOX62F(X) <-> GBOX546F(X)) & (XBOX373P(X) <-> (BOX373P(X) & XBOX374P(X))) & (XBOX556F(X) <-> (BOX556F(X) & XE3G28F(X))) & (BOX43F(X) <-> GBOX534F(X)) & (XBOX424P(X) <-> (BOX424P(X) & XBOX425P(X))) & (BOX361P(X) <-> GE1G28P(X)) & (XBOX465P(X) <-> (BOX465P(X) & XPG17F)) & (XBOX196F(X) <-> (BOX196F(X) & XE1L26F(X))) & (XBOX82F(X) <-> (BOX82F(X) & XBOX561F(X))) & (XBOX490P(X) <-> (BOX490P(X) & XPinvG9F)) & (BOX7F(X) <-> GBOX497F(X)) & (BOX159P(X) <-> GC25P(X)) & (XBOX474P(X) <-> (BOX474P(X) & XPG5F)) & (XBOX351P(X) <-> (BOX351P(X) & XBOX352P(X))) & (XBOX420P(X) <-> (BOX420P(X) & XBOX421P(X))) & (XBOX457P(X) <-> (BOX457P(X) & XPinvG4F)) & (XBOX542F(X) <-> (BOX542F(X) & XE1G16F(X))) & (BOX619P(X) <-> GBOX620P(X)) & (BOX139P(X) <-> GBOX341P(X)) & (BOX433P(X) <-> GE3G25P(X)) & (XBOX464P(X) <-> (BOX464P(X) & XPinvG3F)) & (XBOX364P(X) <-> (BOX364P(X) & XBOX365P(X))) & (BOX3F(X) <-> GBOX494F(X)) & (BOX535F(X) <-> GDIAMOND250F(X)) & (XBOX500F(X) <-> (BOX500F(X) & XE1G17F(X))) & (BOX387P(X) <-> GE2G18P(X)) & (BOX367P(X) <-> GE4G9P(X)) & (BOX645P(X) <-> GBOX462P(X)) & (XBOX300P(X) <-> (BOX300P(X) & XE2G9P(X))) & (XBOX447P(X) <-> (BOX447P(X) & XPG4F)) & (BOX584F(X) <-> GPG14F) & (XBOX248F(X) <-> (BOX248F(X) & X(C12F(X) & C10F(X) & DIAMOND249F(X)))) & (XBOX110F(X) <-> (BOX110F(X) & XBOX589F(X))) & (XBOX51F(X) <-> (BOX51F(X) & XBOX610F(X))) & (XBOX485P(X) <-> (BOX485P(X) & XPG12F)) & (XBOX532F(X) <-> (BOX532F(X) & XE4G12F(X))) & (BOX659P(X) <-> GBOX476P(X)) & (XBOX546F(X) <-> (BOX546F(X) & XE2G9F(X))) & (BOX376P(X) <-> GE5G29P(X)) & (XBOX467P(X) <-> (BOX467P(X) & XPG14F)) & (BOX582F(X) <-> GPG17F) & (BOX630P(X) <-> GBOX447P(X)) & (BOX590F(X) <-> GPG23F) & (BOX526F(X) <-> GBOX527F(X)) & (XBOX126F(X) <-> (BOX126F(X) & XBOX605F(X))) & (XBOX68F(X) <-> (BOX68F(X) & X(DIAMOND217F(X) & DIAMOND218F(X)))) & (XBOX480P(X) <-> (BOX480P(X) & XPG8F)) & (BOX638P(X) <-> GBOX455P(X)) & (BOX665P(X) <-> GBOX482P(X)) & (BOX616P(X) <-> G(BOX617P(X) & DIAMOND297P(X))) & (BOX649P(X) <-> GBOX466P(X)) & (XBOX478P(X) <-> (BOX478P(X) & XPinvG28F)) & (XBOX416P(X) <-> (BOX416P(X) & XBOX417P(X))) & (XBOX331P(X) <-> (BOX331P(X) & XE2G20P(X))) & (BOX77F(X) <-> GBOX557F(X)) & (XBOX102F(X) <-> (BOX102F(X) & XBOX581F(X))) & (XBOX132P(X) <-> (BOX132P(X) & XBOX331P(X))) & (XBOX106F(X) <-> (BOX106F(X) & XBOX585F(X))) & (BOX0F(X) <-> G(BOX491F(X) & BOX492F(X))) & (BOX578F(X) <-> GPG11F) & (XBOX49F(X) <-> (BOX49F(X) & XDIAMOND253F(X))) & (XBOX98F(X) <-> (BOX98F(X) & XBOX577F(X))) & (XBOX1F(X) <-> (BOX1F(X) & XDIAMOND182F(X))) & (BOX38F(X) <-> GBOX529F(X)) & (BOX393P(X) <-> GE1G29P(X)) & (XBOX539F(X) <-> (BOX539F(X) & XBOX540F(X))) & (XBOX283P(X) <-> (BOX283P(X) & XBOX340P(X))) & (BOX143P(X) <-> GDIAMOND144P(X)) & (BOX498F(X) <-> GDIAMOND233F(X)) & (XBOX456P(X) <-> (BOX456P(X) & XPinvG27F)) & (XBOX400P(X) <-> (BOX400P(X) & XBOX286P(X))) & (BOX598F(X) <-> GPinvL15F) & (XBOX127F(X) <-> (BOX127F(X) & XBOX606F(X))) & (BOX442P(X) <-> GE4G8P(X)) & (XBOX515F(X) <-> (BOX515F(X) & XE3G18F(X))) & (BOX294P(X) <-> G(C12P(X) & C10P(X) & DIAMOND295P(X))) & (BOX75F(X) <-> GBOX555F(X)) & (BOX322P(X) <-> GE1G4P(X)) & (BOX16F(X) <-> GBOX507F(X)) & (BOX620P(X) <-> GBOX621P(X)) & (BOX631P(X) <-> GBOX448P(X)) & (BOX607F(X) <-> GPinvG9F) & (BOX656P(X) <-> GBOX473P(X)) & (BOX55F(X) <-> GC28F(X)) & (XBOX541F(X) <-> (BOX541F(X) & XE1G14F(X))) & (BOX568F(X) <-> GPinvG2F) & (XBOX190F(X) <-> (BOX190F(X) & XBOX505F(X))) & (BOX496F(X) <-> G(E4G4F(X) & DIAMOND229F(X) & DIAMOND230F(X))) & (XBOX91F(X) <-> (BOX91F(X) & XBOX570F(X))) & (BOX671P(X) <-> GBOX488P(X)) & (XBOX513F(X) <-> (BOX513F(X) & XDIAMOND245F(X))) & (BOX421P(X) <-> GE5G4P(X)) & (BOX595F(X) <-> GPinvG28F) & (BOX624P(X) <-> GDIAMOND312P(X)) & (XBOX86F(X) <-> (BOX86F(X) & XBOX565F(X))) & (XBOX407P(X) <-> (BOX407P(X) & XC28P(X))) & (BOX37F(X) <-> GBOX528F(X)) & (BOX574F(X) <-> GPinvG4F) & (XBOX69F(X) <-> (BOX69F(X) & XC8F(X))) & (BOX52F(X) <-> GBOX538F(X)) & (XBOX554F(X) <-> (BOX554F(X) & XE3G25F(X))) & (XBOX415P(X) <-> (BOX415P(X) & X(!C1P(X) & DIAMOND160P(X)))) & (XBOX450P(X) <-> (BOX450P(X) & XPinvG29F)) & (BOX603F(X) <-> GPinvG16F) & (XBOX371P(X) <-> (BOX371P(X) & XBOX372P(X))) & (BOX76F(X) <-> GBOX556F(X)) & (BOX594F(X) <-> GPinvG18F) & (BOX42F(X) <-> GBOX533F(X)) & (BOX13F(X) <-> GBOX503F(X)) & (XBOX534F(X) <-> (BOX534F(X) & XE2G20F(X))) & (BOX658P(X) <-> GBOX475P(X)) & (BOX237F(X) <-> GBOX504F(X)) & (BOX628P(X) <-> GBOX445P(X)) & (BOX28F(X) <-> GBOX519F(X)) & (BOX558F(X) <-> G(C21F(X) & E3G28F(X) & !E5G17F(X) & C15F(X))) & (XBOX518F(X) <-> (BOX518F(X) & XE2G5F(X))) & (BOX346P(X) <-> GE4G14P(X)) & (XBOX522F(X) <-> (BOX522F(X) & XE1G8F(X))) & (BOX644P(X) <-> GBOX461P(X)) & (XBOX523F(X) <-> (BOX523F(X) & XE5G29F(X))) & (BOX74F(X) <-> GBOX554F(X)) & (BOX622P(X) <-> G(DIAMOND171P(X) & DIAMOND172P(X))) & (BOX510F(X) <-> G(C17F(X) & E4L1F(X))) & (BOX70F(X) <-> G(C24F(X) & BOX550F(X) & E4G17F(X) & DIAMOND262F(X))) & (XBOX122F(X) <-> (BOX122F(X) & XBOX601F(X))) & (BOX48F(X) <-> GBOX240F(X)) & (BOX437P(X) <-> GE3G28P(X)) & (BOX27F(X) <-> GBOX518F(X)) & (XBOX93F(X) <-> (BOX93F(X) & XBOX572F(X))) & (XBOX114F(X) <-> (BOX114F(X) & XBOX593F(X))) & (XBOX524F(X) <-> (BOX524F(X) & XE4G17F(X))) & (XBOX270P(X) <-> (BOX270P(X) & X!E3G11P(X))) & (BOX413P(X) <-> G(E4G25P(X) & DIAMOND306P(X))) & (XBOX414P(X) <-> (BOX414P(X) & XBOX415P(X))) & (XBOX369P(X) <-> (BOX369P(X) & XBOX370P(X))) & (XBOX517F(X) <-> (BOX517F(X) & XE3G4F(X))) & (XBOX120F(X) <-> (BOX120F(X) & XBOX599F(X))) & (BOX652P(X) <-> GBOX469P(X)) & (XBOX90F(X) <-> (BOX90F(X) & XBOX569F(X))) & (BOX26F(X) <-> GBOX517F(X)) & (BOX337P(X) <-> GE3G2P(X)) & (XBOX426P(X) <-> (BOX426P(X) & X(C24P(X) & BOX427P(X) & E4G17P(X) & DIAMOND311P(X)))) & (BOX405P(X) <-> GBOX406P(X)) & (BOX655P(X) <-> GBOX472P(X)) & (XBOX521F(X) <-> (BOX521F(X) & XE1G2F(X))) & (BOX20F(X) <-> GBOX511F(X)) & (XBOX497F(X) <-> (BOX497F(X) & XE1G25F(X))) & (BOX661P(X) <-> GBOX478P(X)) & (XBOX118F(X) <-> (BOX118F(X) & XBOX597F(X))) & (XBOX475P(X) <-> (BOX475P(X) & XPG3F)) & (BOX25F(X) <-> GBOX516F(X)) & (BOX572F(X) <-> GPG9F) & (BOX57F(X) <-> GBOX542F(X)) & (XBOX128F(X) <-> (BOX128F(X) & XBOX607F(X))) & (BOX632P(X) <-> GBOX449P(X)) & (BOX31F(X) <-> GBOX521F(X)) & (BOX60F(X) <-> GBOX544F(X)) & (XBOX555F(X) <-> (BOX555F(X) & XE4G4F(X))) & (XBOX484P(X) <-> (BOX484P(X) & XPinvL26F)) & (BOX223F(X) <-> GBOX552F(X)) & (XBOX451P(X) <-> (BOX451P(X) & XPinvG2F)) & (XBOX95F(X) <-> (BOX95F(X) & XBOX574F(X))) & (XBOX610F(X) <-> (BOX610F(X) & XBOX611F(X))) & (XBOX381P(X) <-> (BOX381P(X) & XDIAMOND149P(X))) & (BOX562F(X) <-> GPG27F) & (XBOX121F(X) <-> (BOX121F(X) & XBOX600F(X))) & (XBOX459P(X) <-> (BOX459P(X) & XPG7F)) & (BOX355P(X) <-> GDIAMOND291P(X)) & (XBOX479P(X) <-> (BOX479P(X) & XPG19F)) & (BOX537F(X) <-> G(E1G8F(X) & E3G14F(X))) & (XBOX543F(X) <-> (BOX543F(X) & X(E4G25F(X) & DIAMOND258F(X)))) & (BOX575F(X) <-> GPinvG20F) & (XBOX422P(X) <-> (BOX422P(X) & XBOX423P(X))) & (XBOX46F(X) <-> (BOX46F(X) & X(BOX609F(X) & DIAMOND251F(X)))) & (XBOX109F(X) <-> (BOX109F(X) & XBOX588F(X))) & (XBOX116F(X) <-> (BOX116F(X) & XBOX595F(X))) & (BOX596F(X) <-> GPG19F) & (XBOX401P(X) <-> (BOX401P(X) & XBOX402P(X))) & (BOX227F(X) <-> G!E3G11F(X)) & (XBOX611F(X) <-> (BOX611F(X) & X(DIAMOND202F(X) & DIAMOND255F(X)))) & (XBOX477P(X) <-> (BOX477P(X) & XPinvG18F)) & (XBOX488P(X) <-> (BOX488P(X) & XPinvG7F)) & (XBOX83F(X) <-> (BOX83F(X) & XBOX562F(X))) & (BOX553F(X) <-> GDIAMOND224F(X)) & (BOX636P(X) <-> GBOX453P(X)) & (BOX565F(X) <-> GPinvG8F) & (XBOX347P(X) <-> (BOX347P(X) & XDIAMOND284P(X))) & (XBOX461P(X) <-> (BOX461P(X) & XPG11F)) & (XBOX489P(X) <-> (BOX489P(X) & XPinvG12F)) & (XBOX548F(X) <-> (BOX548F(X) & XE1G23F(X))) & (XBOX84F(X) <-> (BOX84F(X) & XBOX563F(X))) & (XBOX353P(X) <-> (BOX353P(X) & X(BOX354P(X) & DIAMOND290P(X) & BOX355P(X)))) & (XBOX356P(X) <-> (BOX356P(X) & XBOX357P(X))) & (XBOX406P(X) <-> (BOX406P(X) & XE3G25P(X))) & (BOX47F(X) <-> GBOX536F(X)) & (XBOX533F(X) <-> (BOX533F(X) & XE1G29F(X))) & (BOX629P(X) <-> GBOX446P(X)) & (BOX265F(X) <-> G!C13F(X)) & (XBOX123F(X) <-> (BOX123F(X) & XBOX602F(X))) & (BOX404P(X) <-> GE2G3P(X)) & (BOX581F(X) <-> GPinvG3F) & (BOX583F(X) <-> GPG29F) & (BOX435P(X) <-> GE4G4P(X)) & (XBOX466P(X) <-> (BOX466P(X) & XPG29F)) & (BOX593F(X) <-> GPL29F) & (XBOX551F(X) <-> (BOX551F(X) & XE1G11F(X))) & (XBOX117F(X) <-> (BOX117F(X) & XBOX596F(X))) & (XBOX323P(X) <-> (BOX323P(X) & XBOX324P(X))) & (BOX342P(X) <-> GDIAMOND140P(X)) & (XBOX441P(X) <-> (BOX441P(X) & XBOX442P(X))) & (BOX491F(X) <-> GDIAMOND226F(X)) & (BOX597F(X) <-> GPG8F) & (XBOX345P(X) <-> (BOX345P(X) & XBOX346P(X))) & (BOX19F(X) <-> GBOX509F(X)) & (XBOX440P(X) <-> (BOX440P(X) & X(C21P(X) & E3G28P(X) & !E5G17P(X) & C15P(X)))) & (XBOX303P(X) <-> (BOX303P(X) & X(DIAMOND155P(X) & BOX405P(X)))) & (BOX651P(X) <-> GBOX468P(X)) & (BOX601F(X) <-> GPinvL26F) & (BOX399P(X) <-> GE1G9P(X)) & (BOX668P(X) <-> GBOX485P(X)) & (BOX571F(X) <-> GPinvG5F) & (XBOX506F(X) <-> (BOX506F(X) & XDIAMOND191F(X))) & (BOX540F(X) <-> GE3G25F(X)) & (XBOX104F(X) <-> (BOX104F(X) & XBOX583F(X))))


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


Generating model LTL file...
Num of Propositions: 41952
Solver...NuSMV
SolverAalta
Solverpltl
SolverTRP++UC
Generating FO file...
Done! Total time:2339ms