Tbox:  ( O O O H O G C27 /\ F >= 2.G20 )  << F  ( H G  ( >= 5.G11 /\ F >= 1.G5 )  /\ !>= 3.G10 ) 
Tbox: H O F O  ( C1 /\ O O !C9 )  << G G G G O G G  ( C21 /\ C17 ) 
Tbox: G  ( G G >= 1.G6 /\ G  ( C7 /\ H >= 5.G17 )  )  << G  ( F O O >= 5.G5 /\ F F G C7 ) 
Tbox: O H H H O F H H H >= 4.G10 << G O  ( G >= 1.G21 /\ O H H F >= 5.G14 ) 
Tbox: H G  ( G F O G C20 /\ F >= 3.G1 )  << O O O O H G O O H C0
Tbox: H H O H F  ( >= 3.G13 /\ O H C12 )  << F O F G  ( G O >= 5.G2 /\ F >= 1.G4 ) 
Tbox: O G G G F G F F O >= 2.G21 << H O H  ( H G O C12 /\ !>= 3.G8 ) 
Tbox: O F O  ( F H O >= 2.G21 /\ H >= 4.L6 )  << H G O F O G F G O C11
Tbox:  ( G >= 4.G4 /\ O H F  ( >= 4.G10 /\ O C29 )  )  << H F F O  ( H >= 4.G7 /\ O H >= 1.G14 ) 
Tbox: H F F F H F H H !C26 << O O H H O  ( >= 5.G28 /\ G !>= 3.G9 ) 
Tbox: G G  ( G H G C26 /\ G F C9 )  << G F F H G H O G F >= 2.G13
Tbox: H G G H O F F G !>= 4.G0 <<  ( F  ( G >= 1.G16 /\ F C2 )  /\ O O >= 5.G27 ) 
Tbox: G G  ( H O C27 /\ H F H >= 5.G18 )  << G H H G H H H O H >= 1.G5
Tbox: O G O O F F O H O >= 4.G13 << F F G F H O G F F C25
Tbox: O G H F F  ( !C28 /\ H C6 )  << H F O F  ( H >= 5.G28 /\ F O C5 ) 
Qrole:>= 1.G14
Qrole1:>= 1.G14
Qrole:>= 1.G16
Qrole1:>= 1.G16
Qrole:>= 5.G11
Qrole1:>= 1.G11
Qrole:>= 5.G14
Qrole1:>= 1.G14
Qrole:>= 5.G2
Qrole1:>= 1.G2
Qrole:>= 4.L6
Qrole1:>= 1.L6
Qrole:>= 3.G1
Qrole1:>= 1.G1
Qrole:>= 5.G17
Qrole1:>= 1.G17
Qrole:>= 5.G18
Qrole1:>= 1.G18
Qrole:>= 1.G4
Qrole1:>= 1.G4
Qrole:>= 3.G8
Qrole1:>= 1.G8
Qrole:>= 3.G9
Qrole1:>= 1.G9
Qrole:>= 2.G13
Qrole1:>= 1.G13
Qrole:>= 5.G5
Qrole1:>= 1.G5
Qrole:>= 1.G6
Qrole1:>= 1.G6
Qrole:>= 1.G5
Qrole1:>= 1.G5
Qrole:>= 1.G21
Qrole1:>= 1.G21
Qrole:>= 3.G13
Qrole1:>= 1.G13
Qrole:>= 3.G10
Qrole1:>= 1.G10
Qrole:>= 4.G0
Qrole1:>= 1.G0
Qrole:>= 5.G27
Qrole1:>= 1.G27
Qrole:>= 5.G28
Qrole1:>= 1.G28
Qrole:>= 4.G10
Qrole1:>= 1.G10
Qrole:>= 4.G13
Qrole1:>= 1.G13
Qrole:>= 4.G4
Qrole1:>= 1.G4
Qrole:>= 2.G20
Qrole1:>= 1.G20
Qrole:>= 4.G7
Qrole1:>= 1.G7
Qrole:>= 2.G21
Qrole1:>= 1.G21
Rerformulation: ((E4G10F(X) -> BOX0F(X)) & (DIAMOND1F(X) -> DIAMOND2F(X)) & (E2G20F(X) -> E1G20F(X)) & (E3G10F(X) -> BOX3F(X)) & (E3G1F(X) -> E1G1F(X)) & (E1G9F(X) -> BOX4F(X)) & (BOX5F(X) -> BOX6F(X)) & (E1G27F(X) -> BOX7F(X)) & (E2G21F(X) -> BOX8F(X)) & (E5G27F(X) -> E1G27F(X)) & ((BOX9F(X) & DIAMOND10F(X)) -> BOX11F(X)) & (E1G16F(X) -> BOX12F(X)) & (E1G13F(X) -> BOX13F(X)) & (BOX14F(X) -> DIAMOND15F(X)) & (E3G9F(X) -> BOX16F(X)) & (E4G0F(X) -> E1G0F(X)) & (E5G27F(X) -> BOX17F(X)) & (E2G13F(X) -> E1G13F(X)) & (BOX18F(X) -> DIAMOND19F(X)) & (E5G11F(X) -> E1G11F(X)) & (E1G20F(X) -> BOX20F(X)) & (DIAMOND21F(X) -> BOX22F(X)) & (E1G11F(X) -> BOX23F(X)) & (E1G28F(X) -> BOX24F(X)) & (BOX25F(X) -> BOX26F(X)) & (E3G13F(X) -> BOX27F(X)) & (E1G1F(X) -> BOX28F(X)) & (E5G5F(X) -> E1G5F(X)) & (E4G13F(X) -> BOX29F(X)) & (E5G11F(X) -> BOX30F(X)) & (E5G28F(X) -> E1G28F(X)) & ((DIAMOND31F(X) & DIAMOND32F(X)) -> DIAMOND33F(X)) & (E1G17F(X) -> BOX34F(X)) & (E3G1F(X) -> BOX35F(X)) & (E4G4F(X) -> E1G4F(X)) & (E5G18F(X) -> BOX36F(X)) & (E1G4F(X) -> BOX37F(X)) & (E1G0F(X) -> BOX38F(X)) & (E5G14F(X) -> E1G14F(X)) & (E1G10F(X) -> BOX39F(X)) & (E1G7F(X) -> BOX40F(X)) & (E2G21F(X) -> E1G21F(X)) & (E5G2F(X) -> BOX41F(X)) & (E3G13F(X) -> E2G13F(X)) & (BOX42F(X) -> BOX43F(X)) & (E5G5F(X) -> BOX44F(X)) & (E4G7F(X) -> BOX45F(X)) & (E5G18F(X) -> E1G18F(X)) & (E5G17F(X) -> BOX46F(X)) & (E1G14F(X) -> BOX47F(X)) & (E1G21F(X) -> BOX48F(X)) & (E4G10F(X) -> E3G10F(X)) & (DIAMOND49F(X) -> BOX50F(X)) & (E1G8F(X) -> BOX51F(X)) & (E4G7F(X) -> E1G7F(X)) & (E1G18F(X) -> BOX52F(X)) & (E5G14F(X) -> BOX53F(X)) & (BOX54F(X) -> BOX55F(X)) & (E1G5F(X) -> BOX56F(X)) & (E3G8F(X) -> E1G8F(X)) & (BOX57F(X) -> DIAMOND58F(X)) & (E2G20F(X) -> BOX59F(X)) & (E4L6F(X) -> E1L6F(X)) & (E3G8F(X) -> BOX60F(X)) & (E4G4F(X) -> BOX61F(X)) & (E4G13F(X) -> E3G13F(X)) & (E2G13F(X) -> BOX62F(X)) & (DIAMOND63F(X) -> BOX64F(X)) & (E1G6F(X) -> BOX65F(X)) & (E5G17F(X) -> E1G17F(X)) & (E4G0F(X) -> BOX66F(X)) & (DIAMOND67F(X) -> BOX68F(X)) & (E5G28F(X) -> BOX69F(X)) & (E3G10F(X) -> E1G10F(X)) & (E3G9F(X) -> E1G9F(X)) & (E1G2F(X) -> BOX70F(X)) & (BOX71F(X) -> (DIAMOND72F(X) & DIAMOND73F(X))) & (E5G2F(X) -> E1G2F(X)) & (E1G7InvF(X) -> BOX74F(X)) & (E1G4InvF(X) -> BOX75F(X)) & (E1G18InvF(X) -> BOX76F(X)) & (E1G9F(X) -> BOX77F(X)) & (E1G18F(X) -> BOX78F(X)) & (E1G20F(X) -> BOX79F(X)) & (E1G5InvF(X) -> BOX80F(X)) & (E1G28F(X) -> BOX81F(X)) & (E1G27InvF(X) -> BOX82F(X)) & (E1G13F(X) -> BOX83F(X)) & (E1G28InvF(X) -> BOX84F(X)) & (E1G16F(X) -> BOX85F(X)) & (E1G2F(X) -> BOX86F(X)) & (E1G6InvF(X) -> BOX87F(X)) & (E1G17InvF(X) -> BOX88F(X)) & (E1G9InvF(X) -> BOX89F(X)) & (E1G8F(X) -> BOX90F(X)) & (E1G11InvF(X) -> BOX91F(X)) & (E1G8InvF(X) -> BOX92F(X)) & (E1G0F(X) -> BOX93F(X)) & (E1G13InvF(X) -> BOX94F(X)) & (E1G2InvF(X) -> BOX95F(X)) & (E1G6F(X) -> BOX96F(X)) & (E1G17F(X) -> BOX97F(X)) & (E1G27F(X) -> BOX98F(X)) & (E1L6F(X) -> BOX99F(X)) & (E1G7F(X) -> BOX100F(X)) & (E1G11F(X) -> BOX101F(X)) & (E1G10F(X) -> BOX102F(X)) & (E1G4F(X) -> BOX103F(X)) & (E1G16InvF(X) -> BOX104F(X)) & (E1G21F(X) -> BOX105F(X)) & (E1G5F(X) -> BOX106F(X)) & (E1G10InvF(X) -> BOX107F(X)) & (E1G20InvF(X) -> BOX108F(X)) & (E1G21InvF(X) -> BOX109F(X)) & (E1G14F(X) -> BOX110F(X)) & (E1L6InvF(X) -> BOX111F(X)) & (E1G0InvF(X) -> BOX112F(X)) & (E1G1InvF(X) -> BOX113F(X)) & (E1G14InvF(X) -> BOX114F(X)) & (E1G1F(X) -> BOX115F(X)))


Modal Equiv Pure Future: G((XDIAMOND246F(X) <-> (DIAMOND246F(X) | XC5F(X))) & (XDIAMOND130P(X) <-> (DIAMOND130P(X) | XE2G13P(X))) & (DIAMOND232F(X) <-> FBOX233F(X)) & (XDIAMOND116P(X) <-> (DIAMOND116P(X) | XDIAMOND117P(X))) & (DIAMOND397P(X) <-> FC11P(X)) & (XDIAMOND301F(X) <-> (DIAMOND301F(X) | XDIAMOND302F(X))) & (DIAMOND389P(X) <-> F(BOX390P(X) & DIAMOND391P(X))) & (DIAMOND201F(X) <-> FBOX202F(X)) & (DIAMOND365P(X) <-> FE5G5P(X)) & (DIAMOND243F(X) <-> F(BOX244F(X) & DIAMOND245F(X))) & (XDIAMOND140P(X) <-> (DIAMOND140P(X) | XDIAMOND141P(X))) & (XDIAMOND211F(X) <-> (DIAMOND211F(X) | XC29F(X))) & (DIAMOND353P(X) <-> FBOX354P(X)) & (XDIAMOND172P(X) <-> (DIAMOND172P(X) | X(E3G13P(X) & DIAMOND173P(X)))) & (XDIAMOND300F(X) <-> (DIAMOND300F(X) | XE5G5F(X))) & (DIAMOND358P(X) <-> F(E5G28P(X) & BOX359P(X))) & (XDIAMOND186P(X) <-> (DIAMOND186P(X) | XDIAMOND187P(X))) & (DIAMOND355P(X) <-> FDIAMOND356P(X)) & (DIAMOND267F(X) <-> FBOX268F(X)) & (XDIAMOND31F(X) <-> (DIAMOND31F(X) | XDIAMOND301F(X))) & (DIAMOND217F(X) <-> FE3G1F(X)) & (XDIAMOND120P(X) <-> (DIAMOND120P(X) | XBOX121P(X))) & (XDIAMOND320F(X) <-> (DIAMOND320F(X) | XDIAMOND255F(X))) & (DIAMOND2F(X) <-> FDIAMOND199F(X)) & (XDIAMOND166P(X) <-> (DIAMOND166P(X) | X(BOX167P(X) & DIAMOND168P(X)))) & (DIAMOND173P(X) <-> FBOX384P(X)) & (XDIAMOND188P(X) <-> (DIAMOND188P(X) | XBOX189P(X))) & (XDIAMOND323F(X) <-> (DIAMOND323F(X) | XBOX324F(X))) & (DIAMOND197F(X) <-> FDIAMOND198F(X)) & (DIAMOND219F(X) <-> FDIAMOND220F(X)) & (XDIAMOND216F(X) <-> (DIAMOND216F(X) | XBOX284F(X))) & (DIAMOND135P(X) <-> F(BOX343P(X) & DIAMOND344P(X))) & (XDIAMOND250F(X) <-> (DIAMOND250F(X) | XBOX317F(X))) & (DIAMOND386P(X) <-> FBOX387P(X)) & (XDIAMOND136P(X) <-> (DIAMOND136P(X) | XDIAMOND137P(X))) & (DIAMOND212F(X) <-> FDIAMOND213F(X)) & (DIAMOND341P(X) <-> FBOX342P(X)) & (DIAMOND235F(X) <-> FE1G5F(X)) & (DIAMOND187P(X) <-> FBOX396P(X)) & (DIAMOND241F(X) <-> FDIAMOND242F(X)) & (XDIAMOND63F(X) <-> (DIAMOND63F(X) | XBOX319F(X))) & (DIAMOND203F(X) <-> FDIAMOND204F(X)) & (XDIAMOND133P(X) <-> (DIAMOND133P(X) | XDIAMOND134P(X))) & (XDIAMOND122P(X) <-> (DIAMOND122P(X) | XBOX123P(X))) & (XDIAMOND153P(X) <-> (DIAMOND153P(X) | XBOX154P(X))) & (DIAMOND231F(X) <-> FDIAMOND232F(X)) & (XDIAMOND127P(X) <-> (DIAMOND127P(X) | XDIAMOND128P(X))) & (DIAMOND165P(X) <-> FDIAMOND166P(X)) & (DIAMOND132P(X) <-> FC29P(X)) & (DIAMOND236F(X) <-> FBOX237F(X)) & (XDIAMOND289F(X) <-> (DIAMOND289F(X) | XDIAMOND290F(X))) & (XDIAMOND124P(X) <-> (DIAMOND124P(X) | XDIAMOND125P(X))) & (DIAMOND229F(X) <-> FDIAMOND230F(X)) & (XDIAMOND312F(X) <-> (DIAMOND312F(X) | X!C9F(X))) & (XDIAMOND21F(X) <-> (DIAMOND21F(X) | XBOX296F(X))) & (XDIAMOND67F(X) <-> (DIAMOND67F(X) | XDIAMOND258F(X))) & (XDIAMOND176P(X) <-> (DIAMOND176P(X) | XBOX177P(X))) & (XDIAMOND15F(X) <-> (DIAMOND15F(X) | XDIAMOND285F(X))) & (DIAMOND258F(X) <-> FDIAMOND259F(X)) & (XDIAMOND326F(X) <-> (DIAMOND326F(X) | XDIAMOND262F(X))) & (DIAMOND266F(X) <-> FDIAMOND267F(X)) & (XDIAMOND184P(X) <-> (DIAMOND184P(X) | XBOX185P(X))) & (XDIAMOND214F(X) <-> (DIAMOND214F(X) | X(BOX281F(X) & DIAMOND282F(X)))) & (DIAMOND196F(X) <-> FDIAMOND197F(X)) & (DIAMOND254F(X) <-> FE1G4F(X)) & (DIAMOND372P(X) <-> FC27P(X)) & (XDIAMOND170P(X) <-> (DIAMOND170P(X) | XDIAMOND171P(X))) & (DIAMOND370P(X) <-> FBOX371P(X)) & (XDIAMOND285F(X) <-> (DIAMOND285F(X) | XDIAMOND286F(X))) & (XDIAMOND292F(X) <-> (DIAMOND292F(X) | XBOX293F(X))) & (DIAMOND393P(X) <-> FDIAMOND182P(X)) & (XDIAMOND242F(X) <-> (DIAMOND242F(X) | XDIAMOND243F(X))) & (XDIAMOND152P(X) <-> (DIAMOND152P(X) | XDIAMOND153P(X))) & (DIAMOND209F(X) <-> FE2G13F(X)) & (XDIAMOND282F(X) <-> (DIAMOND282F(X) | XBOX283F(X))) & (XDIAMOND190P(X) <-> (DIAMOND190P(X) | XDIAMOND191P(X))) & (XDIAMOND259F(X) <-> (DIAMOND259F(X) | X(DIAMOND260F(X) & BOX325F(X)))) & (DIAMOND350P(X) <-> FBOX351P(X)) & (DIAMOND356P(X) <-> FBOX357P(X)) & (XDIAMOND272F(X) <-> (DIAMOND272F(X) | XDIAMOND273F(X))) & (DIAMOND377P(X) <-> FDIAMOND170P(X)) & (DIAMOND151P(X) <-> FDIAMOND365P(X)) & (DIAMOND175P(X) <-> FDIAMOND176P(X)) & (DIAMOND331P(X) <-> FBOX332P(X)) & (DIAMOND348P(X) <-> FDIAMOND349P(X)) & (XDIAMOND138P(X) <-> (DIAMOND138P(X) | XE3G1P(X))) & (DIAMOND245F(X) <-> FDIAMOND246F(X)) & (XDIAMOND286F(X) <-> (DIAMOND286F(X) | XDIAMOND287F(X))) & (XDIAMOND131P(X) <-> (DIAMOND131P(X) | X(E4G10P(X) & DIAMOND132P(X)))) & (XDIAMOND119P(X) <-> (DIAMOND119P(X) | XDIAMOND120P(X))) & (DIAMOND334P(X) <-> FDIAMOND116P(X)) & (XDIAMOND263F(X) <-> (DIAMOND263F(X) | XBOX327F(X))) & (XDIAMOND128P(X) <-> (DIAMOND128P(X) | XBOX129P(X))) & (XDIAMOND126P(X) <-> (DIAMOND126P(X) | XC9P(X))) & (DIAMOND72F(X) <-> F(BOX269F(X) & DIAMOND270F(X))) & (DIAMOND362P(X) <-> FBOX363P(X)) & (XDIAMOND248F(X) <-> (DIAMOND248F(X) | X(C1F(X) & DIAMOND311F(X)))) & (XDIAMOND73F(X) <-> (DIAMOND73F(X) | XDIAMOND330F(X))) & (DIAMOND199F(X) <-> FBOX200F(X)) & (XDIAMOND193P(X) <-> (DIAMOND193P(X) | X(BOX194P(X) & DIAMOND195P(X)))) & (XDIAMOND275F(X) <-> (DIAMOND275F(X) | XE4G13F(X))) & (XDIAMOND273F(X) <-> (DIAMOND273F(X) | XDIAMOND196F(X))) & (XDIAMOND117P(X) <-> (DIAMOND117P(X) | XDIAMOND118P(X))) & (DIAMOND224F(X) <-> FBOX225F(X)) & (DIAMOND247F(X) <-> FDIAMOND248F(X)) & (XDIAMOND321F(X) <-> (DIAMOND321F(X) | X(BOX322F(X) & DIAMOND323F(X)))) & (XDIAMOND168P(X) <-> (DIAMOND168P(X) | XDIAMOND169P(X))) & (DIAMOND333P(X) <-> FDIAMOND334P(X)) & (DIAMOND378P(X) <-> FDIAMOND379P(X)) & (DIAMOND213F(X) <-> FDIAMOND214F(X)) & (XDIAMOND134P(X) <-> (DIAMOND134P(X) | XDIAMOND135P(X))) & (XDIAMOND155P(X) <-> (DIAMOND155P(X) | XE2G20P(X))) & (XDIAMOND159P(X) <-> (DIAMOND159P(X) | XBOX160P(X))) & (DIAMOND218F(X) <-> FDIAMOND219F(X)) & (DIAMOND215F(X) <-> FDIAMOND216F(X)) & (XDIAMOND156P(X) <-> (DIAMOND156P(X) | X(BOX157P(X) & !E3G10P(X)))) & (DIAMOND400P(X) <-> FE5G27P(X)) & (XDIAMOND19F(X) <-> (DIAMOND19F(X) | XDIAMOND292F(X))) & (XDIAMOND328F(X) <-> (DIAMOND328F(X) | XC11F(X))) & (DIAMOND373P(X) <-> FBOX374P(X)) & (XDIAMOND228F(X) <-> (DIAMOND228F(X) | XE2G21F(X))) & (DIAMOND33F(X) <-> F(BOX234F(X) & !E3G10F(X))) & (DIAMOND238F(X) <-> FDIAMOND239F(X)) & (XDIAMOND329F(X) <-> (DIAMOND329F(X) | XDIAMOND266F(X))) & (XDIAMOND198F(X) <-> (DIAMOND198F(X) | XBOX274F(X))) & (XDIAMOND174P(X) <-> (DIAMOND174P(X) | XDIAMOND175P(X))) & (DIAMOND262F(X) <-> FDIAMOND263F(X)) & (DIAMOND239F(X) <-> F(!C28F(X) & BOX240F(X))) & (XDIAMOND191P(X) <-> (DIAMOND191P(X) | XBOX192P(X))) & (DIAMOND352P(X) <-> FDIAMOND353P(X)) & (XDIAMOND141P(X) <-> (DIAMOND141P(X) | XBOX142P(X))) & (DIAMOND149P(X) <-> FE2G21P(X)) & (DIAMOND220F(X) <-> FBOX221F(X)) & (DIAMOND399P(X) <-> FDIAMOND400P(X)) & (XDIAMOND49F(X) <-> (DIAMOND49F(X) | XBOX309F(X))) & (XDIAMOND306F(X) <-> (DIAMOND306F(X) | XC27F(X))) & (XDIAMOND179P(X) <-> (DIAMOND179P(X) | XBOX180P(X))) & (DIAMOND227F(X) <-> FDIAMOND228F(X)) & (DIAMOND204F(X) <-> FC25F(X)) & (DIAMOND252F(X) <-> FBOX253F(X)) & (DIAMOND210F(X) <-> F(E4G10F(X) & DIAMOND211F(X))) & (DIAMOND207F(X) <-> FBOX208F(X)) & (DIAMOND347P(X) <-> FDIAMOND348P(X)) & (XDIAMOND315F(X) <-> (DIAMOND315F(X) | XBOX316F(X))) & (XDIAMOND125P(X) <-> (DIAMOND125P(X) | XC25P(X))) & (XDIAMOND150P(X) <-> (DIAMOND150P(X) | XDIAMOND151P(X))) & (XDIAMOND311F(X) <-> (DIAMOND311F(X) | XDIAMOND312F(X))) & (XDIAMOND148P(X) <-> (DIAMOND148P(X) | XDIAMOND149P(X))) & (DIAMOND367P(X) <-> FDIAMOND368P(X)) & (DIAMOND385P(X) <-> FE5G2P(X)) & (DIAMOND398P(X) <-> FDIAMOND190P(X)) & (DIAMOND349P(X) <-> FDIAMOND350P(X)) & (DIAMOND379P(X) <-> F!C9P(X)) & (DIAMOND368P(X) <-> FBOX369P(X)) & (XDIAMOND162P(X) <-> (DIAMOND162P(X) | X(!C28P(X) & BOX163P(X)))) & (XDIAMOND276F(X) <-> (DIAMOND276F(X) | XBOX277F(X))) & (XDIAMOND302F(X) <-> (DIAMOND302F(X) | XBOX303F(X))) & (XDIAMOND310F(X) <-> (DIAMOND310F(X) | XDIAMOND247F(X))) & (DIAMOND366P(X) <-> FDIAMOND367P(X)) & (XDIAMOND145P(X) <-> (DIAMOND145P(X) | XBOX146P(X))) & (DIAMOND183P(X) <-> F(DIAMOND184P(X) & BOX394P(X))) & (XDIAMOND307F(X) <-> (DIAMOND307F(X) | XBOX308F(X))) & (DIAMOND260F(X) <-> FBOX261F(X)) & (DIAMOND395P(X) <-> FDIAMOND186P(X)) & (DIAMOND205F(X) <-> FC9F(X)) & (DIAMOND339P(X) <-> FBOX340P(X)) & (DIAMOND270F(X) <-> FC2F(X)) & (DIAMOND137P(X) <-> FBOX346P(X)) & (XDIAMOND294F(X) <-> (DIAMOND294F(X) | X(E5G28F(X) & BOX295F(X)))) & (DIAMOND58F(X) <-> FDIAMOND251F(X)) & (XDIAMOND1F(X) <-> (DIAMOND1F(X) | XBOX271F(X))) & (XDIAMOND278F(X) <-> (DIAMOND278F(X) | XBOX279F(X))) & (DIAMOND222F(X) <-> FBOX223F(X)) & (DIAMOND206F(X) <-> FDIAMOND207F(X)) & (XDIAMOND158P(X) <-> (DIAMOND158P(X) | XE1G5P(X))) & (XDIAMOND313F(X) <-> (DIAMOND313F(X) | XBOX314F(X))) & (DIAMOND118P(X) <-> FBOX335P(X)) & (DIAMOND336P(X) <-> FE4G13P(X)) & (XDIAMOND304F(X) <-> (DIAMOND304F(X) | XBOX305F(X))) & (DIAMOND171P(X) <-> F(C1P(X) & DIAMOND378P(X))) & (XDIAMOND299F(X) <-> (DIAMOND299F(X) | XC12F(X))) & (XDIAMOND164P(X) <-> (DIAMOND164P(X) | XDIAMOND165P(X))) & (DIAMOND375P(X) <-> FBOX376P(X)) & (DIAMOND382P(X) <-> FBOX383P(X)) & (DIAMOND169P(X) <-> FC5P(X)) & (XDIAMOND230F(X) <-> (DIAMOND230F(X) | XDIAMOND300F(X))) & (DIAMOND257F(X) <-> FE5G14F(X)) & (XDIAMOND318F(X) <-> (DIAMOND318F(X) | XE5G2F(X))) & (XDIAMOND297F(X) <-> (DIAMOND297F(X) | XBOX298F(X))) & (XDIAMOND139P(X) <-> (DIAMOND139P(X) | XDIAMOND140P(X))) & (DIAMOND388P(X) <-> FDIAMOND179P(X)) & (DIAMOND391P(X) <-> FBOX392P(X)) & (XDIAMOND330F(X) <-> (DIAMOND330F(X) | XE5G27F(X))) & (XDIAMOND161P(X) <-> (DIAMOND161P(X) | XDIAMOND162P(X))) & (DIAMOND249F(X) <-> F(E3G13F(X) & DIAMOND250F(X))) & (DIAMOND226F(X) <-> FDIAMOND227F(X)) & (XDIAMOND181P(X) <-> (DIAMOND181P(X) | XE5G14P(X))) & (DIAMOND32F(X) <-> FE2G20F(X)) & (DIAMOND364P(X) <-> FC12P(X)) & (DIAMOND337P(X) <-> FBOX338P(X)) & (DIAMOND380P(X) <-> FBOX381P(X)) & (XDIAMOND182P(X) <-> (DIAMOND182P(X) | XDIAMOND183P(X))) & (XDIAMOND178P(X) <-> (DIAMOND178P(X) | XE1G4P(X))) & (XDIAMOND195P(X) <-> (DIAMOND195P(X) | XC2P(X))) & (DIAMOND344P(X) <-> FBOX345P(X)) & (XDIAMOND290F(X) <-> (DIAMOND290F(X) | XBOX291F(X))) & (XDIAMOND251F(X) <-> (DIAMOND251F(X) | XDIAMOND252F(X))) & (XDIAMOND10F(X) <-> (DIAMOND10F(X) | XBOX280F(X))) & (XDIAMOND147P(X) <-> (DIAMOND147P(X) | XDIAMOND148P(X))) & (DIAMOND360P(X) <-> FBOX361P(X)) & (XDIAMOND143P(X) <-> (DIAMOND143P(X) | XBOX144P(X))) & (DIAMOND255F(X) <-> FBOX256F(X)) & (XDIAMOND287F(X) <-> (DIAMOND287F(X) | XBOX288F(X))) & (DIAMOND264F(X) <-> FBOX265F(X)) & (XBOX609F(X) <-> (BOX609F(X) & XE5G5F(X))) & (XBOX91F(X) <-> (BOX91F(X) & XBOX648F(X))) & (XBOX585F(X) <-> (BOX585F(X) & XE1G11F(X))) & (BOX433P(X) <-> GE1G20P(X)) & (XBOX418P(X) <-> (BOX418P(X) & XBOX419P(X))) & (BOX185P(X) <-> GDIAMOND149P(X)) & (XBOX409P(X) <-> (BOX409P(X) & XBOX411P(X))) & (XBOX482P(X) <-> (BOX482P(X) & XBOX445P(X))) & (XBOX548P(X) <-> (BOX548P(X) & XPG10F)) & (BOX454P(X) <-> GE5G11P(X)) & (XBOX202F(X) <-> (BOX202F(X) & XDIAMOND276F(X))) & (XBOX563F(X) <-> (BOX563F(X) & XE3G10F(X))) & (XBOX95F(X) <-> (BOX95F(X) & XBOX652F(X))) & (XBOX552P(X) <-> (BOX552P(X) & XPG5F)) & (XBOX303F(X) <-> (BOX303F(X) & XDIAMOND304F(X))) & (BOX736P(X) <-> GBOX552P(X)) & (XBOX78F(X) <-> (BOX78F(X) & XBOX635F(X))) & (XBOX436P(X) <-> (BOX436P(X) & XDIAMOND364P(X))) & (BOX507P(X) <-> GE2G13P(X)) & (BOX693P(X) <-> GDIAMOND373P(X)) & (BOX655F(X) <-> GPG27F) & (BOX666F(X) <-> GPinvG21F) & (XBOX456P(X) <-> (BOX456P(X) & XBOX457P(X))) & (BOX233F(X) <-> GC7F(X)) & (BOX648F(X) <-> GPinvG11F) & (XBOX678F(X) <-> (BOX678F(X) & XDIAMOND307F(X))) & (BOX464P(X) <-> GE1G0P(X)) & (XBOX54F(X) <-> (BOX54F(X) & XDIAMOND310F(X))) & (BOX619F(X) <-> GDIAMOND318F(X)) & (XBOX410P(X) <-> (BOX410P(X) & XDIAMOND126P(X))) & (XBOX518P(X) <-> (BOX518P(X) & XBOX519P(X))) & (BOX129P(X) <-> GBOX414P(X)) & (BOX351P(X) <-> GBOX427P(X)) & (XBOX237F(X) <-> (BOX237F(X) & XE5G18F(X))) & (BOX652F(X) <-> GPinvG2F) & (BOX734P(X) <-> GBOX550P(X)) & (BOX567F(X) <-> GDIAMOND205F(X)) & (XBOX317F(X) <-> (BOX317F(X) & XC12F(X))) & (XBOX508P(X) <-> (BOX508P(X) & XDIAMOND389P(X))) & (XBOX316F(X) <-> (BOX316F(X) & XDIAMOND249F(X))) & (BOX607F(X) <-> GBOX608F(X)) & (BOX142P(X) <-> GDIAMOND143P(X)) & (XBOX455P(X) <-> (BOX455P(X) & X(E5G11P(X) & DIAMOND158P(X)))) & (BOX404P(X) <-> GE3G10P(X)) & (XBOX121P(X) <-> (BOX121P(X) & XDIAMOND122P(X))) & (BOX743P(X) <-> GBOX559P(X)) & (XBOX627F(X) <-> (BOX627F(X) & XE1G2F(X))) & (XBOX536P(X) <-> (BOX536P(X) & XPG8F)) & (BOX41F(X) <-> GBOX602F(X)) & (BOX462P(X) <-> GE1G4P(X)) & (XBOX551P(X) <-> (BOX551P(X) & XPG21F)) & (XBOX545P(X) <-> (BOX545P(X) & XPL6F)) & (BOX712P(X) <-> GBOX528P(X)) & (BOX745P(X) <-> GBOX561P(X)) & (XBOX592F(X) <-> (BOX592F(X) & XE1G1F(X))) & (BOX616F(X) <-> GBOX617F(X)) & (XBOX614F(X) <-> (BOX614F(X) & XE5G14F(X))) & (BOX354P(X) <-> GC0P(X)) & (XBOX293F(X) <-> (BOX293F(X) & XBOX674F(X))) & (XBOX75F(X) <-> (BOX75F(X) & XBOX632F(X))) & (XBOX412P(X) <-> (BOX412P(X) & XC26P(X))) & (BOX485P(X) <-> GE1G21P(X)) & (BOX24F(X) <-> GBOX586F(X)) & (XBOX599F(X) <-> (BOX599F(X) & XE1G0F(X))) & (XBOX546P(X) <-> (BOX546P(X) & XPG7F)) & (XBOX506P(X) <-> (BOX506P(X) & XBOX507P(X))) & (XBOX554P(X) <-> (BOX554P(X) & XPinvG20F)) & (XBOX500P(X) <-> (BOX500P(X) & XBOX501P(X))) & (BOX468P(X) <-> GE1G7P(X)) & (XBOX408P(X) <-> (BOX408P(X) & X(BOX409P(X) & BOX410P(X)))) & (XBOX612F(X) <-> (BOX612F(X) & XE1G8F(X))) & (XBOX443P(X) <-> (BOX443P(X) & X(C7P(X) & BOX445P(X)))) & (BOX723P(X) <-> GBOX539P(X)) & (BOX654F(X) <-> GPG17F) & (XBOX413P(X) <-> (BOX413P(X) & XDIAMOND127P(X))) & (XBOX84F(X) <-> (BOX84F(X) & XBOX641F(X))) & (BOX28F(X) <-> GBOX592F(X)) & (BOX0F(X) <-> GBOX562F(X)) & (XBOX484P(X) <-> (BOX484P(X) & XBOX485P(X))) & (XBOX18F(X) <-> (BOX18F(X) & XDIAMOND218F(X))) & (BOX342P(X) <-> GDIAMOND131P(X)) & (XBOX610F(X) <-> (BOX610F(X) & XE1G21F(X))) & (XBOX340P(X) <-> (BOX340P(X) & XDIAMOND130P(X))) & (BOX476P(X) <-> GBOX691P(X)) & (XBOX559P(X) <-> (BOX559P(X) & XPinvG1F)) & (XBOX681F(X) <-> (BOX681F(X) & XDIAMOND320F(X))) & (XBOX90F(X) <-> (BOX90F(X) & XBOX647F(X))) & (XBOX511P(X) <-> (BOX511P(X) & XBOX512P(X))) & (XBOX489P(X) <-> (BOX489P(X) & XBOX490P(X))) & (XBOX89F(X) <-> (BOX89F(X) & XBOX646F(X))) & (BOX55F(X) <-> GBOX615F(X)) & (BOX657F(X) <-> GPG7F) & (XBOX80F(X) <-> (BOX80F(X) & XBOX637F(X))) & (XBOX542P(X) <-> (BOX542P(X) & XPG6F)) & (BOX180P(X) <-> GBOX700P(X)) & (XBOX465P(X) <-> (BOX465P(X) & XBOX466P(X))) & (XBOX420P(X) <-> (BOX420P(X) & XE4G4P(X))) & (XBOX481P(X) <-> (BOX481P(X) & XBOX343P(X))) & (BOX701P(X) <-> GDIAMOND181P(X)) & (XBOX535P(X) <-> (BOX535P(X) & XPinvG9F)) & (XBOX50F(X) <-> (BOX50F(X) & XDIAMOND241F(X))) & (BOX37F(X) <-> GBOX598F(X)) & (XBOX580F(X) <-> (BOX580F(X) & XE5G27F(X))) & (BOX4F(X) <-> GBOX564F(X)) & (BOX459P(X) <-> GE3G1P(X)) & (BOX59F(X) <-> GBOX620F(X)) & (BOX691P(X) <-> GBOX477P(X)) & (BOX438P(X) <-> GE1G11P(X)) & (BOX714P(X) <-> GBOX530P(X)) & (XBOX361P(X) <-> (BOX361P(X) & XBOX434P(X))) & (XBOX594F(X) <-> (BOX594F(X) & XE5G11F(X))) & (XBOX573F(X) <-> (BOX573F(X) & XE2G21F(X))) & (BOX686P(X) <-> GDIAMOND139P(X)) & (BOX42F(X) <-> GBOX603F(X)) & (BOX422P(X) <-> GE1G16P(X)) & (BOX5F(X) <-> GBOX565F(X)) & (XBOX154P(X) <-> (BOX154P(X) & XC7P(X))) & (XBOX441P(X) <-> (BOX441P(X) & X(BOX442P(X) & BOX443P(X)))) & (XBOX103F(X) <-> (BOX103F(X) & XBOX660F(X))) & (XBOX624F(X) <-> (BOX624F(X) & XE1G6F(X))) & (BOX722P(X) <-> GBOX538P(X)) & (XBOX110F(X) <-> (BOX110F(X) & XBOX667F(X))) & (BOX728P(X) <-> GBOX544P(X)) & (XBOX432P(X) <-> (BOX432P(X) & XBOX433P(X))) & (XBOX593F(X) <-> (BOX593F(X) & XE4G13F(X))) & (BOX634F(X) <-> GPG9F) & (XBOX93F(X) <-> (BOX93F(X) & XBOX650F(X))) & (BOX470P(X) <-> GE5G2P(X)) & (XBOX467P(X) <-> (BOX467P(X) & XBOX468P(X))) & (BOX295F(X) <-> G!E3G9F(X)) & (BOX588F(X) <-> G(C7F(X) & BOX590F(X))) & (XBOX71F(X) <-> (BOX71F(X) & XBOX628F(X))) & (BOX519P(X) <-> GDIAMOND398P(X)) & (BOX744P(X) <-> GBOX560P(X)) & (XBOX553P(X) <-> (BOX553P(X) & XPinvG10F)) & (BOX647F(X) <-> GPG8F) & (XBOX338P(X) <-> (BOX338P(X) & XDIAMOND124P(X))) & (XBOX403P(X) <-> (BOX403P(X) & XBOX404P(X))) & (XBOX601F(X) <-> (BOX601F(X) & XE1G7F(X))) & (BOX636F(X) <-> GPG20F) & (BOX431P(X) <-> GE5G27P(X)) & (BOX617F(X) <-> GDIAMOND313F(X)) & (BOX225F(X) <-> GDIAMOND226F(X)) & (XBOX77F(X) <-> (BOX77F(X) & XBOX634F(X))) & (XBOX359P(X) <-> (BOX359P(X) & X!E3G9P(X))) & (XBOX79F(X) <-> (BOX79F(X) & XBOX636F(X))) & (BOX649F(X) <-> GPinvG8F) & (BOX383P(X) <-> GDIAMOND172P(X)) & (XBOX530P(X) <-> (BOX530P(X) & XPinvG28F)) & (XBOX96F(X) <-> (BOX96F(X) & XBOX653F(X))) & (XBOX99F(X) <-> (BOX99F(X) & XBOX656F(X))) & (BOX13F(X) <-> GBOX575F(X)) & (BOX335P(X) <-> GDIAMOND336P(X)) & (BOX369P(X) <-> GDIAMOND370P(X)) & (XBOX449P(X) <-> (BOX449P(X) & XBOX450P(X))) & (BOX39F(X) <-> GBOX600F(X)) & (XBOX76F(X) <-> (BOX76F(X) & XBOX633F(X))) & (BOX644F(X) <-> GPinvG6F) & (XBOX504P(X) <-> (BOX504P(X) & XBOX505P(X))) & (BOX65F(X) <-> GBOX624F(X)) & (XBOX102F(X) <-> (BOX102F(X) & XBOX659F(X))) & (BOX703P(X) <-> GBOX517P(X)) & (XBOX346P(X) <-> (BOX346P(X) & XC20P(X))) & (XBOX105F(X) <-> (BOX105F(X) & XBOX662F(X))) & (BOX578F(X) <-> GDIAMOND289F(X)) & (BOX671F(X) <-> GPinvG14F) & (XBOX611F(X) <-> (BOX611F(X) & XDIAMOND238F(X))) & (XBOX499P(X) <-> (BOX499P(X) & XDIAMOND385P(X))) & (XBOX414P(X) <-> (BOX414P(X) & XBOX415P(X))) & (BOX167P(X) <-> GE5G28P(X)) & (XBOX520P(X) <-> (BOX520P(X) & XPinvG7F)) & (XBOX115F(X) <-> (BOX115F(X) & XBOX672F(X))) & (BOX640F(X) <-> GPG13F) & (BOX628F(X) <-> GBOX629F(X)) & (XBOX677F(X) <-> (BOX677F(X) & XBOX678F(X))) & (BOX36F(X) <-> GBOX237F(X)) & (BOX642F(X) <-> GPG16F) & (BOX387P(X) <-> GBOX698P(X)) & (BOX729P(X) <-> GBOX545P(X)) & (BOX157P(X) <-> GBOX455P(X)) & (XBOX453P(X) <-> (BOX453P(X) & XBOX454P(X))) & (XBOX469P(X) <-> (BOX469P(X) & XBOX470P(X))) & (BOX641F(X) <-> GPinvG28F) & (BOX45F(X) <-> GBOX281F(X)) & (XBOX674F(X) <-> (BOX674F(X) & XDIAMOND294F(X))) & (BOX731P(X) <-> GBOX547P(X)) & (BOX23F(X) <-> GBOX585F(X)) & (BOX697P(X) <-> GDIAMOND382P(X)) & (XBOX451P(X) <-> (BOX451P(X) & XBOX452P(X))) & (BOX6F(X) <-> GDIAMOND206F(X)) & (BOX716P(X) <-> GBOX532P(X)) & (BOX478P(X) <-> GBOX692P(X)) & (BOX720P(X) <-> GBOX536P(X)) & (BOX501P(X) <-> GE2G20P(X)) & (XBOX472P(X) <-> (BOX472P(X) & X(BOX473P(X) & BOX474P(X)))) & (BOX46F(X) <-> GBOX590F(X)) & (BOX726P(X) <-> GBOX542P(X)) & (BOX646F(X) <-> GPinvG9F) & (XBOX532P(X) <-> (BOX532P(X) & XPG2F)) & (XBOX407P(X) <-> (BOX407P(X) & XBOX408P(X))) & (XBOX564F(X) <-> (BOX564F(X) & XE1G9F(X))) & (BOX419P(X) <-> GE2G21P(X)) & (XBOX447P(X) <-> (BOX447P(X) & XBOX448P(X))) & (XBOX625F(X) <-> (BOX625F(X) & XE4G0F(X))) & (BOX38F(X) <-> GBOX599F(X)) & (BOX699P(X) <-> GDIAMOND388P(X)) & (XBOX538P(X) <-> (BOX538P(X) & XPinvG8F)) & (XBOX223F(X) <-> (BOX223F(X) & XBOX673F(X))) & (BOX394P(X) <-> GE4L6P(X)) & (XBOX463P(X) <-> (BOX463P(X) & XBOX464P(X))) & (BOX706P(X) <-> GBOX522P(X)) & (XBOX676F(X) <-> (BOX676F(X) & XBOX607F(X))) & (BOX732P(X) <-> GBOX548P(X)) & (XBOX81F(X) <-> (BOX81F(X) & XBOX638F(X))) & (BOX660F(X) <-> GPG4F) & (XBOX113F(X) <-> (BOX113F(X) & XBOX670F(X))) & (BOX60F(X) <-> GBOX621F(X)) & (XBOX622F(X) <-> (BOX622F(X) & XE4G4F(X))) & (XBOX112F(X) <-> (BOX112F(X) & XBOX669F(X))) & (BOX43F(X) <-> GBOX606F(X)) & (BOX638F(X) <-> GPG28F) & (BOX309F(X) <-> GBOX611F(X)) & (BOX662F(X) <-> GPG21F) & (XBOX83F(X) <-> (BOX83F(X) & XBOX640F(X))) & (XBOX274F(X) <-> (BOX274F(X) & XDIAMOND275F(X))) & (XBOX605F(X) <-> (BOX605F(X) & XDIAMOND236F(X))) & (XBOX483P(X) <-> (BOX483P(X) & XBOX345P(X))) & (BOX61F(X) <-> GBOX622F(X)) & (BOX7F(X) <-> GBOX572F(X)) & (XBOX109F(X) <-> (BOX109F(X) & XBOX666F(X))) & (BOX322F(X) <-> GE1G21F(X)) & (BOX715P(X) <-> GBOX531P(X)) & (BOX733P(X) <-> GBOX549P(X)) & (XBOX87F(X) <-> (BOX87F(X) & XBOX644F(X))) & (XBOX575F(X) <-> (BOX575F(X) & XE1G13F(X))) & (XBOX537P(X) <-> (BOX537P(X) & XPinvG11F)) & (BOX53F(X) <-> GBOX614F(X)) & (XBOX416P(X) <-> (BOX416P(X) & XBOX417P(X))) & (XBOX107F(X) <-> (BOX107F(X) & XBOX664F(X))) & (BOX277F(X) <-> GDIAMOND203F(X)) & (BOX345P(X) <-> GE1G14P(X)) & (XBOX298F(X) <-> (BOX298F(X) & X(BOX675F(X) & !E3G8F(X)))) & (BOX689P(X) <-> GDIAMOND362P(X)) & (XBOX332P(X) <-> (BOX332P(X) & XDIAMOND333P(X))) & (XBOX539P(X) <-> (BOX539P(X) & XPG0F)) & (XBOX620F(X) <-> (BOX620F(X) & XE2G20F(X))) & (XBOX521P(X) <-> (BOX521P(X) & XPinvG4F)) & (BOX503P(X) <-> GE3G8P(X)) & (BOX685P(X) <-> GBOX425P(X)) & (BOX569F(X) <-> GC26F(X)) & (XBOX517P(X) <-> (BOX517P(X) & XBOX518P(X))) & (BOX690P(X) <-> GBOX436P(X)) & (BOX724P(X) <-> GBOX540P(X)) & (BOX576F(X) <-> G(BOX577F(X) & DIAMOND217F(X))) & (XBOX280F(X) <-> (BOX280F(X) & XDIAMOND210F(X))) & (XBOX493P(X) <-> (BOX493P(X) & XBOX494P(X))) & (BOX696P(X) <-> GBOX697P(X)) & (BOX665F(X) <-> GPinvG20F) & (BOX653F(X) <-> GPG6F) & (XBOX101F(X) <-> (BOX101F(X) & XBOX658F(X))) & (BOX639F(X) <-> GPinvG27F) & (XBOX560P(X) <-> (BOX560P(X) & XPinvG14F)) & (XBOX495P(X) <-> (BOX495P(X) & XBOX496P(X))) & (XBOX371P(X) <-> (BOX371P(X) & XC27P(X))) & (XBOX496P(X) <-> (BOX496P(X) & XDIAMOND380P(X))) & (XBOX600F(X) <-> (BOX600F(X) & XE1G10F(X))) & (BOX392P(X) <-> GBOX701P(X)) & (XBOX446P(X) <-> (BOX446P(X) & X(DIAMOND150P(X) & DIAMOND152P(X)))) & (BOX269F(X) <-> GE1G16F(X)) & (BOX466P(X) <-> GE1G10P(X)) & (XBOX426P(X) <-> (BOX426P(X) & XDIAMOND136P(X))) & (BOX656F(X) <-> GPL6F) & (XBOX98F(X) <-> (BOX98F(X) & XBOX655F(X))) & (XBOX515P(X) <-> (BOX515P(X) & XBOX516P(X))) & (BOX587F(X) <-> GBOX589F(X)) & (XBOX106F(X) <-> (BOX106F(X) & XBOX663F(X))) & (BOX200F(X) <-> GDIAMOND201F(X)) & (XBOX528P(X) <-> (BOX528P(X) & XPinvG27F)) & (BOX486P(X) <-> GDIAMOND161P(X)) & (BOX296F(X) <-> GBOX582F(X)) & (BOX62F(X) <-> GBOX623F(X)) & (XBOX502P(X) <-> (BOX502P(X) & XBOX503P(X))) & (BOX583F(X) <-> GDIAMOND224F(X)) & (BOX705P(X) <-> GBOX521P(X)) & (BOX271F(X) <-> GDIAMOND272F(X)) & (XBOX74F(X) <-> (BOX74F(X) & XBOX631F(X))) & (BOX492P(X) <-> GE5G14P(X)) & (BOX633F(X) <-> GPinvG18F) & (BOX25F(X) <-> G(BOX587F(X) & BOX588F(X))) & (XBOX475P(X) <-> (BOX475P(X) & XBOX476P(X))) & (XBOX460P(X) <-> (BOX460P(X) & XBOX160P(X))) & (XBOX543P(X) <-> (BOX543P(X) & XPG17F)) & (BOX672F(X) <-> GPG1F) & (BOX629F(X) <-> GBOX630F(X)) & (BOX632F(X) <-> GPinvG4F) & (BOX584F(X) <-> GDIAMOND299F(X)) & (XBOX401P(X) <-> (BOX401P(X) & XBOX402P(X))) & (XBOX591F(X) <-> (BOX591F(X) & XE3G13F(X))) & (BOX279F(X) <-> GDIAMOND209F(X)) & (XBOX442P(X) <-> (BOX442P(X) & XBOX444P(X))) & (XBOX97F(X) <-> (BOX97F(X) & XBOX654F(X))) & (XBOX497P(X) <-> (BOX497P(X) & X(C21P(X) & C17P(X)))) & (BOX658F(X) <-> GPG11F) & (XBOX234F(X) <-> (BOX234F(X) & XBOX595F(X))) & (XBOX524P(X) <-> (BOX524P(X) & XPG18F)) & (XBOX533P(X) <-> (BOX533P(X) & XPinvG6F)) & (BOX730P(X) <-> GBOX546P(X)) & (BOX343P(X) <-> GE4G7P(X)) & (XBOX390P(X) <-> (BOX390P(X) & XE1G21P(X))) & (XBOX437P(X) <-> (BOX437P(X) & XBOX438P(X))) & (XBOX487P(X) <-> (BOX487P(X) & XBOX488P(X))) & (XBOX291F(X) <-> (BOX291F(X) & XC0F(X))) & (BOX406P(X) <-> GE1G9P(X)) & (XBOX85F(X) <-> (BOX85F(X) & XBOX642F(X))) & (BOX687P(X) <-> G!C26P(X)) & (XBOX381P(X) <-> (BOX381P(X) & XBOX497P(X))) & (XBOX529P(X) <-> (BOX529P(X) & XPG13F)) & (BOX8F(X) <-> GBOX573F(X)) & (BOX645F(X) <-> GPinvG17F) & (XBOX111F(X) <-> (BOX111F(X) & XBOX668F(X))) & (XBOX100F(X) <-> (BOX100F(X) & XBOX657F(X))) & (BOX474P(X) <-> GDIAMOND159P(X)) & (XBOX423P(X) <-> (BOX423P(X) & XBOX424P(X))) & (XBOX471P(X) <-> (BOX471P(X) & XBOX472P(X))) & (BOX253F(X) <-> G(BOX619F(X) & DIAMOND254F(X))) & (XBOX562F(X) <-> (BOX562F(X) & XE4G10F(X))) & (XBOX679F(X) <-> (BOX679F(X) & XDIAMOND315F(X))) & (XBOX281F(X) <-> (BOX281F(X) & XE4G7F(X))) & (XBOX194P(X) <-> (BOX194P(X) & XE1G16P(X))) & (XBOX568F(X) <-> (BOX568F(X) & XBOX569F(X))) & (BOX490P(X) <-> GE1G18P(X)) & (XBOX221F(X) <-> (BOX221F(X) & XDIAMOND222F(X))) & (XBOX104F(X) <-> (BOX104F(X) & XBOX661F(X))) & (XBOX177P(X) <-> (BOX177P(X) & X(BOX499P(X) & DIAMOND178P(X)))) & (BOX618F(X) <-> G(C21F(X) & C17F(X))) & (BOX448P(X) <-> GE3G13P(X)) & (BOX64F(X) <-> GDIAMOND321F(X)) & (BOX3F(X) <-> GBOX563F(X)) & (XBOX261F(X) <-> (BOX261F(X) & XDIAMOND228F(X))) & (XBOX581F(X) <-> (BOX581F(X) & XE1G20F(X))) & (XBOX514P(X) <-> (BOX514P(X) & XBOX167P(X))) & (BOX160P(X) <-> GE5G18P(X)) & (BOX384P(X) <-> GC12P(X)) & (BOX402P(X) <-> GE4G10P(X)) & (BOX692P(X) <-> GBOX693P(X)) & (XBOX396P(X) <-> (BOX396P(X) & XDIAMOND188P(X))) & (XBOX146P(X) <-> (BOX146P(X) & XDIAMOND147P(X))) & (BOX34F(X) <-> GBOX596F(X)) & (XBOX240F(X) <-> (BOX240F(X) & XC6F(X))) & (BOX702P(X) <-> GBOX513P(X)) & (XBOX613F(X) <-> (BOX613F(X) & XE1G18F(X))) & (XBOX525P(X) <-> (BOX525P(X) & XPG20F)) & (BOX615F(X) <-> GBOX616F(X)) & (XBOX11F(X) <-> (BOX11F(X) & XDIAMOND212F(X))) & (XBOX308F(X) <-> (BOX308F(X) & XE1G5F(X))) & (BOX637F(X) <-> GPinvG5F) & (BOX566F(X) <-> GBOX568F(X)) & (XBOX114F(X) <-> (BOX114F(X) & XBOX671F(X))) & (XBOX14F(X) <-> (BOX14F(X) & XBOX576F(X))) & (XBOX92F(X) <-> (BOX92F(X) & XBOX649F(X))) & (XBOX534P(X) <-> (BOX534P(X) & XPinvG17F)) & (BOX740P(X) <-> GBOX556P(X)) & (XBOX376P(X) <-> (BOX376P(X) & XBOX486P(X))) & (XBOX421P(X) <-> (BOX421P(X) & XBOX422P(X))) & (BOX70F(X) <-> GBOX627F(X)) & (XBOX325F(X) <-> (BOX325F(X) & XE4L6F(X))) & (BOX363P(X) <-> G(BOX690P(X) & !E3G8P(X))) & (BOX735P(X) <-> GBOX551P(X)) & (BOX661F(X) <-> GPinvG16F) & (XBOX108F(X) <-> (BOX108F(X) & XBOX665F(X))) & (BOX305F(X) <-> GC27F(X)) & (XBOX630F(X) <-> (BOX630F(X) & XDIAMOND329F(X))) & (XBOX544P(X) <-> (BOX544P(X) & XPG27F)) & (BOX411P(X) <-> GBOX412P(X)) & (BOX450P(X) <-> GE1G1P(X)) & (BOX635F(X) <-> GPG18F) & (BOX710P(X) <-> GBOX526P(X)) & (BOX694P(X) <-> GDIAMOND164P(X)) & (BOX704P(X) <-> GBOX520P(X)) & (BOX742P(X) <-> GBOX558P(X)) & (BOX17F(X) <-> GBOX580F(X)) & (XBOX288F(X) <-> (BOX288F(X) & XBOX578F(X))) & (BOX708P(X) <-> GBOX524P(X)) & (BOX44F(X) <-> GBOX609F(X)) & (BOX650F(X) <-> GPG0F) & (XBOX531P(X) <-> (BOX531P(X) & XPG16F)) & (BOX709P(X) <-> GBOX525P(X)) & (XBOX604F(X) <-> (BOX604F(X) & XDIAMOND306F(X))) & (BOX698P(X) <-> GBOX699P(X)) & (BOX707P(X) <-> GBOX523P(X)) & (BOX659F(X) <-> GPG10F) & (BOX424P(X) <-> GE1G13P(X)) & (BOX327F(X) <-> GDIAMOND264F(X)) & (BOX144P(X) <-> GBOX687P(X)) & (XBOX598F(X) <-> (BOX598F(X) & XE1G4F(X))) & (XBOX430P(X) <-> (BOX430P(X) & XBOX431P(X))) & (BOX565F(X) <-> G(BOX566F(X) & BOX567F(X))) & (BOX51F(X) <-> GBOX612F(X)) & (XBOX22F(X) <-> (BOX22F(X) & XDIAMOND297F(X))) & (BOX284F(X) <-> GC20F(X)) & (XBOX586F(X) <-> (BOX586F(X) & XE1G28F(X))) & (BOX727P(X) <-> GBOX543P(X)) & (XBOX435P(X) <-> (BOX435P(X) & XDIAMOND145P(X))) & (XBOX477P(X) <-> (BOX477P(X) & XBOX478P(X))) & (BOX631F(X) <-> GPinvG7F) & (BOX595F(X) <-> G(E5G11F(X) & DIAMOND235F(X))) & (BOX626F(X) <-> GDIAMOND326F(X)) & (BOX570F(X) <-> GBOX571F(X)) & (XBOX540P(X) <-> (BOX540P(X) & XPinvG13F)) & (XBOX571F(X) <-> (BOX571F(X) & XDIAMOND278F(X))) & (BOX488P(X) <-> GE1G8P(X)) & (XBOX541P(X) <-> (BOX541P(X) & XPinvG2F)) & (BOX440P(X) <-> GE1G28P(X)) & (XBOX558P(X) <-> (BOX558P(X) & XPinvG0F)) & (BOX35F(X) <-> GBOX597F(X)) & (BOX664F(X) <-> GPinvG10F) & (XBOX88F(X) <-> (BOX88F(X) & XBOX645F(X))) & (BOX668F(X) <-> GPinvL6F) & (BOX473P(X) <-> GDIAMOND372P(X)) & (BOX669F(X) <-> GPinvG0F) & (BOX30F(X) <-> GBOX594F(X)) & (BOX429P(X) <-> GE3G9P(X)) & (XBOX549P(X) <-> (BOX549P(X) & XPG4F)) & (BOX741P(X) <-> GBOX557P(X)) & (BOX589F(X) <-> GE1G6F(X)) & (XBOX324F(X) <-> (BOX324F(X) & XBOX683F(X))) & (BOX12F(X) <-> GBOX574F(X)) & (BOX688P(X) <-> GDIAMOND358P(X)) & (XBOX557P(X) <-> (BOX557P(X) & XPinvL6F)) & (XBOX606F(X) <-> (BOX606F(X) & XBOX676F(X))) & (XBOX621F(X) <-> (BOX621F(X) & XE3G8F(X))) & (BOX670F(X) <-> GPinvG1F) & (BOX684P(X) <-> GDIAMOND133P(X)) & (XBOX434P(X) <-> (BOX434P(X) & XBOX435P(X))) & (BOX663F(X) <-> GPG5F) & (XBOX256F(X) <-> (BOX256F(X) & XBOX682F(X))) & (BOX516P(X) <-> GE1G2P(X)) & (BOX480P(X) <-> GE5G5P(X)) & (XBOX602F(X) <-> (BOX602F(X) & XE5G2F(X))) & (XBOX556P(X) <-> (BOX556P(X) & XPG14F)) & (XBOX82F(X) <-> (BOX82F(X) & XBOX639F(X))) & (XBOX444P(X) <-> (BOX444P(X) & XE1G6P(X))) & (BOX512P(X) <-> GE4G0P(X)) & (BOX417P(X) <-> GE1G27P(X)) & (BOX163P(X) <-> GC6P(X)) & (BOX667F(X) <-> GPG14F) & (BOX738P(X) <-> GBOX554P(X)) & (XBOX550P(X) <-> (BOX550P(X) & XPinvG16F)) & (BOX643F(X) <-> GPG2F) & (BOX695P(X) <-> GDIAMOND377P(X)) & (XBOX680F(X) <-> (BOX680F(X) & XBOX681F(X))) & (XBOX509P(X) <-> (BOX509P(X) & XBOX510P(X))) & (XBOX555P(X) <-> (BOX555P(X) & XPinvG21F)) & (BOX48F(X) <-> GBOX610F(X)) & (BOX20F(X) <-> GBOX581F(X)) & (XBOX68F(X) <-> (BOX68F(X) & XBOX626F(X))) & (BOX452P(X) <-> GE4G13P(X)) & (XBOX561P(X) <-> (BOX561P(X) & XPG1F)) & (BOX582F(X) <-> GBOX583F(X)) & (BOX717P(X) <-> GBOX533P(X)) & (XBOX590F(X) <-> (BOX590F(X) & XE5G17F(X))) & (XBOX192P(X) <-> (BOX192P(X) & X!E4G0P(X))) & (BOX713P(X) <-> GBOX529P(X)) & (BOX27F(X) <-> GBOX591F(X)) & (XBOX479P(X) <-> (BOX479P(X) & XBOX480P(X))) & (XBOX608F(X) <-> (BOX608F(X) & XBOX677F(X))) & (XBOX283F(X) <-> (BOX283F(X) & XE1G14F(X))) & (XBOX405P(X) <-> (BOX405P(X) & XBOX406P(X))) & (BOX40F(X) <-> GBOX601F(X)) & (XBOX682F(X) <-> (BOX682F(X) & XBOX562F(X))) & (XBOX491P(X) <-> (BOX491P(X) & XBOX492P(X))) & (XBOX94F(X) <-> (BOX94F(X) & XBOX651F(X))) & (XBOX189P(X) <-> (BOX189P(X) & XDIAMOND397P(X))) & (BOX577F(X) <-> GDIAMOND215F(X)) & (XBOX579F(X) <-> (BOX579F(X) & XE3G9F(X))) & (BOX52F(X) <-> GBOX613F(X)) & (BOX739P(X) <-> GBOX555P(X)) & (XBOX439P(X) <-> (BOX439P(X) & XBOX440P(X))) & (XBOX572F(X) <-> (BOX572F(X) & XE1G27F(X))) & (XBOX57F(X) <-> (BOX57F(X) & XBOX679F(X))) & (XBOX623F(X) <-> (BOX623F(X) & XE2G13F(X))) & (BOX265F(X) <-> GDIAMOND328F(X)) & (BOX719P(X) <-> GBOX535P(X)) & (XBOX425P(X) <-> (BOX425P(X) & X(BOX426P(X) & DIAMOND138P(X)))) & (XBOX527P(X) <-> (BOX527P(X) & XPG28F)) & (XBOX574F(X) <-> (BOX574F(X) & XE1G16F(X))) & (XBOX513P(X) <-> (BOX513P(X) & XDIAMOND395P(X))) & (XBOX522P(X) <-> (BOX522P(X) & XPinvG18F)) & (XBOX596F(X) <-> (BOX596F(X) & XE1G17F(X))) & (BOX29F(X) <-> GBOX593F(X)) & (BOX457P(X) <-> GE1G17P(X)) & (BOX603F(X) <-> G(BOX604F(X) & BOX605F(X))) & (XBOX494P(X) <-> (BOX494P(X) & XBOX495P(X))) & (XBOX523P(X) <-> (BOX523P(X) & XPG9F)) & (XBOX673F(X) <-> (BOX673F(X) & X!C26F(X))) & (BOX737P(X) <-> GBOX553P(X)) & (XBOX597F(X) <-> (BOX597F(X) & XE3G1F(X))) & (XBOX428P(X) <-> (BOX428P(X) & XBOX429P(X))) & (BOX725P(X) <-> GBOX541P(X)) & (BOX9F(X) <-> GE4G4F(X)) & (XBOX208F(X) <-> (BOX208F(X) & XBOX570F(X))) & (BOX718P(X) <-> GBOX534P(X)) & (BOX445P(X) <-> GE5G17P(X)) & (BOX26F(X) <-> G(DIAMOND229F(X) & DIAMOND231F(X))) & (XBOX683F(X) <-> (BOX683F(X) & XDIAMOND257F(X))) & (BOX415P(X) <-> GDIAMOND339P(X)) & (BOX314F(X) <-> GBOX618F(X)) & (BOX56F(X) <-> GBOX308F(X)) & (BOX357P(X) <-> GBOX688P(X)) & (XBOX498P(X) <-> (BOX498P(X) & XBOX374P(X))) & (BOX66F(X) <-> GBOX625F(X)) & (XBOX675F(X) <-> (BOX675F(X) & XBOX584F(X))) & (XBOX319F(X) <-> (BOX319F(X) & XBOX680F(X))) & (XBOX86F(X) <-> (BOX86F(X) & XBOX643F(X))) & (XBOX461P(X) <-> (BOX461P(X) & XBOX462P(X))) & (XBOX526P(X) <-> (BOX526P(X) & XPinvG5F)) & (BOX69F(X) <-> GBOX244F(X)) & (XBOX547P(X) <-> (BOX547P(X) & XPG11F)) & (XBOX458P(X) <-> (BOX458P(X) & XBOX459P(X))) & (XBOX427P(X) <-> (BOX427P(X) & XDIAMOND352P(X))) & (BOX374P(X) <-> GE1G5P(X)) & (BOX268F(X) <-> G!E4G0F(X)) & (BOX510P(X) <-> GE1G6P(X)) & (BOX700P(X) <-> GBOX402P(X)) & (BOX711P(X) <-> GBOX527P(X)) & (BOX123P(X) <-> GDIAMOND337P(X)) & (BOX721P(X) <-> GBOX537P(X)) & (BOX505P(X) <-> GE4G4P(X)) & (BOX47F(X) <-> GBOX283F(X)) & (BOX651F(X) <-> GPinvG13F) & (BOX16F(X) <-> GBOX579F(X)) & (XBOX244F(X) <-> (BOX244F(X) & XE5G28F(X))))


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


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