diff options
Diffstat (limited to 'test/regress/regress1/lemmas/simple_startup_9nodes.abstract.base.smt')
| -rw-r--r-- | test/regress/regress1/lemmas/simple_startup_9nodes.abstract.base.smt | 128 |
1 files changed, 0 insertions, 128 deletions
diff --git a/test/regress/regress1/lemmas/simple_startup_9nodes.abstract.base.smt b/test/regress/regress1/lemmas/simple_startup_9nodes.abstract.base.smt deleted file mode 100644 index 506b99b46..000000000 --- a/test/regress/regress1/lemmas/simple_startup_9nodes.abstract.base.smt +++ /dev/null @@ -1,128 +0,0 @@ -(benchmark tta_startup - :source { TTA Startup. Bruno Dutertre (bruno@csl.sri.com) } - - - :status unsat -:category { industrial } -:difficulty { 0 } - :logic QF_LRA - - :extrafuns ((x_0 Real)) - :extrafuns ((x_1 Real)) - :extrafuns ((x_2 Real)) - :extrafuns ((x_3 Real)) - :extrafuns ((x_4 Real)) - :extrafuns ((x_5 Real)) - :extrafuns ((x_6 Real)) - :extrafuns ((x_7 Real)) - :extrafuns ((x_8 Real)) - :extrafuns ((x_9 Real)) - :extrafuns ((x_10 Real)) - :extrafuns ((x_11 Real)) - :extrafuns ((x_12 Real)) - :extrafuns ((x_13 Real)) - :extrafuns ((x_14 Real)) - :extrafuns ((x_15 Real)) - :extrafuns ((x_16 Real)) - :extrafuns ((x_17 Real)) - :extrafuns ((x_18 Real)) - :extrapreds ((x_19)) - :extrapreds ((x_20)) - :extrapreds ((x_21)) - :extrapreds ((x_22)) - :extrapreds ((x_23)) - :extrapreds ((x_24)) - :extrapreds ((x_25)) - :extrapreds ((x_26)) - :extrapreds ((x_27)) - :extrafuns ((x_28 Real)) - :extrapreds ((x_29)) - :extrapreds ((x_30)) - :extrapreds ((x_31)) - :extrafuns ((x_32 Real)) - :extrafuns ((x_33 Real)) - :extrafuns ((x_34 Real)) - :extrafuns ((x_35 Real)) - :extrafuns ((x_36 Real)) - :extrafuns ((x_37 Real)) - :extrafuns ((x_38 Real)) - :extrafuns ((x_39 Real)) - :extrafuns ((x_40 Real)) - :extrafuns ((x_41 Real)) - :extrafuns ((x_42 Real)) - :extrafuns ((x_43 Real)) - :extrafuns ((x_44 Real)) - :extrafuns ((x_45 Real)) - :extrafuns ((x_46 Real)) - :extrafuns ((x_47 Real)) - :extrafuns ((x_48 Real)) - :extrafuns ((x_49 Real)) - :extrafuns ((x_50 Real)) - :extrafuns ((x_51 Real)) - :extrafuns ((x_52 Real)) - :extrafuns ((x_53 Real)) - :extrafuns ((x_54 Real)) - :extrafuns ((x_55 Real)) - :extrafuns ((x_56 Real)) - :extrafuns ((x_57 Real)) - :extrafuns ((x_58 Real)) - :extrafuns ((x_59 Real)) - :extrafuns ((x_60 Real)) - :extrafuns ((x_61 Real)) - :extrafuns ((x_62 Real)) - :extrafuns ((x_63 Real)) - :extrafuns ((x_64 Real)) - :extrafuns ((x_65 Real)) - :extrafuns ((x_66 Real)) - :extrafuns ((x_67 Real)) - :extrafuns ((x_68 Real)) - :extrafuns ((x_69 Real)) - :extrafuns ((x_70 Real)) - :extrafuns ((x_71 Real)) - :extrafuns ((x_72 Real)) - :extrafuns ((x_73 Real)) - :extrafuns ((x_74 Real)) - :extrafuns ((x_75 Real)) - :extrafuns ((x_76 Real)) - :extrafuns ((x_77 Real)) - :extrafuns ((x_78 Real)) - :extrafuns ((x_79 Real)) - :extrafuns ((x_80 Real)) - :extrafuns ((x_81 Real)) - :extrafuns ((x_82 Real)) - :extrafuns ((x_83 Real)) - :extrafuns ((x_84 Real)) - :extrafuns ((x_85 Real)) - :extrapreds ((x_86)) - :extrafuns ((x_87 Real)) - :extrapreds ((x_88)) - :extrapreds ((x_89)) - :extrapreds ((x_90)) - :extrapreds ((x_91)) - :extrapreds ((x_92)) - :extrapreds ((x_93)) - :extrapreds ((x_94)) - :extrapreds ((x_95)) - :extrafuns ((x_96 Real)) - :extrafuns ((x_97 Real)) - :extrafuns ((x_98 Real)) - :extrafuns ((x_99 Real)) - :extrafuns ((x_100 Real)) - :extrafuns ((x_101 Real)) - :extrafuns ((x_102 Real)) - :extrafuns ((x_103 Real)) - :extrafuns ((x_104 Real)) - :extrafuns ((x_105 Real)) - :extrafuns ((x_106 Real)) - :extrafuns ((x_107 Real)) - :extrafuns ((x_108 Real)) - :extrafuns ((x_109 Real)) - :extrafuns ((x_110 Real)) - :extrafuns ((x_111 Real)) - :extrafuns ((x_112 Real)) - :extrafuns ((x_113 Real)) - :extrafuns ((x_114 Real)) - :extrafuns ((x_115 Real)) - :formula -(flet ($cvcl_201 (= x_0 0)) (flet ($cvcl_221 (= x_0 1)) (flet ($cvcl_225 (= x_0 2)) (flet ($cvcl_270 (= x_1 0)) (flet ($cvcl_277 (= x_1 1)) (flet ($cvcl_279 (= x_1 2)) (flet ($cvcl_291 (= x_2 0)) (flet ($cvcl_298 (= x_2 1)) (flet ($cvcl_300 (= x_2 2)) (flet ($cvcl_310 (= x_3 0)) (flet ($cvcl_317 (= x_3 1)) (flet ($cvcl_319 (= x_3 2)) (flet ($cvcl_329 (= x_4 0)) (flet ($cvcl_336 (= x_4 1)) (flet ($cvcl_338 (= x_4 2)) (flet ($cvcl_348 (= x_5 0)) (flet ($cvcl_355 (= x_5 1)) (flet ($cvcl_357 (= x_5 2)) (flet ($cvcl_367 (= x_6 0)) (flet ($cvcl_374 (= x_6 1)) (flet ($cvcl_376 (= x_6 2)) (flet ($cvcl_386 (= x_7 0)) (flet ($cvcl_393 (= x_7 1)) (flet ($cvcl_395 (= x_7 2)) (flet ($cvcl_405 (= x_8 0)) (flet ($cvcl_412 (= x_8 1)) (flet ($cvcl_414 (= x_8 2)) (flet ($cvcl_224 (= x_18 0)) (flet ($cvcl_245 (= x_0 3)) (flet ($cvcl_290 (= x_1 3)) (flet ($cvcl_309 (= x_2 3)) (flet ($cvcl_328 (= x_3 3)) (flet ($cvcl_347 (= x_4 3)) (flet ($cvcl_366 (= x_5 3)) (flet ($cvcl_385 (= x_6 3)) (flet ($cvcl_404 (= x_7 3)) (flet ($cvcl_423 (= x_8 3)) (flet ($cvcl_171 (not x_19)) (flet ($cvcl_172 (not x_20)) (flet ($cvcl_173 (not x_21)) (flet ($cvcl_174 (not x_22)) (flet ($cvcl_175 (not x_23)) (flet ($cvcl_176 (not x_24)) (flet ($cvcl_177 (not x_25)) (flet ($cvcl_178 (not x_26)) (flet ($cvcl_179 (not x_27)) (flet ($cvcl_1 (= x_28 9)) (flet ($cvcl_2 (= x_28 8)) (flet ($cvcl_3 (= x_28 7)) (flet ($cvcl_4 (= x_28 6)) (flet ($cvcl_5 (= x_28 5)) (flet ($cvcl_6 (= x_28 4)) (flet ($cvcl_7 (= x_28 3)) (flet ($cvcl_8 (= x_28 2)) (flet ($cvcl_202 (= x_54 1)) (flet ($cvcl_219 (= x_54 2)) (flet ($cvcl_271 (= x_55 1)) (flet ($cvcl_274 (= x_55 2)) (flet ($cvcl_292 (= x_56 1)) (flet ($cvcl_295 (= x_56 2)) (flet ($cvcl_311 (= x_57 1)) (flet ($cvcl_314 (= x_57 2)) (flet ($cvcl_330 (= x_58 1)) (flet ($cvcl_333 (= x_58 2)) (flet ($cvcl_349 (= x_59 1)) (flet ($cvcl_352 (= x_59 2)) (flet ($cvcl_368 (= x_60 1)) (flet ($cvcl_371 (= x_60 2)) (flet ($cvcl_387 (= x_61 1)) (flet ($cvcl_390 (= x_61 2)) (flet ($cvcl_406 (= x_62 1)) (flet ($cvcl_409 (= x_62 2)) (flet ($cvcl_445 (not $cvcl_202)) (flet ($cvcl_524 (not (< x_63 (+ x_64 54)))) (flet ($cvcl_446 (not $cvcl_271)) (flet ($cvcl_526 (not (< x_65 (+ x_64 57)))) (flet ($cvcl_447 (not $cvcl_292)) (flet ($cvcl_528 (not (< x_66 (+ x_64 60)))) (flet ($cvcl_448 (not $cvcl_311)) (flet ($cvcl_530 (not (< x_67 (+ x_64 63)))) (flet ($cvcl_449 (not $cvcl_330)) (flet ($cvcl_532 (not (< x_68 (+ x_64 66)))) (flet ($cvcl_450 (not $cvcl_349)) (flet ($cvcl_534 (not (< x_69 (+ x_64 69)))) (flet ($cvcl_451 (not $cvcl_368)) (flet ($cvcl_536 (not (< x_70 (+ x_64 72)))) (flet ($cvcl_452 (not $cvcl_387)) (flet ($cvcl_538 (not (< x_71 (+ x_64 75)))) (flet ($cvcl_453 (not $cvcl_406)) (flet ($cvcl_540 (not (< x_72 (+ x_64 78)))) (flet ($cvcl_436 (not $cvcl_219)) (flet ($cvcl_437 (not $cvcl_274)) (flet ($cvcl_438 (not $cvcl_295)) (flet ($cvcl_439 (not $cvcl_314)) (flet ($cvcl_440 (not $cvcl_333)) (flet ($cvcl_441 (not $cvcl_352)) (flet ($cvcl_442 (not $cvcl_371)) (flet ($cvcl_443 (not $cvcl_390)) (flet ($cvcl_444 (not $cvcl_409)) (flet ($cvcl_475 (not (<= (- x_65 x_63) x_32))) (flet ($cvcl_476 (not (<= (- x_66 x_63) x_32))) (flet ($cvcl_477 (not (<= (- x_67 x_63) x_32))) (flet ($cvcl_478 (not (<= (- x_68 x_63) x_32))) (flet ($cvcl_479 (not (<= (- x_69 x_63) x_32))) (flet ($cvcl_480 (not (<= (- x_70 x_63) x_32))) (flet ($cvcl_481 (not (<= (- x_71 x_63) x_32))) (flet ($cvcl_482 (not (<= (- x_72 x_63) x_32))) (flet ($cvcl_483 (not (<= (- x_66 x_65) x_32))) (flet ($cvcl_484 (not (<= (- x_67 x_65) x_32))) (flet ($cvcl_485 (not (<= (- x_68 x_65) x_32))) (flet ($cvcl_486 (not (<= (- x_69 x_65) x_32))) (flet ($cvcl_487 (not (<= (- x_70 x_65) x_32))) (flet ($cvcl_488 (not (<= (- x_71 x_65) x_32))) (flet ($cvcl_489 (not (<= (- x_72 x_65) x_32))) (flet ($cvcl_490 (not (<= (- x_67 x_66) x_32))) (flet ($cvcl_491 (not (<= (- x_68 x_66) x_32))) (flet ($cvcl_492 (not (<= (- x_69 x_66) x_32))) (flet ($cvcl_493 (not (<= (- x_70 x_66) x_32))) (flet ($cvcl_494 (not (<= (- x_71 x_66) x_32))) (flet ($cvcl_495 (not (<= (- x_72 x_66) x_32))) (flet ($cvcl_496 (not (<= (- x_68 x_67) x_32))) (flet ($cvcl_497 (not (<= (- x_69 x_67) x_32))) (flet ($cvcl_498 (not (<= (- x_70 x_67) x_32))) (flet ($cvcl_499 (not (<= (- x_71 x_67) x_32))) (flet ($cvcl_500 (not (<= (- x_72 x_67) x_32))) (flet ($cvcl_501 (not (<= (- x_69 x_68) x_32))) (flet ($cvcl_502 (not (<= (- x_70 x_68) x_32))) (flet ($cvcl_503 (not (<= (- x_71 x_68) x_32))) (flet ($cvcl_504 (not (<= (- x_72 x_68) x_32))) (flet ($cvcl_505 (not (<= (- x_70 x_69) x_32))) (flet ($cvcl_506 (not (<= (- x_71 x_69) x_32))) (flet ($cvcl_507 (not (<= (- x_72 x_69) x_32))) (flet ($cvcl_508 (not (<= (- x_71 x_70) x_32))) (flet ($cvcl_509 (not (<= (- x_72 x_70) x_32))) (flet ($cvcl_510 (not (<= (- x_72 x_71) x_32))) (flet ($cvcl_514 (not (< (- x_63 x_64) 27))) (flet ($cvcl_466 (<= (- x_63 x_53) 27)) (flet ($cvcl_515 (not (< (- x_65 x_64) 30))) (flet ($cvcl_467 (<= (- x_65 x_53) 30)) (flet ($cvcl_516 (not (< (- x_66 x_64) 33))) (flet ($cvcl_468 (<= (- x_66 x_53) 33)) (flet ($cvcl_517 (not (< (- x_67 x_64) 36))) (flet ($cvcl_469 (<= (- x_67 x_53) 36)) (flet ($cvcl_518 (not (< (- x_68 x_64) 39))) (flet ($cvcl_470 (<= (- x_68 x_53) 39)) (flet ($cvcl_519 (not (< (- x_69 x_64) 42))) (flet ($cvcl_471 (<= (- x_69 x_53) 42)) (flet ($cvcl_520 (not (< (- x_70 x_64) 45))) (flet ($cvcl_472 (<= (- x_70 x_53) 45)) (flet ($cvcl_521 (not (< (- x_71 x_64) 48))) (flet ($cvcl_473 (<= (- x_71 x_53) 48)) (flet ($cvcl_522 (not (< (- x_72 x_64) 51))) (flet ($cvcl_474 (<= (- x_72 x_53) 51)) (flet ($cvcl_48 (= x_74 x_75)) (flet ($cvcl_51 (= x_74 x_76)) (flet ($cvcl_54 (= x_74 x_77)) (flet ($cvcl_57 (= x_74 x_78)) (flet ($cvcl_60 (= x_74 x_79)) (flet ($cvcl_63 (= x_74 x_80)) (flet ($cvcl_66 (= x_74 x_81)) (flet ($cvcl_69 (= x_74 x_82)) (flet ($cvcl_72 (= x_75 x_74)) (flet ($cvcl_74 (= x_75 x_76)) (flet ($cvcl_76 (= x_75 x_77)) (flet ($cvcl_78 (= x_75 x_78)) (flet ($cvcl_80 (= x_75 x_79)) (flet ($cvcl_82 (= x_75 x_80)) (flet ($cvcl_84 (= x_75 x_81)) (flet ($cvcl_86 (= x_75 x_82)) (flet ($cvcl_87 (= x_76 x_74)) (flet ($cvcl_88 (= x_76 x_75)) (flet ($cvcl_89 (= x_76 x_77)) (flet ($cvcl_90 (= x_76 x_78)) (flet ($cvcl_91 (= x_76 x_79)) (flet ($cvcl_92 (= x_76 x_80)) (flet ($cvcl_93 (= x_76 x_81)) (flet ($cvcl_94 (= x_76 x_82)) (flet ($cvcl_95 (= x_77 x_74)) (flet ($cvcl_96 (= x_77 x_75)) (flet ($cvcl_97 (= x_77 x_76)) (flet ($cvcl_98 (= x_77 x_78)) (flet ($cvcl_99 (= x_77 x_79)) (flet ($cvcl_100 (= x_77 x_80)) (flet ($cvcl_101 (= x_77 x_81)) (flet ($cvcl_102 (= x_77 x_82)) (flet ($cvcl_103 (= x_78 x_74)) (flet ($cvcl_104 (= x_78 x_75)) (flet ($cvcl_105 (= x_78 x_76)) (flet ($cvcl_106 (= x_78 x_77)) (flet ($cvcl_107 (= x_78 x_79)) (flet ($cvcl_108 (= x_78 x_80)) (flet ($cvcl_109 (= x_78 x_81)) (flet ($cvcl_110 (= x_78 x_82)) (flet ($cvcl_111 (= x_79 x_74)) (flet ($cvcl_112 (= x_79 x_75)) (flet ($cvcl_113 (= x_79 x_76)) (flet ($cvcl_114 (= x_79 x_77)) (flet ($cvcl_115 (= x_79 x_78)) (flet ($cvcl_116 (= x_79 x_80)) (flet ($cvcl_117 (= x_79 x_81)) (flet ($cvcl_118 (= x_79 x_82)) (flet ($cvcl_119 (= x_80 x_74)) (flet ($cvcl_120 (= x_80 x_75)) (flet ($cvcl_121 (= x_80 x_76)) (flet ($cvcl_122 (= x_80 x_77)) (flet ($cvcl_123 (= x_80 x_78)) (flet ($cvcl_124 (= x_80 x_79)) (flet ($cvcl_125 (= x_80 x_81)) (flet ($cvcl_126 (= x_80 x_82)) (flet ($cvcl_127 (= x_81 x_74)) (flet ($cvcl_128 (= x_81 x_75)) (flet ($cvcl_129 (= x_81 x_76)) (flet ($cvcl_130 (= x_81 x_77)) (flet ($cvcl_131 (= x_81 x_78)) (flet ($cvcl_132 (= x_81 x_79)) (flet ($cvcl_133 (= x_81 x_80)) (flet ($cvcl_134 (= x_81 x_82)) (flet ($cvcl_135 (= x_82 x_74)) (flet ($cvcl_136 (= x_82 x_75)) (flet ($cvcl_137 (= x_82 x_76)) (flet ($cvcl_138 (= x_82 x_77)) (flet ($cvcl_139 (= x_82 x_78)) (flet ($cvcl_140 (= x_82 x_79)) (flet ($cvcl_141 (= x_82 x_80)) (flet ($cvcl_142 (= x_82 x_81)) (flet ($cvcl_46 (not (< x_53 x_63))) (flet ($cvcl_547 (= x_74 x_84)) (flet ($cvcl_71 (not (< x_53 x_65))) (flet ($cvcl_549 (= x_75 x_84)) (flet ($cvcl_73 (not (< x_53 x_66))) (flet ($cvcl_551 (= x_76 x_84)) (flet ($cvcl_75 (not (< x_53 x_67))) (flet ($cvcl_553 (= x_77 x_84)) (flet ($cvcl_77 (not (< x_53 x_68))) (flet ($cvcl_555 (= x_78 x_84)) (flet ($cvcl_79 (not (< x_53 x_69))) (flet ($cvcl_557 (= x_79 x_84)) (flet ($cvcl_81 (not (< x_53 x_70))) (flet ($cvcl_559 (= x_80 x_84)) (flet ($cvcl_83 (not (< x_53 x_71))) (flet ($cvcl_561 (= x_81 x_84)) (flet ($cvcl_85 (not (< x_53 x_72))) (flet ($cvcl_563 (= x_82 x_84)) (flet ($cvcl_35 (= x_54 3)) (flet ($cvcl_44 (not $cvcl_35)) (flet ($cvcl_47 (not (= x_53 x_63))) (flet ($cvcl_36 (= x_55 3)) (flet ($cvcl_45 (not $cvcl_36)) (flet ($cvcl_49 (not (= x_53 x_65))) (flet ($cvcl_37 (= x_56 3)) (flet ($cvcl_50 (not $cvcl_37)) (flet ($cvcl_52 (not (= x_53 x_66))) (flet ($cvcl_38 (= x_57 3)) (flet ($cvcl_53 (not $cvcl_38)) (flet ($cvcl_55 (not (= x_53 x_67))) (flet ($cvcl_39 (= x_58 3)) (flet ($cvcl_56 (not $cvcl_39)) (flet ($cvcl_58 (not (= x_53 x_68))) (flet ($cvcl_40 (= x_59 3)) (flet ($cvcl_59 (not $cvcl_40)) (flet ($cvcl_61 (not (= x_53 x_69))) (flet ($cvcl_41 (= x_60 3)) (flet ($cvcl_62 (not $cvcl_41)) (flet ($cvcl_64 (not (= x_53 x_70))) (flet ($cvcl_42 (= x_61 3)) (flet ($cvcl_65 (not $cvcl_42)) (flet ($cvcl_67 (not (= x_53 x_71))) (flet ($cvcl_43 (= x_62 3)) (flet ($cvcl_68 (not $cvcl_43)) (flet ($cvcl_70 (not (= x_53 x_72))) (flet ($cvcl_523 (and x_86 (< x_87 x_63))) (flet ($cvcl_525 (and x_88 (< x_87 x_65))) (flet ($cvcl_527 (and x_89 (< x_87 x_66))) (flet ($cvcl_529 (and x_90 (< x_87 x_67))) (flet ($cvcl_531 (and x_91 (< x_87 x_68))) (flet ($cvcl_533 (and x_92 (< x_87 x_69))) (flet ($cvcl_535 (and x_93 (< x_87 x_70))) (flet ($cvcl_537 (and x_94 (< x_87 x_71))) (flet ($cvcl_539 (and x_95 (< x_87 x_72))) (flet ($cvcl_234 (not x_86)) (flet ($cvcl_288 (not x_88)) (flet ($cvcl_307 (not x_89)) (flet ($cvcl_326 (not x_90)) (flet ($cvcl_345 (not x_91)) (flet ($cvcl_364 (not x_92)) (flet ($cvcl_383 (not x_93)) (flet ($cvcl_402 (not x_94)) (flet ($cvcl_421 (not x_95)) (flet ($cvcl_143 (< x_74 1)) (let (?cvcl_144 (ite $cvcl_143 (- (- 1 x_74) 1) (- (+ (- 9 x_74) 1) 1))) (let (?cvcl_147 (ite (< x_75 2) (- (- 2 x_75) 1) (- (+ (- 9 x_75) 2) 1))) (let (?cvcl_155 (ite (< x_76 3) (- (- 3 x_76) 1) (- (+ (- 9 x_76) 3) 1))) (let (?cvcl_156 (ite (< x_77 4) (- (- 4 x_77) 1) (- (+ (- 9 x_77) 4) 1))) (let (?cvcl_157 (ite (< x_78 5) (- (- 5 x_78) 1) (- (+ (- 9 x_78) 5) 1))) (let (?cvcl_158 (ite (< x_79 6) (- (- 6 x_79) 1) (- (+ (- 9 x_79) 6) 1))) (let (?cvcl_159 (ite (< x_80 7) (- (- 7 x_80) 1) (- (+ (- 9 x_80) 7) 1))) (let (?cvcl_160 (ite (< x_81 8) (- (- 8 x_81) 1) (- (+ (- 9 x_81) 8) 1))) (let (?cvcl_161 (ite (< x_82 9) (- x_83 1) (- (+ x_83 9) 1))) (flet ($cvcl_544 (or (or (or (or (or (or (or (or x_86 x_88 ) x_89 ) x_90 ) x_91 ) x_92 ) x_93 ) x_94 ) x_95 )) (flet ($cvcl_18 (= x_84 9)) (flet ($cvcl_19 (= x_84 8)) (flet ($cvcl_20 (= x_84 7)) (flet ($cvcl_21 (= x_84 6)) (flet ($cvcl_22 (= x_84 5)) (flet ($cvcl_23 (= x_84 4)) (flet ($cvcl_24 (= x_84 3)) (flet ($cvcl_25 (= x_84 2)) (let (?cvcl_545 (ite $cvcl_18 x_72 (ite $cvcl_19 x_71 (ite $cvcl_20 x_70 (ite $cvcl_21 x_69 (ite $cvcl_22 x_68 (ite $cvcl_23 x_67 (ite $cvcl_24 x_66 (ite $cvcl_25 x_65 x_63))))))))) (flet ($cvcl_26 (= x_74 9)) (let (?cvcl_564 (ite $cvcl_26 1 (+ x_74 1))) (flet ($cvcl_27 (= x_75 9)) (let (?cvcl_565 (ite $cvcl_27 1 (+ x_75 1))) (flet ($cvcl_28 (= x_76 9)) (let (?cvcl_566 (ite $cvcl_28 1 (+ x_76 1))) (flet ($cvcl_29 (= x_77 9)) (let (?cvcl_567 (ite $cvcl_29 1 (+ x_77 1))) (flet ($cvcl_30 (= x_78 9)) (let (?cvcl_568 (ite $cvcl_30 1 (+ x_78 1))) (flet ($cvcl_31 (= x_79 9)) (let (?cvcl_569 (ite $cvcl_31 1 (+ x_79 1))) (flet ($cvcl_32 (= x_80 9)) (let (?cvcl_570 (ite $cvcl_32 1 (+ x_80 1))) (flet ($cvcl_33 (= x_81 9)) (let (?cvcl_571 (ite $cvcl_33 1 (+ x_81 1))) (flet ($cvcl_34 (= x_82 9)) (let (?cvcl_572 (ite $cvcl_34 1 (+ x_82 1))) (flet ($cvcl_228 (= x_18 1)) (flet ($cvcl_9 (= x_33 9)) (let (?cvcl_162 (ite $cvcl_9 1 (+ x_33 1))) (flet ($cvcl_10 (= x_34 9)) (let (?cvcl_163 (ite $cvcl_10 1 (+ x_34 1))) (flet ($cvcl_11 (= x_35 9)) (let (?cvcl_164 (ite $cvcl_11 1 (+ x_35 1))) (flet ($cvcl_12 (= x_36 9)) (let (?cvcl_165 (ite $cvcl_12 1 (+ x_36 1))) (flet ($cvcl_13 (= x_37 9)) (let (?cvcl_166 (ite $cvcl_13 1 (+ x_37 1))) (flet ($cvcl_14 (= x_38 9)) (let (?cvcl_167 (ite $cvcl_14 1 (+ x_38 1))) (flet ($cvcl_15 (= x_39 9)) (let (?cvcl_168 (ite $cvcl_15 1 (+ x_39 1))) (flet ($cvcl_16 (= x_40 9)) (let (?cvcl_169 (ite $cvcl_16 1 (+ x_40 1))) (flet ($cvcl_17 (= x_41 9)) (let (?cvcl_170 (ite $cvcl_17 1 (+ x_41 1))) (flet ($cvcl_206 (iff x_88 x_20)) (flet ($cvcl_207 (iff x_89 x_21)) (flet ($cvcl_208 (iff x_90 x_22)) (flet ($cvcl_209 (iff x_91 x_23)) (flet ($cvcl_210 (iff x_92 x_24)) (flet ($cvcl_211 (iff x_93 x_25)) (flet ($cvcl_212 (iff x_94 x_26)) (flet ($cvcl_213 (iff x_95 x_27)) (flet ($cvcl_214 (= x_84 x_28)) (flet ($cvcl_230 (= x_74 x_28)) (flet ($cvcl_283 (= x_75 x_28)) (flet ($cvcl_304 (= x_76 x_28)) (flet ($cvcl_323 (= x_77 x_28)) (flet ($cvcl_192 (= x_53 x_9)) (flet ($cvcl_193 (= x_53 x_10)) (flet ($cvcl_342 (= x_78 x_28)) (flet ($cvcl_194 (= x_53 x_11)) (flet ($cvcl_195 (= x_53 x_12)) (flet ($cvcl_196 (= x_53 x_13)) (flet ($cvcl_197 (= x_53 x_14)) (flet ($cvcl_198 (= x_53 x_15)) (flet ($cvcl_199 (= x_53 x_16)) (flet ($cvcl_200 (= x_53 x_17)) (flet ($cvcl_361 (= x_79 x_28)) (flet ($cvcl_380 (= x_80 x_28)) (flet ($cvcl_399 (= x_81 x_28)) (flet ($cvcl_418 (= x_82 x_28)) (flet ($cvcl_267 (= x_62 x_8)) (flet ($cvcl_268 (= x_82 x_41)) (flet ($cvcl_269 (= x_72 x_17)) (flet ($cvcl_216 (= x_54 x_0)) (flet ($cvcl_204 (= x_74 x_33)) (flet ($cvcl_217 (= x_63 x_9)) (flet ($cvcl_246 (= x_55 x_1)) (flet ($cvcl_247 (= x_75 x_34)) (flet ($cvcl_248 (= x_65 x_10)) (flet ($cvcl_249 (= x_56 x_2)) (flet ($cvcl_250 (= x_76 x_35)) (flet ($cvcl_251 (= x_66 x_11)) (flet ($cvcl_252 (= x_57 x_3)) (flet ($cvcl_253 (= x_77 x_36)) (flet ($cvcl_254 (= x_67 x_12)) (flet ($cvcl_255 (= x_58 x_4)) (flet ($cvcl_256 (= x_78 x_37)) (flet ($cvcl_257 (= x_68 x_13)) (flet ($cvcl_258 (= x_59 x_5)) (flet ($cvcl_259 (= x_79 x_38)) (flet ($cvcl_260 (= x_69 x_14)) (flet ($cvcl_261 (= x_60 x_6)) (flet ($cvcl_262 (= x_80 x_39)) (flet ($cvcl_263 (= x_70 x_15)) (flet ($cvcl_264 (= x_61 x_7)) (flet ($cvcl_265 (= x_81 x_40)) (flet ($cvcl_266 (= x_71 x_16)) (flet ($cvcl_190 (and (and (and (and (and (and (and (and $cvcl_171 $cvcl_172) $cvcl_173) $cvcl_174) $cvcl_175) $cvcl_176) $cvcl_177) $cvcl_178) $cvcl_179)) (flet ($cvcl_220 (iff x_86 false)) (flet ($cvcl_276 (iff x_88 false)) (flet ($cvcl_297 (iff x_89 false)) (flet ($cvcl_316 (iff x_90 false)) (flet ($cvcl_335 (iff x_91 false)) (flet ($cvcl_354 (iff x_92 false)) (flet ($cvcl_373 (iff x_93 false)) (flet ($cvcl_392 (iff x_94 false)) (flet ($cvcl_411 (iff x_95 false)) (flet ($cvcl_0 (= x_28 1)) (flet ($cvcl_511 (not x_29)) (flet ($cvcl_454 (not x_30)) (flet ($cvcl_542 (and $cvcl_511 $cvcl_454)) (flet ($cvcl_455 (not x_31)) (flet ($cvcl_425 (and $cvcl_542 $cvcl_455)) (flet ($cvcl_582 (and x_29 $cvcl_454)) (flet ($cvcl_584 (or x_29 x_30 )) (flet ($cvcl_585 (or $cvcl_511 x_30 )) (flet ($cvcl_586 (and (and (and (and (and (or $cvcl_584 x_31 ) (or $cvcl_585 x_31 )) (or (or x_29 $cvcl_454 ) x_31 )) (or (or $cvcl_511 $cvcl_454 ) x_31 )) (or $cvcl_584 $cvcl_455 )) (or $cvcl_585 $cvcl_455 ))) (flet ($cvcl_180 (> x_9 0)) (flet ($cvcl_181 (> x_10 0)) (flet ($cvcl_182 (> x_11 0)) (flet ($cvcl_183 (> x_12 0)) (flet ($cvcl_184 (> x_13 0)) (flet ($cvcl_185 (> x_14 0)) (flet ($cvcl_186 (> x_15 0)) (flet ($cvcl_187 (> x_16 0)) (flet ($cvcl_188 (> x_17 0)) (flet ($cvcl_426 (and (and (and (and (and (and (and (and $cvcl_234 $cvcl_288) $cvcl_307) $cvcl_326) $cvcl_345) $cvcl_364) $cvcl_383) $cvcl_402) $cvcl_421)) (flet ($cvcl_546 (or $cvcl_44 $cvcl_46 )) (flet ($cvcl_548 (or $cvcl_45 $cvcl_71 )) (flet ($cvcl_550 (or $cvcl_50 $cvcl_73 )) (flet ($cvcl_552 (or $cvcl_53 $cvcl_75 )) (flet ($cvcl_554 (or $cvcl_56 $cvcl_77 )) (flet ($cvcl_556 (or $cvcl_59 $cvcl_79 )) (flet ($cvcl_558 (or $cvcl_62 $cvcl_81 )) (flet ($cvcl_560 (or $cvcl_65 $cvcl_83 )) (flet ($cvcl_562 (or $cvcl_68 $cvcl_85 )) (flet ($cvcl_145 (and $cvcl_445 $cvcl_436)) (flet ($cvcl_146 (and $cvcl_446 $cvcl_437)) (flet ($cvcl_148 (and $cvcl_447 $cvcl_438)) (flet ($cvcl_149 (and $cvcl_448 $cvcl_439)) (flet ($cvcl_150 (and $cvcl_449 $cvcl_440)) (flet ($cvcl_151 (and $cvcl_450 $cvcl_441)) (flet ($cvcl_152 (and $cvcl_451 $cvcl_442)) (flet ($cvcl_153 (and $cvcl_452 $cvcl_443)) (flet ($cvcl_154 (and $cvcl_453 $cvcl_444)) (flet ($cvcl_543 (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and $cvcl_426 (or (or (or (or (or (or (or (or $cvcl_35 $cvcl_36 ) $cvcl_37 ) $cvcl_38 ) $cvcl_39 ) $cvcl_40 ) $cvcl_41 ) $cvcl_42 ) $cvcl_43 )) (or $cvcl_44 (<= x_63 (+ x_53 3)) )) (or $cvcl_45 (<= x_65 (+ x_53 3)) )) (or $cvcl_50 (<= x_66 (+ x_53 3)) )) (or $cvcl_53 (<= x_67 (+ x_53 3)) )) (or $cvcl_56 (<= x_68 (+ x_53 3)) )) (or $cvcl_59 (<= x_69 (+ x_53 3)) )) (or $cvcl_62 (<= x_70 (+ x_53 3)) )) (or $cvcl_65 (<= x_71 (+ x_53 3)) )) (or $cvcl_68 (<= x_72 (+ x_53 3)) )) (or $cvcl_44 (and (and (and (and (and (and (and (and (or (or $cvcl_546 $cvcl_47 ) (and (= x_74 x_96) (= x_63 (+ x_63 3))) ) (or $cvcl_45 (and (and (or (or $cvcl_46 $cvcl_71 ) (and $cvcl_48 (= x_63 x_65)) ) (or (or $cvcl_47 $cvcl_49 ) $cvcl_48 )) (or (or $cvcl_46 $cvcl_49 ) (and (= x_74 x_97) (= x_63 (+ x_65 3))) )) )) (or $cvcl_50 (and (and (or (or $cvcl_46 $cvcl_73 ) (and $cvcl_51 (= x_63 x_66)) ) (or (or $cvcl_47 $cvcl_52 ) $cvcl_51 )) (or (or $cvcl_46 $cvcl_52 ) (and (= x_74 x_98) (= x_63 (+ x_66 3))) )) )) (or $cvcl_53 (and (and (or (or $cvcl_46 $cvcl_75 ) (and $cvcl_54 (= x_63 x_67)) ) (or (or $cvcl_47 $cvcl_55 ) $cvcl_54 )) (or (or $cvcl_46 $cvcl_55 ) (and (= x_74 x_99) (= x_63 (+ x_67 3))) )) )) (or $cvcl_56 (and (and (or (or $cvcl_46 $cvcl_77 ) (and $cvcl_57 (= x_63 x_68)) ) (or (or $cvcl_47 $cvcl_58 ) $cvcl_57 )) (or (or $cvcl_46 $cvcl_58 ) (and (= x_74 x_100) (= x_63 (+ x_68 3))) )) )) (or $cvcl_59 (and (and (or (or $cvcl_46 $cvcl_79 ) (and $cvcl_60 (= x_63 x_69)) ) (or (or $cvcl_47 $cvcl_61 ) $cvcl_60 )) (or (or $cvcl_46 $cvcl_61 ) (and (= x_74 x_101) (= x_63 (+ x_69 3))) )) )) (or $cvcl_62 (and (and (or (or $cvcl_46 $cvcl_81 ) (and $cvcl_63 (= x_63 x_70)) ) (or (or $cvcl_47 $cvcl_64 ) $cvcl_63 )) (or (or $cvcl_46 $cvcl_64 ) (and (= x_74 x_102) (= x_63 (+ x_70 3))) )) )) (or $cvcl_65 (and (and (or (or $cvcl_46 $cvcl_83 ) (and $cvcl_66 (= x_63 x_71)) ) (or (or $cvcl_47 $cvcl_67 ) $cvcl_66 )) (or (or $cvcl_46 $cvcl_67 ) (and (= x_74 x_103) (= x_63 (+ x_71 3))) )) )) (or $cvcl_68 (and (and (or (or $cvcl_46 $cvcl_85 ) (and $cvcl_69 (= x_63 x_72)) ) (or (or $cvcl_47 $cvcl_70 ) $cvcl_69 )) (or (or $cvcl_46 $cvcl_70 ) (and (= x_74 x_104) (= x_63 (+ x_72 3))) )) )) )) (or $cvcl_45 (and (and (and (and (and (and (and (and (or $cvcl_44 (and (and (or (or $cvcl_71 $cvcl_46 ) (and $cvcl_72 (= x_65 x_63)) ) (or (or $cvcl_49 $cvcl_47 ) $cvcl_72 )) (or (or $cvcl_71 $cvcl_47 ) (and (= x_75 x_96) (= x_65 (+ x_63 3))) )) ) (or (or $cvcl_548 $cvcl_49 ) (and (= x_75 x_97) (= x_65 (+ x_65 3))) )) (or $cvcl_50 (and (and (or (or $cvcl_71 $cvcl_73 ) (and $cvcl_74 (= x_65 x_66)) ) (or (or $cvcl_49 $cvcl_52 ) $cvcl_74 )) (or (or $cvcl_71 $cvcl_52 ) (and (= x_75 x_98) (= x_65 (+ x_66 3))) )) )) (or $cvcl_53 (and (and (or (or $cvcl_71 $cvcl_75 ) (and $cvcl_76 (= x_65 x_67)) ) (or (or $cvcl_49 $cvcl_55 ) $cvcl_76 )) (or (or $cvcl_71 $cvcl_55 ) (and (= x_75 x_99) (= x_65 (+ x_67 3))) )) )) (or $cvcl_56 (and (and (or (or $cvcl_71 $cvcl_77 ) (and $cvcl_78 (= x_65 x_68)) ) (or (or $cvcl_49 $cvcl_58 ) $cvcl_78 )) (or (or $cvcl_71 $cvcl_58 ) (and (= x_75 x_100) (= x_65 (+ x_68 3))) )) )) (or $cvcl_59 (and (and (or (or $cvcl_71 $cvcl_79 ) (and $cvcl_80 (= x_65 x_69)) ) (or (or $cvcl_49 $cvcl_61 ) $cvcl_80 )) (or (or $cvcl_71 $cvcl_61 ) (and (= x_75 x_101) (= x_65 (+ x_69 3))) )) )) (or $cvcl_62 (and (and (or (or $cvcl_71 $cvcl_81 ) (and $cvcl_82 (= x_65 x_70)) ) (or (or $cvcl_49 $cvcl_64 ) $cvcl_82 )) (or (or $cvcl_71 $cvcl_64 ) (and (= x_75 x_102) (= x_65 (+ x_70 3))) )) )) (or $cvcl_65 (and (and (or (or $cvcl_71 $cvcl_83 ) (and $cvcl_84 (= x_65 x_71)) ) (or (or $cvcl_49 $cvcl_67 ) $cvcl_84 )) (or (or $cvcl_71 $cvcl_67 ) (and (= x_75 x_103) (= x_65 (+ x_71 3))) )) )) (or $cvcl_68 (and (and (or (or $cvcl_71 $cvcl_85 ) (and $cvcl_86 (= x_65 x_72)) ) (or (or $cvcl_49 $cvcl_70 ) $cvcl_86 )) (or (or $cvcl_71 $cvcl_70 ) (and (= x_75 x_104) (= x_65 (+ x_72 3))) )) )) )) (or $cvcl_50 (and (and (and (and (and (and (and (and (or $cvcl_44 (and (and (or (or $cvcl_73 $cvcl_46 ) (and $cvcl_87 (= x_66 x_63)) ) (or (or $cvcl_52 $cvcl_47 ) $cvcl_87 )) (or (or $cvcl_73 $cvcl_47 ) (and (= x_76 x_96) (= x_66 (+ x_63 3))) )) ) (or $cvcl_45 (and (and (or (or $cvcl_73 $cvcl_71 ) (and $cvcl_88 (= x_66 x_65)) ) (or (or $cvcl_52 $cvcl_49 ) $cvcl_88 )) (or (or $cvcl_73 $cvcl_49 ) (and (= x_76 x_97) (= x_66 (+ x_65 3))) )) )) (or (or $cvcl_550 $cvcl_52 ) (and (= x_76 x_98) (= x_66 (+ x_66 3))) )) (or $cvcl_53 (and (and (or (or $cvcl_73 $cvcl_75 ) (and $cvcl_89 (= x_66 x_67)) ) (or (or $cvcl_52 $cvcl_55 ) $cvcl_89 )) (or (or $cvcl_73 $cvcl_55 ) (and (= x_76 x_99) (= x_66 (+ x_67 3))) )) )) (or $cvcl_56 (and (and (or (or $cvcl_73 $cvcl_77 ) (and $cvcl_90 (= x_66 x_68)) ) (or (or $cvcl_52 $cvcl_58 ) $cvcl_90 )) (or (or $cvcl_73 $cvcl_58 ) (and (= x_76 x_100) (= x_66 (+ x_68 3))) )) )) (or $cvcl_59 (and (and (or (or $cvcl_73 $cvcl_79 ) (and $cvcl_91 (= x_66 x_69)) ) (or (or $cvcl_52 $cvcl_61 ) $cvcl_91 )) (or (or $cvcl_73 $cvcl_61 ) (and (= x_76 x_101) (= x_66 (+ x_69 3))) )) )) (or $cvcl_62 (and (and (or (or $cvcl_73 $cvcl_81 ) (and $cvcl_92 (= x_66 x_70)) ) (or (or $cvcl_52 $cvcl_64 ) $cvcl_92 )) (or (or $cvcl_73 $cvcl_64 ) (and (= x_76 x_102) (= x_66 (+ x_70 3))) )) )) (or $cvcl_65 (and (and (or (or $cvcl_73 $cvcl_83 ) (and $cvcl_93 (= x_66 x_71)) ) (or (or $cvcl_52 $cvcl_67 ) $cvcl_93 )) (or (or $cvcl_73 $cvcl_67 ) (and (= x_76 x_103) (= x_66 (+ x_71 3))) )) )) (or $cvcl_68 (and (and (or (or $cvcl_73 $cvcl_85 ) (and $cvcl_94 (= x_66 x_72)) ) (or (or $cvcl_52 $cvcl_70 ) $cvcl_94 )) (or (or $cvcl_73 $cvcl_70 ) (and (= x_76 x_104) (= x_66 (+ x_72 3))) )) )) )) (or $cvcl_53 (and (and (and (and (and (and (and (and (or $cvcl_44 (and (and (or (or $cvcl_75 $cvcl_46 ) (and $cvcl_95 (= x_67 x_63)) ) (or (or $cvcl_55 $cvcl_47 ) $cvcl_95 )) (or (or $cvcl_75 $cvcl_47 ) (and (= x_77 x_96) (= x_67 (+ x_63 3))) )) ) (or $cvcl_45 (and (and (or (or $cvcl_75 $cvcl_71 ) (and $cvcl_96 (= x_67 x_65)) ) (or (or $cvcl_55 $cvcl_49 ) $cvcl_96 )) (or (or $cvcl_75 $cvcl_49 ) (and (= x_77 x_97) (= x_67 (+ x_65 3))) )) )) (or $cvcl_50 (and (and (or (or $cvcl_75 $cvcl_73 ) (and $cvcl_97 (= x_67 x_66)) ) (or (or $cvcl_55 $cvcl_52 ) $cvcl_97 )) (or (or $cvcl_75 $cvcl_52 ) (and (= x_77 x_98) (= x_67 (+ x_66 3))) )) )) (or (or $cvcl_552 $cvcl_55 ) (and (= x_77 x_99) (= x_67 (+ x_67 3))) )) (or $cvcl_56 (and (and (or (or $cvcl_75 $cvcl_77 ) (and $cvcl_98 (= x_67 x_68)) ) (or (or $cvcl_55 $cvcl_58 ) $cvcl_98 )) (or (or $cvcl_75 $cvcl_58 ) (and (= x_77 x_100) (= x_67 (+ x_68 3))) )) )) (or $cvcl_59 (and (and (or (or $cvcl_75 $cvcl_79 ) (and $cvcl_99 (= x_67 x_69)) ) (or (or $cvcl_55 $cvcl_61 ) $cvcl_99 )) (or (or $cvcl_75 $cvcl_61 ) (and (= x_77 x_101) (= x_67 (+ x_69 3))) )) )) (or $cvcl_62 (and (and (or (or $cvcl_75 $cvcl_81 ) (and $cvcl_100 (= x_67 x_70)) ) (or (or $cvcl_55 $cvcl_64 ) $cvcl_100 )) (or (or $cvcl_75 $cvcl_64 ) (and (= x_77 x_102) (= x_67 (+ x_70 3))) )) )) (or $cvcl_65 (and (and (or (or $cvcl_75 $cvcl_83 ) (and $cvcl_101 (= x_67 x_71)) ) (or (or $cvcl_55 $cvcl_67 ) $cvcl_101 )) (or (or $cvcl_75 $cvcl_67 ) (and (= x_77 x_103) (= x_67 (+ x_71 3))) )) )) (or $cvcl_68 (and (and (or (or $cvcl_75 $cvcl_85 ) (and $cvcl_102 (= x_67 x_72)) ) (or (or $cvcl_55 $cvcl_70 ) $cvcl_102 )) (or (or $cvcl_75 $cvcl_70 ) (and (= x_77 x_104) (= x_67 (+ x_72 3))) )) )) )) (or $cvcl_56 (and (and (and (and (and (and (and (and (or $cvcl_44 (and (and (or (or $cvcl_77 $cvcl_46 ) (and $cvcl_103 (= x_68 x_63)) ) (or (or $cvcl_58 $cvcl_47 ) $cvcl_103 )) (or (or $cvcl_77 $cvcl_47 ) (and (= x_78 x_96) (= x_68 (+ x_63 3))) )) ) (or $cvcl_45 (and (and (or (or $cvcl_77 $cvcl_71 ) (and $cvcl_104 (= x_68 x_65)) ) (or (or $cvcl_58 $cvcl_49 ) $cvcl_104 )) (or (or $cvcl_77 $cvcl_49 ) (and (= x_78 x_97) (= x_68 (+ x_65 3))) )) )) (or $cvcl_50 (and (and (or (or $cvcl_77 $cvcl_73 ) (and $cvcl_105 (= x_68 x_66)) ) (or (or $cvcl_58 $cvcl_52 ) $cvcl_105 )) (or (or $cvcl_77 $cvcl_52 ) (and (= x_78 x_98) (= x_68 (+ x_66 3))) )) )) (or $cvcl_53 (and (and (or (or $cvcl_77 $cvcl_75 ) (and $cvcl_106 (= x_68 x_67)) ) (or (or $cvcl_58 $cvcl_55 ) $cvcl_106 )) (or (or $cvcl_77 $cvcl_55 ) (and (= x_78 x_99) (= x_68 (+ x_67 3))) )) )) (or (or $cvcl_554 $cvcl_58 ) (and (= x_78 x_100) (= x_68 (+ x_68 3))) )) (or $cvcl_59 (and (and (or (or $cvcl_77 $cvcl_79 ) (and $cvcl_107 (= x_68 x_69)) ) (or (or $cvcl_58 $cvcl_61 ) $cvcl_107 )) (or (or $cvcl_77 $cvcl_61 ) (and (= x_78 x_101) (= x_68 (+ x_69 3))) )) )) (or $cvcl_62 (and (and (or (or $cvcl_77 $cvcl_81 ) (and $cvcl_108 (= x_68 x_70)) ) (or (or $cvcl_58 $cvcl_64 ) $cvcl_108 )) (or (or $cvcl_77 $cvcl_64 ) (and (= x_78 x_102) (= x_68 (+ x_70 3))) )) )) (or $cvcl_65 (and (and (or (or $cvcl_77 $cvcl_83 ) (and $cvcl_109 (= x_68 x_71)) ) (or (or $cvcl_58 $cvcl_67 ) $cvcl_109 )) (or (or $cvcl_77 $cvcl_67 ) (and (= x_78 x_103) (= x_68 (+ x_71 3))) )) )) (or $cvcl_68 (and (and (or (or $cvcl_77 $cvcl_85 ) (and $cvcl_110 (= x_68 x_72)) ) (or (or $cvcl_58 $cvcl_70 ) $cvcl_110 )) (or (or $cvcl_77 $cvcl_70 ) (and (= x_78 x_104) (= x_68 (+ x_72 3))) )) )) )) (or $cvcl_59 (and (and (and (and (and (and (and (and (or $cvcl_44 (and (and (or (or $cvcl_79 $cvcl_46 ) (and $cvcl_111 (= x_69 x_63)) ) (or (or $cvcl_61 $cvcl_47 ) $cvcl_111 )) (or (or $cvcl_79 $cvcl_47 ) (and (= x_79 x_96) (= x_69 (+ x_63 3))) )) ) (or $cvcl_45 (and (and (or (or $cvcl_79 $cvcl_71 ) (and $cvcl_112 (= x_69 x_65)) ) (or (or $cvcl_61 $cvcl_49 ) $cvcl_112 )) (or (or $cvcl_79 $cvcl_49 ) (and (= x_79 x_97) (= x_69 (+ x_65 3))) )) )) (or $cvcl_50 (and (and (or (or $cvcl_79 $cvcl_73 ) (and $cvcl_113 (= x_69 x_66)) ) (or (or $cvcl_61 $cvcl_52 ) $cvcl_113 )) (or (or $cvcl_79 $cvcl_52 ) (and (= x_79 x_98) (= x_69 (+ x_66 3))) )) )) (or $cvcl_53 (and (and (or (or $cvcl_79 $cvcl_75 ) (and $cvcl_114 (= x_69 x_67)) ) (or (or $cvcl_61 $cvcl_55 ) $cvcl_114 )) (or (or $cvcl_79 $cvcl_55 ) (and (= x_79 x_99) (= x_69 (+ x_67 3))) )) )) (or $cvcl_56 (and (and (or (or $cvcl_79 $cvcl_77 ) (and $cvcl_115 (= x_69 x_68)) ) (or (or $cvcl_61 $cvcl_58 ) $cvcl_115 )) (or (or $cvcl_79 $cvcl_58 ) (and (= x_79 x_100) (= x_69 (+ x_68 3))) )) )) (or (or $cvcl_556 $cvcl_61 ) (and (= x_79 x_101) (= x_69 (+ x_69 3))) )) (or $cvcl_62 (and (and (or (or $cvcl_79 $cvcl_81 ) (and $cvcl_116 (= x_69 x_70)) ) (or (or $cvcl_61 $cvcl_64 ) $cvcl_116 )) (or (or $cvcl_79 $cvcl_64 ) (and (= x_79 x_102) (= x_69 (+ x_70 3))) )) )) (or $cvcl_65 (and (and (or (or $cvcl_79 $cvcl_83 ) (and $cvcl_117 (= x_69 x_71)) ) (or (or $cvcl_61 $cvcl_67 ) $cvcl_117 )) (or (or $cvcl_79 $cvcl_67 ) (and (= x_79 x_103) (= x_69 (+ x_71 3))) )) )) (or $cvcl_68 (and (and (or (or $cvcl_79 $cvcl_85 ) (and $cvcl_118 (= x_69 x_72)) ) (or (or $cvcl_61 $cvcl_70 ) $cvcl_118 )) (or (or $cvcl_79 $cvcl_70 ) (and (= x_79 x_104) (= x_69 (+ x_72 3))) )) )) )) (or $cvcl_62 (and (and (and (and (and (and (and (and (or $cvcl_44 (and (and (or (or $cvcl_81 $cvcl_46 ) (and $cvcl_119 (= x_70 x_63)) ) (or (or $cvcl_64 $cvcl_47 ) $cvcl_119 )) (or (or $cvcl_81 $cvcl_47 ) (and (= x_80 x_96) (= x_70 (+ x_63 3))) )) ) (or $cvcl_45 (and (and (or (or $cvcl_81 $cvcl_71 ) (and $cvcl_120 (= x_70 x_65)) ) (or (or $cvcl_64 $cvcl_49 ) $cvcl_120 )) (or (or $cvcl_81 $cvcl_49 ) (and (= x_80 x_97) (= x_70 (+ x_65 3))) )) )) (or $cvcl_50 (and (and (or (or $cvcl_81 $cvcl_73 ) (and $cvcl_121 (= x_70 x_66)) ) (or (or $cvcl_64 $cvcl_52 ) $cvcl_121 )) (or (or $cvcl_81 $cvcl_52 ) (and (= x_80 x_98) (= x_70 (+ x_66 3))) )) )) (or $cvcl_53 (and (and (or (or $cvcl_81 $cvcl_75 ) (and $cvcl_122 (= x_70 x_67)) ) (or (or $cvcl_64 $cvcl_55 ) $cvcl_122 )) (or (or $cvcl_81 $cvcl_55 ) (and (= x_80 x_99) (= x_70 (+ x_67 3))) )) )) (or $cvcl_56 (and (and (or (or $cvcl_81 $cvcl_77 ) (and $cvcl_123 (= x_70 x_68)) ) (or (or $cvcl_64 $cvcl_58 ) $cvcl_123 )) (or (or $cvcl_81 $cvcl_58 ) (and (= x_80 x_100) (= x_70 (+ x_68 3))) )) )) (or $cvcl_59 (and (and (or (or $cvcl_81 $cvcl_79 ) (and $cvcl_124 (= x_70 x_69)) ) (or (or $cvcl_64 $cvcl_61 ) $cvcl_124 )) (or (or $cvcl_81 $cvcl_61 ) (and (= x_80 x_101) (= x_70 (+ x_69 3))) )) )) (or (or $cvcl_558 $cvcl_64 ) (and (= x_80 x_102) (= x_70 (+ x_70 3))) )) (or $cvcl_65 (and (and (or (or $cvcl_81 $cvcl_83 ) (and $cvcl_125 (= x_70 x_71)) ) (or (or $cvcl_64 $cvcl_67 ) $cvcl_125 )) (or (or $cvcl_81 $cvcl_67 ) (and (= x_80 x_103) (= x_70 (+ x_71 3))) )) )) (or $cvcl_68 (and (and (or (or $cvcl_81 $cvcl_85 ) (and $cvcl_126 (= x_70 x_72)) ) (or (or $cvcl_64 $cvcl_70 ) $cvcl_126 )) (or (or $cvcl_81 $cvcl_70 ) (and (= x_80 x_104) (= x_70 (+ x_72 3))) )) )) )) (or $cvcl_65 (and (and (and (and (and (and (and (and (or $cvcl_44 (and (and (or (or $cvcl_83 $cvcl_46 ) (and $cvcl_127 (= x_71 x_63)) ) (or (or $cvcl_67 $cvcl_47 ) $cvcl_127 )) (or (or $cvcl_83 $cvcl_47 ) (and (= x_81 x_96) (= x_71 (+ x_63 3))) )) ) (or $cvcl_45 (and (and (or (or $cvcl_83 $cvcl_71 ) (and $cvcl_128 (= x_71 x_65)) ) (or (or $cvcl_67 $cvcl_49 ) $cvcl_128 )) (or (or $cvcl_83 $cvcl_49 ) (and (= x_81 x_97) (= x_71 (+ x_65 3))) )) )) (or $cvcl_50 (and (and (or (or $cvcl_83 $cvcl_73 ) (and $cvcl_129 (= x_71 x_66)) ) (or (or $cvcl_67 $cvcl_52 ) $cvcl_129 )) (or (or $cvcl_83 $cvcl_52 ) (and (= x_81 x_98) (= x_71 (+ x_66 3))) )) )) (or $cvcl_53 (and (and (or (or $cvcl_83 $cvcl_75 ) (and $cvcl_130 (= x_71 x_67)) ) (or (or $cvcl_67 $cvcl_55 ) $cvcl_130 )) (or (or $cvcl_83 $cvcl_55 ) (and (= x_81 x_99) (= x_71 (+ x_67 3))) )) )) (or $cvcl_56 (and (and (or (or $cvcl_83 $cvcl_77 ) (and $cvcl_131 (= x_71 x_68)) ) (or (or $cvcl_67 $cvcl_58 ) $cvcl_131 )) (or (or $cvcl_83 $cvcl_58 ) (and (= x_81 x_100) (= x_71 (+ x_68 3))) )) )) (or $cvcl_59 (and (and (or (or $cvcl_83 $cvcl_79 ) (and $cvcl_132 (= x_71 x_69)) ) (or (or $cvcl_67 $cvcl_61 ) $cvcl_132 )) (or (or $cvcl_83 $cvcl_61 ) (and (= x_81 x_101) (= x_71 (+ x_69 3))) )) )) (or $cvcl_62 (and (and (or (or $cvcl_83 $cvcl_81 ) (and $cvcl_133 (= x_71 x_70)) ) (or (or $cvcl_67 $cvcl_64 ) $cvcl_133 )) (or (or $cvcl_83 $cvcl_64 ) (and (= x_81 x_102) (= x_71 (+ x_70 3))) )) )) (or (or $cvcl_560 $cvcl_67 ) (and (= x_81 x_103) (= x_71 (+ x_71 3))) )) (or $cvcl_68 (and (and (or (or $cvcl_83 $cvcl_85 ) (and $cvcl_134 (= x_71 x_72)) ) (or (or $cvcl_67 $cvcl_70 ) $cvcl_134 )) (or (or $cvcl_83 $cvcl_70 ) (and (= x_81 x_104) (= x_71 (+ x_72 3))) )) )) )) (or $cvcl_68 (and (and (and (and (and (and (and (and (or $cvcl_44 (and (and (or (or $cvcl_85 $cvcl_46 ) (and $cvcl_135 (= x_72 x_63)) ) (or (or $cvcl_70 $cvcl_47 ) $cvcl_135 )) (or (or $cvcl_85 $cvcl_47 ) (and (= x_82 x_96) (= x_72 (+ x_63 3))) )) ) (or $cvcl_45 (and (and (or (or $cvcl_85 $cvcl_71 ) (and $cvcl_136 (= x_72 x_65)) ) (or (or $cvcl_70 $cvcl_49 ) $cvcl_136 )) (or (or $cvcl_85 $cvcl_49 ) (and (= x_82 x_97) (= x_72 (+ x_65 3))) )) )) (or $cvcl_50 (and (and (or (or $cvcl_85 $cvcl_73 ) (and $cvcl_137 (= x_72 x_66)) ) (or (or $cvcl_70 $cvcl_52 ) $cvcl_137 )) (or (or $cvcl_85 $cvcl_52 ) (and (= x_82 x_98) (= x_72 (+ x_66 3))) )) )) (or $cvcl_53 (and (and (or (or $cvcl_85 $cvcl_75 ) (and $cvcl_138 (= x_72 x_67)) ) (or (or $cvcl_70 $cvcl_55 ) $cvcl_138 )) (or (or $cvcl_85 $cvcl_55 ) (and (= x_82 x_99) (= x_72 (+ x_67 3))) )) )) (or $cvcl_56 (and (and (or (or $cvcl_85 $cvcl_77 ) (and $cvcl_139 (= x_72 x_68)) ) (or (or $cvcl_70 $cvcl_58 ) $cvcl_139 )) (or (or $cvcl_85 $cvcl_58 ) (and (= x_82 x_100) (= x_72 (+ x_68 3))) )) )) (or $cvcl_59 (and (and (or (or $cvcl_85 $cvcl_79 ) (and $cvcl_140 (= x_72 x_69)) ) (or (or $cvcl_70 $cvcl_61 ) $cvcl_140 )) (or (or $cvcl_85 $cvcl_61 ) (and (= x_82 x_101) (= x_72 (+ x_69 3))) )) )) (or $cvcl_62 (and (and (or (or $cvcl_85 $cvcl_81 ) (and $cvcl_141 (= x_72 x_70)) ) (or (or $cvcl_70 $cvcl_64 ) $cvcl_141 )) (or (or $cvcl_85 $cvcl_64 ) (and (= x_82 x_102) (= x_72 (+ x_70 3))) )) )) (or $cvcl_65 (and (and (or (or $cvcl_85 $cvcl_83 ) (and $cvcl_142 (= x_72 x_71)) ) (or (or $cvcl_70 $cvcl_67 ) $cvcl_142 )) (or (or $cvcl_85 $cvcl_67 ) (and (= x_82 x_103) (= x_72 (+ x_71 3))) )) )) (or (or $cvcl_562 $cvcl_70 ) (and (= x_82 x_104) (= x_72 (+ x_72 3))) )) )) (or $cvcl_44 (and (and (and (and (and (and (and (and (or $cvcl_145 (not (<= x_63 (+ (+ x_63 (* ?cvcl_144 3)) x_32))) ) (or $cvcl_146 (not (<= x_65 (+ (+ x_63 (* ?cvcl_144 3)) x_32))) )) (or $cvcl_148 (not (<= x_66 (+ (+ x_63 (* ?cvcl_144 3)) x_32))) )) (or $cvcl_149 (not (<= x_67 (+ (+ x_63 (* ?cvcl_144 3)) x_32))) )) (or $cvcl_150 (not (<= x_68 (+ (+ x_63 (* ?cvcl_144 3)) x_32))) )) (or $cvcl_151 (not (<= x_69 (+ (+ x_63 (* ?cvcl_144 3)) x_32))) )) (or $cvcl_152 (not (<= x_70 (+ (+ x_63 (* ?cvcl_144 3)) x_32))) )) (or $cvcl_153 (not (<= x_71 (+ (+ x_63 (* ?cvcl_144 3)) x_32))) )) (or $cvcl_154 (not (<= x_72 (+ (+ x_63 (* ?cvcl_144 3)) x_32))) )) )) (or $cvcl_45 (and (and (and (and (and (and (and (and (or $cvcl_145 (not (<= x_63 (+ (+ x_65 (* ?cvcl_147 3)) x_32))) ) (or $cvcl_146 (not (<= x_65 (+ (+ x_65 (* ?cvcl_147 3)) x_32))) )) (or $cvcl_148 (not (<= x_66 (+ (+ x_65 (* ?cvcl_147 3)) x_32))) )) (or $cvcl_149 (not (<= x_67 (+ (+ x_65 (* ?cvcl_147 3)) x_32))) )) (or $cvcl_150 (not (<= x_68 (+ (+ x_65 (* ?cvcl_147 3)) x_32))) )) (or $cvcl_151 (not (<= x_69 (+ (+ x_65 (* ?cvcl_147 3)) x_32))) )) (or $cvcl_152 (not (<= x_70 (+ (+ x_65 (* ?cvcl_147 3)) x_32))) )) (or $cvcl_153 (not (<= x_71 (+ (+ x_65 (* ?cvcl_147 3)) x_32))) )) (or $cvcl_154 (not (<= x_72 (+ (+ x_65 (* ?cvcl_147 3)) x_32))) )) )) (or $cvcl_50 (and (and (and (and (and (and (and (and (or $cvcl_145 (not (<= x_63 (+ (+ x_66 (* ?cvcl_155 3)) x_32))) ) (or $cvcl_146 (not (<= x_65 (+ (+ x_66 (* ?cvcl_155 3)) x_32))) )) (or $cvcl_148 (not (<= x_66 (+ (+ x_66 (* ?cvcl_155 3)) x_32))) )) (or $cvcl_149 (not (<= x_67 (+ (+ x_66 (* ?cvcl_155 3)) x_32))) )) (or $cvcl_150 (not (<= x_68 (+ (+ x_66 (* ?cvcl_155 3)) x_32))) )) (or $cvcl_151 (not (<= x_69 (+ (+ x_66 (* ?cvcl_155 3)) x_32))) )) (or $cvcl_152 (not (<= x_70 (+ (+ x_66 (* ?cvcl_155 3)) x_32))) )) (or $cvcl_153 (not (<= x_71 (+ (+ x_66 (* ?cvcl_155 3)) x_32))) )) (or $cvcl_154 (not (<= x_72 (+ (+ x_66 (* ?cvcl_155 3)) x_32))) )) )) (or $cvcl_53 (and (and (and (and (and (and (and (and (or $cvcl_145 (not (<= x_63 (+ (+ x_67 (* ?cvcl_156 3)) x_32))) ) (or $cvcl_146 (not (<= x_65 (+ (+ x_67 (* ?cvcl_156 3)) x_32))) )) (or $cvcl_148 (not (<= x_66 (+ (+ x_67 (* ?cvcl_156 3)) x_32))) )) (or $cvcl_149 (not (<= x_67 (+ (+ x_67 (* ?cvcl_156 3)) x_32))) )) (or $cvcl_150 (not (<= x_68 (+ (+ x_67 (* ?cvcl_156 3)) x_32))) )) (or $cvcl_151 (not (<= x_69 (+ (+ x_67 (* ?cvcl_156 3)) x_32))) )) (or $cvcl_152 (not (<= x_70 (+ (+ x_67 (* ?cvcl_156 3)) x_32))) )) (or $cvcl_153 (not (<= x_71 (+ (+ x_67 (* ?cvcl_156 3)) x_32))) )) (or $cvcl_154 (not (<= x_72 (+ (+ x_67 (* ?cvcl_156 3)) x_32))) )) )) (or $cvcl_56 (and (and (and (and (and (and (and (and (or $cvcl_145 (not (<= x_63 (+ (+ x_68 (* ?cvcl_157 3)) x_32))) ) (or $cvcl_146 (not (<= x_65 (+ (+ x_68 (* ?cvcl_157 3)) x_32))) )) (or $cvcl_148 (not (<= x_66 (+ (+ x_68 (* ?cvcl_157 3)) x_32))) )) (or $cvcl_149 (not (<= x_67 (+ (+ x_68 (* ?cvcl_157 3)) x_32))) )) (or $cvcl_150 (not (<= x_68 (+ (+ x_68 (* ?cvcl_157 3)) x_32))) )) (or $cvcl_151 (not (<= x_69 (+ (+ x_68 (* ?cvcl_157 3)) x_32))) )) (or $cvcl_152 (not (<= x_70 (+ (+ x_68 (* ?cvcl_157 3)) x_32))) )) (or $cvcl_153 (not (<= x_71 (+ (+ x_68 (* ?cvcl_157 3)) x_32))) )) (or $cvcl_154 (not (<= x_72 (+ (+ x_68 (* ?cvcl_157 3)) x_32))) )) )) (or $cvcl_59 (and (and (and (and (and (and (and (and (or $cvcl_145 (not (<= x_63 (+ (+ x_69 (* ?cvcl_158 3)) x_32))) ) (or $cvcl_146 (not (<= x_65 (+ (+ x_69 (* ?cvcl_158 3)) x_32))) )) (or $cvcl_148 (not (<= x_66 (+ (+ x_69 (* ?cvcl_158 3)) x_32))) )) (or $cvcl_149 (not (<= x_67 (+ (+ x_69 (* ?cvcl_158 3)) x_32))) )) (or $cvcl_150 (not (<= x_68 (+ (+ x_69 (* ?cvcl_158 3)) x_32))) )) (or $cvcl_151 (not (<= x_69 (+ (+ x_69 (* ?cvcl_158 3)) x_32))) )) (or $cvcl_152 (not (<= x_70 (+ (+ x_69 (* ?cvcl_158 3)) x_32))) )) (or $cvcl_153 (not (<= x_71 (+ (+ x_69 (* ?cvcl_158 3)) x_32))) )) (or $cvcl_154 (not (<= x_72 (+ (+ x_69 (* ?cvcl_158 3)) x_32))) )) )) (or $cvcl_62 (and (and (and (and (and (and (and (and (or $cvcl_145 (not (<= x_63 (+ (+ x_70 (* ?cvcl_159 3)) x_32))) ) (or $cvcl_146 (not (<= x_65 (+ (+ x_70 (* ?cvcl_159 3)) x_32))) )) (or $cvcl_148 (not (<= x_66 (+ (+ x_70 (* ?cvcl_159 3)) x_32))) )) (or $cvcl_149 (not (<= x_67 (+ (+ x_70 (* ?cvcl_159 3)) x_32))) )) (or $cvcl_150 (not (<= x_68 (+ (+ x_70 (* ?cvcl_159 3)) x_32))) )) (or $cvcl_151 (not (<= x_69 (+ (+ x_70 (* ?cvcl_159 3)) x_32))) )) (or $cvcl_152 (not (<= x_70 (+ (+ x_70 (* ?cvcl_159 3)) x_32))) )) (or $cvcl_153 (not (<= x_71 (+ (+ x_70 (* ?cvcl_159 3)) x_32))) )) (or $cvcl_154 (not (<= x_72 (+ (+ x_70 (* ?cvcl_159 3)) x_32))) )) )) (or $cvcl_65 (and (and (and (and (and (and (and (and (or $cvcl_145 (not (<= x_63 (+ (+ x_71 (* ?cvcl_160 3)) x_32))) ) (or $cvcl_146 (not (<= x_65 (+ (+ x_71 (* ?cvcl_160 3)) x_32))) )) (or $cvcl_148 (not (<= x_66 (+ (+ x_71 (* ?cvcl_160 3)) x_32))) )) (or $cvcl_149 (not (<= x_67 (+ (+ x_71 (* ?cvcl_160 3)) x_32))) )) (or $cvcl_150 (not (<= x_68 (+ (+ x_71 (* ?cvcl_160 3)) x_32))) )) (or $cvcl_151 (not (<= x_69 (+ (+ x_71 (* ?cvcl_160 3)) x_32))) )) (or $cvcl_152 (not (<= x_70 (+ (+ x_71 (* ?cvcl_160 3)) x_32))) )) (or $cvcl_153 (not (<= x_71 (+ (+ x_71 (* ?cvcl_160 3)) x_32))) )) (or $cvcl_154 (not (<= x_72 (+ (+ x_71 (* ?cvcl_160 3)) x_32))) )) )) (or $cvcl_68 (and (and (and (and (and (and (and (and (or $cvcl_145 (not (<= x_63 (+ (+ x_72 (* ?cvcl_161 3)) x_32))) ) (or $cvcl_146 (not (<= x_65 (+ (+ x_72 (* ?cvcl_161 3)) x_32))) )) (or $cvcl_148 (not (<= x_66 (+ (+ x_72 (* ?cvcl_161 3)) x_32))) )) (or $cvcl_149 (not (<= x_67 (+ (+ x_72 (* ?cvcl_161 3)) x_32))) )) (or $cvcl_150 (not (<= x_68 (+ (+ x_72 (* ?cvcl_161 3)) x_32))) )) (or $cvcl_151 (not (<= x_69 (+ (+ x_72 (* ?cvcl_161 3)) x_32))) )) (or $cvcl_152 (not (<= x_70 (+ (+ x_72 (* ?cvcl_161 3)) x_32))) )) (or $cvcl_153 (not (<= x_71 (+ (+ x_72 (* ?cvcl_161 3)) x_32))) )) (or $cvcl_154 (not (<= x_72 (+ (+ x_72 (* ?cvcl_161 3)) x_32))) )) ))) (flet ($cvcl_189 (and (and (and (and (and (and (and (and $cvcl_180 $cvcl_181) $cvcl_182) $cvcl_183) $cvcl_184) $cvcl_185) $cvcl_186) $cvcl_187) $cvcl_188)) (flet ($cvcl_191 (and (and (and (and (and (and (and (and (<= x_53 x_9) (<= x_53 x_10)) (<= x_53 x_11)) (<= x_53 x_12)) (<= x_53 x_13)) (<= x_53 x_14)) (<= x_53 x_15)) (<= x_53 x_16)) (<= x_53 x_17))) (flet ($cvcl_424 (= x_53 0)) (flet ($cvcl_205 (and (= x_73 x_18) (= x_87 0))) (flet ($cvcl_272 (and $cvcl_205 (iff x_86 x_19))) (flet ($cvcl_293 (and $cvcl_272 $cvcl_206)) (flet ($cvcl_312 (and $cvcl_293 $cvcl_207)) (flet ($cvcl_331 (and $cvcl_312 $cvcl_208)) (flet ($cvcl_350 (and $cvcl_331 $cvcl_209)) (flet ($cvcl_369 (and $cvcl_350 $cvcl_210)) (flet ($cvcl_388 (and $cvcl_369 $cvcl_211)) (flet ($cvcl_407 (and $cvcl_388 $cvcl_212)) (flet ($cvcl_215 (= x_64 0)) (flet ($cvcl_203 (and (and (and $cvcl_407 $cvcl_213) $cvcl_214) $cvcl_215)) (flet ($cvcl_218 (= 0 x_9)) (flet ($cvcl_222 (= 0 0)) (flet ($cvcl_223 (and (and (and (and (and (and (and (and (and (and (and $cvcl_205 $cvcl_220) $cvcl_206) $cvcl_207) $cvcl_208) $cvcl_209) $cvcl_210) $cvcl_211) $cvcl_212) $cvcl_213) $cvcl_214) $cvcl_215)) (flet ($cvcl_226 (= x_63 (+ 0 27))) (flet ($cvcl_233 (= x_87 (ite $cvcl_190 (+ 0 x_32) 0))) (flet ($cvcl_275 (and (= x_73 (ite $cvcl_190 0 x_18)) $cvcl_233)) (flet ($cvcl_235 (iff x_88 (or $cvcl_190 x_20 ))) (flet ($cvcl_236 (iff x_89 (or $cvcl_190 x_21 ))) (flet ($cvcl_237 (iff x_90 (or $cvcl_190 x_22 ))) (flet ($cvcl_238 (iff x_91 (or $cvcl_190 x_23 ))) (flet ($cvcl_239 (iff x_92 (or $cvcl_190 x_24 ))) (flet ($cvcl_240 (iff x_93 (or $cvcl_190 x_25 ))) (flet ($cvcl_241 (iff x_94 (or $cvcl_190 x_26 ))) (flet ($cvcl_242 (iff x_95 (or $cvcl_190 x_27 ))) (flet ($cvcl_243 (= x_84 (ite $cvcl_190 1 x_28))) (flet ($cvcl_244 (= x_64 (ite $cvcl_190 0 0))) (flet ($cvcl_227 (and (and (and (and (and (and (and (and (and (and (and $cvcl_275 $cvcl_220) $cvcl_235) $cvcl_236) $cvcl_237) $cvcl_238) $cvcl_239) $cvcl_240) $cvcl_241) $cvcl_242) $cvcl_243) $cvcl_244)) (flet ($cvcl_229 (= x_63 (- (+ 0 3) x_32))) (flet ($cvcl_231 (and $cvcl_245 $cvcl_218)) (flet ($cvcl_232 (= x_63 (+ 0 3))) (flet ($cvcl_286 (= x_73 (ite $cvcl_190 1 x_18))) (flet ($cvcl_273 (= 0 x_10)) (flet ($cvcl_278 (and (and (and (and (and (and (and (and (and (and $cvcl_272 $cvcl_276) $cvcl_207) $cvcl_208) $cvcl_209) $cvcl_210) $cvcl_211) $cvcl_212) $cvcl_213) $cvcl_214) $cvcl_215)) (flet ($cvcl_280 (= x_65 (+ 0 30))) (flet ($cvcl_287 (iff x_86 (or $cvcl_190 x_19 ))) (flet ($cvcl_296 (and $cvcl_275 $cvcl_287)) (flet ($cvcl_289 (= x_84 (ite $cvcl_190 2 x_28))) (flet ($cvcl_281 (and (and (and (and (and (and (and (and (and (and $cvcl_296 $cvcl_276) $cvcl_236) $cvcl_237) $cvcl_238) $cvcl_239) $cvcl_240) $cvcl_241) $cvcl_242) $cvcl_289) $cvcl_244)) (flet ($cvcl_282 (= x_65 (- (+ 0 3) x_32))) (flet ($cvcl_284 (and $cvcl_290 $cvcl_273)) (flet ($cvcl_285 (= x_65 (+ 0 3))) (flet ($cvcl_294 (= 0 x_11)) (flet ($cvcl_299 (and (and (and (and (and (and (and (and (and $cvcl_293 $cvcl_297) $cvcl_208) $cvcl_209) $cvcl_210) $cvcl_211) $cvcl_212) $cvcl_213) $cvcl_214) $cvcl_215)) (flet ($cvcl_301 (= x_66 (+ 0 33))) (flet ($cvcl_315 (and $cvcl_296 $cvcl_235)) (flet ($cvcl_308 (= x_84 (ite $cvcl_190 3 x_28))) (flet ($cvcl_302 (and (and (and (and (and (and (and (and (and $cvcl_315 $cvcl_297) $cvcl_237) $cvcl_238) $cvcl_239) $cvcl_240) $cvcl_241) $cvcl_242) $cvcl_308) $cvcl_244)) (flet ($cvcl_303 (= x_66 (- (+ 0 3) x_32))) (flet ($cvcl_305 (and $cvcl_309 $cvcl_294)) (flet ($cvcl_306 (= x_66 (+ 0 3))) (flet ($cvcl_313 (= 0 x_12)) (flet ($cvcl_318 (and (and (and (and (and (and (and (and $cvcl_312 $cvcl_316) $cvcl_209) $cvcl_210) $cvcl_211) $cvcl_212) $cvcl_213) $cvcl_214) $cvcl_215)) (flet ($cvcl_320 (= x_67 (+ 0 36))) (flet ($cvcl_334 (and $cvcl_315 $cvcl_236)) (flet ($cvcl_327 (= x_84 (ite $cvcl_190 4 x_28))) (flet ($cvcl_321 (and (and (and (and (and (and (and (and $cvcl_334 $cvcl_316) $cvcl_238) $cvcl_239) $cvcl_240) $cvcl_241) $cvcl_242) $cvcl_327) $cvcl_244)) (flet ($cvcl_322 (= x_67 (- (+ 0 3) x_32))) (flet ($cvcl_324 (and $cvcl_328 $cvcl_313)) (flet ($cvcl_325 (= x_67 (+ 0 3))) (flet ($cvcl_332 (= 0 x_13)) (flet ($cvcl_337 (and (and (and (and (and (and (and $cvcl_331 $cvcl_335) $cvcl_210) $cvcl_211) $cvcl_212) $cvcl_213) $cvcl_214) $cvcl_215)) (flet ($cvcl_339 (= x_68 (+ 0 39))) (flet ($cvcl_353 (and $cvcl_334 $cvcl_237)) (flet ($cvcl_346 (= x_84 (ite $cvcl_190 5 x_28))) (flet ($cvcl_340 (and (and (and (and (and (and (and $cvcl_353 $cvcl_335) $cvcl_239) $cvcl_240) $cvcl_241) $cvcl_242) $cvcl_346) $cvcl_244)) (flet ($cvcl_341 (= x_68 (- (+ 0 3) x_32))) (flet ($cvcl_343 (and $cvcl_347 $cvcl_332)) (flet ($cvcl_344 (= x_68 (+ 0 3))) (flet ($cvcl_351 (= 0 x_14)) (flet ($cvcl_356 (and (and (and (and (and (and $cvcl_350 $cvcl_354) $cvcl_211) $cvcl_212) $cvcl_213) $cvcl_214) $cvcl_215)) (flet ($cvcl_358 (= x_69 (+ 0 42))) (flet ($cvcl_372 (and $cvcl_353 $cvcl_238)) (flet ($cvcl_365 (= x_84 (ite $cvcl_190 6 x_28))) (flet ($cvcl_359 (and (and (and (and (and (and $cvcl_372 $cvcl_354) $cvcl_240) $cvcl_241) $cvcl_242) $cvcl_365) $cvcl_244)) (flet ($cvcl_360 (= x_69 (- (+ 0 3) x_32))) (flet ($cvcl_362 (and $cvcl_366 $cvcl_351)) (flet ($cvcl_363 (= x_69 (+ 0 3))) (flet ($cvcl_370 (= 0 x_15)) (flet ($cvcl_375 (and (and (and (and (and $cvcl_369 $cvcl_373) $cvcl_212) $cvcl_213) $cvcl_214) $cvcl_215)) (flet ($cvcl_377 (= x_70 (+ 0 45))) (flet ($cvcl_391 (and $cvcl_372 $cvcl_239)) (flet ($cvcl_384 (= x_84 (ite $cvcl_190 7 x_28))) (flet ($cvcl_378 (and (and (and (and (and $cvcl_391 $cvcl_373) $cvcl_241) $cvcl_242) $cvcl_384) $cvcl_244)) (flet ($cvcl_379 (= x_70 (- (+ 0 3) x_32))) (flet ($cvcl_381 (and $cvcl_385 $cvcl_370)) (flet ($cvcl_382 (= x_70 (+ 0 3))) (flet ($cvcl_389 (= 0 x_16)) (flet ($cvcl_394 (and (and (and (and $cvcl_388 $cvcl_392) $cvcl_213) $cvcl_214) $cvcl_215)) (flet ($cvcl_396 (= x_71 (+ 0 48))) (flet ($cvcl_410 (and $cvcl_391 $cvcl_240)) (flet ($cvcl_403 (= x_84 (ite $cvcl_190 8 x_28))) (flet ($cvcl_397 (and (and (and (and $cvcl_410 $cvcl_392) $cvcl_242) $cvcl_403) $cvcl_244)) (flet ($cvcl_398 (= x_71 (- (+ 0 3) x_32))) (flet ($cvcl_400 (and $cvcl_404 $cvcl_389)) (flet ($cvcl_401 (= x_71 (+ 0 3))) (flet ($cvcl_408 (= 0 x_17)) (flet ($cvcl_413 (and (and (and $cvcl_407 $cvcl_411) $cvcl_214) $cvcl_215)) (flet ($cvcl_415 (= x_72 (+ 0 51))) (flet ($cvcl_422 (= x_84 (ite $cvcl_190 9 x_28))) (flet ($cvcl_416 (and (and (and (and $cvcl_410 $cvcl_241) $cvcl_411) $cvcl_422) $cvcl_244)) (flet ($cvcl_417 (= x_72 (- (+ 0 3) x_32))) (flet ($cvcl_419 (and $cvcl_423 $cvcl_408)) (flet ($cvcl_420 (= x_72 (+ 0 3))) (flet ($cvcl_427 (or (= x_54 0) $cvcl_202 )) (flet ($cvcl_428 (or (= x_55 0) $cvcl_271 )) (flet ($cvcl_429 (or (= x_56 0) $cvcl_292 )) (flet ($cvcl_430 (or (= x_57 0) $cvcl_311 )) (flet ($cvcl_431 (or (= x_58 0) $cvcl_330 )) (flet ($cvcl_432 (or (= x_59 0) $cvcl_349 )) (flet ($cvcl_433 (or (= x_60 0) $cvcl_368 )) (flet ($cvcl_434 (or (= x_61 0) $cvcl_387 )) (flet ($cvcl_435 (or (= x_62 0) $cvcl_406 )) (flet ($cvcl_513 (and (and $cvcl_544 (= x_73 0)) (= x_85 2))) (flet ($cvcl_457 (or $cvcl_427 $cvcl_219 )) (flet ($cvcl_458 (or $cvcl_428 $cvcl_274 )) (flet ($cvcl_459 (or $cvcl_429 $cvcl_295 )) (flet ($cvcl_460 (or $cvcl_430 $cvcl_314 )) (flet ($cvcl_461 (or $cvcl_431 $cvcl_333 )) (flet ($cvcl_462 (or $cvcl_432 $cvcl_352 )) (flet ($cvcl_463 (or $cvcl_433 $cvcl_371 )) (flet ($cvcl_464 (or $cvcl_434 $cvcl_390 )) (flet ($cvcl_465 (or $cvcl_435 $cvcl_409 )) (flet ($cvcl_456 (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and $cvcl_513 $cvcl_457) $cvcl_458) $cvcl_459) $cvcl_460) $cvcl_461) $cvcl_462) $cvcl_463) $cvcl_464) $cvcl_465) (or $cvcl_436 (and (and $cvcl_234 $cvcl_514) $cvcl_466) )) (or $cvcl_437 (and (and $cvcl_288 $cvcl_515) $cvcl_467) )) (or $cvcl_438 (and (and $cvcl_307 $cvcl_516) $cvcl_468) )) (or $cvcl_439 (and (and $cvcl_326 $cvcl_517) $cvcl_469) )) (or $cvcl_440 (and (and $cvcl_345 $cvcl_518) $cvcl_470) )) (or $cvcl_441 (and (and $cvcl_364 $cvcl_519) $cvcl_471) )) (or $cvcl_442 (and (and $cvcl_383 $cvcl_520) $cvcl_472) )) (or $cvcl_443 (and (and $cvcl_402 $cvcl_521) $cvcl_473) )) (or $cvcl_444 (and (and $cvcl_421 $cvcl_522) $cvcl_474) )) (or (or $cvcl_445 x_86 ) $cvcl_524 )) (or (or $cvcl_446 x_88 ) $cvcl_526 )) (or (or $cvcl_447 x_89 ) $cvcl_528 )) (or (or $cvcl_448 x_90 ) $cvcl_530 )) (or (or $cvcl_449 x_91 ) $cvcl_532 )) (or (or $cvcl_450 x_92 ) $cvcl_534 )) (or (or $cvcl_451 x_93 ) $cvcl_536 )) (or (or $cvcl_452 x_94 ) $cvcl_538 )) (or (or $cvcl_453 x_95 ) $cvcl_540 ))) (flet ($cvcl_512 (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and $cvcl_426 (or (or (or (or (or (or (or (or $cvcl_219 $cvcl_274 ) $cvcl_295 ) $cvcl_314 ) $cvcl_333 ) $cvcl_352 ) $cvcl_371 ) $cvcl_390 ) $cvcl_409 )) $cvcl_457) $cvcl_458) $cvcl_459) $cvcl_460) $cvcl_461) $cvcl_462) $cvcl_463) $cvcl_464) $cvcl_465) (or $cvcl_436 $cvcl_466 )) (or $cvcl_437 $cvcl_467 )) (or $cvcl_438 $cvcl_468 )) (or $cvcl_439 $cvcl_469 )) (or $cvcl_440 $cvcl_470 )) (or $cvcl_441 $cvcl_471 )) (or $cvcl_442 $cvcl_472 )) (or $cvcl_443 $cvcl_473 )) (or $cvcl_444 $cvcl_474 )) (or $cvcl_436 (and (and (and (and (and (and (and (or $cvcl_437 $cvcl_475 ) (or $cvcl_438 $cvcl_476 )) (or $cvcl_439 $cvcl_477 )) (or $cvcl_440 $cvcl_478 )) (or $cvcl_441 $cvcl_479 )) (or $cvcl_442 $cvcl_480 )) (or $cvcl_443 $cvcl_481 )) (or $cvcl_444 $cvcl_482 )) )) (or $cvcl_437 (and (and (and (and (and (and (or $cvcl_438 $cvcl_483 ) (or $cvcl_439 $cvcl_484 )) (or $cvcl_440 $cvcl_485 )) (or $cvcl_441 $cvcl_486 )) (or $cvcl_442 $cvcl_487 )) (or $cvcl_443 $cvcl_488 )) (or $cvcl_444 $cvcl_489 )) )) (or $cvcl_438 (and (and (and (and (and (or $cvcl_439 $cvcl_490 ) (or $cvcl_440 $cvcl_491 )) (or $cvcl_441 $cvcl_492 )) (or $cvcl_442 $cvcl_493 )) (or $cvcl_443 $cvcl_494 )) (or $cvcl_444 $cvcl_495 )) )) (or $cvcl_439 (and (and (and (and (or $cvcl_440 $cvcl_496 ) (or $cvcl_441 $cvcl_497 )) (or $cvcl_442 $cvcl_498 )) (or $cvcl_443 $cvcl_499 )) (or $cvcl_444 $cvcl_500 )) )) (or $cvcl_440 (and (and (and (or $cvcl_441 $cvcl_501 ) (or $cvcl_442 $cvcl_502 )) (or $cvcl_443 $cvcl_503 )) (or $cvcl_444 $cvcl_504 )) )) (or $cvcl_441 (and (and (or $cvcl_442 $cvcl_505 ) (or $cvcl_443 $cvcl_506 )) (or $cvcl_444 $cvcl_507 )) )) (or $cvcl_442 (and (or $cvcl_443 $cvcl_508 ) (or $cvcl_444 $cvcl_509 )) )) (or (or $cvcl_443 $cvcl_444 ) $cvcl_510 )) (or $cvcl_436 (and (and (and (and (and (and (and (and (or $cvcl_445 (not (<= (- x_63 x_63) x_32)) ) (or $cvcl_446 $cvcl_475 )) (or $cvcl_447 $cvcl_476 )) (or $cvcl_448 $cvcl_477 )) (or $cvcl_449 $cvcl_478 )) (or $cvcl_450 $cvcl_479 )) (or $cvcl_451 $cvcl_480 )) (or $cvcl_452 $cvcl_481 )) (or $cvcl_453 $cvcl_482 )) )) (or $cvcl_437 (and (and (and (and (and (and (and (and (or $cvcl_445 (not (<= (- x_63 x_65) x_32)) ) (or $cvcl_446 (not (<= (- x_65 x_65) x_32)) )) (or $cvcl_447 $cvcl_483 )) (or $cvcl_448 $cvcl_484 )) (or $cvcl_449 $cvcl_485 )) (or $cvcl_450 $cvcl_486 )) (or $cvcl_451 $cvcl_487 )) (or $cvcl_452 $cvcl_488 )) (or $cvcl_453 $cvcl_489 )) )) (or $cvcl_438 (and (and (and (and (and (and (and (and (or $cvcl_445 (not (<= (- x_63 x_66) x_32)) ) (or $cvcl_446 (not (<= (- x_65 x_66) x_32)) )) (or $cvcl_447 (not (<= (- x_66 x_66) x_32)) )) (or $cvcl_448 $cvcl_490 )) (or $cvcl_449 $cvcl_491 )) (or $cvcl_450 $cvcl_492 )) (or $cvcl_451 $cvcl_493 )) (or $cvcl_452 $cvcl_494 )) (or $cvcl_453 $cvcl_495 )) )) (or $cvcl_439 (and (and (and (and (and (and (and (and (or $cvcl_445 (not (<= (- x_63 x_67) x_32)) ) (or $cvcl_446 (not (<= (- x_65 x_67) x_32)) )) (or $cvcl_447 (not (<= (- x_66 x_67) x_32)) )) (or $cvcl_448 (not (<= (- x_67 x_67) x_32)) )) (or $cvcl_449 $cvcl_496 )) (or $cvcl_450 $cvcl_497 )) (or $cvcl_451 $cvcl_498 )) (or $cvcl_452 $cvcl_499 )) (or $cvcl_453 $cvcl_500 )) )) (or $cvcl_440 (and (and (and (and (and (and (and (and (or $cvcl_445 (not (<= (- x_63 x_68) x_32)) ) (or $cvcl_446 (not (<= (- x_65 x_68) x_32)) )) (or $cvcl_447 (not (<= (- x_66 x_68) x_32)) )) (or $cvcl_448 (not (<= (- x_67 x_68) x_32)) )) (or $cvcl_449 (not (<= (- x_68 x_68) x_32)) )) (or $cvcl_450 $cvcl_501 )) (or $cvcl_451 $cvcl_502 )) (or $cvcl_452 $cvcl_503 )) (or $cvcl_453 $cvcl_504 )) )) (or $cvcl_441 (and (and (and (and (and (and (and (and (or $cvcl_445 (not (<= (- x_63 x_69) x_32)) ) (or $cvcl_446 (not (<= (- x_65 x_69) x_32)) )) (or $cvcl_447 (not (<= (- x_66 x_69) x_32)) )) (or $cvcl_448 (not (<= (- x_67 x_69) x_32)) )) (or $cvcl_449 (not (<= (- x_68 x_69) x_32)) )) (or $cvcl_450 (not (<= (- x_69 x_69) x_32)) )) (or $cvcl_451 $cvcl_505 )) (or $cvcl_452 $cvcl_506 )) (or $cvcl_453 $cvcl_507 )) )) (or $cvcl_442 (and (and (and (and (and (and (and (and (or $cvcl_445 (not (<= (- x_63 x_70) x_32)) ) (or $cvcl_446 (not (<= (- x_65 x_70) x_32)) )) (or $cvcl_447 (not (<= (- x_66 x_70) x_32)) )) (or $cvcl_448 (not (<= (- x_67 x_70) x_32)) )) (or $cvcl_449 (not (<= (- x_68 x_70) x_32)) )) (or $cvcl_450 (not (<= (- x_69 x_70) x_32)) )) (or $cvcl_451 (not (<= (- x_70 x_70) x_32)) )) (or $cvcl_452 $cvcl_508 )) (or $cvcl_453 $cvcl_509 )) )) (or $cvcl_443 (and (and (and (and (and (and (and (and (or $cvcl_445 (not (<= (- x_63 x_71) x_32)) ) (or $cvcl_446 (not (<= (- x_65 x_71) x_32)) )) (or $cvcl_447 (not (<= (- x_66 x_71) x_32)) )) (or $cvcl_448 (not (<= (- x_67 x_71) x_32)) )) (or $cvcl_449 (not (<= (- x_68 x_71) x_32)) )) (or $cvcl_450 (not (<= (- x_69 x_71) x_32)) )) (or $cvcl_451 (not (<= (- x_70 x_71) x_32)) )) (or $cvcl_452 (not (<= (- x_71 x_71) x_32)) )) (or $cvcl_453 $cvcl_510 )) )) (or $cvcl_444 (and (and (and (and (and (and (and (and (or $cvcl_445 (not (<= (- x_63 x_72) x_32)) ) (or $cvcl_446 (not (<= (- x_65 x_72) x_32)) )) (or $cvcl_447 (not (<= (- x_66 x_72) x_32)) )) (or $cvcl_448 (not (<= (- x_67 x_72) x_32)) )) (or $cvcl_449 (not (<= (- x_68 x_72) x_32)) )) (or $cvcl_450 (not (<= (- x_69 x_72) x_32)) )) (or $cvcl_451 (not (<= (- x_70 x_72) x_32)) )) (or $cvcl_452 (not (<= (- x_71 x_72) x_32)) )) (or $cvcl_453 (not (<= (- x_72 x_72) x_32)) )) ))) (flet ($cvcl_573 (or (or $cvcl_445 $cvcl_523 ) $cvcl_524 )) (flet ($cvcl_574 (or (or $cvcl_446 $cvcl_525 ) $cvcl_526 )) (flet ($cvcl_575 (or (or $cvcl_447 $cvcl_527 ) $cvcl_528 )) (flet ($cvcl_576 (or (or $cvcl_448 $cvcl_529 ) $cvcl_530 )) (flet ($cvcl_577 (or (or $cvcl_449 $cvcl_531 ) $cvcl_532 )) (flet ($cvcl_578 (or (or $cvcl_450 $cvcl_533 ) $cvcl_534 )) (flet ($cvcl_579 (or (or $cvcl_451 $cvcl_535 ) $cvcl_536 )) (flet ($cvcl_580 (or (or $cvcl_452 $cvcl_537 ) $cvcl_538 )) (flet ($cvcl_581 (or (or $cvcl_453 $cvcl_539 ) $cvcl_540 )) (flet ($cvcl_541 (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and $cvcl_513 (= ?cvcl_545 (+ (+ x_64 (* (- x_84 1) 3)) 27))) (not (if_then_else $cvcl_18 x_95 (if_then_else $cvcl_19 x_94 (if_then_else $cvcl_20 x_93 (if_then_else $cvcl_21 x_92 (if_then_else $cvcl_22 x_91 (if_then_else $cvcl_23 x_90 (if_then_else $cvcl_24 x_89 (if_then_else $cvcl_25 x_88 x_86)))))))))) (or (or (or $cvcl_436 (= 1 x_84) ) $cvcl_523 ) (and $cvcl_514 $cvcl_466) )) (or (or (or $cvcl_437 (= 2 x_84) ) $cvcl_525 ) (and $cvcl_515 $cvcl_467) )) (or (or (or $cvcl_438 (= 3 x_84) ) $cvcl_527 ) (and $cvcl_516 $cvcl_468) )) (or (or (or $cvcl_439 (= 4 x_84) ) $cvcl_529 ) (and $cvcl_517 $cvcl_469) )) (or (or (or $cvcl_440 (= 5 x_84) ) $cvcl_531 ) (and $cvcl_518 $cvcl_470) )) (or (or (or $cvcl_441 (= 6 x_84) ) $cvcl_533 ) (and $cvcl_519 $cvcl_471) )) (or (or (or $cvcl_442 (= 7 x_84) ) $cvcl_535 ) (and $cvcl_520 $cvcl_472) )) (or (or (or $cvcl_443 (= 8 x_84) ) $cvcl_537 ) (and $cvcl_521 $cvcl_473) )) (or (or (or $cvcl_444 (= 9 x_84) ) $cvcl_539 ) (and $cvcl_522 $cvcl_474) )) $cvcl_573) $cvcl_574) $cvcl_575) $cvcl_576) $cvcl_577) $cvcl_578) $cvcl_579) $cvcl_580) $cvcl_581) (or $cvcl_44 (and $cvcl_547 (= x_63 (+ x_64 3))) )) (or $cvcl_45 (and $cvcl_549 (= x_65 (+ x_64 3))) )) (or $cvcl_50 (and $cvcl_551 (= x_66 (+ x_64 3))) )) (or $cvcl_53 (and $cvcl_553 (= x_67 (+ x_64 3))) )) (or $cvcl_56 (and $cvcl_555 (= x_68 (+ x_64 3))) )) (or $cvcl_59 (and $cvcl_557 (= x_69 (+ x_64 3))) )) (or $cvcl_62 (and $cvcl_559 (= x_70 (+ x_64 3))) )) (or $cvcl_65 (and $cvcl_561 (= x_71 (+ x_64 3))) )) (or $cvcl_68 (and $cvcl_563 (= x_72 (+ x_64 3))) ))) (flet ($cvcl_583 (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and $cvcl_544 (= x_73 1)) (= x_85 3)) (= (ite $cvcl_18 x_82 (ite $cvcl_19 x_81 (ite $cvcl_20 x_80 (ite $cvcl_21 x_79 (ite $cvcl_22 x_78 (ite $cvcl_23 x_77 (ite $cvcl_24 x_76 (ite $cvcl_25 x_75 x_74)))))))) x_84)) (= ?cvcl_545 (+ x_64 3))) (or $cvcl_546 (and $cvcl_547 (= x_63 ?cvcl_545)) )) (or $cvcl_548 (and $cvcl_549 (= x_65 ?cvcl_545)) )) (or $cvcl_550 (and $cvcl_551 (= x_66 ?cvcl_545)) )) (or $cvcl_552 (and $cvcl_553 (= x_67 ?cvcl_545)) )) (or $cvcl_554 (and $cvcl_555 (= x_68 ?cvcl_545)) )) (or $cvcl_556 (and $cvcl_557 (= x_69 ?cvcl_545)) )) (or $cvcl_558 (and $cvcl_559 (= x_70 ?cvcl_545)) )) (or $cvcl_560 (and $cvcl_561 (= x_71 ?cvcl_545)) )) (or $cvcl_562 (and $cvcl_563 (= x_72 ?cvcl_545)) )) (or (or $cvcl_44 $cvcl_47 ) (and (= ?cvcl_564 x_84) (= ?cvcl_545 (+ x_63 3))) )) (or (or $cvcl_45 $cvcl_49 ) (and (= ?cvcl_565 x_84) (= ?cvcl_545 (+ x_65 3))) )) (or (or $cvcl_50 $cvcl_52 ) (and (= ?cvcl_566 x_84) (= ?cvcl_545 (+ x_66 3))) )) (or (or $cvcl_53 $cvcl_55 ) (and (= ?cvcl_567 x_84) (= ?cvcl_545 (+ x_67 3))) )) (or (or $cvcl_56 $cvcl_58 ) (and (= ?cvcl_568 x_84) (= ?cvcl_545 (+ x_68 3))) )) (or (or $cvcl_59 $cvcl_61 ) (and (= ?cvcl_569 x_84) (= ?cvcl_545 (+ x_69 3))) )) (or (or $cvcl_62 $cvcl_64 ) (and (= ?cvcl_570 x_84) (= ?cvcl_545 (+ x_70 3))) )) (or (or $cvcl_65 $cvcl_67 ) (and (= ?cvcl_571 x_84) (= ?cvcl_545 (+ x_71 3))) )) (or (or $cvcl_68 $cvcl_70 ) (and (= ?cvcl_572 x_84) (= ?cvcl_545 (+ x_72 3))) )) $cvcl_573) $cvcl_574) $cvcl_575) $cvcl_576) $cvcl_577) $cvcl_578) $cvcl_579) $cvcl_580) $cvcl_581) (or $cvcl_436 $cvcl_523 )) (or $cvcl_437 $cvcl_525 )) (or $cvcl_438 $cvcl_527 )) (or $cvcl_439 $cvcl_529 )) (or $cvcl_440 $cvcl_531 )) (or $cvcl_441 $cvcl_533 )) (or $cvcl_442 $cvcl_535 )) (or $cvcl_443 $cvcl_537 )) (or $cvcl_444 $cvcl_539 ))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (<= x_115 6) (>= x_115 0)) (<= x_105 6)) (>= x_105 0)) (<= x_85 3)) (>= x_85 0)) (<= x_73 1)) (>= x_73 0)) (<= x_62 3)) (>= x_62 0)) (<= x_61 3)) (>= x_61 0)) (<= x_60 3)) (>= x_60 0)) (<= x_59 3)) (>= x_59 0)) (<= x_58 3)) (>= x_58 0)) (<= x_57 3)) (>= x_57 0)) (<= x_56 3)) (>= x_56 0)) (<= x_55 3)) (>= x_55 0)) (<= x_54 3)) (>= x_54 0)) (<= x_43 3)) (>= x_43 0)) (<= x_18 1)) (>= x_18 0)) (<= x_8 3)) (>= x_8 0)) (<= x_7 3)) (>= x_7 0)) (<= x_6 3)) (>= x_6 0)) (<= x_5 3)) (>= x_5 0)) (<= x_4 3)) (>= x_4 0)) (<= x_3 3)) (>= x_3 0)) (<= x_2 3)) (>= x_2 0)) (<= x_1 3)) (>= x_1 0)) (<= x_0 3)) (>= x_0 0)) (or (or (or (or (or (or (or (or $cvcl_0 $cvcl_8 ) $cvcl_7 ) $cvcl_6 ) $cvcl_5 ) $cvcl_4 ) $cvcl_3 ) $cvcl_2 ) $cvcl_1 )) (not (< x_28 1))) (<= x_28 9)) (> x_32 0)) (< x_32 (/ 3 2))) (or (or (or (or (or (or (or (or (= x_33 1) (= x_33 2) ) (= x_33 3) ) (= x_33 4) ) (= x_33 5) ) (= x_33 6) ) (= x_33 7) ) (= x_33 8) ) $cvcl_9 )) (not (< x_33 1))) (<= x_33 9)) (or (or (or (or (or (or (or (or (= x_34 1) (= x_34 2) ) (= x_34 3) ) (= x_34 4) ) (= x_34 5) ) (= x_34 6) ) (= x_34 7) ) (= x_34 8) ) $cvcl_10 )) (not (< x_34 1))) (<= x_34 9)) (or (or (or (or (or (or (or (or (= x_35 1) (= x_35 2) ) (= x_35 3) ) (= x_35 4) ) (= x_35 5) ) (= x_35 6) ) (= x_35 7) ) (= x_35 8) ) $cvcl_11 )) (not (< x_35 1))) (<= x_35 9)) (or (or (or (or (or (or (or (or (= x_36 1) (= x_36 2) ) (= x_36 3) ) (= x_36 4) ) (= x_36 5) ) (= x_36 6) ) (= x_36 7) ) (= x_36 8) ) $cvcl_12 )) (not (< x_36 1))) (<= x_36 9)) (or (or (or (or (or (or (or (or (= x_37 1) (= x_37 2) ) (= x_37 3) ) (= x_37 4) ) (= x_37 5) ) (= x_37 6) ) (= x_37 7) ) (= x_37 8) ) $cvcl_13 )) (not (< x_37 1))) (<= x_37 9)) (or (or (or (or (or (or (or (or (= x_38 1) (= x_38 2) ) (= x_38 3) ) (= x_38 4) ) (= x_38 5) ) (= x_38 6) ) (= x_38 7) ) (= x_38 8) ) $cvcl_14 )) (not (< x_38 1))) (<= x_38 9)) (or (or (or (or (or (or (or (or (= x_39 1) (= x_39 2) ) (= x_39 3) ) (= x_39 4) ) (= x_39 5) ) (= x_39 6) ) (= x_39 7) ) (= x_39 8) ) $cvcl_15 )) (not (< x_39 1))) (<= x_39 9)) (or (or (or (or (or (or (or (or (= x_40 1) (= x_40 2) ) (= x_40 3) ) (= x_40 4) ) (= x_40 5) ) (= x_40 6) ) (= x_40 7) ) (= x_40 8) ) $cvcl_16 )) (not (< x_40 1))) (<= x_40 9)) (or (or (or (or (or (or (or (or (= x_41 1) (= x_41 2) ) (= x_41 3) ) (= x_41 4) ) (= x_41 5) ) (= x_41 6) ) (= x_41 7) ) (= x_41 8) ) $cvcl_17 )) (not (< x_41 1))) (<= x_41 9)) (or (or (or (or (or (or (or (or (= x_74 1) (= x_74 2) ) (= x_74 3) ) (= x_74 4) ) (= x_74 5) ) (= x_74 6) ) (= x_74 7) ) (= x_74 8) ) $cvcl_26 )) (not $cvcl_143)) (<= x_74 9)) (or (or (or (or (or (or (or (or (= x_75 1) (= x_75 2) ) (= x_75 3) ) (= x_75 4) ) (= x_75 5) ) (= x_75 6) ) (= x_75 7) ) (= x_75 8) ) $cvcl_27 )) (not (< x_75 1))) (<= x_75 9)) (or (or (or (or (or (or (or (or (= x_76 1) (= x_76 2) ) (= x_76 3) ) (= x_76 4) ) (= x_76 5) ) (= x_76 6) ) (= x_76 7) ) (= x_76 8) ) $cvcl_28 )) (not (< x_76 1))) (<= x_76 9)) (or (or (or (or (or (or (or (or (= x_77 1) (= x_77 2) ) (= x_77 3) ) (= x_77 4) ) (= x_77 5) ) (= x_77 6) ) (= x_77 7) ) (= x_77 8) ) $cvcl_29 )) (not (< x_77 1))) (<= x_77 9)) (or (or (or (or (or (or (or (or (= x_78 1) (= x_78 2) ) (= x_78 3) ) (= x_78 4) ) (= x_78 5) ) (= x_78 6) ) (= x_78 7) ) (= x_78 8) ) $cvcl_30 )) (not (< x_78 1))) (<= x_78 9)) (or (or (or (or (or (or (or (or (= x_79 1) (= x_79 2) ) (= x_79 3) ) (= x_79 4) ) (= x_79 5) ) (= x_79 6) ) (= x_79 7) ) (= x_79 8) ) $cvcl_31 )) (not (< x_79 1))) (<= x_79 9)) (or (or (or (or (or (or (or (or (= x_80 1) (= x_80 2) ) (= x_80 3) ) (= x_80 4) ) (= x_80 5) ) (= x_80 6) ) (= x_80 7) ) (= x_80 8) ) $cvcl_32 )) (not (< x_80 1))) (<= x_80 9)) (or (or (or (or (or (or (or (or (= x_81 1) (= x_81 2) ) (= x_81 3) ) (= x_81 4) ) (= x_81 5) ) (= x_81 6) ) (= x_81 7) ) (= x_81 8) ) $cvcl_33 )) (not (< x_81 1))) (<= x_81 9)) (or (or (or (or (or (or (or (or (= x_82 1) (= x_82 2) ) (= x_82 3) ) (= x_82 4) ) (= x_82 5) ) (= x_82 6) ) (= x_82 7) ) (= x_82 8) ) $cvcl_34 )) (not (< x_82 1))) (<= x_82 9)) (or (or (or (or (or (or (or (or (= x_84 1) $cvcl_25 ) $cvcl_24 ) $cvcl_23 ) $cvcl_22 ) $cvcl_21 ) $cvcl_20 ) $cvcl_19 ) $cvcl_18 )) (not (< x_84 1))) (<= x_84 9)) $cvcl_201) $cvcl_270) $cvcl_291) $cvcl_310) $cvcl_329) $cvcl_348) $cvcl_367) $cvcl_386) $cvcl_405) $cvcl_180) (< x_9 30)) $cvcl_181) (< x_10 30)) $cvcl_182) (< x_11 30)) $cvcl_183) (< x_12 30)) $cvcl_184) (< x_13 30)) $cvcl_185) (< x_14 30)) $cvcl_186) (< x_15 30)) $cvcl_187) (< x_16 30)) $cvcl_188) (< x_17 30)) $cvcl_228) $cvcl_171) $cvcl_172) $cvcl_173) $cvcl_174) $cvcl_175) $cvcl_176) $cvcl_177) $cvcl_178) $cvcl_179) $cvcl_0) $cvcl_425) (= x_42 (- 9 x_41))) (= x_43 (ite $cvcl_1 x_8 (ite $cvcl_2 x_7 (ite $cvcl_3 x_6 (ite $cvcl_4 x_5 (ite $cvcl_5 x_4 (ite $cvcl_6 x_3 (ite $cvcl_7 x_2 (ite $cvcl_8 x_1 x_0)))))))))) (= x_44 ?cvcl_162)) (= x_45 ?cvcl_163)) (= x_46 ?cvcl_164)) (= x_47 ?cvcl_165)) (= x_48 ?cvcl_166)) (= x_49 ?cvcl_167)) (= x_50 ?cvcl_168)) (= x_51 ?cvcl_169)) (= x_52 ?cvcl_170)) (= x_83 (- 9 x_82))) (= x_85 (ite $cvcl_18 x_62 (ite $cvcl_19 x_61 (ite $cvcl_20 x_60 (ite $cvcl_21 x_59 (ite $cvcl_22 x_58 (ite $cvcl_23 x_57 (ite $cvcl_24 x_56 (ite $cvcl_25 x_55 x_54)))))))))) (= x_96 ?cvcl_564)) (= x_97 ?cvcl_565)) (= x_98 ?cvcl_566)) (= x_99 ?cvcl_567)) (= x_100 ?cvcl_568)) (= x_101 ?cvcl_569)) (= x_102 ?cvcl_570)) (= x_103 ?cvcl_571)) (= x_104 ?cvcl_572)) (= x_105 (ite $cvcl_543 4 6))) (= x_106 ?cvcl_162)) (= x_107 ?cvcl_163)) (= x_108 ?cvcl_164)) (= x_109 ?cvcl_165)) (= x_110 ?cvcl_166)) (= x_111 ?cvcl_167)) (= x_112 ?cvcl_168)) (= x_113 ?cvcl_169)) (= x_114 ?cvcl_170)) (or (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (if_then_else $cvcl_190 $cvcl_189 (and $cvcl_189 (> 0 0))) (if_then_else $cvcl_190 (and $cvcl_191 (or (or (or (or (or (or (or (or $cvcl_192 $cvcl_193 ) $cvcl_194 ) $cvcl_195 ) $cvcl_196 ) $cvcl_197 ) $cvcl_198 ) $cvcl_199 ) $cvcl_200 )) (and (and $cvcl_191 (<= x_53 0)) (or (or (or (or (or (or (or (or (or $cvcl_424 $cvcl_192 ) $cvcl_193 ) $cvcl_194 ) $cvcl_195 ) $cvcl_196 ) $cvcl_197 ) $cvcl_198 ) $cvcl_199 ) $cvcl_200 )))) $cvcl_216) $cvcl_246) $cvcl_249) $cvcl_252) $cvcl_255) $cvcl_258) $cvcl_261) $cvcl_264) $cvcl_267) $cvcl_204) $cvcl_247) $cvcl_250) $cvcl_253) $cvcl_256) $cvcl_259) $cvcl_262) $cvcl_265) $cvcl_268) $cvcl_217) $cvcl_248) $cvcl_251) $cvcl_254) $cvcl_257) $cvcl_260) $cvcl_263) $cvcl_266) $cvcl_269) $cvcl_203) (and (or (or (or (or (or (or (or (or (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (or (or (or (or (or (or (or (or (and (and (and (and (and $cvcl_201 $cvcl_218) $cvcl_202) (= x_63 (+ 0 54))) $cvcl_203) $cvcl_204) (and (and (and (and (and (and $cvcl_201 x_19) $cvcl_222) $cvcl_223) $cvcl_216) $cvcl_204) $cvcl_217) ) (and (and (and (and (and $cvcl_221 $cvcl_218) $cvcl_219) $cvcl_226) $cvcl_227) $cvcl_204) ) (and (and (and (and (and (and (and $cvcl_221 x_19) $cvcl_224) $cvcl_222) $cvcl_219) (= x_63 (- (+ 0 27) x_32))) $cvcl_223) $cvcl_204) ) (and (and (and (and (and (and (and $cvcl_225 x_19) $cvcl_224) $cvcl_222) $cvcl_35) $cvcl_229) $cvcl_230) $cvcl_223) ) (and (and (and (and (and $cvcl_225 $cvcl_218) $cvcl_226) $cvcl_227) $cvcl_216) $cvcl_204) ) (and (and (and (and (and (and (and (or $cvcl_221 $cvcl_225 ) x_19) $cvcl_228) $cvcl_222) $cvcl_35) $cvcl_229) $cvcl_230) $cvcl_223) ) (and (and (and (and (and $cvcl_231 (not (= ?cvcl_162 1))) $cvcl_232) (= x_74 x_106)) $cvcl_203) $cvcl_216) ) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and $cvcl_231 (= x_106 1)) $cvcl_232) (= x_74 ?cvcl_162)) $cvcl_286) $cvcl_233) $cvcl_234) $cvcl_235) $cvcl_236) $cvcl_237) $cvcl_238) $cvcl_239) $cvcl_240) $cvcl_241) $cvcl_242) $cvcl_243) $cvcl_244) $cvcl_216) ) (and (and (and (and (and (and (and $cvcl_245 x_19) $cvcl_228) $cvcl_222) $cvcl_223) $cvcl_216) $cvcl_204) $cvcl_217) ) $cvcl_246) $cvcl_247) $cvcl_248) $cvcl_249) $cvcl_250) $cvcl_251) $cvcl_252) $cvcl_253) $cvcl_254) $cvcl_255) $cvcl_256) $cvcl_257) $cvcl_258) $cvcl_259) $cvcl_260) $cvcl_261) $cvcl_262) $cvcl_263) $cvcl_264) $cvcl_265) $cvcl_266) $cvcl_267) $cvcl_268) $cvcl_269) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (or (or (or (or (or (or (or (or (and (and (and (and (and $cvcl_270 $cvcl_273) $cvcl_271) (= x_65 (+ 0 57))) $cvcl_203) $cvcl_247) (and (and (and (and (and (and $cvcl_270 x_20) $cvcl_222) $cvcl_278) $cvcl_246) $cvcl_247) $cvcl_248) ) (and (and (and (and (and $cvcl_277 $cvcl_273) $cvcl_274) $cvcl_280) $cvcl_281) $cvcl_247) ) (and (and (and (and (and (and (and $cvcl_277 x_20) $cvcl_224) $cvcl_222) $cvcl_274) (= x_65 (- (+ 0 30) x_32))) $cvcl_278) $cvcl_247) ) (and (and (and (and (and (and (and $cvcl_279 x_20) $cvcl_224) $cvcl_222) $cvcl_36) $cvcl_282) $cvcl_283) $cvcl_278) ) (and (and (and (and (and $cvcl_279 $cvcl_273) $cvcl_280) $cvcl_281) $cvcl_246) $cvcl_247) ) (and (and (and (and (and (and (and (or $cvcl_277 $cvcl_279 ) x_20) $cvcl_228) $cvcl_222) $cvcl_36) $cvcl_282) $cvcl_283) $cvcl_278) ) (and (and (and (and (and $cvcl_284 (not (= ?cvcl_163 2))) $cvcl_285) (= x_75 x_107)) $cvcl_203) $cvcl_246) ) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and $cvcl_284 (= x_107 2)) $cvcl_285) (= x_75 ?cvcl_163)) $cvcl_286) $cvcl_233) $cvcl_287) $cvcl_288) $cvcl_236) $cvcl_237) $cvcl_238) $cvcl_239) $cvcl_240) $cvcl_241) $cvcl_242) $cvcl_289) $cvcl_244) $cvcl_246) ) (and (and (and (and (and (and (and $cvcl_290 x_20) $cvcl_228) $cvcl_222) $cvcl_278) $cvcl_246) $cvcl_247) $cvcl_248) ) $cvcl_216) $cvcl_204) $cvcl_217) $cvcl_249) $cvcl_250) $cvcl_251) $cvcl_252) $cvcl_253) $cvcl_254) $cvcl_255) $cvcl_256) $cvcl_257) $cvcl_258) $cvcl_259) $cvcl_260) $cvcl_261) $cvcl_262) $cvcl_263) $cvcl_264) $cvcl_265) $cvcl_266) $cvcl_267) $cvcl_268) $cvcl_269) ) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (or (or (or (or (or (or (or (or (and (and (and (and (and $cvcl_291 $cvcl_294) $cvcl_292) (= x_66 (+ 0 60))) $cvcl_203) $cvcl_250) (and (and (and (and (and (and $cvcl_291 x_21) $cvcl_222) $cvcl_299) $cvcl_249) $cvcl_250) $cvcl_251) ) (and (and (and (and (and $cvcl_298 $cvcl_294) $cvcl_295) $cvcl_301) $cvcl_302) $cvcl_250) ) (and (and (and (and (and (and (and $cvcl_298 x_21) $cvcl_224) $cvcl_222) $cvcl_295) (= x_66 (- (+ 0 33) x_32))) $cvcl_299) $cvcl_250) ) (and (and (and (and (and (and (and $cvcl_300 x_21) $cvcl_224) $cvcl_222) $cvcl_37) $cvcl_303) $cvcl_304) $cvcl_299) ) (and (and (and (and (and $cvcl_300 $cvcl_294) $cvcl_301) $cvcl_302) $cvcl_249) $cvcl_250) ) (and (and (and (and (and (and (and (or $cvcl_298 $cvcl_300 ) x_21) $cvcl_228) $cvcl_222) $cvcl_37) $cvcl_303) $cvcl_304) $cvcl_299) ) (and (and (and (and (and $cvcl_305 (not (= ?cvcl_164 3))) $cvcl_306) (= x_76 x_108)) $cvcl_203) $cvcl_249) ) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and $cvcl_305 (= x_108 3)) $cvcl_306) (= x_76 ?cvcl_164)) $cvcl_286) $cvcl_233) $cvcl_287) $cvcl_235) $cvcl_307) $cvcl_237) $cvcl_238) $cvcl_239) $cvcl_240) $cvcl_241) $cvcl_242) $cvcl_308) $cvcl_244) $cvcl_249) ) (and (and (and (and (and (and (and $cvcl_309 x_21) $cvcl_228) $cvcl_222) $cvcl_299) $cvcl_249) $cvcl_250) $cvcl_251) ) $cvcl_216) $cvcl_204) $cvcl_217) $cvcl_246) $cvcl_247) $cvcl_248) $cvcl_252) $cvcl_253) $cvcl_254) $cvcl_255) $cvcl_256) $cvcl_257) $cvcl_258) $cvcl_259) $cvcl_260) $cvcl_261) $cvcl_262) $cvcl_263) $cvcl_264) $cvcl_265) $cvcl_266) $cvcl_267) $cvcl_268) $cvcl_269) ) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (or (or (or (or (or (or (or (or (and (and (and (and (and $cvcl_310 $cvcl_313) $cvcl_311) (= x_67 (+ 0 63))) $cvcl_203) $cvcl_253) (and (and (and (and (and (and $cvcl_310 x_22) $cvcl_222) $cvcl_318) $cvcl_252) $cvcl_253) $cvcl_254) ) (and (and (and (and (and $cvcl_317 $cvcl_313) $cvcl_314) $cvcl_320) $cvcl_321) $cvcl_253) ) (and (and (and (and (and (and (and $cvcl_317 x_22) $cvcl_224) $cvcl_222) $cvcl_314) (= x_67 (- (+ 0 36) x_32))) $cvcl_318) $cvcl_253) ) (and (and (and (and (and (and (and $cvcl_319 x_22) $cvcl_224) $cvcl_222) $cvcl_38) $cvcl_322) $cvcl_323) $cvcl_318) ) (and (and (and (and (and $cvcl_319 $cvcl_313) $cvcl_320) $cvcl_321) $cvcl_252) $cvcl_253) ) (and (and (and (and (and (and (and (or $cvcl_317 $cvcl_319 ) x_22) $cvcl_228) $cvcl_222) $cvcl_38) $cvcl_322) $cvcl_323) $cvcl_318) ) (and (and (and (and (and $cvcl_324 (not (= ?cvcl_165 4))) $cvcl_325) (= x_77 x_109)) $cvcl_203) $cvcl_252) ) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and $cvcl_324 (= x_109 4)) $cvcl_325) (= x_77 ?cvcl_165)) $cvcl_286) $cvcl_233) $cvcl_287) $cvcl_235) $cvcl_236) $cvcl_326) $cvcl_238) $cvcl_239) $cvcl_240) $cvcl_241) $cvcl_242) $cvcl_327) $cvcl_244) $cvcl_252) ) (and (and (and (and (and (and (and $cvcl_328 x_22) $cvcl_228) $cvcl_222) $cvcl_318) $cvcl_252) $cvcl_253) $cvcl_254) ) $cvcl_216) $cvcl_204) $cvcl_217) $cvcl_246) $cvcl_247) $cvcl_248) $cvcl_249) $cvcl_250) $cvcl_251) $cvcl_255) $cvcl_256) $cvcl_257) $cvcl_258) $cvcl_259) $cvcl_260) $cvcl_261) $cvcl_262) $cvcl_263) $cvcl_264) $cvcl_265) $cvcl_266) $cvcl_267) $cvcl_268) $cvcl_269) ) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (or (or (or (or (or (or (or (or (and (and (and (and (and $cvcl_329 $cvcl_332) $cvcl_330) (= x_68 (+ 0 66))) $cvcl_203) $cvcl_256) (and (and (and (and (and (and $cvcl_329 x_23) $cvcl_222) $cvcl_337) $cvcl_255) $cvcl_256) $cvcl_257) ) (and (and (and (and (and $cvcl_336 $cvcl_332) $cvcl_333) $cvcl_339) $cvcl_340) $cvcl_256) ) (and (and (and (and (and (and (and $cvcl_336 x_23) $cvcl_224) $cvcl_222) $cvcl_333) (= x_68 (- (+ 0 39) x_32))) $cvcl_337) $cvcl_256) ) (and (and (and (and (and (and (and $cvcl_338 x_23) $cvcl_224) $cvcl_222) $cvcl_39) $cvcl_341) $cvcl_342) $cvcl_337) ) (and (and (and (and (and $cvcl_338 $cvcl_332) $cvcl_339) $cvcl_340) $cvcl_255) $cvcl_256) ) (and (and (and (and (and (and (and (or $cvcl_336 $cvcl_338 ) x_23) $cvcl_228) $cvcl_222) $cvcl_39) $cvcl_341) $cvcl_342) $cvcl_337) ) (and (and (and (and (and $cvcl_343 (not (= ?cvcl_166 5))) $cvcl_344) (= x_78 x_110)) $cvcl_203) $cvcl_255) ) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and $cvcl_343 (= x_110 5)) $cvcl_344) (= x_78 ?cvcl_166)) $cvcl_286) $cvcl_233) $cvcl_287) $cvcl_235) $cvcl_236) $cvcl_237) $cvcl_345) $cvcl_239) $cvcl_240) $cvcl_241) $cvcl_242) $cvcl_346) $cvcl_244) $cvcl_255) ) (and (and (and (and (and (and (and $cvcl_347 x_23) $cvcl_228) $cvcl_222) $cvcl_337) $cvcl_255) $cvcl_256) $cvcl_257) ) $cvcl_216) $cvcl_204) $cvcl_217) $cvcl_246) $cvcl_247) $cvcl_248) $cvcl_249) $cvcl_250) $cvcl_251) $cvcl_252) $cvcl_253) $cvcl_254) $cvcl_258) $cvcl_259) $cvcl_260) $cvcl_261) $cvcl_262) $cvcl_263) $cvcl_264) $cvcl_265) $cvcl_266) $cvcl_267) $cvcl_268) $cvcl_269) ) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (or (or (or (or (or (or (or (or (and (and (and (and (and $cvcl_348 $cvcl_351) $cvcl_349) (= x_69 (+ 0 69))) $cvcl_203) $cvcl_259) (and (and (and (and (and (and $cvcl_348 x_24) $cvcl_222) $cvcl_356) $cvcl_258) $cvcl_259) $cvcl_260) ) (and (and (and (and (and $cvcl_355 $cvcl_351) $cvcl_352) $cvcl_358) $cvcl_359) $cvcl_259) ) (and (and (and (and (and (and (and $cvcl_355 x_24) $cvcl_224) $cvcl_222) $cvcl_352) (= x_69 (- (+ 0 42) x_32))) $cvcl_356) $cvcl_259) ) (and (and (and (and (and (and (and $cvcl_357 x_24) $cvcl_224) $cvcl_222) $cvcl_40) $cvcl_360) $cvcl_361) $cvcl_356) ) (and (and (and (and (and $cvcl_357 $cvcl_351) $cvcl_358) $cvcl_359) $cvcl_258) $cvcl_259) ) (and (and (and (and (and (and (and (or $cvcl_355 $cvcl_357 ) x_24) $cvcl_228) $cvcl_222) $cvcl_40) $cvcl_360) $cvcl_361) $cvcl_356) ) (and (and (and (and (and $cvcl_362 (not (= ?cvcl_167 6))) $cvcl_363) (= x_79 x_111)) $cvcl_203) $cvcl_258) ) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and $cvcl_362 (= x_111 6)) $cvcl_363) (= x_79 ?cvcl_167)) $cvcl_286) $cvcl_233) $cvcl_287) $cvcl_235) $cvcl_236) $cvcl_237) $cvcl_238) $cvcl_364) $cvcl_240) $cvcl_241) $cvcl_242) $cvcl_365) $cvcl_244) $cvcl_258) ) (and (and (and (and (and (and (and $cvcl_366 x_24) $cvcl_228) $cvcl_222) $cvcl_356) $cvcl_258) $cvcl_259) $cvcl_260) ) $cvcl_216) $cvcl_204) $cvcl_217) $cvcl_246) $cvcl_247) $cvcl_248) $cvcl_249) $cvcl_250) $cvcl_251) $cvcl_252) $cvcl_253) $cvcl_254) $cvcl_255) $cvcl_256) $cvcl_257) $cvcl_261) $cvcl_262) $cvcl_263) $cvcl_264) $cvcl_265) $cvcl_266) $cvcl_267) $cvcl_268) $cvcl_269) ) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (or (or (or (or (or (or (or (or (and (and (and (and (and $cvcl_367 $cvcl_370) $cvcl_368) (= x_70 (+ 0 72))) $cvcl_203) $cvcl_262) (and (and (and (and (and (and $cvcl_367 x_25) $cvcl_222) $cvcl_375) $cvcl_261) $cvcl_262) $cvcl_263) ) (and (and (and (and (and $cvcl_374 $cvcl_370) $cvcl_371) $cvcl_377) $cvcl_378) $cvcl_262) ) (and (and (and (and (and (and (and $cvcl_374 x_25) $cvcl_224) $cvcl_222) $cvcl_371) (= x_70 (- (+ 0 45) x_32))) $cvcl_375) $cvcl_262) ) (and (and (and (and (and (and (and $cvcl_376 x_25) $cvcl_224) $cvcl_222) $cvcl_41) $cvcl_379) $cvcl_380) $cvcl_375) ) (and (and (and (and (and $cvcl_376 $cvcl_370) $cvcl_377) $cvcl_378) $cvcl_261) $cvcl_262) ) (and (and (and (and (and (and (and (or $cvcl_374 $cvcl_376 ) x_25) $cvcl_228) $cvcl_222) $cvcl_41) $cvcl_379) $cvcl_380) $cvcl_375) ) (and (and (and (and (and $cvcl_381 (not (= ?cvcl_168 7))) $cvcl_382) (= x_80 x_112)) $cvcl_203) $cvcl_261) ) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and $cvcl_381 (= x_112 7)) $cvcl_382) (= x_80 ?cvcl_168)) $cvcl_286) $cvcl_233) $cvcl_287) $cvcl_235) $cvcl_236) $cvcl_237) $cvcl_238) $cvcl_239) $cvcl_383) $cvcl_241) $cvcl_242) $cvcl_384) $cvcl_244) $cvcl_261) ) (and (and (and (and (and (and (and $cvcl_385 x_25) $cvcl_228) $cvcl_222) $cvcl_375) $cvcl_261) $cvcl_262) $cvcl_263) ) $cvcl_216) $cvcl_204) $cvcl_217) $cvcl_246) $cvcl_247) $cvcl_248) $cvcl_249) $cvcl_250) $cvcl_251) $cvcl_252) $cvcl_253) $cvcl_254) $cvcl_255) $cvcl_256) $cvcl_257) $cvcl_258) $cvcl_259) $cvcl_260) $cvcl_264) $cvcl_265) $cvcl_266) $cvcl_267) $cvcl_268) $cvcl_269) ) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (or (or (or (or (or (or (or (or (and (and (and (and (and $cvcl_386 $cvcl_389) $cvcl_387) (= x_71 (+ 0 75))) $cvcl_203) $cvcl_265) (and (and (and (and (and (and $cvcl_386 x_26) $cvcl_222) $cvcl_394) $cvcl_264) $cvcl_265) $cvcl_266) ) (and (and (and (and (and $cvcl_393 $cvcl_389) $cvcl_390) $cvcl_396) $cvcl_397) $cvcl_265) ) (and (and (and (and (and (and (and $cvcl_393 x_26) $cvcl_224) $cvcl_222) $cvcl_390) (= x_71 (- (+ 0 48) x_32))) $cvcl_394) $cvcl_265) ) (and (and (and (and (and (and (and $cvcl_395 x_26) $cvcl_224) $cvcl_222) $cvcl_42) $cvcl_398) $cvcl_399) $cvcl_394) ) (and (and (and (and (and $cvcl_395 $cvcl_389) $cvcl_396) $cvcl_397) $cvcl_264) $cvcl_265) ) (and (and (and (and (and (and (and (or $cvcl_393 $cvcl_395 ) x_26) $cvcl_228) $cvcl_222) $cvcl_42) $cvcl_398) $cvcl_399) $cvcl_394) ) (and (and (and (and (and $cvcl_400 (not (= ?cvcl_169 8))) $cvcl_401) (= x_81 x_113)) $cvcl_203) $cvcl_264) ) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and $cvcl_400 (= x_113 8)) $cvcl_401) (= x_81 ?cvcl_169)) $cvcl_286) $cvcl_233) $cvcl_287) $cvcl_235) $cvcl_236) $cvcl_237) $cvcl_238) $cvcl_239) $cvcl_240) $cvcl_402) $cvcl_242) $cvcl_403) $cvcl_244) $cvcl_264) ) (and (and (and (and (and (and (and $cvcl_404 x_26) $cvcl_228) $cvcl_222) $cvcl_394) $cvcl_264) $cvcl_265) $cvcl_266) ) $cvcl_216) $cvcl_204) $cvcl_217) $cvcl_246) $cvcl_247) $cvcl_248) $cvcl_249) $cvcl_250) $cvcl_251) $cvcl_252) $cvcl_253) $cvcl_254) $cvcl_255) $cvcl_256) $cvcl_257) $cvcl_258) $cvcl_259) $cvcl_260) $cvcl_261) $cvcl_262) $cvcl_263) $cvcl_267) $cvcl_268) $cvcl_269) ) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (or (or (or (or (or (or (or (or (and (and (and (and (and $cvcl_405 $cvcl_408) $cvcl_406) (= x_72 (+ 0 78))) $cvcl_203) $cvcl_268) (and (and (and (and (and (and $cvcl_405 x_27) $cvcl_222) $cvcl_413) $cvcl_267) $cvcl_268) $cvcl_269) ) (and (and (and (and (and $cvcl_412 $cvcl_408) $cvcl_409) $cvcl_415) $cvcl_416) $cvcl_268) ) (and (and (and (and (and (and (and $cvcl_412 x_27) $cvcl_224) $cvcl_222) $cvcl_409) (= x_72 (- (+ 0 51) x_32))) $cvcl_413) $cvcl_268) ) (and (and (and (and (and (and (and $cvcl_414 x_27) $cvcl_224) $cvcl_222) $cvcl_43) $cvcl_417) $cvcl_418) $cvcl_413) ) (and (and (and (and (and $cvcl_414 $cvcl_408) $cvcl_415) $cvcl_416) $cvcl_267) $cvcl_268) ) (and (and (and (and (and (and (and (or $cvcl_412 $cvcl_414 ) x_27) $cvcl_228) $cvcl_222) $cvcl_43) $cvcl_417) $cvcl_418) $cvcl_413) ) (and (and (and (and (and $cvcl_419 (not (= ?cvcl_170 9))) $cvcl_420) (= x_82 x_114)) $cvcl_203) $cvcl_267) ) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and $cvcl_419 (= x_114 9)) $cvcl_420) (= x_82 ?cvcl_170)) $cvcl_286) $cvcl_233) $cvcl_287) $cvcl_235) $cvcl_236) $cvcl_237) $cvcl_238) $cvcl_239) $cvcl_240) $cvcl_241) $cvcl_421) $cvcl_422) $cvcl_244) $cvcl_267) ) (and (and (and (and (and (and (and $cvcl_423 x_27) $cvcl_228) $cvcl_222) $cvcl_413) $cvcl_267) $cvcl_268) $cvcl_269) ) $cvcl_216) $cvcl_204) $cvcl_217) $cvcl_246) $cvcl_247) $cvcl_248) $cvcl_249) $cvcl_250) $cvcl_251) $cvcl_252) $cvcl_253) $cvcl_254) $cvcl_255) $cvcl_256) $cvcl_257) $cvcl_258) $cvcl_259) $cvcl_260) $cvcl_261) $cvcl_262) $cvcl_263) $cvcl_264) $cvcl_265) $cvcl_266) ) $cvcl_424) )) (or (or (or (or (or (or (and $cvcl_425 (= x_115 (ite (and (and (and (and (and (and (and (and (and $cvcl_426 $cvcl_427) $cvcl_428) $cvcl_429) $cvcl_430) $cvcl_431) $cvcl_432) $cvcl_433) $cvcl_434) $cvcl_435) 0 (ite $cvcl_456 1 6)))) (and (and $cvcl_582 $cvcl_455) (= x_115 (ite $cvcl_456 1 (ite $cvcl_512 2 6)))) ) (and (and (and $cvcl_511 x_30) $cvcl_455) (= x_115 (ite $cvcl_512 2 (ite $cvcl_541 3 6)))) ) (and (and (and x_29 x_30) $cvcl_455) (= x_115 (ite $cvcl_541 3 (ite $cvcl_512 2 x_105)))) ) (and (and $cvcl_542 x_31) (= x_115 (ite $cvcl_543 4 (ite $cvcl_583 5 6)))) ) (and (and $cvcl_582 x_31) (= x_115 (ite $cvcl_583 5 x_105))) ) (and $cvcl_586 (= x_115 6)) )) (or (and (and (and (and (and (not (= x_115 0)) (not (= x_115 1))) (not (= x_115 2))) (not (= x_115 3))) (not (= x_115 4))) (not (= x_115 5))) $cvcl_586 )) (or (or $cvcl_455 $cvcl_454 ) $cvcl_511 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) -) |