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

  :extrafuns ((tmp419 Real))
  :extrafuns ((tmp418 Real))
  :extrafuns ((tmp417 Real))
  :extrafuns ((tmp416 Real))
  :extrafuns ((tmp415 Real))
  :extrafuns ((tmp414 Real))
  :extrafuns ((tmp413 Real))
  :extrafuns ((tmp412 Real))
  :extrafuns ((tmp411 Real))
  :extrafuns ((tmp410 Real))
  :extrafuns ((tmp409 Real))
  :extrafuns ((tmp408 Real))
  :extrafuns ((tmp407 Real))
  :extrafuns ((tmp406 Real))
  :extrafuns ((tmp405 Real))
  :extrafuns ((tmp404 Real))
  :extrafuns ((tmp403 Real))
  :extrafuns ((tmp402 Real))
  :extrafuns ((tmp401 Real))
  :extrafuns ((tmp400 Real))
  :extrafuns ((tmp399 Real))
  :extrafuns ((tmp398 Real))
  :extrafuns ((tmp397 Real))
  :extrafuns ((tmp396 Real))
  :extrafuns ((tmp395 Real))
  :extrafuns ((tmp394 Real))
  :extrafuns ((tmp393 Real))
  :extrafuns ((tmp392 Real))
  :extrafuns ((tmp391 Real))
  :extrafuns ((tmp390 Real))
  :extrafuns ((tmp389 Real))
  :extrafuns ((tmp388 Real))
  :extrafuns ((tmp387 Real))
  :extrafuns ((tmp386 Real))
  :extrafuns ((tmp385 Real))
  :extrafuns ((tmp384 Real))
  :extrafuns ((tmp383 Real))
  :extrafuns ((tmp382 Real))
  :extrafuns ((tmp381 Real))
  :extrafuns ((tmp380 Real))
  :extrafuns ((tmp379 Real))
  :extrafuns ((tmp378 Real))
  :extrafuns ((tmp377 Real))
  :extrafuns ((tmp376 Real))
  :extrafuns ((tmp375 Real))
  :extrafuns ((tmp374 Real))
  :extrafuns ((tmp373 Real))
  :extrafuns ((tmp372 Real))
  :extrafuns ((tmp371 Real))
  :extrafuns ((tmp370 Real))
  :extrafuns ((tmp369 Real))
  :extrafuns ((tmp368 Real))
  :extrafuns ((tmp367 Real))
  :extrafuns ((tmp366 Real))
  :extrafuns ((tmp365 Real))
  :extrafuns ((tmp364 Real))
  :extrafuns ((tmp363 Real))
  :extrafuns ((tmp362 Real))
  :extrafuns ((tmp361 Real))
  :extrafuns ((tmp360 Real))
  :extrafuns ((tmp359 Real))
  :extrafuns ((tmp358 Real))
  :extrafuns ((tmp357 Real))
  :extrafuns ((tmp356 Real))
  :extrafuns ((tmp355 Real))
  :extrafuns ((tmp354 Real))
  :extrafuns ((tmp353 Real))
  :extrafuns ((tmp352 Real))
  :extrafuns ((tmp351 Real))
  :extrafuns ((tmp350 Real))
  :extrafuns ((tmp349 Real))
  :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 ((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 ((x1 Real))
  :extrapreds ((x2))
  :extrapreds ((x3))
  :extrapreds ((x4))
  :extrapreds ((x5))
  :extrapreds ((x6))
  :extrapreds ((x7))
  :extrapreds ((x8))
  :extrapreds ((x9))
  :extrapreds ((x10))
  :extrapreds ((x11))
  :extrapreds ((x12))
  :extrapreds ((x13))
  :extrapreds ((x14))
  :extrapreds ((x15))
  :extrapreds ((x16))
  :extrapreds ((x17))
  :extrapreds ((x18))
  :extrapreds ((x19))
  :extrapreds ((x20))
  :extrapreds ((x21))
  :extrapreds ((x22))
  :extrapreds ((x23))
  :extrapreds ((x24))
  :extrapreds ((x25))
  :extrapreds ((x26))
  :extrapreds ((x27))
  :extrapreds ((x28))
  :extrapreds ((x29))
  :extrapreds ((x30))
  :extrapreds ((x31))
  :extrapreds ((x32))
  :extrapreds ((x33))
  :extrapreds ((x34))
  :extrapreds ((x35))
  :extrapreds ((x36))
  :extrapreds ((x37))
  :extrapreds ((x38))
  :extrapreds ((x39))
  :extrapreds ((x40))
  :extrapreds ((x41))
  :extrapreds ((x42))
  :extrapreds ((x43))
  :extrapreds ((x44))
  :extrapreds ((x45))
  :extrapreds ((x46))
  :extrapreds ((x47))
  :extrapreds ((x48))
  :extrapreds ((x49))
  :extrapreds ((x50))
  :extrapreds ((x51))
  :extrapreds ((x52))
  :extrapreds ((x53))
  :extrapreds ((x54))
  :extrapreds ((x55))
  :extrapreds ((x56))

  :formula( and
    ( <= ( + 0 ( * 1 x1 ) ) 20 )
    ( >= ( + ( + 0 ( * 1 x1 ) ) ( * (~ 1) x86 ) ) 0 )
    ( >= ( + ( + 0 ( * 1 x1 ) ) ( * (~ 1) x85 ) ) 0 )
    ( >= ( + ( + 0 ( * 1 x1 ) ) ( * (~ 1) x84 ) ) 0 )
    ( >= ( + ( + 0 ( * 1 x1 ) ) ( * (~ 1) x83 ) ) 0 )
    ( >= ( + ( + 0 ( * 1 x1 ) ) ( * (~ 1) x82 ) ) 0 )
    ( >= ( + ( + 0 ( * 1 x1 ) ) ( * (~ 1) x81 ) ) 0 )
    ( >= ( + ( + 0 ( * 1 x1 ) ) ( * (~ 1) x80 ) ) 0 )
    ( >= ( + ( + 0 ( * 1 x1 ) ) ( * (~ 1) x79 ) ) 0 )
    ( >= ( + ( + 0 ( * 1 x1 ) ) ( * (~ 1) x78 ) ) 0 )
    ( >= ( + ( + 0 ( * 1 x1 ) ) ( * (~ 1) x77 ) ) 0 )
    ( >= ( + ( + 0 ( * 1 x1 ) ) ( * (~ 1) x76 ) ) 0 )
    ( >= ( + ( + 0 ( * 1 x1 ) ) ( * (~ 1) x75 ) ) 0 )
    ( >= ( + ( + 0 ( * 1 x1 ) ) ( * (~ 1) x74 ) ) 0 )
    ( >= ( + ( + 0 ( * 1 x1 ) ) ( * (~ 1) x73 ) ) 0 )
    ( >= ( + ( + 0 ( * 1 x1 ) ) ( * (~ 1) x72 ) ) 0 )
    ( >= ( + ( + 0 ( * 1 x1 ) ) ( * (~ 1) x71 ) ) 0 )
    ( >= ( + ( + 0 ( * 1 x1 ) ) ( * (~ 1) x70 ) ) 0 )
    ( >= ( + ( + 0 ( * 1 x1 ) ) ( * (~ 1) x69 ) ) 0 )
    ( >= ( + ( + 0 ( * 1 x1 ) ) ( * (~ 1) x68 ) ) 0 )
    ( >= ( + ( + 0 ( * 1 x1 ) ) ( * (~ 1) x67 ) ) 0 )
    ( >= ( + ( + 0 ( * 1 x1 ) ) ( * (~ 1) x66 ) ) 0 )
    ( >= ( + ( + 0 ( * 1 x1 ) ) ( * (~ 1) x65 ) ) 0 )
    ( >= ( + ( + 0 ( * 1 x1 ) ) ( * (~ 1) x64 ) ) 0 )
    ( >= ( + ( + 0 ( * 1 x1 ) ) ( * (~ 1) x63 ) ) 0 )
    ( >= ( + ( + 0 ( * 1 x1 ) ) ( * (~ 1) x62 ) ) 0 )
    ( >= ( + ( + 0 ( * 1 x1 ) ) ( * (~ 1) x61 ) ) 0 )
    ( >= ( + ( + 0 ( * 1 x1 ) ) ( * (~ 1) x60 ) ) 0 )
    ( >= ( + ( + 0 ( * 1 x1 ) ) ( * (~ 1) x59 ) ) 0 )
    ( >= ( + ( + 0 ( * 1 x1 ) ) ( * (~ 1) x58 ) ) 0 )
    ( >= ( + ( + 0 ( * 1 x1 ) ) ( * (~ 1) x57 ) ) 0 )
    ( = ( + ( + ( * 1 tmp419 ) 0 ) ( + ( * 1 tmp417 ) ( + ( * 1 tmp415 ) ( + ( * 1 tmp413 ) ( + ( * 1 tmp411 ) ( + ( * 1 tmp409 ) ( + ( * 1 tmp407 ) ( + ( * 1 tmp405 ) ( + ( * 1 tmp403 ) ( + ( * 1 tmp401 ) ( + ( * 1 tmp399 ) ( + ( * 1 tmp397 ) ( + ( * 1 tmp395 ) ( + ( * 1 tmp393 ) ( + ( * 1 x85 ) ( + ( * (~ 1) x86 ) ( + ( * 1 tmp392 ) ( + ( * 1 tmp394 ) ( + ( * 1 tmp396 ) ( + ( * 1 tmp398 ) ( + ( * 1 tmp400 ) ( + ( * 1 tmp402 ) ( + ( * 1 tmp404 ) ( + ( * 1 tmp406 ) ( + ( * 1 tmp408 ) ( + ( * 1 tmp410 ) ( + ( * 1 tmp412 ) ( + ( * 1 tmp414 ) ( + ( * 1 tmp416 ) ( + ( * 1 tmp418 ) 0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) 731 )
    ( = ( + ( + ( * 1 tmp391 ) 0 ) ( + ( * 1 tmp389 ) ( + ( * 1 tmp388 ) ( + ( * 1 tmp386 ) ( + ( * 1 tmp384 ) ( + ( * 1 tmp382 ) ( + ( * 1 tmp380 ) ( + ( * 1 tmp378 ) ( + ( * 1 tmp376 ) ( + ( * 1 tmp374 ) ( + ( * 1 tmp372 ) ( + ( * 1 tmp370 ) ( + ( * 1 tmp368 ) ( + ( * 1 tmp366 ) ( + ( * 1 x83 ) ( + ( * (~ 1) x84 ) ( + ( * 1 tmp365 ) ( + ( * 1 tmp367 ) ( + ( * 1 tmp369 ) ( + ( * 1 tmp371 ) ( + ( * 1 tmp373 ) ( + ( * 1 tmp375 ) ( + ( * 1 tmp377 ) ( + ( * 1 tmp379 ) ( + ( * 1 tmp381 ) ( + ( * 1 tmp383 ) ( + ( * 1 tmp385 ) ( + ( * 1 tmp387 ) ( + ( * 1 tmp221 ) ( + ( * 1 tmp390 ) 0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) 731 )
    ( = ( + ( + ( * 1 tmp364 ) 0 ) ( + ( * 1 tmp362 ) ( + ( * 1 tmp360 ) ( + ( * 1 tmp358 ) ( + ( * 1 tmp356 ) ( + ( * 1 tmp354 ) ( + ( * 1 tmp352 ) ( + ( * 1 tmp350 ) ( + ( * 1 tmp348 ) ( + ( * 1 tmp346 ) ( + ( * 1 tmp344 ) ( + ( * 1 tmp342 ) ( + ( * 1 tmp340 ) ( + ( * 1 tmp338 ) ( + ( * 1 x81 ) ( + ( * (~ 1) x82 ) ( + ( * 1 tmp337 ) ( + ( * 1 tmp339 ) ( + ( * 1 tmp341 ) ( + ( * 1 tmp343 ) ( + ( * 1 tmp345 ) ( + ( * 1 tmp347 ) ( + ( * 1 tmp349 ) ( + ( * 1 tmp351 ) ( + ( * 1 tmp353 ) ( + ( * 1 tmp355 ) ( + ( * 1 tmp357 ) ( + ( * 1 tmp359 ) ( + ( * 1 tmp361 ) ( + ( * 1 tmp363 ) 0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) 731 )
    ( = ( + ( + ( * 1 tmp336 ) 0 ) ( + ( * 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 x79 ) ( + ( * (~ 1) x80 ) ( + ( * 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 ) 0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) 731 )
    ( = ( + ( + ( * 1 tmp308 ) 0 ) ( + ( * 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 x77 ) ( + ( * (~ 1) x78 ) ( + ( * 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 ) 0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) 731 )
    ( = ( + ( + ( * 1 tmp280 ) 0 ) ( + ( * 1 tmp278 ) ( + ( * 1 tmp276 ) ( + ( * 1 tmp274 ) ( + ( * 1 tmp272 ) ( + ( * 1 tmp270 ) ( + ( * 1 tmp268 ) ( + ( * 1 tmp266 ) ( + ( * 1 tmp264 ) ( + ( * 1 tmp262 ) ( + ( * 1 tmp260 ) ( + ( * 1 tmp258 ) ( + ( * 1 tmp256 ) ( + ( * 1 tmp254 ) ( + ( * 1 x75 ) ( + ( * (~ 1) x76 ) ( + ( * 1 tmp253 ) ( + ( * 1 tmp255 ) ( + ( * 1 tmp257 ) ( + ( * 1 tmp259 ) ( + ( * 1 tmp261 ) ( + ( * 1 tmp263 ) ( + ( * 1 tmp265 ) ( + ( * 1 tmp267 ) ( + ( * 1 tmp269 ) ( + ( * 1 tmp271 ) ( + ( * 1 tmp273 ) ( + ( * 1 tmp275 ) ( + ( * 1 tmp277 ) ( + ( * 1 tmp279 ) 0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) 731 )
    ( = ( + ( + ( * 1 tmp252 ) 0 ) ( + ( * 1 tmp250 ) ( + ( * 1 tmp248 ) ( + ( * 1 tmp246 ) ( + ( * 1 tmp244 ) ( + ( * 1 tmp242 ) ( + ( * 1 tmp240 ) ( + ( * 1 tmp238 ) ( + ( * 1 tmp236 ) ( + ( * 1 tmp234 ) ( + ( * 1 tmp232 ) ( + ( * 1 tmp230 ) ( + ( * 1 tmp228 ) ( + ( * 1 tmp226 ) ( + ( * 1 x73 ) ( + ( * (~ 1) x74 ) ( + ( * 1 tmp225 ) ( + ( * 1 tmp227 ) ( + ( * 1 tmp229 ) ( + ( * 1 tmp231 ) ( + ( * 1 tmp233 ) ( + ( * 1 tmp235 ) ( + ( * 1 tmp237 ) ( + ( * 1 tmp239 ) ( + ( * 1 tmp241 ) ( + ( * 1 tmp243 ) ( + ( * 1 tmp245 ) ( + ( * 1 tmp247 ) ( + ( * 1 tmp249 ) ( + ( * 1 tmp251 ) 0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) 731 )
    ( = ( + ( + ( * 1 tmp224 ) 0 ) ( + ( * 1 tmp222 ) ( + ( * 1 tmp220 ) ( + ( * 1 tmp218 ) ( + ( * 1 tmp216 ) ( + ( * 1 tmp214 ) ( + ( * 1 tmp212 ) ( + ( * 1 tmp210 ) ( + ( * 1 tmp208 ) ( + ( * 1 tmp206 ) ( + ( * 1 tmp204 ) ( + ( * 1 tmp202 ) ( + ( * 1 tmp200 ) ( + ( * 1 tmp198 ) ( + ( * 1 x71 ) ( + ( * (~ 1) x72 ) ( + ( * 1 tmp197 ) ( + ( * 1 tmp199 ) ( + ( * 1 tmp201 ) ( + ( * 1 tmp203 ) ( + ( * 1 tmp205 ) ( + ( * 1 tmp207 ) ( + ( * 1 tmp209 ) ( + ( * 1 tmp211 ) ( + ( * 1 tmp213 ) ( + ( * 1 tmp215 ) ( + ( * 1 tmp217 ) ( + ( * 1 tmp219 ) ( + ( * 1 tmp221 ) ( + ( * 1 tmp223 ) 0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) 731 )
    ( = ( + ( + ( * 1 tmp196 ) 0 ) ( + ( * 1 tmp194 ) ( + ( * 1 tmp192 ) ( + ( * 1 tmp190 ) ( + ( * 1 tmp188 ) ( + ( * 1 tmp186 ) ( + ( * 1 tmp184 ) ( + ( * 1 tmp182 ) ( + ( * 1 tmp180 ) ( + ( * 1 tmp178 ) ( + ( * 1 tmp176 ) ( + ( * 1 tmp174 ) ( + ( * 1 tmp172 ) ( + ( * 1 tmp170 ) ( + ( * 1 x69 ) ( + ( * (~ 1) x70 ) ( + ( * 1 tmp169 ) ( + ( * 1 tmp171 ) ( + ( * 1 tmp173 ) ( + ( * 1 tmp175 ) ( + ( * 1 tmp177 ) ( + ( * 1 tmp179 ) ( + ( * 1 tmp181 ) ( + ( * 1 tmp183 ) ( + ( * 1 tmp185 ) ( + ( * 1 tmp187 ) ( + ( * 1 tmp189 ) ( + ( * 1 tmp191 ) ( + ( * 1 tmp193 ) ( + ( * 1 tmp195 ) 0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) 731 )
    ( = ( + ( + ( * 1 tmp168 ) 0 ) ( + ( * 1 tmp166 ) ( + ( * 1 tmp164 ) ( + ( * 1 tmp162 ) ( + ( * 1 tmp160 ) ( + ( * 1 tmp158 ) ( + ( * 1 tmp156 ) ( + ( * 1 tmp154 ) ( + ( * 1 tmp152 ) ( + ( * 1 tmp150 ) ( + ( * 1 tmp148 ) ( + ( * 1 tmp146 ) ( + ( * 1 tmp144 ) ( + ( * 1 tmp142 ) ( + ( * 1 x67 ) ( + ( * (~ 1) x68 ) ( + ( * 1 tmp141 ) ( + ( * 1 tmp143 ) ( + ( * 1 tmp145 ) ( + ( * 1 tmp147 ) ( + ( * 1 tmp149 ) ( + ( * 1 tmp151 ) ( + ( * 1 tmp153 ) ( + ( * 1 tmp155 ) ( + ( * 1 tmp157 ) ( + ( * 1 tmp159 ) ( + ( * 1 tmp161 ) ( + ( * 1 tmp163 ) ( + ( * 1 tmp165 ) ( + ( * 1 tmp167 ) 0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) 731 )
    ( = ( + ( + ( * 1 tmp140 ) 0 ) ( + ( * 1 tmp138 ) ( + ( * 1 tmp136 ) ( + ( * 1 tmp134 ) ( + ( * 1 tmp132 ) ( + ( * 1 tmp130 ) ( + ( * 1 tmp128 ) ( + ( * 1 tmp126 ) ( + ( * 1 tmp124 ) ( + ( * 1 tmp122 ) ( + ( * 1 tmp120 ) ( + ( * 1 tmp118 ) ( + ( * 1 tmp116 ) ( + ( * 1 tmp114 ) ( + ( * 1 x65 ) ( + ( * (~ 1) x66 ) ( + ( * 1 tmp113 ) ( + ( * 1 tmp115 ) ( + ( * 1 tmp117 ) ( + ( * 1 tmp119 ) ( + ( * 1 tmp121 ) ( + ( * 1 tmp123 ) ( + ( * 1 tmp125 ) ( + ( * 1 tmp127 ) ( + ( * 1 tmp129 ) ( + ( * 1 tmp131 ) ( + ( * 1 tmp133 ) ( + ( * 1 tmp135 ) ( + ( * 1 tmp137 ) ( + ( * 1 tmp139 ) 0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) 731 )
    ( = ( + ( + ( * 1 tmp112 ) 0 ) ( + ( * 1 tmp110 ) ( + ( * 1 tmp108 ) ( + ( * 1 tmp106 ) ( + ( * 1 tmp104 ) ( + ( * 1 tmp102 ) ( + ( * 1 tmp100 ) ( + ( * 1 tmp98 ) ( + ( * 1 tmp96 ) ( + ( * 1 tmp94 ) ( + ( * 1 tmp92 ) ( + ( * 1 tmp90 ) ( + ( * 1 tmp88 ) ( + ( * 1 tmp86 ) ( + ( * 1 x63 ) ( + ( * (~ 1) x64 ) ( + ( * 1 tmp85 ) ( + ( * 1 tmp87 ) ( + ( * 1 tmp89 ) ( + ( * 1 tmp91 ) ( + ( * 1 tmp93 ) ( + ( * 1 tmp95 ) ( + ( * 1 tmp97 ) ( + ( * 1 tmp99 ) ( + ( * 1 tmp101 ) ( + ( * 1 tmp103 ) ( + ( * 1 tmp105 ) ( + ( * 1 tmp107 ) ( + ( * 1 tmp109 ) ( + ( * 1 tmp111 ) 0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) 731 )
    ( = ( + ( + ( * 1 tmp84 ) 0 ) ( + ( * 1 tmp82 ) ( + ( * 1 tmp80 ) ( + ( * 1 tmp78 ) ( + ( * 1 tmp76 ) ( + ( * 1 tmp74 ) ( + ( * 1 tmp72 ) ( + ( * 1 tmp70 ) ( + ( * 1 tmp68 ) ( + ( * 1 tmp66 ) ( + ( * 1 tmp64 ) ( + ( * 1 tmp62 ) ( + ( * 1 tmp60 ) ( + ( * 1 tmp58 ) ( + ( * 1 x61 ) ( + ( * (~ 1) x62 ) ( + ( * 1 tmp57 ) ( + ( * 1 tmp59 ) ( + ( * 1 tmp61 ) ( + ( * 1 tmp63 ) ( + ( * 1 tmp65 ) ( + ( * 1 tmp67 ) ( + ( * 1 tmp69 ) ( + ( * 1 tmp71 ) ( + ( * 1 tmp73 ) ( + ( * 1 tmp75 ) ( + ( * 1 tmp77 ) ( + ( * 1 tmp79 ) ( + ( * 1 tmp81 ) ( + ( * 1 tmp83 ) 0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) 731 )
    ( = ( + ( + ( * 1 tmp56 ) 0 ) ( + ( * 1 tmp54 ) ( + ( * 1 tmp52 ) ( + ( * 1 tmp50 ) ( + ( * 1 tmp48 ) ( + ( * 1 tmp46 ) ( + ( * 1 tmp44 ) ( + ( * 1 tmp42 ) ( + ( * 1 tmp40 ) ( + ( * 1 tmp38 ) ( + ( * 1 tmp36 ) ( + ( * 1 tmp34 ) ( + ( * 1 tmp32 ) ( + ( * 1 tmp30 ) ( + ( * 1 x59 ) ( + ( * (~ 1) x60 ) ( + ( * 1 tmp29 ) ( + ( * 1 tmp31 ) ( + ( * 1 tmp33 ) ( + ( * 1 tmp35 ) ( + ( * 1 tmp37 ) ( + ( * 1 tmp39 ) ( + ( * 1 tmp41 ) ( + ( * 1 tmp43 ) ( + ( * 1 tmp45 ) ( + ( * 1 tmp47 ) ( + ( * 1 tmp49 ) ( + ( * 1 tmp51 ) ( + ( * 1 tmp53 ) ( + ( * 1 tmp55 ) 0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) 731 )
    ( = ( + ( + ( * 1 tmp28 ) 0 ) ( + ( * 1 tmp26 ) ( + ( * 1 tmp24 ) ( + ( * 1 tmp22 ) ( + ( * 1 tmp20 ) ( + ( * 1 tmp18 ) ( + ( * 1 tmp16 ) ( + ( * 1 tmp14 ) ( + ( * 1 tmp12 ) ( + ( * 1 tmp10 ) ( + ( * 1 tmp8 ) ( + ( * 1 tmp6 ) ( + ( * 1 tmp4 ) ( + ( * 1 tmp2 ) ( + ( * 1 x57 ) ( + ( * (~ 1) x58 ) ( + ( * 1 tmp1 ) ( + ( * 1 tmp3 ) ( + ( * 1 tmp5 ) ( + ( * 1 tmp7 ) ( + ( * 1 tmp9 ) ( + ( * 1 tmp11 ) ( + ( * 1 tmp13 ) ( + ( * 1 tmp15 ) ( + ( * 1 tmp17 ) ( + ( * 1 tmp19 ) ( + ( * 1 tmp21 ) ( + ( * 1 tmp23 ) ( + ( * 1 tmp25 ) ( + ( * 1 tmp27 ) 0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) 731 )
    ( >= x1 0 )
    ( >= x86 0 )
    ( >= x85 0 )
    ( >= x84 0 )
    ( >= x83 0 )
    ( >= x82 0 )
    ( >= x81 0 )
    ( >= x80 0 )
    ( >= x79 0 )
    ( >= x78 0 )
    ( >= x77 0 )
    ( >= x76 0 )
    ( >= x75 0 )
    ( >= x74 0 )
    ( >= x73 0 )
    ( >= x72 0 )
    ( >= x71 0 )
    ( >= x70 0 )
    ( >= x69 0 )
    ( >= x68 0 )
    ( >= x67 0 )
    ( >= x66 0 )
    ( >= x65 0 )
    ( >= x64 0 )
    ( >= x63 0 )
    ( >= x62 0 )
    ( >= x61 0 )
    ( >= x60 0 )
    ( >= x59 0 )
    ( >= x58 0 )
    ( >= x57 0 )
    ( implies ( and ( not x30 ) true ) ( = tmp419 0 ) )
    ( implies ( and x30 true ) ( = tmp419 6 ) )
    ( implies ( and ( not x28 ) ( and ( not x29 ) true ) ) ( = tmp418 0 ) )
    ( implies ( and ( not x28 ) ( and x29 true ) ) ( = tmp418 23 ) )
    ( implies ( and x28 ( and ( not x29 ) true ) ) ( = tmp418 39 ) )
    ( implies ( and x28 ( and x29 true ) ) ( = tmp418 62 ) )
    ( implies ( and ( not x32 ) ( and ( not x31 ) true ) ) ( = tmp417 0 ) )
    ( implies ( and ( not x32 ) ( and x31 true ) ) ( = tmp417 20 ) )
    ( implies ( and x32 ( and ( not x31 ) true ) ) ( = tmp417 36 ) )
    ( implies ( and x32 ( and x31 true ) ) ( = tmp417 56 ) )
    ( implies ( and ( not x26 ) ( and ( not x27 ) true ) ) ( = tmp416 0 ) )
    ( implies ( and ( not x26 ) ( and x27 true ) ) ( = tmp416 28 ) )
    ( implies ( and x26 ( and ( not x27 ) true ) ) ( = tmp416 39 ) )
    ( implies ( and x26 ( and x27 true ) ) ( = tmp416 67 ) )
    ( implies ( and ( not x34 ) ( and ( not x33 ) true ) ) ( = tmp415 0 ) )
    ( implies ( and ( not x34 ) ( and x33 true ) ) ( = tmp415 29 ) )
    ( implies ( and x34 ( and ( not x33 ) true ) ) ( = tmp415 12 ) )
    ( implies ( and x34 ( and x33 true ) ) ( = tmp415 41 ) )
    ( implies ( and ( not x24 ) ( and ( not x25 ) true ) ) ( = tmp414 0 ) )
    ( implies ( and ( not x24 ) ( and x25 true ) ) ( = tmp414 55 ) )
    ( implies ( and x24 ( and ( not x25 ) true ) ) ( = tmp414 44 ) )
    ( implies ( and x24 ( and x25 true ) ) ( = tmp414 99 ) )
    ( implies ( and ( not x36 ) ( and ( not x35 ) true ) ) ( = tmp413 0 ) )
    ( implies ( and ( not x36 ) ( and x35 true ) ) ( = tmp413 48 ) )
    ( implies ( and x36 ( and ( not x35 ) true ) ) ( = tmp413 6 ) )
    ( implies ( and x36 ( and x35 true ) ) ( = tmp413 54 ) )
    ( implies ( and ( not x22 ) ( and ( not x23 ) true ) ) ( = tmp412 0 ) )
    ( implies ( and ( not x22 ) ( and x23 true ) ) ( = tmp412 15 ) )
    ( implies ( and x22 ( and ( not x23 ) true ) ) ( = tmp412 35 ) )
    ( implies ( and x22 ( and x23 true ) ) ( = tmp412 50 ) )
    ( implies ( and ( not x38 ) ( and ( not x37 ) true ) ) ( = tmp411 0 ) )
    ( implies ( and ( not x38 ) ( and x37 true ) ) ( = tmp411 35 ) )
    ( implies ( and x38 ( and ( not x37 ) true ) ) ( = tmp411 8 ) )
    ( implies ( and x38 ( and x37 true ) ) ( = tmp411 43 ) )
    ( implies ( and ( not x20 ) ( and ( not x21 ) true ) ) ( = tmp410 0 ) )
    ( implies ( and ( not x20 ) ( and x21 true ) ) ( = tmp410 33 ) )
    ( implies ( and x20 ( and ( not x21 ) true ) ) ( = tmp410 19 ) )
    ( implies ( and x20 ( and x21 true ) ) ( = tmp410 52 ) )
    ( implies ( and ( not x40 ) ( and ( not x39 ) true ) ) ( = tmp409 0 ) )
    ( implies ( and ( not x40 ) ( and x39 true ) ) ( = tmp409 33 ) )
    ( implies ( and x40 ( and ( not x39 ) true ) ) ( = tmp409 46 ) )
    ( implies ( and x40 ( and x39 true ) ) ( = tmp409 79 ) )
    ( implies ( and ( not x18 ) ( and ( not x19 ) true ) ) ( = tmp408 0 ) )
    ( implies ( and ( not x18 ) ( and x19 true ) ) ( = tmp408 47 ) )
    ( implies ( and x18 ( and ( not x19 ) true ) ) ( = tmp408 13 ) )
    ( implies ( and x18 ( and x19 true ) ) ( = tmp408 60 ) )
    ( implies ( and ( not x42 ) ( and ( not x41 ) true ) ) ( = tmp407 0 ) )
    ( implies ( and ( not x42 ) ( and x41 true ) ) ( = tmp407 15 ) )
    ( implies ( and x42 ( and ( not x41 ) true ) ) ( = tmp407 37 ) )
    ( implies ( and x42 ( and x41 true ) ) ( = tmp407 52 ) )
    ( implies ( and ( not x16 ) ( and ( not x17 ) true ) ) ( = tmp406 0 ) )
    ( implies ( and ( not x16 ) ( and x17 true ) ) ( = tmp406 55 ) )
    ( implies ( and x16 ( and ( not x17 ) true ) ) ( = tmp406 22 ) )
    ( implies ( and x16 ( and x17 true ) ) ( = tmp406 77 ) )
    ( implies ( and ( not x44 ) ( and ( not x43 ) true ) ) ( = tmp405 0 ) )
    ( implies ( and ( not x44 ) ( and x43 true ) ) ( = tmp405 11 ) )
    ( implies ( and x44 ( and ( not x43 ) true ) ) ( = tmp405 44 ) )
    ( implies ( and x44 ( and x43 true ) ) ( = tmp405 55 ) )
    ( implies ( and ( not x14 ) ( and ( not x15 ) true ) ) ( = tmp404 0 ) )
    ( implies ( and ( not x14 ) ( and x15 true ) ) ( = tmp404 54 ) )
    ( implies ( and x14 ( and ( not x15 ) true ) ) ( = tmp404 15 ) )
    ( implies ( and x14 ( and x15 true ) ) ( = tmp404 69 ) )
    ( implies ( and ( not x46 ) ( and ( not x45 ) true ) ) ( = tmp403 0 ) )
    ( implies ( and ( not x46 ) ( and x45 true ) ) ( = tmp403 48 ) )
    ( implies ( and x46 ( and ( not x45 ) true ) ) ( = tmp403 9 ) )
    ( implies ( and x46 ( and x45 true ) ) ( = tmp403 57 ) )
    ( implies ( and ( not x12 ) ( and ( not x13 ) true ) ) ( = tmp402 0 ) )
    ( implies ( and ( not x12 ) ( and x13 true ) ) ( = tmp402 33 ) )
    ( implies ( and x12 ( and ( not x13 ) true ) ) ( = tmp402 21 ) )
    ( implies ( and x12 ( and x13 true ) ) ( = tmp402 54 ) )
    ( implies ( and ( not x48 ) ( and ( not x47 ) true ) ) ( = tmp401 0 ) )
    ( implies ( and ( not x48 ) ( and x47 true ) ) ( = tmp401 11 ) )
    ( implies ( and x48 ( and ( not x47 ) true ) ) ( = tmp401 47 ) )
    ( implies ( and x48 ( and x47 true ) ) ( = tmp401 58 ) )
    ( implies ( and ( not x10 ) ( and ( not x11 ) true ) ) ( = tmp400 0 ) )
    ( implies ( and ( not x10 ) ( and x11 true ) ) ( = tmp400 8 ) )
    ( implies ( and x10 ( and ( not x11 ) true ) ) ( = tmp400 11 ) )
    ( implies ( and x10 ( and x11 true ) ) ( = tmp400 19 ) )
    ( implies ( and ( not x50 ) ( and ( not x49 ) true ) ) ( = tmp399 0 ) )
    ( implies ( and ( not x50 ) ( and x49 true ) ) ( = tmp399 18 ) )
    ( implies ( and x50 ( and ( not x49 ) true ) ) ( = tmp399 54 ) )
    ( implies ( and x50 ( and x49 true ) ) ( = tmp399 72 ) )
    ( implies ( and ( not x8 ) ( and ( not x9 ) true ) ) ( = tmp398 0 ) )
    ( implies ( and ( not x8 ) ( and x9 true ) ) ( = tmp398 15 ) )
    ( implies ( and x8 ( and ( not x9 ) true ) ) ( = tmp398 32 ) )
    ( implies ( and x8 ( and x9 true ) ) ( = tmp398 47 ) )
    ( implies ( and ( not x52 ) ( and ( not x51 ) true ) ) ( = tmp397 0 ) )
    ( implies ( and ( not x52 ) ( and x51 true ) ) ( = tmp397 10 ) )
    ( implies ( and x52 ( and ( not x51 ) true ) ) ( = tmp397 46 ) )
    ( implies ( and x52 ( and x51 true ) ) ( = tmp397 56 ) )
    ( implies ( and ( not x6 ) ( and ( not x7 ) true ) ) ( = tmp396 0 ) )
    ( implies ( and ( not x6 ) ( and x7 true ) ) ( = tmp396 16 ) )
    ( implies ( and x6 ( and ( not x7 ) true ) ) ( = tmp396 28 ) )
    ( implies ( and x6 ( and x7 true ) ) ( = tmp396 44 ) )
    ( implies ( and ( not x54 ) ( and ( not x53 ) true ) ) ( = tmp395 0 ) )
    ( implies ( and ( not x54 ) ( and x53 true ) ) ( = tmp395 34 ) )
    ( implies ( and x54 ( and ( not x53 ) true ) ) ( = tmp395 20 ) )
    ( implies ( and x54 ( and x53 true ) ) ( = tmp395 54 ) )
    ( implies ( and ( not x4 ) ( and ( not x5 ) true ) ) ( = tmp394 0 ) )
    ( implies ( and ( not x4 ) ( and x5 true ) ) ( = tmp394 32 ) )
    ( implies ( and x4 ( and ( not x5 ) true ) ) ( = tmp394 16 ) )
    ( implies ( and x4 ( and x5 true ) ) ( = tmp394 48 ) )
    ( implies ( and ( not x56 ) ( and ( not x55 ) true ) ) ( = tmp393 0 ) )
    ( implies ( and ( not x56 ) ( and x55 true ) ) ( = tmp393 35 ) )
    ( implies ( and x56 ( and ( not x55 ) true ) ) ( = tmp393 33 ) )
    ( implies ( and x56 ( and x55 true ) ) ( = tmp393 68 ) )
    ( implies ( and ( not x2 ) ( and ( not x3 ) true ) ) ( = tmp392 0 ) )
    ( implies ( and ( not x2 ) ( and x3 true ) ) ( = tmp392 47 ) )
    ( implies ( and x2 ( and ( not x3 ) true ) ) ( = tmp392 28 ) )
    ( implies ( and x2 ( and x3 true ) ) ( = tmp392 75 ) )
    ( implies ( and ( not x30 ) true ) ( = tmp391 0 ) )
    ( implies ( and x30 true ) ( = tmp391 37 ) )
    ( implies ( and ( not x28 ) ( and ( not x29 ) true ) ) ( = tmp390 0 ) )
    ( implies ( and ( not x28 ) ( and x29 true ) ) ( = tmp390 9 ) )
    ( implies ( and x28 ( and ( not x29 ) true ) ) ( = tmp390 54 ) )
    ( implies ( and x28 ( and x29 true ) ) ( = tmp390 63 ) )
    ( implies ( and ( not x32 ) ( and ( not x31 ) true ) ) ( = tmp389 0 ) )
    ( implies ( and ( not x32 ) ( and x31 true ) ) ( = tmp389 55 ) )
    ( implies ( and x32 ( and ( not x31 ) true ) ) ( = tmp389 55 ) )
    ( implies ( and x32 ( and x31 true ) ) ( = tmp389 110 ) )
    ( implies ( and ( not x34 ) ( and ( not x33 ) true ) ) ( = tmp388 0 ) )
    ( implies ( and ( not x34 ) ( and x33 true ) ) ( = tmp388 42 ) )
    ( implies ( and x34 ( and ( not x33 ) true ) ) ( = tmp388 51 ) )
    ( implies ( and x34 ( and x33 true ) ) ( = tmp388 93 ) )
    ( implies ( and ( not x24 ) ( and ( not x25 ) true ) ) ( = tmp387 0 ) )
    ( implies ( and ( not x24 ) ( and x25 true ) ) ( = tmp387 34 ) )
    ( implies ( and x24 ( and ( not x25 ) true ) ) ( = tmp387 54 ) )
    ( implies ( and x24 ( and x25 true ) ) ( = tmp387 88 ) )
    ( implies ( and ( not x36 ) ( and ( not x35 ) true ) ) ( = tmp386 0 ) )
    ( implies ( and ( not x36 ) ( and x35 true ) ) ( = tmp386 32 ) )
    ( implies ( and x36 ( and ( not x35 ) true ) ) ( = tmp386 10 ) )
    ( implies ( and x36 ( and x35 true ) ) ( = tmp386 42 ) )
    ( implies ( and ( not x22 ) ( and ( not x23 ) true ) ) ( = tmp385 0 ) )
    ( implies ( and ( not x22 ) ( and x23 true ) ) ( = tmp385 50 ) )
    ( implies ( and x22 ( and ( not x23 ) true ) ) ( = tmp385 14 ) )
    ( implies ( and x22 ( and x23 true ) ) ( = tmp385 64 ) )
    ( implies ( and ( not x38 ) ( and ( not x37 ) true ) ) ( = tmp384 0 ) )
    ( implies ( and ( not x38 ) ( and x37 true ) ) ( = tmp384 26 ) )
    ( implies ( and x38 ( and ( not x37 ) true ) ) ( = tmp384 11 ) )
    ( implies ( and x38 ( and x37 true ) ) ( = tmp384 37 ) )
    ( implies ( and ( not x20 ) ( and ( not x21 ) true ) ) ( = tmp383 0 ) )
    ( implies ( and ( not x20 ) ( and x21 true ) ) ( = tmp383 20 ) )
    ( implies ( and x20 ( and ( not x21 ) true ) ) ( = tmp383 27 ) )
    ( implies ( and x20 ( and x21 true ) ) ( = tmp383 47 ) )
    ( implies ( and ( not x40 ) ( and ( not x39 ) true ) ) ( = tmp382 0 ) )
    ( implies ( and ( not x40 ) ( and x39 true ) ) ( = tmp382 38 ) )
    ( implies ( and x40 ( and ( not x39 ) true ) ) ( = tmp382 45 ) )
    ( implies ( and x40 ( and x39 true ) ) ( = tmp382 83 ) )
    ( implies ( and ( not x18 ) ( and ( not x19 ) true ) ) ( = tmp381 0 ) )
    ( implies ( and ( not x18 ) ( and x19 true ) ) ( = tmp381 33 ) )
    ( implies ( and x18 ( and ( not x19 ) true ) ) ( = tmp381 36 ) )
    ( implies ( and x18 ( and x19 true ) ) ( = tmp381 69 ) )
    ( implies ( and ( not x42 ) ( and ( not x41 ) true ) ) ( = tmp380 0 ) )
    ( implies ( and ( not x42 ) ( and x41 true ) ) ( = tmp380 44 ) )
    ( implies ( and x42 ( and ( not x41 ) true ) ) ( = tmp380 14 ) )
    ( implies ( and x42 ( and x41 true ) ) ( = tmp380 58 ) )
    ( implies ( and ( not x16 ) ( and ( not x17 ) true ) ) ( = tmp379 0 ) )
    ( implies ( and ( not x16 ) ( and x17 true ) ) ( = tmp379 48 ) )
    ( implies ( and x16 ( and ( not x17 ) true ) ) ( = tmp379 37 ) )
    ( implies ( and x16 ( and x17 true ) ) ( = tmp379 85 ) )
    ( implies ( and ( not x44 ) ( and ( not x43 ) true ) ) ( = tmp378 0 ) )
    ( implies ( and ( not x44 ) ( and x43 true ) ) ( = tmp378 30 ) )
    ( implies ( and x44 ( and ( not x43 ) true ) ) ( = tmp378 19 ) )
    ( implies ( and x44 ( and x43 true ) ) ( = tmp378 49 ) )
    ( implies ( and ( not x14 ) ( and ( not x15 ) true ) ) ( = tmp377 0 ) )
    ( implies ( and ( not x14 ) ( and x15 true ) ) ( = tmp377 19 ) )
    ( implies ( and x14 ( and ( not x15 ) true ) ) ( = tmp377 14 ) )
    ( implies ( and x14 ( and x15 true ) ) ( = tmp377 33 ) )
    ( implies ( and ( not x46 ) ( and ( not x45 ) true ) ) ( = tmp376 0 ) )
    ( implies ( and ( not x46 ) ( and x45 true ) ) ( = tmp376 24 ) )
    ( implies ( and x46 ( and ( not x45 ) true ) ) ( = tmp376 44 ) )
    ( implies ( and x46 ( and x45 true ) ) ( = tmp376 68 ) )
    ( implies ( and ( not x12 ) ( and ( not x13 ) true ) ) ( = tmp375 0 ) )
    ( implies ( and ( not x12 ) ( and x13 true ) ) ( = tmp375 30 ) )
    ( implies ( and x12 ( and ( not x13 ) true ) ) ( = tmp375 40 ) )
    ( implies ( and x12 ( and x13 true ) ) ( = tmp375 70 ) )
    ( implies ( and ( not x48 ) ( and ( not x47 ) true ) ) ( = tmp374 0 ) )
    ( implies ( and ( not x48 ) ( and x47 true ) ) ( = tmp374 52 ) )
    ( implies ( and x48 ( and ( not x47 ) true ) ) ( = tmp374 16 ) )
    ( implies ( and x48 ( and x47 true ) ) ( = tmp374 68 ) )
    ( implies ( and ( not x10 ) ( and ( not x11 ) true ) ) ( = tmp373 0 ) )
    ( implies ( and ( not x10 ) ( and x11 true ) ) ( = tmp373 32 ) )
    ( implies ( and x10 ( and ( not x11 ) true ) ) ( = tmp373 38 ) )
    ( implies ( and x10 ( and x11 true ) ) ( = tmp373 70 ) )
    ( implies ( and ( not x50 ) ( and ( not x49 ) true ) ) ( = tmp372 0 ) )
    ( implies ( and ( not x50 ) ( and x49 true ) ) ( = tmp372 24 ) )
    ( implies ( and x50 ( and ( not x49 ) true ) ) ( = tmp372 29 ) )
    ( implies ( and x50 ( and x49 true ) ) ( = tmp372 53 ) )
    ( implies ( and ( not x8 ) ( and ( not x9 ) true ) ) ( = tmp371 0 ) )
    ( implies ( and ( not x8 ) ( and x9 true ) ) ( = tmp371 23 ) )
    ( implies ( and x8 ( and ( not x9 ) true ) ) ( = tmp371 32 ) )
    ( implies ( and x8 ( and x9 true ) ) ( = tmp371 55 ) )
    ( implies ( and ( not x52 ) ( and ( not x51 ) true ) ) ( = tmp370 0 ) )
    ( implies ( and ( not x52 ) ( and x51 true ) ) ( = tmp370 39 ) )
    ( implies ( and x52 ( and ( not x51 ) true ) ) ( = tmp370 39 ) )
    ( implies ( and x52 ( and x51 true ) ) ( = tmp370 78 ) )
    ( implies ( and ( not x6 ) ( and ( not x7 ) true ) ) ( = tmp369 0 ) )
    ( implies ( and ( not x6 ) ( and x7 true ) ) ( = tmp369 34 ) )
    ( implies ( and x6 ( and ( not x7 ) true ) ) ( = tmp369 31 ) )
    ( implies ( and x6 ( and x7 true ) ) ( = tmp369 65 ) )
    ( implies ( and ( not x54 ) ( and ( not x53 ) true ) ) ( = tmp368 0 ) )
    ( implies ( and ( not x54 ) ( and x53 true ) ) ( = tmp368 39 ) )
    ( implies ( and x54 ( and ( not x53 ) true ) ) ( = tmp368 33 ) )
    ( implies ( and x54 ( and x53 true ) ) ( = tmp368 72 ) )
    ( implies ( and ( not x4 ) ( and ( not x5 ) true ) ) ( = tmp367 0 ) )
    ( implies ( and ( not x4 ) ( and x5 true ) ) ( = tmp367 23 ) )
    ( implies ( and x4 ( and ( not x5 ) true ) ) ( = tmp367 33 ) )
    ( implies ( and x4 ( and x5 true ) ) ( = tmp367 56 ) )
    ( implies ( and ( not x56 ) ( and ( not x55 ) true ) ) ( = tmp366 0 ) )
    ( implies ( and ( not x56 ) ( and x55 true ) ) ( = tmp366 37 ) )
    ( implies ( and x56 ( and ( not x55 ) true ) ) ( = tmp366 17 ) )
    ( implies ( and x56 ( and x55 true ) ) ( = tmp366 54 ) )
    ( implies ( and ( not x2 ) ( and ( not x3 ) true ) ) ( = tmp365 0 ) )
    ( implies ( and ( not x2 ) ( and x3 true ) ) ( = tmp365 51 ) )
    ( implies ( and x2 ( and ( not x3 ) true ) ) ( = tmp365 10 ) )
    ( implies ( and x2 ( and x3 true ) ) ( = tmp365 61 ) )
    ( implies ( and ( not x30 ) true ) ( = tmp364 0 ) )
    ( implies ( and x30 true ) ( = tmp364 36 ) )
    ( implies ( and ( not x28 ) ( and ( not x29 ) true ) ) ( = tmp363 0 ) )
    ( implies ( and ( not x28 ) ( and x29 true ) ) ( = tmp363 18 ) )
    ( implies ( and x28 ( and ( not x29 ) true ) ) ( = tmp363 38 ) )
    ( implies ( and x28 ( and x29 true ) ) ( = tmp363 56 ) )
    ( implies ( and ( not x32 ) ( and ( not x31 ) true ) ) ( = tmp362 0 ) )
    ( implies ( and ( not x32 ) ( and x31 true ) ) ( = tmp362 6 ) )
    ( implies ( and x32 ( and ( not x31 ) true ) ) ( = tmp362 13 ) )
    ( implies ( and x32 ( and x31 true ) ) ( = tmp362 19 ) )
    ( implies ( and ( not x26 ) ( and ( not x27 ) true ) ) ( = tmp361 0 ) )
    ( implies ( and ( not x26 ) ( and x27 true ) ) ( = tmp361 50 ) )
    ( implies ( and x26 ( and ( not x27 ) true ) ) ( = tmp361 39 ) )
    ( implies ( and x26 ( and x27 true ) ) ( = tmp361 89 ) )
    ( implies ( and ( not x34 ) ( and ( not x33 ) true ) ) ( = tmp360 0 ) )
    ( implies ( and ( not x34 ) ( and x33 true ) ) ( = tmp360 47 ) )
    ( implies ( and x34 ( and ( not x33 ) true ) ) ( = tmp360 8 ) )
    ( implies ( and x34 ( and x33 true ) ) ( = tmp360 55 ) )
    ( implies ( and ( not x24 ) ( and ( not x25 ) true ) ) ( = tmp359 0 ) )
    ( implies ( and ( not x24 ) ( and x25 true ) ) ( = tmp359 41 ) )
    ( implies ( and x24 ( and ( not x25 ) true ) ) ( = tmp359 36 ) )
    ( implies ( and x24 ( and x25 true ) ) ( = tmp359 77 ) )
    ( implies ( and ( not x36 ) ( and ( not x35 ) true ) ) ( = tmp358 0 ) )
    ( implies ( and ( not x36 ) ( and x35 true ) ) ( = tmp358 5 ) )
    ( implies ( and x36 ( and ( not x35 ) true ) ) ( = tmp358 22 ) )
    ( implies ( and x36 ( and x35 true ) ) ( = tmp358 27 ) )
    ( implies ( and ( not x22 ) ( and ( not x23 ) true ) ) ( = tmp357 0 ) )
    ( implies ( and ( not x22 ) ( and x23 true ) ) ( = tmp357 15 ) )
    ( implies ( and x22 ( and ( not x23 ) true ) ) ( = tmp357 13 ) )
    ( implies ( and x22 ( and x23 true ) ) ( = tmp357 28 ) )
    ( implies ( and ( not x38 ) ( and ( not x37 ) true ) ) ( = tmp356 0 ) )
    ( implies ( and ( not x38 ) ( and x37 true ) ) ( = tmp356 48 ) )
    ( implies ( and x38 ( and ( not x37 ) true ) ) ( = tmp356 37 ) )
    ( implies ( and x38 ( and x37 true ) ) ( = tmp356 85 ) )
    ( implies ( and ( not x20 ) ( and ( not x21 ) true ) ) ( = tmp355 0 ) )
    ( implies ( and ( not x20 ) ( and x21 true ) ) ( = tmp355 6 ) )
    ( implies ( and x20 ( and ( not x21 ) true ) ) ( = tmp355 33 ) )
    ( implies ( and x20 ( and x21 true ) ) ( = tmp355 39 ) )
    ( implies ( and ( not x40 ) ( and ( not x39 ) true ) ) ( = tmp354 0 ) )
    ( implies ( and ( not x40 ) ( and x39 true ) ) ( = tmp354 34 ) )
    ( implies ( and x40 ( and ( not x39 ) true ) ) ( = tmp354 11 ) )
    ( implies ( and x40 ( and x39 true ) ) ( = tmp354 45 ) )
    ( implies ( and ( not x18 ) ( and ( not x19 ) true ) ) ( = tmp353 0 ) )
    ( implies ( and ( not x18 ) ( and x19 true ) ) ( = tmp353 34 ) )
    ( implies ( and x18 ( and ( not x19 ) true ) ) ( = tmp353 43 ) )
    ( implies ( and x18 ( and x19 true ) ) ( = tmp353 77 ) )
    ( implies ( and ( not x42 ) ( and ( not x41 ) true ) ) ( = tmp352 0 ) )
    ( implies ( and ( not x42 ) ( and x41 true ) ) ( = tmp352 38 ) )
    ( implies ( and x42 ( and ( not x41 ) true ) ) ( = tmp352 22 ) )
    ( implies ( and x42 ( and x41 true ) ) ( = tmp352 60 ) )
    ( implies ( and ( not x16 ) ( and ( not x17 ) true ) ) ( = tmp351 0 ) )
    ( implies ( and ( not x16 ) ( and x17 true ) ) ( = tmp351 55 ) )
    ( implies ( and x16 ( and ( not x17 ) true ) ) ( = tmp351 47 ) )
    ( implies ( and x16 ( and x17 true ) ) ( = tmp351 102 ) )
    ( implies ( and ( not x44 ) ( and ( not x43 ) true ) ) ( = tmp350 0 ) )
    ( implies ( and ( not x44 ) ( and x43 true ) ) ( = tmp350 52 ) )
    ( implies ( and x44 ( and ( not x43 ) true ) ) ( = tmp350 35 ) )
    ( implies ( and x44 ( and x43 true ) ) ( = tmp350 87 ) )
    ( implies ( and ( not x14 ) ( and ( not x15 ) true ) ) ( = tmp349 0 ) )
    ( implies ( and ( not x14 ) ( and x15 true ) ) ( = tmp349 40 ) )
    ( implies ( and x14 ( and ( not x15 ) true ) ) ( = tmp349 22 ) )
    ( implies ( and x14 ( and x15 true ) ) ( = tmp349 62 ) )
    ( implies ( and ( not x46 ) ( and ( not x45 ) true ) ) ( = tmp348 0 ) )
    ( implies ( and ( not x46 ) ( and x45 true ) ) ( = tmp348 39 ) )
    ( implies ( and x46 ( and ( not x45 ) true ) ) ( = tmp348 37 ) )
    ( implies ( and x46 ( and x45 true ) ) ( = tmp348 76 ) )
    ( implies ( and ( not x12 ) ( and ( not x13 ) true ) ) ( = tmp347 0 ) )
    ( implies ( and ( not x12 ) ( and x13 true ) ) ( = tmp347 53 ) )
    ( implies ( and x12 ( and ( not x13 ) true ) ) ( = tmp347 45 ) )
    ( implies ( and x12 ( and x13 true ) ) ( = tmp347 98 ) )
    ( implies ( and ( not x48 ) ( and ( not x47 ) true ) ) ( = tmp346 0 ) )
    ( implies ( and ( not x48 ) ( and x47 true ) ) ( = tmp346 27 ) )
    ( implies ( and x48 ( and ( not x47 ) true ) ) ( = tmp346 38 ) )
    ( implies ( and x48 ( and x47 true ) ) ( = tmp346 65 ) )
    ( implies ( and ( not x10 ) ( and ( not x11 ) true ) ) ( = tmp345 0 ) )
    ( implies ( and ( not x10 ) ( and x11 true ) ) ( = tmp345 44 ) )
    ( implies ( and x10 ( and ( not x11 ) true ) ) ( = tmp345 5 ) )
    ( implies ( and x10 ( and x11 true ) ) ( = tmp345 49 ) )
    ( implies ( and ( not x50 ) ( and ( not x49 ) true ) ) ( = tmp344 0 ) )
    ( implies ( and ( not x50 ) ( and x49 true ) ) ( = tmp344 24 ) )
    ( implies ( and x50 ( and ( not x49 ) true ) ) ( = tmp344 5 ) )
    ( implies ( and x50 ( and x49 true ) ) ( = tmp344 29 ) )
    ( implies ( and ( not x8 ) ( and ( not x9 ) true ) ) ( = tmp343 0 ) )
    ( implies ( and ( not x8 ) ( and x9 true ) ) ( = tmp343 19 ) )
    ( implies ( and x8 ( and ( not x9 ) true ) ) ( = tmp343 16 ) )
    ( implies ( and x8 ( and x9 true ) ) ( = tmp343 35 ) )
    ( implies ( and ( not x52 ) ( and ( not x51 ) true ) ) ( = tmp342 0 ) )
    ( implies ( and ( not x52 ) ( and x51 true ) ) ( = tmp342 16 ) )
    ( implies ( and x52 ( and ( not x51 ) true ) ) ( = tmp342 25 ) )
    ( implies ( and x52 ( and x51 true ) ) ( = tmp342 41 ) )
    ( implies ( and ( not x6 ) ( and ( not x7 ) true ) ) ( = tmp341 0 ) )
    ( implies ( and ( not x6 ) ( and x7 true ) ) ( = tmp341 37 ) )
    ( implies ( and x6 ( and ( not x7 ) true ) ) ( = tmp341 45 ) )
    ( implies ( and x6 ( and x7 true ) ) ( = tmp341 82 ) )
    ( implies ( and ( not x54 ) ( and ( not x53 ) true ) ) ( = tmp340 0 ) )
    ( implies ( and ( not x54 ) ( and x53 true ) ) ( = tmp340 14 ) )
    ( implies ( and x54 ( and ( not x53 ) true ) ) ( = tmp340 27 ) )
    ( implies ( and x54 ( and x53 true ) ) ( = tmp340 41 ) )
    ( implies ( and ( not x4 ) ( and ( not x5 ) true ) ) ( = tmp339 0 ) )
    ( implies ( and ( not x4 ) ( and x5 true ) ) ( = tmp339 30 ) )
    ( implies ( and x4 ( and ( not x5 ) true ) ) ( = tmp339 47 ) )
    ( implies ( and x4 ( and x5 true ) ) ( = tmp339 77 ) )
    ( implies ( and ( not x56 ) ( and ( not x55 ) true ) ) ( = tmp338 0 ) )
    ( implies ( and ( not x56 ) ( and x55 true ) ) ( = tmp338 6 ) )
    ( implies ( and x56 ( and ( not x55 ) true ) ) ( = tmp338 51 ) )
    ( implies ( and x56 ( and x55 true ) ) ( = tmp338 57 ) )
    ( implies ( and ( not x2 ) ( and ( not x3 ) true ) ) ( = tmp337 0 ) )
    ( implies ( and ( not x2 ) ( and x3 true ) ) ( = tmp337 6 ) )
    ( implies ( and x2 ( and ( not x3 ) true ) ) ( = tmp337 16 ) )
    ( implies ( and x2 ( and x3 true ) ) ( = tmp337 22 ) )
    ( implies ( and ( not x30 ) true ) ( = tmp336 0 ) )
    ( implies ( and x30 true ) ( = tmp336 43 ) )
    ( implies ( and ( not x28 ) ( and ( not x29 ) true ) ) ( = tmp335 0 ) )
    ( implies ( and ( not x28 ) ( and x29 true ) ) ( = tmp335 18 ) )
    ( implies ( and x28 ( and ( not x29 ) true ) ) ( = tmp335 52 ) )
    ( implies ( and x28 ( and x29 true ) ) ( = tmp335 70 ) )
    ( implies ( and ( not x32 ) ( and ( not x31 ) true ) ) ( = tmp334 0 ) )
    ( implies ( and ( not x32 ) ( and x31 true ) ) ( = tmp334 46 ) )
    ( implies ( and x32 ( and ( not x31 ) true ) ) ( = tmp334 42 ) )
    ( implies ( and x32 ( and x31 true ) ) ( = tmp334 88 ) )
    ( implies ( and ( not x26 ) ( and ( not x27 ) true ) ) ( = tmp333 0 ) )
    ( implies ( and ( not x26 ) ( and x27 true ) ) ( = tmp333 38 ) )
    ( implies ( and x26 ( and ( not x27 ) true ) ) ( = tmp333 30 ) )
    ( implies ( and x26 ( and x27 true ) ) ( = tmp333 68 ) )
    ( implies ( and ( not x34 ) ( and ( not x33 ) true ) ) ( = tmp332 0 ) )
    ( implies ( and ( not x34 ) ( and x33 true ) ) ( = tmp332 29 ) )
    ( implies ( and x34 ( and ( not x33 ) true ) ) ( = tmp332 23 ) )
    ( implies ( and x34 ( and x33 true ) ) ( = tmp332 52 ) )
    ( implies ( and ( not x24 ) ( and ( not x25 ) true ) ) ( = tmp331 0 ) )
    ( implies ( and ( not x24 ) ( and x25 true ) ) ( = tmp331 21 ) )
    ( implies ( and x24 ( and ( not x25 ) true ) ) ( = tmp331 27 ) )
    ( implies ( and x24 ( and x25 true ) ) ( = tmp331 48 ) )
    ( implies ( and ( not x36 ) ( and ( not x35 ) true ) ) ( = tmp330 0 ) )
    ( implies ( and ( not x36 ) ( and x35 true ) ) ( = tmp330 32 ) )
    ( implies ( and x36 ( and ( not x35 ) true ) ) ( = tmp330 31 ) )
    ( implies ( and x36 ( and x35 true ) ) ( = tmp330 63 ) )
    ( implies ( and ( not x22 ) ( and ( not x23 ) true ) ) ( = tmp329 0 ) )
    ( implies ( and ( not x22 ) ( and x23 true ) ) ( = tmp329 28 ) )
    ( implies ( and x22 ( and ( not x23 ) true ) ) ( = tmp329 11 ) )
    ( implies ( and x22 ( and x23 true ) ) ( = tmp329 39 ) )
    ( implies ( and ( not x38 ) ( and ( not x37 ) true ) ) ( = tmp328 0 ) )
    ( implies ( and ( not x38 ) ( and x37 true ) ) ( = tmp328 52 ) )
    ( implies ( and x38 ( and ( not x37 ) true ) ) ( = tmp328 33 ) )
    ( implies ( and x38 ( and x37 true ) ) ( = tmp328 85 ) )
    ( implies ( and ( not x20 ) ( and ( not x21 ) true ) ) ( = tmp327 0 ) )
    ( implies ( and ( not x20 ) ( and x21 true ) ) ( = tmp327 23 ) )
    ( implies ( and x20 ( and ( not x21 ) true ) ) ( = tmp327 39 ) )
    ( implies ( and x20 ( and x21 true ) ) ( = tmp327 62 ) )
    ( implies ( and ( not x40 ) ( and ( not x39 ) true ) ) ( = tmp326 0 ) )
    ( implies ( and ( not x40 ) ( and x39 true ) ) ( = tmp326 51 ) )
    ( implies ( and x40 ( and ( not x39 ) true ) ) ( = tmp326 50 ) )
    ( implies ( and x40 ( and x39 true ) ) ( = tmp326 101 ) )
    ( implies ( and ( not x18 ) ( and ( not x19 ) true ) ) ( = tmp325 0 ) )
    ( implies ( and ( not x18 ) ( and x19 true ) ) ( = tmp325 46 ) )
    ( implies ( and x18 ( and ( not x19 ) true ) ) ( = tmp325 54 ) )
    ( implies ( and x18 ( and x19 true ) ) ( = tmp325 100 ) )
    ( implies ( and ( not x42 ) ( and ( not x41 ) true ) ) ( = tmp324 0 ) )
    ( implies ( and ( not x42 ) ( and x41 true ) ) ( = tmp324 38 ) )
    ( implies ( and x42 ( and ( not x41 ) true ) ) ( = tmp324 7 ) )
    ( implies ( and x42 ( and x41 true ) ) ( = tmp324 45 ) )
    ( implies ( and ( not x16 ) ( and ( not x17 ) true ) ) ( = tmp323 0 ) )
    ( implies ( and ( not x16 ) ( and x17 true ) ) ( = tmp323 21 ) )
    ( implies ( and x16 ( and ( not x17 ) true ) ) ( = tmp323 8 ) )
    ( implies ( and x16 ( and x17 true ) ) ( = tmp323 29 ) )
    ( implies ( and ( not x44 ) ( and ( not x43 ) true ) ) ( = tmp322 0 ) )
    ( implies ( and ( not x44 ) ( and x43 true ) ) ( = tmp322 42 ) )
    ( implies ( and x44 ( and ( not x43 ) true ) ) ( = tmp322 34 ) )
    ( implies ( and x44 ( and x43 true ) ) ( = tmp322 76 ) )
    ( implies ( and ( not x14 ) ( and ( not x15 ) true ) ) ( = tmp321 0 ) )
    ( implies ( and ( not x14 ) ( and x15 true ) ) ( = tmp321 48 ) )
    ( implies ( and x14 ( and ( not x15 ) true ) ) ( = tmp321 16 ) )
    ( implies ( and x14 ( and x15 true ) ) ( = tmp321 64 ) )
    ( implies ( and ( not x46 ) ( and ( not x45 ) true ) ) ( = tmp320 0 ) )
    ( implies ( and ( not x46 ) ( and x45 true ) ) ( = tmp320 18 ) )
    ( implies ( and x46 ( and ( not x45 ) true ) ) ( = tmp320 35 ) )
    ( implies ( and x46 ( and x45 true ) ) ( = tmp320 53 ) )
    ( implies ( and ( not x12 ) ( and ( not x13 ) true ) ) ( = tmp319 0 ) )
    ( implies ( and ( not x12 ) ( and x13 true ) ) ( = tmp319 51 ) )
    ( implies ( and x12 ( and ( not x13 ) true ) ) ( = tmp319 48 ) )
    ( implies ( and x12 ( and x13 true ) ) ( = tmp319 99 ) )
    ( implies ( and ( not x48 ) ( and ( not x47 ) true ) ) ( = tmp318 0 ) )
    ( implies ( and ( not x48 ) ( and x47 true ) ) ( = tmp318 37 ) )
    ( implies ( and x48 ( and ( not x47 ) true ) ) ( = tmp318 35 ) )
    ( implies ( and x48 ( and x47 true ) ) ( = tmp318 72 ) )
    ( implies ( and ( not x10 ) ( and ( not x11 ) true ) ) ( = tmp317 0 ) )
    ( implies ( and ( not x10 ) ( and x11 true ) ) ( = tmp317 12 ) )
    ( implies ( and x10 ( and ( not x11 ) true ) ) ( = tmp317 9 ) )
    ( implies ( and x10 ( and x11 true ) ) ( = tmp317 21 ) )
    ( implies ( and ( not x50 ) ( and ( not x49 ) true ) ) ( = tmp316 0 ) )
    ( implies ( and ( not x50 ) ( and x49 true ) ) ( = tmp316 33 ) )
    ( implies ( and x50 ( and ( not x49 ) true ) ) ( = tmp316 28 ) )
    ( implies ( and x50 ( and x49 true ) ) ( = tmp316 61 ) )
    ( implies ( and ( not x8 ) ( and ( not x9 ) true ) ) ( = tmp315 0 ) )
    ( implies ( and ( not x8 ) ( and x9 true ) ) ( = tmp315 54 ) )
    ( implies ( and x8 ( and ( not x9 ) true ) ) ( = tmp315 24 ) )
    ( implies ( and x8 ( and x9 true ) ) ( = tmp315 78 ) )
    ( implies ( and ( not x52 ) ( and ( not x51 ) true ) ) ( = tmp314 0 ) )
    ( implies ( and ( not x52 ) ( and x51 true ) ) ( = tmp314 18 ) )
    ( implies ( and x52 ( and ( not x51 ) true ) ) ( = tmp314 52 ) )
    ( implies ( and x52 ( and x51 true ) ) ( = tmp314 70 ) )
    ( implies ( and ( not x6 ) ( and ( not x7 ) true ) ) ( = tmp313 0 ) )
    ( implies ( and ( not x6 ) ( and x7 true ) ) ( = tmp313 6 ) )
    ( implies ( and x6 ( and ( not x7 ) true ) ) ( = tmp313 33 ) )
    ( implies ( and x6 ( and x7 true ) ) ( = tmp313 39 ) )
    ( implies ( and ( not x54 ) ( and ( not x53 ) true ) ) ( = tmp312 0 ) )
    ( implies ( and ( not x54 ) ( and x53 true ) ) ( = tmp312 34 ) )
    ( implies ( and x54 ( and ( not x53 ) true ) ) ( = tmp312 42 ) )
    ( implies ( and x54 ( and x53 true ) ) ( = tmp312 76 ) )
    ( implies ( and ( not x4 ) ( and ( not x5 ) true ) ) ( = tmp311 0 ) )
    ( implies ( and ( not x4 ) ( and x5 true ) ) ( = tmp311 6 ) )
    ( implies ( and x4 ( and ( not x5 ) true ) ) ( = tmp311 45 ) )
    ( implies ( and x4 ( and x5 true ) ) ( = tmp311 51 ) )
    ( implies ( and ( not x56 ) ( and ( not x55 ) true ) ) ( = tmp310 0 ) )
    ( implies ( and ( not x56 ) ( and x55 true ) ) ( = tmp310 24 ) )
    ( implies ( and x56 ( and ( not x55 ) true ) ) ( = tmp310 51 ) )
    ( implies ( and x56 ( and x55 true ) ) ( = tmp310 75 ) )
    ( implies ( and ( not x2 ) ( and ( not x3 ) true ) ) ( = tmp309 0 ) )
    ( implies ( and ( not x2 ) ( and x3 true ) ) ( = tmp309 33 ) )
    ( implies ( and x2 ( and ( not x3 ) true ) ) ( = tmp309 42 ) )
    ( implies ( and x2 ( and x3 true ) ) ( = tmp309 75 ) )
    ( implies ( and ( not x30 ) true ) ( = tmp308 0 ) )
    ( implies ( and x30 true ) ( = tmp308 5 ) )
    ( implies ( and ( not x28 ) ( and ( not x29 ) true ) ) ( = tmp307 0 ) )
    ( implies ( and ( not x28 ) ( and x29 true ) ) ( = tmp307 20 ) )
    ( implies ( and x28 ( and ( not x29 ) true ) ) ( = tmp307 22 ) )
    ( implies ( and x28 ( and x29 true ) ) ( = tmp307 42 ) )
    ( implies ( and ( not x32 ) ( and ( not x31 ) true ) ) ( = tmp306 0 ) )
    ( implies ( and ( not x32 ) ( and x31 true ) ) ( = tmp306 16 ) )
    ( implies ( and x32 ( and ( not x31 ) true ) ) ( = tmp306 22 ) )
    ( implies ( and x32 ( and x31 true ) ) ( = tmp306 38 ) )
    ( implies ( and ( not x26 ) ( and ( not x27 ) true ) ) ( = tmp305 0 ) )
    ( implies ( and ( not x26 ) ( and x27 true ) ) ( = tmp305 38 ) )
    ( implies ( and x26 ( and ( not x27 ) true ) ) ( = tmp305 37 ) )
    ( implies ( and x26 ( and x27 true ) ) ( = tmp305 75 ) )
    ( implies ( and ( not x34 ) ( and ( not x33 ) true ) ) ( = tmp304 0 ) )
    ( implies ( and ( not x34 ) ( and x33 true ) ) ( = tmp304 25 ) )
    ( implies ( and x34 ( and ( not x33 ) true ) ) ( = tmp304 8 ) )
    ( implies ( and x34 ( and x33 true ) ) ( = tmp304 33 ) )
    ( implies ( and ( not x24 ) ( and ( not x25 ) true ) ) ( = tmp303 0 ) )
    ( implies ( and ( not x24 ) ( and x25 true ) ) ( = tmp303 40 ) )
    ( implies ( and x24 ( and ( not x25 ) true ) ) ( = tmp303 19 ) )
    ( implies ( and x24 ( and x25 true ) ) ( = tmp303 59 ) )
    ( implies ( and ( not x36 ) ( and ( not x35 ) true ) ) ( = tmp302 0 ) )
    ( implies ( and ( not x36 ) ( and x35 true ) ) ( = tmp302 43 ) )
    ( implies ( and x36 ( and ( not x35 ) true ) ) ( = tmp302 50 ) )
    ( implies ( and x36 ( and x35 true ) ) ( = tmp302 93 ) )
    ( implies ( and ( not x22 ) ( and ( not x23 ) true ) ) ( = tmp301 0 ) )
    ( implies ( and ( not x22 ) ( and x23 true ) ) ( = tmp301 50 ) )
    ( implies ( and x22 ( and ( not x23 ) true ) ) ( = tmp301 42 ) )
    ( implies ( and x22 ( and x23 true ) ) ( = tmp301 92 ) )
    ( implies ( and ( not x38 ) ( and ( not x37 ) true ) ) ( = tmp300 0 ) )
    ( implies ( and ( not x38 ) ( and x37 true ) ) ( = tmp300 47 ) )
    ( implies ( and x38 ( and ( not x37 ) true ) ) ( = tmp300 9 ) )
    ( implies ( and x38 ( and x37 true ) ) ( = tmp300 56 ) )
    ( implies ( and ( not x20 ) ( and ( not x21 ) true ) ) ( = tmp299 0 ) )
    ( implies ( and ( not x20 ) ( and x21 true ) ) ( = tmp299 25 ) )
    ( implies ( and x20 ( and ( not x21 ) true ) ) ( = tmp299 11 ) )
    ( implies ( and x20 ( and x21 true ) ) ( = tmp299 36 ) )
    ( implies ( and ( not x40 ) ( and ( not x39 ) true ) ) ( = tmp298 0 ) )
    ( implies ( and ( not x40 ) ( and x39 true ) ) ( = tmp298 5 ) )
    ( implies ( and x40 ( and ( not x39 ) true ) ) ( = tmp298 12 ) )
    ( implies ( and x40 ( and x39 true ) ) ( = tmp298 17 ) )
    ( implies ( and ( not x18 ) ( and ( not x19 ) true ) ) ( = tmp297 0 ) )
    ( implies ( and ( not x18 ) ( and x19 true ) ) ( = tmp297 17 ) )
    ( implies ( and x18 ( and ( not x19 ) true ) ) ( = tmp297 50 ) )
    ( implies ( and x18 ( and x19 true ) ) ( = tmp297 67 ) )
    ( implies ( and ( not x42 ) ( and ( not x41 ) true ) ) ( = tmp296 0 ) )
    ( implies ( and ( not x42 ) ( and x41 true ) ) ( = tmp296 10 ) )
    ( implies ( and x42 ( and ( not x41 ) true ) ) ( = tmp296 10 ) )
    ( implies ( and x42 ( and x41 true ) ) ( = tmp296 20 ) )
    ( implies ( and ( not x16 ) ( and ( not x17 ) true ) ) ( = tmp295 0 ) )
    ( implies ( and ( not x16 ) ( and x17 true ) ) ( = tmp295 39 ) )
    ( implies ( and x16 ( and ( not x17 ) true ) ) ( = tmp295 27 ) )
    ( implies ( and x16 ( and x17 true ) ) ( = tmp295 66 ) )
    ( implies ( and ( not x44 ) ( and ( not x43 ) true ) ) ( = tmp294 0 ) )
    ( implies ( and ( not x44 ) ( and x43 true ) ) ( = tmp294 42 ) )
    ( implies ( and x44 ( and ( not x43 ) true ) ) ( = tmp294 22 ) )
    ( implies ( and x44 ( and x43 true ) ) ( = tmp294 64 ) )
    ( implies ( and ( not x14 ) ( and ( not x15 ) true ) ) ( = tmp293 0 ) )
    ( implies ( and ( not x14 ) ( and x15 true ) ) ( = tmp293 33 ) )
    ( implies ( and x14 ( and ( not x15 ) true ) ) ( = tmp293 20 ) )
    ( implies ( and x14 ( and x15 true ) ) ( = tmp293 53 ) )
    ( implies ( and ( not x46 ) ( and ( not x45 ) true ) ) ( = tmp292 0 ) )
    ( implies ( and ( not x46 ) ( and x45 true ) ) ( = tmp292 25 ) )
    ( implies ( and x46 ( and ( not x45 ) true ) ) ( = tmp292 20 ) )
    ( implies ( and x46 ( and x45 true ) ) ( = tmp292 45 ) )
    ( implies ( and ( not x12 ) ( and ( not x13 ) true ) ) ( = tmp291 0 ) )
    ( implies ( and ( not x12 ) ( and x13 true ) ) ( = tmp291 17 ) )
    ( implies ( and x12 ( and ( not x13 ) true ) ) ( = tmp291 35 ) )
    ( implies ( and x12 ( and x13 true ) ) ( = tmp291 52 ) )
    ( implies ( and ( not x48 ) ( and ( not x47 ) true ) ) ( = tmp290 0 ) )
    ( implies ( and ( not x48 ) ( and x47 true ) ) ( = tmp290 45 ) )
    ( implies ( and x48 ( and ( not x47 ) true ) ) ( = tmp290 9 ) )
    ( implies ( and x48 ( and x47 true ) ) ( = tmp290 54 ) )
    ( implies ( and ( not x10 ) ( and ( not x11 ) true ) ) ( = tmp289 0 ) )
    ( implies ( and ( not x10 ) ( and x11 true ) ) ( = tmp289 10 ) )
    ( implies ( and x10 ( and ( not x11 ) true ) ) ( = tmp289 5 ) )
    ( implies ( and x10 ( and x11 true ) ) ( = tmp289 15 ) )
    ( implies ( and ( not x50 ) ( and ( not x49 ) true ) ) ( = tmp288 0 ) )
    ( implies ( and ( not x50 ) ( and x49 true ) ) ( = tmp288 15 ) )
    ( implies ( and x50 ( and ( not x49 ) true ) ) ( = tmp288 7 ) )
    ( implies ( and x50 ( and x49 true ) ) ( = tmp288 22 ) )
    ( implies ( and ( not x8 ) ( and ( not x9 ) true ) ) ( = tmp287 0 ) )
    ( implies ( and ( not x8 ) ( and x9 true ) ) ( = tmp287 21 ) )
    ( implies ( and x8 ( and ( not x9 ) true ) ) ( = tmp287 10 ) )
    ( implies ( and x8 ( and x9 true ) ) ( = tmp287 31 ) )
    ( implies ( and ( not x52 ) ( and ( not x51 ) true ) ) ( = tmp286 0 ) )
    ( implies ( and ( not x52 ) ( and x51 true ) ) ( = tmp286 15 ) )
    ( implies ( and x52 ( and ( not x51 ) true ) ) ( = tmp286 35 ) )
    ( implies ( and x52 ( and x51 true ) ) ( = tmp286 50 ) )
    ( implies ( and ( not x6 ) ( and ( not x7 ) true ) ) ( = tmp285 0 ) )
    ( implies ( and ( not x6 ) ( and x7 true ) ) ( = tmp285 22 ) )
    ( implies ( and x6 ( and ( not x7 ) true ) ) ( = tmp285 44 ) )
    ( implies ( and x6 ( and x7 true ) ) ( = tmp285 66 ) )
    ( implies ( and ( not x54 ) ( and ( not x53 ) true ) ) ( = tmp284 0 ) )
    ( implies ( and ( not x54 ) ( and x53 true ) ) ( = tmp284 44 ) )
    ( implies ( and x54 ( and ( not x53 ) true ) ) ( = tmp284 9 ) )
    ( implies ( and x54 ( and x53 true ) ) ( = tmp284 53 ) )
    ( implies ( and ( not x4 ) ( and ( not x5 ) true ) ) ( = tmp283 0 ) )
    ( implies ( and ( not x4 ) ( and x5 true ) ) ( = tmp283 29 ) )
    ( implies ( and x4 ( and ( not x5 ) true ) ) ( = tmp283 25 ) )
    ( implies ( and x4 ( and x5 true ) ) ( = tmp283 54 ) )
    ( implies ( and ( not x56 ) ( and ( not x55 ) true ) ) ( = tmp282 0 ) )
    ( implies ( and ( not x56 ) ( and x55 true ) ) ( = tmp282 50 ) )
    ( implies ( and x56 ( and ( not x55 ) true ) ) ( = tmp282 28 ) )
    ( implies ( and x56 ( and x55 true ) ) ( = tmp282 78 ) )
    ( implies ( and ( not x2 ) ( and ( not x3 ) true ) ) ( = tmp281 0 ) )
    ( implies ( and ( not x2 ) ( and x3 true ) ) ( = tmp281 47 ) )
    ( implies ( and x2 ( and ( not x3 ) true ) ) ( = tmp281 25 ) )
    ( implies ( and x2 ( and x3 true ) ) ( = tmp281 72 ) )
    ( implies ( and ( not x30 ) true ) ( = tmp280 0 ) )
    ( implies ( and x30 true ) ( = tmp280 52 ) )
    ( implies ( and ( not x28 ) ( and ( not x29 ) true ) ) ( = tmp279 0 ) )
    ( implies ( and ( not x28 ) ( and x29 true ) ) ( = tmp279 9 ) )
    ( implies ( and x28 ( and ( not x29 ) true ) ) ( = tmp279 23 ) )
    ( implies ( and x28 ( and x29 true ) ) ( = tmp279 32 ) )
    ( implies ( and ( not x32 ) ( and ( not x31 ) true ) ) ( = tmp278 0 ) )
    ( implies ( and ( not x32 ) ( and x31 true ) ) ( = tmp278 52 ) )
    ( implies ( and x32 ( and ( not x31 ) true ) ) ( = tmp278 37 ) )
    ( implies ( and x32 ( and x31 true ) ) ( = tmp278 89 ) )
    ( implies ( and ( not x26 ) ( and ( not x27 ) true ) ) ( = tmp277 0 ) )
    ( implies ( and ( not x26 ) ( and x27 true ) ) ( = tmp277 53 ) )
    ( implies ( and x26 ( and ( not x27 ) true ) ) ( = tmp277 8 ) )
    ( implies ( and x26 ( and x27 true ) ) ( = tmp277 61 ) )
    ( implies ( and ( not x34 ) ( and ( not x33 ) true ) ) ( = tmp276 0 ) )
    ( implies ( and ( not x34 ) ( and x33 true ) ) ( = tmp276 33 ) )
    ( implies ( and x34 ( and ( not x33 ) true ) ) ( = tmp276 39 ) )
    ( implies ( and x34 ( and x33 true ) ) ( = tmp276 72 ) )
    ( implies ( and ( not x24 ) ( and ( not x25 ) true ) ) ( = tmp275 0 ) )
    ( implies ( and ( not x24 ) ( and x25 true ) ) ( = tmp275 23 ) )
    ( implies ( and x24 ( and ( not x25 ) true ) ) ( = tmp275 16 ) )
    ( implies ( and x24 ( and x25 true ) ) ( = tmp275 39 ) )
    ( implies ( and ( not x36 ) ( and ( not x35 ) true ) ) ( = tmp274 0 ) )
    ( implies ( and ( not x36 ) ( and x35 true ) ) ( = tmp274 55 ) )
    ( implies ( and x36 ( and ( not x35 ) true ) ) ( = tmp274 18 ) )
    ( implies ( and x36 ( and x35 true ) ) ( = tmp274 73 ) )
    ( implies ( and ( not x22 ) ( and ( not x23 ) true ) ) ( = tmp273 0 ) )
    ( implies ( and ( not x22 ) ( and x23 true ) ) ( = tmp273 54 ) )
    ( implies ( and x22 ( and ( not x23 ) true ) ) ( = tmp273 52 ) )
    ( implies ( and x22 ( and x23 true ) ) ( = tmp273 106 ) )
    ( implies ( and ( not x38 ) ( and ( not x37 ) true ) ) ( = tmp272 0 ) )
    ( implies ( and ( not x38 ) ( and x37 true ) ) ( = tmp272 17 ) )
    ( implies ( and x38 ( and ( not x37 ) true ) ) ( = tmp272 14 ) )
    ( implies ( and x38 ( and x37 true ) ) ( = tmp272 31 ) )
    ( implies ( and ( not x20 ) ( and ( not x21 ) true ) ) ( = tmp271 0 ) )
    ( implies ( and ( not x20 ) ( and x21 true ) ) ( = tmp271 40 ) )
    ( implies ( and x20 ( and ( not x21 ) true ) ) ( = tmp271 29 ) )
    ( implies ( and x20 ( and x21 true ) ) ( = tmp271 69 ) )
    ( implies ( and ( not x40 ) ( and ( not x39 ) true ) ) ( = tmp270 0 ) )
    ( implies ( and ( not x40 ) ( and x39 true ) ) ( = tmp270 54 ) )
    ( implies ( and x40 ( and ( not x39 ) true ) ) ( = tmp270 14 ) )
    ( implies ( and x40 ( and x39 true ) ) ( = tmp270 68 ) )
    ( implies ( and ( not x18 ) ( and ( not x19 ) true ) ) ( = tmp269 0 ) )
    ( implies ( and ( not x18 ) ( and x19 true ) ) ( = tmp269 55 ) )
    ( implies ( and x18 ( and ( not x19 ) true ) ) ( = tmp269 29 ) )
    ( implies ( and x18 ( and x19 true ) ) ( = tmp269 84 ) )
    ( implies ( and ( not x42 ) ( and ( not x41 ) true ) ) ( = tmp268 0 ) )
    ( implies ( and ( not x42 ) ( and x41 true ) ) ( = tmp268 24 ) )
    ( implies ( and x42 ( and ( not x41 ) true ) ) ( = tmp268 21 ) )
    ( implies ( and x42 ( and x41 true ) ) ( = tmp268 45 ) )
    ( implies ( and ( not x16 ) ( and ( not x17 ) true ) ) ( = tmp267 0 ) )
    ( implies ( and ( not x16 ) ( and x17 true ) ) ( = tmp267 24 ) )
    ( implies ( and x16 ( and ( not x17 ) true ) ) ( = tmp267 19 ) )
    ( implies ( and x16 ( and x17 true ) ) ( = tmp267 43 ) )
    ( implies ( and ( not x44 ) ( and ( not x43 ) true ) ) ( = tmp266 0 ) )
    ( implies ( and ( not x44 ) ( and x43 true ) ) ( = tmp266 46 ) )
    ( implies ( and x44 ( and ( not x43 ) true ) ) ( = tmp266 28 ) )
    ( implies ( and x44 ( and x43 true ) ) ( = tmp266 74 ) )
    ( implies ( and ( not x14 ) ( and ( not x15 ) true ) ) ( = tmp265 0 ) )
    ( implies ( and ( not x14 ) ( and x15 true ) ) ( = tmp265 38 ) )
    ( implies ( and x14 ( and ( not x15 ) true ) ) ( = tmp265 14 ) )
    ( implies ( and x14 ( and x15 true ) ) ( = tmp265 52 ) )
    ( implies ( and ( not x46 ) ( and ( not x45 ) true ) ) ( = tmp264 0 ) )
    ( implies ( and ( not x46 ) ( and x45 true ) ) ( = tmp264 30 ) )
    ( implies ( and x46 ( and ( not x45 ) true ) ) ( = tmp264 29 ) )
    ( implies ( and x46 ( and x45 true ) ) ( = tmp264 59 ) )
    ( implies ( and ( not x12 ) ( and ( not x13 ) true ) ) ( = tmp263 0 ) )
    ( implies ( and ( not x12 ) ( and x13 true ) ) ( = tmp263 9 ) )
    ( implies ( and x12 ( and ( not x13 ) true ) ) ( = tmp263 37 ) )
    ( implies ( and x12 ( and x13 true ) ) ( = tmp263 46 ) )
    ( implies ( and ( not x48 ) ( and ( not x47 ) true ) ) ( = tmp262 0 ) )
    ( implies ( and ( not x48 ) ( and x47 true ) ) ( = tmp262 43 ) )
    ( implies ( and x48 ( and ( not x47 ) true ) ) ( = tmp262 50 ) )
    ( implies ( and x48 ( and x47 true ) ) ( = tmp262 93 ) )
    ( implies ( and ( not x10 ) ( and ( not x11 ) true ) ) ( = tmp261 0 ) )
    ( implies ( and ( not x10 ) ( and x11 true ) ) ( = tmp261 23 ) )
    ( implies ( and x10 ( and ( not x11 ) true ) ) ( = tmp261 14 ) )
    ( implies ( and x10 ( and x11 true ) ) ( = tmp261 37 ) )
    ( implies ( and ( not x50 ) ( and ( not x49 ) true ) ) ( = tmp260 0 ) )
    ( implies ( and ( not x50 ) ( and x49 true ) ) ( = tmp260 53 ) )
    ( implies ( and x50 ( and ( not x49 ) true ) ) ( = tmp260 43 ) )
    ( implies ( and x50 ( and x49 true ) ) ( = tmp260 96 ) )
    ( implies ( and ( not x8 ) ( and ( not x9 ) true ) ) ( = tmp259 0 ) )
    ( implies ( and ( not x8 ) ( and x9 true ) ) ( = tmp259 53 ) )
    ( implies ( and x8 ( and ( not x9 ) true ) ) ( = tmp259 40 ) )
    ( implies ( and x8 ( and x9 true ) ) ( = tmp259 93 ) )
    ( implies ( and ( not x52 ) ( and ( not x51 ) true ) ) ( = tmp258 0 ) )
    ( implies ( and ( not x52 ) ( and x51 true ) ) ( = tmp258 24 ) )
    ( implies ( and x52 ( and ( not x51 ) true ) ) ( = tmp258 38 ) )
    ( implies ( and x52 ( and x51 true ) ) ( = tmp258 62 ) )
    ( implies ( and ( not x6 ) ( and ( not x7 ) true ) ) ( = tmp257 0 ) )
    ( implies ( and ( not x6 ) ( and x7 true ) ) ( = tmp257 14 ) )
    ( implies ( and x6 ( and ( not x7 ) true ) ) ( = tmp257 33 ) )
    ( implies ( and x6 ( and x7 true ) ) ( = tmp257 47 ) )
    ( implies ( and ( not x54 ) ( and ( not x53 ) true ) ) ( = tmp256 0 ) )
    ( implies ( and ( not x54 ) ( and x53 true ) ) ( = tmp256 39 ) )
    ( implies ( and x54 ( and ( not x53 ) true ) ) ( = tmp256 22 ) )
    ( implies ( and x54 ( and x53 true ) ) ( = tmp256 61 ) )
    ( implies ( and ( not x4 ) ( and ( not x5 ) true ) ) ( = tmp255 0 ) )
    ( implies ( and ( not x4 ) ( and x5 true ) ) ( = tmp255 41 ) )
    ( implies ( and x4 ( and ( not x5 ) true ) ) ( = tmp255 23 ) )
    ( implies ( and x4 ( and x5 true ) ) ( = tmp255 64 ) )
    ( implies ( and ( not x56 ) ( and ( not x55 ) true ) ) ( = tmp254 0 ) )
    ( implies ( and ( not x56 ) ( and x55 true ) ) ( = tmp254 49 ) )
    ( implies ( and x56 ( and ( not x55 ) true ) ) ( = tmp254 7 ) )
    ( implies ( and x56 ( and x55 true ) ) ( = tmp254 56 ) )
    ( implies ( and ( not x2 ) ( and ( not x3 ) true ) ) ( = tmp253 0 ) )
    ( implies ( and ( not x2 ) ( and x3 true ) ) ( = tmp253 42 ) )
    ( implies ( and x2 ( and ( not x3 ) true ) ) ( = tmp253 37 ) )
    ( implies ( and x2 ( and x3 true ) ) ( = tmp253 79 ) )
    ( implies ( and ( not x30 ) true ) ( = tmp252 0 ) )
    ( implies ( and x30 true ) ( = tmp252 46 ) )
    ( implies ( and ( not x28 ) ( and ( not x29 ) true ) ) ( = tmp251 0 ) )
    ( implies ( and ( not x28 ) ( and x29 true ) ) ( = tmp251 9 ) )
    ( implies ( and x28 ( and ( not x29 ) true ) ) ( = tmp251 47 ) )
    ( implies ( and x28 ( and x29 true ) ) ( = tmp251 56 ) )
    ( implies ( and ( not x32 ) ( and ( not x31 ) true ) ) ( = tmp250 0 ) )
    ( implies ( and ( not x32 ) ( and x31 true ) ) ( = tmp250 46 ) )
    ( implies ( and x32 ( and ( not x31 ) true ) ) ( = tmp250 55 ) )
    ( implies ( and x32 ( and x31 true ) ) ( = tmp250 101 ) )
    ( implies ( and ( not x26 ) ( and ( not x27 ) true ) ) ( = tmp249 0 ) )
    ( implies ( and ( not x26 ) ( and x27 true ) ) ( = tmp249 12 ) )
    ( implies ( and x26 ( and ( not x27 ) true ) ) ( = tmp249 39 ) )
    ( implies ( and x26 ( and x27 true ) ) ( = tmp249 51 ) )
    ( implies ( and ( not x34 ) ( and ( not x33 ) true ) ) ( = tmp248 0 ) )
    ( implies ( and ( not x34 ) ( and x33 true ) ) ( = tmp248 25 ) )
    ( implies ( and x34 ( and ( not x33 ) true ) ) ( = tmp248 55 ) )
    ( implies ( and x34 ( and x33 true ) ) ( = tmp248 80 ) )
    ( implies ( and ( not x24 ) ( and ( not x25 ) true ) ) ( = tmp247 0 ) )
    ( implies ( and ( not x24 ) ( and x25 true ) ) ( = tmp247 31 ) )
    ( implies ( and x24 ( and ( not x25 ) true ) ) ( = tmp247 35 ) )
    ( implies ( and x24 ( and x25 true ) ) ( = tmp247 66 ) )
    ( implies ( and ( not x36 ) ( and ( not x35 ) true ) ) ( = tmp246 0 ) )
    ( implies ( and ( not x36 ) ( and x35 true ) ) ( = tmp246 38 ) )
    ( implies ( and x36 ( and ( not x35 ) true ) ) ( = tmp246 39 ) )
    ( implies ( and x36 ( and x35 true ) ) ( = tmp246 77 ) )
    ( implies ( and ( not x22 ) ( and ( not x23 ) true ) ) ( = tmp245 0 ) )
    ( implies ( and ( not x22 ) ( and x23 true ) ) ( = tmp245 17 ) )
    ( implies ( and x22 ( and ( not x23 ) true ) ) ( = tmp245 51 ) )
    ( implies ( and x22 ( and x23 true ) ) ( = tmp245 68 ) )
    ( implies ( and ( not x38 ) ( and ( not x37 ) true ) ) ( = tmp244 0 ) )
    ( implies ( and ( not x38 ) ( and x37 true ) ) ( = tmp244 51 ) )
    ( implies ( and x38 ( and ( not x37 ) true ) ) ( = tmp244 46 ) )
    ( implies ( and x38 ( and x37 true ) ) ( = tmp244 97 ) )
    ( implies ( and ( not x20 ) ( and ( not x21 ) true ) ) ( = tmp243 0 ) )
    ( implies ( and ( not x20 ) ( and x21 true ) ) ( = tmp243 33 ) )
    ( implies ( and x20 ( and ( not x21 ) true ) ) ( = tmp243 14 ) )
    ( implies ( and x20 ( and x21 true ) ) ( = tmp243 47 ) )
    ( implies ( and ( not x40 ) ( and ( not x39 ) true ) ) ( = tmp242 0 ) )
    ( implies ( and ( not x40 ) ( and x39 true ) ) ( = tmp242 6 ) )
    ( implies ( and x40 ( and ( not x39 ) true ) ) ( = tmp242 15 ) )
    ( implies ( and x40 ( and x39 true ) ) ( = tmp242 21 ) )
    ( implies ( and ( not x18 ) ( and ( not x19 ) true ) ) ( = tmp241 0 ) )
    ( implies ( and ( not x18 ) ( and x19 true ) ) ( = tmp241 36 ) )
    ( implies ( and x18 ( and ( not x19 ) true ) ) ( = tmp241 29 ) )
    ( implies ( and x18 ( and x19 true ) ) ( = tmp241 65 ) )
    ( implies ( and ( not x42 ) ( and ( not x41 ) true ) ) ( = tmp240 0 ) )
    ( implies ( and ( not x42 ) ( and x41 true ) ) ( = tmp240 15 ) )
    ( implies ( and x42 ( and ( not x41 ) true ) ) ( = tmp240 47 ) )
    ( implies ( and x42 ( and x41 true ) ) ( = tmp240 62 ) )
    ( implies ( and ( not x16 ) ( and ( not x17 ) true ) ) ( = tmp239 0 ) )
    ( implies ( and ( not x16 ) ( and x17 true ) ) ( = tmp239 22 ) )
    ( implies ( and x16 ( and ( not x17 ) true ) ) ( = tmp239 23 ) )
    ( implies ( and x16 ( and x17 true ) ) ( = tmp239 45 ) )
    ( implies ( and ( not x44 ) ( and ( not x43 ) true ) ) ( = tmp238 0 ) )
    ( implies ( and ( not x44 ) ( and x43 true ) ) ( = tmp238 40 ) )
    ( implies ( and x44 ( and ( not x43 ) true ) ) ( = tmp238 10 ) )
    ( implies ( and x44 ( and x43 true ) ) ( = tmp238 50 ) )
    ( implies ( and ( not x14 ) ( and ( not x15 ) true ) ) ( = tmp237 0 ) )
    ( implies ( and ( not x14 ) ( and x15 true ) ) ( = tmp237 17 ) )
    ( implies ( and x14 ( and ( not x15 ) true ) ) ( = tmp237 24 ) )
    ( implies ( and x14 ( and x15 true ) ) ( = tmp237 41 ) )
    ( implies ( and ( not x46 ) ( and ( not x45 ) true ) ) ( = tmp236 0 ) )
    ( implies ( and ( not x46 ) ( and x45 true ) ) ( = tmp236 15 ) )
    ( implies ( and x46 ( and ( not x45 ) true ) ) ( = tmp236 52 ) )
    ( implies ( and x46 ( and x45 true ) ) ( = tmp236 67 ) )
    ( implies ( and ( not x12 ) ( and ( not x13 ) true ) ) ( = tmp235 0 ) )
    ( implies ( and ( not x12 ) ( and x13 true ) ) ( = tmp235 51 ) )
    ( implies ( and x12 ( and ( not x13 ) true ) ) ( = tmp235 30 ) )
    ( implies ( and x12 ( and x13 true ) ) ( = tmp235 81 ) )
    ( implies ( and ( not x48 ) ( and ( not x47 ) true ) ) ( = tmp234 0 ) )
    ( implies ( and ( not x48 ) ( and x47 true ) ) ( = tmp234 29 ) )
    ( implies ( and x48 ( and ( not x47 ) true ) ) ( = tmp234 32 ) )
    ( implies ( and x48 ( and x47 true ) ) ( = tmp234 61 ) )
    ( implies ( and ( not x10 ) ( and ( not x11 ) true ) ) ( = tmp233 0 ) )
    ( implies ( and ( not x10 ) ( and x11 true ) ) ( = tmp233 45 ) )
    ( implies ( and x10 ( and ( not x11 ) true ) ) ( = tmp233 24 ) )
    ( implies ( and x10 ( and x11 true ) ) ( = tmp233 69 ) )
    ( implies ( and ( not x50 ) ( and ( not x49 ) true ) ) ( = tmp232 0 ) )
    ( implies ( and ( not x50 ) ( and x49 true ) ) ( = tmp232 26 ) )
    ( implies ( and x50 ( and ( not x49 ) true ) ) ( = tmp232 10 ) )
    ( implies ( and x50 ( and x49 true ) ) ( = tmp232 36 ) )
    ( implies ( and ( not x8 ) ( and ( not x9 ) true ) ) ( = tmp231 0 ) )
    ( implies ( and ( not x8 ) ( and x9 true ) ) ( = tmp231 20 ) )
    ( implies ( and x8 ( and ( not x9 ) true ) ) ( = tmp231 22 ) )
    ( implies ( and x8 ( and x9 true ) ) ( = tmp231 42 ) )
    ( implies ( and ( not x52 ) ( and ( not x51 ) true ) ) ( = tmp230 0 ) )
    ( implies ( and ( not x52 ) ( and x51 true ) ) ( = tmp230 42 ) )
    ( implies ( and x52 ( and ( not x51 ) true ) ) ( = tmp230 55 ) )
    ( implies ( and x52 ( and x51 true ) ) ( = tmp230 97 ) )
    ( implies ( and ( not x6 ) ( and ( not x7 ) true ) ) ( = tmp229 0 ) )
    ( implies ( and ( not x6 ) ( and x7 true ) ) ( = tmp229 13 ) )
    ( implies ( and x6 ( and ( not x7 ) true ) ) ( = tmp229 51 ) )
    ( implies ( and x6 ( and x7 true ) ) ( = tmp229 64 ) )
    ( implies ( and ( not x54 ) ( and ( not x53 ) true ) ) ( = tmp228 0 ) )
    ( implies ( and ( not x54 ) ( and x53 true ) ) ( = tmp228 6 ) )
    ( implies ( and x54 ( and ( not x53 ) true ) ) ( = tmp228 54 ) )
    ( implies ( and x54 ( and x53 true ) ) ( = tmp228 60 ) )
    ( implies ( and ( not x4 ) ( and ( not x5 ) true ) ) ( = tmp227 0 ) )
    ( implies ( and ( not x4 ) ( and x5 true ) ) ( = tmp227 19 ) )
    ( implies ( and x4 ( and ( not x5 ) true ) ) ( = tmp227 39 ) )
    ( implies ( and x4 ( and x5 true ) ) ( = tmp227 58 ) )
    ( implies ( and ( not x56 ) ( and ( not x55 ) true ) ) ( = tmp226 0 ) )
    ( implies ( and ( not x56 ) ( and x55 true ) ) ( = tmp226 34 ) )
    ( implies ( and x56 ( and ( not x55 ) true ) ) ( = tmp226 32 ) )
    ( implies ( and x56 ( and x55 true ) ) ( = tmp226 66 ) )
    ( implies ( and ( not x2 ) ( and ( not x3 ) true ) ) ( = tmp225 0 ) )
    ( implies ( and ( not x2 ) ( and x3 true ) ) ( = tmp225 13 ) )
    ( implies ( and x2 ( and ( not x3 ) true ) ) ( = tmp225 34 ) )
    ( implies ( and x2 ( and x3 true ) ) ( = tmp225 47 ) )
    ( implies ( and ( not x30 ) true ) ( = tmp224 0 ) )
    ( implies ( and x30 true ) ( = tmp224 42 ) )
    ( implies ( and ( not x28 ) ( and ( not x29 ) true ) ) ( = tmp223 0 ) )
    ( implies ( and ( not x28 ) ( and x29 true ) ) ( = tmp223 41 ) )
    ( implies ( and x28 ( and ( not x29 ) true ) ) ( = tmp223 44 ) )
    ( implies ( and x28 ( and x29 true ) ) ( = tmp223 85 ) )
    ( implies ( and ( not x32 ) ( and ( not x31 ) true ) ) ( = tmp222 0 ) )
    ( implies ( and ( not x32 ) ( and x31 true ) ) ( = tmp222 29 ) )
    ( implies ( and x32 ( and ( not x31 ) true ) ) ( = tmp222 8 ) )
    ( implies ( and x32 ( and x31 true ) ) ( = tmp222 37 ) )
    ( implies ( and ( not x26 ) ( and ( not x27 ) true ) ) ( = tmp221 0 ) )
    ( implies ( and ( not x26 ) ( and x27 true ) ) ( = tmp221 14 ) )
    ( implies ( and x26 ( and ( not x27 ) true ) ) ( = tmp221 50 ) )
    ( implies ( and x26 ( and x27 true ) ) ( = tmp221 64 ) )
    ( implies ( and ( not x34 ) ( and ( not x33 ) true ) ) ( = tmp220 0 ) )
    ( implies ( and ( not x34 ) ( and x33 true ) ) ( = tmp220 24 ) )
    ( implies ( and x34 ( and ( not x33 ) true ) ) ( = tmp220 16 ) )
    ( implies ( and x34 ( and x33 true ) ) ( = tmp220 40 ) )
    ( implies ( and ( not x24 ) ( and ( not x25 ) true ) ) ( = tmp219 0 ) )
    ( implies ( and ( not x24 ) ( and x25 true ) ) ( = tmp219 30 ) )
    ( implies ( and x24 ( and ( not x25 ) true ) ) ( = tmp219 40 ) )
    ( implies ( and x24 ( and x25 true ) ) ( = tmp219 70 ) )
    ( implies ( and ( not x36 ) ( and ( not x35 ) true ) ) ( = tmp218 0 ) )
    ( implies ( and ( not x36 ) ( and x35 true ) ) ( = tmp218 27 ) )
    ( implies ( and x36 ( and ( not x35 ) true ) ) ( = tmp218 15 ) )
    ( implies ( and x36 ( and x35 true ) ) ( = tmp218 42 ) )
    ( implies ( and ( not x22 ) ( and ( not x23 ) true ) ) ( = tmp217 0 ) )
    ( implies ( and ( not x22 ) ( and x23 true ) ) ( = tmp217 10 ) )
    ( implies ( and x22 ( and ( not x23 ) true ) ) ( = tmp217 54 ) )
    ( implies ( and x22 ( and x23 true ) ) ( = tmp217 64 ) )
    ( implies ( and ( not x38 ) ( and ( not x37 ) true ) ) ( = tmp216 0 ) )
    ( implies ( and ( not x38 ) ( and x37 true ) ) ( = tmp216 31 ) )
    ( implies ( and x38 ( and ( not x37 ) true ) ) ( = tmp216 34 ) )
    ( implies ( and x38 ( and x37 true ) ) ( = tmp216 65 ) )
    ( implies ( and ( not x20 ) ( and ( not x21 ) true ) ) ( = tmp215 0 ) )
    ( implies ( and ( not x20 ) ( and x21 true ) ) ( = tmp215 40 ) )
    ( implies ( and x20 ( and ( not x21 ) true ) ) ( = tmp215 31 ) )
    ( implies ( and x20 ( and x21 true ) ) ( = tmp215 71 ) )
    ( implies ( and ( not x40 ) ( and ( not x39 ) true ) ) ( = tmp214 0 ) )
    ( implies ( and ( not x40 ) ( and x39 true ) ) ( = tmp214 42 ) )
    ( implies ( and x40 ( and ( not x39 ) true ) ) ( = tmp214 28 ) )
    ( implies ( and x40 ( and x39 true ) ) ( = tmp214 70 ) )
    ( implies ( and ( not x18 ) ( and ( not x19 ) true ) ) ( = tmp213 0 ) )
    ( implies ( and ( not x18 ) ( and x19 true ) ) ( = tmp213 24 ) )
    ( implies ( and x18 ( and ( not x19 ) true ) ) ( = tmp213 20 ) )
    ( implies ( and x18 ( and x19 true ) ) ( = tmp213 44 ) )
    ( implies ( and ( not x42 ) ( and ( not x41 ) true ) ) ( = tmp212 0 ) )
    ( implies ( and ( not x42 ) ( and x41 true ) ) ( = tmp212 53 ) )
    ( implies ( and x42 ( and ( not x41 ) true ) ) ( = tmp212 17 ) )
    ( implies ( and x42 ( and x41 true ) ) ( = tmp212 70 ) )
    ( implies ( and ( not x16 ) ( and ( not x17 ) true ) ) ( = tmp211 0 ) )
    ( implies ( and ( not x16 ) ( and x17 true ) ) ( = tmp211 53 ) )
    ( implies ( and x16 ( and ( not x17 ) true ) ) ( = tmp211 15 ) )
    ( implies ( and x16 ( and x17 true ) ) ( = tmp211 68 ) )
    ( implies ( and ( not x44 ) ( and ( not x43 ) true ) ) ( = tmp210 0 ) )
    ( implies ( and ( not x44 ) ( and x43 true ) ) ( = tmp210 18 ) )
    ( implies ( and x44 ( and ( not x43 ) true ) ) ( = tmp210 48 ) )
    ( implies ( and x44 ( and x43 true ) ) ( = tmp210 66 ) )
    ( implies ( and ( not x14 ) ( and ( not x15 ) true ) ) ( = tmp209 0 ) )
    ( implies ( and ( not x14 ) ( and x15 true ) ) ( = tmp209 6 ) )
    ( implies ( and x14 ( and ( not x15 ) true ) ) ( = tmp209 47 ) )
    ( implies ( and x14 ( and x15 true ) ) ( = tmp209 53 ) )
    ( implies ( and ( not x46 ) ( and ( not x45 ) true ) ) ( = tmp208 0 ) )
    ( implies ( and ( not x46 ) ( and x45 true ) ) ( = tmp208 8 ) )
    ( implies ( and x46 ( and ( not x45 ) true ) ) ( = tmp208 19 ) )
    ( implies ( and x46 ( and x45 true ) ) ( = tmp208 27 ) )
    ( implies ( and ( not x12 ) ( and ( not x13 ) true ) ) ( = tmp207 0 ) )
    ( implies ( and ( not x12 ) ( and x13 true ) ) ( = tmp207 50 ) )
    ( implies ( and x12 ( and ( not x13 ) true ) ) ( = tmp207 45 ) )
    ( implies ( and x12 ( and x13 true ) ) ( = tmp207 95 ) )
    ( implies ( and ( not x48 ) ( and ( not x47 ) true ) ) ( = tmp206 0 ) )
    ( implies ( and ( not x48 ) ( and x47 true ) ) ( = tmp206 7 ) )
    ( implies ( and x48 ( and ( not x47 ) true ) ) ( = tmp206 6 ) )
    ( implies ( and x48 ( and x47 true ) ) ( = tmp206 13 ) )
    ( implies ( and ( not x10 ) ( and ( not x11 ) true ) ) ( = tmp205 0 ) )
    ( implies ( and ( not x10 ) ( and x11 true ) ) ( = tmp205 31 ) )
    ( implies ( and x10 ( and ( not x11 ) true ) ) ( = tmp205 24 ) )
    ( implies ( and x10 ( and x11 true ) ) ( = tmp205 55 ) )
    ( implies ( and ( not x50 ) ( and ( not x49 ) true ) ) ( = tmp204 0 ) )
    ( implies ( and ( not x50 ) ( and x49 true ) ) ( = tmp204 35 ) )
    ( implies ( and x50 ( and ( not x49 ) true ) ) ( = tmp204 27 ) )
    ( implies ( and x50 ( and x49 true ) ) ( = tmp204 62 ) )
    ( implies ( and ( not x8 ) ( and ( not x9 ) true ) ) ( = tmp203 0 ) )
    ( implies ( and ( not x8 ) ( and x9 true ) ) ( = tmp203 52 ) )
    ( implies ( and x8 ( and ( not x9 ) true ) ) ( = tmp203 32 ) )
    ( implies ( and x8 ( and x9 true ) ) ( = tmp203 84 ) )
    ( implies ( and ( not x52 ) ( and ( not x51 ) true ) ) ( = tmp202 0 ) )
    ( implies ( and ( not x52 ) ( and x51 true ) ) ( = tmp202 33 ) )
    ( implies ( and x52 ( and ( not x51 ) true ) ) ( = tmp202 20 ) )
    ( implies ( and x52 ( and x51 true ) ) ( = tmp202 53 ) )
    ( implies ( and ( not x6 ) ( and ( not x7 ) true ) ) ( = tmp201 0 ) )
    ( implies ( and ( not x6 ) ( and x7 true ) ) ( = tmp201 11 ) )
    ( implies ( and x6 ( and ( not x7 ) true ) ) ( = tmp201 20 ) )
    ( implies ( and x6 ( and x7 true ) ) ( = tmp201 31 ) )
    ( implies ( and ( not x54 ) ( and ( not x53 ) true ) ) ( = tmp200 0 ) )
    ( implies ( and ( not x54 ) ( and x53 true ) ) ( = tmp200 25 ) )
    ( implies ( and x54 ( and ( not x53 ) true ) ) ( = tmp200 39 ) )
    ( implies ( and x54 ( and x53 true ) ) ( = tmp200 64 ) )
    ( implies ( and ( not x4 ) ( and ( not x5 ) true ) ) ( = tmp199 0 ) )
    ( implies ( and ( not x4 ) ( and x5 true ) ) ( = tmp199 46 ) )
    ( implies ( and x4 ( and ( not x5 ) true ) ) ( = tmp199 24 ) )
    ( implies ( and x4 ( and x5 true ) ) ( = tmp199 70 ) )
    ( implies ( and ( not x56 ) ( and ( not x55 ) true ) ) ( = tmp198 0 ) )
    ( implies ( and ( not x56 ) ( and x55 true ) ) ( = tmp198 55 ) )
    ( implies ( and x56 ( and ( not x55 ) true ) ) ( = tmp198 51 ) )
    ( implies ( and x56 ( and x55 true ) ) ( = tmp198 106 ) )
    ( implies ( and ( not x2 ) ( and ( not x3 ) true ) ) ( = tmp197 0 ) )
    ( implies ( and ( not x2 ) ( and x3 true ) ) ( = tmp197 42 ) )
    ( implies ( and x2 ( and ( not x3 ) true ) ) ( = tmp197 38 ) )
    ( implies ( and x2 ( and x3 true ) ) ( = tmp197 80 ) )
    ( implies ( and ( not x30 ) true ) ( = tmp196 0 ) )
    ( implies ( and x30 true ) ( = tmp196 33 ) )
    ( implies ( and ( not x28 ) ( and ( not x29 ) true ) ) ( = tmp195 0 ) )
    ( implies ( and ( not x28 ) ( and x29 true ) ) ( = tmp195 12 ) )
    ( implies ( and x28 ( and ( not x29 ) true ) ) ( = tmp195 7 ) )
    ( implies ( and x28 ( and x29 true ) ) ( = tmp195 19 ) )
    ( implies ( and ( not x32 ) ( and ( not x31 ) true ) ) ( = tmp194 0 ) )
    ( implies ( and ( not x32 ) ( and x31 true ) ) ( = tmp194 42 ) )
    ( implies ( and x32 ( and ( not x31 ) true ) ) ( = tmp194 41 ) )
    ( implies ( and x32 ( and x31 true ) ) ( = tmp194 83 ) )
    ( implies ( and ( not x26 ) ( and ( not x27 ) true ) ) ( = tmp193 0 ) )
    ( implies ( and ( not x26 ) ( and x27 true ) ) ( = tmp193 6 ) )
    ( implies ( and x26 ( and ( not x27 ) true ) ) ( = tmp193 10 ) )
    ( implies ( and x26 ( and x27 true ) ) ( = tmp193 16 ) )
    ( implies ( and ( not x34 ) ( and ( not x33 ) true ) ) ( = tmp192 0 ) )
    ( implies ( and ( not x34 ) ( and x33 true ) ) ( = tmp192 37 ) )
    ( implies ( and x34 ( and ( not x33 ) true ) ) ( = tmp192 17 ) )
    ( implies ( and x34 ( and x33 true ) ) ( = tmp192 54 ) )
    ( implies ( and ( not x24 ) ( and ( not x25 ) true ) ) ( = tmp191 0 ) )
    ( implies ( and ( not x24 ) ( and x25 true ) ) ( = tmp191 31 ) )
    ( implies ( and x24 ( and ( not x25 ) true ) ) ( = tmp191 26 ) )
    ( implies ( and x24 ( and x25 true ) ) ( = tmp191 57 ) )
    ( implies ( and ( not x36 ) ( and ( not x35 ) true ) ) ( = tmp190 0 ) )
    ( implies ( and ( not x36 ) ( and x35 true ) ) ( = tmp190 55 ) )
    ( implies ( and x36 ( and ( not x35 ) true ) ) ( = tmp190 48 ) )
    ( implies ( and x36 ( and x35 true ) ) ( = tmp190 103 ) )
    ( implies ( and ( not x22 ) ( and ( not x23 ) true ) ) ( = tmp189 0 ) )
    ( implies ( and ( not x22 ) ( and x23 true ) ) ( = tmp189 8 ) )
    ( implies ( and x22 ( and ( not x23 ) true ) ) ( = tmp189 7 ) )
    ( implies ( and x22 ( and x23 true ) ) ( = tmp189 15 ) )
    ( implies ( and ( not x38 ) ( and ( not x37 ) true ) ) ( = tmp188 0 ) )
    ( implies ( and ( not x38 ) ( and x37 true ) ) ( = tmp188 31 ) )
    ( implies ( and x38 ( and ( not x37 ) true ) ) ( = tmp188 20 ) )
    ( implies ( and x38 ( and x37 true ) ) ( = tmp188 51 ) )
    ( implies ( and ( not x20 ) ( and ( not x21 ) true ) ) ( = tmp187 0 ) )
    ( implies ( and ( not x20 ) ( and x21 true ) ) ( = tmp187 43 ) )
    ( implies ( and x20 ( and ( not x21 ) true ) ) ( = tmp187 29 ) )
    ( implies ( and x20 ( and x21 true ) ) ( = tmp187 72 ) )
    ( implies ( and ( not x40 ) ( and ( not x39 ) true ) ) ( = tmp186 0 ) )
    ( implies ( and ( not x40 ) ( and x39 true ) ) ( = tmp186 17 ) )
    ( implies ( and x40 ( and ( not x39 ) true ) ) ( = tmp186 21 ) )
    ( implies ( and x40 ( and x39 true ) ) ( = tmp186 38 ) )
    ( implies ( and ( not x18 ) ( and ( not x19 ) true ) ) ( = tmp185 0 ) )
    ( implies ( and ( not x18 ) ( and x19 true ) ) ( = tmp185 14 ) )
    ( implies ( and x18 ( and ( not x19 ) true ) ) ( = tmp185 52 ) )
    ( implies ( and x18 ( and x19 true ) ) ( = tmp185 66 ) )
    ( implies ( and ( not x42 ) ( and ( not x41 ) true ) ) ( = tmp184 0 ) )
    ( implies ( and ( not x42 ) ( and x41 true ) ) ( = tmp184 11 ) )
    ( implies ( and x42 ( and ( not x41 ) true ) ) ( = tmp184 19 ) )
    ( implies ( and x42 ( and x41 true ) ) ( = tmp184 30 ) )
    ( implies ( and ( not x16 ) ( and ( not x17 ) true ) ) ( = tmp183 0 ) )
    ( implies ( and ( not x16 ) ( and x17 true ) ) ( = tmp183 36 ) )
    ( implies ( and x16 ( and ( not x17 ) true ) ) ( = tmp183 6 ) )
    ( implies ( and x16 ( and x17 true ) ) ( = tmp183 42 ) )
    ( implies ( and ( not x44 ) ( and ( not x43 ) true ) ) ( = tmp182 0 ) )
    ( implies ( and ( not x44 ) ( and x43 true ) ) ( = tmp182 13 ) )
    ( implies ( and x44 ( and ( not x43 ) true ) ) ( = tmp182 34 ) )
    ( implies ( and x44 ( and x43 true ) ) ( = tmp182 47 ) )
    ( implies ( and ( not x14 ) ( and ( not x15 ) true ) ) ( = tmp181 0 ) )
    ( implies ( and ( not x14 ) ( and x15 true ) ) ( = tmp181 26 ) )
    ( implies ( and x14 ( and ( not x15 ) true ) ) ( = tmp181 10 ) )
    ( implies ( and x14 ( and x15 true ) ) ( = tmp181 36 ) )
    ( implies ( and ( not x46 ) ( and ( not x45 ) true ) ) ( = tmp180 0 ) )
    ( implies ( and ( not x46 ) ( and x45 true ) ) ( = tmp180 24 ) )
    ( implies ( and x46 ( and ( not x45 ) true ) ) ( = tmp180 35 ) )
    ( implies ( and x46 ( and x45 true ) ) ( = tmp180 59 ) )
    ( implies ( and ( not x12 ) ( and ( not x13 ) true ) ) ( = tmp179 0 ) )
    ( implies ( and ( not x12 ) ( and x13 true ) ) ( = tmp179 27 ) )
    ( implies ( and x12 ( and ( not x13 ) true ) ) ( = tmp179 48 ) )
    ( implies ( and x12 ( and x13 true ) ) ( = tmp179 75 ) )
    ( implies ( and ( not x48 ) ( and ( not x47 ) true ) ) ( = tmp178 0 ) )
    ( implies ( and ( not x48 ) ( and x47 true ) ) ( = tmp178 35 ) )
    ( implies ( and x48 ( and ( not x47 ) true ) ) ( = tmp178 55 ) )
    ( implies ( and x48 ( and x47 true ) ) ( = tmp178 90 ) )
    ( implies ( and ( not x10 ) ( and ( not x11 ) true ) ) ( = tmp177 0 ) )
    ( implies ( and ( not x10 ) ( and x11 true ) ) ( = tmp177 6 ) )
    ( implies ( and x10 ( and ( not x11 ) true ) ) ( = tmp177 47 ) )
    ( implies ( and x10 ( and x11 true ) ) ( = tmp177 53 ) )
    ( implies ( and ( not x50 ) ( and ( not x49 ) true ) ) ( = tmp176 0 ) )
    ( implies ( and ( not x50 ) ( and x49 true ) ) ( = tmp176 31 ) )
    ( implies ( and x50 ( and ( not x49 ) true ) ) ( = tmp176 44 ) )
    ( implies ( and x50 ( and x49 true ) ) ( = tmp176 75 ) )
    ( implies ( and ( not x8 ) ( and ( not x9 ) true ) ) ( = tmp175 0 ) )
    ( implies ( and ( not x8 ) ( and x9 true ) ) ( = tmp175 46 ) )
    ( implies ( and x8 ( and ( not x9 ) true ) ) ( = tmp175 24 ) )
    ( implies ( and x8 ( and x9 true ) ) ( = tmp175 70 ) )
    ( implies ( and ( not x52 ) ( and ( not x51 ) true ) ) ( = tmp174 0 ) )
    ( implies ( and ( not x52 ) ( and x51 true ) ) ( = tmp174 29 ) )
    ( implies ( and x52 ( and ( not x51 ) true ) ) ( = tmp174 19 ) )
    ( implies ( and x52 ( and x51 true ) ) ( = tmp174 48 ) )
    ( implies ( and ( not x6 ) ( and ( not x7 ) true ) ) ( = tmp173 0 ) )
    ( implies ( and ( not x6 ) ( and x7 true ) ) ( = tmp173 21 ) )
    ( implies ( and x6 ( and ( not x7 ) true ) ) ( = tmp173 18 ) )
    ( implies ( and x6 ( and x7 true ) ) ( = tmp173 39 ) )
    ( implies ( and ( not x54 ) ( and ( not x53 ) true ) ) ( = tmp172 0 ) )
    ( implies ( and ( not x54 ) ( and x53 true ) ) ( = tmp172 46 ) )
    ( implies ( and x54 ( and ( not x53 ) true ) ) ( = tmp172 33 ) )
    ( implies ( and x54 ( and x53 true ) ) ( = tmp172 79 ) )
    ( implies ( and ( not x4 ) ( and ( not x5 ) true ) ) ( = tmp171 0 ) )
    ( implies ( and ( not x4 ) ( and x5 true ) ) ( = tmp171 16 ) )
    ( implies ( and x4 ( and ( not x5 ) true ) ) ( = tmp171 18 ) )
    ( implies ( and x4 ( and x5 true ) ) ( = tmp171 34 ) )
    ( implies ( and ( not x56 ) ( and ( not x55 ) true ) ) ( = tmp170 0 ) )
    ( implies ( and ( not x56 ) ( and x55 true ) ) ( = tmp170 41 ) )
    ( implies ( and x56 ( and ( not x55 ) true ) ) ( = tmp170 22 ) )
    ( implies ( and x56 ( and x55 true ) ) ( = tmp170 63 ) )
    ( implies ( and ( not x2 ) ( and ( not x3 ) true ) ) ( = tmp169 0 ) )
    ( implies ( and ( not x2 ) ( and x3 true ) ) ( = tmp169 30 ) )
    ( implies ( and x2 ( and ( not x3 ) true ) ) ( = tmp169 8 ) )
    ( implies ( and x2 ( and x3 true ) ) ( = tmp169 38 ) )
    ( implies ( and ( not x30 ) true ) ( = tmp168 0 ) )
    ( implies ( and x30 true ) ( = tmp168 44 ) )
    ( implies ( and ( not x28 ) ( and ( not x29 ) true ) ) ( = tmp167 0 ) )
    ( implies ( and ( not x28 ) ( and x29 true ) ) ( = tmp167 12 ) )
    ( implies ( and x28 ( and ( not x29 ) true ) ) ( = tmp167 41 ) )
    ( implies ( and x28 ( and x29 true ) ) ( = tmp167 53 ) )
    ( implies ( and ( not x32 ) ( and ( not x31 ) true ) ) ( = tmp166 0 ) )
    ( implies ( and ( not x32 ) ( and x31 true ) ) ( = tmp166 7 ) )
    ( implies ( and x32 ( and ( not x31 ) true ) ) ( = tmp166 12 ) )
    ( implies ( and x32 ( and x31 true ) ) ( = tmp166 19 ) )
    ( implies ( and ( not x26 ) ( and ( not x27 ) true ) ) ( = tmp165 0 ) )
    ( implies ( and ( not x26 ) ( and x27 true ) ) ( = tmp165 46 ) )
    ( implies ( and x26 ( and ( not x27 ) true ) ) ( = tmp165 32 ) )
    ( implies ( and x26 ( and x27 true ) ) ( = tmp165 78 ) )
    ( implies ( and ( not x34 ) ( and ( not x33 ) true ) ) ( = tmp164 0 ) )
    ( implies ( and ( not x34 ) ( and x33 true ) ) ( = tmp164 32 ) )
    ( implies ( and x34 ( and ( not x33 ) true ) ) ( = tmp164 30 ) )
    ( implies ( and x34 ( and x33 true ) ) ( = tmp164 62 ) )
    ( implies ( and ( not x24 ) ( and ( not x25 ) true ) ) ( = tmp163 0 ) )
    ( implies ( and ( not x24 ) ( and x25 true ) ) ( = tmp163 30 ) )
    ( implies ( and x24 ( and ( not x25 ) true ) ) ( = tmp163 13 ) )
    ( implies ( and x24 ( and x25 true ) ) ( = tmp163 43 ) )
    ( implies ( and ( not x36 ) ( and ( not x35 ) true ) ) ( = tmp162 0 ) )
    ( implies ( and ( not x36 ) ( and x35 true ) ) ( = tmp162 38 ) )
    ( implies ( and x36 ( and ( not x35 ) true ) ) ( = tmp162 6 ) )
    ( implies ( and x36 ( and x35 true ) ) ( = tmp162 44 ) )
    ( implies ( and ( not x22 ) ( and ( not x23 ) true ) ) ( = tmp161 0 ) )
    ( implies ( and ( not x22 ) ( and x23 true ) ) ( = tmp161 52 ) )
    ( implies ( and x22 ( and ( not x23 ) true ) ) ( = tmp161 6 ) )
    ( implies ( and x22 ( and x23 true ) ) ( = tmp161 58 ) )
    ( implies ( and ( not x38 ) ( and ( not x37 ) true ) ) ( = tmp160 0 ) )
    ( implies ( and ( not x38 ) ( and x37 true ) ) ( = tmp160 36 ) )
    ( implies ( and x38 ( and ( not x37 ) true ) ) ( = tmp160 8 ) )
    ( implies ( and x38 ( and x37 true ) ) ( = tmp160 44 ) )
    ( implies ( and ( not x20 ) ( and ( not x21 ) true ) ) ( = tmp159 0 ) )
    ( implies ( and ( not x20 ) ( and x21 true ) ) ( = tmp159 7 ) )
    ( implies ( and x20 ( and ( not x21 ) true ) ) ( = tmp159 52 ) )
    ( implies ( and x20 ( and x21 true ) ) ( = tmp159 59 ) )
    ( implies ( and ( not x40 ) ( and ( not x39 ) true ) ) ( = tmp158 0 ) )
    ( implies ( and ( not x40 ) ( and x39 true ) ) ( = tmp158 34 ) )
    ( implies ( and x40 ( and ( not x39 ) true ) ) ( = tmp158 34 ) )
    ( implies ( and x40 ( and x39 true ) ) ( = tmp158 68 ) )
    ( implies ( and ( not x18 ) ( and ( not x19 ) true ) ) ( = tmp157 0 ) )
    ( implies ( and ( not x18 ) ( and x19 true ) ) ( = tmp157 27 ) )
    ( implies ( and x18 ( and ( not x19 ) true ) ) ( = tmp157 36 ) )
    ( implies ( and x18 ( and x19 true ) ) ( = tmp157 63 ) )
    ( implies ( and ( not x42 ) ( and ( not x41 ) true ) ) ( = tmp156 0 ) )
    ( implies ( and ( not x42 ) ( and x41 true ) ) ( = tmp156 30 ) )
    ( implies ( and x42 ( and ( not x41 ) true ) ) ( = tmp156 31 ) )
    ( implies ( and x42 ( and x41 true ) ) ( = tmp156 61 ) )
    ( implies ( and ( not x16 ) ( and ( not x17 ) true ) ) ( = tmp155 0 ) )
    ( implies ( and ( not x16 ) ( and x17 true ) ) ( = tmp155 47 ) )
    ( implies ( and x16 ( and ( not x17 ) true ) ) ( = tmp155 41 ) )
    ( implies ( and x16 ( and x17 true ) ) ( = tmp155 88 ) )
    ( implies ( and ( not x44 ) ( and ( not x43 ) true ) ) ( = tmp154 0 ) )
    ( implies ( and ( not x44 ) ( and x43 true ) ) ( = tmp154 13 ) )
    ( implies ( and x44 ( and ( not x43 ) true ) ) ( = tmp154 49 ) )
    ( implies ( and x44 ( and x43 true ) ) ( = tmp154 62 ) )
    ( implies ( and ( not x14 ) ( and ( not x15 ) true ) ) ( = tmp153 0 ) )
    ( implies ( and ( not x14 ) ( and x15 true ) ) ( = tmp153 39 ) )
    ( implies ( and x14 ( and ( not x15 ) true ) ) ( = tmp153 21 ) )
    ( implies ( and x14 ( and x15 true ) ) ( = tmp153 60 ) )
    ( implies ( and ( not x46 ) ( and ( not x45 ) true ) ) ( = tmp152 0 ) )
    ( implies ( and ( not x46 ) ( and x45 true ) ) ( = tmp152 47 ) )
    ( implies ( and x46 ( and ( not x45 ) true ) ) ( = tmp152 48 ) )
    ( implies ( and x46 ( and x45 true ) ) ( = tmp152 95 ) )
    ( implies ( and ( not x12 ) ( and ( not x13 ) true ) ) ( = tmp151 0 ) )
    ( implies ( and ( not x12 ) ( and x13 true ) ) ( = tmp151 24 ) )
    ( implies ( and x12 ( and ( not x13 ) true ) ) ( = tmp151 34 ) )
    ( implies ( and x12 ( and x13 true ) ) ( = tmp151 58 ) )
    ( implies ( and ( not x48 ) ( and ( not x47 ) true ) ) ( = tmp150 0 ) )
    ( implies ( and ( not x48 ) ( and x47 true ) ) ( = tmp150 35 ) )
    ( implies ( and x48 ( and ( not x47 ) true ) ) ( = tmp150 39 ) )
    ( implies ( and x48 ( and x47 true ) ) ( = tmp150 74 ) )
    ( implies ( and ( not x10 ) ( and ( not x11 ) true ) ) ( = tmp149 0 ) )
    ( implies ( and ( not x10 ) ( and x11 true ) ) ( = tmp149 52 ) )
    ( implies ( and x10 ( and ( not x11 ) true ) ) ( = tmp149 26 ) )
    ( implies ( and x10 ( and x11 true ) ) ( = tmp149 78 ) )
    ( implies ( and ( not x50 ) ( and ( not x49 ) true ) ) ( = tmp148 0 ) )
    ( implies ( and ( not x50 ) ( and x49 true ) ) ( = tmp148 29 ) )
    ( implies ( and x50 ( and ( not x49 ) true ) ) ( = tmp148 6 ) )
    ( implies ( and x50 ( and x49 true ) ) ( = tmp148 35 ) )
    ( implies ( and ( not x8 ) ( and ( not x9 ) true ) ) ( = tmp147 0 ) )
    ( implies ( and ( not x8 ) ( and x9 true ) ) ( = tmp147 54 ) )
    ( implies ( and x8 ( and ( not x9 ) true ) ) ( = tmp147 32 ) )
    ( implies ( and x8 ( and x9 true ) ) ( = tmp147 86 ) )
    ( implies ( and ( not x52 ) ( and ( not x51 ) true ) ) ( = tmp146 0 ) )
    ( implies ( and ( not x52 ) ( and x51 true ) ) ( = tmp146 35 ) )
    ( implies ( and x52 ( and ( not x51 ) true ) ) ( = tmp146 32 ) )
    ( implies ( and x52 ( and x51 true ) ) ( = tmp146 67 ) )
    ( implies ( and ( not x6 ) ( and ( not x7 ) true ) ) ( = tmp145 0 ) )
    ( implies ( and ( not x6 ) ( and x7 true ) ) ( = tmp145 26 ) )
    ( implies ( and x6 ( and ( not x7 ) true ) ) ( = tmp145 10 ) )
    ( implies ( and x6 ( and x7 true ) ) ( = tmp145 36 ) )
    ( implies ( and ( not x54 ) ( and ( not x53 ) true ) ) ( = tmp144 0 ) )
    ( implies ( and ( not x54 ) ( and x53 true ) ) ( = tmp144 7 ) )
    ( implies ( and x54 ( and ( not x53 ) true ) ) ( = tmp144 32 ) )
    ( implies ( and x54 ( and x53 true ) ) ( = tmp144 39 ) )
    ( implies ( and ( not x4 ) ( and ( not x5 ) true ) ) ( = tmp143 0 ) )
    ( implies ( and ( not x4 ) ( and x5 true ) ) ( = tmp143 30 ) )
    ( implies ( and x4 ( and ( not x5 ) true ) ) ( = tmp143 30 ) )
    ( implies ( and x4 ( and x5 true ) ) ( = tmp143 60 ) )
    ( implies ( and ( not x56 ) ( and ( not x55 ) true ) ) ( = tmp142 0 ) )
    ( implies ( and ( not x56 ) ( and x55 true ) ) ( = tmp142 40 ) )
    ( implies ( and x56 ( and ( not x55 ) true ) ) ( = tmp142 33 ) )
    ( implies ( and x56 ( and x55 true ) ) ( = tmp142 73 ) )
    ( implies ( and ( not x2 ) ( and ( not x3 ) true ) ) ( = tmp141 0 ) )
    ( implies ( and ( not x2 ) ( and x3 true ) ) ( = tmp141 28 ) )
    ( implies ( and x2 ( and ( not x3 ) true ) ) ( = tmp141 43 ) )
    ( implies ( and x2 ( and x3 true ) ) ( = tmp141 71 ) )
    ( implies ( and ( not x30 ) true ) ( = tmp140 0 ) )
    ( implies ( and x30 true ) ( = tmp140 38 ) )
    ( implies ( and ( not x28 ) ( and ( not x29 ) true ) ) ( = tmp139 0 ) )
    ( implies ( and ( not x28 ) ( and x29 true ) ) ( = tmp139 42 ) )
    ( implies ( and x28 ( and ( not x29 ) true ) ) ( = tmp139 30 ) )
    ( implies ( and x28 ( and x29 true ) ) ( = tmp139 72 ) )
    ( implies ( and ( not x32 ) ( and ( not x31 ) true ) ) ( = tmp138 0 ) )
    ( implies ( and ( not x32 ) ( and x31 true ) ) ( = tmp138 51 ) )
    ( implies ( and x32 ( and ( not x31 ) true ) ) ( = tmp138 6 ) )
    ( implies ( and x32 ( and x31 true ) ) ( = tmp138 57 ) )
    ( implies ( and ( not x26 ) ( and ( not x27 ) true ) ) ( = tmp137 0 ) )
    ( implies ( and ( not x26 ) ( and x27 true ) ) ( = tmp137 10 ) )
    ( implies ( and x26 ( and ( not x27 ) true ) ) ( = tmp137 45 ) )
    ( implies ( and x26 ( and x27 true ) ) ( = tmp137 55 ) )
    ( implies ( and ( not x34 ) ( and ( not x33 ) true ) ) ( = tmp136 0 ) )
    ( implies ( and ( not x34 ) ( and x33 true ) ) ( = tmp136 48 ) )
    ( implies ( and x34 ( and ( not x33 ) true ) ) ( = tmp136 5 ) )
    ( implies ( and x34 ( and x33 true ) ) ( = tmp136 53 ) )
    ( implies ( and ( not x24 ) ( and ( not x25 ) true ) ) ( = tmp135 0 ) )
    ( implies ( and ( not x24 ) ( and x25 true ) ) ( = tmp135 24 ) )
    ( implies ( and x24 ( and ( not x25 ) true ) ) ( = tmp135 11 ) )
    ( implies ( and x24 ( and x25 true ) ) ( = tmp135 35 ) )
    ( implies ( and ( not x36 ) ( and ( not x35 ) true ) ) ( = tmp134 0 ) )
    ( implies ( and ( not x36 ) ( and x35 true ) ) ( = tmp134 25 ) )
    ( implies ( and x36 ( and ( not x35 ) true ) ) ( = tmp134 36 ) )
    ( implies ( and x36 ( and x35 true ) ) ( = tmp134 61 ) )
    ( implies ( and ( not x22 ) ( and ( not x23 ) true ) ) ( = tmp133 0 ) )
    ( implies ( and ( not x22 ) ( and x23 true ) ) ( = tmp133 21 ) )
    ( implies ( and x22 ( and ( not x23 ) true ) ) ( = tmp133 55 ) )
    ( implies ( and x22 ( and x23 true ) ) ( = tmp133 76 ) )
    ( implies ( and ( not x38 ) ( and ( not x37 ) true ) ) ( = tmp132 0 ) )
    ( implies ( and ( not x38 ) ( and x37 true ) ) ( = tmp132 53 ) )
    ( implies ( and x38 ( and ( not x37 ) true ) ) ( = tmp132 24 ) )
    ( implies ( and x38 ( and x37 true ) ) ( = tmp132 77 ) )
    ( implies ( and ( not x20 ) ( and ( not x21 ) true ) ) ( = tmp131 0 ) )
    ( implies ( and ( not x20 ) ( and x21 true ) ) ( = tmp131 42 ) )
    ( implies ( and x20 ( and ( not x21 ) true ) ) ( = tmp131 32 ) )
    ( implies ( and x20 ( and x21 true ) ) ( = tmp131 74 ) )
    ( implies ( and ( not x40 ) ( and ( not x39 ) true ) ) ( = tmp130 0 ) )
    ( implies ( and ( not x40 ) ( and x39 true ) ) ( = tmp130 10 ) )
    ( implies ( and x40 ( and ( not x39 ) true ) ) ( = tmp130 22 ) )
    ( implies ( and x40 ( and x39 true ) ) ( = tmp130 32 ) )
    ( implies ( and ( not x18 ) ( and ( not x19 ) true ) ) ( = tmp129 0 ) )
    ( implies ( and ( not x18 ) ( and x19 true ) ) ( = tmp129 36 ) )
    ( implies ( and x18 ( and ( not x19 ) true ) ) ( = tmp129 50 ) )
    ( implies ( and x18 ( and x19 true ) ) ( = tmp129 86 ) )
    ( implies ( and ( not x42 ) ( and ( not x41 ) true ) ) ( = tmp128 0 ) )
    ( implies ( and ( not x42 ) ( and x41 true ) ) ( = tmp128 31 ) )
    ( implies ( and x42 ( and ( not x41 ) true ) ) ( = tmp128 53 ) )
    ( implies ( and x42 ( and x41 true ) ) ( = tmp128 84 ) )
    ( implies ( and ( not x16 ) ( and ( not x17 ) true ) ) ( = tmp127 0 ) )
    ( implies ( and ( not x16 ) ( and x17 true ) ) ( = tmp127 39 ) )
    ( implies ( and x16 ( and ( not x17 ) true ) ) ( = tmp127 50 ) )
    ( implies ( and x16 ( and x17 true ) ) ( = tmp127 89 ) )
    ( implies ( and ( not x44 ) ( and ( not x43 ) true ) ) ( = tmp126 0 ) )
    ( implies ( and ( not x44 ) ( and x43 true ) ) ( = tmp126 41 ) )
    ( implies ( and x44 ( and ( not x43 ) true ) ) ( = tmp126 10 ) )
    ( implies ( and x44 ( and x43 true ) ) ( = tmp126 51 ) )
    ( implies ( and ( not x14 ) ( and ( not x15 ) true ) ) ( = tmp125 0 ) )
    ( implies ( and ( not x14 ) ( and x15 true ) ) ( = tmp125 49 ) )
    ( implies ( and x14 ( and ( not x15 ) true ) ) ( = tmp125 29 ) )
    ( implies ( and x14 ( and x15 true ) ) ( = tmp125 78 ) )
    ( implies ( and ( not x46 ) ( and ( not x45 ) true ) ) ( = tmp124 0 ) )
    ( implies ( and ( not x46 ) ( and x45 true ) ) ( = tmp124 26 ) )
    ( implies ( and x46 ( and ( not x45 ) true ) ) ( = tmp124 35 ) )
    ( implies ( and x46 ( and x45 true ) ) ( = tmp124 61 ) )
    ( implies ( and ( not x12 ) ( and ( not x13 ) true ) ) ( = tmp123 0 ) )
    ( implies ( and ( not x12 ) ( and x13 true ) ) ( = tmp123 34 ) )
    ( implies ( and x12 ( and ( not x13 ) true ) ) ( = tmp123 24 ) )
    ( implies ( and x12 ( and x13 true ) ) ( = tmp123 58 ) )
    ( implies ( and ( not x48 ) ( and ( not x47 ) true ) ) ( = tmp122 0 ) )
    ( implies ( and ( not x48 ) ( and x47 true ) ) ( = tmp122 55 ) )
    ( implies ( and x48 ( and ( not x47 ) true ) ) ( = tmp122 10 ) )
    ( implies ( and x48 ( and x47 true ) ) ( = tmp122 65 ) )
    ( implies ( and ( not x10 ) ( and ( not x11 ) true ) ) ( = tmp121 0 ) )
    ( implies ( and ( not x10 ) ( and x11 true ) ) ( = tmp121 47 ) )
    ( implies ( and x10 ( and ( not x11 ) true ) ) ( = tmp121 11 ) )
    ( implies ( and x10 ( and x11 true ) ) ( = tmp121 58 ) )
    ( implies ( and ( not x50 ) ( and ( not x49 ) true ) ) ( = tmp120 0 ) )
    ( implies ( and ( not x50 ) ( and x49 true ) ) ( = tmp120 29 ) )
    ( implies ( and x50 ( and ( not x49 ) true ) ) ( = tmp120 36 ) )
    ( implies ( and x50 ( and x49 true ) ) ( = tmp120 65 ) )
    ( implies ( and ( not x8 ) ( and ( not x9 ) true ) ) ( = tmp119 0 ) )
    ( implies ( and ( not x8 ) ( and x9 true ) ) ( = tmp119 24 ) )
    ( implies ( and x8 ( and ( not x9 ) true ) ) ( = tmp119 29 ) )
    ( implies ( and x8 ( and x9 true ) ) ( = tmp119 53 ) )
    ( implies ( and ( not x52 ) ( and ( not x51 ) true ) ) ( = tmp118 0 ) )
    ( implies ( and ( not x52 ) ( and x51 true ) ) ( = tmp118 37 ) )
    ( implies ( and x52 ( and ( not x51 ) true ) ) ( = tmp118 15 ) )
    ( implies ( and x52 ( and x51 true ) ) ( = tmp118 52 ) )
    ( implies ( and ( not x6 ) ( and ( not x7 ) true ) ) ( = tmp117 0 ) )
    ( implies ( and ( not x6 ) ( and x7 true ) ) ( = tmp117 54 ) )
    ( implies ( and x6 ( and ( not x7 ) true ) ) ( = tmp117 53 ) )
    ( implies ( and x6 ( and x7 true ) ) ( = tmp117 107 ) )
    ( implies ( and ( not x54 ) ( and ( not x53 ) true ) ) ( = tmp116 0 ) )
    ( implies ( and ( not x54 ) ( and x53 true ) ) ( = tmp116 36 ) )
    ( implies ( and x54 ( and ( not x53 ) true ) ) ( = tmp116 54 ) )
    ( implies ( and x54 ( and x53 true ) ) ( = tmp116 90 ) )
    ( implies ( and ( not x4 ) ( and ( not x5 ) true ) ) ( = tmp115 0 ) )
    ( implies ( and ( not x4 ) ( and x5 true ) ) ( = tmp115 43 ) )
    ( implies ( and x4 ( and ( not x5 ) true ) ) ( = tmp115 24 ) )
    ( implies ( and x4 ( and x5 true ) ) ( = tmp115 67 ) )
    ( implies ( and ( not x56 ) ( and ( not x55 ) true ) ) ( = tmp114 0 ) )
    ( implies ( and ( not x56 ) ( and x55 true ) ) ( = tmp114 22 ) )
    ( implies ( and x56 ( and ( not x55 ) true ) ) ( = tmp114 55 ) )
    ( implies ( and x56 ( and x55 true ) ) ( = tmp114 77 ) )
    ( implies ( and ( not x2 ) ( and ( not x3 ) true ) ) ( = tmp113 0 ) )
    ( implies ( and ( not x2 ) ( and x3 true ) ) ( = tmp113 9 ) )
    ( implies ( and x2 ( and ( not x3 ) true ) ) ( = tmp113 15 ) )
    ( implies ( and x2 ( and x3 true ) ) ( = tmp113 24 ) )
    ( implies ( and ( not x30 ) true ) ( = tmp112 0 ) )
    ( implies ( and x30 true ) ( = tmp112 48 ) )
    ( implies ( and ( not x28 ) ( and ( not x29 ) true ) ) ( = tmp111 0 ) )
    ( implies ( and ( not x28 ) ( and x29 true ) ) ( = tmp111 33 ) )
    ( implies ( and x28 ( and ( not x29 ) true ) ) ( = tmp111 9 ) )
    ( implies ( and x28 ( and x29 true ) ) ( = tmp111 42 ) )
    ( implies ( and ( not x32 ) ( and ( not x31 ) true ) ) ( = tmp110 0 ) )
    ( implies ( and ( not x32 ) ( and x31 true ) ) ( = tmp110 35 ) )
    ( implies ( and x32 ( and ( not x31 ) true ) ) ( = tmp110 42 ) )
    ( implies ( and x32 ( and x31 true ) ) ( = tmp110 77 ) )
    ( implies ( and ( not x26 ) ( and ( not x27 ) true ) ) ( = tmp109 0 ) )
    ( implies ( and ( not x26 ) ( and x27 true ) ) ( = tmp109 40 ) )
    ( implies ( and x26 ( and ( not x27 ) true ) ) ( = tmp109 38 ) )
    ( implies ( and x26 ( and x27 true ) ) ( = tmp109 78 ) )
    ( implies ( and ( not x34 ) ( and ( not x33 ) true ) ) ( = tmp108 0 ) )
    ( implies ( and ( not x34 ) ( and x33 true ) ) ( = tmp108 26 ) )
    ( implies ( and x34 ( and ( not x33 ) true ) ) ( = tmp108 13 ) )
    ( implies ( and x34 ( and x33 true ) ) ( = tmp108 39 ) )
    ( implies ( and ( not x24 ) ( and ( not x25 ) true ) ) ( = tmp107 0 ) )
    ( implies ( and ( not x24 ) ( and x25 true ) ) ( = tmp107 21 ) )
    ( implies ( and x24 ( and ( not x25 ) true ) ) ( = tmp107 19 ) )
    ( implies ( and x24 ( and x25 true ) ) ( = tmp107 40 ) )
    ( implies ( and ( not x36 ) ( and ( not x35 ) true ) ) ( = tmp106 0 ) )
    ( implies ( and ( not x36 ) ( and x35 true ) ) ( = tmp106 23 ) )
    ( implies ( and x36 ( and ( not x35 ) true ) ) ( = tmp106 55 ) )
    ( implies ( and x36 ( and x35 true ) ) ( = tmp106 78 ) )
    ( implies ( and ( not x22 ) ( and ( not x23 ) true ) ) ( = tmp105 0 ) )
    ( implies ( and ( not x22 ) ( and x23 true ) ) ( = tmp105 33 ) )
    ( implies ( and x22 ( and ( not x23 ) true ) ) ( = tmp105 30 ) )
    ( implies ( and x22 ( and x23 true ) ) ( = tmp105 63 ) )
    ( implies ( and ( not x38 ) ( and ( not x37 ) true ) ) ( = tmp104 0 ) )
    ( implies ( and ( not x38 ) ( and x37 true ) ) ( = tmp104 27 ) )
    ( implies ( and x38 ( and ( not x37 ) true ) ) ( = tmp104 37 ) )
    ( implies ( and x38 ( and x37 true ) ) ( = tmp104 64 ) )
    ( implies ( and ( not x20 ) ( and ( not x21 ) true ) ) ( = tmp103 0 ) )
    ( implies ( and ( not x20 ) ( and x21 true ) ) ( = tmp103 42 ) )
    ( implies ( and x20 ( and ( not x21 ) true ) ) ( = tmp103 34 ) )
    ( implies ( and x20 ( and x21 true ) ) ( = tmp103 76 ) )
    ( implies ( and ( not x40 ) ( and ( not x39 ) true ) ) ( = tmp102 0 ) )
    ( implies ( and ( not x40 ) ( and x39 true ) ) ( = tmp102 30 ) )
    ( implies ( and x40 ( and ( not x39 ) true ) ) ( = tmp102 20 ) )
    ( implies ( and x40 ( and x39 true ) ) ( = tmp102 50 ) )
    ( implies ( and ( not x18 ) ( and ( not x19 ) true ) ) ( = tmp101 0 ) )
    ( implies ( and ( not x18 ) ( and x19 true ) ) ( = tmp101 39 ) )
    ( implies ( and x18 ( and ( not x19 ) true ) ) ( = tmp101 5 ) )
    ( implies ( and x18 ( and x19 true ) ) ( = tmp101 44 ) )
    ( implies ( and ( not x42 ) ( and ( not x41 ) true ) ) ( = tmp100 0 ) )
    ( implies ( and ( not x42 ) ( and x41 true ) ) ( = tmp100 14 ) )
    ( implies ( and x42 ( and ( not x41 ) true ) ) ( = tmp100 5 ) )
    ( implies ( and x42 ( and x41 true ) ) ( = tmp100 19 ) )
    ( implies ( and ( not x16 ) ( and ( not x17 ) true ) ) ( = tmp99 0 ) )
    ( implies ( and ( not x16 ) ( and x17 true ) ) ( = tmp99 33 ) )
    ( implies ( and x16 ( and ( not x17 ) true ) ) ( = tmp99 52 ) )
    ( implies ( and x16 ( and x17 true ) ) ( = tmp99 85 ) )
    ( implies ( and ( not x44 ) ( and ( not x43 ) true ) ) ( = tmp98 0 ) )
    ( implies ( and ( not x44 ) ( and x43 true ) ) ( = tmp98 42 ) )
    ( implies ( and x44 ( and ( not x43 ) true ) ) ( = tmp98 49 ) )
    ( implies ( and x44 ( and x43 true ) ) ( = tmp98 91 ) )
    ( implies ( and ( not x14 ) ( and ( not x15 ) true ) ) ( = tmp97 0 ) )
    ( implies ( and ( not x14 ) ( and x15 true ) ) ( = tmp97 37 ) )
    ( implies ( and x14 ( and ( not x15 ) true ) ) ( = tmp97 47 ) )
    ( implies ( and x14 ( and x15 true ) ) ( = tmp97 84 ) )
    ( implies ( and ( not x46 ) ( and ( not x45 ) true ) ) ( = tmp96 0 ) )
    ( implies ( and ( not x46 ) ( and x45 true ) ) ( = tmp96 47 ) )
    ( implies ( and x46 ( and ( not x45 ) true ) ) ( = tmp96 24 ) )
    ( implies ( and x46 ( and x45 true ) ) ( = tmp96 71 ) )
    ( implies ( and ( not x12 ) ( and ( not x13 ) true ) ) ( = tmp95 0 ) )
    ( implies ( and ( not x12 ) ( and x13 true ) ) ( = tmp95 39 ) )
    ( implies ( and x12 ( and ( not x13 ) true ) ) ( = tmp95 26 ) )
    ( implies ( and x12 ( and x13 true ) ) ( = tmp95 65 ) )
    ( implies ( and ( not x48 ) ( and ( not x47 ) true ) ) ( = tmp94 0 ) )
    ( implies ( and ( not x48 ) ( and x47 true ) ) ( = tmp94 45 ) )
    ( implies ( and x48 ( and ( not x47 ) true ) ) ( = tmp94 25 ) )
    ( implies ( and x48 ( and x47 true ) ) ( = tmp94 70 ) )
    ( implies ( and ( not x10 ) ( and ( not x11 ) true ) ) ( = tmp93 0 ) )
    ( implies ( and ( not x10 ) ( and x11 true ) ) ( = tmp93 30 ) )
    ( implies ( and x10 ( and ( not x11 ) true ) ) ( = tmp93 32 ) )
    ( implies ( and x10 ( and x11 true ) ) ( = tmp93 62 ) )
    ( implies ( and ( not x50 ) ( and ( not x49 ) true ) ) ( = tmp92 0 ) )
    ( implies ( and ( not x50 ) ( and x49 true ) ) ( = tmp92 24 ) )
    ( implies ( and x50 ( and ( not x49 ) true ) ) ( = tmp92 28 ) )
    ( implies ( and x50 ( and x49 true ) ) ( = tmp92 52 ) )
    ( implies ( and ( not x8 ) ( and ( not x9 ) true ) ) ( = tmp91 0 ) )
    ( implies ( and ( not x8 ) ( and x9 true ) ) ( = tmp91 48 ) )
    ( implies ( and x8 ( and ( not x9 ) true ) ) ( = tmp91 30 ) )
    ( implies ( and x8 ( and x9 true ) ) ( = tmp91 78 ) )
    ( implies ( and ( not x52 ) ( and ( not x51 ) true ) ) ( = tmp90 0 ) )
    ( implies ( and ( not x52 ) ( and x51 true ) ) ( = tmp90 54 ) )
    ( implies ( and x52 ( and ( not x51 ) true ) ) ( = tmp90 11 ) )
    ( implies ( and x52 ( and x51 true ) ) ( = tmp90 65 ) )
    ( implies ( and ( not x6 ) ( and ( not x7 ) true ) ) ( = tmp89 0 ) )
    ( implies ( and ( not x6 ) ( and x7 true ) ) ( = tmp89 19 ) )
    ( implies ( and x6 ( and ( not x7 ) true ) ) ( = tmp89 19 ) )
    ( implies ( and x6 ( and x7 true ) ) ( = tmp89 38 ) )
    ( implies ( and ( not x54 ) ( and ( not x53 ) true ) ) ( = tmp88 0 ) )
    ( implies ( and ( not x54 ) ( and x53 true ) ) ( = tmp88 53 ) )
    ( implies ( and x54 ( and ( not x53 ) true ) ) ( = tmp88 32 ) )
    ( implies ( and x54 ( and x53 true ) ) ( = tmp88 85 ) )
    ( implies ( and ( not x4 ) ( and ( not x5 ) true ) ) ( = tmp87 0 ) )
    ( implies ( and ( not x4 ) ( and x5 true ) ) ( = tmp87 34 ) )
    ( implies ( and x4 ( and ( not x5 ) true ) ) ( = tmp87 36 ) )
    ( implies ( and x4 ( and x5 true ) ) ( = tmp87 70 ) )
    ( implies ( and ( not x56 ) ( and ( not x55 ) true ) ) ( = tmp86 0 ) )
    ( implies ( and ( not x56 ) ( and x55 true ) ) ( = tmp86 25 ) )
    ( implies ( and x56 ( and ( not x55 ) true ) ) ( = tmp86 19 ) )
    ( implies ( and x56 ( and x55 true ) ) ( = tmp86 44 ) )
    ( implies ( and ( not x2 ) ( and ( not x3 ) true ) ) ( = tmp85 0 ) )
    ( implies ( and ( not x2 ) ( and x3 true ) ) ( = tmp85 34 ) )
    ( implies ( and x2 ( and ( not x3 ) true ) ) ( = tmp85 33 ) )
    ( implies ( and x2 ( and x3 true ) ) ( = tmp85 67 ) )
    ( implies ( and ( not x30 ) true ) ( = tmp84 0 ) )
    ( implies ( and x30 true ) ( = tmp84 41 ) )
    ( implies ( and ( not x28 ) ( and ( not x29 ) true ) ) ( = tmp83 0 ) )
    ( implies ( and ( not x28 ) ( and x29 true ) ) ( = tmp83 5 ) )
    ( implies ( and x28 ( and ( not x29 ) true ) ) ( = tmp83 27 ) )
    ( implies ( and x28 ( and x29 true ) ) ( = tmp83 32 ) )
    ( implies ( and ( not x32 ) ( and ( not x31 ) true ) ) ( = tmp82 0 ) )
    ( implies ( and ( not x32 ) ( and x31 true ) ) ( = tmp82 39 ) )
    ( implies ( and x32 ( and ( not x31 ) true ) ) ( = tmp82 52 ) )
    ( implies ( and x32 ( and x31 true ) ) ( = tmp82 91 ) )
    ( implies ( and ( not x26 ) ( and ( not x27 ) true ) ) ( = tmp81 0 ) )
    ( implies ( and ( not x26 ) ( and x27 true ) ) ( = tmp81 8 ) )
    ( implies ( and x26 ( and ( not x27 ) true ) ) ( = tmp81 25 ) )
    ( implies ( and x26 ( and x27 true ) ) ( = tmp81 33 ) )
    ( implies ( and ( not x34 ) ( and ( not x33 ) true ) ) ( = tmp80 0 ) )
    ( implies ( and ( not x34 ) ( and x33 true ) ) ( = tmp80 33 ) )
    ( implies ( and x34 ( and ( not x33 ) true ) ) ( = tmp80 17 ) )
    ( implies ( and x34 ( and x33 true ) ) ( = tmp80 50 ) )
    ( implies ( and ( not x24 ) ( and ( not x25 ) true ) ) ( = tmp79 0 ) )
    ( implies ( and ( not x24 ) ( and x25 true ) ) ( = tmp79 19 ) )
    ( implies ( and x24 ( and ( not x25 ) true ) ) ( = tmp79 43 ) )
    ( implies ( and x24 ( and x25 true ) ) ( = tmp79 62 ) )
    ( implies ( and ( not x36 ) ( and ( not x35 ) true ) ) ( = tmp78 0 ) )
    ( implies ( and ( not x36 ) ( and x35 true ) ) ( = tmp78 5 ) )
    ( implies ( and x36 ( and ( not x35 ) true ) ) ( = tmp78 34 ) )
    ( implies ( and x36 ( and x35 true ) ) ( = tmp78 39 ) )
    ( implies ( and ( not x22 ) ( and ( not x23 ) true ) ) ( = tmp77 0 ) )
    ( implies ( and ( not x22 ) ( and x23 true ) ) ( = tmp77 42 ) )
    ( implies ( and x22 ( and ( not x23 ) true ) ) ( = tmp77 45 ) )
    ( implies ( and x22 ( and x23 true ) ) ( = tmp77 87 ) )
    ( implies ( and ( not x38 ) ( and ( not x37 ) true ) ) ( = tmp76 0 ) )
    ( implies ( and ( not x38 ) ( and x37 true ) ) ( = tmp76 11 ) )
    ( implies ( and x38 ( and ( not x37 ) true ) ) ( = tmp76 21 ) )
    ( implies ( and x38 ( and x37 true ) ) ( = tmp76 32 ) )
    ( implies ( and ( not x20 ) ( and ( not x21 ) true ) ) ( = tmp75 0 ) )
    ( implies ( and ( not x20 ) ( and x21 true ) ) ( = tmp75 52 ) )
    ( implies ( and x20 ( and ( not x21 ) true ) ) ( = tmp75 50 ) )
    ( implies ( and x20 ( and x21 true ) ) ( = tmp75 102 ) )
    ( implies ( and ( not x40 ) ( and ( not x39 ) true ) ) ( = tmp74 0 ) )
    ( implies ( and ( not x40 ) ( and x39 true ) ) ( = tmp74 16 ) )
    ( implies ( and x40 ( and ( not x39 ) true ) ) ( = tmp74 17 ) )
    ( implies ( and x40 ( and x39 true ) ) ( = tmp74 33 ) )
    ( implies ( and ( not x18 ) ( and ( not x19 ) true ) ) ( = tmp73 0 ) )
    ( implies ( and ( not x18 ) ( and x19 true ) ) ( = tmp73 10 ) )
    ( implies ( and x18 ( and ( not x19 ) true ) ) ( = tmp73 5 ) )
    ( implies ( and x18 ( and x19 true ) ) ( = tmp73 15 ) )
    ( implies ( and ( not x42 ) ( and ( not x41 ) true ) ) ( = tmp72 0 ) )
    ( implies ( and ( not x42 ) ( and x41 true ) ) ( = tmp72 42 ) )
    ( implies ( and x42 ( and ( not x41 ) true ) ) ( = tmp72 23 ) )
    ( implies ( and x42 ( and x41 true ) ) ( = tmp72 65 ) )
    ( implies ( and ( not x16 ) ( and ( not x17 ) true ) ) ( = tmp71 0 ) )
    ( implies ( and ( not x16 ) ( and x17 true ) ) ( = tmp71 46 ) )
    ( implies ( and x16 ( and ( not x17 ) true ) ) ( = tmp71 55 ) )
    ( implies ( and x16 ( and x17 true ) ) ( = tmp71 101 ) )
    ( implies ( and ( not x44 ) ( and ( not x43 ) true ) ) ( = tmp70 0 ) )
    ( implies ( and ( not x44 ) ( and x43 true ) ) ( = tmp70 43 ) )
    ( implies ( and x44 ( and ( not x43 ) true ) ) ( = tmp70 5 ) )
    ( implies ( and x44 ( and x43 true ) ) ( = tmp70 48 ) )
    ( implies ( and ( not x14 ) ( and ( not x15 ) true ) ) ( = tmp69 0 ) )
    ( implies ( and ( not x14 ) ( and x15 true ) ) ( = tmp69 8 ) )
    ( implies ( and x14 ( and ( not x15 ) true ) ) ( = tmp69 23 ) )
    ( implies ( and x14 ( and x15 true ) ) ( = tmp69 31 ) )
    ( implies ( and ( not x46 ) ( and ( not x45 ) true ) ) ( = tmp68 0 ) )
    ( implies ( and ( not x46 ) ( and x45 true ) ) ( = tmp68 42 ) )
    ( implies ( and x46 ( and ( not x45 ) true ) ) ( = tmp68 47 ) )
    ( implies ( and x46 ( and x45 true ) ) ( = tmp68 89 ) )
    ( implies ( and ( not x12 ) ( and ( not x13 ) true ) ) ( = tmp67 0 ) )
    ( implies ( and ( not x12 ) ( and x13 true ) ) ( = tmp67 18 ) )
    ( implies ( and x12 ( and ( not x13 ) true ) ) ( = tmp67 30 ) )
    ( implies ( and x12 ( and x13 true ) ) ( = tmp67 48 ) )
    ( implies ( and ( not x48 ) ( and ( not x47 ) true ) ) ( = tmp66 0 ) )
    ( implies ( and ( not x48 ) ( and x47 true ) ) ( = tmp66 55 ) )
    ( implies ( and x48 ( and ( not x47 ) true ) ) ( = tmp66 32 ) )
    ( implies ( and x48 ( and x47 true ) ) ( = tmp66 87 ) )
    ( implies ( and ( not x10 ) ( and ( not x11 ) true ) ) ( = tmp65 0 ) )
    ( implies ( and ( not x10 ) ( and x11 true ) ) ( = tmp65 12 ) )
    ( implies ( and x10 ( and ( not x11 ) true ) ) ( = tmp65 26 ) )
    ( implies ( and x10 ( and x11 true ) ) ( = tmp65 38 ) )
    ( implies ( and ( not x50 ) ( and ( not x49 ) true ) ) ( = tmp64 0 ) )
    ( implies ( and ( not x50 ) ( and x49 true ) ) ( = tmp64 47 ) )
    ( implies ( and x50 ( and ( not x49 ) true ) ) ( = tmp64 9 ) )
    ( implies ( and x50 ( and x49 true ) ) ( = tmp64 56 ) )
    ( implies ( and ( not x8 ) ( and ( not x9 ) true ) ) ( = tmp63 0 ) )
    ( implies ( and ( not x8 ) ( and x9 true ) ) ( = tmp63 11 ) )
    ( implies ( and x8 ( and ( not x9 ) true ) ) ( = tmp63 38 ) )
    ( implies ( and x8 ( and x9 true ) ) ( = tmp63 49 ) )
    ( implies ( and ( not x52 ) ( and ( not x51 ) true ) ) ( = tmp62 0 ) )
    ( implies ( and ( not x52 ) ( and x51 true ) ) ( = tmp62 26 ) )
    ( implies ( and x52 ( and ( not x51 ) true ) ) ( = tmp62 43 ) )
    ( implies ( and x52 ( and x51 true ) ) ( = tmp62 69 ) )
    ( implies ( and ( not x6 ) ( and ( not x7 ) true ) ) ( = tmp61 0 ) )
    ( implies ( and ( not x6 ) ( and x7 true ) ) ( = tmp61 21 ) )
    ( implies ( and x6 ( and ( not x7 ) true ) ) ( = tmp61 49 ) )
    ( implies ( and x6 ( and x7 true ) ) ( = tmp61 70 ) )
    ( implies ( and ( not x54 ) ( and ( not x53 ) true ) ) ( = tmp60 0 ) )
    ( implies ( and ( not x54 ) ( and x53 true ) ) ( = tmp60 50 ) )
    ( implies ( and x54 ( and ( not x53 ) true ) ) ( = tmp60 13 ) )
    ( implies ( and x54 ( and x53 true ) ) ( = tmp60 63 ) )
    ( implies ( and ( not x4 ) ( and ( not x5 ) true ) ) ( = tmp59 0 ) )
    ( implies ( and ( not x4 ) ( and x5 true ) ) ( = tmp59 5 ) )
    ( implies ( and x4 ( and ( not x5 ) true ) ) ( = tmp59 8 ) )
    ( implies ( and x4 ( and x5 true ) ) ( = tmp59 13 ) )
    ( implies ( and ( not x56 ) ( and ( not x55 ) true ) ) ( = tmp58 0 ) )
    ( implies ( and ( not x56 ) ( and x55 true ) ) ( = tmp58 30 ) )
    ( implies ( and x56 ( and ( not x55 ) true ) ) ( = tmp58 14 ) )
    ( implies ( and x56 ( and x55 true ) ) ( = tmp58 44 ) )
    ( implies ( and ( not x2 ) ( and ( not x3 ) true ) ) ( = tmp57 0 ) )
    ( implies ( and ( not x2 ) ( and x3 true ) ) ( = tmp57 34 ) )
    ( implies ( and x2 ( and ( not x3 ) true ) ) ( = tmp57 48 ) )
    ( implies ( and x2 ( and x3 true ) ) ( = tmp57 82 ) )
    ( implies ( and ( not x30 ) true ) ( = tmp56 0 ) )
    ( implies ( and x30 true ) ( = tmp56 19 ) )
    ( implies ( and ( not x28 ) ( and ( not x29 ) true ) ) ( = tmp55 0 ) )
    ( implies ( and ( not x28 ) ( and x29 true ) ) ( = tmp55 12 ) )
    ( implies ( and x28 ( and ( not x29 ) true ) ) ( = tmp55 12 ) )
    ( implies ( and x28 ( and x29 true ) ) ( = tmp55 24 ) )
    ( implies ( and ( not x32 ) ( and ( not x31 ) true ) ) ( = tmp54 0 ) )
    ( implies ( and ( not x32 ) ( and x31 true ) ) ( = tmp54 17 ) )
    ( implies ( and x32 ( and ( not x31 ) true ) ) ( = tmp54 38 ) )
    ( implies ( and x32 ( and x31 true ) ) ( = tmp54 55 ) )
    ( implies ( and ( not x26 ) ( and ( not x27 ) true ) ) ( = tmp53 0 ) )
    ( implies ( and ( not x26 ) ( and x27 true ) ) ( = tmp53 22 ) )
    ( implies ( and x26 ( and ( not x27 ) true ) ) ( = tmp53 15 ) )
    ( implies ( and x26 ( and x27 true ) ) ( = tmp53 37 ) )
    ( implies ( and ( not x34 ) ( and ( not x33 ) true ) ) ( = tmp52 0 ) )
    ( implies ( and ( not x34 ) ( and x33 true ) ) ( = tmp52 17 ) )
    ( implies ( and x34 ( and ( not x33 ) true ) ) ( = tmp52 9 ) )
    ( implies ( and x34 ( and x33 true ) ) ( = tmp52 26 ) )
    ( implies ( and ( not x24 ) ( and ( not x25 ) true ) ) ( = tmp51 0 ) )
    ( implies ( and ( not x24 ) ( and x25 true ) ) ( = tmp51 21 ) )
    ( implies ( and x24 ( and ( not x25 ) true ) ) ( = tmp51 9 ) )
    ( implies ( and x24 ( and x25 true ) ) ( = tmp51 30 ) )
    ( implies ( and ( not x36 ) ( and ( not x35 ) true ) ) ( = tmp50 0 ) )
    ( implies ( and ( not x36 ) ( and x35 true ) ) ( = tmp50 30 ) )
    ( implies ( and x36 ( and ( not x35 ) true ) ) ( = tmp50 24 ) )
    ( implies ( and x36 ( and x35 true ) ) ( = tmp50 54 ) )
    ( implies ( and ( not x22 ) ( and ( not x23 ) true ) ) ( = tmp49 0 ) )
    ( implies ( and ( not x22 ) ( and x23 true ) ) ( = tmp49 21 ) )
    ( implies ( and x22 ( and ( not x23 ) true ) ) ( = tmp49 52 ) )
    ( implies ( and x22 ( and x23 true ) ) ( = tmp49 73 ) )
    ( implies ( and ( not x38 ) ( and ( not x37 ) true ) ) ( = tmp48 0 ) )
    ( implies ( and ( not x38 ) ( and x37 true ) ) ( = tmp48 48 ) )
    ( implies ( and x38 ( and ( not x37 ) true ) ) ( = tmp48 16 ) )
    ( implies ( and x38 ( and x37 true ) ) ( = tmp48 64 ) )
    ( implies ( and ( not x20 ) ( and ( not x21 ) true ) ) ( = tmp47 0 ) )
    ( implies ( and ( not x20 ) ( and x21 true ) ) ( = tmp47 38 ) )
    ( implies ( and x20 ( and ( not x21 ) true ) ) ( = tmp47 30 ) )
    ( implies ( and x20 ( and x21 true ) ) ( = tmp47 68 ) )
    ( implies ( and ( not x40 ) ( and ( not x39 ) true ) ) ( = tmp46 0 ) )
    ( implies ( and ( not x40 ) ( and x39 true ) ) ( = tmp46 34 ) )
    ( implies ( and x40 ( and ( not x39 ) true ) ) ( = tmp46 41 ) )
    ( implies ( and x40 ( and x39 true ) ) ( = tmp46 75 ) )
    ( implies ( and ( not x18 ) ( and ( not x19 ) true ) ) ( = tmp45 0 ) )
    ( implies ( and ( not x18 ) ( and x19 true ) ) ( = tmp45 46 ) )
    ( implies ( and x18 ( and ( not x19 ) true ) ) ( = tmp45 45 ) )
    ( implies ( and x18 ( and x19 true ) ) ( = tmp45 91 ) )
    ( implies ( and ( not x42 ) ( and ( not x41 ) true ) ) ( = tmp44 0 ) )
    ( implies ( and ( not x42 ) ( and x41 true ) ) ( = tmp44 28 ) )
    ( implies ( and x42 ( and ( not x41 ) true ) ) ( = tmp44 52 ) )
    ( implies ( and x42 ( and x41 true ) ) ( = tmp44 80 ) )
    ( implies ( and ( not x16 ) ( and ( not x17 ) true ) ) ( = tmp43 0 ) )
    ( implies ( and ( not x16 ) ( and x17 true ) ) ( = tmp43 51 ) )
    ( implies ( and x16 ( and ( not x17 ) true ) ) ( = tmp43 45 ) )
    ( implies ( and x16 ( and x17 true ) ) ( = tmp43 96 ) )
    ( implies ( and ( not x44 ) ( and ( not x43 ) true ) ) ( = tmp42 0 ) )
    ( implies ( and ( not x44 ) ( and x43 true ) ) ( = tmp42 10 ) )
    ( implies ( and x44 ( and ( not x43 ) true ) ) ( = tmp42 8 ) )
    ( implies ( and x44 ( and x43 true ) ) ( = tmp42 18 ) )
    ( implies ( and ( not x14 ) ( and ( not x15 ) true ) ) ( = tmp41 0 ) )
    ( implies ( and ( not x14 ) ( and x15 true ) ) ( = tmp41 34 ) )
    ( implies ( and x14 ( and ( not x15 ) true ) ) ( = tmp41 54 ) )
    ( implies ( and x14 ( and x15 true ) ) ( = tmp41 88 ) )
    ( implies ( and ( not x46 ) ( and ( not x45 ) true ) ) ( = tmp40 0 ) )
    ( implies ( and ( not x46 ) ( and x45 true ) ) ( = tmp40 51 ) )
    ( implies ( and x46 ( and ( not x45 ) true ) ) ( = tmp40 40 ) )
    ( implies ( and x46 ( and x45 true ) ) ( = tmp40 91 ) )
    ( implies ( and ( not x12 ) ( and ( not x13 ) true ) ) ( = tmp39 0 ) )
    ( implies ( and ( not x12 ) ( and x13 true ) ) ( = tmp39 36 ) )
    ( implies ( and x12 ( and ( not x13 ) true ) ) ( = tmp39 25 ) )
    ( implies ( and x12 ( and x13 true ) ) ( = tmp39 61 ) )
    ( implies ( and ( not x48 ) ( and ( not x47 ) true ) ) ( = tmp38 0 ) )
    ( implies ( and ( not x48 ) ( and x47 true ) ) ( = tmp38 48 ) )
    ( implies ( and x48 ( and ( not x47 ) true ) ) ( = tmp38 46 ) )
    ( implies ( and x48 ( and x47 true ) ) ( = tmp38 94 ) )
    ( implies ( and ( not x10 ) ( and ( not x11 ) true ) ) ( = tmp37 0 ) )
    ( implies ( and ( not x10 ) ( and x11 true ) ) ( = tmp37 23 ) )
    ( implies ( and x10 ( and ( not x11 ) true ) ) ( = tmp37 16 ) )
    ( implies ( and x10 ( and x11 true ) ) ( = tmp37 39 ) )
    ( implies ( and ( not x50 ) ( and ( not x49 ) true ) ) ( = tmp36 0 ) )
    ( implies ( and ( not x50 ) ( and x49 true ) ) ( = tmp36 30 ) )
    ( implies ( and x50 ( and ( not x49 ) true ) ) ( = tmp36 38 ) )
    ( implies ( and x50 ( and x49 true ) ) ( = tmp36 68 ) )
    ( implies ( and ( not x8 ) ( and ( not x9 ) true ) ) ( = tmp35 0 ) )
    ( implies ( and ( not x8 ) ( and x9 true ) ) ( = tmp35 48 ) )
    ( implies ( and x8 ( and ( not x9 ) true ) ) ( = tmp35 14 ) )
    ( implies ( and x8 ( and x9 true ) ) ( = tmp35 62 ) )
    ( implies ( and ( not x52 ) ( and ( not x51 ) true ) ) ( = tmp34 0 ) )
    ( implies ( and ( not x52 ) ( and x51 true ) ) ( = tmp34 21 ) )
    ( implies ( and x52 ( and ( not x51 ) true ) ) ( = tmp34 12 ) )
    ( implies ( and x52 ( and x51 true ) ) ( = tmp34 33 ) )
    ( implies ( and ( not x6 ) ( and ( not x7 ) true ) ) ( = tmp33 0 ) )
    ( implies ( and ( not x6 ) ( and x7 true ) ) ( = tmp33 42 ) )
    ( implies ( and x6 ( and ( not x7 ) true ) ) ( = tmp33 43 ) )
    ( implies ( and x6 ( and x7 true ) ) ( = tmp33 85 ) )
    ( implies ( and ( not x54 ) ( and ( not x53 ) true ) ) ( = tmp32 0 ) )
    ( implies ( and ( not x54 ) ( and x53 true ) ) ( = tmp32 35 ) )
    ( implies ( and x54 ( and ( not x53 ) true ) ) ( = tmp32 38 ) )
    ( implies ( and x54 ( and x53 true ) ) ( = tmp32 73 ) )
    ( implies ( and ( not x4 ) ( and ( not x5 ) true ) ) ( = tmp31 0 ) )
    ( implies ( and ( not x4 ) ( and x5 true ) ) ( = tmp31 12 ) )
    ( implies ( and x4 ( and ( not x5 ) true ) ) ( = tmp31 48 ) )
    ( implies ( and x4 ( and x5 true ) ) ( = tmp31 60 ) )
    ( implies ( and ( not x56 ) ( and ( not x55 ) true ) ) ( = tmp30 0 ) )
    ( implies ( and ( not x56 ) ( and x55 true ) ) ( = tmp30 17 ) )
    ( implies ( and x56 ( and ( not x55 ) true ) ) ( = tmp30 52 ) )
    ( implies ( and x56 ( and x55 true ) ) ( = tmp30 69 ) )
    ( implies ( and ( not x2 ) ( and ( not x3 ) true ) ) ( = tmp29 0 ) )
    ( implies ( and ( not x2 ) ( and x3 true ) ) ( = tmp29 48 ) )
    ( implies ( and x2 ( and ( not x3 ) true ) ) ( = tmp29 53 ) )
    ( implies ( and x2 ( and x3 true ) ) ( = tmp29 101 ) )
    ( implies ( and ( not x30 ) true ) ( = tmp28 0 ) )
    ( implies ( and x30 true ) ( = tmp28 51 ) )
    ( implies ( and ( not x28 ) ( and ( not x29 ) true ) ) ( = tmp27 0 ) )
    ( implies ( and ( not x28 ) ( and x29 true ) ) ( = tmp27 14 ) )
    ( implies ( and x28 ( and ( not x29 ) true ) ) ( = tmp27 22 ) )
    ( implies ( and x28 ( and x29 true ) ) ( = tmp27 36 ) )
    ( implies ( and ( not x32 ) ( and ( not x31 ) true ) ) ( = tmp26 0 ) )
    ( implies ( and ( not x32 ) ( and x31 true ) ) ( = tmp26 49 ) )
    ( implies ( and x32 ( and ( not x31 ) true ) ) ( = tmp26 7 ) )
    ( implies ( and x32 ( and x31 true ) ) ( = tmp26 56 ) )
    ( implies ( and ( not x26 ) ( and ( not x27 ) true ) ) ( = tmp25 0 ) )
    ( implies ( and ( not x26 ) ( and x27 true ) ) ( = tmp25 42 ) )
    ( implies ( and x26 ( and ( not x27 ) true ) ) ( = tmp25 5 ) )
    ( implies ( and x26 ( and x27 true ) ) ( = tmp25 47 ) )
    ( implies ( and ( not x34 ) ( and ( not x33 ) true ) ) ( = tmp24 0 ) )
    ( implies ( and ( not x34 ) ( and x33 true ) ) ( = tmp24 10 ) )
    ( implies ( and x34 ( and ( not x33 ) true ) ) ( = tmp24 30 ) )
    ( implies ( and x34 ( and x33 true ) ) ( = tmp24 40 ) )
    ( implies ( and ( not x24 ) ( and ( not x25 ) true ) ) ( = tmp23 0 ) )
    ( implies ( and ( not x24 ) ( and x25 true ) ) ( = tmp23 33 ) )
    ( implies ( and x24 ( and ( not x25 ) true ) ) ( = tmp23 19 ) )
    ( implies ( and x24 ( and x25 true ) ) ( = tmp23 52 ) )
    ( implies ( and ( not x36 ) ( and ( not x35 ) true ) ) ( = tmp22 0 ) )
    ( implies ( and ( not x36 ) ( and x35 true ) ) ( = tmp22 14 ) )
    ( implies ( and x36 ( and ( not x35 ) true ) ) ( = tmp22 32 ) )
    ( implies ( and x36 ( and x35 true ) ) ( = tmp22 46 ) )
    ( implies ( and ( not x22 ) ( and ( not x23 ) true ) ) ( = tmp21 0 ) )
    ( implies ( and ( not x22 ) ( and x23 true ) ) ( = tmp21 40 ) )
    ( implies ( and x22 ( and ( not x23 ) true ) ) ( = tmp21 8 ) )
    ( implies ( and x22 ( and x23 true ) ) ( = tmp21 48 ) )
    ( implies ( and ( not x38 ) ( and ( not x37 ) true ) ) ( = tmp20 0 ) )
    ( implies ( and ( not x38 ) ( and x37 true ) ) ( = tmp20 24 ) )
    ( implies ( and x38 ( and ( not x37 ) true ) ) ( = tmp20 36 ) )
    ( implies ( and x38 ( and x37 true ) ) ( = tmp20 60 ) )
    ( implies ( and ( not x20 ) ( and ( not x21 ) true ) ) ( = tmp19 0 ) )
    ( implies ( and ( not x20 ) ( and x21 true ) ) ( = tmp19 26 ) )
    ( implies ( and x20 ( and ( not x21 ) true ) ) ( = tmp19 46 ) )
    ( implies ( and x20 ( and x21 true ) ) ( = tmp19 72 ) )
    ( implies ( and ( not x40 ) ( and ( not x39 ) true ) ) ( = tmp18 0 ) )
    ( implies ( and ( not x40 ) ( and x39 true ) ) ( = tmp18 14 ) )
    ( implies ( and x40 ( and ( not x39 ) true ) ) ( = tmp18 13 ) )
    ( implies ( and x40 ( and x39 true ) ) ( = tmp18 27 ) )
    ( implies ( and ( not x18 ) ( and ( not x19 ) true ) ) ( = tmp17 0 ) )
    ( implies ( and ( not x18 ) ( and x19 true ) ) ( = tmp17 7 ) )
    ( implies ( and x18 ( and ( not x19 ) true ) ) ( = tmp17 17 ) )
    ( implies ( and x18 ( and x19 true ) ) ( = tmp17 24 ) )
    ( implies ( and ( not x42 ) ( and ( not x41 ) true ) ) ( = tmp16 0 ) )
    ( implies ( and ( not x42 ) ( and x41 true ) ) ( = tmp16 52 ) )
    ( implies ( and x42 ( and ( not x41 ) true ) ) ( = tmp16 16 ) )
    ( implies ( and x42 ( and x41 true ) ) ( = tmp16 68 ) )
    ( implies ( and ( not x16 ) ( and ( not x17 ) true ) ) ( = tmp15 0 ) )
    ( implies ( and ( not x16 ) ( and x17 true ) ) ( = tmp15 35 ) )
    ( implies ( and x16 ( and ( not x17 ) true ) ) ( = tmp15 16 ) )
    ( implies ( and x16 ( and x17 true ) ) ( = tmp15 51 ) )
    ( implies ( and ( not x44 ) ( and ( not x43 ) true ) ) ( = tmp14 0 ) )
    ( implies ( and ( not x44 ) ( and x43 true ) ) ( = tmp14 5 ) )
    ( implies ( and x44 ( and ( not x43 ) true ) ) ( = tmp14 35 ) )
    ( implies ( and x44 ( and x43 true ) ) ( = tmp14 40 ) )
    ( implies ( and ( not x14 ) ( and ( not x15 ) true ) ) ( = tmp13 0 ) )
    ( implies ( and ( not x14 ) ( and x15 true ) ) ( = tmp13 10 ) )
    ( implies ( and x14 ( and ( not x15 ) true ) ) ( = tmp13 37 ) )
    ( implies ( and x14 ( and x15 true ) ) ( = tmp13 47 ) )
    ( implies ( and ( not x46 ) ( and ( not x45 ) true ) ) ( = tmp12 0 ) )
    ( implies ( and ( not x46 ) ( and x45 true ) ) ( = tmp12 48 ) )
    ( implies ( and x46 ( and ( not x45 ) true ) ) ( = tmp12 11 ) )
    ( implies ( and x46 ( and x45 true ) ) ( = tmp12 59 ) )
    ( implies ( and ( not x12 ) ( and ( not x13 ) true ) ) ( = tmp11 0 ) )
    ( implies ( and ( not x12 ) ( and x13 true ) ) ( = tmp11 38 ) )
    ( implies ( and x12 ( and ( not x13 ) true ) ) ( = tmp11 48 ) )
    ( implies ( and x12 ( and x13 true ) ) ( = tmp11 86 ) )
    ( implies ( and ( not x48 ) ( and ( not x47 ) true ) ) ( = tmp10 0 ) )
    ( implies ( and ( not x48 ) ( and x47 true ) ) ( = tmp10 47 ) )
    ( implies ( and x48 ( and ( not x47 ) true ) ) ( = tmp10 27 ) )
    ( implies ( and x48 ( and x47 true ) ) ( = tmp10 74 ) )
    ( implies ( and ( not x10 ) ( and ( not x11 ) true ) ) ( = tmp9 0 ) )
    ( implies ( and ( not x10 ) ( and x11 true ) ) ( = tmp9 6 ) )
    ( implies ( and x10 ( and ( not x11 ) true ) ) ( = tmp9 21 ) )
    ( implies ( and x10 ( and x11 true ) ) ( = tmp9 27 ) )
    ( implies ( and ( not x50 ) ( and ( not x49 ) true ) ) ( = tmp8 0 ) )
    ( implies ( and ( not x50 ) ( and x49 true ) ) ( = tmp8 24 ) )
    ( implies ( and x50 ( and ( not x49 ) true ) ) ( = tmp8 49 ) )
    ( implies ( and x50 ( and x49 true ) ) ( = tmp8 73 ) )
    ( implies ( and ( not x8 ) ( and ( not x9 ) true ) ) ( = tmp7 0 ) )
    ( implies ( and ( not x8 ) ( and x9 true ) ) ( = tmp7 45 ) )
    ( implies ( and x8 ( and ( not x9 ) true ) ) ( = tmp7 37 ) )
    ( implies ( and x8 ( and x9 true ) ) ( = tmp7 82 ) )
    ( implies ( and ( not x52 ) ( and ( not x51 ) true ) ) ( = tmp6 0 ) )
    ( implies ( and ( not x52 ) ( and x51 true ) ) ( = tmp6 17 ) )
    ( implies ( and x52 ( and ( not x51 ) true ) ) ( = tmp6 46 ) )
    ( implies ( and x52 ( and x51 true ) ) ( = tmp6 63 ) )
    ( implies ( and ( not x6 ) ( and ( not x7 ) true ) ) ( = tmp5 0 ) )
    ( implies ( and ( not x6 ) ( and x7 true ) ) ( = tmp5 26 ) )
    ( implies ( and x6 ( and ( not x7 ) true ) ) ( = tmp5 49 ) )
    ( implies ( and x6 ( and x7 true ) ) ( = tmp5 75 ) )
    ( implies ( and ( not x54 ) ( and ( not x53 ) true ) ) ( = tmp4 0 ) )
    ( implies ( and ( not x54 ) ( and x53 true ) ) ( = tmp4 53 ) )
    ( implies ( and x54 ( and ( not x53 ) true ) ) ( = tmp4 53 ) )
    ( implies ( and x54 ( and x53 true ) ) ( = tmp4 106 ) )
    ( implies ( and ( not x4 ) ( and ( not x5 ) true ) ) ( = tmp3 0 ) )
    ( implies ( and ( not x4 ) ( and x5 true ) ) ( = tmp3 27 ) )
    ( implies ( and x4 ( and ( not x5 ) true ) ) ( = tmp3 11 ) )
    ( implies ( and x4 ( and x5 true ) ) ( = tmp3 38 ) )
    ( implies ( and ( not x56 ) ( and ( not x55 ) true ) ) ( = tmp2 0 ) )
    ( implies ( and ( not x56 ) ( and x55 true ) ) ( = tmp2 10 ) )
    ( implies ( and x56 ( and ( not x55 ) true ) ) ( = tmp2 30 ) )
    ( implies ( and x56 ( and x55 true ) ) ( = tmp2 40 ) )
    ( implies ( and ( not x2 ) ( and ( not x3 ) true ) ) ( = tmp1 0 ) )
    ( implies ( and ( not x2 ) ( and x3 true ) ) ( = tmp1 36 ) )
    ( implies ( and x2 ( and ( not x3 ) true ) ) ( = tmp1 14 ) )
    ( implies ( and x2 ( and x3 true ) ) ( = tmp1 50 ) )
  )
)