(set-info :source |
   Extracted from SMT-LIB/incremental/uf/20190926-CLEARSY/0012/00092.smt2.
   This is the 30th check.
   This is a scrambled benchmark, which is kind of important as the same
   exists term is differently represented in the two formulas.  This checks
   if the term axioms for quantified formulas appearing as uf arguments is
   correctly handled|)
(set-option :produce-proofs true)
(set-logic UF)
(declare-sort x467 0)
(declare-fun x253 (x467 x467) x467)
(declare-fun x38 (x467 x467) Bool)
(declare-fun x429 () x467)
(declare-fun x19 () x467)
(declare-fun x246 (x467 x467) Bool)
(declare-fun x504 (x467 x467) Bool)
(declare-fun x358 (x467 x467) x467)
(declare-fun x443 (x467 x467) Bool)
(declare-fun x6 (x467 x467) Bool)
(declare-fun x531 (x467) x467)
(declare-fun x161 (x467 x467) x467)
(declare-fun x525 (x467 x467) Bool)
(declare-fun x350 (x467 x467) x467)
(declare-fun x251 (x467 x467) x467)
(declare-fun x256 (x467) x467)
(declare-fun x259 (x467 x467) x467)
(declare-fun x219 (x467 x467) x467)
(declare-fun x530 (x467 x467) Bool)
(declare-fun x437 (x467 x467) x467)
(declare-fun x447 (x467 x467) x467)
(declare-fun x339 (x467 x467) Bool)
(assert (not (= x19 x429)))
(declare-fun x29 () x467)
(declare-fun x306 () x467)
(declare-fun x400 (x467 x467) x467)
(declare-fun x212 () x467)
(declare-fun x329 () x467)
(declare-fun x479 () x467)
(declare-fun x546 (x467 x467) x467)
(declare-fun x10 () x467)
(declare-fun x376 () x467)
(declare-fun x25 (x467) x467)
(declare-fun x325 () x467)
(declare-fun x133 () x467)
(declare-fun x129 (x467) x467)
(declare-fun x106 () x467)
(declare-fun x439 () x467)
(declare-fun x203 (x467 x467) x467)
(declare-fun x486 () x467)
(declare-fun x311 () x467)
(declare-fun x286 () x467)
(declare-fun x299 () x467)
(declare-fun x86 () x467)
(declare-fun x272 () x467)
(declare-fun x69 () x467)
(declare-fun x150 () x467)
(declare-fun x465 (x467 x467) Bool)
(declare-fun x77 () x467)
(declare-fun x295 () x467)
(declare-fun x477 () x467)
(declare-fun x260 () x467)
(declare-fun x88 (x467) x467)
(declare-fun x323 () x467)
(declare-fun x484 (x467) x467)
(declare-fun x305 () x467)
(declare-fun x533 () x467)
(declare-fun x392 () x467)
(declare-fun x341 () x467)
(declare-fun x3 () x467)
(declare-fun x210 () x467)
(declare-fun x332 () x467)
(declare-fun x448 () x467)
(declare-fun x456 () x467)
(declare-fun x527 () x467)
(declare-fun x139 (x467) x467)
(declare-fun x63 (x467 x467) x467)
(declare-fun x234 () x467)
(declare-fun x23 () x467)
(declare-fun x285 () x467)
(declare-fun x213 () x467)
(declare-fun x501 (x467 x467) x467)
(declare-fun x73 () x467)
(declare-fun x364 () x467)
(declare-fun x349 () x467)
(declare-fun x391 () x467)
(declare-fun x290 () x467)
(declare-fun x498 (x467) x467)
(declare-fun x436 () x467)
(declare-fun x79 () x467)
(declare-fun x62 () x467)
(declare-fun x192 () x467)
(declare-fun x47 () x467)
(declare-fun x43 () x467)
(declare-fun x50 () x467)
(declare-fun x197 () x467)
(declare-fun x304 () x467)
(declare-fun x264 () x467)
(declare-fun x368 () x467)
(declare-fun x428 () x467)
(declare-fun x503 () x467)
(declare-fun x432 () x467)
(declare-fun x402 () x467)
(declare-fun x100 (x467 x467) x467)
(declare-fun x221 () x467)
(declare-fun x242 () x467)
(declare-fun x493 (x467) x467)
(declare-fun x328 () x467)
(declare-fun x536 () x467)
(declare-fun x28 () x467)
(declare-fun x241 () x467)
(declare-fun x146 () x467)
(declare-fun x104 (x467) x467)
(declare-fun x511 () x467)
(declare-fun x171 () x467)
(declare-fun x413 () x467)
(declare-fun x420 () x467)
(declare-fun x216 () x467)
(declare-fun x136 () x467)
(declare-fun x414 () x467)
(declare-fun x268 () x467)
(declare-fun x15 () x467)
(declare-fun x506 () x467)
(declare-fun x380 () x467)
(declare-fun x220 () x467)
(declare-fun x226 (x467 x467) x467)
(declare-fun x384 () x467)
(declare-fun x316 (x467 x467) x467)
(declare-fun x485 () x467)
(declare-fun x274 (x467 x467) x467)
(declare-fun x499 () x467)
(declare-fun x487 () x467)
(declare-fun x76 () x467)
(declare-fun x245 (x467) x467)
(declare-fun x33 () x467)
(declare-fun x172 () x467)
(declare-fun x532 () x467)
(declare-fun x497 (x467) x467)
(declare-fun x40 () x467)
(declare-fun x101 (Bool) x467)
(declare-fun x421 () x467)
(declare-fun x107 () x467)
(declare-fun x158 (x467 x467) x467)
(declare-fun x87 () x467)
(declare-fun x509 () x467)
(declare-fun x99 () x467)
(declare-fun x51 () x467)
(declare-fun x239 () x467)
(declare-fun x236 () x467)
(declare-fun x444 () x467)
(declare-fun x362 () x467)
(declare-fun x71 () x467)
(declare-fun x336 () x467)
(declare-fun x195 () x467)
(declare-fun x80 (x467) x467)
(declare-fun x283 () x467)
(declare-fun x24 () x467)
(declare-fun x130 () x467)
(declare-fun x204 () x467)
(declare-fun x249 () x467)
(declare-fun x132 (x467 x467) x467)
(declare-fun x13 () x467)
(declare-fun x185 () x467)
(declare-fun x108 () x467)
(declare-fun x505 () x467)
(declare-fun x114 () x467)
(declare-fun x258 () x467)
(declare-fun x483 () x467)
(declare-fun x60 () x467)
(declare-fun x93 () x467)
(declare-fun x116 () x467)
(declare-fun x492 (x467) x467)
(declare-fun x453 () x467)
(declare-fun x360 () x467)
(declare-fun x375 () x467)
(declare-fun x542 (x467 x467) x467)
(declare-fun x379 () x467)
(declare-fun x214 () x467)
(declare-fun x153 (x467) x467)
(declare-fun x32 () x467)
(declare-fun x227 (x467) x467)
(declare-fun x544 (x467 x467 x467) x467)
(declare-fun x42 (x467) x467)
(declare-fun x194 () x467)
(declare-fun x519 (x467) x467)
(declare-fun x359 () x467)
(declare-fun x154 () x467)
(declare-fun x321 () x467)
(declare-fun x469 () x467)
(declare-fun x385 () x467)
(declare-fun x422 (x467 x467) x467)
(declare-fun x178 (x467 x467) x467)
(declare-fun x407 (x467 x467) Bool)
(declare-fun x273 () x467)
(declare-fun x302 () x467)
(declare-fun x317 () x467)
(declare-fun x182 () x467)
(declare-fun x162 () x467)
(declare-fun x331 () x467)
(declare-fun x404 () x467)
(declare-fun x361 () x467)
(declare-fun x292 () x467)
(declare-fun x122 () x467)
(declare-fun x449 () x467)
(declare-fun x412 () x467)
(declare-fun x287 () x467)
(declare-fun x435 (x467) x467)
(declare-fun x398 (x467 x467) x467)
(declare-fun x22 () x467)
(declare-fun x205 () x467)
(declare-fun x1 (x467) x467)
(declare-fun x537 () x467)
(declare-fun x120 (x467) x467)
(declare-fun x92 () x467)
(declare-fun x309 () x467)
(declare-fun x159 () x467)
(declare-fun x473 (x467 x467) Bool)
(declare-fun x72 (x467 x467) x467)
(declare-fun x27 () x467)
(declare-fun x367 () x467)
(declare-fun x348 () x467)
(declare-fun x389 (x467) x467)
(declare-fun x89 (x467 x467) x467)
(declare-fun x147 () x467)
(declare-fun x424 () x467)
(declare-fun x109 () x467)
(declare-fun x313 () x467)
(declare-fun x119 (x467 x467) x467)
(declare-fun x200 () x467)
(declare-fun x223 () x467)
(declare-fun x250 () x467)
(declare-fun x535 () x467)
(declare-fun x230 () x467)
(declare-fun x5 () x467)
(declare-fun x20 () x467)
(declare-fun x75 () x467)
(declare-fun x411 (x467 x467) x467)
(declare-fun x94 () x467)
(declare-fun x138 () x467)
(declare-fun x472 () x467)
(declare-fun x174 () x467)
(declare-fun x489 () x467)
(declare-fun x377 () x467)
(declare-fun x134 () x467)
(declare-fun x312 () x467)
(declare-fun x90 () x467)
(declare-fun x37 () x467)
(declare-fun x383 (x467 x467) x467)
(declare-fun x2 () x467)
(declare-fun x12 () x467)
(declare-fun x342 () x467)
(declare-fun x296 () x467)
(declare-fun x320 (x467 x467) x467)
(declare-fun x141 (x467) x467)
(declare-fun x495 () x467)
(declare-fun x517 () x467)
(declare-fun x164 () x467)
(declare-fun x454 () x467)
(declare-fun x65 () x467)
(declare-fun x127 () x467)
(declare-fun x175 () x467)
(declare-fun x58 () x467)
(declare-fun x156 () x467)
(declare-fun x198 () x467)
(declare-fun x244 (x467 x467) x467)
(declare-fun x397 () x467)
(declare-fun x373 (x467) x467)
(declare-fun x118 () x467)
(declare-fun x366 () x467)
(declare-fun x460 () x467)
(declare-fun x74 () x467)
(declare-fun x55 () x467)
(declare-fun x113 () x467)
(declare-fun x289 () x467)
(declare-fun x48 () x467)
(declare-fun x82 () x467)
(declare-fun x84 () x467)
(declare-fun x193 () x467)
(declare-fun x347 () x467)
(declare-fun x235 () x467)
(declare-fun x11 () x467)
(declare-fun x160 (x467) x467)
(declare-fun x381 (x467) x467)
(declare-fun x98 () x467)
(declare-fun x363 () x467)
(declare-fun x327 () x467)
(declare-fun x179 () x467)
(declare-fun x142 () x467)
(declare-fun x252 (x467) x467)
(declare-fun x209 () x467)
(declare-fun x322 (x467 x467) x467)
(declare-fun x494 () x467)
(declare-fun x395 (x467) x467)
(declare-fun x208 () x467)
(declare-fun x333 () x467)
(declare-fun x406 () x467)
(declare-fun x97 () x467)
(declare-fun x346 (x467 x467) x467)
(declare-fun x151 () x467)
(declare-fun x266 (x467) x467)
(declare-fun x56 () x467)
(declare-fun x173 () x467)
(declare-fun x522 () x467)
(declare-fun x340 () x467)
(declare-fun x265 () x467)
(declare-fun x35 (x467) x467)
(declare-fun x344 (x467) x467)
(declare-fun x26 () x467)
(declare-fun x330 () x467)
(declare-fun x187 () x467)
(declare-fun x382 () x467)
(declare-fun x463 () x467)
(declare-fun x232 () x467)
(declare-fun x526 () x467)
(declare-fun x262 () x467)
(declare-fun x44 () x467)
(declare-fun x540 (x467 x467) x467)
(declare-fun x225 () x467)
(declare-fun x502 () x467)
(declare-fun x165 () x467)
(declare-fun x457 () x467)
(declare-fun x181 () x467)
(declare-fun x427 () x467)
(declare-fun x83 () x467)
(declare-fun x280 () x467)
(declare-fun x102 (x467) x467)
(declare-fun x343 () x467)
(declare-fun x394 () x467)
(declare-fun x410 () x467)
(declare-fun x224 (x467) x467)
(declare-fun x310 () x467)
(declare-fun x279 () x467)
(declare-fun x417 () x467)
(declare-fun x231 () x467)
(declare-fun x163 () x467)
(declare-fun x190 () x467)
(declare-fun x461 () x467)
(declare-fun x496 (x467) x467)
(declare-fun x403 () x467)
(declare-fun x315 () x467)
(declare-fun x415 (x467) x467)
(declare-fun x353 () x467)
(declare-fun x68 (x467) x467)
(declare-fun x488 () x467)
(declare-fun x445 () x467)
(declare-fun x354 () x467)
(declare-fun x510 () x467)
(declare-fun x49 () x467)
(declare-fun x282 () x467)
(declare-fun x468 () x467)
(declare-fun x111 () x467)
(declare-fun x110 () x467)
(declare-fun x137 () x467)
(declare-fun x66 () x467)
(declare-fun x52 () x467)
(declare-fun x270 () x467)
(declare-fun x338 () x467)
(declare-fun x78 () x467)
(declare-fun x538 () x467)
(declare-fun x475 () x467)
(declare-fun x215 () x467)
(declare-fun x278 () x467)
(declare-fun x257 (x467) x467)
(declare-fun x440 (x467) x467)
(declare-fun x59 () x467)
(declare-fun x490 () x467)
(declare-fun x238 () x467)
(declare-fun x218 (x467) x467)
(declare-fun x115 () x467)
(declare-fun x371 () x467)
(declare-fun x508 () x467)
(declare-fun x418 () x467)
(declare-fun x166 () x467)
(declare-fun x351 (x467 x467) x467)
(declare-fun x211 () x467)
(declare-fun x288 () x467)
(declare-fun x229 () x467)
(declare-fun x294 (x467) x467)
(declare-fun x121 () x467)
(declare-fun x149 (x467 x467 x467) x467)
(declare-fun x433 () x467)
(declare-fun x46 (x467 x467) Bool)
(declare-fun x378 () x467)
(declare-fun x326 () x467)
(declare-fun x541 () x467)
(declare-fun x248 () x467)
(declare-fun x188 (x467 x467) x467)
(declare-fun x255 () x467)
(declare-fun x21 () x467)
(declare-fun x81 () x467)
(declare-fun x186 () x467)
(declare-fun x388 (x467 x467) x467)
(declare-fun x217 () x467)
(declare-fun x481 () x467)
(declare-fun x135 (x467) x467)
(declare-fun x374 (x467) x467)
(declare-fun x61 () x467)
(declare-fun x462 () x467)
(declare-fun x125 (x467) x467)
(declare-fun x277 () x467)
(declare-fun x105 () x467)
(declare-fun x291 () x467)
(declare-fun x145 () x467)
(declare-fun x518 (x467) x467)
(declare-fun x324 (x467) x467)
(declare-fun x4 () x467)
(declare-fun x124 () x467)
(declare-fun x112 (x467 x467) x467)
(declare-fun x169 () x467)
(declare-fun x152 () x467)
(declare-fun x390 (x467 x467) x467)
(declare-fun x482 (x467) x467)
(declare-fun x480 () x467)
(declare-fun x117 () x467)
(declare-fun x399 () x467)
(declare-fun x516 () x467)
(declare-fun x276 () x467)
(declare-fun x370 () x467)
(declare-fun x307 () x467)
(declare-fun x470 () x467)
(declare-fun x180 () x467)
(declare-fun x452 () x467)
(declare-fun x243 () x467)
(declare-fun x458 () x467)
(declare-fun x466 () x467)
(declare-fun x131 () x467)
(declare-fun x345 () x467)
(declare-fun x474 () x467)
(declare-fun x450 (x467) x467)
(declare-fun x41 () x467)
(declare-fun x386 () x467)
(declare-fun x441 (x467) x467)
(declare-fun x491 () x467)
(declare-fun x423 () x467)
(declare-fun x528 (x467 x467) x467)
(declare-fun x455 () x467)
(declare-fun x30 () x467)
(declare-fun x514 () x467)
(declare-fun x8 (x467 x467) x467)
(declare-fun x513 () x467)
(declare-fun x184 () x467)
(declare-fun x202 () x467)
(declare-fun x254 () x467)
(declare-fun x167 () x467)
(declare-fun x233 () x467)
(declare-fun x298 () x467)
(declare-fun x57 () x467)
(declare-fun x91 (x467 x467) Bool)
(declare-fun x126 () x467)
(declare-fun x267 () x467)
(declare-fun x356 () x467)
(declare-fun x318 () x467)
(declare-fun x271 () x467)
(declare-fun x9 (x467 x467) x467)
(declare-fun x314 () x467)
(declare-fun x95 () x467)
(declare-fun x261 () x467)
(declare-fun x155 () x467)
(declare-fun x334 () x467)
(declare-fun x36 () x467)
(declare-fun x191 (x467 x467) x467)
(declare-fun x337 () x467)
(declare-fun x319 () x467)
(declare-fun x67 () x467)
(declare-fun x387 () x467)
(declare-fun x471 (x467 x467) x467)
(declare-fun x144 () x467)
(declare-fun x529 () x467)
(declare-fun x301 () x467)
(declare-fun x206 () x467)
(declare-fun x45 () x467)
(declare-fun x18 () x467)
(declare-fun x431 (x467 x467) x467)
(declare-fun x539 (x467 x467) x467)
(declare-fun x176 () x467)
(declare-fun x85 (x467 x467) x467)
(declare-fun x300 () x467)
(declare-fun x54 () x467)
(declare-fun x199 () x467)
(declare-fun x401 () x467)
(declare-fun x64 () x467)
(declare-fun x396 (x467) x467)
(declare-fun x34 (x467 x467) x467)
(declare-fun x303 () x467)
(declare-fun x515 () x467)
(declare-fun x96 () x467)
(declare-fun x103 () x467)
(declare-fun x357 () x467)
(declare-fun x459 () x467)
(declare-fun x17 () x467)
(declare-fun x157 (x467 x467) x467)
(declare-fun x405 () x467)
(declare-fun x408 () x467)
(declare-fun x512 () x467)
(declare-fun x425 () x467)
(declare-fun x128 () x467)
(declare-fun x222 () x467)
(declare-fun x335 () x467)
(declare-fun x409 () x467)
(declare-fun x70 (x467) x467)
(declare-fun x189 (x467 x467) Bool)
(declare-fun x207 () x467)
(declare-fun x228 () x467)
(declare-fun x500 () x467)
(declare-fun x523 (x467 x467) x467)
(declare-fun x237 () x467)
(declare-fun x478 () x467)
(declare-fun x416 () x467)
(declare-fun x426 () x467)
(declare-fun x451 () x467)
(declare-fun x53 () x467)
(declare-fun x123 () x467)
(declare-fun x148 () x467)
(declare-fun x369 (x467) x467)
(declare-fun x201 () x467)
(declare-fun x434 () x467)
(declare-fun x476 () x467)
(declare-fun x355 () x467)
(declare-fun x170 () x467)
(declare-fun x240 (x467 x467) x467)
(declare-fun x545 (x467) x467)
(declare-fun x275 () x467)
(declare-fun x140 (x467 x467) x467)
(declare-fun x393 () x467)
(declare-fun x521 () x467)
(declare-fun x183 () x467)
(declare-fun x520 () x467)
(declare-fun x507 (x467 x467) x467)
(declare-fun x372 () x467)
(declare-fun x284 () x467)
(declare-fun x365 () x467)
(declare-fun x143 () x467)
(declare-fun x419 () x467)
(declare-fun x297 () x467)
(declare-fun x534 (x467 x467) Bool)
(declare-fun x543 (x467 x467) x467)
(declare-fun x430 (x467) x467)
(declare-fun x7 () x467)
(declare-fun x438 () x467)
(declare-fun x31 () x467)
(declare-fun x281 () x467)
(declare-fun x464 () x467)
(declare-fun x168 () x467)
(declare-fun x308 () x467)
(declare-fun x247 () x467)
(define-fun x524 () Bool (and (= x527 (x400 x456 x297)) (= x137 (x400 x43 x297))))
(define-fun x446 () Bool (and (x407 x67 x363) (= x115 (x447 x114 x343)) (x407 x279 x363) (x407 x265 x363) (x407 x83 x207) (x407 x130 x207) (= (x492 (x9 x151 x156)) x404) (x407 x499 x363) (x407 x521 x419) (= x236 (x112 x268 (x178 x84 (x492 x288)))) (x407 x448 x363) (x407 x4 x363) (= (x447 x318 x97) x526) (x407 x64 x363) (x407 x206 x363) (x407 x334 x363) (x407 x312 x207) (= x367 (x259 x210 x444)) (x407 x434 x282) (= x511 (x492 (x9 (x9 x19 x168) (x9 x429 x399)))) (x407 x413 x363) (x407 x478 x363) (= (x447 x237 x391) x478) (x407 x299 x363) (x407 x52 x282) (x407 x5 x59) (= x126 (x259 (x259 x56 x487) x444)) (x407 x295 x363) (= (x447 x309 x52) x190) (x407 x477 x282) (x504 x444 x17) (= x86 (x447 x285 x362)) (= (x447 x413 x78) x481) (x407 x537 x363) (x407 x124 x363) (= (x447 x114 x327) x148) (x407 x392 x282) (= x265 (x259 x286 x444)) (= x354 (x259 x290 x154)) (and (x504 x163 x109) (x6 x163 x456)) (x407 x541 x363) (x407 x453 x363) (= x377 (x492 (x9 (x447 x67 x444) (x447 x261 x444)))) (x504 x456 x210) (= x356 (x447 x237 x31)) (x407 x290 x419) (= (x447 x114 x180) x298) (= x468 (x492 (x9 x231 (x9 x92 (x9 x359 (x9 x451 (x9 x457 (x9 x321 (x9 x418 (x9 x184 x427)))))))))) (= x438 (x447 x264 x379)) (x407 x73 x59) (= (x447 x413 x516) x206) (x407 x74 x363) (x504 x50 x426) (not (= x510 x261)) (= (x259 x76 x12) x330) (x407 x272 x207) (x407 x335 x363) (x407 x115 x363) (x407 x78 x59) (x407 x248 x419) (x407 x37 x363) (x407 x506 x207) (x407 x376 x59) (x407 x255 x207) (x407 x462 x59) (x407 x117 x363) (x407 x289 x207) (x407 x166 x363) (= (x400 x456 x150) x207) (x38 (x447 x215 x210) x341) (x38 x315 x341) (x407 x249 x363) (x407 x84 (x422 x468 x468)) (x407 x50 x363) (= (x447 x413 x317) x167) (x504 x136 x336) (= (x447 x413 x199) x87) (x407 x71 x419) (x407 x469 x59) (x407 x309 x363) (x407 x210 x363) (x407 x13 x363) (x407 x356 x363) (not (= x510 x54)) (x407 x522 x419) (= x480 (x447 x413 x192)) (= x27 (x447 x36 x210)) (x407 x283 x363) (= (x259 x334 x444) x368) (x407 x108 x419) (x407 x486 x207) (x407 x307 x363) (x407 x216 x207) (= (x492 (x9 x81 x95)) x470) (= x64 (x259 x76 x444)) (x407 x286 x363) (= x229 (x259 (x259 x299 x13) x444)) (x407 x176 x363) (x407 x264 x363) (x38 (x447 x464 x210) x341) (x38 x10 x341) (x407 x27 x363) (x407 x364 x363) (x407 x268 (x132 (x178 x468 x468) (x158 x419 (x492 x288)))) (x407 x254 x419) (x407 x187 x207) (x407 x454 x282) (x38 x438 x341) (x407 x232 x419) (x407 x458 x363) (x407 x241 x363) (x407 x163 x363) (x407 x487 x363) (x407 x87 x363) (= (x253 x210 x364) x286) (x407 x336 x363) (x407 x315 x363) (x407 x29 x59) (x407 x386 x363) (= x363 (x400 x456 x60)) (x407 x391 x282) (x38 x394 x341) (= x37 (x259 x364 x444)) (= x76 (x447 x215 x210)) (x407 x529 x363) (x407 x136 x363) (x407 x239 x419) (x407 x421 x363) (x407 x439 x59) (x407 x97 x59) (= (x447 x413 x96) x273) (x504 x522 x300) (x407 x75 x207) (x407 x179 x363) (x504 x444 x52) (x407 x55 x207) (x407 x31 x282) (x407 x106 x59) (x407 x463 (x132 (x178 x468 x468) x363)) (x407 x24 x363) (= (x259 x214 x12) x228) (x38 x94 x341) (x504 x12 x210) (= x315 (x447 x264 x5)) (x504 x12 x386) (x407 x508 x363) (x407 x172 x207) (x407 x116 x282) (and (x504 x243 x109) (x6 x243 x456)) (= x329 (x259 x307 x444)) (x407 x61 x363) (x407 x21 x363) (x504 x28 x300) (and (x6 x365 x456) (x504 x365 x109)) (x407 x250 x207) (x407 x228 x363) (x407 x432 x419) (x407 x66 x363) (x407 x86 x363) (= x214 (x447 x421 x210)) (x504 x12 x391) (x504 (x447 x36 x12) x341) (x407 x483 x363) (= (x447 x318 x495) x66) (x407 x426 x363) (x407 x480 x363) (x407 x408 x363) (x407 x204 x363) (x407 x296 x207) (= x74 (x447 x309 x434)) (= x10 (x447 x541 x210)) (x407 x433 x363) (x407 x235 x282) (x407 x99 x363) (and (x6 x168 x456) (x504 x168 x341)) (x407 x280 x207) (x407 x17 x282) (not (= x432 x254)) (x407 x76 x363) (x407 x162 x363) (not (= x54 x261)) (x407 x347 x207) (= x426 (x259 x386 x444)) (x407 x213 x363) (x407 x372 x363) (x407 x481 x363) (x407 x56 x207) (x407 x287 x363) (x407 x10 x363) (x407 x298 x363) (x407 x197 x363) (x504 x408 x336) (x407 x394 x363) (= (x259 x172 x13) x462) (x407 x516 x282) (x407 x28 x419) (x504 x283 x426) (x407 x503 x207) (x407 x142 x419) (x407 x243 x363) (x407 x171 x363) (x407 x365 x363) (x407 x330 x363) (= x300 x288) (= x458 (x447 x413 x262)) (x407 x416 x363) (= x79 (x492 (x9 x455 x98))) (x407 x229 x59) (x504 x239 x300) (x407 x258 x419) (x407 x368 x363) (x407 x273 x363) (x407 x285 x363) (x407 x337 x207) (= x213 (x447 x413 x338)) (x407 x333 x207) (= (x259 x216 x444) x347) (x407 x424 x363) (x407 x77 x207) (= x143 (x259 x27 x444)) (x407 x174 x363) (x407 x154 x419) (x407 x406 x207) (x407 x138 x59) (x504 x444 x116) (x407 x466 x207) (x407 x205 x207) (x407 x214 x363) (x407 x94 x363) (x407 x319 x59) (x407 x332 x363) (x407 x237 x363) (x407 x146 x363) (x504 x444 x364) (x407 x354 x282) (x407 x405 x207) (x407 x479 x363) (x407 x96 x282) (x407 x53 x363) (x504 x108 x48) (= (x447 x285 x454) x416) (x407 x384 x59) (= x90 (x447 x285 x235)) (x407 x474 x207) (= x220 (x259 x117 x99)) (x407 x464 x363) (x407 x114 x363) (x407 x491 x282) (= x133 (x259 x214 x444)) (x407 x495 x59) (x407 x343 x59) (= (x447 x413 x477) x295) (x407 x134 x363) (x407 x247 x207) (x407 x167 x363) (= x393 (x492 (x9 x328 (x9 x32 (x9 x306 (x9 x105 (x9 x520 (x9 x2 (x9 x348 (x9 x82 x118)))))))))) (x407 x190 x363) (x407 x69 x363) (x407 x382 x363) (x407 x472 x419) (x407 x314 (x422 x468 x468)) (x407 x341 x363) (= x326 (x492 (x9 (x447 x510 x444) (x447 x54 x444)))) (x407 x143 x363) (x407 x313 x207) (= x419 (x400 x456 x288)) (x407 x54 x363) (and (x504 x399 x341) (x6 x399 x456)) (x407 x533 x207) (not (= x261 x67)) (x407 x242 x207) (= (x447 x264 x73) x94) (x407 x362 x282) (x407 x526 x363) (and (x504 x241 x109) (x6 x241 x456)) (x504 x176 x336) (x407 x329 x363) (and (x6 x195 x456) (x504 x195 x109)) (x407 x168 x363) (x38 x364 x341) (x407 x460 x207) (x407 x276 x363) (x407 x325 x363) (x407 x182 x207) (x504 x12 x31) (= (x447 x103 x376) x65) (x407 x532 x207) (= x334 (x253 x210 x210)) (= (x492 (x9 x221 (x9 x165 (x9 x49 (x9 x410 (x9 x502 (x9 x538 (x9 x417 (x9 x159 (x9 x355 (x9 x260 (x9 x277 (x9 x107 (x9 x7 (x9 x517 (x9 x360 (x9 x121 x357))))))))))))))))) x201) (x407 x275 x207) (= (x259 x486 x444) x333) (= x499 (x447 x309 x17)) (x407 x238 x363) (x407 x399 x363) (= (x447 x114 x469) x179) (x38 x526 x341) (x407 x173 x363) (= x60 x341) (x407 x438 x363) (x504 x444 x515) (not (= x510 x67)) (x407 x208 x363) (x407 x199 x282) (= (x447 x318 x106) x394) (x407 x262 x282) (x407 x304 x207) (= x515 (x259 x332 x99)) (x38 (x447 x421 x210) x341) (x407 x510 x363) (x504 x444 x413) (= x439 (x259 x4 x13)) (x407 x126 x59) (x407 x209 x59) (= (x492 (x9 x436 x123)) x371) (= x249 (x447 x114 x319)) (x407 x284 x207) (x407 x515 x282) (x407 x490 x363) (x407 x48 x419) (x407 x412 x207) (x407 x41 x282) (x38 x27 x341) (x504 x325 x336) (= (x447 x413 x491) x503) (x407 x44 x363) (x407 x148 x363) (x407 x195 x363) (x407 x65 x363) (x38 x66 x341) (x407 x131 x419) (= x529 (x447 x285 x41)) (x407 x327 x59) (x407 x90 x363) (not (= x399 x168)) (x407 x461 x363) (x504 x30 x300) (x407 x202 x363) (= x202 (x447 x237 x392)) (= x279 (x447 x309 x116)) (= x314 (x383 (x25 x463) (x492 x399))) (x407 x308 x419) (= (x447 x114 x29) x461) (x407 x379 x59) (x504 x444 x434) (x407 x378 x419) (= x174 (x447 x114 x384)) (= (x492 (x9 x168 x399)) x345) (x407 x236 (x132 (x178 x468 x468) x419)) (x407 x194 x419) (x407 x485 x419) (= (x259 (x259 x508 x13) x444) x209) (x407 x192 x282) (x407 x367 x363) (x407 x261 x363) (not (= x54 x67)) (x407 x215 x363) (x407 x133 x363) (x407 x300 x419) (x407 x170 x363) (x407 x281 x207) (x407 x180 x59) (x504 x12 x392) (= (x400 x456 x367) (x492 (x9 x510 (x9 x67 (x9 x261 x54))))) (= (x259 (x259 x382 x13) x444) x138) (and (x504 x335 x109) (x6 x335 x456)) (x407 x403 x207) (x407 x317 x282) (x407 x36 x363) (x504 x391 x31) (= x255 x150) (x407 x122 x207) (x407 x30 x419) (x407 x318 x363) (x407 x220 x59) (x407 x514 x207) (x407 x291 x419) (x407 x338 x282) (x504 x444 x454) (x407 x310 x207) (x407 x47 x419) (x407 x103 x363) (= x69 (x447 x464 x210))))
(define-fun x263 () Bool (and (x407 x511 (x34 x488 x363)) (x407 x535 (x132 (x400 x456 x367) x363)) (x46 x303 (x400 x444 x210)) (x407 x211 (x132 (x400 x456 x367) x363)) (x407 x366 (x132 (x400 x456 x367) (x132 (x400 x456 x329) x419))) (x407 x175 x363) (x407 x230 (x132 (x400 x456 x367) x419)) (x407 x23 (x132 (x400 x456 x367) x419)) (x407 x509 (x132 (x400 x456 x336) x363)) (x407 x223 (x132 (x400 x456 x367) x419)) (x407 x267 (x132 (x400 x456 x367) x363)) (x407 x361 x207) (x407 x397 x207) (or (= x444 x452) (= x12 x452)) (x407 x144 (x132 (x400 x456 x367) x363)) (x407 x505 (x132 (x400 x456 x367) (x132 (x400 x456 x329) x419))) (x407 x152 (x132 (x400 x456 x367) x419)) (x407 x183 (x132 (x400 x456 x367) (x132 (x400 x456 x406) x363))) (x407 x500 (x132 (x400 x456 x367) (x132 (x400 x456 x329) x419))) (x407 x380 (x132 (x400 x456 x367) (x132 (x400 x456 x329) x419))) (x407 x385 (x132 (x400 x456 x367) (x132 (x400 x456 x333) x363))) (x407 x353 (x132 (x400 x456 x367) (x132 (x400 x456 x329) (x132 (x400 x456 x347) x363)))) (x407 x181 (x132 (x400 x456 x367) x363)) (x407 x414 x488) (x407 x128 (x132 (x400 x456 x367) (x132 (x400 x456 x329) x419))) (x407 x423 (x132 (x400 x456 x367) x419)) (x407 x476 x207) (x407 x511 (x34 x488 x207)) (x407 x302 (x132 (x400 x456 x367) (x132 (x400 x456 x329) x419))) (x407 x3 (x132 (x400 x456 x367) x363)) (x407 x175 x345) (x407 x200 (x132 (x400 x456 x367) (x132 (x400 x456 x329) x419))) (x407 x212 (x132 (x400 x456 x367) x363)) (x407 x342 (x132 (x400 x456 x367) x419)) (x407 x155 (x132 (x400 x456 x367) x363)) (x407 x33 (x132 (x400 x456 x367) (x132 (x400 x456 x329) (x132 (x400 x456 x347) x363)))) (x407 x186 (x132 (x400 x456 x367) x419)) (x407 x110 (x132 (x400 x456 x367) x363)) (x407 x198 (x132 (x400 x456 x367) x363)) (x407 x311 (x132 (x400 x456 x367) x363)) (x407 x331 x488) (x407 x111 x207) (x407 x147 x207) (x407 x494 x488) (x407 x452 x363) (x407 x387 x488) (x407 x234 x488) (x407 x93 (x132 (x400 x456 x367) x419)) (x407 x217 (x132 (x400 x456 x367) x363)) (x407 x305 (x132 (x400 x456 x367) x363)) (x407 x340 (x132 (x400 x456 x367) x363)) (x407 x20 (x132 (x400 x456 x367) x363)) (x407 x57 (x132 (x400 x456 x287) x363)) (x407 x18 (x132 (x400 x456 x367) x363)) (x407 x511 (x34 x488 x419)) (x407 x26 (x132 (x400 x456 x367) (x132 (x400 x456 x333) x363))) (x407 x45 (x132 (x400 x456 x367) (x132 (x400 x456 x329) (x132 (x400 x456 x405) x363)))) (x46 x22 (x400 x444 x210)) (x46 x62 (x400 x444 x210)) (x407 x375 x207) (x407 x449 (x132 (x400 x456 x367) x419)) (x407 x145 (x132 (x400 x456 x367) x419)) (x407 x233 (x132 (x400 x456 x367) (x132 (x400 x456 x329) x419))) (x407 x51 x488) (x407 x512 (x132 (x400 x456 x367) x419))))
(define-fun x39 () Bool true)
(define-fun x14 () Bool true)
(define-fun x177 () Bool true)
(define-fun x442 () Bool true)
(define-fun x269 () Bool true)
(define-fun x16 () Bool (and (=> (= x429 x475) (not (x407 x113 (x492 (x9 x150 x456))))) (x407 x271 x488) (x407 x420 x488) (x407 x113 x207) (x407 x475 x488)))
(define-fun x352 () Bool (and (x407 x513 x282) (= x225 x475) (x407 x489 x282) (x46 x370 (x400 x444 x489)) (= x292 x420) (x407 x169 x207) (= x271 x278) (= x113 x169) (x46 x301 (x400 x444 x210)) (x46 x323 (x400 x444 x489)) (x407 x402 (x422 (x400 x444 x210) (x400 x444 x513))) (x46 x193 (x400 x444 x11)) (x407 x349 x488) (x407 x225 x488) (x46 x445 (x400 x444 x489)) (x407 x428 (x132 (x400 x444 x210) x282)) (x46 x409 (x400 x444 x11)) (x407 x11 x282)))
(define-fun x293 () Bool true)
(define-fun x196 () Bool true)
(define-fun x551 () Bool (= x429 x387))
(define-fun x548 () Bool (x407 x536 x207))
(define-fun x555 () Bool (=> (= x429 (x101 (exists ((x556 x467)) (and (and (x6 x556 x444) (x504 x556 x210)) (x6 (x188 (x178 (x400 x444 x210) (x492 x456)) x556) x208) (x46 (x400 (x259 (x447 x513 x444) x126) (x447 x513 x444)) (x383 (x540 x402 (x178 x401 (x492 (x447 x513 x444)))) (x492 x556))))))) (not (x407 x536 (x492 (x9 x150 x456))))))
(define-fun x552 () Bool (= (x101 (exists ((x556 x467)) (and (x46 (x400 (x259 (x447 x513 x444) x126) (x447 x513 x444)) (x383 (x540 x402 (x178 x401 (x492 (x447 x513 x444)))) (x492 x556))) (and (x6 x556 x444) (x504 x556 x210)) (x6 (x188 (x178 (x400 x444 x210) (x492 x456)) x556) x208)))) x429))
(push 1)
(assert (not (=> (and x551 x555 x552 x548) (not (x407 x536 (x492 (x9 x150 x456)))))))
(set-info :status unsat)
(check-sat)
(get-proof)
(pop 1)
(exit)