%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : PUZ074+1 : TPTP v8.1.0. Released v3.5.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n018.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Mon Jul 18 18:27:52 EDT 2022 % Result : Theorem 2.88s 3.07s % Output : Proof 2.88s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : PUZ074+1 : TPTP v8.1.0. Released v3.5.0. % 0.03/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.13/0.34 % Computer : n018.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Sun May 29 00:22:40 EDT 2022 % 0.13/0.34 % CPUTime : % 2.88/3.07 % SZS status Theorem % 2.88/3.07 (* PROOF-FOUND *) % 2.88/3.07 (* BEGIN-PROOF *) % 2.88/3.07 % SZS output start Proof % 2.88/3.07 1. ((cell2) != (cell100)) ((cell100) = (cell2)) ### Sym(=) % 2.88/3.07 2. (((cell1) = (cell1)) /\ ((cell100) = (cell2))) ((cell2) != (cell100)) ### And 1 % 2.88/3.07 3. ((cell2) != (cell1)) ((cell1) = (cell2)) ### Sym(=) % 2.88/3.07 4. (((cell1) = (cell2)) /\ ((cell100) = (cell3))) ((cell2) != (cell1)) ### And 3 % 2.88/3.07 5. ((cell3) != (cell1)) ((cell1) = (cell3)) ### Sym(=) % 2.88/3.07 6. (((cell1) = (cell3)) /\ ((cell100) = (cell4))) ((cell3) != (cell1)) ### And 5 % 2.88/3.07 7. ((cell4) != (cell1)) ((cell1) = (cell4)) ### Sym(=) % 2.88/3.07 8. (((cell1) = (cell4)) /\ ((cell100) = (cell5))) ((cell4) != (cell1)) ### And 7 % 2.88/3.07 9. ((cell5) != (cell1)) ((cell1) = (cell5)) ### Sym(=) % 2.88/3.07 10. (((cell1) = (cell5)) /\ ((cell100) = (cell6))) ((cell5) != (cell1)) ### And 9 % 2.88/3.07 11. ((cell6) != (cell1)) ((cell1) = (cell6)) ### Sym(=) % 2.88/3.07 12. (((cell1) = (cell6)) /\ ((cell100) = (cell7))) ((cell6) != (cell1)) ### And 11 % 2.88/3.07 13. ((cell7) != (cell1)) ((cell1) = (cell7)) ### Sym(=) % 2.88/3.07 14. (((cell1) = (cell7)) /\ ((cell100) = (cell8))) ((cell7) != (cell1)) ### And 13 % 2.88/3.07 15. ((cell8) != (cell1)) ((cell1) = (cell8)) ### Sym(=) % 2.88/3.07 16. (((cell1) = (cell8)) /\ ((cell100) = (cell9))) ((cell8) != (cell1)) ### And 15 % 2.88/3.07 17. ((cell9) != (cell1)) ((cell1) = (cell9)) ### Sym(=) % 2.88/3.07 18. (((cell1) = (cell9)) /\ ((cell100) = (cell10))) ((cell9) != (cell1)) ### And 17 % 2.88/3.07 19. ((cell11) != (cell1)) ((cell1) = (cell11)) ### Sym(=) % 2.88/3.07 20. (((cell1) = (cell11)) /\ ((cell100) = (cell12))) ((cell11) != (cell1)) ### And 19 % 2.88/3.07 21. ((cell12) != (cell1)) ((cell1) = (cell12)) ### Sym(=) % 2.88/3.07 22. (((cell1) = (cell12)) /\ ((cell100) = (cell13))) ((cell12) != (cell1)) ### And 21 % 2.88/3.07 23. ((cell13) != (cell1)) ((cell1) = (cell13)) ### Sym(=) % 2.88/3.07 24. (((cell1) = (cell13)) /\ ((cell100) = (cell14))) ((cell13) != (cell1)) ### And 23 % 2.88/3.07 25. ((cell14) != (cell1)) ((cell1) = (cell14)) ### Sym(=) % 2.88/3.07 26. (((cell1) = (cell14)) /\ ((cell100) = (cell15))) ((cell14) != (cell1)) ### And 25 % 2.88/3.07 27. ((cell15) != (cell1)) ((cell1) = (cell15)) ### Sym(=) % 2.88/3.07 28. (((cell1) = (cell15)) /\ ((cell100) = (cell16))) ((cell15) != (cell1)) ### And 27 % 2.88/3.07 29. ((cell16) != (cell1)) ((cell1) = (cell16)) ### Sym(=) % 2.88/3.07 30. (((cell1) = (cell16)) /\ ((cell100) = (cell17))) ((cell16) != (cell1)) ### And 29 % 2.88/3.07 31. ((cell17) != (cell1)) ((cell1) = (cell17)) ### Sym(=) % 2.88/3.07 32. (((cell1) = (cell17)) /\ ((cell100) = (cell18))) ((cell17) != (cell1)) ### And 31 % 2.88/3.07 33. ((cell18) != (cell1)) ((cell1) = (cell18)) ### Sym(=) % 2.88/3.07 34. (((cell1) = (cell18)) /\ ((cell100) = (cell19))) ((cell18) != (cell1)) ### And 33 % 2.88/3.07 35. ((cell19) != (cell1)) ((cell1) = (cell19)) ### Sym(=) % 2.88/3.07 36. (((cell1) = (cell19)) /\ ((cell100) = (cell20))) ((cell19) != (cell1)) ### And 35 % 2.88/3.07 37. ((cell21) != (cell1)) ((cell1) = (cell21)) ### Sym(=) % 2.88/3.07 38. (((cell1) = (cell21)) /\ ((cell100) = (cell22))) ((cell21) != (cell1)) ### And 37 % 2.88/3.07 39. ((cell22) != (cell1)) ((cell1) = (cell22)) ### Sym(=) % 2.88/3.07 40. (((cell1) = (cell22)) /\ ((cell100) = (cell23))) ((cell22) != (cell1)) ### And 39 % 2.88/3.07 41. ((cell23) != (cell1)) ((cell1) = (cell23)) ### Sym(=) % 2.88/3.07 42. (((cell1) = (cell23)) /\ ((cell100) = (cell24))) ((cell23) != (cell1)) ### And 41 % 2.88/3.07 43. ((cell24) != (cell1)) ((cell1) = (cell24)) ### Sym(=) % 2.88/3.07 44. (((cell1) = (cell24)) /\ ((cell100) = (cell25))) ((cell24) != (cell1)) ### And 43 % 2.88/3.07 45. ((cell25) != (cell1)) ((cell1) = (cell25)) ### Sym(=) % 2.88/3.07 46. (((cell1) = (cell25)) /\ ((cell100) = (cell26))) ((cell25) != (cell1)) ### And 45 % 2.88/3.07 47. ((cell26) != (cell1)) ((cell1) = (cell26)) ### Sym(=) % 2.88/3.07 48. (((cell1) = (cell26)) /\ ((cell100) = (cell27))) ((cell26) != (cell1)) ### And 47 % 2.88/3.07 49. ((cell27) != (cell1)) ((cell1) = (cell27)) ### Sym(=) % 2.88/3.07 50. (((cell1) = (cell27)) /\ ((cell100) = (cell28))) ((cell27) != (cell1)) ### And 49 % 2.88/3.07 51. ((cell28) != (cell1)) ((cell1) = (cell28)) ### Sym(=) % 2.88/3.07 52. (((cell1) = (cell28)) /\ ((cell100) = (cell29))) ((cell28) != (cell1)) ### And 51 % 2.88/3.07 53. ((cell29) != (cell1)) ((cell1) = (cell29)) ### Sym(=) % 2.88/3.07 54. (((cell1) = (cell29)) /\ ((cell100) = (cell30))) ((cell29) != (cell1)) ### And 53 % 2.88/3.07 55. ((cell31) != (cell1)) ((cell1) = (cell31)) ### Sym(=) % 2.88/3.07 56. (((cell1) = (cell31)) /\ ((cell100) = (cell32))) ((cell31) != (cell1)) ### And 55 % 2.88/3.07 57. ((cell32) != (cell1)) ((cell1) = (cell32)) ### Sym(=) % 2.88/3.07 58. (((cell1) = (cell32)) /\ ((cell100) = (cell33))) ((cell32) != (cell1)) ### And 57 % 2.88/3.07 59. ((cell33) != (cell1)) ((cell1) = (cell33)) ### Sym(=) % 2.88/3.07 60. (((cell1) = (cell33)) /\ ((cell100) = (cell34))) ((cell33) != (cell1)) ### And 59 % 2.88/3.07 61. ((cell34) != (cell1)) ((cell1) = (cell34)) ### Sym(=) % 2.88/3.07 62. (((cell1) = (cell34)) /\ ((cell100) = (cell35))) ((cell34) != (cell1)) ### And 61 % 2.88/3.07 63. ((cell35) != (cell1)) ((cell1) = (cell35)) ### Sym(=) % 2.88/3.07 64. (((cell1) = (cell35)) /\ ((cell100) = (cell36))) ((cell35) != (cell1)) ### And 63 % 2.88/3.07 65. ((cell36) != (cell1)) ((cell1) = (cell36)) ### Sym(=) % 2.88/3.07 66. (((cell1) = (cell36)) /\ ((cell100) = (cell37))) ((cell36) != (cell1)) ### And 65 % 2.88/3.07 67. ((cell37) != (cell1)) ((cell1) = (cell37)) ### Sym(=) % 2.88/3.07 68. (((cell1) = (cell37)) /\ ((cell100) = (cell38))) ((cell37) != (cell1)) ### And 67 % 2.88/3.07 69. ((cell38) != (cell1)) ((cell1) = (cell38)) ### Sym(=) % 2.88/3.07 70. (((cell1) = (cell38)) /\ ((cell100) = (cell39))) ((cell38) != (cell1)) ### And 69 % 2.88/3.07 71. ((cell39) != (cell1)) ((cell1) = (cell39)) ### Sym(=) % 2.88/3.07 72. (((cell1) = (cell39)) /\ ((cell100) = (cell40))) ((cell39) != (cell1)) ### And 71 % 2.88/3.07 73. ((cell41) != (cell1)) ((cell1) = (cell41)) ### Sym(=) % 2.88/3.07 74. (((cell1) = (cell41)) /\ ((cell100) = (cell42))) ((cell41) != (cell1)) ### And 73 % 2.88/3.07 75. ((cell42) != (cell1)) ((cell1) = (cell42)) ### Sym(=) % 2.88/3.07 76. (((cell1) = (cell42)) /\ ((cell100) = (cell43))) ((cell42) != (cell1)) ### And 75 % 2.88/3.07 77. ((cell43) != (cell1)) ((cell1) = (cell43)) ### Sym(=) % 2.88/3.07 78. (((cell1) = (cell43)) /\ ((cell100) = (cell44))) ((cell43) != (cell1)) ### And 77 % 2.88/3.07 79. ((cell44) != (cell1)) ((cell1) = (cell44)) ### Sym(=) % 2.88/3.07 80. (((cell1) = (cell44)) /\ ((cell100) = (cell45))) ((cell44) != (cell1)) ### And 79 % 2.88/3.07 81. ((cell45) != (cell1)) ((cell1) = (cell45)) ### Sym(=) % 2.88/3.07 82. (((cell1) = (cell45)) /\ ((cell100) = (cell46))) ((cell45) != (cell1)) ### And 81 % 2.88/3.07 83. ((cell46) != (cell1)) ((cell1) = (cell46)) ### Sym(=) % 2.88/3.07 84. (((cell1) = (cell46)) /\ ((cell100) = (cell47))) ((cell46) != (cell1)) ### And 83 % 2.88/3.07 85. ((cell47) != (cell1)) ((cell1) = (cell47)) ### Sym(=) % 2.88/3.07 86. (((cell1) = (cell47)) /\ ((cell100) = (cell48))) ((cell47) != (cell1)) ### And 85 % 2.88/3.07 87. ((cell48) != (cell1)) ((cell1) = (cell48)) ### Sym(=) % 2.88/3.07 88. (((cell1) = (cell48)) /\ ((cell100) = (cell49))) ((cell48) != (cell1)) ### And 87 % 2.88/3.07 89. ((cell49) != (cell1)) ((cell1) = (cell49)) ### Sym(=) % 2.88/3.07 90. (((cell1) = (cell49)) /\ ((cell100) = (cell50))) ((cell49) != (cell1)) ### And 89 % 2.88/3.07 91. ((cell51) != (cell1)) ((cell1) = (cell51)) ### Sym(=) % 2.88/3.07 92. (((cell1) = (cell51)) /\ ((cell100) = (cell52))) ((cell51) != (cell1)) ### And 91 % 2.88/3.07 93. ((cell52) != (cell1)) ((cell1) = (cell52)) ### Sym(=) % 2.88/3.07 94. (((cell1) = (cell52)) /\ ((cell100) = (cell53))) ((cell52) != (cell1)) ### And 93 % 2.88/3.07 95. ((cell53) != (cell1)) ((cell1) = (cell53)) ### Sym(=) % 2.88/3.07 96. (((cell1) = (cell53)) /\ ((cell100) = (cell54))) ((cell53) != (cell1)) ### And 95 % 2.88/3.07 97. ((cell54) != (cell1)) ((cell1) = (cell54)) ### Sym(=) % 2.88/3.07 98. (((cell1) = (cell54)) /\ ((cell100) = (cell55))) ((cell54) != (cell1)) ### And 97 % 2.88/3.07 99. ((cell55) != (cell1)) ((cell1) = (cell55)) ### Sym(=) % 2.88/3.07 100. (((cell1) = (cell55)) /\ ((cell100) = (cell56))) ((cell55) != (cell1)) ### And 99 % 2.88/3.07 101. ((cell56) != (cell1)) ((cell1) = (cell56)) ### Sym(=) % 2.88/3.07 102. (((cell1) = (cell56)) /\ ((cell100) = (cell57))) ((cell56) != (cell1)) ### And 101 % 2.88/3.07 103. ((cell57) != (cell1)) ((cell1) = (cell57)) ### Sym(=) % 2.88/3.07 104. (((cell1) = (cell57)) /\ ((cell100) = (cell58))) ((cell57) != (cell1)) ### And 103 % 2.88/3.07 105. ((cell58) != (cell1)) ((cell1) = (cell58)) ### Sym(=) % 2.88/3.07 106. (((cell1) = (cell58)) /\ ((cell100) = (cell59))) ((cell58) != (cell1)) ### And 105 % 2.88/3.07 107. ((cell59) != (cell1)) ((cell1) = (cell59)) ### Sym(=) % 2.88/3.07 108. (((cell1) = (cell59)) /\ ((cell100) = (cell60))) ((cell59) != (cell1)) ### And 107 % 2.88/3.07 109. ((cell61) != (cell1)) ((cell1) = (cell61)) ### Sym(=) % 2.88/3.07 110. (((cell1) = (cell61)) /\ ((cell100) = (cell62))) ((cell61) != (cell1)) ### And 109 % 2.88/3.07 111. ((cell62) != (cell1)) ((cell1) = (cell62)) ### Sym(=) % 2.88/3.07 112. (((cell1) = (cell62)) /\ ((cell100) = (cell63))) ((cell62) != (cell1)) ### And 111 % 2.88/3.07 113. ((cell63) != (cell1)) ((cell1) = (cell63)) ### Sym(=) % 2.88/3.07 114. (((cell1) = (cell63)) /\ ((cell100) = (cell64))) ((cell63) != (cell1)) ### And 113 % 2.88/3.07 115. ((cell64) != (cell1)) ((cell1) = (cell64)) ### Sym(=) % 2.88/3.07 116. (((cell1) = (cell64)) /\ ((cell100) = (cell65))) ((cell64) != (cell1)) ### And 115 % 2.88/3.07 117. ((cell65) != (cell1)) ((cell1) = (cell65)) ### Sym(=) % 2.88/3.07 118. (((cell1) = (cell65)) /\ ((cell100) = (cell66))) ((cell65) != (cell1)) ### And 117 % 2.88/3.07 119. ((cell66) != (cell1)) ((cell1) = (cell66)) ### Sym(=) % 2.88/3.07 120. (((cell1) = (cell66)) /\ ((cell100) = (cell67))) ((cell66) != (cell1)) ### And 119 % 2.88/3.07 121. ((cell67) != (cell1)) ((cell1) = (cell67)) ### Sym(=) % 2.88/3.07 122. (((cell1) = (cell67)) /\ ((cell100) = (cell68))) ((cell67) != (cell1)) ### And 121 % 2.88/3.07 123. ((cell68) != (cell1)) ((cell1) = (cell68)) ### Sym(=) % 2.88/3.07 124. (((cell1) = (cell68)) /\ ((cell100) = (cell69))) ((cell68) != (cell1)) ### And 123 % 2.88/3.07 125. ((cell69) != (cell1)) ((cell1) = (cell69)) ### Sym(=) % 2.88/3.07 126. (((cell1) = (cell69)) /\ ((cell100) = (cell70))) ((cell69) != (cell1)) ### And 125 % 2.88/3.07 127. ((cell71) != (cell1)) ((cell1) = (cell71)) ### Sym(=) % 2.88/3.07 128. (((cell1) = (cell71)) /\ ((cell100) = (cell72))) ((cell71) != (cell1)) ### And 127 % 2.88/3.07 129. ((cell72) != (cell1)) ((cell1) = (cell72)) ### Sym(=) % 2.88/3.07 130. (((cell1) = (cell72)) /\ ((cell100) = (cell73))) ((cell72) != (cell1)) ### And 129 % 2.88/3.07 131. ((cell73) != (cell1)) ((cell1) = (cell73)) ### Sym(=) % 2.88/3.07 132. (((cell1) = (cell73)) /\ ((cell100) = (cell74))) ((cell73) != (cell1)) ### And 131 % 2.88/3.07 133. ((cell74) != (cell1)) ((cell1) = (cell74)) ### Sym(=) % 2.88/3.07 134. (((cell1) = (cell74)) /\ ((cell100) = (cell75))) ((cell74) != (cell1)) ### And 133 % 2.88/3.07 135. ((cell75) != (cell1)) ((cell1) = (cell75)) ### Sym(=) % 2.88/3.07 136. (((cell1) = (cell75)) /\ ((cell100) = (cell76))) ((cell75) != (cell1)) ### And 135 % 2.88/3.07 137. ((cell76) != (cell1)) ((cell1) = (cell76)) ### Sym(=) % 2.88/3.07 138. (((cell1) = (cell76)) /\ ((cell100) = (cell77))) ((cell76) != (cell1)) ### And 137 % 2.88/3.07 139. ((cell77) != (cell1)) ((cell1) = (cell77)) ### Sym(=) % 2.88/3.07 140. (((cell1) = (cell77)) /\ ((cell100) = (cell78))) ((cell77) != (cell1)) ### And 139 % 2.88/3.07 141. ((cell78) != (cell1)) ((cell1) = (cell78)) ### Sym(=) % 2.88/3.07 142. (((cell1) = (cell78)) /\ ((cell100) = (cell79))) ((cell78) != (cell1)) ### And 141 % 2.88/3.07 143. ((cell79) != (cell1)) ((cell1) = (cell79)) ### Sym(=) % 2.88/3.07 144. (((cell1) = (cell79)) /\ ((cell100) = (cell80))) ((cell79) != (cell1)) ### And 143 % 2.88/3.07 145. ((cell81) != (cell1)) ((cell1) = (cell81)) ### Sym(=) % 2.88/3.07 146. (((cell1) = (cell81)) /\ ((cell100) = (cell82))) ((cell81) != (cell1)) ### And 145 % 2.88/3.07 147. ((cell82) != (cell1)) ((cell1) = (cell82)) ### Sym(=) % 2.88/3.07 148. (((cell1) = (cell82)) /\ ((cell100) = (cell83))) ((cell82) != (cell1)) ### And 147 % 2.88/3.07 149. ((cell83) != (cell1)) ((cell1) = (cell83)) ### Sym(=) % 2.88/3.07 150. (((cell1) = (cell83)) /\ ((cell100) = (cell84))) ((cell83) != (cell1)) ### And 149 % 2.88/3.07 151. ((cell84) != (cell1)) ((cell1) = (cell84)) ### Sym(=) % 2.88/3.07 152. (((cell1) = (cell84)) /\ ((cell100) = (cell85))) ((cell84) != (cell1)) ### And 151 % 2.88/3.07 153. ((cell85) != (cell1)) ((cell1) = (cell85)) ### Sym(=) % 2.88/3.07 154. (((cell1) = (cell85)) /\ ((cell100) = (cell86))) ((cell85) != (cell1)) ### And 153 % 2.88/3.07 155. ((cell86) != (cell1)) ((cell1) = (cell86)) ### Sym(=) % 2.88/3.07 156. (((cell1) = (cell86)) /\ ((cell100) = (cell87))) ((cell86) != (cell1)) ### And 155 % 2.88/3.07 157. ((cell87) != (cell1)) ((cell1) = (cell87)) ### Sym(=) % 2.88/3.07 158. (((cell1) = (cell87)) /\ ((cell100) = (cell88))) ((cell87) != (cell1)) ### And 157 % 2.88/3.07 159. ((cell88) != (cell1)) ((cell1) = (cell88)) ### Sym(=) % 2.88/3.07 160. (((cell1) = (cell88)) /\ ((cell100) = (cell89))) ((cell88) != (cell1)) ### And 159 % 2.88/3.07 161. ((cell89) != (cell1)) ((cell1) = (cell89)) ### Sym(=) % 2.88/3.07 162. (((cell1) = (cell89)) /\ ((cell100) = (cell90))) ((cell89) != (cell1)) ### And 161 % 2.88/3.07 163. ((cell91) != (cell1)) ((cell1) = (cell91)) ### Sym(=) % 2.88/3.07 164. (((cell1) = (cell91)) /\ ((cell100) = (cell92))) ((cell91) != (cell1)) ### And 163 % 2.88/3.07 165. ((cell92) != (cell1)) ((cell1) = (cell92)) ### Sym(=) % 2.88/3.07 166. (((cell1) = (cell92)) /\ ((cell100) = (cell93))) ((cell92) != (cell1)) ### And 165 % 2.88/3.07 167. ((cell93) != (cell1)) ((cell1) = (cell93)) ### Sym(=) % 2.88/3.07 168. (((cell1) = (cell93)) /\ ((cell100) = (cell94))) ((cell93) != (cell1)) ### And 167 % 2.88/3.07 169. ((cell94) != (cell1)) ((cell1) = (cell94)) ### Sym(=) % 2.88/3.07 170. (((cell1) = (cell94)) /\ ((cell100) = (cell95))) ((cell94) != (cell1)) ### And 169 % 2.88/3.07 171. ((cell95) != (cell1)) ((cell1) = (cell95)) ### Sym(=) % 2.88/3.07 172. (((cell1) = (cell95)) /\ ((cell100) = (cell96))) ((cell95) != (cell1)) ### And 171 % 2.88/3.07 173. ((cell96) != (cell1)) ((cell1) = (cell96)) ### Sym(=) % 2.88/3.07 174. (((cell1) = (cell96)) /\ ((cell100) = (cell97))) ((cell96) != (cell1)) ### And 173 % 2.88/3.07 175. ((cell97) != (cell1)) ((cell1) = (cell97)) ### Sym(=) % 2.88/3.07 176. (((cell1) = (cell97)) /\ ((cell100) = (cell98))) ((cell97) != (cell1)) ### And 175 % 2.88/3.07 177. ((cell98) != (cell1)) ((cell1) = (cell98)) ### Sym(=) % 2.88/3.07 178. (((cell1) = (cell98)) /\ ((cell100) = (cell99))) ((cell98) != (cell1)) ### And 177 % 2.88/3.07 179. ((cell99) != (cell1)) ((cell1) = (cell99)) ### Sym(=) % 2.88/3.07 180. (((cell1) = (cell99)) /\ ((cell100) = (cell100))) ((cell99) != (cell1)) ### And 179 % 2.88/3.07 181. ((cell11) != (cell100)) ((cell100) = (cell11)) ### Sym(=) % 2.88/3.07 182. (((cell1) = (cell1)) /\ ((cell100) = (cell11))) ((cell11) != (cell100)) ### And 181 % 2.88/3.07 183. ((cell2) != (cell1)) ((cell1) = (cell2)) ### Sym(=) % 2.88/3.07 184. (((cell1) = (cell2)) /\ ((cell100) = (cell12))) ((cell2) != (cell1)) ### And 183 % 2.88/3.07 185. ((cell3) != (cell1)) ((cell1) = (cell3)) ### Sym(=) % 2.88/3.07 186. (((cell1) = (cell3)) /\ ((cell100) = (cell13))) ((cell3) != (cell1)) ### And 185 % 2.88/3.07 187. ((cell4) != (cell1)) ((cell1) = (cell4)) ### Sym(=) % 2.88/3.07 188. (((cell1) = (cell4)) /\ ((cell100) = (cell14))) ((cell4) != (cell1)) ### And 187 % 2.88/3.07 189. ((cell5) != (cell1)) ((cell1) = (cell5)) ### Sym(=) % 2.88/3.07 190. (((cell1) = (cell5)) /\ ((cell100) = (cell15))) ((cell5) != (cell1)) ### And 189 % 2.88/3.07 191. ((cell6) != (cell1)) ((cell1) = (cell6)) ### Sym(=) % 2.88/3.07 192. (((cell1) = (cell6)) /\ ((cell100) = (cell16))) ((cell6) != (cell1)) ### And 191 % 2.88/3.07 193. ((cell7) != (cell1)) ((cell1) = (cell7)) ### Sym(=) % 2.88/3.07 194. (((cell1) = (cell7)) /\ ((cell100) = (cell17))) ((cell7) != (cell1)) ### And 193 % 2.88/3.07 195. ((cell8) != (cell1)) ((cell1) = (cell8)) ### Sym(=) % 2.88/3.07 196. (((cell1) = (cell8)) /\ ((cell100) = (cell18))) ((cell8) != (cell1)) ### And 195 % 2.88/3.07 197. ((cell9) != (cell1)) ((cell1) = (cell9)) ### Sym(=) % 2.88/3.07 198. (((cell1) = (cell9)) /\ ((cell100) = (cell19))) ((cell9) != (cell1)) ### And 197 % 2.88/3.07 199. ((cell10) != (cell1)) ((cell1) = (cell10)) ### Sym(=) % 2.88/3.07 200. (((cell1) = (cell10)) /\ ((cell100) = (cell20))) ((cell10) != (cell1)) ### And 199 % 2.88/3.07 201. ((cell11) != (cell1)) ((cell1) = (cell11)) ### Sym(=) % 2.88/3.07 202. (((cell1) = (cell11)) /\ ((cell100) = (cell21))) ((cell11) != (cell1)) ### And 201 % 2.88/3.07 203. ((cell12) != (cell1)) ((cell1) = (cell12)) ### Sym(=) % 2.88/3.07 204. (((cell1) = (cell12)) /\ ((cell100) = (cell22))) ((cell12) != (cell1)) ### And 203 % 2.88/3.07 205. ((cell13) != (cell1)) ((cell1) = (cell13)) ### Sym(=) % 2.88/3.07 206. (((cell1) = (cell13)) /\ ((cell100) = (cell23))) ((cell13) != (cell1)) ### And 205 % 2.88/3.07 207. ((cell14) != (cell1)) ((cell1) = (cell14)) ### Sym(=) % 2.88/3.07 208. (((cell1) = (cell14)) /\ ((cell100) = (cell24))) ((cell14) != (cell1)) ### And 207 % 2.88/3.07 209. ((cell15) != (cell1)) ((cell1) = (cell15)) ### Sym(=) % 2.88/3.07 210. (((cell1) = (cell15)) /\ ((cell100) = (cell25))) ((cell15) != (cell1)) ### And 209 % 2.88/3.07 211. ((cell16) != (cell1)) ((cell1) = (cell16)) ### Sym(=) % 2.88/3.07 212. (((cell1) = (cell16)) /\ ((cell100) = (cell26))) ((cell16) != (cell1)) ### And 211 % 2.88/3.07 213. ((cell17) != (cell1)) ((cell1) = (cell17)) ### Sym(=) % 2.88/3.07 214. (((cell1) = (cell17)) /\ ((cell100) = (cell27))) ((cell17) != (cell1)) ### And 213 % 2.88/3.07 215. ((cell18) != (cell1)) ((cell1) = (cell18)) ### Sym(=) % 2.88/3.07 216. (((cell1) = (cell18)) /\ ((cell100) = (cell28))) ((cell18) != (cell1)) ### And 215 % 2.88/3.07 217. ((cell19) != (cell1)) ((cell1) = (cell19)) ### Sym(=) % 2.88/3.07 218. (((cell1) = (cell19)) /\ ((cell100) = (cell29))) ((cell19) != (cell1)) ### And 217 % 2.88/3.07 219. ((cell20) != (cell1)) ((cell1) = (cell20)) ### Sym(=) % 2.88/3.07 220. (((cell1) = (cell20)) /\ ((cell100) = (cell30))) ((cell20) != (cell1)) ### And 219 % 2.88/3.07 221. ((cell21) != (cell1)) ((cell1) = (cell21)) ### Sym(=) % 2.88/3.07 222. (((cell1) = (cell21)) /\ ((cell100) = (cell31))) ((cell21) != (cell1)) ### And 221 % 2.88/3.07 223. ((cell22) != (cell1)) ((cell1) = (cell22)) ### Sym(=) % 2.88/3.07 224. (((cell1) = (cell22)) /\ ((cell100) = (cell32))) ((cell22) != (cell1)) ### And 223 % 2.88/3.07 225. ((cell23) != (cell1)) ((cell1) = (cell23)) ### Sym(=) % 2.88/3.07 226. (((cell1) = (cell23)) /\ ((cell100) = (cell33))) ((cell23) != (cell1)) ### And 225 % 2.88/3.07 227. ((cell24) != (cell1)) ((cell1) = (cell24)) ### Sym(=) % 2.88/3.07 228. (((cell1) = (cell24)) /\ ((cell100) = (cell34))) ((cell24) != (cell1)) ### And 227 % 2.88/3.07 229. ((cell25) != (cell1)) ((cell1) = (cell25)) ### Sym(=) % 2.88/3.07 230. (((cell1) = (cell25)) /\ ((cell100) = (cell35))) ((cell25) != (cell1)) ### And 229 % 2.88/3.07 231. ((cell26) != (cell1)) ((cell1) = (cell26)) ### Sym(=) % 2.88/3.07 232. (((cell1) = (cell26)) /\ ((cell100) = (cell36))) ((cell26) != (cell1)) ### And 231 % 2.88/3.07 233. ((cell27) != (cell1)) ((cell1) = (cell27)) ### Sym(=) % 2.88/3.07 234. (((cell1) = (cell27)) /\ ((cell100) = (cell37))) ((cell27) != (cell1)) ### And 233 % 2.88/3.07 235. ((cell28) != (cell1)) ((cell1) = (cell28)) ### Sym(=) % 2.88/3.07 236. (((cell1) = (cell28)) /\ ((cell100) = (cell38))) ((cell28) != (cell1)) ### And 235 % 2.88/3.07 237. ((cell29) != (cell1)) ((cell1) = (cell29)) ### Sym(=) % 2.88/3.07 238. (((cell1) = (cell29)) /\ ((cell100) = (cell39))) ((cell29) != (cell1)) ### And 237 % 2.88/3.07 239. ((cell30) != (cell1)) ((cell1) = (cell30)) ### Sym(=) % 2.88/3.07 240. (((cell1) = (cell30)) /\ ((cell100) = (cell40))) ((cell30) != (cell1)) ### And 239 % 2.88/3.07 241. ((cell31) != (cell1)) ((cell1) = (cell31)) ### Sym(=) % 2.88/3.07 242. (((cell1) = (cell31)) /\ ((cell100) = (cell41))) ((cell31) != (cell1)) ### And 241 % 2.88/3.07 243. ((cell32) != (cell1)) ((cell1) = (cell32)) ### Sym(=) % 2.88/3.07 244. (((cell1) = (cell32)) /\ ((cell100) = (cell42))) ((cell32) != (cell1)) ### And 243 % 2.88/3.07 245. ((cell33) != (cell1)) ((cell1) = (cell33)) ### Sym(=) % 2.88/3.07 246. (((cell1) = (cell33)) /\ ((cell100) = (cell43))) ((cell33) != (cell1)) ### And 245 % 2.88/3.07 247. ((cell34) != (cell1)) ((cell1) = (cell34)) ### Sym(=) % 2.88/3.07 248. (((cell1) = (cell34)) /\ ((cell100) = (cell44))) ((cell34) != (cell1)) ### And 247 % 2.88/3.07 249. ((cell35) != (cell1)) ((cell1) = (cell35)) ### Sym(=) % 2.88/3.07 250. (((cell1) = (cell35)) /\ ((cell100) = (cell45))) ((cell35) != (cell1)) ### And 249 % 2.88/3.07 251. ((cell36) != (cell1)) ((cell1) = (cell36)) ### Sym(=) % 2.88/3.07 252. (((cell1) = (cell36)) /\ ((cell100) = (cell46))) ((cell36) != (cell1)) ### And 251 % 2.88/3.07 253. ((cell37) != (cell1)) ((cell1) = (cell37)) ### Sym(=) % 2.88/3.07 254. (((cell1) = (cell37)) /\ ((cell100) = (cell47))) ((cell37) != (cell1)) ### And 253 % 2.88/3.07 255. ((cell38) != (cell1)) ((cell1) = (cell38)) ### Sym(=) % 2.88/3.07 256. (((cell1) = (cell38)) /\ ((cell100) = (cell48))) ((cell38) != (cell1)) ### And 255 % 2.88/3.07 257. ((cell39) != (cell1)) ((cell1) = (cell39)) ### Sym(=) % 2.88/3.07 258. (((cell1) = (cell39)) /\ ((cell100) = (cell49))) ((cell39) != (cell1)) ### And 257 % 2.88/3.07 259. ((cell40) != (cell1)) ((cell1) = (cell40)) ### Sym(=) % 2.88/3.07 260. (((cell1) = (cell40)) /\ ((cell100) = (cell50))) ((cell40) != (cell1)) ### And 259 % 2.88/3.07 261. ((cell41) != (cell1)) ((cell1) = (cell41)) ### Sym(=) % 2.88/3.07 262. (((cell1) = (cell41)) /\ ((cell100) = (cell51))) ((cell41) != (cell1)) ### And 261 % 2.88/3.07 263. ((cell42) != (cell1)) ((cell1) = (cell42)) ### Sym(=) % 2.88/3.07 264. (((cell1) = (cell42)) /\ ((cell100) = (cell52))) ((cell42) != (cell1)) ### And 263 % 2.88/3.07 265. ((cell43) != (cell1)) ((cell1) = (cell43)) ### Sym(=) % 2.88/3.07 266. (((cell1) = (cell43)) /\ ((cell100) = (cell53))) ((cell43) != (cell1)) ### And 265 % 2.88/3.07 267. ((cell44) != (cell1)) ((cell1) = (cell44)) ### Sym(=) % 2.88/3.07 268. (((cell1) = (cell44)) /\ ((cell100) = (cell54))) ((cell44) != (cell1)) ### And 267 % 2.88/3.07 269. ((cell45) != (cell1)) ((cell1) = (cell45)) ### Sym(=) % 2.88/3.07 270. (((cell1) = (cell45)) /\ ((cell100) = (cell55))) ((cell45) != (cell1)) ### And 269 % 2.88/3.07 271. ((cell46) != (cell1)) ((cell1) = (cell46)) ### Sym(=) % 2.88/3.07 272. (((cell1) = (cell46)) /\ ((cell100) = (cell56))) ((cell46) != (cell1)) ### And 271 % 2.88/3.07 273. ((cell47) != (cell1)) ((cell1) = (cell47)) ### Sym(=) % 2.88/3.07 274. (((cell1) = (cell47)) /\ ((cell100) = (cell57))) ((cell47) != (cell1)) ### And 273 % 2.88/3.07 275. ((cell48) != (cell1)) ((cell1) = (cell48)) ### Sym(=) % 2.88/3.07 276. (((cell1) = (cell48)) /\ ((cell100) = (cell58))) ((cell48) != (cell1)) ### And 275 % 2.88/3.07 277. ((cell49) != (cell1)) ((cell1) = (cell49)) ### Sym(=) % 2.88/3.07 278. (((cell1) = (cell49)) /\ ((cell100) = (cell59))) ((cell49) != (cell1)) ### And 277 % 2.88/3.07 279. ((cell50) != (cell1)) ((cell1) = (cell50)) ### Sym(=) % 2.88/3.07 280. (((cell1) = (cell50)) /\ ((cell100) = (cell60))) ((cell50) != (cell1)) ### And 279 % 2.88/3.07 281. ((cell51) != (cell1)) ((cell1) = (cell51)) ### Sym(=) % 2.88/3.07 282. (((cell1) = (cell51)) /\ ((cell100) = (cell61))) ((cell51) != (cell1)) ### And 281 % 2.88/3.07 283. ((cell52) != (cell1)) ((cell1) = (cell52)) ### Sym(=) % 2.88/3.07 284. (((cell1) = (cell52)) /\ ((cell100) = (cell62))) ((cell52) != (cell1)) ### And 283 % 2.88/3.07 285. ((cell53) != (cell1)) ((cell1) = (cell53)) ### Sym(=) % 2.88/3.07 286. (((cell1) = (cell53)) /\ ((cell100) = (cell63))) ((cell53) != (cell1)) ### And 285 % 2.88/3.07 287. ((cell54) != (cell1)) ((cell1) = (cell54)) ### Sym(=) % 2.88/3.07 288. (((cell1) = (cell54)) /\ ((cell100) = (cell64))) ((cell54) != (cell1)) ### And 287 % 2.88/3.07 289. ((cell55) != (cell1)) ((cell1) = (cell55)) ### Sym(=) % 2.88/3.07 290. (((cell1) = (cell55)) /\ ((cell100) = (cell65))) ((cell55) != (cell1)) ### And 289 % 2.88/3.07 291. ((cell56) != (cell1)) ((cell1) = (cell56)) ### Sym(=) % 2.88/3.07 292. (((cell1) = (cell56)) /\ ((cell100) = (cell66))) ((cell56) != (cell1)) ### And 291 % 2.88/3.07 293. ((cell57) != (cell1)) ((cell1) = (cell57)) ### Sym(=) % 2.88/3.07 294. (((cell1) = (cell57)) /\ ((cell100) = (cell67))) ((cell57) != (cell1)) ### And 293 % 2.88/3.07 295. ((cell58) != (cell1)) ((cell1) = (cell58)) ### Sym(=) % 2.88/3.07 296. (((cell1) = (cell58)) /\ ((cell100) = (cell68))) ((cell58) != (cell1)) ### And 295 % 2.88/3.07 297. ((cell59) != (cell1)) ((cell1) = (cell59)) ### Sym(=) % 2.88/3.07 298. (((cell1) = (cell59)) /\ ((cell100) = (cell69))) ((cell59) != (cell1)) ### And 297 % 2.88/3.07 299. ((cell60) != (cell1)) ((cell1) = (cell60)) ### Sym(=) % 2.88/3.07 300. (((cell1) = (cell60)) /\ ((cell100) = (cell70))) ((cell60) != (cell1)) ### And 299 % 2.88/3.07 301. ((cell61) != (cell1)) ((cell1) = (cell61)) ### Sym(=) % 2.88/3.07 302. (((cell1) = (cell61)) /\ ((cell100) = (cell71))) ((cell61) != (cell1)) ### And 301 % 2.88/3.07 303. ((cell62) != (cell1)) ((cell1) = (cell62)) ### Sym(=) % 2.88/3.07 304. (((cell1) = (cell62)) /\ ((cell100) = (cell72))) ((cell62) != (cell1)) ### And 303 % 2.88/3.07 305. ((cell63) != (cell1)) ((cell1) = (cell63)) ### Sym(=) % 2.88/3.07 306. (((cell1) = (cell63)) /\ ((cell100) = (cell73))) ((cell63) != (cell1)) ### And 305 % 2.88/3.07 307. ((cell64) != (cell1)) ((cell1) = (cell64)) ### Sym(=) % 2.88/3.07 308. (((cell1) = (cell64)) /\ ((cell100) = (cell74))) ((cell64) != (cell1)) ### And 307 % 2.88/3.07 309. ((cell65) != (cell1)) ((cell1) = (cell65)) ### Sym(=) % 2.88/3.07 310. (((cell1) = (cell65)) /\ ((cell100) = (cell75))) ((cell65) != (cell1)) ### And 309 % 2.88/3.07 311. ((cell66) != (cell1)) ((cell1) = (cell66)) ### Sym(=) % 2.88/3.07 312. (((cell1) = (cell66)) /\ ((cell100) = (cell76))) ((cell66) != (cell1)) ### And 311 % 2.88/3.07 313. ((cell67) != (cell1)) ((cell1) = (cell67)) ### Sym(=) % 2.88/3.07 314. (((cell1) = (cell67)) /\ ((cell100) = (cell77))) ((cell67) != (cell1)) ### And 313 % 2.88/3.07 315. ((cell68) != (cell1)) ((cell1) = (cell68)) ### Sym(=) % 2.88/3.07 316. (((cell1) = (cell68)) /\ ((cell100) = (cell78))) ((cell68) != (cell1)) ### And 315 % 2.88/3.07 317. ((cell69) != (cell1)) ((cell1) = (cell69)) ### Sym(=) % 2.88/3.07 318. (((cell1) = (cell69)) /\ ((cell100) = (cell79))) ((cell69) != (cell1)) ### And 317 % 2.88/3.07 319. ((cell70) != (cell1)) ((cell1) = (cell70)) ### Sym(=) % 2.88/3.07 320. (((cell1) = (cell70)) /\ ((cell100) = (cell80))) ((cell70) != (cell1)) ### And 319 % 2.88/3.07 321. ((cell71) != (cell1)) ((cell1) = (cell71)) ### Sym(=) % 2.88/3.07 322. (((cell1) = (cell71)) /\ ((cell100) = (cell81))) ((cell71) != (cell1)) ### And 321 % 2.88/3.07 323. ((cell72) != (cell1)) ((cell1) = (cell72)) ### Sym(=) % 2.88/3.07 324. (((cell1) = (cell72)) /\ ((cell100) = (cell82))) ((cell72) != (cell1)) ### And 323 % 2.88/3.07 325. ((cell73) != (cell1)) ((cell1) = (cell73)) ### Sym(=) % 2.88/3.07 326. (((cell1) = (cell73)) /\ ((cell100) = (cell83))) ((cell73) != (cell1)) ### And 325 % 2.88/3.07 327. ((cell74) != (cell1)) ((cell1) = (cell74)) ### Sym(=) % 2.88/3.07 328. (((cell1) = (cell74)) /\ ((cell100) = (cell84))) ((cell74) != (cell1)) ### And 327 % 2.88/3.07 329. ((cell75) != (cell1)) ((cell1) = (cell75)) ### Sym(=) % 2.88/3.07 330. (((cell1) = (cell75)) /\ ((cell100) = (cell85))) ((cell75) != (cell1)) ### And 329 % 2.88/3.07 331. ((cell76) != (cell1)) ((cell1) = (cell76)) ### Sym(=) % 2.88/3.07 332. (((cell1) = (cell76)) /\ ((cell100) = (cell86))) ((cell76) != (cell1)) ### And 331 % 2.88/3.07 333. ((cell77) != (cell1)) ((cell1) = (cell77)) ### Sym(=) % 2.88/3.07 334. (((cell1) = (cell77)) /\ ((cell100) = (cell87))) ((cell77) != (cell1)) ### And 333 % 2.88/3.07 335. ((cell78) != (cell1)) ((cell1) = (cell78)) ### Sym(=) % 2.88/3.07 336. (((cell1) = (cell78)) /\ ((cell100) = (cell88))) ((cell78) != (cell1)) ### And 335 % 2.88/3.07 337. ((cell79) != (cell1)) ((cell1) = (cell79)) ### Sym(=) % 2.88/3.07 338. (((cell1) = (cell79)) /\ ((cell100) = (cell89))) ((cell79) != (cell1)) ### And 337 % 2.88/3.07 339. ((cell80) != (cell1)) ((cell1) = (cell80)) ### Sym(=) % 2.88/3.07 340. (((cell1) = (cell80)) /\ ((cell100) = (cell90))) ((cell80) != (cell1)) ### And 339 % 2.88/3.07 341. ((cell81) != (cell1)) ((cell1) = (cell81)) ### Sym(=) % 2.88/3.07 342. (((cell1) = (cell81)) /\ ((cell100) = (cell91))) ((cell81) != (cell1)) ### And 341 % 2.88/3.07 343. ((cell82) != (cell1)) ((cell1) = (cell82)) ### Sym(=) % 2.88/3.07 344. (((cell1) = (cell82)) /\ ((cell100) = (cell92))) ((cell82) != (cell1)) ### And 343 % 2.88/3.07 345. ((cell83) != (cell1)) ((cell1) = (cell83)) ### Sym(=) % 2.88/3.07 346. (((cell1) = (cell83)) /\ ((cell100) = (cell93))) ((cell83) != (cell1)) ### And 345 % 2.88/3.07 347. ((cell84) != (cell1)) ((cell1) = (cell84)) ### Sym(=) % 2.88/3.07 348. (((cell1) = (cell84)) /\ ((cell100) = (cell94))) ((cell84) != (cell1)) ### And 347 % 2.88/3.07 349. ((cell85) != (cell1)) ((cell1) = (cell85)) ### Sym(=) % 2.88/3.07 350. (((cell1) = (cell85)) /\ ((cell100) = (cell95))) ((cell85) != (cell1)) ### And 349 % 2.88/3.07 351. ((cell86) != (cell1)) ((cell1) = (cell86)) ### Sym(=) % 2.88/3.07 352. (((cell1) = (cell86)) /\ ((cell100) = (cell96))) ((cell86) != (cell1)) ### And 351 % 2.88/3.07 353. ((cell87) != (cell1)) ((cell1) = (cell87)) ### Sym(=) % 2.88/3.07 354. (((cell1) = (cell87)) /\ ((cell100) = (cell97))) ((cell87) != (cell1)) ### And 353 % 2.88/3.07 355. ((cell88) != (cell1)) ((cell1) = (cell88)) ### Sym(=) % 2.88/3.07 356. (((cell1) = (cell88)) /\ ((cell100) = (cell98))) ((cell88) != (cell1)) ### And 355 % 2.88/3.07 357. ((cell89) != (cell1)) ((cell1) = (cell89)) ### Sym(=) % 2.88/3.07 358. (((cell1) = (cell89)) /\ ((cell100) = (cell99))) ((cell89) != (cell1)) ### And 357 % 2.88/3.07 359. ((cell90) != (cell1)) ((cell1) = (cell90)) ### Sym(=) % 2.88/3.07 360. (((cell1) = (cell90)) /\ ((cell100) = (cell100))) ((cell90) != (cell1)) ### And 359 % 2.88/3.07 361. ((((cell1) = (cell1)) /\ ((cell100) = (cell2))) \/ ((((cell1) = (cell2)) /\ ((cell100) = (cell3))) \/ ((((cell1) = (cell3)) /\ ((cell100) = (cell4))) \/ ((((cell1) = (cell4)) /\ ((cell100) = (cell5))) \/ ((((cell1) = (cell5)) /\ ((cell100) = (cell6))) \/ ((((cell1) = (cell6)) /\ ((cell100) = (cell7))) \/ ((((cell1) = (cell7)) /\ ((cell100) = (cell8))) \/ ((((cell1) = (cell8)) /\ ((cell100) = (cell9))) \/ ((((cell1) = (cell9)) /\ ((cell100) = (cell10))) \/ ((((cell1) = (cell11)) /\ ((cell100) = (cell12))) \/ ((((cell1) = (cell12)) /\ ((cell100) = (cell13))) \/ ((((cell1) = (cell13)) /\ ((cell100) = (cell14))) \/ ((((cell1) = (cell14)) /\ ((cell100) = (cell15))) \/ ((((cell1) = (cell15)) /\ ((cell100) = (cell16))) \/ ((((cell1) = (cell16)) /\ ((cell100) = (cell17))) \/ ((((cell1) = (cell17)) /\ ((cell100) = (cell18))) \/ ((((cell1) = (cell18)) /\ ((cell100) = (cell19))) \/ ((((cell1) = (cell19)) /\ ((cell100) = (cell20))) \/ ((((cell1) = (cell21)) /\ ((cell100) = (cell22))) \/ ((((cell1) = (cell22)) /\ ((cell100) = (cell23))) \/ ((((cell1) = (cell23)) /\ ((cell100) = (cell24))) \/ ((((cell1) = (cell24)) /\ ((cell100) = (cell25))) \/ ((((cell1) = (cell25)) /\ ((cell100) = (cell26))) \/ ((((cell1) = (cell26)) /\ ((cell100) = (cell27))) \/ ((((cell1) = (cell27)) /\ ((cell100) = (cell28))) \/ ((((cell1) = (cell28)) /\ ((cell100) = (cell29))) \/ ((((cell1) = (cell29)) /\ ((cell100) = (cell30))) \/ ((((cell1) = (cell31)) /\ ((cell100) = (cell32))) \/ ((((cell1) = (cell32)) /\ ((cell100) = (cell33))) \/ ((((cell1) = (cell33)) /\ ((cell100) = (cell34))) \/ ((((cell1) = (cell34)) /\ ((cell100) = (cell35))) \/ ((((cell1) = (cell35)) /\ ((cell100) = (cell36))) \/ ((((cell1) = (cell36)) /\ ((cell100) = (cell37))) \/ ((((cell1) = (cell37)) /\ ((cell100) = (cell38))) \/ ((((cell1) = (cell38)) /\ ((cell100) = (cell39))) \/ ((((cell1) = (cell39)) /\ ((cell100) = (cell40))) \/ ((((cell1) = (cell41)) /\ ((cell100) = (cell42))) \/ ((((cell1) = (cell42)) /\ ((cell100) = (cell43))) \/ ((((cell1) = (cell43)) /\ ((cell100) = (cell44))) \/ ((((cell1) = (cell44)) /\ ((cell100) = (cell45))) \/ ((((cell1) = (cell45)) /\ ((cell100) = (cell46))) \/ ((((cell1) = (cell46)) /\ ((cell100) = (cell47))) \/ ((((cell1) = (cell47)) /\ ((cell100) = (cell48))) \/ ((((cell1) = (cell48)) /\ ((cell100) = (cell49))) \/ ((((cell1) = (cell49)) /\ ((cell100) = (cell50))) \/ ((((cell1) = (cell51)) /\ ((cell100) = (cell52))) \/ ((((cell1) = (cell52)) /\ ((cell100) = (cell53))) \/ ((((cell1) = (cell53)) /\ ((cell100) = (cell54))) \/ ((((cell1) = (cell54)) /\ ((cell100) = (cell55))) \/ ((((cell1) = (cell55)) /\ ((cell100) = (cell56))) \/ ((((cell1) = (cell56)) /\ ((cell100) = (cell57))) \/ ((((cell1) = (cell57)) /\ ((cell100) = (cell58))) \/ ((((cell1) = (cell58)) /\ ((cell100) = (cell59))) \/ ((((cell1) = (cell59)) /\ ((cell100) = (cell60))) \/ ((((cell1) = (cell61)) /\ ((cell100) = (cell62))) \/ ((((cell1) = (cell62)) /\ ((cell100) = (cell63))) \/ ((((cell1) = (cell63)) /\ ((cell100) = (cell64))) \/ ((((cell1) = (cell64)) /\ ((cell100) = (cell65))) \/ ((((cell1) = (cell65)) /\ ((cell100) = (cell66))) \/ ((((cell1) = (cell66)) /\ ((cell100) = (cell67))) \/ ((((cell1) = (cell67)) /\ ((cell100) = (cell68))) \/ ((((cell1) = (cell68)) /\ ((cell100) = (cell69))) \/ ((((cell1) = (cell69)) /\ ((cell100) = (cell70))) \/ ((((cell1) = (cell71)) /\ ((cell100) = (cell72))) \/ ((((cell1) = (cell72)) /\ ((cell100) = (cell73))) \/ ((((cell1) = (cell73)) /\ ((cell100) = (cell74))) \/ ((((cell1) = (cell74)) /\ ((cell100) = (cell75))) \/ ((((cell1) = (cell75)) /\ ((cell100) = (cell76))) \/ ((((cell1) = (cell76)) /\ ((cell100) = (cell77))) \/ ((((cell1) = (cell77)) /\ ((cell100) = (cell78))) \/ ((((cell1) = (cell78)) /\ ((cell100) = (cell79))) \/ ((((cell1) = (cell79)) /\ ((cell100) = (cell80))) \/ ((((cell1) = (cell81)) /\ ((cell100) = (cell82))) \/ ((((cell1) = (cell82)) /\ ((cell100) = (cell83))) \/ ((((cell1) = (cell83)) /\ ((cell100) = (cell84))) \/ ((((cell1) = (cell84)) /\ ((cell100) = (cell85))) \/ ((((cell1) = (cell85)) /\ ((cell100) = (cell86))) \/ ((((cell1) = (cell86)) /\ ((cell100) = (cell87))) \/ ((((cell1) = (cell87)) /\ ((cell100) = (cell88))) \/ ((((cell1) = (cell88)) /\ ((cell100) = (cell89))) \/ ((((cell1) = (cell89)) /\ ((cell100) = (cell90))) \/ ((((cell1) = (cell91)) /\ ((cell100) = (cell92))) \/ ((((cell1) = (cell92)) /\ ((cell100) = (cell93))) \/ ((((cell1) = (cell93)) /\ ((cell100) = (cell94))) \/ ((((cell1) = (cell94)) /\ ((cell100) = (cell95))) \/ ((((cell1) = (cell95)) /\ ((cell100) = (cell96))) \/ ((((cell1) = (cell96)) /\ ((cell100) = (cell97))) \/ ((((cell1) = (cell97)) /\ ((cell100) = (cell98))) \/ ((((cell1) = (cell98)) /\ ((cell100) = (cell99))) \/ ((((cell1) = (cell99)) /\ ((cell100) = (cell100))) \/ ((((cell1) = (cell1)) /\ ((cell100) = (cell11))) \/ ((((cell1) = (cell2)) /\ ((cell100) = (cell12))) \/ ((((cell1) = (cell3)) /\ ((cell100) = (cell13))) \/ ((((cell1) = (cell4)) /\ ((cell100) = (cell14))) \/ ((((cell1) = (cell5)) /\ ((cell100) = (cell15))) \/ ((((cell1) = (cell6)) /\ ((cell100) = (cell16))) \/ ((((cell1) = (cell7)) /\ ((cell100) = (cell17))) \/ ((((cell1) = (cell8)) /\ ((cell100) = (cell18))) \/ ((((cell1) = (cell9)) /\ ((cell100) = (cell19))) \/ ((((cell1) = (cell10)) /\ ((cell100) = (cell20))) \/ ((((cell1) = (cell11)) /\ ((cell100) = (cell21))) \/ ((((cell1) = (cell12)) /\ ((cell100) = (cell22))) \/ ((((cell1) = (cell13)) /\ ((cell100) = (cell23))) \/ ((((cell1) = (cell14)) /\ ((cell100) = (cell24))) \/ ((((cell1) = (cell15)) /\ ((cell100) = (cell25))) \/ ((((cell1) = (cell16)) /\ ((cell100) = (cell26))) \/ ((((cell1) = (cell17)) /\ ((cell100) = (cell27))) \/ ((((cell1) = (cell18)) /\ ((cell100) = (cell28))) \/ ((((cell1) = (cell19)) /\ ((cell100) = (cell29))) \/ ((((cell1) = (cell20)) /\ ((cell100) = (cell30))) \/ ((((cell1) = (cell21)) /\ ((cell100) = (cell31))) \/ ((((cell1) = (cell22)) /\ ((cell100) = (cell32))) \/ ((((cell1) = (cell23)) /\ ((cell100) = (cell33))) \/ ((((cell1) = (cell24)) /\ ((cell100) = (cell34))) \/ ((((cell1) = (cell25)) /\ ((cell100) = (cell35))) \/ ((((cell1) = (cell26)) /\ ((cell100) = (cell36))) \/ ((((cell1) = (cell27)) /\ ((cell100) = (cell37))) \/ ((((cell1) = (cell28)) /\ ((cell100) = (cell38))) \/ ((((cell1) = (cell29)) /\ ((cell100) = (cell39))) \/ ((((cell1) = (cell30)) /\ ((cell100) = (cell40))) \/ ((((cell1) = (cell31)) /\ ((cell100) = (cell41))) \/ ((((cell1) = (cell32)) /\ ((cell100) = (cell42))) \/ ((((cell1) = (cell33)) /\ ((cell100) = (cell43))) \/ ((((cell1) = (cell34)) /\ ((cell100) = (cell44))) \/ ((((cell1) = (cell35)) /\ ((cell100) = (cell45))) \/ ((((cell1) = (cell36)) /\ ((cell100) = (cell46))) \/ ((((cell1) = (cell37)) /\ ((cell100) = (cell47))) \/ ((((cell1) = (cell38)) /\ ((cell100) = (cell48))) \/ ((((cell1) = (cell39)) /\ ((cell100) = (cell49))) \/ ((((cell1) = (cell40)) /\ ((cell100) = (cell50))) \/ ((((cell1) = (cell41)) /\ ((cell100) = (cell51))) \/ ((((cell1) = (cell42)) /\ ((cell100) = (cell52))) \/ ((((cell1) = (cell43)) /\ ((cell100) = (cell53))) \/ ((((cell1) = (cell44)) /\ ((cell100) = (cell54))) \/ ((((cell1) = (cell45)) /\ ((cell100) = (cell55))) \/ ((((cell1) = (cell46)) /\ ((cell100) = (cell56))) \/ ((((cell1) = (cell47)) /\ ((cell100) = (cell57))) \/ ((((cell1) = (cell48)) /\ ((cell100) = (cell58))) \/ ((((cell1) = (cell49)) /\ ((cell100) = (cell59))) \/ ((((cell1) = (cell50)) /\ ((cell100) = (cell60))) \/ ((((cell1) = (cell51)) /\ ((cell100) = (cell61))) \/ ((((cell1) = (cell52)) /\ ((cell100) = (cell62))) \/ ((((cell1) = (cell53)) /\ ((cell100) = (cell63))) \/ ((((cell1) = (cell54)) /\ ((cell100) = (cell64))) \/ ((((cell1) = (cell55)) /\ ((cell100) = (cell65))) \/ ((((cell1) = (cell56)) /\ ((cell100) = (cell66))) \/ ((((cell1) = (cell57)) /\ ((cell100) = (cell67))) \/ ((((cell1) = (cell58)) /\ ((cell100) = (cell68))) \/ ((((cell1) = (cell59)) /\ ((cell100) = (cell69))) \/ ((((cell1) = (cell60)) /\ ((cell100) = (cell70))) \/ ((((cell1) = (cell61)) /\ ((cell100) = (cell71))) \/ ((((cell1) = (cell62)) /\ ((cell100) = (cell72))) \/ ((((cell1) = (cell63)) /\ ((cell100) = (cell73))) \/ ((((cell1) = (cell64)) /\ ((cell100) = (cell74))) \/ ((((cell1) = (cell65)) /\ ((cell100) = (cell75))) \/ ((((cell1) = (cell66)) /\ ((cell100) = (cell76))) \/ ((((cell1) = (cell67)) /\ ((cell100) = (cell77))) \/ ((((cell1) = (cell68)) /\ ((cell100) = (cell78))) \/ ((((cell1) = (cell69)) /\ ((cell100) = (cell79))) \/ ((((cell1) = (cell70)) /\ ((cell100) = (cell80))) \/ ((((cell1) = (cell71)) /\ ((cell100) = (cell81))) \/ ((((cell1) = (cell72)) /\ ((cell100) = (cell82))) \/ ((((cell1) = (cell73)) /\ ((cell100) = (cell83))) \/ ((((cell1) = (cell74)) /\ ((cell100) = (cell84))) \/ ((((cell1) = (cell75)) /\ ((cell100) = (cell85))) \/ ((((cell1) = (cell76)) /\ ((cell100) = (cell86))) \/ ((((cell1) = (cell77)) /\ ((cell100) = (cell87))) \/ ((((cell1) = (cell78)) /\ ((cell100) = (cell88))) \/ ((((cell1) = (cell79)) /\ ((cell100) = (cell89))) \/ ((((cell1) = (cell80)) /\ ((cell100) = (cell90))) \/ ((((cell1) = (cell81)) /\ ((cell100) = (cell91))) \/ ((((cell1) = (cell82)) /\ ((cell100) = (cell92))) \/ ((((cell1) = (cell83)) /\ ((cell100) = (cell93))) \/ ((((cell1) = (cell84)) /\ ((cell100) = (cell94))) \/ ((((cell1) = (cell85)) /\ ((cell100) = (cell95))) \/ ((((cell1) = (cell86)) /\ ((cell100) = (cell96))) \/ ((((cell1) = (cell87)) /\ ((cell100) = (cell97))) \/ ((((cell1) = (cell88)) /\ ((cell100) = (cell98))) \/ ((((cell1) = (cell89)) /\ ((cell100) = (cell99))) \/ (((cell1) = (cell90)) /\ ((cell100) = (cell100)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ((cell90) != (cell1)) ((cell80) != (cell1)) ((cell70) != (cell1)) ((cell60) != (cell1)) ((cell50) != (cell1)) ((cell40) != (cell1)) ((cell30) != (cell1)) ((cell20) != (cell1)) ((cell10) != (cell1)) ((cell11) != (cell100)) ((cell99) != (cell1)) ((cell98) != (cell1)) ((cell97) != (cell1)) ((cell96) != (cell1)) ((cell95) != (cell1)) ((cell94) != (cell1)) ((cell93) != (cell1)) ((cell92) != (cell1)) ((cell91) != (cell1)) ((cell89) != (cell1)) ((cell88) != (cell1)) ((cell87) != (cell1)) ((cell86) != (cell1)) ((cell85) != (cell1)) ((cell84) != (cell1)) ((cell83) != (cell1)) ((cell82) != (cell1)) ((cell81) != (cell1)) ((cell79) != (cell1)) ((cell78) != (cell1)) ((cell77) != (cell1)) ((cell76) != (cell1)) ((cell75) != (cell1)) ((cell74) != (cell1)) ((cell73) != (cell1)) ((cell72) != (cell1)) ((cell71) != (cell1)) ((cell69) != (cell1)) ((cell68) != (cell1)) ((cell67) != (cell1)) ((cell66) != (cell1)) ((cell65) != (cell1)) ((cell64) != (cell1)) ((cell63) != (cell1)) ((cell62) != (cell1)) ((cell61) != (cell1)) ((cell59) != (cell1)) ((cell58) != (cell1)) ((cell57) != (cell1)) ((cell56) != (cell1)) ((cell55) != (cell1)) ((cell54) != (cell1)) ((cell53) != (cell1)) ((cell52) != (cell1)) ((cell51) != (cell1)) ((cell49) != (cell1)) ((cell48) != (cell1)) ((cell47) != (cell1)) ((cell46) != (cell1)) ((cell45) != (cell1)) ((cell44) != (cell1)) ((cell43) != (cell1)) ((cell42) != (cell1)) ((cell41) != (cell1)) ((cell39) != (cell1)) ((cell38) != (cell1)) ((cell37) != (cell1)) ((cell36) != (cell1)) ((cell35) != (cell1)) ((cell34) != (cell1)) ((cell33) != (cell1)) ((cell32) != (cell1)) ((cell31) != (cell1)) ((cell29) != (cell1)) ((cell28) != (cell1)) ((cell27) != (cell1)) ((cell26) != (cell1)) ((cell25) != (cell1)) ((cell24) != (cell1)) ((cell23) != (cell1)) ((cell22) != (cell1)) ((cell21) != (cell1)) ((cell19) != (cell1)) ((cell18) != (cell1)) ((cell17) != (cell1)) ((cell16) != (cell1)) ((cell15) != (cell1)) ((cell14) != (cell1)) ((cell13) != (cell1)) ((cell12) != (cell1)) ((cell11) != (cell1)) ((cell9) != (cell1)) ((cell8) != (cell1)) ((cell7) != (cell1)) ((cell6) != (cell1)) ((cell5) != (cell1)) ((cell4) != (cell1)) ((cell3) != (cell1)) ((cell2) != (cell1)) ((cell2) != (cell100)) ### DisjTree 2 4 6 8 10 12 14 16 18 20 22 24 26 28 30 32 34 36 38 40 42 44 46 48 50 52 54 56 58 60 62 64 66 68 70 72 74 76 78 80 82 84 86 88 90 92 94 96 98 100 102 104 106 108 110 112 114 116 118 120 122 124 126 128 130 132 134 136 138 140 142 144 146 148 150 152 154 156 158 160 162 164 166 168 170 172 174 176 178 180 182 184 186 188 190 192 194 196 198 200 202 204 206 208 210 212 214 216 218 220 222 224 226 228 230 232 234 236 238 240 242 244 246 248 250 252 254 256 258 260 262 264 266 268 270 272 274 276 278 280 282 284 286 288 290 292 294 296 298 300 302 304 306 308 310 312 314 316 318 320 322 324 326 328 330 332 334 336 338 340 342 344 346 348 350 352 354 356 358 360 % 2.88/3.07 362. (edge (cell1) (cell100)) ((cell2) != (cell100)) ((cell2) != (cell1)) ((cell3) != (cell1)) ((cell4) != (cell1)) ((cell5) != (cell1)) ((cell6) != (cell1)) ((cell7) != (cell1)) ((cell8) != (cell1)) ((cell9) != (cell1)) ((cell11) != (cell1)) ((cell12) != (cell1)) ((cell13) != (cell1)) ((cell14) != (cell1)) ((cell15) != (cell1)) ((cell16) != (cell1)) ((cell17) != (cell1)) ((cell18) != (cell1)) ((cell19) != (cell1)) ((cell21) != (cell1)) ((cell22) != (cell1)) ((cell23) != (cell1)) ((cell24) != (cell1)) ((cell25) != (cell1)) ((cell26) != (cell1)) ((cell27) != (cell1)) ((cell28) != (cell1)) ((cell29) != (cell1)) ((cell31) != (cell1)) ((cell32) != (cell1)) ((cell33) != (cell1)) ((cell34) != (cell1)) ((cell35) != (cell1)) ((cell36) != (cell1)) ((cell37) != (cell1)) ((cell38) != (cell1)) ((cell39) != (cell1)) ((cell41) != (cell1)) ((cell42) != (cell1)) ((cell43) != (cell1)) ((cell44) != (cell1)) ((cell45) != (cell1)) ((cell46) != (cell1)) ((cell47) != (cell1)) ((cell48) != (cell1)) ((cell49) != (cell1)) ((cell51) != (cell1)) ((cell52) != (cell1)) ((cell53) != (cell1)) ((cell54) != (cell1)) ((cell55) != (cell1)) ((cell56) != (cell1)) ((cell57) != (cell1)) ((cell58) != (cell1)) ((cell59) != (cell1)) ((cell61) != (cell1)) ((cell62) != (cell1)) ((cell63) != (cell1)) ((cell64) != (cell1)) ((cell65) != (cell1)) ((cell66) != (cell1)) ((cell67) != (cell1)) ((cell68) != (cell1)) ((cell69) != (cell1)) ((cell71) != (cell1)) ((cell72) != (cell1)) ((cell73) != (cell1)) ((cell74) != (cell1)) ((cell75) != (cell1)) ((cell76) != (cell1)) ((cell77) != (cell1)) ((cell78) != (cell1)) ((cell79) != (cell1)) ((cell81) != (cell1)) ((cell82) != (cell1)) ((cell83) != (cell1)) ((cell84) != (cell1)) ((cell85) != (cell1)) ((cell86) != (cell1)) ((cell87) != (cell1)) ((cell88) != (cell1)) ((cell89) != (cell1)) ((cell91) != (cell1)) ((cell92) != (cell1)) ((cell93) != (cell1)) ((cell94) != (cell1)) ((cell95) != (cell1)) ((cell96) != (cell1)) ((cell97) != (cell1)) ((cell98) != (cell1)) ((cell99) != (cell1)) ((cell11) != (cell100)) ((cell10) != (cell1)) ((cell20) != (cell1)) ((cell30) != (cell1)) ((cell40) != (cell1)) ((cell50) != (cell1)) ((cell60) != (cell1)) ((cell70) != (cell1)) ((cell80) != (cell1)) ((cell90) != (cell1)) ### Definition-Pseudo(edge) 361 % 2.88/3.07 363. ((cell1) != (cell100)) ((cell100) = (cell1)) ### Sym(=) % 2.88/3.07 364. (((cell100) = (cell1)) /\ ((cell1) = (cell2))) ((cell1) != (cell100)) ### And 363 % 2.88/3.07 365. ((cell2) != (cell100)) ((cell100) = (cell2)) ### Sym(=) % 2.88/3.07 366. (((cell100) = (cell2)) /\ ((cell1) = (cell3))) ((cell2) != (cell100)) ### And 365 % 2.88/3.07 367. ((cell3) != (cell100)) ((cell100) = (cell3)) ### Sym(=) % 2.88/3.07 368. (((cell100) = (cell3)) /\ ((cell1) = (cell4))) ((cell3) != (cell100)) ### And 367 % 2.88/3.07 369. ((cell4) != (cell100)) ((cell100) = (cell4)) ### Sym(=) % 2.88/3.07 370. (((cell100) = (cell4)) /\ ((cell1) = (cell5))) ((cell4) != (cell100)) ### And 369 % 2.88/3.07 371. ((cell5) != (cell100)) ((cell100) = (cell5)) ### Sym(=) % 2.88/3.07 372. (((cell100) = (cell5)) /\ ((cell1) = (cell6))) ((cell5) != (cell100)) ### And 371 % 2.88/3.07 373. ((cell6) != (cell100)) ((cell100) = (cell6)) ### Sym(=) % 2.88/3.07 374. (((cell100) = (cell6)) /\ ((cell1) = (cell7))) ((cell6) != (cell100)) ### And 373 % 2.88/3.07 375. ((cell7) != (cell100)) ((cell100) = (cell7)) ### Sym(=) % 2.88/3.07 376. (((cell100) = (cell7)) /\ ((cell1) = (cell8))) ((cell7) != (cell100)) ### And 375 % 2.88/3.07 377. ((cell8) != (cell100)) ((cell100) = (cell8)) ### Sym(=) % 2.88/3.07 378. (((cell100) = (cell8)) /\ ((cell1) = (cell9))) ((cell8) != (cell100)) ### And 377 % 2.88/3.07 379. ((cell9) != (cell100)) ((cell100) = (cell9)) ### Sym(=) % 2.88/3.07 380. (((cell100) = (cell9)) /\ ((cell1) = (cell10))) ((cell9) != (cell100)) ### And 379 % 2.88/3.07 381. ((cell11) != (cell100)) ((cell100) = (cell11)) ### Sym(=) % 2.88/3.07 382. (((cell100) = (cell11)) /\ ((cell1) = (cell12))) ((cell11) != (cell100)) ### And 381 % 2.88/3.07 383. ((cell12) != (cell100)) ((cell100) = (cell12)) ### Sym(=) % 2.88/3.07 384. (((cell100) = (cell12)) /\ ((cell1) = (cell13))) ((cell12) != (cell100)) ### And 383 % 2.88/3.07 385. ((cell13) != (cell100)) ((cell100) = (cell13)) ### Sym(=) % 2.88/3.07 386. (((cell100) = (cell13)) /\ ((cell1) = (cell14))) ((cell13) != (cell100)) ### And 385 % 2.88/3.07 387. ((cell14) != (cell100)) ((cell100) = (cell14)) ### Sym(=) % 2.88/3.07 388. (((cell100) = (cell14)) /\ ((cell1) = (cell15))) ((cell14) != (cell100)) ### And 387 % 2.88/3.07 389. ((cell15) != (cell100)) ((cell100) = (cell15)) ### Sym(=) % 2.88/3.07 390. (((cell100) = (cell15)) /\ ((cell1) = (cell16))) ((cell15) != (cell100)) ### And 389 % 2.88/3.07 391. ((cell16) != (cell100)) ((cell100) = (cell16)) ### Sym(=) % 2.88/3.07 392. (((cell100) = (cell16)) /\ ((cell1) = (cell17))) ((cell16) != (cell100)) ### And 391 % 2.88/3.07 393. ((cell17) != (cell100)) ((cell100) = (cell17)) ### Sym(=) % 2.88/3.07 394. (((cell100) = (cell17)) /\ ((cell1) = (cell18))) ((cell17) != (cell100)) ### And 393 % 2.88/3.07 395. ((cell18) != (cell100)) ((cell100) = (cell18)) ### Sym(=) % 2.88/3.07 396. (((cell100) = (cell18)) /\ ((cell1) = (cell19))) ((cell18) != (cell100)) ### And 395 % 2.88/3.07 397. ((cell19) != (cell100)) ((cell100) = (cell19)) ### Sym(=) % 2.88/3.07 398. (((cell100) = (cell19)) /\ ((cell1) = (cell20))) ((cell19) != (cell100)) ### And 397 % 2.88/3.07 399. ((cell21) != (cell100)) ((cell100) = (cell21)) ### Sym(=) % 2.88/3.07 400. (((cell100) = (cell21)) /\ ((cell1) = (cell22))) ((cell21) != (cell100)) ### And 399 % 2.88/3.07 401. ((cell22) != (cell100)) ((cell100) = (cell22)) ### Sym(=) % 2.88/3.07 402. (((cell100) = (cell22)) /\ ((cell1) = (cell23))) ((cell22) != (cell100)) ### And 401 % 2.88/3.07 403. ((cell23) != (cell100)) ((cell100) = (cell23)) ### Sym(=) % 2.88/3.07 404. (((cell100) = (cell23)) /\ ((cell1) = (cell24))) ((cell23) != (cell100)) ### And 403 % 2.88/3.07 405. ((cell24) != (cell100)) ((cell100) = (cell24)) ### Sym(=) % 2.88/3.07 406. (((cell100) = (cell24)) /\ ((cell1) = (cell25))) ((cell24) != (cell100)) ### And 405 % 2.88/3.07 407. ((cell25) != (cell100)) ((cell100) = (cell25)) ### Sym(=) % 2.88/3.07 408. (((cell100) = (cell25)) /\ ((cell1) = (cell26))) ((cell25) != (cell100)) ### And 407 % 2.88/3.07 409. ((cell26) != (cell100)) ((cell100) = (cell26)) ### Sym(=) % 2.88/3.07 410. (((cell100) = (cell26)) /\ ((cell1) = (cell27))) ((cell26) != (cell100)) ### And 409 % 2.88/3.07 411. ((cell27) != (cell100)) ((cell100) = (cell27)) ### Sym(=) % 2.88/3.07 412. (((cell100) = (cell27)) /\ ((cell1) = (cell28))) ((cell27) != (cell100)) ### And 411 % 2.88/3.07 413. ((cell28) != (cell100)) ((cell100) = (cell28)) ### Sym(=) % 2.88/3.07 414. (((cell100) = (cell28)) /\ ((cell1) = (cell29))) ((cell28) != (cell100)) ### And 413 % 2.88/3.07 415. ((cell29) != (cell100)) ((cell100) = (cell29)) ### Sym(=) % 2.88/3.07 416. (((cell100) = (cell29)) /\ ((cell1) = (cell30))) ((cell29) != (cell100)) ### And 415 % 2.88/3.07 417. ((cell31) != (cell100)) ((cell100) = (cell31)) ### Sym(=) % 2.88/3.07 418. (((cell100) = (cell31)) /\ ((cell1) = (cell32))) ((cell31) != (cell100)) ### And 417 % 2.88/3.07 419. ((cell32) != (cell100)) ((cell100) = (cell32)) ### Sym(=) % 2.88/3.07 420. (((cell100) = (cell32)) /\ ((cell1) = (cell33))) ((cell32) != (cell100)) ### And 419 % 2.88/3.07 421. ((cell33) != (cell100)) ((cell100) = (cell33)) ### Sym(=) % 2.88/3.07 422. (((cell100) = (cell33)) /\ ((cell1) = (cell34))) ((cell33) != (cell100)) ### And 421 % 2.88/3.07 423. ((cell34) != (cell100)) ((cell100) = (cell34)) ### Sym(=) % 2.88/3.07 424. (((cell100) = (cell34)) /\ ((cell1) = (cell35))) ((cell34) != (cell100)) ### And 423 % 2.88/3.07 425. ((cell35) != (cell100)) ((cell100) = (cell35)) ### Sym(=) % 2.88/3.07 426. (((cell100) = (cell35)) /\ ((cell1) = (cell36))) ((cell35) != (cell100)) ### And 425 % 2.88/3.07 427. ((cell36) != (cell100)) ((cell100) = (cell36)) ### Sym(=) % 2.88/3.07 428. (((cell100) = (cell36)) /\ ((cell1) = (cell37))) ((cell36) != (cell100)) ### And 427 % 2.88/3.07 429. ((cell37) != (cell100)) ((cell100) = (cell37)) ### Sym(=) % 2.88/3.07 430. (((cell100) = (cell37)) /\ ((cell1) = (cell38))) ((cell37) != (cell100)) ### And 429 % 2.88/3.07 431. ((cell38) != (cell100)) ((cell100) = (cell38)) ### Sym(=) % 2.88/3.07 432. (((cell100) = (cell38)) /\ ((cell1) = (cell39))) ((cell38) != (cell100)) ### And 431 % 2.88/3.07 433. ((cell39) != (cell100)) ((cell100) = (cell39)) ### Sym(=) % 2.88/3.07 434. (((cell100) = (cell39)) /\ ((cell1) = (cell40))) ((cell39) != (cell100)) ### And 433 % 2.88/3.07 435. ((cell41) != (cell100)) ((cell100) = (cell41)) ### Sym(=) % 2.88/3.07 436. (((cell100) = (cell41)) /\ ((cell1) = (cell42))) ((cell41) != (cell100)) ### And 435 % 2.88/3.07 437. ((cell42) != (cell100)) ((cell100) = (cell42)) ### Sym(=) % 2.88/3.07 438. (((cell100) = (cell42)) /\ ((cell1) = (cell43))) ((cell42) != (cell100)) ### And 437 % 2.88/3.07 439. ((cell43) != (cell100)) ((cell100) = (cell43)) ### Sym(=) % 2.88/3.07 440. (((cell100) = (cell43)) /\ ((cell1) = (cell44))) ((cell43) != (cell100)) ### And 439 % 2.88/3.07 441. ((cell44) != (cell100)) ((cell100) = (cell44)) ### Sym(=) % 2.88/3.07 442. (((cell100) = (cell44)) /\ ((cell1) = (cell45))) ((cell44) != (cell100)) ### And 441 % 2.88/3.07 443. ((cell45) != (cell100)) ((cell100) = (cell45)) ### Sym(=) % 2.88/3.07 444. (((cell100) = (cell45)) /\ ((cell1) = (cell46))) ((cell45) != (cell100)) ### And 443 % 2.88/3.07 445. ((cell46) != (cell100)) ((cell100) = (cell46)) ### Sym(=) % 2.88/3.07 446. (((cell100) = (cell46)) /\ ((cell1) = (cell47))) ((cell46) != (cell100)) ### And 445 % 2.88/3.07 447. ((cell47) != (cell100)) ((cell100) = (cell47)) ### Sym(=) % 2.88/3.07 448. (((cell100) = (cell47)) /\ ((cell1) = (cell48))) ((cell47) != (cell100)) ### And 447 % 2.88/3.07 449. ((cell48) != (cell100)) ((cell100) = (cell48)) ### Sym(=) % 2.88/3.07 450. (((cell100) = (cell48)) /\ ((cell1) = (cell49))) ((cell48) != (cell100)) ### And 449 % 2.88/3.07 451. ((cell49) != (cell100)) ((cell100) = (cell49)) ### Sym(=) % 2.88/3.07 452. (((cell100) = (cell49)) /\ ((cell1) = (cell50))) ((cell49) != (cell100)) ### And 451 % 2.88/3.07 453. ((cell51) != (cell100)) ((cell100) = (cell51)) ### Sym(=) % 2.88/3.07 454. (((cell100) = (cell51)) /\ ((cell1) = (cell52))) ((cell51) != (cell100)) ### And 453 % 2.88/3.07 455. ((cell52) != (cell100)) ((cell100) = (cell52)) ### Sym(=) % 2.88/3.07 456. (((cell100) = (cell52)) /\ ((cell1) = (cell53))) ((cell52) != (cell100)) ### And 455 % 2.88/3.07 457. ((cell53) != (cell100)) ((cell100) = (cell53)) ### Sym(=) % 2.88/3.07 458. (((cell100) = (cell53)) /\ ((cell1) = (cell54))) ((cell53) != (cell100)) ### And 457 % 2.88/3.07 459. ((cell54) != (cell100)) ((cell100) = (cell54)) ### Sym(=) % 2.88/3.07 460. (((cell100) = (cell54)) /\ ((cell1) = (cell55))) ((cell54) != (cell100)) ### And 459 % 2.88/3.07 461. ((cell55) != (cell100)) ((cell100) = (cell55)) ### Sym(=) % 2.88/3.07 462. (((cell100) = (cell55)) /\ ((cell1) = (cell56))) ((cell55) != (cell100)) ### And 461 % 2.88/3.07 463. ((cell56) != (cell100)) ((cell100) = (cell56)) ### Sym(=) % 2.88/3.07 464. (((cell100) = (cell56)) /\ ((cell1) = (cell57))) ((cell56) != (cell100)) ### And 463 % 2.88/3.07 465. ((cell57) != (cell100)) ((cell100) = (cell57)) ### Sym(=) % 2.88/3.07 466. (((cell100) = (cell57)) /\ ((cell1) = (cell58))) ((cell57) != (cell100)) ### And 465 % 2.88/3.07 467. ((cell58) != (cell100)) ((cell100) = (cell58)) ### Sym(=) % 2.88/3.07 468. (((cell100) = (cell58)) /\ ((cell1) = (cell59))) ((cell58) != (cell100)) ### And 467 % 2.88/3.07 469. ((cell59) != (cell100)) ((cell100) = (cell59)) ### Sym(=) % 2.88/3.07 470. (((cell100) = (cell59)) /\ ((cell1) = (cell60))) ((cell59) != (cell100)) ### And 469 % 2.88/3.07 471. ((cell61) != (cell100)) ((cell100) = (cell61)) ### Sym(=) % 2.88/3.07 472. (((cell100) = (cell61)) /\ ((cell1) = (cell62))) ((cell61) != (cell100)) ### And 471 % 2.88/3.07 473. ((cell62) != (cell100)) ((cell100) = (cell62)) ### Sym(=) % 2.88/3.07 474. (((cell100) = (cell62)) /\ ((cell1) = (cell63))) ((cell62) != (cell100)) ### And 473 % 2.88/3.07 475. ((cell63) != (cell100)) ((cell100) = (cell63)) ### Sym(=) % 2.88/3.07 476. (((cell100) = (cell63)) /\ ((cell1) = (cell64))) ((cell63) != (cell100)) ### And 475 % 2.88/3.07 477. ((cell64) != (cell100)) ((cell100) = (cell64)) ### Sym(=) % 2.88/3.07 478. (((cell100) = (cell64)) /\ ((cell1) = (cell65))) ((cell64) != (cell100)) ### And 477 % 2.88/3.07 479. ((cell65) != (cell100)) ((cell100) = (cell65)) ### Sym(=) % 2.88/3.07 480. (((cell100) = (cell65)) /\ ((cell1) = (cell66))) ((cell65) != (cell100)) ### And 479 % 2.88/3.07 481. ((cell66) != (cell100)) ((cell100) = (cell66)) ### Sym(=) % 2.88/3.07 482. (((cell100) = (cell66)) /\ ((cell1) = (cell67))) ((cell66) != (cell100)) ### And 481 % 2.88/3.07 483. ((cell67) != (cell100)) ((cell100) = (cell67)) ### Sym(=) % 2.88/3.07 484. (((cell100) = (cell67)) /\ ((cell1) = (cell68))) ((cell67) != (cell100)) ### And 483 % 2.88/3.07 485. ((cell68) != (cell100)) ((cell100) = (cell68)) ### Sym(=) % 2.88/3.07 486. (((cell100) = (cell68)) /\ ((cell1) = (cell69))) ((cell68) != (cell100)) ### And 485 % 2.88/3.07 487. ((cell69) != (cell100)) ((cell100) = (cell69)) ### Sym(=) % 2.88/3.07 488. (((cell100) = (cell69)) /\ ((cell1) = (cell70))) ((cell69) != (cell100)) ### And 487 % 2.88/3.07 489. ((cell71) != (cell100)) ((cell100) = (cell71)) ### Sym(=) % 2.88/3.07 490. (((cell100) = (cell71)) /\ ((cell1) = (cell72))) ((cell71) != (cell100)) ### And 489 % 2.88/3.07 491. ((cell72) != (cell100)) ((cell100) = (cell72)) ### Sym(=) % 2.88/3.07 492. (((cell100) = (cell72)) /\ ((cell1) = (cell73))) ((cell72) != (cell100)) ### And 491 % 2.88/3.07 493. ((cell73) != (cell100)) ((cell100) = (cell73)) ### Sym(=) % 2.88/3.07 494. (((cell100) = (cell73)) /\ ((cell1) = (cell74))) ((cell73) != (cell100)) ### And 493 % 2.88/3.07 495. ((cell74) != (cell100)) ((cell100) = (cell74)) ### Sym(=) % 2.88/3.07 496. (((cell100) = (cell74)) /\ ((cell1) = (cell75))) ((cell74) != (cell100)) ### And 495 % 2.88/3.07 497. ((cell75) != (cell100)) ((cell100) = (cell75)) ### Sym(=) % 2.88/3.07 498. (((cell100) = (cell75)) /\ ((cell1) = (cell76))) ((cell75) != (cell100)) ### And 497 % 2.88/3.07 499. ((cell76) != (cell100)) ((cell100) = (cell76)) ### Sym(=) % 2.88/3.07 500. (((cell100) = (cell76)) /\ ((cell1) = (cell77))) ((cell76) != (cell100)) ### And 499 % 2.88/3.07 501. ((cell77) != (cell100)) ((cell100) = (cell77)) ### Sym(=) % 2.88/3.07 502. (((cell100) = (cell77)) /\ ((cell1) = (cell78))) ((cell77) != (cell100)) ### And 501 % 2.88/3.07 503. ((cell78) != (cell100)) ((cell100) = (cell78)) ### Sym(=) % 2.88/3.07 504. (((cell100) = (cell78)) /\ ((cell1) = (cell79))) ((cell78) != (cell100)) ### And 503 % 2.88/3.07 505. ((cell79) != (cell100)) ((cell100) = (cell79)) ### Sym(=) % 2.88/3.07 506. (((cell100) = (cell79)) /\ ((cell1) = (cell80))) ((cell79) != (cell100)) ### And 505 % 2.88/3.07 507. ((cell81) != (cell100)) ((cell100) = (cell81)) ### Sym(=) % 2.88/3.07 508. (((cell100) = (cell81)) /\ ((cell1) = (cell82))) ((cell81) != (cell100)) ### And 507 % 2.88/3.07 509. ((cell82) != (cell100)) ((cell100) = (cell82)) ### Sym(=) % 2.88/3.07 510. (((cell100) = (cell82)) /\ ((cell1) = (cell83))) ((cell82) != (cell100)) ### And 509 % 2.88/3.07 511. ((cell83) != (cell100)) ((cell100) = (cell83)) ### Sym(=) % 2.88/3.07 512. (((cell100) = (cell83)) /\ ((cell1) = (cell84))) ((cell83) != (cell100)) ### And 511 % 2.88/3.07 513. ((cell84) != (cell100)) ((cell100) = (cell84)) ### Sym(=) % 2.88/3.07 514. (((cell100) = (cell84)) /\ ((cell1) = (cell85))) ((cell84) != (cell100)) ### And 513 % 2.88/3.07 515. ((cell85) != (cell100)) ((cell100) = (cell85)) ### Sym(=) % 2.88/3.07 516. (((cell100) = (cell85)) /\ ((cell1) = (cell86))) ((cell85) != (cell100)) ### And 515 % 2.88/3.07 517. ((cell86) != (cell100)) ((cell100) = (cell86)) ### Sym(=) % 2.88/3.07 518. (((cell100) = (cell86)) /\ ((cell1) = (cell87))) ((cell86) != (cell100)) ### And 517 % 2.88/3.07 519. ((cell87) != (cell100)) ((cell100) = (cell87)) ### Sym(=) % 2.88/3.07 520. (((cell100) = (cell87)) /\ ((cell1) = (cell88))) ((cell87) != (cell100)) ### And 519 % 2.88/3.07 521. ((cell88) != (cell100)) ((cell100) = (cell88)) ### Sym(=) % 2.88/3.07 522. (((cell100) = (cell88)) /\ ((cell1) = (cell89))) ((cell88) != (cell100)) ### And 521 % 2.88/3.07 523. ((cell89) != (cell100)) ((cell100) = (cell89)) ### Sym(=) % 2.88/3.07 524. (((cell100) = (cell89)) /\ ((cell1) = (cell90))) ((cell89) != (cell100)) ### And 523 % 2.88/3.07 525. ((cell91) != (cell100)) ((cell100) = (cell91)) ### Sym(=) % 2.88/3.07 526. (((cell100) = (cell91)) /\ ((cell1) = (cell92))) ((cell91) != (cell100)) ### And 525 % 2.88/3.07 527. ((cell92) != (cell100)) ((cell100) = (cell92)) ### Sym(=) % 2.88/3.07 528. (((cell100) = (cell92)) /\ ((cell1) = (cell93))) ((cell92) != (cell100)) ### And 527 % 2.88/3.07 529. ((cell93) != (cell100)) ((cell100) = (cell93)) ### Sym(=) % 2.88/3.07 530. (((cell100) = (cell93)) /\ ((cell1) = (cell94))) ((cell93) != (cell100)) ### And 529 % 2.88/3.07 531. ((cell94) != (cell100)) ((cell100) = (cell94)) ### Sym(=) % 2.88/3.07 532. (((cell100) = (cell94)) /\ ((cell1) = (cell95))) ((cell94) != (cell100)) ### And 531 % 2.88/3.07 533. ((cell95) != (cell100)) ((cell100) = (cell95)) ### Sym(=) % 2.88/3.07 534. (((cell100) = (cell95)) /\ ((cell1) = (cell96))) ((cell95) != (cell100)) ### And 533 % 2.88/3.07 535. ((cell96) != (cell100)) ((cell100) = (cell96)) ### Sym(=) % 2.88/3.07 536. (((cell100) = (cell96)) /\ ((cell1) = (cell97))) ((cell96) != (cell100)) ### And 535 % 2.88/3.07 537. ((cell97) != (cell100)) ((cell100) = (cell97)) ### Sym(=) % 2.88/3.07 538. (((cell100) = (cell97)) /\ ((cell1) = (cell98))) ((cell97) != (cell100)) ### And 537 % 2.88/3.07 539. ((cell98) != (cell100)) ((cell100) = (cell98)) ### Sym(=) % 2.88/3.07 540. (((cell100) = (cell98)) /\ ((cell1) = (cell99))) ((cell98) != (cell100)) ### And 539 % 2.88/3.07 541. ((cell99) != (cell100)) ((cell100) = (cell99)) ### Sym(=) % 2.88/3.07 542. (((cell100) = (cell99)) /\ ((cell1) = (cell100))) ((cell99) != (cell100)) ### And 541 % 2.88/3.07 543. ((cell1) != (cell100)) ((cell100) = (cell1)) ### Sym(=) % 2.88/3.07 544. (((cell100) = (cell1)) /\ ((cell1) = (cell11))) ((cell1) != (cell100)) ### And 543 % 2.88/3.07 545. ((cell2) != (cell100)) ((cell100) = (cell2)) ### Sym(=) % 2.88/3.07 546. (((cell100) = (cell2)) /\ ((cell1) = (cell12))) ((cell2) != (cell100)) ### And 545 % 2.88/3.07 547. ((cell3) != (cell100)) ((cell100) = (cell3)) ### Sym(=) % 2.88/3.07 548. (((cell100) = (cell3)) /\ ((cell1) = (cell13))) ((cell3) != (cell100)) ### And 547 % 2.88/3.07 549. ((cell4) != (cell100)) ((cell100) = (cell4)) ### Sym(=) % 2.88/3.07 550. (((cell100) = (cell4)) /\ ((cell1) = (cell14))) ((cell4) != (cell100)) ### And 549 % 2.88/3.07 551. ((cell5) != (cell100)) ((cell100) = (cell5)) ### Sym(=) % 2.88/3.07 552. (((cell100) = (cell5)) /\ ((cell1) = (cell15))) ((cell5) != (cell100)) ### And 551 % 2.88/3.07 553. ((cell6) != (cell100)) ((cell100) = (cell6)) ### Sym(=) % 2.88/3.07 554. (((cell100) = (cell6)) /\ ((cell1) = (cell16))) ((cell6) != (cell100)) ### And 553 % 2.88/3.07 555. ((cell7) != (cell100)) ((cell100) = (cell7)) ### Sym(=) % 2.88/3.07 556. (((cell100) = (cell7)) /\ ((cell1) = (cell17))) ((cell7) != (cell100)) ### And 555 % 2.88/3.07 557. ((cell8) != (cell100)) ((cell100) = (cell8)) ### Sym(=) % 2.88/3.07 558. (((cell100) = (cell8)) /\ ((cell1) = (cell18))) ((cell8) != (cell100)) ### And 557 % 2.88/3.07 559. ((cell9) != (cell100)) ((cell100) = (cell9)) ### Sym(=) % 2.88/3.07 560. (((cell100) = (cell9)) /\ ((cell1) = (cell19))) ((cell9) != (cell100)) ### And 559 % 2.88/3.07 561. ((cell10) != (cell100)) ((cell100) = (cell10)) ### Sym(=) % 2.88/3.07 562. (((cell100) = (cell10)) /\ ((cell1) = (cell20))) ((cell10) != (cell100)) ### And 561 % 2.88/3.07 563. ((cell11) != (cell100)) ((cell100) = (cell11)) ### Sym(=) % 2.88/3.07 564. (((cell100) = (cell11)) /\ ((cell1) = (cell21))) ((cell11) != (cell100)) ### And 563 % 2.88/3.07 565. ((cell12) != (cell100)) ((cell100) = (cell12)) ### Sym(=) % 2.88/3.07 566. (((cell100) = (cell12)) /\ ((cell1) = (cell22))) ((cell12) != (cell100)) ### And 565 % 2.88/3.07 567. ((cell13) != (cell100)) ((cell100) = (cell13)) ### Sym(=) % 2.88/3.07 568. (((cell100) = (cell13)) /\ ((cell1) = (cell23))) ((cell13) != (cell100)) ### And 567 % 2.88/3.07 569. ((cell14) != (cell100)) ((cell100) = (cell14)) ### Sym(=) % 2.88/3.07 570. (((cell100) = (cell14)) /\ ((cell1) = (cell24))) ((cell14) != (cell100)) ### And 569 % 2.88/3.07 571. ((cell15) != (cell100)) ((cell100) = (cell15)) ### Sym(=) % 2.88/3.07 572. (((cell100) = (cell15)) /\ ((cell1) = (cell25))) ((cell15) != (cell100)) ### And 571 % 2.88/3.07 573. ((cell16) != (cell100)) ((cell100) = (cell16)) ### Sym(=) % 2.88/3.07 574. (((cell100) = (cell16)) /\ ((cell1) = (cell26))) ((cell16) != (cell100)) ### And 573 % 2.88/3.07 575. ((cell17) != (cell100)) ((cell100) = (cell17)) ### Sym(=) % 2.88/3.07 576. (((cell100) = (cell17)) /\ ((cell1) = (cell27))) ((cell17) != (cell100)) ### And 575 % 2.88/3.07 577. ((cell18) != (cell100)) ((cell100) = (cell18)) ### Sym(=) % 2.88/3.07 578. (((cell100) = (cell18)) /\ ((cell1) = (cell28))) ((cell18) != (cell100)) ### And 577 % 2.88/3.07 579. ((cell19) != (cell100)) ((cell100) = (cell19)) ### Sym(=) % 2.88/3.07 580. (((cell100) = (cell19)) /\ ((cell1) = (cell29))) ((cell19) != (cell100)) ### And 579 % 2.88/3.07 581. ((cell20) != (cell100)) ((cell100) = (cell20)) ### Sym(=) % 2.88/3.07 582. (((cell100) = (cell20)) /\ ((cell1) = (cell30))) ((cell20) != (cell100)) ### And 581 % 2.88/3.07 583. ((cell21) != (cell100)) ((cell100) = (cell21)) ### Sym(=) % 2.88/3.07 584. (((cell100) = (cell21)) /\ ((cell1) = (cell31))) ((cell21) != (cell100)) ### And 583 % 2.88/3.07 585. ((cell22) != (cell100)) ((cell100) = (cell22)) ### Sym(=) % 2.88/3.07 586. (((cell100) = (cell22)) /\ ((cell1) = (cell32))) ((cell22) != (cell100)) ### And 585 % 2.88/3.07 587. ((cell23) != (cell100)) ((cell100) = (cell23)) ### Sym(=) % 2.88/3.07 588. (((cell100) = (cell23)) /\ ((cell1) = (cell33))) ((cell23) != (cell100)) ### And 587 % 2.88/3.07 589. ((cell24) != (cell100)) ((cell100) = (cell24)) ### Sym(=) % 2.88/3.07 590. (((cell100) = (cell24)) /\ ((cell1) = (cell34))) ((cell24) != (cell100)) ### And 589 % 2.88/3.07 591. ((cell25) != (cell100)) ((cell100) = (cell25)) ### Sym(=) % 2.88/3.07 592. (((cell100) = (cell25)) /\ ((cell1) = (cell35))) ((cell25) != (cell100)) ### And 591 % 2.88/3.07 593. ((cell26) != (cell100)) ((cell100) = (cell26)) ### Sym(=) % 2.88/3.07 594. (((cell100) = (cell26)) /\ ((cell1) = (cell36))) ((cell26) != (cell100)) ### And 593 % 2.88/3.07 595. ((cell27) != (cell100)) ((cell100) = (cell27)) ### Sym(=) % 2.88/3.07 596. (((cell100) = (cell27)) /\ ((cell1) = (cell37))) ((cell27) != (cell100)) ### And 595 % 2.88/3.07 597. ((cell28) != (cell100)) ((cell100) = (cell28)) ### Sym(=) % 2.88/3.07 598. (((cell100) = (cell28)) /\ ((cell1) = (cell38))) ((cell28) != (cell100)) ### And 597 % 2.88/3.07 599. ((cell29) != (cell100)) ((cell100) = (cell29)) ### Sym(=) % 2.88/3.07 600. (((cell100) = (cell29)) /\ ((cell1) = (cell39))) ((cell29) != (cell100)) ### And 599 % 2.88/3.07 601. ((cell30) != (cell100)) ((cell100) = (cell30)) ### Sym(=) % 2.88/3.07 602. (((cell100) = (cell30)) /\ ((cell1) = (cell40))) ((cell30) != (cell100)) ### And 601 % 2.88/3.07 603. ((cell31) != (cell100)) ((cell100) = (cell31)) ### Sym(=) % 2.88/3.07 604. (((cell100) = (cell31)) /\ ((cell1) = (cell41))) ((cell31) != (cell100)) ### And 603 % 2.88/3.07 605. ((cell32) != (cell100)) ((cell100) = (cell32)) ### Sym(=) % 2.88/3.07 606. (((cell100) = (cell32)) /\ ((cell1) = (cell42))) ((cell32) != (cell100)) ### And 605 % 2.88/3.07 607. ((cell33) != (cell100)) ((cell100) = (cell33)) ### Sym(=) % 2.88/3.07 608. (((cell100) = (cell33)) /\ ((cell1) = (cell43))) ((cell33) != (cell100)) ### And 607 % 2.88/3.07 609. ((cell34) != (cell100)) ((cell100) = (cell34)) ### Sym(=) % 2.88/3.07 610. (((cell100) = (cell34)) /\ ((cell1) = (cell44))) ((cell34) != (cell100)) ### And 609 % 2.88/3.07 611. ((cell35) != (cell100)) ((cell100) = (cell35)) ### Sym(=) % 2.88/3.07 612. (((cell100) = (cell35)) /\ ((cell1) = (cell45))) ((cell35) != (cell100)) ### And 611 % 2.88/3.07 613. ((cell36) != (cell100)) ((cell100) = (cell36)) ### Sym(=) % 2.88/3.07 614. (((cell100) = (cell36)) /\ ((cell1) = (cell46))) ((cell36) != (cell100)) ### And 613 % 2.88/3.07 615. ((cell37) != (cell100)) ((cell100) = (cell37)) ### Sym(=) % 2.88/3.07 616. (((cell100) = (cell37)) /\ ((cell1) = (cell47))) ((cell37) != (cell100)) ### And 615 % 2.88/3.07 617. ((cell38) != (cell100)) ((cell100) = (cell38)) ### Sym(=) % 2.88/3.07 618. (((cell100) = (cell38)) /\ ((cell1) = (cell48))) ((cell38) != (cell100)) ### And 617 % 2.88/3.07 619. ((cell39) != (cell100)) ((cell100) = (cell39)) ### Sym(=) % 2.88/3.07 620. (((cell100) = (cell39)) /\ ((cell1) = (cell49))) ((cell39) != (cell100)) ### And 619 % 2.88/3.07 621. ((cell40) != (cell100)) ((cell100) = (cell40)) ### Sym(=) % 2.88/3.07 622. (((cell100) = (cell40)) /\ ((cell1) = (cell50))) ((cell40) != (cell100)) ### And 621 % 2.88/3.07 623. ((cell41) != (cell100)) ((cell100) = (cell41)) ### Sym(=) % 2.88/3.07 624. (((cell100) = (cell41)) /\ ((cell1) = (cell51))) ((cell41) != (cell100)) ### And 623 % 2.88/3.07 625. ((cell42) != (cell100)) ((cell100) = (cell42)) ### Sym(=) % 2.88/3.07 626. (((cell100) = (cell42)) /\ ((cell1) = (cell52))) ((cell42) != (cell100)) ### And 625 % 2.88/3.07 627. ((cell43) != (cell100)) ((cell100) = (cell43)) ### Sym(=) % 2.88/3.07 628. (((cell100) = (cell43)) /\ ((cell1) = (cell53))) ((cell43) != (cell100)) ### And 627 % 2.88/3.07 629. ((cell44) != (cell100)) ((cell100) = (cell44)) ### Sym(=) % 2.88/3.07 630. (((cell100) = (cell44)) /\ ((cell1) = (cell54))) ((cell44) != (cell100)) ### And 629 % 2.88/3.07 631. ((cell45) != (cell100)) ((cell100) = (cell45)) ### Sym(=) % 2.88/3.07 632. (((cell100) = (cell45)) /\ ((cell1) = (cell55))) ((cell45) != (cell100)) ### And 631 % 2.88/3.07 633. ((cell46) != (cell100)) ((cell100) = (cell46)) ### Sym(=) % 2.88/3.07 634. (((cell100) = (cell46)) /\ ((cell1) = (cell56))) ((cell46) != (cell100)) ### And 633 % 2.88/3.07 635. ((cell47) != (cell100)) ((cell100) = (cell47)) ### Sym(=) % 2.88/3.07 636. (((cell100) = (cell47)) /\ ((cell1) = (cell57))) ((cell47) != (cell100)) ### And 635 % 2.88/3.07 637. ((cell48) != (cell100)) ((cell100) = (cell48)) ### Sym(=) % 2.88/3.07 638. (((cell100) = (cell48)) /\ ((cell1) = (cell58))) ((cell48) != (cell100)) ### And 637 % 2.88/3.07 639. ((cell49) != (cell100)) ((cell100) = (cell49)) ### Sym(=) % 2.88/3.07 640. (((cell100) = (cell49)) /\ ((cell1) = (cell59))) ((cell49) != (cell100)) ### And 639 % 2.88/3.07 641. ((cell50) != (cell100)) ((cell100) = (cell50)) ### Sym(=) % 2.88/3.07 642. (((cell100) = (cell50)) /\ ((cell1) = (cell60))) ((cell50) != (cell100)) ### And 641 % 2.88/3.07 643. ((cell51) != (cell100)) ((cell100) = (cell51)) ### Sym(=) % 2.88/3.07 644. (((cell100) = (cell51)) /\ ((cell1) = (cell61))) ((cell51) != (cell100)) ### And 643 % 2.88/3.07 645. ((cell52) != (cell100)) ((cell100) = (cell52)) ### Sym(=) % 2.88/3.07 646. (((cell100) = (cell52)) /\ ((cell1) = (cell62))) ((cell52) != (cell100)) ### And 645 % 2.88/3.07 647. ((cell53) != (cell100)) ((cell100) = (cell53)) ### Sym(=) % 2.88/3.07 648. (((cell100) = (cell53)) /\ ((cell1) = (cell63))) ((cell53) != (cell100)) ### And 647 % 2.88/3.07 649. ((cell54) != (cell100)) ((cell100) = (cell54)) ### Sym(=) % 2.88/3.07 650. (((cell100) = (cell54)) /\ ((cell1) = (cell64))) ((cell54) != (cell100)) ### And 649 % 2.88/3.07 651. ((cell55) != (cell100)) ((cell100) = (cell55)) ### Sym(=) % 2.88/3.07 652. (((cell100) = (cell55)) /\ ((cell1) = (cell65))) ((cell55) != (cell100)) ### And 651 % 2.88/3.07 653. ((cell56) != (cell100)) ((cell100) = (cell56)) ### Sym(=) % 2.88/3.07 654. (((cell100) = (cell56)) /\ ((cell1) = (cell66))) ((cell56) != (cell100)) ### And 653 % 2.88/3.07 655. ((cell57) != (cell100)) ((cell100) = (cell57)) ### Sym(=) % 2.88/3.07 656. (((cell100) = (cell57)) /\ ((cell1) = (cell67))) ((cell57) != (cell100)) ### And 655 % 2.88/3.07 657. ((cell58) != (cell100)) ((cell100) = (cell58)) ### Sym(=) % 2.88/3.07 658. (((cell100) = (cell58)) /\ ((cell1) = (cell68))) ((cell58) != (cell100)) ### And 657 % 2.88/3.07 659. ((cell59) != (cell100)) ((cell100) = (cell59)) ### Sym(=) % 2.88/3.07 660. (((cell100) = (cell59)) /\ ((cell1) = (cell69))) ((cell59) != (cell100)) ### And 659 % 2.88/3.07 661. ((cell60) != (cell100)) ((cell100) = (cell60)) ### Sym(=) % 2.88/3.07 662. (((cell100) = (cell60)) /\ ((cell1) = (cell70))) ((cell60) != (cell100)) ### And 661 % 2.88/3.07 663. ((cell61) != (cell100)) ((cell100) = (cell61)) ### Sym(=) % 2.88/3.07 664. (((cell100) = (cell61)) /\ ((cell1) = (cell71))) ((cell61) != (cell100)) ### And 663 % 2.88/3.07 665. ((cell62) != (cell100)) ((cell100) = (cell62)) ### Sym(=) % 2.88/3.07 666. (((cell100) = (cell62)) /\ ((cell1) = (cell72))) ((cell62) != (cell100)) ### And 665 % 2.88/3.07 667. ((cell63) != (cell100)) ((cell100) = (cell63)) ### Sym(=) % 2.88/3.07 668. (((cell100) = (cell63)) /\ ((cell1) = (cell73))) ((cell63) != (cell100)) ### And 667 % 2.88/3.07 669. ((cell64) != (cell100)) ((cell100) = (cell64)) ### Sym(=) % 2.88/3.07 670. (((cell100) = (cell64)) /\ ((cell1) = (cell74))) ((cell64) != (cell100)) ### And 669 % 2.88/3.07 671. ((cell65) != (cell100)) ((cell100) = (cell65)) ### Sym(=) % 2.88/3.07 672. (((cell100) = (cell65)) /\ ((cell1) = (cell75))) ((cell65) != (cell100)) ### And 671 % 2.88/3.07 673. ((cell66) != (cell100)) ((cell100) = (cell66)) ### Sym(=) % 2.88/3.07 674. (((cell100) = (cell66)) /\ ((cell1) = (cell76))) ((cell66) != (cell100)) ### And 673 % 2.88/3.07 675. ((cell67) != (cell100)) ((cell100) = (cell67)) ### Sym(=) % 2.88/3.07 676. (((cell100) = (cell67)) /\ ((cell1) = (cell77))) ((cell67) != (cell100)) ### And 675 % 2.88/3.07 677. ((cell68) != (cell100)) ((cell100) = (cell68)) ### Sym(=) % 2.88/3.07 678. (((cell100) = (cell68)) /\ ((cell1) = (cell78))) ((cell68) != (cell100)) ### And 677 % 2.88/3.07 679. ((cell69) != (cell100)) ((cell100) = (cell69)) ### Sym(=) % 2.88/3.07 680. (((cell100) = (cell69)) /\ ((cell1) = (cell79))) ((cell69) != (cell100)) ### And 679 % 2.88/3.07 681. ((cell70) != (cell100)) ((cell100) = (cell70)) ### Sym(=) % 2.88/3.07 682. (((cell100) = (cell70)) /\ ((cell1) = (cell80))) ((cell70) != (cell100)) ### And 681 % 2.88/3.07 683. ((cell71) != (cell100)) ((cell100) = (cell71)) ### Sym(=) % 2.88/3.07 684. (((cell100) = (cell71)) /\ ((cell1) = (cell81))) ((cell71) != (cell100)) ### And 683 % 2.88/3.07 685. ((cell72) != (cell100)) ((cell100) = (cell72)) ### Sym(=) % 2.88/3.07 686. (((cell100) = (cell72)) /\ ((cell1) = (cell82))) ((cell72) != (cell100)) ### And 685 % 2.88/3.07 687. ((cell73) != (cell100)) ((cell100) = (cell73)) ### Sym(=) % 2.88/3.07 688. (((cell100) = (cell73)) /\ ((cell1) = (cell83))) ((cell73) != (cell100)) ### And 687 % 2.88/3.07 689. ((cell74) != (cell100)) ((cell100) = (cell74)) ### Sym(=) % 2.88/3.07 690. (((cell100) = (cell74)) /\ ((cell1) = (cell84))) ((cell74) != (cell100)) ### And 689 % 2.88/3.07 691. ((cell75) != (cell100)) ((cell100) = (cell75)) ### Sym(=) % 2.88/3.07 692. (((cell100) = (cell75)) /\ ((cell1) = (cell85))) ((cell75) != (cell100)) ### And 691 % 2.88/3.07 693. ((cell76) != (cell100)) ((cell100) = (cell76)) ### Sym(=) % 2.88/3.07 694. (((cell100) = (cell76)) /\ ((cell1) = (cell86))) ((cell76) != (cell100)) ### And 693 % 2.88/3.07 695. ((cell77) != (cell100)) ((cell100) = (cell77)) ### Sym(=) % 2.88/3.07 696. (((cell100) = (cell77)) /\ ((cell1) = (cell87))) ((cell77) != (cell100)) ### And 695 % 2.88/3.07 697. ((cell78) != (cell100)) ((cell100) = (cell78)) ### Sym(=) % 2.88/3.07 698. (((cell100) = (cell78)) /\ ((cell1) = (cell88))) ((cell78) != (cell100)) ### And 697 % 2.88/3.07 699. ((cell79) != (cell100)) ((cell100) = (cell79)) ### Sym(=) % 2.88/3.07 700. (((cell100) = (cell79)) /\ ((cell1) = (cell89))) ((cell79) != (cell100)) ### And 699 % 2.88/3.07 701. ((cell80) != (cell100)) ((cell100) = (cell80)) ### Sym(=) % 2.88/3.07 702. (((cell100) = (cell80)) /\ ((cell1) = (cell90))) ((cell80) != (cell100)) ### And 701 % 2.88/3.07 703. ((cell81) != (cell100)) ((cell100) = (cell81)) ### Sym(=) % 2.88/3.07 704. (((cell100) = (cell81)) /\ ((cell1) = (cell91))) ((cell81) != (cell100)) ### And 703 % 2.88/3.07 705. ((cell82) != (cell100)) ((cell100) = (cell82)) ### Sym(=) % 2.88/3.07 706. (((cell100) = (cell82)) /\ ((cell1) = (cell92))) ((cell82) != (cell100)) ### And 705 % 2.88/3.07 707. ((cell83) != (cell100)) ((cell100) = (cell83)) ### Sym(=) % 2.88/3.07 708. (((cell100) = (cell83)) /\ ((cell1) = (cell93))) ((cell83) != (cell100)) ### And 707 % 2.88/3.07 709. ((cell84) != (cell100)) ((cell100) = (cell84)) ### Sym(=) % 2.88/3.07 710. (((cell100) = (cell84)) /\ ((cell1) = (cell94))) ((cell84) != (cell100)) ### And 709 % 2.88/3.07 711. ((cell85) != (cell100)) ((cell100) = (cell85)) ### Sym(=) % 2.88/3.07 712. (((cell100) = (cell85)) /\ ((cell1) = (cell95))) ((cell85) != (cell100)) ### And 711 % 2.88/3.07 713. ((cell86) != (cell100)) ((cell100) = (cell86)) ### Sym(=) % 2.88/3.07 714. (((cell100) = (cell86)) /\ ((cell1) = (cell96))) ((cell86) != (cell100)) ### And 713 % 2.88/3.07 715. ((cell87) != (cell100)) ((cell100) = (cell87)) ### Sym(=) % 2.88/3.07 716. (((cell100) = (cell87)) /\ ((cell1) = (cell97))) ((cell87) != (cell100)) ### And 715 % 2.88/3.07 717. ((cell88) != (cell100)) ((cell100) = (cell88)) ### Sym(=) % 2.88/3.07 718. (((cell100) = (cell88)) /\ ((cell1) = (cell98))) ((cell88) != (cell100)) ### And 717 % 2.88/3.07 719. ((cell89) != (cell100)) ((cell100) = (cell89)) ### Sym(=) % 2.88/3.07 720. (((cell100) = (cell89)) /\ ((cell1) = (cell99))) ((cell89) != (cell100)) ### And 719 % 2.88/3.07 721. ((cell90) != (cell100)) ((cell100) = (cell90)) ### Sym(=) % 2.88/3.07 722. (((cell100) = (cell90)) /\ ((cell1) = (cell100))) ((cell90) != (cell100)) ### And 721 % 2.88/3.07 723. ((((cell100) = (cell1)) /\ ((cell1) = (cell2))) \/ ((((cell100) = (cell2)) /\ ((cell1) = (cell3))) \/ ((((cell100) = (cell3)) /\ ((cell1) = (cell4))) \/ ((((cell100) = (cell4)) /\ ((cell1) = (cell5))) \/ ((((cell100) = (cell5)) /\ ((cell1) = (cell6))) \/ ((((cell100) = (cell6)) /\ ((cell1) = (cell7))) \/ ((((cell100) = (cell7)) /\ ((cell1) = (cell8))) \/ ((((cell100) = (cell8)) /\ ((cell1) = (cell9))) \/ ((((cell100) = (cell9)) /\ ((cell1) = (cell10))) \/ ((((cell100) = (cell11)) /\ ((cell1) = (cell12))) \/ ((((cell100) = (cell12)) /\ ((cell1) = (cell13))) \/ ((((cell100) = (cell13)) /\ ((cell1) = (cell14))) \/ ((((cell100) = (cell14)) /\ ((cell1) = (cell15))) \/ ((((cell100) = (cell15)) /\ ((cell1) = (cell16))) \/ ((((cell100) = (cell16)) /\ ((cell1) = (cell17))) \/ ((((cell100) = (cell17)) /\ ((cell1) = (cell18))) \/ ((((cell100) = (cell18)) /\ ((cell1) = (cell19))) \/ ((((cell100) = (cell19)) /\ ((cell1) = (cell20))) \/ ((((cell100) = (cell21)) /\ ((cell1) = (cell22))) \/ ((((cell100) = (cell22)) /\ ((cell1) = (cell23))) \/ ((((cell100) = (cell23)) /\ ((cell1) = (cell24))) \/ ((((cell100) = (cell24)) /\ ((cell1) = (cell25))) \/ ((((cell100) = (cell25)) /\ ((cell1) = (cell26))) \/ ((((cell100) = (cell26)) /\ ((cell1) = (cell27))) \/ ((((cell100) = (cell27)) /\ ((cell1) = (cell28))) \/ ((((cell100) = (cell28)) /\ ((cell1) = (cell29))) \/ ((((cell100) = (cell29)) /\ ((cell1) = (cell30))) \/ ((((cell100) = (cell31)) /\ ((cell1) = (cell32))) \/ ((((cell100) = (cell32)) /\ ((cell1) = (cell33))) \/ ((((cell100) = (cell33)) /\ ((cell1) = (cell34))) \/ ((((cell100) = (cell34)) /\ ((cell1) = (cell35))) \/ ((((cell100) = (cell35)) /\ ((cell1) = (cell36))) \/ ((((cell100) = (cell36)) /\ ((cell1) = (cell37))) \/ ((((cell100) = (cell37)) /\ ((cell1) = (cell38))) \/ ((((cell100) = (cell38)) /\ ((cell1) = (cell39))) \/ ((((cell100) = (cell39)) /\ ((cell1) = (cell40))) \/ ((((cell100) = (cell41)) /\ ((cell1) = (cell42))) \/ ((((cell100) = (cell42)) /\ ((cell1) = (cell43))) \/ ((((cell100) = (cell43)) /\ ((cell1) = (cell44))) \/ ((((cell100) = (cell44)) /\ ((cell1) = (cell45))) \/ ((((cell100) = (cell45)) /\ ((cell1) = (cell46))) \/ ((((cell100) = (cell46)) /\ ((cell1) = (cell47))) \/ ((((cell100) = (cell47)) /\ ((cell1) = (cell48))) \/ ((((cell100) = (cell48)) /\ ((cell1) = (cell49))) \/ ((((cell100) = (cell49)) /\ ((cell1) = (cell50))) \/ ((((cell100) = (cell51)) /\ ((cell1) = (cell52))) \/ ((((cell100) = (cell52)) /\ ((cell1) = (cell53))) \/ ((((cell100) = (cell53)) /\ ((cell1) = (cell54))) \/ ((((cell100) = (cell54)) /\ ((cell1) = (cell55))) \/ ((((cell100) = (cell55)) /\ ((cell1) = (cell56))) \/ ((((cell100) = (cell56)) /\ ((cell1) = (cell57))) \/ ((((cell100) = (cell57)) /\ ((cell1) = (cell58))) \/ ((((cell100) = (cell58)) /\ ((cell1) = (cell59))) \/ ((((cell100) = (cell59)) /\ ((cell1) = (cell60))) \/ ((((cell100) = (cell61)) /\ ((cell1) = (cell62))) \/ ((((cell100) = (cell62)) /\ ((cell1) = (cell63))) \/ ((((cell100) = (cell63)) /\ ((cell1) = (cell64))) \/ ((((cell100) = (cell64)) /\ ((cell1) = (cell65))) \/ ((((cell100) = (cell65)) /\ ((cell1) = (cell66))) \/ ((((cell100) = (cell66)) /\ ((cell1) = (cell67))) \/ ((((cell100) = (cell67)) /\ ((cell1) = (cell68))) \/ ((((cell100) = (cell68)) /\ ((cell1) = (cell69))) \/ ((((cell100) = (cell69)) /\ ((cell1) = (cell70))) \/ ((((cell100) = (cell71)) /\ ((cell1) = (cell72))) \/ ((((cell100) = (cell72)) /\ ((cell1) = (cell73))) \/ ((((cell100) = (cell73)) /\ ((cell1) = (cell74))) \/ ((((cell100) = (cell74)) /\ ((cell1) = (cell75))) \/ ((((cell100) = (cell75)) /\ ((cell1) = (cell76))) \/ ((((cell100) = (cell76)) /\ ((cell1) = (cell77))) \/ ((((cell100) = (cell77)) /\ ((cell1) = (cell78))) \/ ((((cell100) = (cell78)) /\ ((cell1) = (cell79))) \/ ((((cell100) = (cell79)) /\ ((cell1) = (cell80))) \/ ((((cell100) = (cell81)) /\ ((cell1) = (cell82))) \/ ((((cell100) = (cell82)) /\ ((cell1) = (cell83))) \/ ((((cell100) = (cell83)) /\ ((cell1) = (cell84))) \/ ((((cell100) = (cell84)) /\ ((cell1) = (cell85))) \/ ((((cell100) = (cell85)) /\ ((cell1) = (cell86))) \/ ((((cell100) = (cell86)) /\ ((cell1) = (cell87))) \/ ((((cell100) = (cell87)) /\ ((cell1) = (cell88))) \/ ((((cell100) = (cell88)) /\ ((cell1) = (cell89))) \/ ((((cell100) = (cell89)) /\ ((cell1) = (cell90))) \/ ((((cell100) = (cell91)) /\ ((cell1) = (cell92))) \/ ((((cell100) = (cell92)) /\ ((cell1) = (cell93))) \/ ((((cell100) = (cell93)) /\ ((cell1) = (cell94))) \/ ((((cell100) = (cell94)) /\ ((cell1) = (cell95))) \/ ((((cell100) = (cell95)) /\ ((cell1) = (cell96))) \/ ((((cell100) = (cell96)) /\ ((cell1) = (cell97))) \/ ((((cell100) = (cell97)) /\ ((cell1) = (cell98))) \/ ((((cell100) = (cell98)) /\ ((cell1) = (cell99))) \/ ((((cell100) = (cell99)) /\ ((cell1) = (cell100))) \/ ((((cell100) = (cell1)) /\ ((cell1) = (cell11))) \/ ((((cell100) = (cell2)) /\ ((cell1) = (cell12))) \/ ((((cell100) = (cell3)) /\ ((cell1) = (cell13))) \/ ((((cell100) = (cell4)) /\ ((cell1) = (cell14))) \/ ((((cell100) = (cell5)) /\ ((cell1) = (cell15))) \/ ((((cell100) = (cell6)) /\ ((cell1) = (cell16))) \/ ((((cell100) = (cell7)) /\ ((cell1) = (cell17))) \/ ((((cell100) = (cell8)) /\ ((cell1) = (cell18))) \/ ((((cell100) = (cell9)) /\ ((cell1) = (cell19))) \/ ((((cell100) = (cell10)) /\ ((cell1) = (cell20))) \/ ((((cell100) = (cell11)) /\ ((cell1) = (cell21))) \/ ((((cell100) = (cell12)) /\ ((cell1) = (cell22))) \/ ((((cell100) = (cell13)) /\ ((cell1) = (cell23))) \/ ((((cell100) = (cell14)) /\ ((cell1) = (cell24))) \/ ((((cell100) = (cell15)) /\ ((cell1) = (cell25))) \/ ((((cell100) = (cell16)) /\ ((cell1) = (cell26))) \/ ((((cell100) = (cell17)) /\ ((cell1) = (cell27))) \/ ((((cell100) = (cell18)) /\ ((cell1) = (cell28))) \/ ((((cell100) = (cell19)) /\ ((cell1) = (cell29))) \/ ((((cell100) = (cell20)) /\ ((cell1) = (cell30))) \/ ((((cell100) = (cell21)) /\ ((cell1) = (cell31))) \/ ((((cell100) = (cell22)) /\ ((cell1) = (cell32))) \/ ((((cell100) = (cell23)) /\ ((cell1) = (cell33))) \/ ((((cell100) = (cell24)) /\ ((cell1) = (cell34))) \/ ((((cell100) = (cell25)) /\ ((cell1) = (cell35))) \/ ((((cell100) = (cell26)) /\ ((cell1) = (cell36))) \/ ((((cell100) = (cell27)) /\ ((cell1) = (cell37))) \/ ((((cell100) = (cell28)) /\ ((cell1) = (cell38))) \/ ((((cell100) = (cell29)) /\ ((cell1) = (cell39))) \/ ((((cell100) = (cell30)) /\ ((cell1) = (cell40))) \/ ((((cell100) = (cell31)) /\ ((cell1) = (cell41))) \/ ((((cell100) = (cell32)) /\ ((cell1) = (cell42))) \/ ((((cell100) = (cell33)) /\ ((cell1) = (cell43))) \/ ((((cell100) = (cell34)) /\ ((cell1) = (cell44))) \/ ((((cell100) = (cell35)) /\ ((cell1) = (cell45))) \/ ((((cell100) = (cell36)) /\ ((cell1) = (cell46))) \/ ((((cell100) = (cell37)) /\ ((cell1) = (cell47))) \/ ((((cell100) = (cell38)) /\ ((cell1) = (cell48))) \/ ((((cell100) = (cell39)) /\ ((cell1) = (cell49))) \/ ((((cell100) = (cell40)) /\ ((cell1) = (cell50))) \/ ((((cell100) = (cell41)) /\ ((cell1) = (cell51))) \/ ((((cell100) = (cell42)) /\ ((cell1) = (cell52))) \/ ((((cell100) = (cell43)) /\ ((cell1) = (cell53))) \/ ((((cell100) = (cell44)) /\ ((cell1) = (cell54))) \/ ((((cell100) = (cell45)) /\ ((cell1) = (cell55))) \/ ((((cell100) = (cell46)) /\ ((cell1) = (cell56))) \/ ((((cell100) = (cell47)) /\ ((cell1) = (cell57))) \/ ((((cell100) = (cell48)) /\ ((cell1) = (cell58))) \/ ((((cell100) = (cell49)) /\ ((cell1) = (cell59))) \/ ((((cell100) = (cell50)) /\ ((cell1) = (cell60))) \/ ((((cell100) = (cell51)) /\ ((cell1) = (cell61))) \/ ((((cell100) = (cell52)) /\ ((cell1) = (cell62))) \/ ((((cell100) = (cell53)) /\ ((cell1) = (cell63))) \/ ((((cell100) = (cell54)) /\ ((cell1) = (cell64))) \/ ((((cell100) = (cell55)) /\ ((cell1) = (cell65))) \/ ((((cell100) = (cell56)) /\ ((cell1) = (cell66))) \/ ((((cell100) = (cell57)) /\ ((cell1) = (cell67))) \/ ((((cell100) = (cell58)) /\ ((cell1) = (cell68))) \/ ((((cell100) = (cell59)) /\ ((cell1) = (cell69))) \/ ((((cell100) = (cell60)) /\ ((cell1) = (cell70))) \/ ((((cell100) = (cell61)) /\ ((cell1) = (cell71))) \/ ((((cell100) = (cell62)) /\ ((cell1) = (cell72))) \/ ((((cell100) = (cell63)) /\ ((cell1) = (cell73))) \/ ((((cell100) = (cell64)) /\ ((cell1) = (cell74))) \/ ((((cell100) = (cell65)) /\ ((cell1) = (cell75))) \/ ((((cell100) = (cell66)) /\ ((cell1) = (cell76))) \/ ((((cell100) = (cell67)) /\ ((cell1) = (cell77))) \/ ((((cell100) = (cell68)) /\ ((cell1) = (cell78))) \/ ((((cell100) = (cell69)) /\ ((cell1) = (cell79))) \/ ((((cell100) = (cell70)) /\ ((cell1) = (cell80))) \/ ((((cell100) = (cell71)) /\ ((cell1) = (cell81))) \/ ((((cell100) = (cell72)) /\ ((cell1) = (cell82))) \/ ((((cell100) = (cell73)) /\ ((cell1) = (cell83))) \/ ((((cell100) = (cell74)) /\ ((cell1) = (cell84))) \/ ((((cell100) = (cell75)) /\ ((cell1) = (cell85))) \/ ((((cell100) = (cell76)) /\ ((cell1) = (cell86))) \/ ((((cell100) = (cell77)) /\ ((cell1) = (cell87))) \/ ((((cell100) = (cell78)) /\ ((cell1) = (cell88))) \/ ((((cell100) = (cell79)) /\ ((cell1) = (cell89))) \/ ((((cell100) = (cell80)) /\ ((cell1) = (cell90))) \/ ((((cell100) = (cell81)) /\ ((cell1) = (cell91))) \/ ((((cell100) = (cell82)) /\ ((cell1) = (cell92))) \/ ((((cell100) = (cell83)) /\ ((cell1) = (cell93))) \/ ((((cell100) = (cell84)) /\ ((cell1) = (cell94))) \/ ((((cell100) = (cell85)) /\ ((cell1) = (cell95))) \/ ((((cell100) = (cell86)) /\ ((cell1) = (cell96))) \/ ((((cell100) = (cell87)) /\ ((cell1) = (cell97))) \/ ((((cell100) = (cell88)) /\ ((cell1) = (cell98))) \/ ((((cell100) = (cell89)) /\ ((cell1) = (cell99))) \/ (((cell100) = (cell90)) /\ ((cell1) = (cell100)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ((cell90) != (cell100)) ((cell80) != (cell100)) ((cell70) != (cell100)) ((cell60) != (cell100)) ((cell50) != (cell100)) ((cell40) != (cell100)) ((cell30) != (cell100)) ((cell20) != (cell100)) ((cell10) != (cell100)) ((cell99) != (cell100)) ((cell98) != (cell100)) ((cell97) != (cell100)) ((cell96) != (cell100)) ((cell95) != (cell100)) ((cell94) != (cell100)) ((cell93) != (cell100)) ((cell92) != (cell100)) ((cell91) != (cell100)) ((cell89) != (cell100)) ((cell88) != (cell100)) ((cell87) != (cell100)) ((cell86) != (cell100)) ((cell85) != (cell100)) ((cell84) != (cell100)) ((cell83) != (cell100)) ((cell82) != (cell100)) ((cell81) != (cell100)) ((cell79) != (cell100)) ((cell78) != (cell100)) ((cell77) != (cell100)) ((cell76) != (cell100)) ((cell75) != (cell100)) ((cell74) != (cell100)) ((cell73) != (cell100)) ((cell72) != (cell100)) ((cell71) != (cell100)) ((cell69) != (cell100)) ((cell68) != (cell100)) ((cell67) != (cell100)) ((cell66) != (cell100)) ((cell65) != (cell100)) ((cell64) != (cell100)) ((cell63) != (cell100)) ((cell62) != (cell100)) ((cell61) != (cell100)) ((cell59) != (cell100)) ((cell58) != (cell100)) ((cell57) != (cell100)) ((cell56) != (cell100)) ((cell55) != (cell100)) ((cell54) != (cell100)) ((cell53) != (cell100)) ((cell52) != (cell100)) ((cell51) != (cell100)) ((cell49) != (cell100)) ((cell48) != (cell100)) ((cell47) != (cell100)) ((cell46) != (cell100)) ((cell45) != (cell100)) ((cell44) != (cell100)) ((cell43) != (cell100)) ((cell42) != (cell100)) ((cell41) != (cell100)) ((cell39) != (cell100)) ((cell38) != (cell100)) ((cell37) != (cell100)) ((cell36) != (cell100)) ((cell35) != (cell100)) ((cell34) != (cell100)) ((cell33) != (cell100)) ((cell32) != (cell100)) ((cell31) != (cell100)) ((cell29) != (cell100)) ((cell28) != (cell100)) ((cell27) != (cell100)) ((cell26) != (cell100)) ((cell25) != (cell100)) ((cell24) != (cell100)) ((cell23) != (cell100)) ((cell22) != (cell100)) ((cell21) != (cell100)) ((cell19) != (cell100)) ((cell18) != (cell100)) ((cell17) != (cell100)) ((cell16) != (cell100)) ((cell15) != (cell100)) ((cell14) != (cell100)) ((cell13) != (cell100)) ((cell12) != (cell100)) ((cell11) != (cell100)) ((cell9) != (cell100)) ((cell8) != (cell100)) ((cell7) != (cell100)) ((cell6) != (cell100)) ((cell5) != (cell100)) ((cell4) != (cell100)) ((cell3) != (cell100)) ((cell2) != (cell100)) ((cell1) != (cell100)) ### DisjTree 364 366 368 370 372 374 376 378 380 382 384 386 388 390 392 394 396 398 400 402 404 406 408 410 412 414 416 418 420 422 424 426 428 430 432 434 436 438 440 442 444 446 448 450 452 454 456 458 460 462 464 466 468 470 472 474 476 478 480 482 484 486 488 490 492 494 496 498 500 502 504 506 508 510 512 514 516 518 520 522 524 526 528 530 532 534 536 538 540 542 544 546 548 550 552 554 556 558 560 562 564 566 568 570 572 574 576 578 580 582 584 586 588 590 592 594 596 598 600 602 604 606 608 610 612 614 616 618 620 622 624 626 628 630 632 634 636 638 640 642 644 646 648 650 652 654 656 658 660 662 664 666 668 670 672 674 676 678 680 682 684 686 688 690 692 694 696 698 700 702 704 706 708 710 712 714 716 718 720 722 % 2.88/3.07 724. (edge (cell100) (cell1)) ((cell1) != (cell100)) ((cell2) != (cell100)) ((cell3) != (cell100)) ((cell4) != (cell100)) ((cell5) != (cell100)) ((cell6) != (cell100)) ((cell7) != (cell100)) ((cell8) != (cell100)) ((cell9) != (cell100)) ((cell11) != (cell100)) ((cell12) != (cell100)) ((cell13) != (cell100)) ((cell14) != (cell100)) ((cell15) != (cell100)) ((cell16) != (cell100)) ((cell17) != (cell100)) ((cell18) != (cell100)) ((cell19) != (cell100)) ((cell21) != (cell100)) ((cell22) != (cell100)) ((cell23) != (cell100)) ((cell24) != (cell100)) ((cell25) != (cell100)) ((cell26) != (cell100)) ((cell27) != (cell100)) ((cell28) != (cell100)) ((cell29) != (cell100)) ((cell31) != (cell100)) ((cell32) != (cell100)) ((cell33) != (cell100)) ((cell34) != (cell100)) ((cell35) != (cell100)) ((cell36) != (cell100)) ((cell37) != (cell100)) ((cell38) != (cell100)) ((cell39) != (cell100)) ((cell41) != (cell100)) ((cell42) != (cell100)) ((cell43) != (cell100)) ((cell44) != (cell100)) ((cell45) != (cell100)) ((cell46) != (cell100)) ((cell47) != (cell100)) ((cell48) != (cell100)) ((cell49) != (cell100)) ((cell51) != (cell100)) ((cell52) != (cell100)) ((cell53) != (cell100)) ((cell54) != (cell100)) ((cell55) != (cell100)) ((cell56) != (cell100)) ((cell57) != (cell100)) ((cell58) != (cell100)) ((cell59) != (cell100)) ((cell61) != (cell100)) ((cell62) != (cell100)) ((cell63) != (cell100)) ((cell64) != (cell100)) ((cell65) != (cell100)) ((cell66) != (cell100)) ((cell67) != (cell100)) ((cell68) != (cell100)) ((cell69) != (cell100)) ((cell71) != (cell100)) ((cell72) != (cell100)) ((cell73) != (cell100)) ((cell74) != (cell100)) ((cell75) != (cell100)) ((cell76) != (cell100)) ((cell77) != (cell100)) ((cell78) != (cell100)) ((cell79) != (cell100)) ((cell81) != (cell100)) ((cell82) != (cell100)) ((cell83) != (cell100)) ((cell84) != (cell100)) ((cell85) != (cell100)) ((cell86) != (cell100)) ((cell87) != (cell100)) ((cell88) != (cell100)) ((cell89) != (cell100)) ((cell91) != (cell100)) ((cell92) != (cell100)) ((cell93) != (cell100)) ((cell94) != (cell100)) ((cell95) != (cell100)) ((cell96) != (cell100)) ((cell97) != (cell100)) ((cell98) != (cell100)) ((cell99) != (cell100)) ((cell10) != (cell100)) ((cell20) != (cell100)) ((cell30) != (cell100)) ((cell40) != (cell100)) ((cell50) != (cell100)) ((cell60) != (cell100)) ((cell70) != (cell100)) ((cell80) != (cell100)) ((cell90) != (cell100)) ### Definition-Pseudo(edge) 723 % 2.88/3.07 725. ((edge (cell1) (cell100)) \/ (edge (cell100) (cell1))) ((cell90) != (cell100)) ((cell80) != (cell100)) ((cell70) != (cell100)) ((cell60) != (cell100)) ((cell50) != (cell100)) ((cell40) != (cell100)) ((cell30) != (cell100)) ((cell20) != (cell100)) ((cell10) != (cell100)) ((cell99) != (cell100)) ((cell98) != (cell100)) ((cell97) != (cell100)) ((cell96) != (cell100)) ((cell95) != (cell100)) ((cell94) != (cell100)) ((cell93) != (cell100)) ((cell92) != (cell100)) ((cell91) != (cell100)) ((cell89) != (cell100)) ((cell88) != (cell100)) ((cell87) != (cell100)) ((cell86) != (cell100)) ((cell85) != (cell100)) ((cell84) != (cell100)) ((cell83) != (cell100)) ((cell82) != (cell100)) ((cell81) != (cell100)) ((cell79) != (cell100)) ((cell78) != (cell100)) ((cell77) != (cell100)) ((cell76) != (cell100)) ((cell75) != (cell100)) ((cell74) != (cell100)) ((cell73) != (cell100)) ((cell72) != (cell100)) ((cell71) != (cell100)) ((cell69) != (cell100)) ((cell68) != (cell100)) ((cell67) != (cell100)) ((cell66) != (cell100)) ((cell65) != (cell100)) ((cell64) != (cell100)) ((cell63) != (cell100)) ((cell62) != (cell100)) ((cell61) != (cell100)) ((cell59) != (cell100)) ((cell58) != (cell100)) ((cell57) != (cell100)) ((cell56) != (cell100)) ((cell55) != (cell100)) ((cell54) != (cell100)) ((cell53) != (cell100)) ((cell52) != (cell100)) ((cell51) != (cell100)) ((cell49) != (cell100)) ((cell48) != (cell100)) ((cell47) != (cell100)) ((cell46) != (cell100)) ((cell45) != (cell100)) ((cell44) != (cell100)) ((cell43) != (cell100)) ((cell42) != (cell100)) ((cell41) != (cell100)) ((cell39) != (cell100)) ((cell38) != (cell100)) ((cell37) != (cell100)) ((cell36) != (cell100)) ((cell35) != (cell100)) ((cell34) != (cell100)) ((cell33) != (cell100)) ((cell32) != (cell100)) ((cell31) != (cell100)) ((cell29) != (cell100)) ((cell28) != (cell100)) ((cell27) != (cell100)) ((cell26) != (cell100)) ((cell25) != (cell100)) ((cell24) != (cell100)) ((cell23) != (cell100)) ((cell22) != (cell100)) ((cell21) != (cell100)) ((cell19) != (cell100)) ((cell18) != (cell100)) ((cell17) != (cell100)) ((cell16) != (cell100)) ((cell15) != (cell100)) ((cell14) != (cell100)) ((cell13) != (cell100)) ((cell12) != (cell100)) ((cell9) != (cell100)) ((cell8) != (cell100)) ((cell7) != (cell100)) ((cell6) != (cell100)) ((cell5) != (cell100)) ((cell4) != (cell100)) ((cell3) != (cell100)) ((cell1) != (cell100)) ((cell90) != (cell1)) ((cell80) != (cell1)) ((cell70) != (cell1)) ((cell60) != (cell1)) ((cell50) != (cell1)) ((cell40) != (cell1)) ((cell30) != (cell1)) ((cell20) != (cell1)) ((cell10) != (cell1)) ((cell11) != (cell100)) ((cell99) != (cell1)) ((cell98) != (cell1)) ((cell97) != (cell1)) ((cell96) != (cell1)) ((cell95) != (cell1)) ((cell94) != (cell1)) ((cell93) != (cell1)) ((cell92) != (cell1)) ((cell91) != (cell1)) ((cell89) != (cell1)) ((cell88) != (cell1)) ((cell87) != (cell1)) ((cell86) != (cell1)) ((cell85) != (cell1)) ((cell84) != (cell1)) ((cell83) != (cell1)) ((cell82) != (cell1)) ((cell81) != (cell1)) ((cell79) != (cell1)) ((cell78) != (cell1)) ((cell77) != (cell1)) ((cell76) != (cell1)) ((cell75) != (cell1)) ((cell74) != (cell1)) ((cell73) != (cell1)) ((cell72) != (cell1)) ((cell71) != (cell1)) ((cell69) != (cell1)) ((cell68) != (cell1)) ((cell67) != (cell1)) ((cell66) != (cell1)) ((cell65) != (cell1)) ((cell64) != (cell1)) ((cell63) != (cell1)) ((cell62) != (cell1)) ((cell61) != (cell1)) ((cell59) != (cell1)) ((cell58) != (cell1)) ((cell57) != (cell1)) ((cell56) != (cell1)) ((cell55) != (cell1)) ((cell54) != (cell1)) ((cell53) != (cell1)) ((cell52) != (cell1)) ((cell51) != (cell1)) ((cell49) != (cell1)) ((cell48) != (cell1)) ((cell47) != (cell1)) ((cell46) != (cell1)) ((cell45) != (cell1)) ((cell44) != (cell1)) ((cell43) != (cell1)) ((cell42) != (cell1)) ((cell41) != (cell1)) ((cell39) != (cell1)) ((cell38) != (cell1)) ((cell37) != (cell1)) ((cell36) != (cell1)) ((cell35) != (cell1)) ((cell34) != (cell1)) ((cell33) != (cell1)) ((cell32) != (cell1)) ((cell31) != (cell1)) ((cell29) != (cell1)) ((cell28) != (cell1)) ((cell27) != (cell1)) ((cell26) != (cell1)) ((cell25) != (cell1)) ((cell24) != (cell1)) ((cell23) != (cell1)) ((cell22) != (cell1)) ((cell21) != (cell1)) ((cell19) != (cell1)) ((cell18) != (cell1)) ((cell17) != (cell1)) ((cell16) != (cell1)) ((cell15) != (cell1)) ((cell14) != (cell1)) ((cell13) != (cell1)) ((cell12) != (cell1)) ((cell11) != (cell1)) ((cell9) != (cell1)) ((cell8) != (cell1)) ((cell7) != (cell1)) ((cell6) != (cell1)) ((cell5) != (cell1)) ((cell4) != (cell1)) ((cell3) != (cell1)) ((cell2) != (cell1)) ((cell2) != (cell100)) ### Or 362 724 % 2.88/3.07 726. (adj (cell1) (cell100)) ((cell2) != (cell100)) ((cell2) != (cell1)) ((cell3) != (cell1)) ((cell4) != (cell1)) ((cell5) != (cell1)) ((cell6) != (cell1)) ((cell7) != (cell1)) ((cell8) != (cell1)) ((cell9) != (cell1)) ((cell11) != (cell1)) ((cell12) != (cell1)) ((cell13) != (cell1)) ((cell14) != (cell1)) ((cell15) != (cell1)) ((cell16) != (cell1)) ((cell17) != (cell1)) ((cell18) != (cell1)) ((cell19) != (cell1)) ((cell21) != (cell1)) ((cell22) != (cell1)) ((cell23) != (cell1)) ((cell24) != (cell1)) ((cell25) != (cell1)) ((cell26) != (cell1)) ((cell27) != (cell1)) ((cell28) != (cell1)) ((cell29) != (cell1)) ((cell31) != (cell1)) ((cell32) != (cell1)) ((cell33) != (cell1)) ((cell34) != (cell1)) ((cell35) != (cell1)) ((cell36) != (cell1)) ((cell37) != (cell1)) ((cell38) != (cell1)) ((cell39) != (cell1)) ((cell41) != (cell1)) ((cell42) != (cell1)) ((cell43) != (cell1)) ((cell44) != (cell1)) ((cell45) != (cell1)) ((cell46) != (cell1)) ((cell47) != (cell1)) ((cell48) != (cell1)) ((cell49) != (cell1)) ((cell51) != (cell1)) ((cell52) != (cell1)) ((cell53) != (cell1)) ((cell54) != (cell1)) ((cell55) != (cell1)) ((cell56) != (cell1)) ((cell57) != (cell1)) ((cell58) != (cell1)) ((cell59) != (cell1)) ((cell61) != (cell1)) ((cell62) != (cell1)) ((cell63) != (cell1)) ((cell64) != (cell1)) ((cell65) != (cell1)) ((cell66) != (cell1)) ((cell67) != (cell1)) ((cell68) != (cell1)) ((cell69) != (cell1)) ((cell71) != (cell1)) ((cell72) != (cell1)) ((cell73) != (cell1)) ((cell74) != (cell1)) ((cell75) != (cell1)) ((cell76) != (cell1)) ((cell77) != (cell1)) ((cell78) != (cell1)) ((cell79) != (cell1)) ((cell81) != (cell1)) ((cell82) != (cell1)) ((cell83) != (cell1)) ((cell84) != (cell1)) ((cell85) != (cell1)) ((cell86) != (cell1)) ((cell87) != (cell1)) ((cell88) != (cell1)) ((cell89) != (cell1)) ((cell91) != (cell1)) ((cell92) != (cell1)) ((cell93) != (cell1)) ((cell94) != (cell1)) ((cell95) != (cell1)) ((cell96) != (cell1)) ((cell97) != (cell1)) ((cell98) != (cell1)) ((cell99) != (cell1)) ((cell11) != (cell100)) ((cell10) != (cell1)) ((cell20) != (cell1)) ((cell30) != (cell1)) ((cell40) != (cell1)) ((cell50) != (cell1)) ((cell60) != (cell1)) ((cell70) != (cell1)) ((cell80) != (cell1)) ((cell90) != (cell1)) ((cell1) != (cell100)) ((cell3) != (cell100)) ((cell4) != (cell100)) ((cell5) != (cell100)) ((cell6) != (cell100)) ((cell7) != (cell100)) ((cell8) != (cell100)) ((cell9) != (cell100)) ((cell12) != (cell100)) ((cell13) != (cell100)) ((cell14) != (cell100)) ((cell15) != (cell100)) ((cell16) != (cell100)) ((cell17) != (cell100)) ((cell18) != (cell100)) ((cell19) != (cell100)) ((cell21) != (cell100)) ((cell22) != (cell100)) ((cell23) != (cell100)) ((cell24) != (cell100)) ((cell25) != (cell100)) ((cell26) != (cell100)) ((cell27) != (cell100)) ((cell28) != (cell100)) ((cell29) != (cell100)) ((cell31) != (cell100)) ((cell32) != (cell100)) ((cell33) != (cell100)) ((cell34) != (cell100)) ((cell35) != (cell100)) ((cell36) != (cell100)) ((cell37) != (cell100)) ((cell38) != (cell100)) ((cell39) != (cell100)) ((cell41) != (cell100)) ((cell42) != (cell100)) ((cell43) != (cell100)) ((cell44) != (cell100)) ((cell45) != (cell100)) ((cell46) != (cell100)) ((cell47) != (cell100)) ((cell48) != (cell100)) ((cell49) != (cell100)) ((cell51) != (cell100)) ((cell52) != (cell100)) ((cell53) != (cell100)) ((cell54) != (cell100)) ((cell55) != (cell100)) ((cell56) != (cell100)) ((cell57) != (cell100)) ((cell58) != (cell100)) ((cell59) != (cell100)) ((cell61) != (cell100)) ((cell62) != (cell100)) ((cell63) != (cell100)) ((cell64) != (cell100)) ((cell65) != (cell100)) ((cell66) != (cell100)) ((cell67) != (cell100)) ((cell68) != (cell100)) ((cell69) != (cell100)) ((cell71) != (cell100)) ((cell72) != (cell100)) ((cell73) != (cell100)) ((cell74) != (cell100)) ((cell75) != (cell100)) ((cell76) != (cell100)) ((cell77) != (cell100)) ((cell78) != (cell100)) ((cell79) != (cell100)) ((cell81) != (cell100)) ((cell82) != (cell100)) ((cell83) != (cell100)) ((cell84) != (cell100)) ((cell85) != (cell100)) ((cell86) != (cell100)) ((cell87) != (cell100)) ((cell88) != (cell100)) ((cell89) != (cell100)) ((cell91) != (cell100)) ((cell92) != (cell100)) ((cell93) != (cell100)) ((cell94) != (cell100)) ((cell95) != (cell100)) ((cell96) != (cell100)) ((cell97) != (cell100)) ((cell98) != (cell100)) ((cell99) != (cell100)) ((cell10) != (cell100)) ((cell20) != (cell100)) ((cell30) != (cell100)) ((cell40) != (cell100)) ((cell50) != (cell100)) ((cell60) != (cell100)) ((cell70) != (cell100)) ((cell80) != (cell100)) ((cell90) != (cell100)) ### Definition-Pseudo(adj) 725 % 2.88/3.07 727. (-. (-. (adj (cell1) (cell100)))) ((cell90) != (cell100)) ((cell80) != (cell100)) ((cell70) != (cell100)) ((cell60) != (cell100)) ((cell50) != (cell100)) ((cell40) != (cell100)) ((cell30) != (cell100)) ((cell20) != (cell100)) ((cell10) != (cell100)) ((cell99) != (cell100)) ((cell98) != (cell100)) ((cell97) != (cell100)) ((cell96) != (cell100)) ((cell95) != (cell100)) ((cell94) != (cell100)) ((cell93) != (cell100)) ((cell92) != (cell100)) ((cell91) != (cell100)) ((cell89) != (cell100)) ((cell88) != (cell100)) ((cell87) != (cell100)) ((cell86) != (cell100)) ((cell85) != (cell100)) ((cell84) != (cell100)) ((cell83) != (cell100)) ((cell82) != (cell100)) ((cell81) != (cell100)) ((cell79) != (cell100)) ((cell78) != (cell100)) ((cell77) != (cell100)) ((cell76) != (cell100)) ((cell75) != (cell100)) ((cell74) != (cell100)) ((cell73) != (cell100)) ((cell72) != (cell100)) ((cell71) != (cell100)) ((cell69) != (cell100)) ((cell68) != (cell100)) ((cell67) != (cell100)) ((cell66) != (cell100)) ((cell65) != (cell100)) ((cell64) != (cell100)) ((cell63) != (cell100)) ((cell62) != (cell100)) ((cell61) != (cell100)) ((cell59) != (cell100)) ((cell58) != (cell100)) ((cell57) != (cell100)) ((cell56) != (cell100)) ((cell55) != (cell100)) ((cell54) != (cell100)) ((cell53) != (cell100)) ((cell52) != (cell100)) ((cell51) != (cell100)) ((cell49) != (cell100)) ((cell48) != (cell100)) ((cell47) != (cell100)) ((cell46) != (cell100)) ((cell45) != (cell100)) ((cell44) != (cell100)) ((cell43) != (cell100)) ((cell42) != (cell100)) ((cell41) != (cell100)) ((cell39) != (cell100)) ((cell38) != (cell100)) ((cell37) != (cell100)) ((cell36) != (cell100)) ((cell35) != (cell100)) ((cell34) != (cell100)) ((cell33) != (cell100)) ((cell32) != (cell100)) ((cell31) != (cell100)) ((cell29) != (cell100)) ((cell28) != (cell100)) ((cell27) != (cell100)) ((cell26) != (cell100)) ((cell25) != (cell100)) ((cell24) != (cell100)) ((cell23) != (cell100)) ((cell22) != (cell100)) ((cell21) != (cell100)) ((cell19) != (cell100)) ((cell18) != (cell100)) ((cell17) != (cell100)) ((cell16) != (cell100)) ((cell15) != (cell100)) ((cell14) != (cell100)) ((cell13) != (cell100)) ((cell12) != (cell100)) ((cell9) != (cell100)) ((cell8) != (cell100)) ((cell7) != (cell100)) ((cell6) != (cell100)) ((cell5) != (cell100)) ((cell4) != (cell100)) ((cell3) != (cell100)) ((cell1) != (cell100)) ((cell90) != (cell1)) ((cell80) != (cell1)) ((cell70) != (cell1)) ((cell60) != (cell1)) ((cell50) != (cell1)) ((cell40) != (cell1)) ((cell30) != (cell1)) ((cell20) != (cell1)) ((cell10) != (cell1)) ((cell11) != (cell100)) ((cell99) != (cell1)) ((cell98) != (cell1)) ((cell97) != (cell1)) ((cell96) != (cell1)) ((cell95) != (cell1)) ((cell94) != (cell1)) ((cell93) != (cell1)) ((cell92) != (cell1)) ((cell91) != (cell1)) ((cell89) != (cell1)) ((cell88) != (cell1)) ((cell87) != (cell1)) ((cell86) != (cell1)) ((cell85) != (cell1)) ((cell84) != (cell1)) ((cell83) != (cell1)) ((cell82) != (cell1)) ((cell81) != (cell1)) ((cell79) != (cell1)) ((cell78) != (cell1)) ((cell77) != (cell1)) ((cell76) != (cell1)) ((cell75) != (cell1)) ((cell74) != (cell1)) ((cell73) != (cell1)) ((cell72) != (cell1)) ((cell71) != (cell1)) ((cell69) != (cell1)) ((cell68) != (cell1)) ((cell67) != (cell1)) ((cell66) != (cell1)) ((cell65) != (cell1)) ((cell64) != (cell1)) ((cell63) != (cell1)) ((cell62) != (cell1)) ((cell61) != (cell1)) ((cell59) != (cell1)) ((cell58) != (cell1)) ((cell57) != (cell1)) ((cell56) != (cell1)) ((cell55) != (cell1)) ((cell54) != (cell1)) ((cell53) != (cell1)) ((cell52) != (cell1)) ((cell51) != (cell1)) ((cell49) != (cell1)) ((cell48) != (cell1)) ((cell47) != (cell1)) ((cell46) != (cell1)) ((cell45) != (cell1)) ((cell44) != (cell1)) ((cell43) != (cell1)) ((cell42) != (cell1)) ((cell41) != (cell1)) ((cell39) != (cell1)) ((cell38) != (cell1)) ((cell37) != (cell1)) ((cell36) != (cell1)) ((cell35) != (cell1)) ((cell34) != (cell1)) ((cell33) != (cell1)) ((cell32) != (cell1)) ((cell31) != (cell1)) ((cell29) != (cell1)) ((cell28) != (cell1)) ((cell27) != (cell1)) ((cell26) != (cell1)) ((cell25) != (cell1)) ((cell24) != (cell1)) ((cell23) != (cell1)) ((cell22) != (cell1)) ((cell21) != (cell1)) ((cell19) != (cell1)) ((cell18) != (cell1)) ((cell17) != (cell1)) ((cell16) != (cell1)) ((cell15) != (cell1)) ((cell14) != (cell1)) ((cell13) != (cell1)) ((cell12) != (cell1)) ((cell11) != (cell1)) ((cell9) != (cell1)) ((cell8) != (cell1)) ((cell7) != (cell1)) ((cell6) != (cell1)) ((cell5) != (cell1)) ((cell4) != (cell1)) ((cell3) != (cell1)) ((cell2) != (cell1)) ((cell2) != (cell100)) ### NotNot 726 % 2.88/3.08 % SZS output end Proof % 2.88/3.08 (* END-PROOF *) %------------------------------------------------------------------------------