(benchmark mip_vpm2
:source {
Relaxation of the Mixed-Integer Programming
optimization problem vpm2 from the MIPLIB (http://miplib.zib.de/)
by Enric Rodriguez-Carbonell (erodri@lsi.upc.edu)
}
  :status sat
  :category { industrial }
  :difficulty { 2 }
  :logic QF_LRA

  :extrafuns ((tmp348 Real))
  :extrafuns ((tmp347 Real))
  :extrafuns ((tmp346 Real))
  :extrafuns ((tmp345 Real))
  :extrafuns ((tmp344 Real))
  :extrafuns ((tmp343 Real))
  :extrafuns ((tmp342 Real))
  :extrafuns ((tmp341 Real))
  :extrafuns ((tmp340 Real))
  :extrafuns ((tmp339 Real))
  :extrafuns ((tmp338 Real))
  :extrafuns ((tmp337 Real))
  :extrafuns ((tmp336 Real))
  :extrafuns ((tmp335 Real))
  :extrafuns ((tmp334 Real))
  :extrafuns ((tmp333 Real))
  :extrafuns ((tmp332 Real))
  :extrafuns ((tmp331 Real))
  :extrafuns ((tmp330 Real))
  :extrafuns ((tmp329 Real))
  :extrafuns ((tmp328 Real))
  :extrafuns ((tmp327 Real))
  :extrafuns ((tmp326 Real))
  :extrafuns ((tmp325 Real))
  :extrafuns ((tmp324 Real))
  :extrafuns ((tmp323 Real))
  :extrafuns ((tmp322 Real))
  :extrafuns ((tmp321 Real))
  :extrafuns ((tmp320 Real))
  :extrafuns ((tmp319 Real))
  :extrafuns ((tmp318 Real))
  :extrafuns ((tmp317 Real))
  :extrafuns ((tmp316 Real))
  :extrafuns ((tmp315 Real))
  :extrafuns ((tmp314 Real))
  :extrafuns ((tmp313 Real))
  :extrafuns ((tmp312 Real))
  :extrafuns ((tmp311 Real))
  :extrafuns ((tmp310 Real))
  :extrafuns ((tmp309 Real))
  :extrafuns ((tmp308 Real))
  :extrafuns ((tmp307 Real))
  :extrafuns ((tmp306 Real))
  :extrafuns ((tmp305 Real))
  :extrafuns ((tmp304 Real))
  :extrafuns ((tmp303 Real))
  :extrafuns ((tmp302 Real))
  :extrafuns ((tmp301 Real))
  :extrafuns ((tmp300 Real))
  :extrafuns ((tmp299 Real))
  :extrafuns ((tmp298 Real))
  :extrafuns ((tmp297 Real))
  :extrafuns ((tmp296 Real))
  :extrafuns ((tmp295 Real))
  :extrafuns ((tmp294 Real))
  :extrafuns ((tmp293 Real))
  :extrafuns ((tmp292 Real))
  :extrafuns ((tmp291 Real))
  :extrafuns ((tmp290 Real))
  :extrafuns ((tmp289 Real))
  :extrafuns ((tmp288 Real))
  :extrafuns ((tmp287 Real))
  :extrafuns ((tmp286 Real))
  :extrafuns ((tmp285 Real))
  :extrafuns ((tmp284 Real))
  :extrafuns ((tmp283 Real))
  :extrafuns ((tmp282 Real))
  :extrafuns ((tmp281 Real))
  :extrafuns ((tmp280 Real))
  :extrafuns ((tmp279 Real))
  :extrafuns ((tmp278 Real))
  :extrafuns ((tmp277 Real))
  :extrafuns ((tmp276 Real))
  :extrafuns ((tmp275 Real))
  :extrafuns ((tmp274 Real))
  :extrafuns ((tmp273 Real))
  :extrafuns ((tmp272 Real))
  :extrafuns ((tmp271 Real))
  :extrafuns ((tmp270 Real))
  :extrafuns ((tmp269 Real))
  :extrafuns ((tmp268 Real))
  :extrafuns ((tmp267 Real))
  :extrafuns ((tmp266 Real))
  :extrafuns ((tmp265 Real))
  :extrafuns ((tmp264 Real))
  :extrafuns ((tmp263 Real))
  :extrafuns ((tmp262 Real))
  :extrafuns ((tmp261 Real))
  :extrafuns ((tmp260 Real))
  :extrafuns ((tmp259 Real))
  :extrafuns ((tmp258 Real))
  :extrafuns ((tmp257 Real))
  :extrafuns ((tmp256 Real))
  :extrafuns ((tmp255 Real))
  :extrafuns ((tmp254 Real))
  :extrafuns ((tmp253 Real))
  :extrafuns ((tmp252 Real))
  :extrafuns ((tmp251 Real))
  :extrafuns ((tmp250 Real))
  :extrafuns ((tmp249 Real))
  :extrafuns ((tmp248 Real))
  :extrafuns ((tmp247 Real))
  :extrafuns ((tmp246 Real))
  :extrafuns ((tmp245 Real))
  :extrafuns ((tmp244 Real))
  :extrafuns ((tmp243 Real))
  :extrafuns ((tmp242 Real))
  :extrafuns ((tmp241 Real))
  :extrafuns ((tmp240 Real))
  :extrafuns ((tmp239 Real))
  :extrafuns ((tmp238 Real))
  :extrafuns ((tmp237 Real))
  :extrafuns ((tmp236 Real))
  :extrafuns ((tmp235 Real))
  :extrafuns ((tmp234 Real))
  :extrafuns ((tmp233 Real))
  :extrafuns ((tmp232 Real))
  :extrafuns ((tmp231 Real))
  :extrafuns ((tmp230 Real))
  :extrafuns ((tmp229 Real))
  :extrafuns ((tmp228 Real))
  :extrafuns ((tmp227 Real))
  :extrafuns ((tmp226 Real))
  :extrafuns ((tmp225 Real))
  :extrafuns ((tmp224 Real))
  :extrafuns ((tmp223 Real))
  :extrafuns ((tmp222 Real))
  :extrafuns ((tmp221 Real))
  :extrafuns ((tmp220 Real))
  :extrafuns ((tmp219 Real))
  :extrafuns ((tmp218 Real))
  :extrafuns ((tmp217 Real))
  :extrafuns ((tmp216 Real))
  :extrafuns ((tmp215 Real))
  :extrafuns ((tmp214 Real))
  :extrafuns ((tmp213 Real))
  :extrafuns ((tmp212 Real))
  :extrafuns ((tmp211 Real))
  :extrafuns ((tmp210 Real))
  :extrafuns ((tmp209 Real))
  :extrafuns ((tmp208 Real))
  :extrafuns ((tmp207 Real))
  :extrafuns ((tmp206 Real))
  :extrafuns ((tmp205 Real))
  :extrafuns ((tmp204 Real))
  :extrafuns ((tmp203 Real))
  :extrafuns ((tmp202 Real))
  :extrafuns ((tmp201 Real))
  :extrafuns ((tmp200 Real))
  :extrafuns ((tmp199 Real))
  :extrafuns ((tmp198 Real))
  :extrafuns ((tmp197 Real))
  :extrafuns ((tmp196 Real))
  :extrafuns ((tmp195 Real))
  :extrafuns ((tmp194 Real))
  :extrafuns ((tmp193 Real))
  :extrafuns ((tmp192 Real))
  :extrafuns ((tmp191 Real))
  :extrafuns ((tmp190 Real))
  :extrafuns ((tmp189 Real))
  :extrafuns ((tmp188 Real))
  :extrafuns ((tmp187 Real))
  :extrafuns ((tmp186 Real))
  :extrafuns ((tmp185 Real))
  :extrafuns ((tmp184 Real))
  :extrafuns ((tmp183 Real))
  :extrafuns ((tmp182 Real))
  :extrafuns ((tmp181 Real))
  :extrafuns ((tmp180 Real))
  :extrafuns ((tmp179 Real))
  :extrafuns ((tmp178 Real))
  :extrafuns ((tmp177 Real))
  :extrafuns ((tmp176 Real))
  :extrafuns ((tmp175 Real))
  :extrafuns ((tmp174 Real))
  :extrafuns ((tmp173 Real))
  :extrafuns ((tmp172 Real))
  :extrafuns ((tmp171 Real))
  :extrafuns ((tmp170 Real))
  :extrafuns ((tmp169 Real))
  :extrafuns ((tmp168 Real))
  :extrafuns ((tmp167 Real))
  :extrafuns ((tmp166 Real))
  :extrafuns ((tmp165 Real))
  :extrafuns ((tmp164 Real))
  :extrafuns ((tmp163 Real))
  :extrafuns ((tmp162 Real))
  :extrafuns ((tmp161 Real))
  :extrafuns ((tmp160 Real))
  :extrafuns ((tmp159 Real))
  :extrafuns ((tmp158 Real))
  :extrafuns ((tmp157 Real))
  :extrafuns ((tmp156 Real))
  :extrafuns ((tmp155 Real))
  :extrafuns ((tmp154 Real))
  :extrafuns ((tmp153 Real))
  :extrafuns ((tmp152 Real))
  :extrafuns ((tmp151 Real))
  :extrafuns ((tmp150 Real))
  :extrafuns ((tmp149 Real))
  :extrafuns ((tmp148 Real))
  :extrafuns ((tmp147 Real))
  :extrafuns ((tmp146 Real))
  :extrafuns ((tmp145 Real))
  :extrafuns ((tmp144 Real))
  :extrafuns ((tmp143 Real))
  :extrafuns ((tmp142 Real))
  :extrafuns ((tmp141 Real))
  :extrafuns ((tmp140 Real))
  :extrafuns ((tmp139 Real))
  :extrafuns ((tmp138 Real))
  :extrafuns ((tmp137 Real))
  :extrafuns ((tmp136 Real))
  :extrafuns ((tmp135 Real))
  :extrafuns ((tmp134 Real))
  :extrafuns ((tmp133 Real))
  :extrafuns ((tmp132 Real))
  :extrafuns ((tmp131 Real))
  :extrafuns ((tmp130 Real))
  :extrafuns ((tmp129 Real))
  :extrafuns ((tmp128 Real))
  :extrafuns ((tmp127 Real))
  :extrafuns ((tmp126 Real))
  :extrafuns ((tmp125 Real))
  :extrafuns ((tmp124 Real))
  :extrafuns ((tmp123 Real))
  :extrafuns ((tmp122 Real))
  :extrafuns ((tmp121 Real))
  :extrafuns ((tmp120 Real))
  :extrafuns ((tmp119 Real))
  :extrafuns ((tmp118 Real))
  :extrafuns ((tmp117 Real))
  :extrafuns ((tmp116 Real))
  :extrafuns ((tmp115 Real))
  :extrafuns ((tmp114 Real))
  :extrafuns ((tmp113 Real))
  :extrafuns ((tmp112 Real))
  :extrafuns ((tmp111 Real))
  :extrafuns ((tmp110 Real))
  :extrafuns ((tmp109 Real))
  :extrafuns ((tmp108 Real))
  :extrafuns ((tmp107 Real))
  :extrafuns ((tmp106 Real))
  :extrafuns ((tmp105 Real))
  :extrafuns ((tmp104 Real))
  :extrafuns ((tmp103 Real))
  :extrafuns ((tmp102 Real))
  :extrafuns ((tmp101 Real))
  :extrafuns ((tmp100 Real))
  :extrafuns ((tmp99 Real))
  :extrafuns ((tmp98 Real))
  :extrafuns ((tmp97 Real))
  :extrafuns ((tmp96 Real))
  :extrafuns ((tmp95 Real))
  :extrafuns ((tmp94 Real))
  :extrafuns ((tmp93 Real))
  :extrafuns ((tmp92 Real))
  :extrafuns ((tmp91 Real))
  :extrafuns ((tmp90 Real))
  :extrafuns ((tmp89 Real))
  :extrafuns ((tmp88 Real))
  :extrafuns ((tmp87 Real))
  :extrafuns ((tmp86 Real))
  :extrafuns ((tmp85 Real))
  :extrafuns ((tmp84 Real))
  :extrafuns ((tmp83 Real))
  :extrafuns ((tmp82 Real))
  :extrafuns ((tmp81 Real))
  :extrafuns ((tmp80 Real))
  :extrafuns ((tmp79 Real))
  :extrafuns ((tmp78 Real))
  :extrafuns ((tmp77 Real))
  :extrafuns ((tmp76 Real))
  :extrafuns ((tmp75 Real))
  :extrafuns ((tmp74 Real))
  :extrafuns ((tmp73 Real))
  :extrafuns ((tmp72 Real))
  :extrafuns ((tmp71 Real))
  :extrafuns ((tmp70 Real))
  :extrafuns ((tmp69 Real))
  :extrafuns ((tmp68 Real))
  :extrafuns ((tmp67 Real))
  :extrafuns ((tmp66 Real))
  :extrafuns ((tmp65 Real))
  :extrafuns ((tmp64 Real))
  :extrafuns ((tmp63 Real))
  :extrafuns ((tmp62 Real))
  :extrafuns ((tmp61 Real))
  :extrafuns ((tmp60 Real))
  :extrafuns ((tmp59 Real))
  :extrafuns ((tmp58 Real))
  :extrafuns ((tmp57 Real))
  :extrafuns ((tmp56 Real))
  :extrafuns ((tmp55 Real))
  :extrafuns ((tmp54 Real))
  :extrafuns ((tmp53 Real))
  :extrafuns ((tmp52 Real))
  :extrafuns ((tmp51 Real))
  :extrafuns ((tmp50 Real))
  :extrafuns ((tmp49 Real))
  :extrafuns ((tmp48 Real))
  :extrafuns ((tmp47 Real))
  :extrafuns ((tmp46 Real))
  :extrafuns ((tmp45 Real))
  :extrafuns ((tmp44 Real))
  :extrafuns ((tmp43 Real))
  :extrafuns ((tmp42 Real))
  :extrafuns ((tmp41 Real))
  :extrafuns ((tmp40 Real))
  :extrafuns ((tmp39 Real))
  :extrafuns ((tmp38 Real))
  :extrafuns ((tmp37 Real))
  :extrafuns ((tmp36 Real))
  :extrafuns ((tmp35 Real))
  :extrafuns ((tmp34 Real))
  :extrafuns ((tmp33 Real))
  :extrafuns ((tmp32 Real))
  :extrafuns ((tmp31 Real))
  :extrafuns ((tmp30 Real))
  :extrafuns ((tmp29 Real))
  :extrafuns ((tmp28 Real))
  :extrafuns ((tmp27 Real))
  :extrafuns ((tmp26 Real))
  :extrafuns ((tmp25 Real))
  :extrafuns ((tmp24 Real))
  :extrafuns ((tmp23 Real))
  :extrafuns ((tmp22 Real))
  :extrafuns ((tmp21 Real))
  :extrafuns ((tmp20 Real))
  :extrafuns ((tmp19 Real))
  :extrafuns ((tmp18 Real))
  :extrafuns ((tmp17 Real))
  :extrafuns ((tmp16 Real))
  :extrafuns ((tmp15 Real))
  :extrafuns ((tmp14 Real))
  :extrafuns ((tmp13 Real))
  :extrafuns ((tmp12 Real))
  :extrafuns ((tmp11 Real))
  :extrafuns ((tmp10 Real))
  :extrafuns ((tmp9 Real))
  :extrafuns ((tmp8 Real))
  :extrafuns ((tmp7 Real))
  :extrafuns ((tmp6 Real))
  :extrafuns ((tmp5 Real))
  :extrafuns ((tmp4 Real))
  :extrafuns ((tmp3 Real))
  :extrafuns ((tmp2 Real))
  :extrafuns ((tmp1 Real))
  :extrafuns ((x338 Real))
  :extrafuns ((x339 Real))
  :extrafuns ((x340 Real))
  :extrafuns ((x342 Real))
  :extrafuns ((x341 Real))
  :extrafuns ((x344 Real))
  :extrafuns ((x345 Real))
  :extrafuns ((x346 Real))
  :extrafuns ((x348 Real))
  :extrafuns ((x347 Real))
  :extrafuns ((x350 Real))
  :extrafuns ((x351 Real))
  :extrafuns ((x352 Real))
  :extrafuns ((x354 Real))
  :extrafuns ((x353 Real))
  :extrafuns ((x356 Real))
  :extrafuns ((x357 Real))
  :extrafuns ((x358 Real))
  :extrafuns ((x360 Real))
  :extrafuns ((x359 Real))
  :extrafuns ((x362 Real))
  :extrafuns ((x363 Real))
  :extrafuns ((x364 Real))
  :extrafuns ((x366 Real))
  :extrafuns ((x365 Real))
  :extrafuns ((x368 Real))
  :extrafuns ((x369 Real))
  :extrafuns ((x370 Real))
  :extrafuns ((x372 Real))
  :extrafuns ((x371 Real))
  :extrafuns ((x374 Real))
  :extrafuns ((x375 Real))
  :extrafuns ((x376 Real))
  :extrafuns ((x378 Real))
  :extrafuns ((x377 Real))
  :extrafuns ((x337 Real))
  :extrafuns ((x343 Real))
  :extrafuns ((x349 Real))
  :extrafuns ((x355 Real))
  :extrafuns ((x361 Real))
  :extrafuns ((x367 Real))
  :extrafuns ((x373 Real))
  :extrafuns ((x1 Real))
  :extrafuns ((x2 Real))
  :extrafuns ((x3 Real))
  :extrafuns ((x4 Real))
  :extrafuns ((x5 Real))
  :extrafuns ((x6 Real))
  :extrafuns ((x7 Real))
  :extrafuns ((x8 Real))
  :extrafuns ((x9 Real))
  :extrafuns ((x10 Real))
  :extrafuns ((x11 Real))
  :extrafuns ((x12 Real))
  :extrafuns ((x13 Real))
  :extrafuns ((x14 Real))
  :extrafuns ((x15 Real))
  :extrafuns ((x16 Real))
  :extrafuns ((x17 Real))
  :extrafuns ((x18 Real))
  :extrafuns ((x19 Real))
  :extrafuns ((x20 Real))
  :extrafuns ((x21 Real))
  :extrafuns ((x22 Real))
  :extrafuns ((x23 Real))
  :extrafuns ((x24 Real))
  :extrafuns ((x25 Real))
  :extrafuns ((x26 Real))
  :extrafuns ((x27 Real))
  :extrafuns ((x28 Real))
  :extrafuns ((x29 Real))
  :extrafuns ((x30 Real))
  :extrafuns ((x31 Real))
  :extrafuns ((x32 Real))
  :extrafuns ((x33 Real))
  :extrafuns ((x34 Real))
  :extrafuns ((x35 Real))
  :extrafuns ((x36 Real))
  :extrafuns ((x37 Real))
  :extrafuns ((x38 Real))
  :extrafuns ((x39 Real))
  :extrafuns ((x40 Real))
  :extrafuns ((x41 Real))
  :extrafuns ((x42 Real))
  :extrafuns ((x43 Real))
  :extrafuns ((x44 Real))
  :extrafuns ((x45 Real))
  :extrafuns ((x46 Real))
  :extrafuns ((x47 Real))
  :extrafuns ((x48 Real))
  :extrafuns ((x49 Real))
  :extrafuns ((x50 Real))
  :extrafuns ((x51 Real))
  :extrafuns ((x52 Real))
  :extrafuns ((x53 Real))
  :extrafuns ((x54 Real))
  :extrafuns ((x55 Real))
  :extrafuns ((x56 Real))
  :extrafuns ((x57 Real))
  :extrafuns ((x58 Real))
  :extrafuns ((x59 Real))
  :extrafuns ((x60 Real))
  :extrafuns ((x61 Real))
  :extrafuns ((x62 Real))
  :extrafuns ((x63 Real))
  :extrafuns ((x64 Real))
  :extrafuns ((x65 Real))
  :extrafuns ((x66 Real))
  :extrafuns ((x67 Real))
  :extrafuns ((x68 Real))
  :extrafuns ((x69 Real))
  :extrafuns ((x70 Real))
  :extrafuns ((x71 Real))
  :extrafuns ((x72 Real))
  :extrafuns ((x73 Real))
  :extrafuns ((x74 Real))
  :extrafuns ((x75 Real))
  :extrafuns ((x76 Real))
  :extrafuns ((x77 Real))
  :extrafuns ((x78 Real))
  :extrafuns ((x79 Real))
  :extrafuns ((x80 Real))
  :extrafuns ((x81 Real))
  :extrafuns ((x82 Real))
  :extrafuns ((x83 Real))
  :extrafuns ((x84 Real))
  :extrafuns ((x85 Real))
  :extrafuns ((x86 Real))
  :extrafuns ((x87 Real))
  :extrafuns ((x88 Real))
  :extrafuns ((x89 Real))
  :extrafuns ((x90 Real))
  :extrafuns ((x91 Real))
  :extrafuns ((x92 Real))
  :extrafuns ((x93 Real))
  :extrafuns ((x94 Real))
  :extrafuns ((x95 Real))
  :extrafuns ((x96 Real))
  :extrafuns ((x97 Real))
  :extrafuns ((x98 Real))
  :extrafuns ((x99 Real))
  :extrafuns ((x100 Real))
  :extrafuns ((x101 Real))
  :extrafuns ((x102 Real))
  :extrafuns ((x103 Real))
  :extrafuns ((x104 Real))
  :extrafuns ((x105 Real))
  :extrafuns ((x106 Real))
  :extrafuns ((x107 Real))
  :extrafuns ((x108 Real))
  :extrafuns ((x109 Real))
  :extrafuns ((x110 Real))
  :extrafuns ((x111 Real))
  :extrafuns ((x112 Real))
  :extrafuns ((x113 Real))
  :extrafuns ((x114 Real))
  :extrafuns ((x115 Real))
  :extrafuns ((x116 Real))
  :extrafuns ((x117 Real))
  :extrafuns ((x118 Real))
  :extrafuns ((x119 Real))
  :extrafuns ((x120 Real))
  :extrafuns ((x121 Real))
  :extrafuns ((x122 Real))
  :extrafuns ((x123 Real))
  :extrafuns ((x124 Real))
  :extrafuns ((x125 Real))
  :extrafuns ((x126 Real))
  :extrafuns ((x127 Real))
  :extrafuns ((x128 Real))
  :extrafuns ((x129 Real))
  :extrafuns ((x130 Real))
  :extrafuns ((x131 Real))
  :extrafuns ((x132 Real))
  :extrafuns ((x133 Real))
  :extrafuns ((x134 Real))
  :extrafuns ((x135 Real))
  :extrafuns ((x136 Real))
  :extrafuns ((x137 Real))
  :extrafuns ((x138 Real))
  :extrafuns ((x139 Real))
  :extrafuns ((x140 Real))
  :extrafuns ((x141 Real))
  :extrafuns ((x142 Real))
  :extrafuns ((x143 Real))
  :extrafuns ((x144 Real))
  :extrafuns ((x145 Real))
  :extrafuns ((x146 Real))
  :extrafuns ((x147 Real))
  :extrafuns ((x148 Real))
  :extrafuns ((x149 Real))
  :extrafuns ((x150 Real))
  :extrafuns ((x151 Real))
  :extrafuns ((x152 Real))
  :extrafuns ((x153 Real))
  :extrafuns ((x154 Real))
  :extrafuns ((x155 Real))
  :extrafuns ((x156 Real))
  :extrafuns ((x157 Real))
  :extrafuns ((x158 Real))
  :extrafuns ((x159 Real))
  :extrafuns ((x160 Real))
  :extrafuns ((x161 Real))
  :extrafuns ((x162 Real))
  :extrafuns ((x163 Real))
  :extrafuns ((x164 Real))
  :extrafuns ((x165 Real))
  :extrafuns ((x166 Real))
  :extrafuns ((x167 Real))
  :extrafuns ((x168 Real))
  :extrapreds ((x169))
  :extrapreds ((x170))
  :extrapreds ((x171))
  :extrapreds ((x172))
  :extrapreds ((x173))
  :extrapreds ((x174))
  :extrapreds ((x175))
  :extrapreds ((x176))
  :extrapreds ((x177))
  :extrapreds ((x178))
  :extrapreds ((x179))
  :extrapreds ((x180))
  :extrapreds ((x181))
  :extrapreds ((x182))
  :extrapreds ((x183))
  :extrapreds ((x184))
  :extrapreds ((x185))
  :extrapreds ((x186))
  :extrapreds ((x187))
  :extrapreds ((x188))
  :extrapreds ((x189))
  :extrapreds ((x190))
  :extrapreds ((x191))
  :extrapreds ((x192))
  :extrapreds ((x193))
  :extrapreds ((x194))
  :extrapreds ((x195))
  :extrapreds ((x196))
  :extrapreds ((x197))
  :extrapreds ((x198))
  :extrapreds ((x199))
  :extrapreds ((x200))
  :extrapreds ((x201))
  :extrapreds ((x202))
  :extrapreds ((x203))
  :extrapreds ((x204))
  :extrapreds ((x205))
  :extrapreds ((x206))
  :extrapreds ((x207))
  :extrapreds ((x208))
  :extrapreds ((x209))
  :extrapreds ((x210))
  :extrapreds ((x211))
  :extrapreds ((x212))
  :extrapreds ((x213))
  :extrapreds ((x214))
  :extrapreds ((x215))
  :extrapreds ((x216))
  :extrapreds ((x217))
  :extrapreds ((x218))
  :extrapreds ((x219))
  :extrapreds ((x220))
  :extrapreds ((x221))
  :extrapreds ((x222))
  :extrapreds ((x223))
  :extrapreds ((x224))
  :extrapreds ((x225))
  :extrapreds ((x226))
  :extrapreds ((x227))
  :extrapreds ((x228))
  :extrapreds ((x229))
  :extrapreds ((x230))
  :extrapreds ((x231))
  :extrapreds ((x232))
  :extrapreds ((x233))
  :extrapreds ((x234))
  :extrapreds ((x235))
  :extrapreds ((x236))
  :extrapreds ((x237))
  :extrapreds ((x238))
  :extrapreds ((x239))
  :extrapreds ((x240))
  :extrapreds ((x241))
  :extrapreds ((x242))
  :extrapreds ((x243))
  :extrapreds ((x244))
  :extrapreds ((x245))
  :extrapreds ((x246))
  :extrapreds ((x247))
  :extrapreds ((x248))
  :extrapreds ((x249))
  :extrapreds ((x250))
  :extrapreds ((x251))
  :extrapreds ((x252))
  :extrapreds ((x253))
  :extrapreds ((x254))
  :extrapreds ((x255))
  :extrapreds ((x256))
  :extrapreds ((x257))
  :extrapreds ((x258))
  :extrapreds ((x259))
  :extrapreds ((x260))
  :extrapreds ((x261))
  :extrapreds ((x262))
  :extrapreds ((x263))
  :extrapreds ((x264))
  :extrapreds ((x265))
  :extrapreds ((x266))
  :extrapreds ((x267))
  :extrapreds ((x268))
  :extrapreds ((x269))
  :extrapreds ((x270))
  :extrapreds ((x271))
  :extrapreds ((x272))
  :extrapreds ((x273))
  :extrapreds ((x274))
  :extrapreds ((x275))
  :extrapreds ((x276))
  :extrapreds ((x277))
  :extrapreds ((x278))
  :extrapreds ((x279))
  :extrapreds ((x280))
  :extrapreds ((x281))
  :extrapreds ((x282))
  :extrapreds ((x283))
  :extrapreds ((x284))
  :extrapreds ((x285))
  :extrapreds ((x286))
  :extrapreds ((x287))
  :extrapreds ((x288))
  :extrapreds ((x289))
  :extrapreds ((x290))
  :extrapreds ((x291))
  :extrapreds ((x292))
  :extrapreds ((x293))
  :extrapreds ((x294))
  :extrapreds ((x295))
  :extrapreds ((x296))
  :extrapreds ((x297))
  :extrapreds ((x298))
  :extrapreds ((x299))
  :extrapreds ((x300))
  :extrapreds ((x301))
  :extrapreds ((x302))
  :extrapreds ((x303))
  :extrapreds ((x304))
  :extrapreds ((x305))
  :extrapreds ((x306))
  :extrapreds ((x307))
  :extrapreds ((x308))
  :extrapreds ((x309))
  :extrapreds ((x310))
  :extrapreds ((x311))
  :extrapreds ((x312))
  :extrapreds ((x313))
  :extrapreds ((x314))
  :extrapreds ((x315))
  :extrapreds ((x316))
  :extrapreds ((x317))
  :extrapreds ((x318))
  :extrapreds ((x319))
  :extrapreds ((x320))
  :extrapreds ((x321))
  :extrapreds ((x322))
  :extrapreds ((x323))
  :extrapreds ((x324))
  :extrapreds ((x325))
  :extrapreds ((x326))
  :extrapreds ((x327))
  :extrapreds ((x328))
  :extrapreds ((x329))
  :extrapreds ((x330))
  :extrapreds ((x331))
  :extrapreds ((x332))
  :extrapreds ((x333))
  :extrapreds ((x334))
  :extrapreds ((x335))
  :extrapreds ((x336))

  :formula( and
    ( <= ( + ( + ( * 1 tmp348 ) 0 ) ( + ( * 1 tmp346 ) ( + ( * 1 tmp344 ) ( + ( * 1 tmp342 ) ( + ( * 1 tmp340 ) ( + ( * 1 tmp338 ) ( + ( * 1 tmp336 ) ( + ( * 1 tmp334 ) ( + ( * 1 tmp332 ) ( + ( * 1 tmp330 ) ( + ( * 1 tmp328 ) ( + ( * 1 tmp326 ) ( + ( * 1 tmp324 ) ( + ( * 1 tmp322 ) ( + ( * 1 tmp320 ) ( + ( * 1 tmp318 ) ( + ( * 1 tmp316 ) ( + ( * 1 tmp314 ) ( + ( * 1 tmp312 ) ( + ( * 1 tmp310 ) ( + ( * 1 tmp308 ) ( + ( * 1 tmp306 ) ( + ( * 1 tmp304 ) ( + ( * 1 tmp302 ) ( + ( * 1 tmp300 ) ( + ( * 1 tmp298 ) ( + ( * 1 tmp296 ) ( + ( * 1 tmp294 ) ( + ( * 1 tmp292 ) ( + ( * 1 tmp290 ) ( + ( * 1 tmp288 ) ( + ( * 1 tmp286 ) ( + ( * 1 tmp284 ) ( + ( * 1 tmp282 ) ( + ( * 1 tmp280 ) ( + ( * 1 tmp278 ) ( + ( * 1 tmp276 ) ( + ( * 1 tmp274 ) ( + ( * 1 tmp272 ) ( + ( * 1 tmp270 ) ( + ( * 1 tmp268 ) ( + ( * 1 tmp266 ) ( + ( * 1 tmp265 ) ( + ( * 1 tmp267 ) ( + ( * 1 tmp269 ) ( + ( * 1 tmp271 ) ( + ( * 1 tmp273 ) ( + ( * 1 tmp275 ) ( + ( * 1 tmp277 ) ( + ( * 1 tmp279 ) ( + ( * 1 tmp281 ) ( + ( * 1 tmp283 ) ( + ( * 1 tmp285 ) ( + ( * 1 tmp287 ) ( + ( * 1 tmp289 ) ( + ( * 1 tmp291 ) ( + ( * 1 tmp293 ) ( + ( * 1 tmp295 ) ( + ( * 1 tmp297 ) ( + ( * 1 tmp299 ) ( + ( * 1 tmp301 ) ( + ( * 1 tmp303 ) ( + ( * 1 tmp305 ) ( + ( * 1 tmp307 ) ( + ( * 1 tmp309 ) ( + ( * 1 tmp311 ) ( + ( * 1 tmp313 ) ( + ( * 1 tmp315 ) ( + ( * 1 tmp317 ) ( + ( * 1 tmp319 ) ( + ( * 1 tmp321 ) ( + ( * 1 tmp323 ) ( + ( * 1 tmp325 ) ( + ( * 1 tmp327 ) ( + ( * 1 tmp329 ) ( + ( * 1 tmp331 ) ( + ( * 1 tmp333 ) ( + ( * 1 tmp335 ) ( + ( * 1 tmp337 ) ( + ( * 1 tmp339 ) ( + ( * 1 tmp341 ) ( + ( * 1 tmp343 ) ( + ( * 1 tmp345 ) ( + ( * 1 tmp347 ) 0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - 20 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) 0 ) )
    ( >= ( + ( + ( * 1 tmp264 ) 0 ) ( + ( * (~ 1) x168 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp263 ) 0 ) ( + ( * (~ 1) x167 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp262 ) 0 ) ( + ( * (~ 1) x166 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp261 ) 0 ) ( + ( * (~ 1) x165 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp260 ) 0 ) ( + ( * (~ 1) x164 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp259 ) 0 ) ( + ( * (~ 1) x163 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp258 ) 0 ) ( + ( * (~ 1) x162 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp257 ) 0 ) ( + ( * (~ 1) x161 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp256 ) 0 ) ( + ( * (~ 1) x160 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp255 ) 0 ) ( + ( * (~ 1) x159 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp254 ) 0 ) ( + ( * (~ 1) x158 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp253 ) 0 ) ( + ( * (~ 1) x157 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp252 ) 0 ) ( + ( * (~ 1) x156 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp251 ) 0 ) ( + ( * (~ 1) x155 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp250 ) 0 ) ( + ( * (~ 1) x154 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp249 ) 0 ) ( + ( * (~ 1) x153 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp248 ) 0 ) ( + ( * (~ 1) x152 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp247 ) 0 ) ( + ( * (~ 1) x151 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp246 ) 0 ) ( + ( * (~ 1) x150 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp245 ) 0 ) ( + ( * (~ 1) x149 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp244 ) 0 ) ( + ( * (~ 1) x148 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp243 ) 0 ) ( + ( * (~ 1) x147 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp242 ) 0 ) ( + ( * (~ 1) x146 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp241 ) 0 ) ( + ( * (~ 1) x145 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp240 ) 0 ) ( + ( * (~ 1) x144 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp239 ) 0 ) ( + ( * (~ 1) x143 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp238 ) 0 ) ( + ( * (~ 1) x142 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp237 ) 0 ) ( + ( * (~ 1) x141 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp236 ) 0 ) ( + ( * (~ 1) x140 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp235 ) 0 ) ( + ( * (~ 1) x139 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp234 ) 0 ) ( + ( * (~ 1) x138 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp233 ) 0 ) ( + ( * (~ 1) x137 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp232 ) 0 ) ( + ( * (~ 1) x136 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp231 ) 0 ) ( + ( * (~ 1) x135 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp230 ) 0 ) ( + ( * (~ 1) x134 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp229 ) 0 ) ( + ( * (~ 1) x133 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp228 ) 0 ) ( + ( * (~ 1) x132 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp227 ) 0 ) ( + ( * (~ 1) x131 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp226 ) 0 ) ( + ( * (~ 1) x130 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp225 ) 0 ) ( + ( * (~ 1) x129 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp224 ) 0 ) ( + ( * (~ 1) x128 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp223 ) 0 ) ( + ( * (~ 1) x127 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp222 ) 0 ) ( + ( * (~ 1) x126 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp221 ) 0 ) ( + ( * (~ 1) x125 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp220 ) 0 ) ( + ( * (~ 1) x124 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp219 ) 0 ) ( + ( * (~ 1) x123 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp218 ) 0 ) ( + ( * (~ 1) x122 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp217 ) 0 ) ( + ( * (~ 1) x121 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp216 ) 0 ) ( + ( * (~ 1) x120 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp215 ) 0 ) ( + ( * (~ 1) x119 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp214 ) 0 ) ( + ( * (~ 1) x118 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp213 ) 0 ) ( + ( * (~ 1) x117 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp212 ) 0 ) ( + ( * (~ 1) x116 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp211 ) 0 ) ( + ( * (~ 1) x115 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp210 ) 0 ) ( + ( * (~ 1) x114 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp209 ) 0 ) ( + ( * (~ 1) x113 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp208 ) 0 ) ( + ( * (~ 1) x112 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp207 ) 0 ) ( + ( * (~ 1) x111 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp206 ) 0 ) ( + ( * (~ 1) x110 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp205 ) 0 ) ( + ( * (~ 1) x109 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp204 ) 0 ) ( + ( * (~ 1) x108 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp203 ) 0 ) ( + ( * (~ 1) x107 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp202 ) 0 ) ( + ( * (~ 1) x106 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp201 ) 0 ) ( + ( * (~ 1) x105 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp200 ) 0 ) ( + ( * (~ 1) x104 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp199 ) 0 ) ( + ( * (~ 1) x103 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp198 ) 0 ) ( + ( * (~ 1) x102 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp197 ) 0 ) ( + ( * (~ 1) x101 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp196 ) 0 ) ( + ( * (~ 1) x100 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp195 ) 0 ) ( + ( * (~ 1) x99 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp194 ) 0 ) ( + ( * (~ 1) x98 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp193 ) 0 ) ( + ( * (~ 1) x97 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp192 ) 0 ) ( + ( * (~ 1) x96 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp191 ) 0 ) ( + ( * (~ 1) x95 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp190 ) 0 ) ( + ( * (~ 1) x94 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp189 ) 0 ) ( + ( * (~ 1) x93 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp188 ) 0 ) ( + ( * (~ 1) x92 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp187 ) 0 ) ( + ( * (~ 1) x91 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp186 ) 0 ) ( + ( * (~ 1) x90 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp185 ) 0 ) ( + ( * (~ 1) x89 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp184 ) 0 ) ( + ( * (~ 1) x88 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp183 ) 0 ) ( + ( * (~ 1) x87 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp182 ) 0 ) ( + ( * (~ 1) x86 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp181 ) 0 ) ( + ( * (~ 1) x85 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp180 ) 0 ) ( + ( * (~ 1) x84 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp179 ) 0 ) ( + ( * (~ 1) x83 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp178 ) 0 ) ( + ( * (~ 1) x82 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp177 ) 0 ) ( + ( * (~ 1) x81 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp176 ) 0 ) ( + ( * (~ 1) x80 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp175 ) 0 ) ( + ( * (~ 1) x79 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp174 ) 0 ) ( + ( * (~ 1) x78 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp173 ) 0 ) ( + ( * (~ 1) x77 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp172 ) 0 ) ( + ( * (~ 1) x76 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp171 ) 0 ) ( + ( * (~ 1) x75 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp170 ) 0 ) ( + ( * (~ 1) x74 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp169 ) 0 ) ( + ( * (~ 1) x73 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp168 ) 0 ) ( + ( * (~ 1) x72 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp167 ) 0 ) ( + ( * (~ 1) x71 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp166 ) 0 ) ( + ( * (~ 1) x70 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp165 ) 0 ) ( + ( * (~ 1) x69 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp164 ) 0 ) ( + ( * (~ 1) x68 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp163 ) 0 ) ( + ( * (~ 1) x67 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp162 ) 0 ) ( + ( * (~ 1) x66 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp161 ) 0 ) ( + ( * (~ 1) x65 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp160 ) 0 ) ( + ( * (~ 1) x64 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp159 ) 0 ) ( + ( * (~ 1) x63 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp158 ) 0 ) ( + ( * (~ 1) x62 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp157 ) 0 ) ( + ( * (~ 1) x61 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp156 ) 0 ) ( + ( * (~ 1) x60 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp155 ) 0 ) ( + ( * (~ 1) x59 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp154 ) 0 ) ( + ( * (~ 1) x58 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp153 ) 0 ) ( + ( * (~ 1) x57 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp152 ) 0 ) ( + ( * (~ 1) x56 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp151 ) 0 ) ( + ( * (~ 1) x55 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp150 ) 0 ) ( + ( * (~ 1) x54 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp149 ) 0 ) ( + ( * (~ 1) x53 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp148 ) 0 ) ( + ( * (~ 1) x52 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp147 ) 0 ) ( + ( * (~ 1) x51 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp146 ) 0 ) ( + ( * (~ 1) x50 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp145 ) 0 ) ( + ( * (~ 1) x49 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp144 ) 0 ) ( + ( * (~ 1) x48 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp143 ) 0 ) ( + ( * (~ 1) x47 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp142 ) 0 ) ( + ( * (~ 1) x46 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp141 ) 0 ) ( + ( * (~ 1) x45 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp140 ) 0 ) ( + ( * (~ 1) x44 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp139 ) 0 ) ( + ( * (~ 1) x43 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp138 ) 0 ) ( + ( * (~ 1) x42 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp137 ) 0 ) ( + ( * (~ 1) x41 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp136 ) 0 ) ( + ( * (~ 1) x40 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp135 ) 0 ) ( + ( * (~ 1) x39 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp134 ) 0 ) ( + ( * (~ 1) x38 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp133 ) 0 ) ( + ( * (~ 1) x37 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp132 ) 0 ) ( + ( * (~ 1) x36 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp131 ) 0 ) ( + ( * (~ 1) x35 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp130 ) 0 ) ( + ( * (~ 1) x34 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp129 ) 0 ) ( + ( * (~ 1) x33 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp128 ) 0 ) ( + ( * (~ 1) x32 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp127 ) 0 ) ( + ( * (~ 1) x31 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp126 ) 0 ) ( + ( * (~ 1) x30 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp125 ) 0 ) ( + ( * (~ 1) x29 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp124 ) 0 ) ( + ( * (~ 1) x28 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp123 ) 0 ) ( + ( * (~ 1) x27 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp122 ) 0 ) ( + ( * (~ 1) x26 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp121 ) 0 ) ( + ( * (~ 1) x25 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp120 ) 0 ) ( + ( * (~ 1) x24 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp119 ) 0 ) ( + ( * (~ 1) x23 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp118 ) 0 ) ( + ( * (~ 1) x22 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp117 ) 0 ) ( + ( * (~ 1) x21 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp116 ) 0 ) ( + ( * (~ 1) x20 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp115 ) 0 ) ( + ( * (~ 1) x19 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp114 ) 0 ) ( + ( * (~ 1) x18 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp113 ) 0 ) ( + ( * (~ 1) x17 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp112 ) 0 ) ( + ( * (~ 1) x16 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp111 ) 0 ) ( + ( * (~ 1) x15 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp110 ) 0 ) ( + ( * (~ 1) x14 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp109 ) 0 ) ( + ( * (~ 1) x13 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp108 ) 0 ) ( + ( * (~ 1) x12 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp107 ) 0 ) ( + ( * (~ 1) x11 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp106 ) 0 ) ( + ( * (~ 1) x10 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp105 ) 0 ) ( + ( * (~ 1) x9 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp104 ) 0 ) ( + ( * (~ 1) x8 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp103 ) 0 ) ( + ( * (~ 1) x7 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp102 ) 0 ) ( + ( * (~ 1) x6 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp101 ) 0 ) ( + ( * (~ 1) x5 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp100 ) 0 ) ( + ( * (~ 1) x4 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp99 ) 0 ) ( + ( * (~ 1) x3 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp98 ) 0 ) ( + ( * (~ 1) x2 ) 0 ) ) 0 )
    ( >= ( + ( + ( * 1 tmp97 ) 0 ) ( + ( * (~ 1) x1 ) 0 ) ) 0 )
    ( <= ( + ( + ( * 1 tmp96 ) 0 ) ( + ( * 1 tmp94 ) ( + ( * 1 x24 ) ( + ( * 1 x48 ) ( + ( * 1 x72 ) ( + ( * 1 x96 ) ( + ( * 1 x120 ) ( + ( * 1 x144 ) ( + ( * 1 x168 ) ( + ( * 1 tmp93 ) ( + ( * 1 tmp95 ) 0 ) ) ) ) ) ) ) ) ) ) ) 1 )
    ( <= ( + ( + ( * 1 tmp92 ) 0 ) ( + ( * 1 tmp90 ) ( + ( * 1 x23 ) ( + ( * 1 x47 ) ( + ( * 1 x71 ) ( + ( * 1 x95 ) ( + ( * 1 x119 ) ( + ( * 1 x143 ) ( + ( * 1 x167 ) ( + ( * 1 tmp89 ) ( + ( * 1 tmp91 ) 0 ) ) ) ) ) ) ) ) ) ) ) 1 )
    ( <= ( + ( + ( * 1 tmp88 ) 0 ) ( + ( * 1 tmp86 ) ( + ( * 1 x22 ) ( + ( * 1 x46 ) ( + ( * 1 x70 ) ( + ( * 1 x94 ) ( + ( * 1 x118 ) ( + ( * 1 x142 ) ( + ( * 1 x166 ) ( + ( * 1 tmp85 ) ( + ( * 1 tmp87 ) 0 ) ) ) ) ) ) ) ) ) ) ) 1 )
    ( <= ( + ( + ( * 1 tmp84 ) 0 ) ( + ( * 1 tmp82 ) ( + ( * 1 x21 ) ( + ( * 1 x45 ) ( + ( * 1 x69 ) ( + ( * 1 x93 ) ( + ( * 1 x117 ) ( + ( * 1 x141 ) ( + ( * 1 x165 ) ( + ( * 1 tmp81 ) ( + ( * 1 tmp83 ) 0 ) ) ) ) ) ) ) ) ) ) ) 1 )
    ( <= ( + ( + ( * 1 tmp80 ) 0 ) ( + ( * 1 tmp78 ) ( + ( * 1 x20 ) ( + ( * 1 x44 ) ( + ( * 1 x68 ) ( + ( * 1 x92 ) ( + ( * 1 x116 ) ( + ( * 1 x140 ) ( + ( * 1 x164 ) ( + ( * 1 tmp77 ) ( + ( * 1 tmp79 ) 0 ) ) ) ) ) ) ) ) ) ) ) 1 )
    ( <= ( + ( + ( * 1 tmp76 ) 0 ) ( + ( * 1 tmp74 ) ( + ( * 1 x19 ) ( + ( * 1 x43 ) ( + ( * 1 x67 ) ( + ( * 1 x91 ) ( + ( * 1 x115 ) ( + ( * 1 x139 ) ( + ( * 1 x163 ) ( + ( * 1 tmp73 ) ( + ( * 1 tmp75 ) 0 ) ) ) ) ) ) ) ) ) ) ) 1 )
    ( <= ( + ( + ( * 1 tmp72 ) 0 ) ( + ( * 1 tmp70 ) ( + ( * 1 x18 ) ( + ( * 1 x42 ) ( + ( * 1 x66 ) ( + ( * 1 x90 ) ( + ( * 1 x114 ) ( + ( * 1 x138 ) ( + ( * 1 x162 ) ( + ( * 1 tmp69 ) ( + ( * 1 tmp71 ) 0 ) ) ) ) ) ) ) ) ) ) ) 1 )
    ( <= ( + ( + ( * 1 tmp68 ) 0 ) ( + ( * 1 tmp66 ) ( + ( * 1 x17 ) ( + ( * 1 x41 ) ( + ( * 1 x65 ) ( + ( * 1 x89 ) ( + ( * 1 x113 ) ( + ( * 1 x137 ) ( + ( * 1 x161 ) ( + ( * 1 tmp65 ) ( + ( * 1 tmp67 ) 0 ) ) ) ) ) ) ) ) ) ) ) 1 )
    ( <= ( + ( + ( * 1 tmp64 ) 0 ) ( + ( * 1 tmp62 ) ( + ( * 1 x16 ) ( + ( * 1 x40 ) ( + ( * 1 x64 ) ( + ( * 1 x88 ) ( + ( * 1 x112 ) ( + ( * 1 x136 ) ( + ( * 1 x160 ) ( + ( * 1 tmp61 ) ( + ( * 1 tmp63 ) 0 ) ) ) ) ) ) ) ) ) ) ) 1 )
    ( <= ( + ( + ( * 1 tmp60 ) 0 ) ( + ( * 1 tmp58 ) ( + ( * 1 x15 ) ( + ( * 1 x39 ) ( + ( * 1 x63 ) ( + ( * 1 x87 ) ( + ( * 1 x111 ) ( + ( * 1 x135 ) ( + ( * 1 x159 ) ( + ( * 1 tmp57 ) ( + ( * 1 tmp59 ) 0 ) ) ) ) ) ) ) ) ) ) ) 1 )
    ( <= ( + ( + ( * 1 tmp56 ) 0 ) ( + ( * 1 tmp54 ) ( + ( * 1 x14 ) ( + ( * 1 x38 ) ( + ( * 1 x62 ) ( + ( * 1 x86 ) ( + ( * 1 x110 ) ( + ( * 1 x134 ) ( + ( * 1 x158 ) ( + ( * 1 tmp53 ) ( + ( * 1 tmp55 ) 0 ) ) ) ) ) ) ) ) ) ) ) 1 )
    ( <= ( + ( + ( * 1 tmp52 ) 0 ) ( + ( * 1 tmp50 ) ( + ( * 1 x13 ) ( + ( * 1 x37 ) ( + ( * 1 x61 ) ( + ( * 1 x85 ) ( + ( * 1 x109 ) ( + ( * 1 x133 ) ( + ( * 1 x157 ) ( + ( * 1 tmp49 ) ( + ( * 1 tmp51 ) 0 ) ) ) ) ) ) ) ) ) ) ) 1 )
    ( <= ( + ( + ( * 1 tmp48 ) 0 ) ( + ( * 1 tmp46 ) ( + ( * 1 x12 ) ( + ( * 1 x36 ) ( + ( * 1 x60 ) ( + ( * 1 x84 ) ( + ( * 1 x108 ) ( + ( * 1 x132 ) ( + ( * 1 x156 ) ( + ( * 1 tmp45 ) ( + ( * 1 tmp47 ) 0 ) ) ) ) ) ) ) ) ) ) ) 1 )
    ( <= ( + ( + ( * 1 tmp44 ) 0 ) ( + ( * 1 tmp42 ) ( + ( * 1 x11 ) ( + ( * 1 x35 ) ( + ( * 1 x59 ) ( + ( * 1 x83 ) ( + ( * 1 x107 ) ( + ( * 1 x131 ) ( + ( * 1 x155 ) ( + ( * 1 tmp41 ) ( + ( * 1 tmp43 ) 0 ) ) ) ) ) ) ) ) ) ) ) 1 )
    ( <= ( + ( + ( * 1 tmp40 ) 0 ) ( + ( * 1 tmp38 ) ( + ( * 1 x10 ) ( + ( * 1 x34 ) ( + ( * 1 x58 ) ( + ( * 1 x82 ) ( + ( * 1 x106 ) ( + ( * 1 x130 ) ( + ( * 1 x154 ) ( + ( * 1 tmp37 ) ( + ( * 1 tmp39 ) 0 ) ) ) ) ) ) ) ) ) ) ) 1 )
    ( <= ( + ( + ( * 1 tmp36 ) 0 ) ( + ( * 1 tmp34 ) ( + ( * 1 x9 ) ( + ( * 1 x33 ) ( + ( * 1 x57 ) ( + ( * 1 x81 ) ( + ( * 1 x105 ) ( + ( * 1 x129 ) ( + ( * 1 x153 ) ( + ( * 1 tmp33 ) ( + ( * 1 tmp35 ) 0 ) ) ) ) ) ) ) ) ) ) ) 1 )
    ( <= ( + ( + ( * 1 tmp32 ) 0 ) ( + ( * 1 tmp30 ) ( + ( * 1 x8 ) ( + ( * 1 x32 ) ( + ( * 1 x56 ) ( + ( * 1 x80 ) ( + ( * 1 x104 ) ( + ( * 1 x128 ) ( + ( * 1 x152 ) ( + ( * 1 tmp29 ) ( + ( * 1 tmp31 ) 0 ) ) ) ) ) ) ) ) ) ) ) 1 )
    ( <= ( + ( + ( * 1 tmp28 ) 0 ) ( + ( * 1 tmp26 ) ( + ( * 1 x7 ) ( + ( * 1 x31 ) ( + ( * 1 x55 ) ( + ( * 1 x79 ) ( + ( * 1 x103 ) ( + ( * 1 x127 ) ( + ( * 1 x151 ) ( + ( * 1 tmp25 ) ( + ( * 1 tmp27 ) 0 ) ) ) ) ) ) ) ) ) ) ) 1 )
    ( <= ( + ( + ( * 1 tmp24 ) 0 ) ( + ( * 1 tmp22 ) ( + ( * 1 x6 ) ( + ( * 1 x30 ) ( + ( * 1 x54 ) ( + ( * 1 x78 ) ( + ( * 1 x102 ) ( + ( * 1 x126 ) ( + ( * 1 x150 ) ( + ( * 1 tmp21 ) ( + ( * 1 tmp23 ) 0 ) ) ) ) ) ) ) ) ) ) ) 1 )
    ( <= ( + ( + ( * 1 tmp20 ) 0 ) ( + ( * 1 tmp18 ) ( + ( * 1 x5 ) ( + ( * 1 x29 ) ( + ( * 1 x53 ) ( + ( * 1 x77 ) ( + ( * 1 x101 ) ( + ( * 1 x125 ) ( + ( * 1 x149 ) ( + ( * 1 tmp17 ) ( + ( * 1 tmp19 ) 0 ) ) ) ) ) ) ) ) ) ) ) 1 )
    ( <= ( + ( + ( * 1 tmp16 ) 0 ) ( + ( * 1 tmp14 ) ( + ( * 1 x4 ) ( + ( * 1 x28 ) ( + ( * 1 x52 ) ( + ( * 1 x76 ) ( + ( * 1 x100 ) ( + ( * 1 x124 ) ( + ( * 1 x148 ) ( + ( * 1 tmp13 ) ( + ( * 1 tmp15 ) 0 ) ) ) ) ) ) ) ) ) ) ) 1 )
    ( <= ( + ( + ( * 1 tmp12 ) 0 ) ( + ( * 1 tmp10 ) ( + ( * 1 x3 ) ( + ( * 1 x27 ) ( + ( * 1 x51 ) ( + ( * 1 x75 ) ( + ( * 1 x99 ) ( + ( * 1 x123 ) ( + ( * 1 x147 ) ( + ( * 1 tmp9 ) ( + ( * 1 tmp11 ) 0 ) ) ) ) ) ) ) ) ) ) ) 1 )
    ( <= ( + ( + ( * 1 tmp8 ) 0 ) ( + ( * 1 tmp6 ) ( + ( * 1 x2 ) ( + ( * 1 x26 ) ( + ( * 1 x50 ) ( + ( * 1 x74 ) ( + ( * 1 x98 ) ( + ( * 1 x122 ) ( + ( * 1 x146 ) ( + ( * 1 tmp5 ) ( + ( * 1 tmp7 ) 0 ) ) ) ) ) ) ) ) ) ) ) 1 )
    ( <= ( + ( + ( * 1 tmp4 ) 0 ) ( + ( * 1 tmp2 ) ( + ( * 1 x1 ) ( + ( * 1 x25 ) ( + ( * 1 x49 ) ( + ( * 1 x73 ) ( + ( * 1 x97 ) ( + ( * 1 x121 ) ( + ( * 1 x145 ) ( + ( * 1 tmp1 ) ( + ( * 1 tmp3 ) 0 ) ) ) ) ) ) ) ) ) ) ) 1 )
    ( = ( + ( + ( + ( + ( + 0 ( * 500 x145 ) ) ( * 500 x151 ) ) ( * 400 x157 ) ) ( * 600 x163 ) ) ( * (~ 1) x373 ) ) (~ 300) )
    ( = ( + ( + ( + ( + ( + 0 ( * 300 x121 ) ) ( * 500 x127 ) ) ( * 600 x133 ) ) ( * 600 x139 ) ) ( * (~ 1) x367 ) ) 400 )
    ( = ( + ( + ( + ( + ( + 0 ( * 200 x97 ) ) ( * 200 x103 ) ) ( * 100 x109 ) ) ( * 200 x115 ) ) ( * (~ 1) x361 ) ) (~ 500) )
    ( = ( + ( + ( + ( + ( + 0 ( * 300 x73 ) ) ( * 400 x79 ) ) ( * 200 x85 ) ) ( * 300 x91 ) ) ( * (~ 1) x355 ) ) (~ 500) )
    ( = ( + ( + ( + ( + ( + 0 ( * 400 x49 ) ) ( * 400 x55 ) ) ( * 300 x61 ) ) ( * 400 x67 ) ) ( * (~ 1) x349 ) ) (~ 400) )
    ( = ( + ( + ( + ( + ( + 0 ( * 400 x25 ) ) ( * 200 x31 ) ) ( * 100 x37 ) ) ( * 400 x43 ) ) ( * (~ 1) x343 ) ) (~ 400) )
    ( = ( + ( + ( + ( + ( + 0 ( * 200 x1 ) ) ( * 300 x7 ) ) ( * 400 x13 ) ) ( * 300 x19 ) ) ( * (~ 1) x337 ) ) 200 )
    ( = ( + ( + ( + ( + ( + ( + 0 ( * 500 x150 ) ) ( * 500 x156 ) ) ( * 400 x162 ) ) ( * 600 x168 ) ) ( * 1 x377 ) ) ( * (~ 1) x378 ) ) 0 )
    ( = ( + ( + ( + ( + ( + ( + 0 ( * 500 x149 ) ) ( * 500 x155 ) ) ( * 400 x161 ) ) ( * 600 x167 ) ) ( * 1 x376 ) ) ( * (~ 1) x377 ) ) 0 )
    ( = ( + ( + ( + ( + ( + ( + 0 ( * 500 x148 ) ) ( * 500 x154 ) ) ( * 400 x160 ) ) ( * 600 x166 ) ) ( * 1 x375 ) ) ( * (~ 1) x376 ) ) 0 )
    ( = ( + ( + ( + ( + ( + ( + 0 ( * 500 x147 ) ) ( * 500 x153 ) ) ( * 400 x159 ) ) ( * 600 x165 ) ) ( * 1 x374 ) ) ( * (~ 1) x375 ) ) 500 )
    ( = ( + ( + ( + ( + ( + ( + 0 ( * 500 x146 ) ) ( * 500 x152 ) ) ( * 400 x158 ) ) ( * 600 x164 ) ) ( * 1 x373 ) ) ( * (~ 1) x374 ) ) 300 )
    ( = ( + ( + ( + ( + ( + ( + 0 ( * 300 x126 ) ) ( * 500 x132 ) ) ( * 600 x138 ) ) ( * 600 x144 ) ) ( * 1 x371 ) ) ( * (~ 1) x372 ) ) 0 )
    ( = ( + ( + ( + ( + ( + ( + 0 ( * 300 x125 ) ) ( * 500 x131 ) ) ( * 600 x137 ) ) ( * 600 x143 ) ) ( * 1 x370 ) ) ( * (~ 1) x371 ) ) 0 )
    ( = ( + ( + ( + ( + ( + ( + 0 ( * 300 x124 ) ) ( * 500 x130 ) ) ( * 600 x136 ) ) ( * 600 x142 ) ) ( * 1 x369 ) ) ( * (~ 1) x370 ) ) 0 )
    ( = ( + ( + ( + ( + ( + ( + 0 ( * 300 x123 ) ) ( * 500 x129 ) ) ( * 600 x135 ) ) ( * 600 x141 ) ) ( * 1 x368 ) ) ( * (~ 1) x369 ) ) 0 )
    ( = ( + ( + ( + ( + ( + ( + 0 ( * 300 x122 ) ) ( * 500 x128 ) ) ( * 600 x134 ) ) ( * 600 x140 ) ) ( * 1 x367 ) ) ( * (~ 1) x368 ) ) 200 )
    ( = ( + ( + ( + ( + ( + ( + 0 ( * 200 x102 ) ) ( * 200 x108 ) ) ( * 100 x114 ) ) ( * 200 x120 ) ) ( * 1 x365 ) ) ( * (~ 1) x366 ) ) 100 )
    ( = ( + ( + ( + ( + ( + ( + 0 ( * 200 x101 ) ) ( * 200 x107 ) ) ( * 100 x113 ) ) ( * 200 x119 ) ) ( * 1 x364 ) ) ( * (~ 1) x365 ) ) 0 )
    ( = ( + ( + ( + ( + ( + ( + 0 ( * 200 x100 ) ) ( * 200 x106 ) ) ( * 100 x112 ) ) ( * 200 x118 ) ) ( * 1 x363 ) ) ( * (~ 1) x364 ) ) 500 )
    ( = ( + ( + ( + ( + ( + ( + 0 ( * 200 x99 ) ) ( * 200 x105 ) ) ( * 100 x111 ) ) ( * 200 x117 ) ) ( * 1 x362 ) ) ( * (~ 1) x363 ) ) 0 )
    ( = ( + ( + ( + ( + ( + ( + 0 ( * 200 x98 ) ) ( * 200 x104 ) ) ( * 100 x110 ) ) ( * 200 x116 ) ) ( * 1 x361 ) ) ( * (~ 1) x362 ) ) 0 )
    ( = ( + ( + ( + ( + ( + ( + 0 ( * 300 x78 ) ) ( * 400 x84 ) ) ( * 200 x90 ) ) ( * 300 x96 ) ) ( * 1 x359 ) ) ( * (~ 1) x360 ) ) 800 )
    ( = ( + ( + ( + ( + ( + ( + 0 ( * 300 x77 ) ) ( * 400 x83 ) ) ( * 200 x89 ) ) ( * 300 x95 ) ) ( * 1 x358 ) ) ( * (~ 1) x359 ) ) 300 )
    ( = ( + ( + ( + ( + ( + ( + 0 ( * 300 x76 ) ) ( * 400 x82 ) ) ( * 200 x88 ) ) ( * 300 x94 ) ) ( * 1 x357 ) ) ( * (~ 1) x358 ) ) 0 )
    ( = ( + ( + ( + ( + ( + ( + 0 ( * 300 x75 ) ) ( * 400 x81 ) ) ( * 200 x87 ) ) ( * 300 x93 ) ) ( * 1 x356 ) ) ( * (~ 1) x357 ) ) 0 )
    ( = ( + ( + ( + ( + ( + ( + 0 ( * 300 x74 ) ) ( * 400 x80 ) ) ( * 200 x86 ) ) ( * 300 x92 ) ) ( * 1 x355 ) ) ( * (~ 1) x356 ) ) 0 )
    ( = ( + ( + ( + ( + ( + ( + 0 ( * 400 x54 ) ) ( * 400 x60 ) ) ( * 300 x66 ) ) ( * 400 x72 ) ) ( * 1 x353 ) ) ( * (~ 1) x354 ) ) 0 )
    ( = ( + ( + ( + ( + ( + ( + 0 ( * 400 x53 ) ) ( * 400 x59 ) ) ( * 300 x65 ) ) ( * 400 x71 ) ) ( * 1 x352 ) ) ( * (~ 1) x353 ) ) 600 )
    ( = ( + ( + ( + ( + ( + ( + 0 ( * 400 x52 ) ) ( * 400 x58 ) ) ( * 300 x64 ) ) ( * 400 x70 ) ) ( * 1 x351 ) ) ( * (~ 1) x352 ) ) 300 )
    ( = ( + ( + ( + ( + ( + ( + 0 ( * 400 x51 ) ) ( * 400 x57 ) ) ( * 300 x63 ) ) ( * 400 x69 ) ) ( * 1 x350 ) ) ( * (~ 1) x351 ) ) 0 )
    ( = ( + ( + ( + ( + ( + ( + 0 ( * 400 x50 ) ) ( * 400 x56 ) ) ( * 300 x62 ) ) ( * 400 x68 ) ) ( * 1 x349 ) ) ( * (~ 1) x350 ) ) 0 )
    ( = ( + ( + ( + ( + ( + ( + 0 ( * 400 x30 ) ) ( * 200 x36 ) ) ( * 100 x42 ) ) ( * 400 x48 ) ) ( * 1 x347 ) ) ( * (~ 1) x348 ) ) 0 )
    ( = ( + ( + ( + ( + ( + ( + 0 ( * 400 x29 ) ) ( * 200 x35 ) ) ( * 100 x41 ) ) ( * 400 x47 ) ) ( * 1 x346 ) ) ( * (~ 1) x347 ) ) 400 )
    ( = ( + ( + ( + ( + ( + ( + 0 ( * 400 x28 ) ) ( * 200 x34 ) ) ( * 100 x40 ) ) ( * 400 x46 ) ) ( * 1 x345 ) ) ( * (~ 1) x346 ) ) 400 )
    ( = ( + ( + ( + ( + ( + ( + 0 ( * 400 x27 ) ) ( * 200 x33 ) ) ( * 100 x39 ) ) ( * 400 x45 ) ) ( * 1 x344 ) ) ( * (~ 1) x345 ) ) 200 )
    ( = ( + ( + ( + ( + ( + ( + 0 ( * 400 x26 ) ) ( * 200 x32 ) ) ( * 100 x38 ) ) ( * 400 x44 ) ) ( * 1 x343 ) ) ( * (~ 1) x344 ) ) 300 )
    ( = ( + ( + ( + ( + ( + ( + 0 ( * 200 x6 ) ) ( * 300 x12 ) ) ( * 400 x18 ) ) ( * 300 x24 ) ) ( * 1 x341 ) ) ( * (~ 1) x342 ) ) 600 )
    ( = ( + ( + ( + ( + ( + ( + 0 ( * 200 x5 ) ) ( * 300 x11 ) ) ( * 400 x17 ) ) ( * 300 x23 ) ) ( * 1 x340 ) ) ( * (~ 1) x341 ) ) 0 )
    ( = ( + ( + ( + ( + ( + ( + 0 ( * 200 x4 ) ) ( * 300 x10 ) ) ( * 400 x16 ) ) ( * 300 x22 ) ) ( * 1 x339 ) ) ( * (~ 1) x340 ) ) 0 )
    ( = ( + ( + ( + ( + ( + ( + 0 ( * 200 x3 ) ) ( * 300 x9 ) ) ( * 400 x15 ) ) ( * 300 x21 ) ) ( * 1 x338 ) ) ( * (~ 1) x339 ) ) 300 )
    ( = ( + ( + ( + ( + ( + ( + 0 ( * 200 x2 ) ) ( * 300 x8 ) ) ( * 400 x14 ) ) ( * 300 x20 ) ) ( * 1 x337 ) ) ( * (~ 1) x338 ) ) 300 )
    ( <= x168 1 )
    ( >= x168 0 )
    ( <= x167 1 )
    ( >= x167 0 )
    ( <= x166 1 )
    ( >= x166 0 )
    ( <= x165 1 )
    ( >= x165 0 )
    ( <= x164 1 )
    ( >= x164 0 )
    ( <= x163 1 )
    ( >= x163 0 )
    ( <= x162 1 )
    ( >= x162 0 )
    ( <= x161 1 )
    ( >= x161 0 )
    ( <= x160 1 )
    ( >= x160 0 )
    ( <= x159 1 )
    ( >= x159 0 )
    ( <= x158 1 )
    ( >= x158 0 )
    ( <= x157 1 )
    ( >= x157 0 )
    ( <= x156 1 )
    ( >= x156 0 )
    ( <= x155 1 )
    ( >= x155 0 )
    ( <= x154 1 )
    ( >= x154 0 )
    ( <= x153 1 )
    ( >= x153 0 )
    ( <= x152 1 )
    ( >= x152 0 )
    ( <= x151 1 )
    ( >= x151 0 )
    ( <= x150 1 )
    ( >= x150 0 )
    ( <= x149 1 )
    ( >= x149 0 )
    ( <= x148 1 )
    ( >= x148 0 )
    ( <= x147 1 )
    ( >= x147 0 )
    ( <= x146 1 )
    ( >= x146 0 )
    ( <= x145 1 )
    ( >= x145 0 )
    ( <= x144 1 )
    ( >= x144 0 )
    ( <= x143 1 )
    ( >= x143 0 )
    ( <= x142 1 )
    ( >= x142 0 )
    ( <= x141 1 )
    ( >= x141 0 )
    ( <= x140 1 )
    ( >= x140 0 )
    ( <= x139 1 )
    ( >= x139 0 )
    ( <= x138 1 )
    ( >= x138 0 )
    ( <= x137 1 )
    ( >= x137 0 )
    ( <= x136 1 )
    ( >= x136 0 )
    ( <= x135 1 )
    ( >= x135 0 )
    ( <= x134 1 )
    ( >= x134 0 )
    ( <= x133 1 )
    ( >= x133 0 )
    ( <= x132 1 )
    ( >= x132 0 )
    ( <= x131 1 )
    ( >= x131 0 )
    ( <= x130 1 )
    ( >= x130 0 )
    ( <= x129 1 )
    ( >= x129 0 )
    ( <= x128 1 )
    ( >= x128 0 )
    ( <= x127 1 )
    ( >= x127 0 )
    ( <= x126 1 )
    ( >= x126 0 )
    ( <= x125 1 )
    ( >= x125 0 )
    ( <= x124 1 )
    ( >= x124 0 )
    ( <= x123 1 )
    ( >= x123 0 )
    ( <= x122 1 )
    ( >= x122 0 )
    ( <= x121 1 )
    ( >= x121 0 )
    ( <= x120 1 )
    ( >= x120 0 )
    ( <= x119 1 )
    ( >= x119 0 )
    ( <= x118 1 )
    ( >= x118 0 )
    ( <= x117 1 )
    ( >= x117 0 )
    ( <= x116 1 )
    ( >= x116 0 )
    ( <= x115 1 )
    ( >= x115 0 )
    ( <= x114 1 )
    ( >= x114 0 )
    ( <= x113 1 )
    ( >= x113 0 )
    ( <= x112 1 )
    ( >= x112 0 )
    ( <= x111 1 )
    ( >= x111 0 )
    ( <= x110 1 )
    ( >= x110 0 )
    ( <= x109 1 )
    ( >= x109 0 )
    ( <= x108 1 )
    ( >= x108 0 )
    ( <= x107 1 )
    ( >= x107 0 )
    ( <= x106 1 )
    ( >= x106 0 )
    ( <= x105 1 )
    ( >= x105 0 )
    ( <= x104 1 )
    ( >= x104 0 )
    ( <= x103 1 )
    ( >= x103 0 )
    ( <= x102 1 )
    ( >= x102 0 )
    ( <= x101 1 )
    ( >= x101 0 )
    ( <= x100 1 )
    ( >= x100 0 )
    ( <= x99 1 )
    ( >= x99 0 )
    ( <= x98 1 )
    ( >= x98 0 )
    ( <= x97 1 )
    ( >= x97 0 )
    ( <= x96 1 )
    ( >= x96 0 )
    ( <= x95 1 )
    ( >= x95 0 )
    ( <= x94 1 )
    ( >= x94 0 )
    ( <= x93 1 )
    ( >= x93 0 )
    ( <= x92 1 )
    ( >= x92 0 )
    ( <= x91 1 )
    ( >= x91 0 )
    ( <= x90 1 )
    ( >= x90 0 )
    ( <= x89 1 )
    ( >= x89 0 )
    ( <= x88 1 )
    ( >= x88 0 )
    ( <= x87 1 )
    ( >= x87 0 )
    ( <= x86 1 )
    ( >= x86 0 )
    ( <= x85 1 )
    ( >= x85 0 )
    ( <= x84 1 )
    ( >= x84 0 )
    ( <= x83 1 )
    ( >= x83 0 )
    ( <= x82 1 )
    ( >= x82 0 )
    ( <= x81 1 )
    ( >= x81 0 )
    ( <= x80 1 )
    ( >= x80 0 )
    ( <= x79 1 )
    ( >= x79 0 )
    ( <= x78 1 )
    ( >= x78 0 )
    ( <= x77 1 )
    ( >= x77 0 )
    ( <= x76 1 )
    ( >= x76 0 )
    ( <= x75 1 )
    ( >= x75 0 )
    ( <= x74 1 )
    ( >= x74 0 )
    ( <= x73 1 )
    ( >= x73 0 )
    ( <= x72 1 )
    ( >= x72 0 )
    ( <= x71 1 )
    ( >= x71 0 )
    ( <= x70 1 )
    ( >= x70 0 )
    ( <= x69 1 )
    ( >= x69 0 )
    ( <= x68 1 )
    ( >= x68 0 )
    ( <= x67 1 )
    ( >= x67 0 )
    ( <= x66 1 )
    ( >= x66 0 )
    ( <= x65 1 )
    ( >= x65 0 )
    ( <= x64 1 )
    ( >= x64 0 )
    ( <= x63 1 )
    ( >= x63 0 )
    ( <= x62 1 )
    ( >= x62 0 )
    ( <= x61 1 )
    ( >= x61 0 )
    ( <= x60 1 )
    ( >= x60 0 )
    ( <= x59 1 )
    ( >= x59 0 )
    ( <= x58 1 )
    ( >= x58 0 )
    ( <= x57 1 )
    ( >= x57 0 )
    ( <= x56 1 )
    ( >= x56 0 )
    ( <= x55 1 )
    ( >= x55 0 )
    ( <= x54 1 )
    ( >= x54 0 )
    ( <= x53 1 )
    ( >= x53 0 )
    ( <= x52 1 )
    ( >= x52 0 )
    ( <= x51 1 )
    ( >= x51 0 )
    ( <= x50 1 )
    ( >= x50 0 )
    ( <= x49 1 )
    ( >= x49 0 )
    ( <= x48 1 )
    ( >= x48 0 )
    ( <= x47 1 )
    ( >= x47 0 )
    ( <= x46 1 )
    ( >= x46 0 )
    ( <= x45 1 )
    ( >= x45 0 )
    ( <= x44 1 )
    ( >= x44 0 )
    ( <= x43 1 )
    ( >= x43 0 )
    ( <= x42 1 )
    ( >= x42 0 )
    ( <= x41 1 )
    ( >= x41 0 )
    ( <= x40 1 )
    ( >= x40 0 )
    ( <= x39 1 )
    ( >= x39 0 )
    ( <= x38 1 )
    ( >= x38 0 )
    ( <= x37 1 )
    ( >= x37 0 )
    ( <= x36 1 )
    ( >= x36 0 )
    ( <= x35 1 )
    ( >= x35 0 )
    ( <= x34 1 )
    ( >= x34 0 )
    ( <= x33 1 )
    ( >= x33 0 )
    ( <= x32 1 )
    ( >= x32 0 )
    ( <= x31 1 )
    ( >= x31 0 )
    ( <= x30 1 )
    ( >= x30 0 )
    ( <= x29 1 )
    ( >= x29 0 )
    ( <= x28 1 )
    ( >= x28 0 )
    ( <= x27 1 )
    ( >= x27 0 )
    ( <= x26 1 )
    ( >= x26 0 )
    ( <= x25 1 )
    ( >= x25 0 )
    ( <= x24 1 )
    ( >= x24 0 )
    ( <= x23 1 )
    ( >= x23 0 )
    ( <= x22 1 )
    ( >= x22 0 )
    ( <= x21 1 )
    ( >= x21 0 )
    ( <= x20 1 )
    ( >= x20 0 )
    ( <= x19 1 )
    ( >= x19 0 )
    ( <= x18 1 )
    ( >= x18 0 )
    ( <= x17 1 )
    ( >= x17 0 )
    ( <= x16 1 )
    ( >= x16 0 )
    ( <= x15 1 )
    ( >= x15 0 )
    ( <= x14 1 )
    ( >= x14 0 )
    ( <= x13 1 )
    ( >= x13 0 )
    ( <= x12 1 )
    ( >= x12 0 )
    ( <= x11 1 )
    ( >= x11 0 )
    ( <= x10 1 )
    ( >= x10 0 )
    ( <= x9 1 )
    ( >= x9 0 )
    ( <= x8 1 )
    ( >= x8 0 )
    ( <= x7 1 )
    ( >= x7 0 )
    ( <= x6 1 )
    ( >= x6 0 )
    ( <= x5 1 )
    ( >= x5 0 )
    ( <= x4 1 )
    ( >= x4 0 )
    ( <= x3 1 )
    ( >= x3 0 )
    ( <= x2 1 )
    ( >= x2 0 )
    ( <= x1 1 )
    ( >= x1 0 )
    ( <= x373 300 )
    ( >= x373 200 )
    ( <= x367 400 )
    ( >= x367 300 )
    ( <= x361 500 )
    ( >= x361 200 )
    ( <= x355 500 )
    ( >= x355 400 )
    ( <= x349 400 )
    ( >= x349 300 )
    ( <= x343 400 )
    ( >= x343 200 )
    ( <= x337 300 )
    ( >= x337 100 )
    ( <= x377 300 )
    ( >= x377 200 )
    ( <= x378 300 )
    ( >= x378 200 )
    ( <= x376 300 )
    ( >= x376 200 )
    ( <= x375 300 )
    ( >= x375 200 )
    ( <= x374 300 )
    ( >= x374 200 )
    ( <= x371 400 )
    ( >= x371 300 )
    ( <= x372 400 )
    ( >= x372 300 )
    ( <= x370 400 )
    ( >= x370 300 )
    ( <= x369 400 )
    ( >= x369 300 )
    ( <= x368 400 )
    ( >= x368 300 )
    ( <= x365 500 )
    ( >= x365 200 )
    ( <= x366 500 )
    ( >= x366 200 )
    ( <= x364 500 )
    ( >= x364 200 )
    ( <= x363 500 )
    ( >= x363 200 )
    ( <= x362 500 )
    ( >= x362 200 )
    ( <= x359 500 )
    ( >= x359 400 )
    ( <= x360 500 )
    ( >= x360 400 )
    ( <= x358 500 )
    ( >= x358 400 )
    ( <= x357 500 )
    ( >= x357 400 )
    ( <= x356 500 )
    ( >= x356 400 )
    ( <= x353 400 )
    ( >= x353 300 )
    ( <= x354 400 )
    ( >= x354 300 )
    ( <= x352 400 )
    ( >= x352 300 )
    ( <= x351 400 )
    ( >= x351 300 )
    ( <= x350 400 )
    ( >= x350 300 )
    ( <= x347 400 )
    ( >= x347 200 )
    ( <= x348 400 )
    ( >= x348 200 )
    ( <= x346 400 )
    ( >= x346 200 )
    ( <= x345 400 )
    ( >= x345 200 )
    ( <= x344 400 )
    ( >= x344 200 )
    ( <= x341 300 )
    ( >= x341 100 )
    ( <= x342 300 )
    ( >= x342 100 )
    ( <= x340 300 )
    ( >= x340 100 )
    ( <= x339 300 )
    ( >= x339 100 )
    ( <= x338 300 )
    ( >= x338 100 )
    ( implies ( and ( not x254 ) ( and ( not x253 ) true ) ) ( = tmp348 0 ) )
    ( implies ( and ( not x254 ) ( and x253 true ) ) ( = tmp348 1 ) )
    ( implies ( and x254 ( and ( not x253 ) true ) ) ( = tmp348 1 ) )
    ( implies ( and x254 ( and x253 true ) ) ( = tmp348 2 ) )
    ( implies ( and ( not x251 ) ( and ( not x252 ) true ) ) ( = tmp347 0 ) )
    ( implies ( and ( not x251 ) ( and x252 true ) ) ( = tmp347 ( / 5 10 ) ) )
    ( implies ( and x251 ( and ( not x252 ) true ) ) ( = tmp347 ( / 5 10 ) ) )
    ( implies ( and x251 ( and x252 true ) ) ( = tmp347 ( + ( / 5 10 ) ( / 5 10 ) ) ) )
    ( implies ( and ( not x256 ) ( and ( not x255 ) true ) ) ( = tmp346 0 ) )
    ( implies ( and ( not x256 ) ( and x255 true ) ) ( = tmp346 1 ) )
    ( implies ( and x256 ( and ( not x255 ) true ) ) ( = tmp346 1 ) )
    ( implies ( and x256 ( and x255 true ) ) ( = tmp346 2 ) )
    ( implies ( and ( not x249 ) ( and ( not x250 ) true ) ) ( = tmp345 0 ) )
    ( implies ( and ( not x249 ) ( and x250 true ) ) ( = tmp345 ( / 5 10 ) ) )
    ( implies ( and x249 ( and ( not x250 ) true ) ) ( = tmp345 ( / 5 10 ) ) )
    ( implies ( and x249 ( and x250 true ) ) ( = tmp345 ( + ( / 5 10 ) ( / 5 10 ) ) ) )
    ( implies ( and ( not x258 ) ( and ( not x257 ) true ) ) ( = tmp344 0 ) )
    ( implies ( and ( not x258 ) ( and x257 true ) ) ( = tmp344 1 ) )
    ( implies ( and x258 ( and ( not x257 ) true ) ) ( = tmp344 1 ) )
    ( implies ( and x258 ( and x257 true ) ) ( = tmp344 2 ) )
    ( implies ( and ( not x247 ) ( and ( not x248 ) true ) ) ( = tmp343 0 ) )
    ( implies ( and ( not x247 ) ( and x248 true ) ) ( = tmp343 ( / 5 10 ) ) )
    ( implies ( and x247 ( and ( not x248 ) true ) ) ( = tmp343 ( / 5 10 ) ) )
    ( implies ( and x247 ( and x248 true ) ) ( = tmp343 ( + ( / 5 10 ) ( / 5 10 ) ) ) )
    ( implies ( and ( not x260 ) ( and ( not x259 ) true ) ) ( = tmp342 0 ) )
    ( implies ( and ( not x260 ) ( and x259 true ) ) ( = tmp342 ( + 1 ( / 25 100 ) ) ) )
    ( implies ( and x260 ( and ( not x259 ) true ) ) ( = tmp342 ( + 1 ( / 25 100 ) ) ) )
    ( implies ( and x260 ( and x259 true ) ) ( = tmp342 ( + ( + 1 ( / 25 100 ) ) ( + 1 ( / 25 100 ) ) ) ) )
    ( implies ( and ( not x245 ) ( and ( not x246 ) true ) ) ( = tmp341 0 ) )
    ( implies ( and ( not x245 ) ( and x246 true ) ) ( = tmp341 ( / 25 100 ) ) )
    ( implies ( and x245 ( and ( not x246 ) true ) ) ( = tmp341 ( / 25 100 ) ) )
    ( implies ( and x245 ( and x246 true ) ) ( = tmp341 ( + ( / 25 100 ) ( / 25 100 ) ) ) )
    ( implies ( and ( not x262 ) ( and ( not x261 ) true ) ) ( = tmp340 0 ) )
    ( implies ( and ( not x262 ) ( and x261 true ) ) ( = tmp340 ( + 1 ( / 25 100 ) ) ) )
    ( implies ( and x262 ( and ( not x261 ) true ) ) ( = tmp340 ( + 1 ( / 25 100 ) ) ) )
    ( implies ( and x262 ( and x261 true ) ) ( = tmp340 ( + ( + 1 ( / 25 100 ) ) ( + 1 ( / 25 100 ) ) ) ) )
    ( implies ( and ( not x243 ) ( and ( not x244 ) true ) ) ( = tmp339 0 ) )
    ( implies ( and ( not x243 ) ( and x244 true ) ) ( = tmp339 ( / 25 100 ) ) )
    ( implies ( and x243 ( and ( not x244 ) true ) ) ( = tmp339 ( / 25 100 ) ) )
    ( implies ( and x243 ( and x244 true ) ) ( = tmp339 ( + ( / 25 100 ) ( / 25 100 ) ) ) )
    ( implies ( and ( not x264 ) ( and ( not x263 ) true ) ) ( = tmp338 0 ) )
    ( implies ( and ( not x264 ) ( and x263 true ) ) ( = tmp338 ( + 1 ( / 25 100 ) ) ) )
    ( implies ( and x264 ( and ( not x263 ) true ) ) ( = tmp338 ( + 1 ( / 25 100 ) ) ) )
    ( implies ( and x264 ( and x263 true ) ) ( = tmp338 ( + ( + 1 ( / 25 100 ) ) ( + 1 ( / 25 100 ) ) ) ) )
    ( implies ( and ( not x241 ) ( and ( not x242 ) true ) ) ( = tmp337 0 ) )
    ( implies ( and ( not x241 ) ( and x242 true ) ) ( = tmp337 ( / 25 100 ) ) )
    ( implies ( and x241 ( and ( not x242 ) true ) ) ( = tmp337 ( / 25 100 ) ) )
    ( implies ( and x241 ( and x242 true ) ) ( = tmp337 ( + ( / 25 100 ) ( / 25 100 ) ) ) )
    ( implies ( and ( not x266 ) ( and ( not x265 ) true ) ) ( = tmp336 0 ) )
    ( implies ( and ( not x266 ) ( and x265 true ) ) ( = tmp336 ( / 25 100 ) ) )
    ( implies ( and x266 ( and ( not x265 ) true ) ) ( = tmp336 ( / 25 100 ) ) )
    ( implies ( and x266 ( and x265 true ) ) ( = tmp336 ( + ( / 25 100 ) ( / 25 100 ) ) ) )
    ( implies ( and ( not x239 ) ( and ( not x240 ) true ) ) ( = tmp335 0 ) )
    ( implies ( and ( not x239 ) ( and x240 true ) ) ( = tmp335 ( + 1 ( / 25 100 ) ) ) )
    ( implies ( and x239 ( and ( not x240 ) true ) ) ( = tmp335 ( + 1 ( / 25 100 ) ) ) )
    ( implies ( and x239 ( and x240 true ) ) ( = tmp335 ( + ( + 1 ( / 25 100 ) ) ( + 1 ( / 25 100 ) ) ) ) )
    ( implies ( and ( not x268 ) ( and ( not x267 ) true ) ) ( = tmp334 0 ) )
    ( implies ( and ( not x268 ) ( and x267 true ) ) ( = tmp334 ( / 25 100 ) ) )
    ( implies ( and x268 ( and ( not x267 ) true ) ) ( = tmp334 ( / 25 100 ) ) )
    ( implies ( and x268 ( and x267 true ) ) ( = tmp334 ( + ( / 25 100 ) ( / 25 100 ) ) ) )
    ( implies ( and ( not x237 ) ( and ( not x238 ) true ) ) ( = tmp333 0 ) )
    ( implies ( and ( not x237 ) ( and x238 true ) ) ( = tmp333 ( + 1 ( / 25 100 ) ) ) )
    ( implies ( and x237 ( and ( not x238 ) true ) ) ( = tmp333 ( + 1 ( / 25 100 ) ) ) )
    ( implies ( and x237 ( and x238 true ) ) ( = tmp333 ( + ( + 1 ( / 25 100 ) ) ( + 1 ( / 25 100 ) ) ) ) )
    ( implies ( and ( not x270 ) ( and ( not x269 ) true ) ) ( = tmp332 0 ) )
    ( implies ( and ( not x270 ) ( and x269 true ) ) ( = tmp332 ( / 25 100 ) ) )
    ( implies ( and x270 ( and ( not x269 ) true ) ) ( = tmp332 ( / 25 100 ) ) )
    ( implies ( and x270 ( and x269 true ) ) ( = tmp332 ( + ( / 25 100 ) ( / 25 100 ) ) ) )
    ( implies ( and ( not x235 ) ( and ( not x236 ) true ) ) ( = tmp331 0 ) )
    ( implies ( and ( not x235 ) ( and x236 true ) ) ( = tmp331 ( + 1 ( / 25 100 ) ) ) )
    ( implies ( and x235 ( and ( not x236 ) true ) ) ( = tmp331 ( + 1 ( / 25 100 ) ) ) )
    ( implies ( and x235 ( and x236 true ) ) ( = tmp331 ( + ( + 1 ( / 25 100 ) ) ( + 1 ( / 25 100 ) ) ) ) )
    ( implies ( and ( not x272 ) ( and ( not x271 ) true ) ) ( = tmp330 0 ) )
    ( implies ( and ( not x272 ) ( and x271 true ) ) ( = tmp330 ( / 5 10 ) ) )
    ( implies ( and x272 ( and ( not x271 ) true ) ) ( = tmp330 ( / 5 10 ) ) )
    ( implies ( and x272 ( and x271 true ) ) ( = tmp330 ( + ( / 5 10 ) ( / 5 10 ) ) ) )
    ( implies ( and ( not x233 ) ( and ( not x234 ) true ) ) ( = tmp329 0 ) )
    ( implies ( and ( not x233 ) ( and x234 true ) ) ( = tmp329 1 ) )
    ( implies ( and x233 ( and ( not x234 ) true ) ) ( = tmp329 1 ) )
    ( implies ( and x233 ( and x234 true ) ) ( = tmp329 2 ) )
    ( implies ( and ( not x274 ) ( and ( not x273 ) true ) ) ( = tmp328 0 ) )
    ( implies ( and ( not x274 ) ( and x273 true ) ) ( = tmp328 ( / 5 10 ) ) )
    ( implies ( and x274 ( and ( not x273 ) true ) ) ( = tmp328 ( / 5 10 ) ) )
    ( implies ( and x274 ( and x273 true ) ) ( = tmp328 ( + ( / 5 10 ) ( / 5 10 ) ) ) )
    ( implies ( and ( not x231 ) ( and ( not x232 ) true ) ) ( = tmp327 0 ) )
    ( implies ( and ( not x231 ) ( and x232 true ) ) ( = tmp327 1 ) )
    ( implies ( and x231 ( and ( not x232 ) true ) ) ( = tmp327 1 ) )
    ( implies ( and x231 ( and x232 true ) ) ( = tmp327 2 ) )
    ( implies ( and ( not x276 ) ( and ( not x275 ) true ) ) ( = tmp326 0 ) )
    ( implies ( and ( not x276 ) ( and x275 true ) ) ( = tmp326 ( / 5 10 ) ) )
    ( implies ( and x276 ( and ( not x275 ) true ) ) ( = tmp326 ( / 5 10 ) ) )
    ( implies ( and x276 ( and x275 true ) ) ( = tmp326 ( + ( / 5 10 ) ( / 5 10 ) ) ) )
    ( implies ( and ( not x229 ) ( and ( not x230 ) true ) ) ( = tmp325 0 ) )
    ( implies ( and ( not x229 ) ( and x230 true ) ) ( = tmp325 1 ) )
    ( implies ( and x229 ( and ( not x230 ) true ) ) ( = tmp325 1 ) )
    ( implies ( and x229 ( and x230 true ) ) ( = tmp325 2 ) )
    ( implies ( and ( not x278 ) ( and ( not x277 ) true ) ) ( = tmp324 0 ) )
    ( implies ( and ( not x278 ) ( and x277 true ) ) ( = tmp324 1 ) )
    ( implies ( and x278 ( and ( not x277 ) true ) ) ( = tmp324 1 ) )
    ( implies ( and x278 ( and x277 true ) ) ( = tmp324 2 ) )
    ( implies ( and ( not x227 ) ( and ( not x228 ) true ) ) ( = tmp323 0 ) )
    ( implies ( and ( not x227 ) ( and x228 true ) ) ( = tmp323 ( / 5 10 ) ) )
    ( implies ( and x227 ( and ( not x228 ) true ) ) ( = tmp323 ( / 5 10 ) ) )
    ( implies ( and x227 ( and x228 true ) ) ( = tmp323 ( + ( / 5 10 ) ( / 5 10 ) ) ) )
    ( implies ( and ( not x280 ) ( and ( not x279 ) true ) ) ( = tmp322 0 ) )
    ( implies ( and ( not x280 ) ( and x279 true ) ) ( = tmp322 1 ) )
    ( implies ( and x280 ( and ( not x279 ) true ) ) ( = tmp322 1 ) )
    ( implies ( and x280 ( and x279 true ) ) ( = tmp322 2 ) )
    ( implies ( and ( not x225 ) ( and ( not x226 ) true ) ) ( = tmp321 0 ) )
    ( implies ( and ( not x225 ) ( and x226 true ) ) ( = tmp321 ( / 5 10 ) ) )
    ( implies ( and x225 ( and ( not x226 ) true ) ) ( = tmp321 ( / 5 10 ) ) )
    ( implies ( and x225 ( and x226 true ) ) ( = tmp321 ( + ( / 5 10 ) ( / 5 10 ) ) ) )
    ( implies ( and ( not x282 ) ( and ( not x281 ) true ) ) ( = tmp320 0 ) )
    ( implies ( and ( not x282 ) ( and x281 true ) ) ( = tmp320 1 ) )
    ( implies ( and x282 ( and ( not x281 ) true ) ) ( = tmp320 1 ) )
    ( implies ( and x282 ( and x281 true ) ) ( = tmp320 2 ) )
    ( implies ( and ( not x223 ) ( and ( not x224 ) true ) ) ( = tmp319 0 ) )
    ( implies ( and ( not x223 ) ( and x224 true ) ) ( = tmp319 ( / 5 10 ) ) )
    ( implies ( and x223 ( and ( not x224 ) true ) ) ( = tmp319 ( / 5 10 ) ) )
    ( implies ( and x223 ( and x224 true ) ) ( = tmp319 ( + ( / 5 10 ) ( / 5 10 ) ) ) )
    ( implies ( and ( not x284 ) ( and ( not x283 ) true ) ) ( = tmp318 0 ) )
    ( implies ( and ( not x284 ) ( and x283 true ) ) ( = tmp318 ( + 1 ( / 25 100 ) ) ) )
    ( implies ( and x284 ( and ( not x283 ) true ) ) ( = tmp318 ( + 1 ( / 25 100 ) ) ) )
    ( implies ( and x284 ( and x283 true ) ) ( = tmp318 ( + ( + 1 ( / 25 100 ) ) ( + 1 ( / 25 100 ) ) ) ) )
    ( implies ( and ( not x221 ) ( and ( not x222 ) true ) ) ( = tmp317 0 ) )
    ( implies ( and ( not x221 ) ( and x222 true ) ) ( = tmp317 ( / 25 100 ) ) )
    ( implies ( and x221 ( and ( not x222 ) true ) ) ( = tmp317 ( / 25 100 ) ) )
    ( implies ( and x221 ( and x222 true ) ) ( = tmp317 ( + ( / 25 100 ) ( / 25 100 ) ) ) )
    ( implies ( and ( not x286 ) ( and ( not x285 ) true ) ) ( = tmp316 0 ) )
    ( implies ( and ( not x286 ) ( and x285 true ) ) ( = tmp316 ( + 1 ( / 25 100 ) ) ) )
    ( implies ( and x286 ( and ( not x285 ) true ) ) ( = tmp316 ( + 1 ( / 25 100 ) ) ) )
    ( implies ( and x286 ( and x285 true ) ) ( = tmp316 ( + ( + 1 ( / 25 100 ) ) ( + 1 ( / 25 100 ) ) ) ) )
    ( implies ( and ( not x219 ) ( and ( not x220 ) true ) ) ( = tmp315 0 ) )
    ( implies ( and ( not x219 ) ( and x220 true ) ) ( = tmp315 ( / 25 100 ) ) )
    ( implies ( and x219 ( and ( not x220 ) true ) ) ( = tmp315 ( / 25 100 ) ) )
    ( implies ( and x219 ( and x220 true ) ) ( = tmp315 ( + ( / 25 100 ) ( / 25 100 ) ) ) )
    ( implies ( and ( not x288 ) ( and ( not x287 ) true ) ) ( = tmp314 0 ) )
    ( implies ( and ( not x288 ) ( and x287 true ) ) ( = tmp314 ( + 1 ( / 25 100 ) ) ) )
    ( implies ( and x288 ( and ( not x287 ) true ) ) ( = tmp314 ( + 1 ( / 25 100 ) ) ) )
    ( implies ( and x288 ( and x287 true ) ) ( = tmp314 ( + ( + 1 ( / 25 100 ) ) ( + 1 ( / 25 100 ) ) ) ) )
    ( implies ( and ( not x217 ) ( and ( not x218 ) true ) ) ( = tmp313 0 ) )
    ( implies ( and ( not x217 ) ( and x218 true ) ) ( = tmp313 ( / 25 100 ) ) )
    ( implies ( and x217 ( and ( not x218 ) true ) ) ( = tmp313 ( / 25 100 ) ) )
    ( implies ( and x217 ( and x218 true ) ) ( = tmp313 ( + ( / 25 100 ) ( / 25 100 ) ) ) )
    ( implies ( and ( not x290 ) ( and ( not x289 ) true ) ) ( = tmp312 0 ) )
    ( implies ( and ( not x290 ) ( and x289 true ) ) ( = tmp312 ( / 25 100 ) ) )
    ( implies ( and x290 ( and ( not x289 ) true ) ) ( = tmp312 ( / 25 100 ) ) )
    ( implies ( and x290 ( and x289 true ) ) ( = tmp312 ( + ( / 25 100 ) ( / 25 100 ) ) ) )
    ( implies ( and ( not x215 ) ( and ( not x216 ) true ) ) ( = tmp311 0 ) )
    ( implies ( and ( not x215 ) ( and x216 true ) ) ( = tmp311 ( + 1 ( / 25 100 ) ) ) )
    ( implies ( and x215 ( and ( not x216 ) true ) ) ( = tmp311 ( + 1 ( / 25 100 ) ) ) )
    ( implies ( and x215 ( and x216 true ) ) ( = tmp311 ( + ( + 1 ( / 25 100 ) ) ( + 1 ( / 25 100 ) ) ) ) )
    ( implies ( and ( not x292 ) ( and ( not x291 ) true ) ) ( = tmp310 0 ) )
    ( implies ( and ( not x292 ) ( and x291 true ) ) ( = tmp310 ( / 25 100 ) ) )
    ( implies ( and x292 ( and ( not x291 ) true ) ) ( = tmp310 ( / 25 100 ) ) )
    ( implies ( and x292 ( and x291 true ) ) ( = tmp310 ( + ( / 25 100 ) ( / 25 100 ) ) ) )
    ( implies ( and ( not x213 ) ( and ( not x214 ) true ) ) ( = tmp309 0 ) )
    ( implies ( and ( not x213 ) ( and x214 true ) ) ( = tmp309 ( + 1 ( / 25 100 ) ) ) )
    ( implies ( and x213 ( and ( not x214 ) true ) ) ( = tmp309 ( + 1 ( / 25 100 ) ) ) )
    ( implies ( and x213 ( and x214 true ) ) ( = tmp309 ( + ( + 1 ( / 25 100 ) ) ( + 1 ( / 25 100 ) ) ) ) )
    ( implies ( and ( not x294 ) ( and ( not x293 ) true ) ) ( = tmp308 0 ) )
    ( implies ( and ( not x294 ) ( and x293 true ) ) ( = tmp308 ( / 25 100 ) ) )
    ( implies ( and x294 ( and ( not x293 ) true ) ) ( = tmp308 ( / 25 100 ) ) )
    ( implies ( and x294 ( and x293 true ) ) ( = tmp308 ( + ( / 25 100 ) ( / 25 100 ) ) ) )
    ( implies ( and ( not x211 ) ( and ( not x212 ) true ) ) ( = tmp307 0 ) )
    ( implies ( and ( not x211 ) ( and x212 true ) ) ( = tmp307 ( + 1 ( / 25 100 ) ) ) )
    ( implies ( and x211 ( and ( not x212 ) true ) ) ( = tmp307 ( + 1 ( / 25 100 ) ) ) )
    ( implies ( and x211 ( and x212 true ) ) ( = tmp307 ( + ( + 1 ( / 25 100 ) ) ( + 1 ( / 25 100 ) ) ) ) )
    ( implies ( and ( not x296 ) ( and ( not x295 ) true ) ) ( = tmp306 0 ) )
    ( implies ( and ( not x296 ) ( and x295 true ) ) ( = tmp306 ( / 5 10 ) ) )
    ( implies ( and x296 ( and ( not x295 ) true ) ) ( = tmp306 ( / 5 10 ) ) )
    ( implies ( and x296 ( and x295 true ) ) ( = tmp306 ( + ( / 5 10 ) ( / 5 10 ) ) ) )
    ( implies ( and ( not x209 ) ( and ( not x210 ) true ) ) ( = tmp305 0 ) )
    ( implies ( and ( not x209 ) ( and x210 true ) ) ( = tmp305 1 ) )
    ( implies ( and x209 ( and ( not x210 ) true ) ) ( = tmp305 1 ) )
    ( implies ( and x209 ( and x210 true ) ) ( = tmp305 2 ) )
    ( implies ( and ( not x298 ) ( and ( not x297 ) true ) ) ( = tmp304 0 ) )
    ( implies ( and ( not x298 ) ( and x297 true ) ) ( = tmp304 ( / 5 10 ) ) )
    ( implies ( and x298 ( and ( not x297 ) true ) ) ( = tmp304 ( / 5 10 ) ) )
    ( implies ( and x298 ( and x297 true ) ) ( = tmp304 ( + ( / 5 10 ) ( / 5 10 ) ) ) )
    ( implies ( and ( not x207 ) ( and ( not x208 ) true ) ) ( = tmp303 0 ) )
    ( implies ( and ( not x207 ) ( and x208 true ) ) ( = tmp303 1 ) )
    ( implies ( and x207 ( and ( not x208 ) true ) ) ( = tmp303 1 ) )
    ( implies ( and x207 ( and x208 true ) ) ( = tmp303 2 ) )
    ( implies ( and ( not x300 ) ( and ( not x299 ) true ) ) ( = tmp302 0 ) )
    ( implies ( and ( not x300 ) ( and x299 true ) ) ( = tmp302 ( / 5 10 ) ) )
    ( implies ( and x300 ( and ( not x299 ) true ) ) ( = tmp302 ( / 5 10 ) ) )
    ( implies ( and x300 ( and x299 true ) ) ( = tmp302 ( + ( / 5 10 ) ( / 5 10 ) ) ) )
    ( implies ( and ( not x205 ) ( and ( not x206 ) true ) ) ( = tmp301 0 ) )
    ( implies ( and ( not x205 ) ( and x206 true ) ) ( = tmp301 1 ) )
    ( implies ( and x205 ( and ( not x206 ) true ) ) ( = tmp301 1 ) )
    ( implies ( and x205 ( and x206 true ) ) ( = tmp301 2 ) )
    ( implies ( and ( not x302 ) ( and ( not x301 ) true ) ) ( = tmp300 0 ) )
    ( implies ( and ( not x302 ) ( and x301 true ) ) ( = tmp300 1 ) )
    ( implies ( and x302 ( and ( not x301 ) true ) ) ( = tmp300 1 ) )
    ( implies ( and x302 ( and x301 true ) ) ( = tmp300 2 ) )
    ( implies ( and ( not x203 ) ( and ( not x204 ) true ) ) ( = tmp299 0 ) )
    ( implies ( and ( not x203 ) ( and x204 true ) ) ( = tmp299 ( / 5 10 ) ) )
    ( implies ( and x203 ( and ( not x204 ) true ) ) ( = tmp299 ( / 5 10 ) ) )
    ( implies ( and x203 ( and x204 true ) ) ( = tmp299 ( + ( / 5 10 ) ( / 5 10 ) ) ) )
    ( implies ( and ( not x304 ) ( and ( not x303 ) true ) ) ( = tmp298 0 ) )
    ( implies ( and ( not x304 ) ( and x303 true ) ) ( = tmp298 1 ) )
    ( implies ( and x304 ( and ( not x303 ) true ) ) ( = tmp298 1 ) )
    ( implies ( and x304 ( and x303 true ) ) ( = tmp298 2 ) )
    ( implies ( and ( not x201 ) ( and ( not x202 ) true ) ) ( = tmp297 0 ) )
    ( implies ( and ( not x201 ) ( and x202 true ) ) ( = tmp297 ( / 5 10 ) ) )
    ( implies ( and x201 ( and ( not x202 ) true ) ) ( = tmp297 ( / 5 10 ) ) )
    ( implies ( and x201 ( and x202 true ) ) ( = tmp297 ( + ( / 5 10 ) ( / 5 10 ) ) ) )
    ( implies ( and ( not x306 ) ( and ( not x305 ) true ) ) ( = tmp296 0 ) )
    ( implies ( and ( not x306 ) ( and x305 true ) ) ( = tmp296 1 ) )
    ( implies ( and x306 ( and ( not x305 ) true ) ) ( = tmp296 1 ) )
    ( implies ( and x306 ( and x305 true ) ) ( = tmp296 2 ) )
    ( implies ( and ( not x199 ) ( and ( not x200 ) true ) ) ( = tmp295 0 ) )
    ( implies ( and ( not x199 ) ( and x200 true ) ) ( = tmp295 ( / 5 10 ) ) )
    ( implies ( and x199 ( and ( not x200 ) true ) ) ( = tmp295 ( / 5 10 ) ) )
    ( implies ( and x199 ( and x200 true ) ) ( = tmp295 ( + ( / 5 10 ) ( / 5 10 ) ) ) )
    ( implies ( and ( not x308 ) ( and ( not x307 ) true ) ) ( = tmp294 0 ) )
    ( implies ( and ( not x308 ) ( and x307 true ) ) ( = tmp294 ( + 1 ( / 25 100 ) ) ) )
    ( implies ( and x308 ( and ( not x307 ) true ) ) ( = tmp294 ( + 1 ( / 25 100 ) ) ) )
    ( implies ( and x308 ( and x307 true ) ) ( = tmp294 ( + ( + 1 ( / 25 100 ) ) ( + 1 ( / 25 100 ) ) ) ) )
    ( implies ( and ( not x197 ) ( and ( not x198 ) true ) ) ( = tmp293 0 ) )
    ( implies ( and ( not x197 ) ( and x198 true ) ) ( = tmp293 ( / 25 100 ) ) )
    ( implies ( and x197 ( and ( not x198 ) true ) ) ( = tmp293 ( / 25 100 ) ) )
    ( implies ( and x197 ( and x198 true ) ) ( = tmp293 ( + ( / 25 100 ) ( / 25 100 ) ) ) )
    ( implies ( and ( not x310 ) ( and ( not x309 ) true ) ) ( = tmp292 0 ) )
    ( implies ( and ( not x310 ) ( and x309 true ) ) ( = tmp292 ( + 1 ( / 25 100 ) ) ) )
    ( implies ( and x310 ( and ( not x309 ) true ) ) ( = tmp292 ( + 1 ( / 25 100 ) ) ) )
    ( implies ( and x310 ( and x309 true ) ) ( = tmp292 ( + ( + 1 ( / 25 100 ) ) ( + 1 ( / 25 100 ) ) ) ) )
    ( implies ( and ( not x195 ) ( and ( not x196 ) true ) ) ( = tmp291 0 ) )
    ( implies ( and ( not x195 ) ( and x196 true ) ) ( = tmp291 ( / 25 100 ) ) )
    ( implies ( and x195 ( and ( not x196 ) true ) ) ( = tmp291 ( / 25 100 ) ) )
    ( implies ( and x195 ( and x196 true ) ) ( = tmp291 ( + ( / 25 100 ) ( / 25 100 ) ) ) )
    ( implies ( and ( not x312 ) ( and ( not x311 ) true ) ) ( = tmp290 0 ) )
    ( implies ( and ( not x312 ) ( and x311 true ) ) ( = tmp290 ( + 1 ( / 25 100 ) ) ) )
    ( implies ( and x312 ( and ( not x311 ) true ) ) ( = tmp290 ( + 1 ( / 25 100 ) ) ) )
    ( implies ( and x312 ( and x311 true ) ) ( = tmp290 ( + ( + 1 ( / 25 100 ) ) ( + 1 ( / 25 100 ) ) ) ) )
    ( implies ( and ( not x193 ) ( and ( not x194 ) true ) ) ( = tmp289 0 ) )
    ( implies ( and ( not x193 ) ( and x194 true ) ) ( = tmp289 ( / 25 100 ) ) )
    ( implies ( and x193 ( and ( not x194 ) true ) ) ( = tmp289 ( / 25 100 ) ) )
    ( implies ( and x193 ( and x194 true ) ) ( = tmp289 ( + ( / 25 100 ) ( / 25 100 ) ) ) )
    ( implies ( and ( not x314 ) ( and ( not x313 ) true ) ) ( = tmp288 0 ) )
    ( implies ( and ( not x314 ) ( and x313 true ) ) ( = tmp288 ( / 25 100 ) ) )
    ( implies ( and x314 ( and ( not x313 ) true ) ) ( = tmp288 ( / 25 100 ) ) )
    ( implies ( and x314 ( and x313 true ) ) ( = tmp288 ( + ( / 25 100 ) ( / 25 100 ) ) ) )
    ( implies ( and ( not x191 ) ( and ( not x192 ) true ) ) ( = tmp287 0 ) )
    ( implies ( and ( not x191 ) ( and x192 true ) ) ( = tmp287 ( + 1 ( / 25 100 ) ) ) )
    ( implies ( and x191 ( and ( not x192 ) true ) ) ( = tmp287 ( + 1 ( / 25 100 ) ) ) )
    ( implies ( and x191 ( and x192 true ) ) ( = tmp287 ( + ( + 1 ( / 25 100 ) ) ( + 1 ( / 25 100 ) ) ) ) )
    ( implies ( and ( not x316 ) ( and ( not x315 ) true ) ) ( = tmp286 0 ) )
    ( implies ( and ( not x316 ) ( and x315 true ) ) ( = tmp286 ( / 25 100 ) ) )
    ( implies ( and x316 ( and ( not x315 ) true ) ) ( = tmp286 ( / 25 100 ) ) )
    ( implies ( and x316 ( and x315 true ) ) ( = tmp286 ( + ( / 25 100 ) ( / 25 100 ) ) ) )
    ( implies ( and ( not x189 ) ( and ( not x190 ) true ) ) ( = tmp285 0 ) )
    ( implies ( and ( not x189 ) ( and x190 true ) ) ( = tmp285 ( + 1 ( / 25 100 ) ) ) )
    ( implies ( and x189 ( and ( not x190 ) true ) ) ( = tmp285 ( + 1 ( / 25 100 ) ) ) )
    ( implies ( and x189 ( and x190 true ) ) ( = tmp285 ( + ( + 1 ( / 25 100 ) ) ( + 1 ( / 25 100 ) ) ) ) )
    ( implies ( and ( not x318 ) ( and ( not x317 ) true ) ) ( = tmp284 0 ) )
    ( implies ( and ( not x318 ) ( and x317 true ) ) ( = tmp284 ( / 25 100 ) ) )
    ( implies ( and x318 ( and ( not x317 ) true ) ) ( = tmp284 ( / 25 100 ) ) )
    ( implies ( and x318 ( and x317 true ) ) ( = tmp284 ( + ( / 25 100 ) ( / 25 100 ) ) ) )
    ( implies ( and ( not x187 ) ( and ( not x188 ) true ) ) ( = tmp283 0 ) )
    ( implies ( and ( not x187 ) ( and x188 true ) ) ( = tmp283 ( + 1 ( / 25 100 ) ) ) )
    ( implies ( and x187 ( and ( not x188 ) true ) ) ( = tmp283 ( + 1 ( / 25 100 ) ) ) )
    ( implies ( and x187 ( and x188 true ) ) ( = tmp283 ( + ( + 1 ( / 25 100 ) ) ( + 1 ( / 25 100 ) ) ) ) )
    ( implies ( and ( not x320 ) ( and ( not x319 ) true ) ) ( = tmp282 0 ) )
    ( implies ( and ( not x320 ) ( and x319 true ) ) ( = tmp282 ( / 5 10 ) ) )
    ( implies ( and x320 ( and ( not x319 ) true ) ) ( = tmp282 ( / 5 10 ) ) )
    ( implies ( and x320 ( and x319 true ) ) ( = tmp282 ( + ( / 5 10 ) ( / 5 10 ) ) ) )
    ( implies ( and ( not x185 ) ( and ( not x186 ) true ) ) ( = tmp281 0 ) )
    ( implies ( and ( not x185 ) ( and x186 true ) ) ( = tmp281 1 ) )
    ( implies ( and x185 ( and ( not x186 ) true ) ) ( = tmp281 1 ) )
    ( implies ( and x185 ( and x186 true ) ) ( = tmp281 2 ) )
    ( implies ( and ( not x322 ) ( and ( not x321 ) true ) ) ( = tmp280 0 ) )
    ( implies ( and ( not x322 ) ( and x321 true ) ) ( = tmp280 ( / 5 10 ) ) )
    ( implies ( and x322 ( and ( not x321 ) true ) ) ( = tmp280 ( / 5 10 ) ) )
    ( implies ( and x322 ( and x321 true ) ) ( = tmp280 ( + ( / 5 10 ) ( / 5 10 ) ) ) )
    ( implies ( and ( not x183 ) ( and ( not x184 ) true ) ) ( = tmp279 0 ) )
    ( implies ( and ( not x183 ) ( and x184 true ) ) ( = tmp279 1 ) )
    ( implies ( and x183 ( and ( not x184 ) true ) ) ( = tmp279 1 ) )
    ( implies ( and x183 ( and x184 true ) ) ( = tmp279 2 ) )
    ( implies ( and ( not x324 ) ( and ( not x323 ) true ) ) ( = tmp278 0 ) )
    ( implies ( and ( not x324 ) ( and x323 true ) ) ( = tmp278 ( / 5 10 ) ) )
    ( implies ( and x324 ( and ( not x323 ) true ) ) ( = tmp278 ( / 5 10 ) ) )
    ( implies ( and x324 ( and x323 true ) ) ( = tmp278 ( + ( / 5 10 ) ( / 5 10 ) ) ) )
    ( implies ( and ( not x181 ) ( and ( not x182 ) true ) ) ( = tmp277 0 ) )
    ( implies ( and ( not x181 ) ( and x182 true ) ) ( = tmp277 1 ) )
    ( implies ( and x181 ( and ( not x182 ) true ) ) ( = tmp277 1 ) )
    ( implies ( and x181 ( and x182 true ) ) ( = tmp277 2 ) )
    ( implies ( and ( not x326 ) ( and ( not x325 ) true ) ) ( = tmp276 0 ) )
    ( implies ( and ( not x326 ) ( and x325 true ) ) ( = tmp276 1 ) )
    ( implies ( and x326 ( and ( not x325 ) true ) ) ( = tmp276 1 ) )
    ( implies ( and x326 ( and x325 true ) ) ( = tmp276 2 ) )
    ( implies ( and ( not x179 ) ( and ( not x180 ) true ) ) ( = tmp275 0 ) )
    ( implies ( and ( not x179 ) ( and x180 true ) ) ( = tmp275 ( / 5 10 ) ) )
    ( implies ( and x179 ( and ( not x180 ) true ) ) ( = tmp275 ( / 5 10 ) ) )
    ( implies ( and x179 ( and x180 true ) ) ( = tmp275 ( + ( / 5 10 ) ( / 5 10 ) ) ) )
    ( implies ( and ( not x328 ) ( and ( not x327 ) true ) ) ( = tmp274 0 ) )
    ( implies ( and ( not x328 ) ( and x327 true ) ) ( = tmp274 1 ) )
    ( implies ( and x328 ( and ( not x327 ) true ) ) ( = tmp274 1 ) )
    ( implies ( and x328 ( and x327 true ) ) ( = tmp274 2 ) )
    ( implies ( and ( not x177 ) ( and ( not x178 ) true ) ) ( = tmp273 0 ) )
    ( implies ( and ( not x177 ) ( and x178 true ) ) ( = tmp273 ( / 5 10 ) ) )
    ( implies ( and x177 ( and ( not x178 ) true ) ) ( = tmp273 ( / 5 10 ) ) )
    ( implies ( and x177 ( and x178 true ) ) ( = tmp273 ( + ( / 5 10 ) ( / 5 10 ) ) ) )
    ( implies ( and ( not x330 ) ( and ( not x329 ) true ) ) ( = tmp272 0 ) )
    ( implies ( and ( not x330 ) ( and x329 true ) ) ( = tmp272 1 ) )
    ( implies ( and x330 ( and ( not x329 ) true ) ) ( = tmp272 1 ) )
    ( implies ( and x330 ( and x329 true ) ) ( = tmp272 2 ) )
    ( implies ( and ( not x175 ) ( and ( not x176 ) true ) ) ( = tmp271 0 ) )
    ( implies ( and ( not x175 ) ( and x176 true ) ) ( = tmp271 ( / 5 10 ) ) )
    ( implies ( and x175 ( and ( not x176 ) true ) ) ( = tmp271 ( / 5 10 ) ) )
    ( implies ( and x175 ( and x176 true ) ) ( = tmp271 ( + ( / 5 10 ) ( / 5 10 ) ) ) )
    ( implies ( and ( not x332 ) ( and ( not x331 ) true ) ) ( = tmp270 0 ) )
    ( implies ( and ( not x332 ) ( and x331 true ) ) ( = tmp270 ( + 1 ( / 25 100 ) ) ) )
    ( implies ( and x332 ( and ( not x331 ) true ) ) ( = tmp270 ( + 1 ( / 25 100 ) ) ) )
    ( implies ( and x332 ( and x331 true ) ) ( = tmp270 ( + ( + 1 ( / 25 100 ) ) ( + 1 ( / 25 100 ) ) ) ) )
    ( implies ( and ( not x173 ) ( and ( not x174 ) true ) ) ( = tmp269 0 ) )
    ( implies ( and ( not x173 ) ( and x174 true ) ) ( = tmp269 ( / 25 100 ) ) )
    ( implies ( and x173 ( and ( not x174 ) true ) ) ( = tmp269 ( / 25 100 ) ) )
    ( implies ( and x173 ( and x174 true ) ) ( = tmp269 ( + ( / 25 100 ) ( / 25 100 ) ) ) )
    ( implies ( and ( not x334 ) ( and ( not x333 ) true ) ) ( = tmp268 0 ) )
    ( implies ( and ( not x334 ) ( and x333 true ) ) ( = tmp268 ( + 1 ( / 25 100 ) ) ) )
    ( implies ( and x334 ( and ( not x333 ) true ) ) ( = tmp268 ( + 1 ( / 25 100 ) ) ) )
    ( implies ( and x334 ( and x333 true ) ) ( = tmp268 ( + ( + 1 ( / 25 100 ) ) ( + 1 ( / 25 100 ) ) ) ) )
    ( implies ( and ( not x171 ) ( and ( not x172 ) true ) ) ( = tmp267 0 ) )
    ( implies ( and ( not x171 ) ( and x172 true ) ) ( = tmp267 ( / 25 100 ) ) )
    ( implies ( and x171 ( and ( not x172 ) true ) ) ( = tmp267 ( / 25 100 ) ) )
    ( implies ( and x171 ( and x172 true ) ) ( = tmp267 ( + ( / 25 100 ) ( / 25 100 ) ) ) )
    ( implies ( and ( not x336 ) ( and ( not x335 ) true ) ) ( = tmp266 0 ) )
    ( implies ( and ( not x336 ) ( and x335 true ) ) ( = tmp266 ( + 1 ( / 25 100 ) ) ) )
    ( implies ( and x336 ( and ( not x335 ) true ) ) ( = tmp266 ( + 1 ( / 25 100 ) ) ) )
    ( implies ( and x336 ( and x335 true ) ) ( = tmp266 ( + ( + 1 ( / 25 100 ) ) ( + 1 ( / 25 100 ) ) ) ) )
    ( implies ( and ( not x169 ) ( and ( not x170 ) true ) ) ( = tmp265 0 ) )
    ( implies ( and ( not x169 ) ( and x170 true ) ) ( = tmp265 ( / 25 100 ) ) )
    ( implies ( and x169 ( and ( not x170 ) true ) ) ( = tmp265 ( / 25 100 ) ) )
    ( implies ( and x169 ( and x170 true ) ) ( = tmp265 ( + ( / 25 100 ) ( / 25 100 ) ) ) )
    ( implies ( and ( not x336 ) true ) ( = tmp264 0 ) )
    ( implies ( and x336 true ) ( = tmp264 1 ) )
    ( implies ( and ( not x335 ) true ) ( = tmp263 0 ) )
    ( implies ( and x335 true ) ( = tmp263 1 ) )
    ( implies ( and ( not x334 ) true ) ( = tmp262 0 ) )
    ( implies ( and x334 true ) ( = tmp262 1 ) )
    ( implies ( and ( not x333 ) true ) ( = tmp261 0 ) )
    ( implies ( and x333 true ) ( = tmp261 1 ) )
    ( implies ( and ( not x332 ) true ) ( = tmp260 0 ) )
    ( implies ( and x332 true ) ( = tmp260 1 ) )
    ( implies ( and ( not x331 ) true ) ( = tmp259 0 ) )
    ( implies ( and x331 true ) ( = tmp259 1 ) )
    ( implies ( and ( not x330 ) true ) ( = tmp258 0 ) )
    ( implies ( and x330 true ) ( = tmp258 1 ) )
    ( implies ( and ( not x329 ) true ) ( = tmp257 0 ) )
    ( implies ( and x329 true ) ( = tmp257 1 ) )
    ( implies ( and ( not x328 ) true ) ( = tmp256 0 ) )
    ( implies ( and x328 true ) ( = tmp256 1 ) )
    ( implies ( and ( not x327 ) true ) ( = tmp255 0 ) )
    ( implies ( and x327 true ) ( = tmp255 1 ) )
    ( implies ( and ( not x326 ) true ) ( = tmp254 0 ) )
    ( implies ( and x326 true ) ( = tmp254 1 ) )
    ( implies ( and ( not x325 ) true ) ( = tmp253 0 ) )
    ( implies ( and x325 true ) ( = tmp253 1 ) )
    ( implies ( and ( not x324 ) true ) ( = tmp252 0 ) )
    ( implies ( and x324 true ) ( = tmp252 1 ) )
    ( implies ( and ( not x323 ) true ) ( = tmp251 0 ) )
    ( implies ( and x323 true ) ( = tmp251 1 ) )
    ( implies ( and ( not x322 ) true ) ( = tmp250 0 ) )
    ( implies ( and x322 true ) ( = tmp250 1 ) )
    ( implies ( and ( not x321 ) true ) ( = tmp249 0 ) )
    ( implies ( and x321 true ) ( = tmp249 1 ) )
    ( implies ( and ( not x320 ) true ) ( = tmp248 0 ) )
    ( implies ( and x320 true ) ( = tmp248 1 ) )
    ( implies ( and ( not x319 ) true ) ( = tmp247 0 ) )
    ( implies ( and x319 true ) ( = tmp247 1 ) )
    ( implies ( and ( not x318 ) true ) ( = tmp246 0 ) )
    ( implies ( and x318 true ) ( = tmp246 1 ) )
    ( implies ( and ( not x317 ) true ) ( = tmp245 0 ) )
    ( implies ( and x317 true ) ( = tmp245 1 ) )
    ( implies ( and ( not x316 ) true ) ( = tmp244 0 ) )
    ( implies ( and x316 true ) ( = tmp244 1 ) )
    ( implies ( and ( not x315 ) true ) ( = tmp243 0 ) )
    ( implies ( and x315 true ) ( = tmp243 1 ) )
    ( implies ( and ( not x314 ) true ) ( = tmp242 0 ) )
    ( implies ( and x314 true ) ( = tmp242 1 ) )
    ( implies ( and ( not x313 ) true ) ( = tmp241 0 ) )
    ( implies ( and x313 true ) ( = tmp241 1 ) )
    ( implies ( and ( not x312 ) true ) ( = tmp240 0 ) )
    ( implies ( and x312 true ) ( = tmp240 1 ) )
    ( implies ( and ( not x311 ) true ) ( = tmp239 0 ) )
    ( implies ( and x311 true ) ( = tmp239 1 ) )
    ( implies ( and ( not x310 ) true ) ( = tmp238 0 ) )
    ( implies ( and x310 true ) ( = tmp238 1 ) )
    ( implies ( and ( not x309 ) true ) ( = tmp237 0 ) )
    ( implies ( and x309 true ) ( = tmp237 1 ) )
    ( implies ( and ( not x308 ) true ) ( = tmp236 0 ) )
    ( implies ( and x308 true ) ( = tmp236 1 ) )
    ( implies ( and ( not x307 ) true ) ( = tmp235 0 ) )
    ( implies ( and x307 true ) ( = tmp235 1 ) )
    ( implies ( and ( not x306 ) true ) ( = tmp234 0 ) )
    ( implies ( and x306 true ) ( = tmp234 1 ) )
    ( implies ( and ( not x305 ) true ) ( = tmp233 0 ) )
    ( implies ( and x305 true ) ( = tmp233 1 ) )
    ( implies ( and ( not x304 ) true ) ( = tmp232 0 ) )
    ( implies ( and x304 true ) ( = tmp232 1 ) )
    ( implies ( and ( not x303 ) true ) ( = tmp231 0 ) )
    ( implies ( and x303 true ) ( = tmp231 1 ) )
    ( implies ( and ( not x302 ) true ) ( = tmp230 0 ) )
    ( implies ( and x302 true ) ( = tmp230 1 ) )
    ( implies ( and ( not x301 ) true ) ( = tmp229 0 ) )
    ( implies ( and x301 true ) ( = tmp229 1 ) )
    ( implies ( and ( not x300 ) true ) ( = tmp228 0 ) )
    ( implies ( and x300 true ) ( = tmp228 1 ) )
    ( implies ( and ( not x299 ) true ) ( = tmp227 0 ) )
    ( implies ( and x299 true ) ( = tmp227 1 ) )
    ( implies ( and ( not x298 ) true ) ( = tmp226 0 ) )
    ( implies ( and x298 true ) ( = tmp226 1 ) )
    ( implies ( and ( not x297 ) true ) ( = tmp225 0 ) )
    ( implies ( and x297 true ) ( = tmp225 1 ) )
    ( implies ( and ( not x296 ) true ) ( = tmp224 0 ) )
    ( implies ( and x296 true ) ( = tmp224 1 ) )
    ( implies ( and ( not x295 ) true ) ( = tmp223 0 ) )
    ( implies ( and x295 true ) ( = tmp223 1 ) )
    ( implies ( and ( not x294 ) true ) ( = tmp222 0 ) )
    ( implies ( and x294 true ) ( = tmp222 1 ) )
    ( implies ( and ( not x293 ) true ) ( = tmp221 0 ) )
    ( implies ( and x293 true ) ( = tmp221 1 ) )
    ( implies ( and ( not x292 ) true ) ( = tmp220 0 ) )
    ( implies ( and x292 true ) ( = tmp220 1 ) )
    ( implies ( and ( not x291 ) true ) ( = tmp219 0 ) )
    ( implies ( and x291 true ) ( = tmp219 1 ) )
    ( implies ( and ( not x290 ) true ) ( = tmp218 0 ) )
    ( implies ( and x290 true ) ( = tmp218 1 ) )
    ( implies ( and ( not x289 ) true ) ( = tmp217 0 ) )
    ( implies ( and x289 true ) ( = tmp217 1 ) )
    ( implies ( and ( not x288 ) true ) ( = tmp216 0 ) )
    ( implies ( and x288 true ) ( = tmp216 1 ) )
    ( implies ( and ( not x287 ) true ) ( = tmp215 0 ) )
    ( implies ( and x287 true ) ( = tmp215 1 ) )
    ( implies ( and ( not x286 ) true ) ( = tmp214 0 ) )
    ( implies ( and x286 true ) ( = tmp214 1 ) )
    ( implies ( and ( not x285 ) true ) ( = tmp213 0 ) )
    ( implies ( and x285 true ) ( = tmp213 1 ) )
    ( implies ( and ( not x284 ) true ) ( = tmp212 0 ) )
    ( implies ( and x284 true ) ( = tmp212 1 ) )
    ( implies ( and ( not x283 ) true ) ( = tmp211 0 ) )
    ( implies ( and x283 true ) ( = tmp211 1 ) )
    ( implies ( and ( not x282 ) true ) ( = tmp210 0 ) )
    ( implies ( and x282 true ) ( = tmp210 1 ) )
    ( implies ( and ( not x281 ) true ) ( = tmp209 0 ) )
    ( implies ( and x281 true ) ( = tmp209 1 ) )
    ( implies ( and ( not x280 ) true ) ( = tmp208 0 ) )
    ( implies ( and x280 true ) ( = tmp208 1 ) )
    ( implies ( and ( not x279 ) true ) ( = tmp207 0 ) )
    ( implies ( and x279 true ) ( = tmp207 1 ) )
    ( implies ( and ( not x278 ) true ) ( = tmp206 0 ) )
    ( implies ( and x278 true ) ( = tmp206 1 ) )
    ( implies ( and ( not x277 ) true ) ( = tmp205 0 ) )
    ( implies ( and x277 true ) ( = tmp205 1 ) )
    ( implies ( and ( not x276 ) true ) ( = tmp204 0 ) )
    ( implies ( and x276 true ) ( = tmp204 1 ) )
    ( implies ( and ( not x275 ) true ) ( = tmp203 0 ) )
    ( implies ( and x275 true ) ( = tmp203 1 ) )
    ( implies ( and ( not x274 ) true ) ( = tmp202 0 ) )
    ( implies ( and x274 true ) ( = tmp202 1 ) )
    ( implies ( and ( not x273 ) true ) ( = tmp201 0 ) )
    ( implies ( and x273 true ) ( = tmp201 1 ) )
    ( implies ( and ( not x272 ) true ) ( = tmp200 0 ) )
    ( implies ( and x272 true ) ( = tmp200 1 ) )
    ( implies ( and ( not x271 ) true ) ( = tmp199 0 ) )
    ( implies ( and x271 true ) ( = tmp199 1 ) )
    ( implies ( and ( not x270 ) true ) ( = tmp198 0 ) )
    ( implies ( and x270 true ) ( = tmp198 1 ) )
    ( implies ( and ( not x269 ) true ) ( = tmp197 0 ) )
    ( implies ( and x269 true ) ( = tmp197 1 ) )
    ( implies ( and ( not x268 ) true ) ( = tmp196 0 ) )
    ( implies ( and x268 true ) ( = tmp196 1 ) )
    ( implies ( and ( not x267 ) true ) ( = tmp195 0 ) )
    ( implies ( and x267 true ) ( = tmp195 1 ) )
    ( implies ( and ( not x266 ) true ) ( = tmp194 0 ) )
    ( implies ( and x266 true ) ( = tmp194 1 ) )
    ( implies ( and ( not x265 ) true ) ( = tmp193 0 ) )
    ( implies ( and x265 true ) ( = tmp193 1 ) )
    ( implies ( and ( not x264 ) true ) ( = tmp192 0 ) )
    ( implies ( and x264 true ) ( = tmp192 1 ) )
    ( implies ( and ( not x263 ) true ) ( = tmp191 0 ) )
    ( implies ( and x263 true ) ( = tmp191 1 ) )
    ( implies ( and ( not x262 ) true ) ( = tmp190 0 ) )
    ( implies ( and x262 true ) ( = tmp190 1 ) )
    ( implies ( and ( not x261 ) true ) ( = tmp189 0 ) )
    ( implies ( and x261 true ) ( = tmp189 1 ) )
    ( implies ( and ( not x260 ) true ) ( = tmp188 0 ) )
    ( implies ( and x260 true ) ( = tmp188 1 ) )
    ( implies ( and ( not x259 ) true ) ( = tmp187 0 ) )
    ( implies ( and x259 true ) ( = tmp187 1 ) )
    ( implies ( and ( not x258 ) true ) ( = tmp186 0 ) )
    ( implies ( and x258 true ) ( = tmp186 1 ) )
    ( implies ( and ( not x257 ) true ) ( = tmp185 0 ) )
    ( implies ( and x257 true ) ( = tmp185 1 ) )
    ( implies ( and ( not x256 ) true ) ( = tmp184 0 ) )
    ( implies ( and x256 true ) ( = tmp184 1 ) )
    ( implies ( and ( not x255 ) true ) ( = tmp183 0 ) )
    ( implies ( and x255 true ) ( = tmp183 1 ) )
    ( implies ( and ( not x254 ) true ) ( = tmp182 0 ) )
    ( implies ( and x254 true ) ( = tmp182 1 ) )
    ( implies ( and ( not x253 ) true ) ( = tmp181 0 ) )
    ( implies ( and x253 true ) ( = tmp181 1 ) )
    ( implies ( and ( not x252 ) true ) ( = tmp180 0 ) )
    ( implies ( and x252 true ) ( = tmp180 1 ) )
    ( implies ( and ( not x251 ) true ) ( = tmp179 0 ) )
    ( implies ( and x251 true ) ( = tmp179 1 ) )
    ( implies ( and ( not x250 ) true ) ( = tmp178 0 ) )
    ( implies ( and x250 true ) ( = tmp178 1 ) )
    ( implies ( and ( not x249 ) true ) ( = tmp177 0 ) )
    ( implies ( and x249 true ) ( = tmp177 1 ) )
    ( implies ( and ( not x248 ) true ) ( = tmp176 0 ) )
    ( implies ( and x248 true ) ( = tmp176 1 ) )
    ( implies ( and ( not x247 ) true ) ( = tmp175 0 ) )
    ( implies ( and x247 true ) ( = tmp175 1 ) )
    ( implies ( and ( not x246 ) true ) ( = tmp174 0 ) )
    ( implies ( and x246 true ) ( = tmp174 1 ) )
    ( implies ( and ( not x245 ) true ) ( = tmp173 0 ) )
    ( implies ( and x245 true ) ( = tmp173 1 ) )
    ( implies ( and ( not x244 ) true ) ( = tmp172 0 ) )
    ( implies ( and x244 true ) ( = tmp172 1 ) )
    ( implies ( and ( not x243 ) true ) ( = tmp171 0 ) )
    ( implies ( and x243 true ) ( = tmp171 1 ) )
    ( implies ( and ( not x242 ) true ) ( = tmp170 0 ) )
    ( implies ( and x242 true ) ( = tmp170 1 ) )
    ( implies ( and ( not x241 ) true ) ( = tmp169 0 ) )
    ( implies ( and x241 true ) ( = tmp169 1 ) )
    ( implies ( and ( not x240 ) true ) ( = tmp168 0 ) )
    ( implies ( and x240 true ) ( = tmp168 1 ) )
    ( implies ( and ( not x239 ) true ) ( = tmp167 0 ) )
    ( implies ( and x239 true ) ( = tmp167 1 ) )
    ( implies ( and ( not x238 ) true ) ( = tmp166 0 ) )
    ( implies ( and x238 true ) ( = tmp166 1 ) )
    ( implies ( and ( not x237 ) true ) ( = tmp165 0 ) )
    ( implies ( and x237 true ) ( = tmp165 1 ) )
    ( implies ( and ( not x236 ) true ) ( = tmp164 0 ) )
    ( implies ( and x236 true ) ( = tmp164 1 ) )
    ( implies ( and ( not x235 ) true ) ( = tmp163 0 ) )
    ( implies ( and x235 true ) ( = tmp163 1 ) )
    ( implies ( and ( not x234 ) true ) ( = tmp162 0 ) )
    ( implies ( and x234 true ) ( = tmp162 1 ) )
    ( implies ( and ( not x233 ) true ) ( = tmp161 0 ) )
    ( implies ( and x233 true ) ( = tmp161 1 ) )
    ( implies ( and ( not x232 ) true ) ( = tmp160 0 ) )
    ( implies ( and x232 true ) ( = tmp160 1 ) )
    ( implies ( and ( not x231 ) true ) ( = tmp159 0 ) )
    ( implies ( and x231 true ) ( = tmp159 1 ) )
    ( implies ( and ( not x230 ) true ) ( = tmp158 0 ) )
    ( implies ( and x230 true ) ( = tmp158 1 ) )
    ( implies ( and ( not x229 ) true ) ( = tmp157 0 ) )
    ( implies ( and x229 true ) ( = tmp157 1 ) )
    ( implies ( and ( not x228 ) true ) ( = tmp156 0 ) )
    ( implies ( and x228 true ) ( = tmp156 1 ) )
    ( implies ( and ( not x227 ) true ) ( = tmp155 0 ) )
    ( implies ( and x227 true ) ( = tmp155 1 ) )
    ( implies ( and ( not x226 ) true ) ( = tmp154 0 ) )
    ( implies ( and x226 true ) ( = tmp154 1 ) )
    ( implies ( and ( not x225 ) true ) ( = tmp153 0 ) )
    ( implies ( and x225 true ) ( = tmp153 1 ) )
    ( implies ( and ( not x224 ) true ) ( = tmp152 0 ) )
    ( implies ( and x224 true ) ( = tmp152 1 ) )
    ( implies ( and ( not x223 ) true ) ( = tmp151 0 ) )
    ( implies ( and x223 true ) ( = tmp151 1 ) )
    ( implies ( and ( not x222 ) true ) ( = tmp150 0 ) )
    ( implies ( and x222 true ) ( = tmp150 1 ) )
    ( implies ( and ( not x221 ) true ) ( = tmp149 0 ) )
    ( implies ( and x221 true ) ( = tmp149 1 ) )
    ( implies ( and ( not x220 ) true ) ( = tmp148 0 ) )
    ( implies ( and x220 true ) ( = tmp148 1 ) )
    ( implies ( and ( not x219 ) true ) ( = tmp147 0 ) )
    ( implies ( and x219 true ) ( = tmp147 1 ) )
    ( implies ( and ( not x218 ) true ) ( = tmp146 0 ) )
    ( implies ( and x218 true ) ( = tmp146 1 ) )
    ( implies ( and ( not x217 ) true ) ( = tmp145 0 ) )
    ( implies ( and x217 true ) ( = tmp145 1 ) )
    ( implies ( and ( not x216 ) true ) ( = tmp144 0 ) )
    ( implies ( and x216 true ) ( = tmp144 1 ) )
    ( implies ( and ( not x215 ) true ) ( = tmp143 0 ) )
    ( implies ( and x215 true ) ( = tmp143 1 ) )
    ( implies ( and ( not x214 ) true ) ( = tmp142 0 ) )
    ( implies ( and x214 true ) ( = tmp142 1 ) )
    ( implies ( and ( not x213 ) true ) ( = tmp141 0 ) )
    ( implies ( and x213 true ) ( = tmp141 1 ) )
    ( implies ( and ( not x212 ) true ) ( = tmp140 0 ) )
    ( implies ( and x212 true ) ( = tmp140 1 ) )
    ( implies ( and ( not x211 ) true ) ( = tmp139 0 ) )
    ( implies ( and x211 true ) ( = tmp139 1 ) )
    ( implies ( and ( not x210 ) true ) ( = tmp138 0 ) )
    ( implies ( and x210 true ) ( = tmp138 1 ) )
    ( implies ( and ( not x209 ) true ) ( = tmp137 0 ) )
    ( implies ( and x209 true ) ( = tmp137 1 ) )
    ( implies ( and ( not x208 ) true ) ( = tmp136 0 ) )
    ( implies ( and x208 true ) ( = tmp136 1 ) )
    ( implies ( and ( not x207 ) true ) ( = tmp135 0 ) )
    ( implies ( and x207 true ) ( = tmp135 1 ) )
    ( implies ( and ( not x206 ) true ) ( = tmp134 0 ) )
    ( implies ( and x206 true ) ( = tmp134 1 ) )
    ( implies ( and ( not x205 ) true ) ( = tmp133 0 ) )
    ( implies ( and x205 true ) ( = tmp133 1 ) )
    ( implies ( and ( not x204 ) true ) ( = tmp132 0 ) )
    ( implies ( and x204 true ) ( = tmp132 1 ) )
    ( implies ( and ( not x203 ) true ) ( = tmp131 0 ) )
    ( implies ( and x203 true ) ( = tmp131 1 ) )
    ( implies ( and ( not x202 ) true ) ( = tmp130 0 ) )
    ( implies ( and x202 true ) ( = tmp130 1 ) )
    ( implies ( and ( not x201 ) true ) ( = tmp129 0 ) )
    ( implies ( and x201 true ) ( = tmp129 1 ) )
    ( implies ( and ( not x200 ) true ) ( = tmp128 0 ) )
    ( implies ( and x200 true ) ( = tmp128 1 ) )
    ( implies ( and ( not x199 ) true ) ( = tmp127 0 ) )
    ( implies ( and x199 true ) ( = tmp127 1 ) )
    ( implies ( and ( not x198 ) true ) ( = tmp126 0 ) )
    ( implies ( and x198 true ) ( = tmp126 1 ) )
    ( implies ( and ( not x197 ) true ) ( = tmp125 0 ) )
    ( implies ( and x197 true ) ( = tmp125 1 ) )
    ( implies ( and ( not x196 ) true ) ( = tmp124 0 ) )
    ( implies ( and x196 true ) ( = tmp124 1 ) )
    ( implies ( and ( not x195 ) true ) ( = tmp123 0 ) )
    ( implies ( and x195 true ) ( = tmp123 1 ) )
    ( implies ( and ( not x194 ) true ) ( = tmp122 0 ) )
    ( implies ( and x194 true ) ( = tmp122 1 ) )
    ( implies ( and ( not x193 ) true ) ( = tmp121 0 ) )
    ( implies ( and x193 true ) ( = tmp121 1 ) )
    ( implies ( and ( not x192 ) true ) ( = tmp120 0 ) )
    ( implies ( and x192 true ) ( = tmp120 1 ) )
    ( implies ( and ( not x191 ) true ) ( = tmp119 0 ) )
    ( implies ( and x191 true ) ( = tmp119 1 ) )
    ( implies ( and ( not x190 ) true ) ( = tmp118 0 ) )
    ( implies ( and x190 true ) ( = tmp118 1 ) )
    ( implies ( and ( not x189 ) true ) ( = tmp117 0 ) )
    ( implies ( and x189 true ) ( = tmp117 1 ) )
    ( implies ( and ( not x188 ) true ) ( = tmp116 0 ) )
    ( implies ( and x188 true ) ( = tmp116 1 ) )
    ( implies ( and ( not x187 ) true ) ( = tmp115 0 ) )
    ( implies ( and x187 true ) ( = tmp115 1 ) )
    ( implies ( and ( not x186 ) true ) ( = tmp114 0 ) )
    ( implies ( and x186 true ) ( = tmp114 1 ) )
    ( implies ( and ( not x185 ) true ) ( = tmp113 0 ) )
    ( implies ( and x185 true ) ( = tmp113 1 ) )
    ( implies ( and ( not x184 ) true ) ( = tmp112 0 ) )
    ( implies ( and x184 true ) ( = tmp112 1 ) )
    ( implies ( and ( not x183 ) true ) ( = tmp111 0 ) )
    ( implies ( and x183 true ) ( = tmp111 1 ) )
    ( implies ( and ( not x182 ) true ) ( = tmp110 0 ) )
    ( implies ( and x182 true ) ( = tmp110 1 ) )
    ( implies ( and ( not x181 ) true ) ( = tmp109 0 ) )
    ( implies ( and x181 true ) ( = tmp109 1 ) )
    ( implies ( and ( not x180 ) true ) ( = tmp108 0 ) )
    ( implies ( and x180 true ) ( = tmp108 1 ) )
    ( implies ( and ( not x179 ) true ) ( = tmp107 0 ) )
    ( implies ( and x179 true ) ( = tmp107 1 ) )
    ( implies ( and ( not x178 ) true ) ( = tmp106 0 ) )
    ( implies ( and x178 true ) ( = tmp106 1 ) )
    ( implies ( and ( not x177 ) true ) ( = tmp105 0 ) )
    ( implies ( and x177 true ) ( = tmp105 1 ) )
    ( implies ( and ( not x176 ) true ) ( = tmp104 0 ) )
    ( implies ( and x176 true ) ( = tmp104 1 ) )
    ( implies ( and ( not x175 ) true ) ( = tmp103 0 ) )
    ( implies ( and x175 true ) ( = tmp103 1 ) )
    ( implies ( and ( not x174 ) true ) ( = tmp102 0 ) )
    ( implies ( and x174 true ) ( = tmp102 1 ) )
    ( implies ( and ( not x173 ) true ) ( = tmp101 0 ) )
    ( implies ( and x173 true ) ( = tmp101 1 ) )
    ( implies ( and ( not x172 ) true ) ( = tmp100 0 ) )
    ( implies ( and x172 true ) ( = tmp100 1 ) )
    ( implies ( and ( not x171 ) true ) ( = tmp99 0 ) )
    ( implies ( and x171 true ) ( = tmp99 1 ) )
    ( implies ( and ( not x170 ) true ) ( = tmp98 0 ) )
    ( implies ( and x170 true ) ( = tmp98 1 ) )
    ( implies ( and ( not x169 ) true ) ( = tmp97 0 ) )
    ( implies ( and x169 true ) ( = tmp97 1 ) )
    ( implies ( and ( not x288 ) true ) ( = tmp96 0 ) )
    ( implies ( and x288 true ) ( = tmp96 ( / 125 1000 ) ) )
    ( implies ( and ( not x240 ) ( and ( not x264 ) true ) ) ( = tmp95 0 ) )
    ( implies ( and ( not x240 ) ( and x264 true ) ) ( = tmp95 ( / 125 1000 ) ) )
    ( implies ( and x240 ( and ( not x264 ) true ) ) ( = tmp95 ( / 125 1000 ) ) )
    ( implies ( and x240 ( and x264 true ) ) ( = tmp95 ( + ( / 125 1000 ) ( / 125 1000 ) ) ) )
    ( implies ( and ( not x336 ) ( and ( not x312 ) true ) ) ( = tmp94 0 ) )
    ( implies ( and ( not x336 ) ( and x312 true ) ) ( = tmp94 ( / 125 1000 ) ) )
    ( implies ( and x336 ( and ( not x312 ) true ) ) ( = tmp94 ( / 125 1000 ) ) )
    ( implies ( and x336 ( and x312 true ) ) ( = tmp94 ( + ( / 125 1000 ) ( / 125 1000 ) ) ) )
    ( implies ( and ( not x192 ) ( and ( not x216 ) true ) ) ( = tmp93 0 ) )
    ( implies ( and ( not x192 ) ( and x216 true ) ) ( = tmp93 ( / 125 1000 ) ) )
    ( implies ( and x192 ( and ( not x216 ) true ) ) ( = tmp93 ( / 125 1000 ) ) )
    ( implies ( and x192 ( and x216 true ) ) ( = tmp93 ( + ( / 125 1000 ) ( / 125 1000 ) ) ) )
    ( implies ( and ( not x287 ) true ) ( = tmp92 0 ) )
    ( implies ( and x287 true ) ( = tmp92 ( / 125 1000 ) ) )
    ( implies ( and ( not x239 ) ( and ( not x263 ) true ) ) ( = tmp91 0 ) )
    ( implies ( and ( not x239 ) ( and x263 true ) ) ( = tmp91 ( / 125 1000 ) ) )
    ( implies ( and x239 ( and ( not x263 ) true ) ) ( = tmp91 ( / 125 1000 ) ) )
    ( implies ( and x239 ( and x263 true ) ) ( = tmp91 ( + ( / 125 1000 ) ( / 125 1000 ) ) ) )
    ( implies ( and ( not x335 ) ( and ( not x311 ) true ) ) ( = tmp90 0 ) )
    ( implies ( and ( not x335 ) ( and x311 true ) ) ( = tmp90 ( / 125 1000 ) ) )
    ( implies ( and x335 ( and ( not x311 ) true ) ) ( = tmp90 ( / 125 1000 ) ) )
    ( implies ( and x335 ( and x311 true ) ) ( = tmp90 ( + ( / 125 1000 ) ( / 125 1000 ) ) ) )
    ( implies ( and ( not x191 ) ( and ( not x215 ) true ) ) ( = tmp89 0 ) )
    ( implies ( and ( not x191 ) ( and x215 true ) ) ( = tmp89 ( / 125 1000 ) ) )
    ( implies ( and x191 ( and ( not x215 ) true ) ) ( = tmp89 ( / 125 1000 ) ) )
    ( implies ( and x191 ( and x215 true ) ) ( = tmp89 ( + ( / 125 1000 ) ( / 125 1000 ) ) ) )
    ( implies ( and ( not x286 ) true ) ( = tmp88 0 ) )
    ( implies ( and x286 true ) ( = tmp88 ( / 125 1000 ) ) )
    ( implies ( and ( not x238 ) ( and ( not x262 ) true ) ) ( = tmp87 0 ) )
    ( implies ( and ( not x238 ) ( and x262 true ) ) ( = tmp87 ( / 125 1000 ) ) )
    ( implies ( and x238 ( and ( not x262 ) true ) ) ( = tmp87 ( / 125 1000 ) ) )
    ( implies ( and x238 ( and x262 true ) ) ( = tmp87 ( + ( / 125 1000 ) ( / 125 1000 ) ) ) )
    ( implies ( and ( not x334 ) ( and ( not x310 ) true ) ) ( = tmp86 0 ) )
    ( implies ( and ( not x334 ) ( and x310 true ) ) ( = tmp86 ( / 125 1000 ) ) )
    ( implies ( and x334 ( and ( not x310 ) true ) ) ( = tmp86 ( / 125 1000 ) ) )
    ( implies ( and x334 ( and x310 true ) ) ( = tmp86 ( + ( / 125 1000 ) ( / 125 1000 ) ) ) )
    ( implies ( and ( not x190 ) ( and ( not x214 ) true ) ) ( = tmp85 0 ) )
    ( implies ( and ( not x190 ) ( and x214 true ) ) ( = tmp85 ( / 125 1000 ) ) )
    ( implies ( and x190 ( and ( not x214 ) true ) ) ( = tmp85 ( / 125 1000 ) ) )
    ( implies ( and x190 ( and x214 true ) ) ( = tmp85 ( + ( / 125 1000 ) ( / 125 1000 ) ) ) )
    ( implies ( and ( not x285 ) true ) ( = tmp84 0 ) )
    ( implies ( and x285 true ) ( = tmp84 ( / 125 1000 ) ) )
    ( implies ( and ( not x237 ) ( and ( not x261 ) true ) ) ( = tmp83 0 ) )
    ( implies ( and ( not x237 ) ( and x261 true ) ) ( = tmp83 ( / 125 1000 ) ) )
    ( implies ( and x237 ( and ( not x261 ) true ) ) ( = tmp83 ( / 125 1000 ) ) )
    ( implies ( and x237 ( and x261 true ) ) ( = tmp83 ( + ( / 125 1000 ) ( / 125 1000 ) ) ) )
    ( implies ( and ( not x333 ) ( and ( not x309 ) true ) ) ( = tmp82 0 ) )
    ( implies ( and ( not x333 ) ( and x309 true ) ) ( = tmp82 ( / 125 1000 ) ) )
    ( implies ( and x333 ( and ( not x309 ) true ) ) ( = tmp82 ( / 125 1000 ) ) )
    ( implies ( and x333 ( and x309 true ) ) ( = tmp82 ( + ( / 125 1000 ) ( / 125 1000 ) ) ) )
    ( implies ( and ( not x189 ) ( and ( not x213 ) true ) ) ( = tmp81 0 ) )
    ( implies ( and ( not x189 ) ( and x213 true ) ) ( = tmp81 ( / 125 1000 ) ) )
    ( implies ( and x189 ( and ( not x213 ) true ) ) ( = tmp81 ( / 125 1000 ) ) )
    ( implies ( and x189 ( and x213 true ) ) ( = tmp81 ( + ( / 125 1000 ) ( / 125 1000 ) ) ) )
    ( implies ( and ( not x284 ) true ) ( = tmp80 0 ) )
    ( implies ( and x284 true ) ( = tmp80 ( / 125 1000 ) ) )
    ( implies ( and ( not x236 ) ( and ( not x260 ) true ) ) ( = tmp79 0 ) )
    ( implies ( and ( not x236 ) ( and x260 true ) ) ( = tmp79 ( / 125 1000 ) ) )
    ( implies ( and x236 ( and ( not x260 ) true ) ) ( = tmp79 ( / 125 1000 ) ) )
    ( implies ( and x236 ( and x260 true ) ) ( = tmp79 ( + ( / 125 1000 ) ( / 125 1000 ) ) ) )
    ( implies ( and ( not x332 ) ( and ( not x308 ) true ) ) ( = tmp78 0 ) )
    ( implies ( and ( not x332 ) ( and x308 true ) ) ( = tmp78 ( / 125 1000 ) ) )
    ( implies ( and x332 ( and ( not x308 ) true ) ) ( = tmp78 ( / 125 1000 ) ) )
    ( implies ( and x332 ( and x308 true ) ) ( = tmp78 ( + ( / 125 1000 ) ( / 125 1000 ) ) ) )
    ( implies ( and ( not x188 ) ( and ( not x212 ) true ) ) ( = tmp77 0 ) )
    ( implies ( and ( not x188 ) ( and x212 true ) ) ( = tmp77 ( / 125 1000 ) ) )
    ( implies ( and x188 ( and ( not x212 ) true ) ) ( = tmp77 ( / 125 1000 ) ) )
    ( implies ( and x188 ( and x212 true ) ) ( = tmp77 ( + ( / 125 1000 ) ( / 125 1000 ) ) ) )
    ( implies ( and ( not x283 ) true ) ( = tmp76 0 ) )
    ( implies ( and x283 true ) ( = tmp76 ( / 125 1000 ) ) )
    ( implies ( and ( not x235 ) ( and ( not x259 ) true ) ) ( = tmp75 0 ) )
    ( implies ( and ( not x235 ) ( and x259 true ) ) ( = tmp75 ( / 125 1000 ) ) )
    ( implies ( and x235 ( and ( not x259 ) true ) ) ( = tmp75 ( / 125 1000 ) ) )
    ( implies ( and x235 ( and x259 true ) ) ( = tmp75 ( + ( / 125 1000 ) ( / 125 1000 ) ) ) )
    ( implies ( and ( not x331 ) ( and ( not x307 ) true ) ) ( = tmp74 0 ) )
    ( implies ( and ( not x331 ) ( and x307 true ) ) ( = tmp74 ( / 125 1000 ) ) )
    ( implies ( and x331 ( and ( not x307 ) true ) ) ( = tmp74 ( / 125 1000 ) ) )
    ( implies ( and x331 ( and x307 true ) ) ( = tmp74 ( + ( / 125 1000 ) ( / 125 1000 ) ) ) )
    ( implies ( and ( not x187 ) ( and ( not x211 ) true ) ) ( = tmp73 0 ) )
    ( implies ( and ( not x187 ) ( and x211 true ) ) ( = tmp73 ( / 125 1000 ) ) )
    ( implies ( and x187 ( and ( not x211 ) true ) ) ( = tmp73 ( / 125 1000 ) ) )
    ( implies ( and x187 ( and x211 true ) ) ( = tmp73 ( + ( / 125 1000 ) ( / 125 1000 ) ) ) )
    ( implies ( and ( not x282 ) true ) ( = tmp72 0 ) )
    ( implies ( and x282 true ) ( = tmp72 ( / 1 10 ) ) )
    ( implies ( and ( not x234 ) ( and ( not x258 ) true ) ) ( = tmp71 0 ) )
    ( implies ( and ( not x234 ) ( and x258 true ) ) ( = tmp71 ( / 1 10 ) ) )
    ( implies ( and x234 ( and ( not x258 ) true ) ) ( = tmp71 ( / 1 10 ) ) )
    ( implies ( and x234 ( and x258 true ) ) ( = tmp71 ( + ( / 1 10 ) ( / 1 10 ) ) ) )
    ( implies ( and ( not x330 ) ( and ( not x306 ) true ) ) ( = tmp70 0 ) )
    ( implies ( and ( not x330 ) ( and x306 true ) ) ( = tmp70 ( / 1 10 ) ) )
    ( implies ( and x330 ( and ( not x306 ) true ) ) ( = tmp70 ( / 1 10 ) ) )
    ( implies ( and x330 ( and x306 true ) ) ( = tmp70 ( + ( / 1 10 ) ( / 1 10 ) ) ) )
    ( implies ( and ( not x186 ) ( and ( not x210 ) true ) ) ( = tmp69 0 ) )
    ( implies ( and ( not x186 ) ( and x210 true ) ) ( = tmp69 ( / 1 10 ) ) )
    ( implies ( and x186 ( and ( not x210 ) true ) ) ( = tmp69 ( / 1 10 ) ) )
    ( implies ( and x186 ( and x210 true ) ) ( = tmp69 ( + ( / 1 10 ) ( / 1 10 ) ) ) )
    ( implies ( and ( not x281 ) true ) ( = tmp68 0 ) )
    ( implies ( and x281 true ) ( = tmp68 ( / 1 10 ) ) )
    ( implies ( and ( not x233 ) ( and ( not x257 ) true ) ) ( = tmp67 0 ) )
    ( implies ( and ( not x233 ) ( and x257 true ) ) ( = tmp67 ( / 1 10 ) ) )
    ( implies ( and x233 ( and ( not x257 ) true ) ) ( = tmp67 ( / 1 10 ) ) )
    ( implies ( and x233 ( and x257 true ) ) ( = tmp67 ( + ( / 1 10 ) ( / 1 10 ) ) ) )
    ( implies ( and ( not x329 ) ( and ( not x305 ) true ) ) ( = tmp66 0 ) )
    ( implies ( and ( not x329 ) ( and x305 true ) ) ( = tmp66 ( / 1 10 ) ) )
    ( implies ( and x329 ( and ( not x305 ) true ) ) ( = tmp66 ( / 1 10 ) ) )
    ( implies ( and x329 ( and x305 true ) ) ( = tmp66 ( + ( / 1 10 ) ( / 1 10 ) ) ) )
    ( implies ( and ( not x185 ) ( and ( not x209 ) true ) ) ( = tmp65 0 ) )
    ( implies ( and ( not x185 ) ( and x209 true ) ) ( = tmp65 ( / 1 10 ) ) )
    ( implies ( and x185 ( and ( not x209 ) true ) ) ( = tmp65 ( / 1 10 ) ) )
    ( implies ( and x185 ( and x209 true ) ) ( = tmp65 ( + ( / 1 10 ) ( / 1 10 ) ) ) )
    ( implies ( and ( not x280 ) true ) ( = tmp64 0 ) )
    ( implies ( and x280 true ) ( = tmp64 ( / 1 10 ) ) )
    ( implies ( and ( not x232 ) ( and ( not x256 ) true ) ) ( = tmp63 0 ) )
    ( implies ( and ( not x232 ) ( and x256 true ) ) ( = tmp63 ( / 1 10 ) ) )
    ( implies ( and x232 ( and ( not x256 ) true ) ) ( = tmp63 ( / 1 10 ) ) )
    ( implies ( and x232 ( and x256 true ) ) ( = tmp63 ( + ( / 1 10 ) ( / 1 10 ) ) ) )
    ( implies ( and ( not x328 ) ( and ( not x304 ) true ) ) ( = tmp62 0 ) )
    ( implies ( and ( not x328 ) ( and x304 true ) ) ( = tmp62 ( / 1 10 ) ) )
    ( implies ( and x328 ( and ( not x304 ) true ) ) ( = tmp62 ( / 1 10 ) ) )
    ( implies ( and x328 ( and x304 true ) ) ( = tmp62 ( + ( / 1 10 ) ( / 1 10 ) ) ) )
    ( implies ( and ( not x184 ) ( and ( not x208 ) true ) ) ( = tmp61 0 ) )
    ( implies ( and ( not x184 ) ( and x208 true ) ) ( = tmp61 ( / 1 10 ) ) )
    ( implies ( and x184 ( and ( not x208 ) true ) ) ( = tmp61 ( / 1 10 ) ) )
    ( implies ( and x184 ( and x208 true ) ) ( = tmp61 ( + ( / 1 10 ) ( / 1 10 ) ) ) )
    ( implies ( and ( not x279 ) true ) ( = tmp60 0 ) )
    ( implies ( and x279 true ) ( = tmp60 ( / 1 10 ) ) )
    ( implies ( and ( not x231 ) ( and ( not x255 ) true ) ) ( = tmp59 0 ) )
    ( implies ( and ( not x231 ) ( and x255 true ) ) ( = tmp59 ( / 1 10 ) ) )
    ( implies ( and x231 ( and ( not x255 ) true ) ) ( = tmp59 ( / 1 10 ) ) )
    ( implies ( and x231 ( and x255 true ) ) ( = tmp59 ( + ( / 1 10 ) ( / 1 10 ) ) ) )
    ( implies ( and ( not x327 ) ( and ( not x303 ) true ) ) ( = tmp58 0 ) )
    ( implies ( and ( not x327 ) ( and x303 true ) ) ( = tmp58 ( / 1 10 ) ) )
    ( implies ( and x327 ( and ( not x303 ) true ) ) ( = tmp58 ( / 1 10 ) ) )
    ( implies ( and x327 ( and x303 true ) ) ( = tmp58 ( + ( / 1 10 ) ( / 1 10 ) ) ) )
    ( implies ( and ( not x183 ) ( and ( not x207 ) true ) ) ( = tmp57 0 ) )
    ( implies ( and ( not x183 ) ( and x207 true ) ) ( = tmp57 ( / 1 10 ) ) )
    ( implies ( and x183 ( and ( not x207 ) true ) ) ( = tmp57 ( / 1 10 ) ) )
    ( implies ( and x183 ( and x207 true ) ) ( = tmp57 ( + ( / 1 10 ) ( / 1 10 ) ) ) )
    ( implies ( and ( not x278 ) true ) ( = tmp56 0 ) )
    ( implies ( and x278 true ) ( = tmp56 ( / 1 10 ) ) )
    ( implies ( and ( not x230 ) ( and ( not x254 ) true ) ) ( = tmp55 0 ) )
    ( implies ( and ( not x230 ) ( and x254 true ) ) ( = tmp55 ( / 1 10 ) ) )
    ( implies ( and x230 ( and ( not x254 ) true ) ) ( = tmp55 ( / 1 10 ) ) )
    ( implies ( and x230 ( and x254 true ) ) ( = tmp55 ( + ( / 1 10 ) ( / 1 10 ) ) ) )
    ( implies ( and ( not x326 ) ( and ( not x302 ) true ) ) ( = tmp54 0 ) )
    ( implies ( and ( not x326 ) ( and x302 true ) ) ( = tmp54 ( / 1 10 ) ) )
    ( implies ( and x326 ( and ( not x302 ) true ) ) ( = tmp54 ( / 1 10 ) ) )
    ( implies ( and x326 ( and x302 true ) ) ( = tmp54 ( + ( / 1 10 ) ( / 1 10 ) ) ) )
    ( implies ( and ( not x182 ) ( and ( not x206 ) true ) ) ( = tmp53 0 ) )
    ( implies ( and ( not x182 ) ( and x206 true ) ) ( = tmp53 ( / 1 10 ) ) )
    ( implies ( and x182 ( and ( not x206 ) true ) ) ( = tmp53 ( / 1 10 ) ) )
    ( implies ( and x182 ( and x206 true ) ) ( = tmp53 ( + ( / 1 10 ) ( / 1 10 ) ) ) )
    ( implies ( and ( not x277 ) true ) ( = tmp52 0 ) )
    ( implies ( and x277 true ) ( = tmp52 ( / 1 10 ) ) )
    ( implies ( and ( not x229 ) ( and ( not x253 ) true ) ) ( = tmp51 0 ) )
    ( implies ( and ( not x229 ) ( and x253 true ) ) ( = tmp51 ( / 1 10 ) ) )
    ( implies ( and x229 ( and ( not x253 ) true ) ) ( = tmp51 ( / 1 10 ) ) )
    ( implies ( and x229 ( and x253 true ) ) ( = tmp51 ( + ( / 1 10 ) ( / 1 10 ) ) ) )
    ( implies ( and ( not x325 ) ( and ( not x301 ) true ) ) ( = tmp50 0 ) )
    ( implies ( and ( not x325 ) ( and x301 true ) ) ( = tmp50 ( / 1 10 ) ) )
    ( implies ( and x325 ( and ( not x301 ) true ) ) ( = tmp50 ( / 1 10 ) ) )
    ( implies ( and x325 ( and x301 true ) ) ( = tmp50 ( + ( / 1 10 ) ( / 1 10 ) ) ) )
    ( implies ( and ( not x181 ) ( and ( not x205 ) true ) ) ( = tmp49 0 ) )
    ( implies ( and ( not x181 ) ( and x205 true ) ) ( = tmp49 ( / 1 10 ) ) )
    ( implies ( and x181 ( and ( not x205 ) true ) ) ( = tmp49 ( / 1 10 ) ) )
    ( implies ( and x181 ( and x205 true ) ) ( = tmp49 ( + ( / 1 10 ) ( / 1 10 ) ) ) )
    ( implies ( and ( not x276 ) true ) ( = tmp48 0 ) )
    ( implies ( and x276 true ) ( = tmp48 ( / 5 100 ) ) )
    ( implies ( and ( not x228 ) ( and ( not x252 ) true ) ) ( = tmp47 0 ) )
    ( implies ( and ( not x228 ) ( and x252 true ) ) ( = tmp47 ( / 5 100 ) ) )
    ( implies ( and x228 ( and ( not x252 ) true ) ) ( = tmp47 ( / 5 100 ) ) )
    ( implies ( and x228 ( and x252 true ) ) ( = tmp47 ( + ( / 5 100 ) ( / 5 100 ) ) ) )
    ( implies ( and ( not x324 ) ( and ( not x300 ) true ) ) ( = tmp46 0 ) )
    ( implies ( and ( not x324 ) ( and x300 true ) ) ( = tmp46 ( / 5 100 ) ) )
    ( implies ( and x324 ( and ( not x300 ) true ) ) ( = tmp46 ( / 5 100 ) ) )
    ( implies ( and x324 ( and x300 true ) ) ( = tmp46 ( + ( / 5 100 ) ( / 5 100 ) ) ) )
    ( implies ( and ( not x180 ) ( and ( not x204 ) true ) ) ( = tmp45 0 ) )
    ( implies ( and ( not x180 ) ( and x204 true ) ) ( = tmp45 ( / 5 100 ) ) )
    ( implies ( and x180 ( and ( not x204 ) true ) ) ( = tmp45 ( / 5 100 ) ) )
    ( implies ( and x180 ( and x204 true ) ) ( = tmp45 ( + ( / 5 100 ) ( / 5 100 ) ) ) )
    ( implies ( and ( not x275 ) true ) ( = tmp44 0 ) )
    ( implies ( and x275 true ) ( = tmp44 ( / 5 100 ) ) )
    ( implies ( and ( not x227 ) ( and ( not x251 ) true ) ) ( = tmp43 0 ) )
    ( implies ( and ( not x227 ) ( and x251 true ) ) ( = tmp43 ( / 5 100 ) ) )
    ( implies ( and x227 ( and ( not x251 ) true ) ) ( = tmp43 ( / 5 100 ) ) )
    ( implies ( and x227 ( and x251 true ) ) ( = tmp43 ( + ( / 5 100 ) ( / 5 100 ) ) ) )
    ( implies ( and ( not x323 ) ( and ( not x299 ) true ) ) ( = tmp42 0 ) )
    ( implies ( and ( not x323 ) ( and x299 true ) ) ( = tmp42 ( / 5 100 ) ) )
    ( implies ( and x323 ( and ( not x299 ) true ) ) ( = tmp42 ( / 5 100 ) ) )
    ( implies ( and x323 ( and x299 true ) ) ( = tmp42 ( + ( / 5 100 ) ( / 5 100 ) ) ) )
    ( implies ( and ( not x179 ) ( and ( not x203 ) true ) ) ( = tmp41 0 ) )
    ( implies ( and ( not x179 ) ( and x203 true ) ) ( = tmp41 ( / 5 100 ) ) )
    ( implies ( and x179 ( and ( not x203 ) true ) ) ( = tmp41 ( / 5 100 ) ) )
    ( implies ( and x179 ( and x203 true ) ) ( = tmp41 ( + ( / 5 100 ) ( / 5 100 ) ) ) )
    ( implies ( and ( not x274 ) true ) ( = tmp40 0 ) )
    ( implies ( and x274 true ) ( = tmp40 ( / 5 100 ) ) )
    ( implies ( and ( not x226 ) ( and ( not x250 ) true ) ) ( = tmp39 0 ) )
    ( implies ( and ( not x226 ) ( and x250 true ) ) ( = tmp39 ( / 5 100 ) ) )
    ( implies ( and x226 ( and ( not x250 ) true ) ) ( = tmp39 ( / 5 100 ) ) )
    ( implies ( and x226 ( and x250 true ) ) ( = tmp39 ( + ( / 5 100 ) ( / 5 100 ) ) ) )
    ( implies ( and ( not x322 ) ( and ( not x298 ) true ) ) ( = tmp38 0 ) )
    ( implies ( and ( not x322 ) ( and x298 true ) ) ( = tmp38 ( / 5 100 ) ) )
    ( implies ( and x322 ( and ( not x298 ) true ) ) ( = tmp38 ( / 5 100 ) ) )
    ( implies ( and x322 ( and x298 true ) ) ( = tmp38 ( + ( / 5 100 ) ( / 5 100 ) ) ) )
    ( implies ( and ( not x178 ) ( and ( not x202 ) true ) ) ( = tmp37 0 ) )
    ( implies ( and ( not x178 ) ( and x202 true ) ) ( = tmp37 ( / 5 100 ) ) )
    ( implies ( and x178 ( and ( not x202 ) true ) ) ( = tmp37 ( / 5 100 ) ) )
    ( implies ( and x178 ( and x202 true ) ) ( = tmp37 ( + ( / 5 100 ) ( / 5 100 ) ) ) )
    ( implies ( and ( not x273 ) true ) ( = tmp36 0 ) )
    ( implies ( and x273 true ) ( = tmp36 ( / 5 100 ) ) )
    ( implies ( and ( not x225 ) ( and ( not x249 ) true ) ) ( = tmp35 0 ) )
    ( implies ( and ( not x225 ) ( and x249 true ) ) ( = tmp35 ( / 5 100 ) ) )
    ( implies ( and x225 ( and ( not x249 ) true ) ) ( = tmp35 ( / 5 100 ) ) )
    ( implies ( and x225 ( and x249 true ) ) ( = tmp35 ( + ( / 5 100 ) ( / 5 100 ) ) ) )
    ( implies ( and ( not x321 ) ( and ( not x297 ) true ) ) ( = tmp34 0 ) )
    ( implies ( and ( not x321 ) ( and x297 true ) ) ( = tmp34 ( / 5 100 ) ) )
    ( implies ( and x321 ( and ( not x297 ) true ) ) ( = tmp34 ( / 5 100 ) ) )
    ( implies ( and x321 ( and x297 true ) ) ( = tmp34 ( + ( / 5 100 ) ( / 5 100 ) ) ) )
    ( implies ( and ( not x177 ) ( and ( not x201 ) true ) ) ( = tmp33 0 ) )
    ( implies ( and ( not x177 ) ( and x201 true ) ) ( = tmp33 ( / 5 100 ) ) )
    ( implies ( and x177 ( and ( not x201 ) true ) ) ( = tmp33 ( / 5 100 ) ) )
    ( implies ( and x177 ( and x201 true ) ) ( = tmp33 ( + ( / 5 100 ) ( / 5 100 ) ) ) )
    ( implies ( and ( not x272 ) true ) ( = tmp32 0 ) )
    ( implies ( and x272 true ) ( = tmp32 ( / 5 100 ) ) )
    ( implies ( and ( not x224 ) ( and ( not x248 ) true ) ) ( = tmp31 0 ) )
    ( implies ( and ( not x224 ) ( and x248 true ) ) ( = tmp31 ( / 5 100 ) ) )
    ( implies ( and x224 ( and ( not x248 ) true ) ) ( = tmp31 ( / 5 100 ) ) )
    ( implies ( and x224 ( and x248 true ) ) ( = tmp31 ( + ( / 5 100 ) ( / 5 100 ) ) ) )
    ( implies ( and ( not x320 ) ( and ( not x296 ) true ) ) ( = tmp30 0 ) )
    ( implies ( and ( not x320 ) ( and x296 true ) ) ( = tmp30 ( / 5 100 ) ) )
    ( implies ( and x320 ( and ( not x296 ) true ) ) ( = tmp30 ( / 5 100 ) ) )
    ( implies ( and x320 ( and x296 true ) ) ( = tmp30 ( + ( / 5 100 ) ( / 5 100 ) ) ) )
    ( implies ( and ( not x176 ) ( and ( not x200 ) true ) ) ( = tmp29 0 ) )
    ( implies ( and ( not x176 ) ( and x200 true ) ) ( = tmp29 ( / 5 100 ) ) )
    ( implies ( and x176 ( and ( not x200 ) true ) ) ( = tmp29 ( / 5 100 ) ) )
    ( implies ( and x176 ( and x200 true ) ) ( = tmp29 ( + ( / 5 100 ) ( / 5 100 ) ) ) )
    ( implies ( and ( not x271 ) true ) ( = tmp28 0 ) )
    ( implies ( and x271 true ) ( = tmp28 ( / 5 100 ) ) )
    ( implies ( and ( not x223 ) ( and ( not x247 ) true ) ) ( = tmp27 0 ) )
    ( implies ( and ( not x223 ) ( and x247 true ) ) ( = tmp27 ( / 5 100 ) ) )
    ( implies ( and x223 ( and ( not x247 ) true ) ) ( = tmp27 ( / 5 100 ) ) )
    ( implies ( and x223 ( and x247 true ) ) ( = tmp27 ( + ( / 5 100 ) ( / 5 100 ) ) ) )
    ( implies ( and ( not x319 ) ( and ( not x295 ) true ) ) ( = tmp26 0 ) )
    ( implies ( and ( not x319 ) ( and x295 true ) ) ( = tmp26 ( / 5 100 ) ) )
    ( implies ( and x319 ( and ( not x295 ) true ) ) ( = tmp26 ( / 5 100 ) ) )
    ( implies ( and x319 ( and x295 true ) ) ( = tmp26 ( + ( / 5 100 ) ( / 5 100 ) ) ) )
    ( implies ( and ( not x175 ) ( and ( not x199 ) true ) ) ( = tmp25 0 ) )
    ( implies ( and ( not x175 ) ( and x199 true ) ) ( = tmp25 ( / 5 100 ) ) )
    ( implies ( and x175 ( and ( not x199 ) true ) ) ( = tmp25 ( / 5 100 ) ) )
    ( implies ( and x175 ( and x199 true ) ) ( = tmp25 ( + ( / 5 100 ) ( / 5 100 ) ) ) )
    ( implies ( and ( not x270 ) true ) ( = tmp24 0 ) )
    ( implies ( and x270 true ) ( = tmp24 ( / 25 1000 ) ) )
    ( implies ( and ( not x222 ) ( and ( not x246 ) true ) ) ( = tmp23 0 ) )
    ( implies ( and ( not x222 ) ( and x246 true ) ) ( = tmp23 ( / 25 1000 ) ) )
    ( implies ( and x222 ( and ( not x246 ) true ) ) ( = tmp23 ( / 25 1000 ) ) )
    ( implies ( and x222 ( and x246 true ) ) ( = tmp23 ( + ( / 25 1000 ) ( / 25 1000 ) ) ) )
    ( implies ( and ( not x318 ) ( and ( not x294 ) true ) ) ( = tmp22 0 ) )
    ( implies ( and ( not x318 ) ( and x294 true ) ) ( = tmp22 ( / 25 1000 ) ) )
    ( implies ( and x318 ( and ( not x294 ) true ) ) ( = tmp22 ( / 25 1000 ) ) )
    ( implies ( and x318 ( and x294 true ) ) ( = tmp22 ( + ( / 25 1000 ) ( / 25 1000 ) ) ) )
    ( implies ( and ( not x174 ) ( and ( not x198 ) true ) ) ( = tmp21 0 ) )
    ( implies ( and ( not x174 ) ( and x198 true ) ) ( = tmp21 ( / 25 1000 ) ) )
    ( implies ( and x174 ( and ( not x198 ) true ) ) ( = tmp21 ( / 25 1000 ) ) )
    ( implies ( and x174 ( and x198 true ) ) ( = tmp21 ( + ( / 25 1000 ) ( / 25 1000 ) ) ) )
    ( implies ( and ( not x269 ) true ) ( = tmp20 0 ) )
    ( implies ( and x269 true ) ( = tmp20 ( / 25 1000 ) ) )
    ( implies ( and ( not x221 ) ( and ( not x245 ) true ) ) ( = tmp19 0 ) )
    ( implies ( and ( not x221 ) ( and x245 true ) ) ( = tmp19 ( / 25 1000 ) ) )
    ( implies ( and x221 ( and ( not x245 ) true ) ) ( = tmp19 ( / 25 1000 ) ) )
    ( implies ( and x221 ( and x245 true ) ) ( = tmp19 ( + ( / 25 1000 ) ( / 25 1000 ) ) ) )
    ( implies ( and ( not x317 ) ( and ( not x293 ) true ) ) ( = tmp18 0 ) )
    ( implies ( and ( not x317 ) ( and x293 true ) ) ( = tmp18 ( / 25 1000 ) ) )
    ( implies ( and x317 ( and ( not x293 ) true ) ) ( = tmp18 ( / 25 1000 ) ) )
    ( implies ( and x317 ( and x293 true ) ) ( = tmp18 ( + ( / 25 1000 ) ( / 25 1000 ) ) ) )
    ( implies ( and ( not x173 ) ( and ( not x197 ) true ) ) ( = tmp17 0 ) )
    ( implies ( and ( not x173 ) ( and x197 true ) ) ( = tmp17 ( / 25 1000 ) ) )
    ( implies ( and x173 ( and ( not x197 ) true ) ) ( = tmp17 ( / 25 1000 ) ) )
    ( implies ( and x173 ( and x197 true ) ) ( = tmp17 ( + ( / 25 1000 ) ( / 25 1000 ) ) ) )
    ( implies ( and ( not x268 ) true ) ( = tmp16 0 ) )
    ( implies ( and x268 true ) ( = tmp16 ( / 25 1000 ) ) )
    ( implies ( and ( not x220 ) ( and ( not x244 ) true ) ) ( = tmp15 0 ) )
    ( implies ( and ( not x220 ) ( and x244 true ) ) ( = tmp15 ( / 25 1000 ) ) )
    ( implies ( and x220 ( and ( not x244 ) true ) ) ( = tmp15 ( / 25 1000 ) ) )
    ( implies ( and x220 ( and x244 true ) ) ( = tmp15 ( + ( / 25 1000 ) ( / 25 1000 ) ) ) )
    ( implies ( and ( not x316 ) ( and ( not x292 ) true ) ) ( = tmp14 0 ) )
    ( implies ( and ( not x316 ) ( and x292 true ) ) ( = tmp14 ( / 25 1000 ) ) )
    ( implies ( and x316 ( and ( not x292 ) true ) ) ( = tmp14 ( / 25 1000 ) ) )
    ( implies ( and x316 ( and x292 true ) ) ( = tmp14 ( + ( / 25 1000 ) ( / 25 1000 ) ) ) )
    ( implies ( and ( not x172 ) ( and ( not x196 ) true ) ) ( = tmp13 0 ) )
    ( implies ( and ( not x172 ) ( and x196 true ) ) ( = tmp13 ( / 25 1000 ) ) )
    ( implies ( and x172 ( and ( not x196 ) true ) ) ( = tmp13 ( / 25 1000 ) ) )
    ( implies ( and x172 ( and x196 true ) ) ( = tmp13 ( + ( / 25 1000 ) ( / 25 1000 ) ) ) )
    ( implies ( and ( not x267 ) true ) ( = tmp12 0 ) )
    ( implies ( and x267 true ) ( = tmp12 ( / 25 1000 ) ) )
    ( implies ( and ( not x219 ) ( and ( not x243 ) true ) ) ( = tmp11 0 ) )
    ( implies ( and ( not x219 ) ( and x243 true ) ) ( = tmp11 ( / 25 1000 ) ) )
    ( implies ( and x219 ( and ( not x243 ) true ) ) ( = tmp11 ( / 25 1000 ) ) )
    ( implies ( and x219 ( and x243 true ) ) ( = tmp11 ( + ( / 25 1000 ) ( / 25 1000 ) ) ) )
    ( implies ( and ( not x315 ) ( and ( not x291 ) true ) ) ( = tmp10 0 ) )
    ( implies ( and ( not x315 ) ( and x291 true ) ) ( = tmp10 ( / 25 1000 ) ) )
    ( implies ( and x315 ( and ( not x291 ) true ) ) ( = tmp10 ( / 25 1000 ) ) )
    ( implies ( and x315 ( and x291 true ) ) ( = tmp10 ( + ( / 25 1000 ) ( / 25 1000 ) ) ) )
    ( implies ( and ( not x171 ) ( and ( not x195 ) true ) ) ( = tmp9 0 ) )
    ( implies ( and ( not x171 ) ( and x195 true ) ) ( = tmp9 ( / 25 1000 ) ) )
    ( implies ( and x171 ( and ( not x195 ) true ) ) ( = tmp9 ( / 25 1000 ) ) )
    ( implies ( and x171 ( and x195 true ) ) ( = tmp9 ( + ( / 25 1000 ) ( / 25 1000 ) ) ) )
    ( implies ( and ( not x266 ) true ) ( = tmp8 0 ) )
    ( implies ( and x266 true ) ( = tmp8 ( / 25 1000 ) ) )
    ( implies ( and ( not x218 ) ( and ( not x242 ) true ) ) ( = tmp7 0 ) )
    ( implies ( and ( not x218 ) ( and x242 true ) ) ( = tmp7 ( / 25 1000 ) ) )
    ( implies ( and x218 ( and ( not x242 ) true ) ) ( = tmp7 ( / 25 1000 ) ) )
    ( implies ( and x218 ( and x242 true ) ) ( = tmp7 ( + ( / 25 1000 ) ( / 25 1000 ) ) ) )
    ( implies ( and ( not x314 ) ( and ( not x290 ) true ) ) ( = tmp6 0 ) )
    ( implies ( and ( not x314 ) ( and x290 true ) ) ( = tmp6 ( / 25 1000 ) ) )
    ( implies ( and x314 ( and ( not x290 ) true ) ) ( = tmp6 ( / 25 1000 ) ) )
    ( implies ( and x314 ( and x290 true ) ) ( = tmp6 ( + ( / 25 1000 ) ( / 25 1000 ) ) ) )
    ( implies ( and ( not x170 ) ( and ( not x194 ) true ) ) ( = tmp5 0 ) )
    ( implies ( and ( not x170 ) ( and x194 true ) ) ( = tmp5 ( / 25 1000 ) ) )
    ( implies ( and x170 ( and ( not x194 ) true ) ) ( = tmp5 ( / 25 1000 ) ) )
    ( implies ( and x170 ( and x194 true ) ) ( = tmp5 ( + ( / 25 1000 ) ( / 25 1000 ) ) ) )
    ( implies ( and ( not x265 ) true ) ( = tmp4 0 ) )
    ( implies ( and x265 true ) ( = tmp4 ( / 25 1000 ) ) )
    ( implies ( and ( not x217 ) ( and ( not x241 ) true ) ) ( = tmp3 0 ) )
    ( implies ( and ( not x217 ) ( and x241 true ) ) ( = tmp3 ( / 25 1000 ) ) )
    ( implies ( and x217 ( and ( not x241 ) true ) ) ( = tmp3 ( / 25 1000 ) ) )
    ( implies ( and x217 ( and x241 true ) ) ( = tmp3 ( + ( / 25 1000 ) ( / 25 1000 ) ) ) )
    ( implies ( and ( not x313 ) ( and ( not x289 ) true ) ) ( = tmp2 0 ) )
    ( implies ( and ( not x313 ) ( and x289 true ) ) ( = tmp2 ( / 25 1000 ) ) )
    ( implies ( and x313 ( and ( not x289 ) true ) ) ( = tmp2 ( / 25 1000 ) ) )
    ( implies ( and x313 ( and x289 true ) ) ( = tmp2 ( + ( / 25 1000 ) ( / 25 1000 ) ) ) )
    ( implies ( and ( not x169 ) ( and ( not x193 ) true ) ) ( = tmp1 0 ) )
    ( implies ( and ( not x169 ) ( and x193 true ) ) ( = tmp1 ( / 25 1000 ) ) )
    ( implies ( and x169 ( and ( not x193 ) true ) ) ( = tmp1 ( / 25 1000 ) ) )
    ( implies ( and x169 ( and x193 true ) ) ( = tmp1 ( + ( / 25 1000 ) ( / 25 1000 ) ) ) )
  )
)