(set-logic QF_UFLIA)
(declare-fun _base () Int)
(declare-fun _n () Int)
(assert (let ((.def_5 (<= 0 _n)))
.def_5
))
(declare-fun ___z2z___ (Int) Bool)
(declare-fun ___z3z___ (Int) Bool)
(declare-fun ___z4z___ (Int) Bool)
(declare-fun ___z5z___ (Int) Bool)
(declare-fun ___z6z___ (Int) Bool)
(declare-fun ___z7z___ (Int) Bool)
(declare-fun ___z8z___ (Int) Bool)
(declare-fun ___z9z___ (Int) Bool)
(declare-fun ___z10z___ (Int) Int)
(declare-fun ___z11z___ (Int) Bool)
(declare-fun ___z12z___ (Int) Int)
(declare-fun ___z13z___ (Int) Int)
(declare-fun ___z14z___ (Int) Int)
(declare-fun ___z15z___ (Int) Int)
(declare-fun ___z16z___ (Int) Bool)
(declare-fun ___z18z___ (Int) Bool)
(declare-fun ___z19z___ (Int) Bool)
(declare-fun ___z20z___ (Int) Bool)
(declare-fun ___z21z___ (Int) Bool)
(declare-fun ___z22z___ (Int) Bool)
(declare-fun ___z23z___ (Int) Bool)
(declare-fun ___z24z___ (Int) Bool)
(declare-fun ___z25z___ (Int) Bool)
(declare-fun ___z26z___ (Int) Int)
(declare-fun ___z27z___ (Int) Bool)
(push 1)
(assert (let ((.def_531 (___z20z___ 0)))
(let ((.def_528 (___z12z___ (- 1))))
(let ((.def_529 (<= 1 .def_528)))
(let ((.def_525 (___z15z___ (- 1))))
(let ((.def_524 (___z14z___ (- 1))))
(let ((.def_526 (+ .def_524 .def_525)))
(let ((.def_527 (<= 1 .def_526)))
(let ((.def_530 (and .def_527 .def_529)))
(let ((.def_532 (= .def_530 .def_531)))
.def_532
))))))))))
(assert (let ((.def_538 (___z11z___ 0)))
(let ((.def_535 (___z15z___ 0)))
(let ((.def_536 (<= 0 .def_535)))
(let ((.def_533 (___z16z___ 0)))
(let ((.def_534 (not .def_533)))
(let ((.def_537 (or .def_534 .def_536)))
(let ((.def_539 (= .def_537 .def_538)))
.def_539
))))))))
(assert (let ((.def_541 (___z21z___ 0)))
(let ((.def_524 (___z14z___ (- 1))))
(let ((.def_540 (<= 1 .def_524)))
(let ((.def_542 (= .def_540 .def_541)))
.def_542
)))))
(assert (let ((.def_570 (___z12z___ 0)))
(let ((.def_528 (___z12z___ (- 1))))
(let ((.def_543 (+ (- 1) .def_528)))
(let ((.def_544 (___z25z___ 0)))
(let ((.def_545 (ite .def_544 .def_543 .def_528)))
(let ((.def_546 (___z9z___ 0)))
(let ((.def_547 (ite .def_546 .def_545 .def_528)))
(let ((.def_548 (___z24z___ 0)))
(let ((.def_549 (ite .def_548 .def_543 .def_528)))
(let ((.def_550 (___z8z___ 0)))
(let ((.def_551 (ite .def_550 .def_549 .def_547)))
(let ((.def_552 (___z23z___ 0)))
(let ((.def_553 (ite .def_552 .def_543 .def_528)))
(let ((.def_554 (___z7z___ 0)))
(let ((.def_555 (ite .def_554 .def_553 .def_551)))
(let ((.def_531 (___z20z___ 0)))
(let ((.def_556 (ite .def_531 .def_543 .def_528)))
(let ((.def_557 (___z4z___ 0)))
(let ((.def_558 (ite .def_557 .def_556 .def_555)))
(let ((.def_559 (___z19z___ 0)))
(let ((.def_560 (ite .def_559 .def_543 .def_528)))
(let ((.def_561 (___z3z___ 0)))
(let ((.def_562 (ite .def_561 .def_560 .def_558)))
(let ((.def_563 (___z18z___ 0)))
(let ((.def_564 (ite .def_563 .def_543 .def_528)))
(let ((.def_565 (___z2z___ 0)))
(let ((.def_566 (ite .def_565 .def_564 .def_562)))
(let ((.def_567 (___z26z___ 0)))
(let ((.def_568 (= _base 0)))
(let ((.def_569 (ite .def_568 .def_567 .def_566)))
(let ((.def_571 (= .def_569 .def_570)))
.def_571
))))))))))))))))))))))))))))))))
(assert (let ((.def_573 (___z22z___ 0)))
(let ((.def_525 (___z15z___ (- 1))))
(let ((.def_572 (= .def_525 1)))
(let ((.def_574 (= .def_572 .def_573)))
.def_574
)))))
(assert (let ((.def_588 (___z13z___ 0)))
(let ((.def_575 (___z13z___ (- 1))))
(let ((.def_576 (+ (- 1) .def_575)))
(let ((.def_548 (___z24z___ 0)))
(let ((.def_577 (ite .def_548 .def_576 .def_575)))
(let ((.def_550 (___z8z___ 0)))
(let ((.def_578 (ite .def_550 .def_577 .def_575)))
(let ((.def_552 (___z23z___ 0)))
(let ((.def_579 (ite .def_552 1 .def_575)))
(let ((.def_554 (___z7z___ 0)))
(let ((.def_580 (ite .def_554 .def_579 .def_578)))
(let ((.def_581 (+ 1 .def_575)))
(let ((.def_541 (___z21z___ 0)))
(let ((.def_582 (ite .def_541 .def_581 .def_575)))
(let ((.def_583 (___z5z___ 0)))
(let ((.def_584 (ite .def_583 .def_582 .def_580)))
(let ((.def_559 (___z19z___ 0)))
(let ((.def_585 (ite .def_559 .def_576 .def_575)))
(let ((.def_561 (___z3z___ 0)))
(let ((.def_586 (ite .def_561 .def_585 .def_584)))
(let ((.def_568 (= _base 0)))
(let ((.def_587 (ite .def_568 0 .def_586)))
(let ((.def_589 (= .def_587 .def_588)))
.def_589
))))))))))))))))))))))))
(assert (let ((.def_575 (___z13z___ (- 1))))
(let ((.def_592 (= .def_575 0)))
(let ((.def_528 (___z12z___ (- 1))))
(let ((.def_529 (<= 1 .def_528)))
(let ((.def_593 (and .def_529 .def_592)))
(let ((.def_525 (___z15z___ (- 1))))
(let ((.def_591 (= .def_525 0)))
(let ((.def_594 (and .def_591 .def_593)))
(let ((.def_524 (___z14z___ (- 1))))
(let ((.def_590 (= .def_524 0)))
(let ((.def_595 (and .def_590 .def_594)))
(let ((.def_552 (___z23z___ 0)))
(let ((.def_596 (= .def_552 .def_595)))
.def_596
))))))))))))))
(assert (let ((.def_611 (___z14z___ 0)))
(let ((.def_524 (___z14z___ (- 1))))
(let ((.def_544 (___z25z___ 0)))
(let ((.def_597 (ite .def_544 0 .def_524)))
(let ((.def_546 (___z9z___ 0)))
(let ((.def_598 (ite .def_546 .def_597 .def_524)))
(let ((.def_599 (+ 1 .def_524)))
(let ((.def_573 (___z22z___ 0)))
(let ((.def_600 (ite .def_573 .def_599 .def_524)))
(let ((.def_601 (___z6z___ 0)))
(let ((.def_602 (ite .def_601 .def_600 .def_598)))
(let ((.def_603 (+ (- 1) .def_524)))
(let ((.def_541 (___z21z___ 0)))
(let ((.def_604 (ite .def_541 .def_603 .def_524)))
(let ((.def_583 (___z5z___ 0)))
(let ((.def_605 (ite .def_583 .def_604 .def_602)))
(let ((.def_531 (___z20z___ 0)))
(let ((.def_606 (ite .def_531 0 .def_524)))
(let ((.def_557 (___z4z___ 0)))
(let ((.def_607 (ite .def_557 .def_606 .def_605)))
(let ((.def_563 (___z18z___ 0)))
(let ((.def_608 (ite .def_563 .def_599 .def_524)))
(let ((.def_565 (___z2z___ 0)))
(let ((.def_609 (ite .def_565 .def_608 .def_607)))
(let ((.def_568 (= _base 0)))
(let ((.def_610 (ite .def_568 0 .def_609)))
(let ((.def_612 (= .def_610 .def_611)))
.def_612
))))))))))))))))))))))))))))
(assert (let ((.def_575 (___z13z___ (- 1))))
(let ((.def_613 (<= 1 .def_575)))
(let ((.def_528 (___z12z___ (- 1))))
(let ((.def_529 (<= 1 .def_528)))
(let ((.def_614 (and .def_529 .def_613)))
(let ((.def_548 (___z24z___ 0)))
(let ((.def_615 (= .def_548 .def_614)))
.def_615
))))))))
(assert (let ((.def_525 (___z15z___ (- 1))))
(let ((.def_524 (___z14z___ (- 1))))
(let ((.def_526 (+ .def_524 .def_525)))
(let ((.def_616 (+ 1 .def_526)))
(let ((.def_544 (___z25z___ 0)))
(let ((.def_617 (ite .def_544 .def_616 .def_525)))
(let ((.def_546 (___z9z___ 0)))
(let ((.def_618 (ite .def_546 .def_617 .def_525)))
(let ((.def_619 (+ 2 .def_525)))
(let ((.def_548 (___z24z___ 0)))
(let ((.def_620 (ite .def_548 .def_619 .def_525)))
(let ((.def_550 (___z8z___ 0)))
(let ((.def_621 (ite .def_550 .def_620 .def_618)))
(let ((.def_573 (___z22z___ 0)))
(let ((.def_622 (ite .def_573 0 .def_525)))
(let ((.def_601 (___z6z___ 0)))
(let ((.def_623 (ite .def_601 .def_622 .def_621)))
(let ((.def_624 (+ (- 1) .def_525)))
(let ((.def_625 (+ .def_524 .def_624)))
(let ((.def_626 (+ 1 .def_625)))
(let ((.def_531 (___z20z___ 0)))
(let ((.def_627 (ite .def_531 .def_626 .def_525)))
(let ((.def_557 (___z4z___ 0)))
(let ((.def_628 (ite .def_557 .def_627 .def_623)))
(let ((.def_559 (___z19z___ 0)))
(let ((.def_629 (ite .def_559 .def_619 .def_525)))
(let ((.def_561 (___z3z___ 0)))
(let ((.def_630 (ite .def_561 .def_629 .def_628)))
(let ((.def_568 (= _base 0)))
(let ((.def_631 (ite .def_568 0 .def_630)))
(let ((.def_535 (___z15z___ 0)))
(let ((.def_632 (= .def_535 .def_631)))
.def_632
)))))))))))))))))))))))))))))))))
(assert (let ((.def_544 (___z25z___ 0)))
(let ((.def_528 (___z12z___ (- 1))))
(let ((.def_529 (<= 1 .def_528)))
(let ((.def_525 (___z15z___ (- 1))))
(let ((.def_524 (___z14z___ (- 1))))
(let ((.def_526 (+ .def_524 .def_525)))
(let ((.def_527 (<= 1 .def_526)))
(let ((.def_530 (and .def_527 .def_529)))
(let ((.def_633 (= .def_530 .def_544)))
.def_633
))))))))))
(assert (let ((.def_637 (___z16z___ (- 1))))
(let ((.def_635 (___z27z___ 0)))
(let ((.def_638 (or .def_635 .def_637)))
(let ((.def_568 (= _base 0)))
(let ((.def_639 (or .def_568 .def_638)))
(let ((.def_634 (not .def_568)))
(let ((.def_636 (or .def_634 .def_635)))
(let ((.def_640 (and .def_636 .def_639)))
(let ((.def_533 (___z16z___ 0)))
(let ((.def_641 (= .def_533 .def_640)))
.def_641
)))))))))))
(assert (let ((.def_642 (___z26z___ (- 1))))
(let ((.def_643 (___z10z___ 0)))
(let ((.def_568 (= _base 0)))
(let ((.def_644 (ite .def_568 .def_643 .def_642)))
(let ((.def_567 (___z26z___ 0)))
(let ((.def_645 (= .def_567 .def_644)))
.def_645
)))))))
(assert (let ((.def_546 (___z9z___ 0)))
(let ((.def_664 (not .def_546)))
(let ((.def_565 (___z2z___ 0)))
(let ((.def_655 (not .def_565)))
(let ((.def_561 (___z3z___ 0)))
(let ((.def_654 (not .def_561)))
(let ((.def_656 (and .def_654 .def_655)))
(let ((.def_557 (___z4z___ 0)))
(let ((.def_653 (not .def_557)))
(let ((.def_657 (and .def_653 .def_656)))
(let ((.def_583 (___z5z___ 0)))
(let ((.def_652 (not .def_583)))
(let ((.def_658 (and .def_652 .def_657)))
(let ((.def_601 (___z6z___ 0)))
(let ((.def_651 (not .def_601)))
(let ((.def_659 (and .def_651 .def_658)))
(let ((.def_554 (___z7z___ 0)))
(let ((.def_650 (not .def_554)))
(let ((.def_660 (and .def_650 .def_659)))
(let ((.def_550 (___z8z___ 0)))
(let ((.def_649 (not .def_550)))
(let ((.def_661 (and .def_649 .def_660)))
(let ((.def_698 (and .def_661 .def_664)))
(let ((.def_691 (and .def_565 .def_654)))
(let ((.def_692 (and .def_653 .def_691)))
(let ((.def_693 (and .def_652 .def_692)))
(let ((.def_694 (and .def_651 .def_693)))
(let ((.def_695 (and .def_650 .def_694)))
(let ((.def_696 (and .def_649 .def_695)))
(let ((.def_697 (and .def_664 .def_696)))
(let ((.def_699 (or .def_697 .def_698)))
(let ((.def_684 (and .def_561 .def_655)))
(let ((.def_685 (and .def_653 .def_684)))
(let ((.def_686 (and .def_652 .def_685)))
(let ((.def_687 (and .def_651 .def_686)))
(let ((.def_688 (and .def_650 .def_687)))
(let ((.def_689 (and .def_649 .def_688)))
(let ((.def_690 (and .def_664 .def_689)))
(let ((.def_700 (or .def_690 .def_699)))
(let ((.def_678 (and .def_557 .def_656)))
(let ((.def_679 (and .def_652 .def_678)))
(let ((.def_680 (and .def_651 .def_679)))
(let ((.def_681 (and .def_650 .def_680)))
(let ((.def_682 (and .def_649 .def_681)))
(let ((.def_683 (and .def_664 .def_682)))
(let ((.def_701 (or .def_683 .def_700)))
(let ((.def_673 (and .def_583 .def_657)))
(let ((.def_674 (and .def_651 .def_673)))
(let ((.def_675 (and .def_650 .def_674)))
(let ((.def_676 (and .def_649 .def_675)))
(let ((.def_677 (and .def_664 .def_676)))
(let ((.def_702 (or .def_677 .def_701)))
(let ((.def_669 (and .def_601 .def_658)))
(let ((.def_670 (and .def_650 .def_669)))
(let ((.def_671 (and .def_649 .def_670)))
(let ((.def_672 (and .def_664 .def_671)))
(let ((.def_703 (or .def_672 .def_702)))
(let ((.def_666 (and .def_554 .def_659)))
(let ((.def_667 (and .def_649 .def_666)))
(let ((.def_668 (and .def_664 .def_667)))
(let ((.def_704 (or .def_668 .def_703)))
(let ((.def_663 (and .def_550 .def_660)))
(let ((.def_665 (and .def_663 .def_664)))
(let ((.def_705 (or .def_665 .def_704)))
(let ((.def_662 (and .def_546 .def_661)))
(let ((.def_706 (or .def_662 .def_705)))
(let ((.def_643 (___z10z___ 0)))
(let ((.def_648 (<= 0 .def_643)))
(let ((.def_707 (and .def_648 .def_706)))
(let ((.def_646 (<= 5 .def_643)))
(let ((.def_647 (not .def_646)))
(let ((.def_708 (and .def_647 .def_707)))
(let ((.def_635 (___z27z___ 0)))
(let ((.def_709 (= .def_635 .def_708)))
.def_709
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(assert (let ((.def_575 (___z13z___ (- 1))))
(let ((.def_592 (= .def_575 0)))
(let ((.def_528 (___z12z___ (- 1))))
(let ((.def_529 (<= 1 .def_528)))
(let ((.def_593 (and .def_529 .def_592)))
(let ((.def_525 (___z15z___ (- 1))))
(let ((.def_591 (= .def_525 0)))
(let ((.def_594 (and .def_591 .def_593)))
(let ((.def_524 (___z14z___ (- 1))))
(let ((.def_590 (= .def_524 0)))
(let ((.def_595 (and .def_590 .def_594)))
(let ((.def_563 (___z18z___ 0)))
(let ((.def_710 (= .def_563 .def_595)))
.def_710
))))))))))))))
(assert (let ((.def_575 (___z13z___ (- 1))))
(let ((.def_613 (<= 1 .def_575)))
(let ((.def_528 (___z12z___ (- 1))))
(let ((.def_529 (<= 1 .def_528)))
(let ((.def_614 (and .def_529 .def_613)))
(let ((.def_559 (___z19z___ 0)))
(let ((.def_711 (= .def_559 .def_614)))
.def_711
))))))))
(assert (let ((.def_720 (___z20z___ (- 1))))
(let ((.def_717 (___z12z___ (- 2))))
(let ((.def_718 (<= 1 .def_717)))
(let ((.def_714 (___z15z___ (- 2))))
(let ((.def_713 (___z14z___ (- 2))))
(let ((.def_715 (+ .def_713 .def_714)))
(let ((.def_716 (<= 1 .def_715)))
(let ((.def_719 (and .def_716 .def_718)))
(let ((.def_721 (= .def_719 .def_720)))
.def_721
))))))))))
(assert (let ((.def_725 (___z11z___ (- 1))))
(let ((.def_525 (___z15z___ (- 1))))
(let ((.def_723 (<= 0 .def_525)))
(let ((.def_637 (___z16z___ (- 1))))
(let ((.def_722 (not .def_637)))
(let ((.def_724 (or .def_722 .def_723)))
(let ((.def_726 (= .def_724 .def_725)))
.def_726
))))))))
(assert (let ((.def_728 (___z21z___ (- 1))))
(let ((.def_713 (___z14z___ (- 2))))
(let ((.def_727 (<= 1 .def_713)))
(let ((.def_729 (= .def_727 .def_728)))
.def_729
)))))
(assert (let ((.def_717 (___z12z___ (- 2))))
(let ((.def_730 (+ (- 1) .def_717)))
(let ((.def_731 (___z25z___ (- 1))))
(let ((.def_732 (ite .def_731 .def_730 .def_717)))
(let ((.def_733 (___z9z___ (- 1))))
(let ((.def_734 (ite .def_733 .def_732 .def_717)))
(let ((.def_735 (___z24z___ (- 1))))
(let ((.def_736 (ite .def_735 .def_730 .def_717)))
(let ((.def_737 (___z8z___ (- 1))))
(let ((.def_738 (ite .def_737 .def_736 .def_734)))
(let ((.def_739 (___z23z___ (- 1))))
(let ((.def_740 (ite .def_739 .def_730 .def_717)))
(let ((.def_741 (___z7z___ (- 1))))
(let ((.def_742 (ite .def_741 .def_740 .def_738)))
(let ((.def_720 (___z20z___ (- 1))))
(let ((.def_743 (ite .def_720 .def_730 .def_717)))
(let ((.def_744 (___z4z___ (- 1))))
(let ((.def_745 (ite .def_744 .def_743 .def_742)))
(let ((.def_746 (___z19z___ (- 1))))
(let ((.def_747 (ite .def_746 .def_730 .def_717)))
(let ((.def_748 (___z3z___ (- 1))))
(let ((.def_749 (ite .def_748 .def_747 .def_745)))
(let ((.def_750 (___z18z___ (- 1))))
(let ((.def_751 (ite .def_750 .def_730 .def_717)))
(let ((.def_752 (___z2z___ (- 1))))
(let ((.def_753 (ite .def_752 .def_751 .def_749)))
(let ((.def_642 (___z26z___ (- 1))))
(let ((.def_754 (= _base (- 1))))
(let ((.def_755 (ite .def_754 .def_642 .def_753)))
(let ((.def_528 (___z12z___ (- 1))))
(let ((.def_756 (= .def_528 .def_755)))
.def_756
))))))))))))))))))))))))))))))))
(assert (let ((.def_758 (___z22z___ (- 1))))
(let ((.def_714 (___z15z___ (- 2))))
(let ((.def_757 (= .def_714 1)))
(let ((.def_759 (= .def_757 .def_758)))
.def_759
)))))
(assert (let ((.def_760 (___z13z___ (- 2))))
(let ((.def_761 (+ (- 1) .def_760)))
(let ((.def_735 (___z24z___ (- 1))))
(let ((.def_762 (ite .def_735 .def_761 .def_760)))
(let ((.def_737 (___z8z___ (- 1))))
(let ((.def_763 (ite .def_737 .def_762 .def_760)))
(let ((.def_739 (___z23z___ (- 1))))
(let ((.def_764 (ite .def_739 1 .def_760)))
(let ((.def_741 (___z7z___ (- 1))))
(let ((.def_765 (ite .def_741 .def_764 .def_763)))
(let ((.def_766 (+ 1 .def_760)))
(let ((.def_728 (___z21z___ (- 1))))
(let ((.def_767 (ite .def_728 .def_766 .def_760)))
(let ((.def_768 (___z5z___ (- 1))))
(let ((.def_769 (ite .def_768 .def_767 .def_765)))
(let ((.def_746 (___z19z___ (- 1))))
(let ((.def_770 (ite .def_746 .def_761 .def_760)))
(let ((.def_748 (___z3z___ (- 1))))
(let ((.def_771 (ite .def_748 .def_770 .def_769)))
(let ((.def_754 (= _base (- 1))))
(let ((.def_772 (ite .def_754 0 .def_771)))
(let ((.def_575 (___z13z___ (- 1))))
(let ((.def_773 (= .def_575 .def_772)))
.def_773
))))))))))))))))))))))))
(assert (let ((.def_760 (___z13z___ (- 2))))
(let ((.def_776 (= .def_760 0)))
(let ((.def_717 (___z12z___ (- 2))))
(let ((.def_718 (<= 1 .def_717)))
(let ((.def_777 (and .def_718 .def_776)))
(let ((.def_714 (___z15z___ (- 2))))
(let ((.def_775 (= .def_714 0)))
(let ((.def_778 (and .def_775 .def_777)))
(let ((.def_713 (___z14z___ (- 2))))
(let ((.def_774 (= .def_713 0)))
(let ((.def_779 (and .def_774 .def_778)))
(let ((.def_739 (___z23z___ (- 1))))
(let ((.def_780 (= .def_739 .def_779)))
.def_780
))))))))))))))
(assert (let ((.def_713 (___z14z___ (- 2))))
(let ((.def_731 (___z25z___ (- 1))))
(let ((.def_781 (ite .def_731 0 .def_713)))
(let ((.def_733 (___z9z___ (- 1))))
(let ((.def_782 (ite .def_733 .def_781 .def_713)))
(let ((.def_783 (+ 1 .def_713)))
(let ((.def_758 (___z22z___ (- 1))))
(let ((.def_784 (ite .def_758 .def_783 .def_713)))
(let ((.def_785 (___z6z___ (- 1))))
(let ((.def_786 (ite .def_785 .def_784 .def_782)))
(let ((.def_787 (+ (- 1) .def_713)))
(let ((.def_728 (___z21z___ (- 1))))
(let ((.def_788 (ite .def_728 .def_787 .def_713)))
(let ((.def_768 (___z5z___ (- 1))))
(let ((.def_789 (ite .def_768 .def_788 .def_786)))
(let ((.def_720 (___z20z___ (- 1))))
(let ((.def_790 (ite .def_720 0 .def_713)))
(let ((.def_744 (___z4z___ (- 1))))
(let ((.def_791 (ite .def_744 .def_790 .def_789)))
(let ((.def_750 (___z18z___ (- 1))))
(let ((.def_792 (ite .def_750 .def_783 .def_713)))
(let ((.def_752 (___z2z___ (- 1))))
(let ((.def_793 (ite .def_752 .def_792 .def_791)))
(let ((.def_754 (= _base (- 1))))
(let ((.def_794 (ite .def_754 0 .def_793)))
(let ((.def_524 (___z14z___ (- 1))))
(let ((.def_795 (= .def_524 .def_794)))
.def_795
))))))))))))))))))))))))))))
(assert (let ((.def_760 (___z13z___ (- 2))))
(let ((.def_796 (<= 1 .def_760)))
(let ((.def_717 (___z12z___ (- 2))))
(let ((.def_718 (<= 1 .def_717)))
(let ((.def_797 (and .def_718 .def_796)))
(let ((.def_735 (___z24z___ (- 1))))
(let ((.def_798 (= .def_735 .def_797)))
.def_798
))))))))
(assert (let ((.def_714 (___z15z___ (- 2))))
(let ((.def_713 (___z14z___ (- 2))))
(let ((.def_715 (+ .def_713 .def_714)))
(let ((.def_799 (+ 1 .def_715)))
(let ((.def_731 (___z25z___ (- 1))))
(let ((.def_800 (ite .def_731 .def_799 .def_714)))
(let ((.def_733 (___z9z___ (- 1))))
(let ((.def_801 (ite .def_733 .def_800 .def_714)))
(let ((.def_802 (+ 2 .def_714)))
(let ((.def_735 (___z24z___ (- 1))))
(let ((.def_803 (ite .def_735 .def_802 .def_714)))
(let ((.def_737 (___z8z___ (- 1))))
(let ((.def_804 (ite .def_737 .def_803 .def_801)))
(let ((.def_758 (___z22z___ (- 1))))
(let ((.def_805 (ite .def_758 0 .def_714)))
(let ((.def_785 (___z6z___ (- 1))))
(let ((.def_806 (ite .def_785 .def_805 .def_804)))
(let ((.def_807 (+ (- 1) .def_714)))
(let ((.def_808 (+ .def_713 .def_807)))
(let ((.def_809 (+ 1 .def_808)))
(let ((.def_720 (___z20z___ (- 1))))
(let ((.def_810 (ite .def_720 .def_809 .def_714)))
(let ((.def_744 (___z4z___ (- 1))))
(let ((.def_811 (ite .def_744 .def_810 .def_806)))
(let ((.def_746 (___z19z___ (- 1))))
(let ((.def_812 (ite .def_746 .def_802 .def_714)))
(let ((.def_748 (___z3z___ (- 1))))
(let ((.def_813 (ite .def_748 .def_812 .def_811)))
(let ((.def_754 (= _base (- 1))))
(let ((.def_814 (ite .def_754 0 .def_813)))
(let ((.def_525 (___z15z___ (- 1))))
(let ((.def_815 (= .def_525 .def_814)))
.def_815
)))))))))))))))))))))))))))))))))
(assert (let ((.def_731 (___z25z___ (- 1))))
(let ((.def_717 (___z12z___ (- 2))))
(let ((.def_718 (<= 1 .def_717)))
(let ((.def_714 (___z15z___ (- 2))))
(let ((.def_713 (___z14z___ (- 2))))
(let ((.def_715 (+ .def_713 .def_714)))
(let ((.def_716 (<= 1 .def_715)))
(let ((.def_719 (and .def_716 .def_718)))
(let ((.def_816 (= .def_719 .def_731)))
.def_816
))))))))))
(assert (let ((.def_820 (___z16z___ (- 2))))
(let ((.def_818 (___z27z___ (- 1))))
(let ((.def_821 (or .def_818 .def_820)))
(let ((.def_754 (= _base (- 1))))
(let ((.def_822 (or .def_754 .def_821)))
(let ((.def_817 (not .def_754)))
(let ((.def_819 (or .def_817 .def_818)))
(let ((.def_823 (and .def_819 .def_822)))
(let ((.def_637 (___z16z___ (- 1))))
(let ((.def_824 (= .def_637 .def_823)))
.def_824
)))))))))))
(assert (let ((.def_825 (___z26z___ (- 2))))
(let ((.def_826 (___z10z___ (- 1))))
(let ((.def_754 (= _base (- 1))))
(let ((.def_827 (ite .def_754 .def_826 .def_825)))
(let ((.def_642 (___z26z___ (- 1))))
(let ((.def_828 (= .def_642 .def_827)))
.def_828
)))))))
(assert (let ((.def_733 (___z9z___ (- 1))))
(let ((.def_847 (not .def_733)))
(let ((.def_752 (___z2z___ (- 1))))
(let ((.def_838 (not .def_752)))
(let ((.def_748 (___z3z___ (- 1))))
(let ((.def_837 (not .def_748)))
(let ((.def_839 (and .def_837 .def_838)))
(let ((.def_744 (___z4z___ (- 1))))
(let ((.def_836 (not .def_744)))
(let ((.def_840 (and .def_836 .def_839)))
(let ((.def_768 (___z5z___ (- 1))))
(let ((.def_835 (not .def_768)))
(let ((.def_841 (and .def_835 .def_840)))
(let ((.def_785 (___z6z___ (- 1))))
(let ((.def_834 (not .def_785)))
(let ((.def_842 (and .def_834 .def_841)))
(let ((.def_741 (___z7z___ (- 1))))
(let ((.def_833 (not .def_741)))
(let ((.def_843 (and .def_833 .def_842)))
(let ((.def_737 (___z8z___ (- 1))))
(let ((.def_832 (not .def_737)))
(let ((.def_844 (and .def_832 .def_843)))
(let ((.def_881 (and .def_844 .def_847)))
(let ((.def_874 (and .def_752 .def_837)))
(let ((.def_875 (and .def_836 .def_874)))
(let ((.def_876 (and .def_835 .def_875)))
(let ((.def_877 (and .def_834 .def_876)))
(let ((.def_878 (and .def_833 .def_877)))
(let ((.def_879 (and .def_832 .def_878)))
(let ((.def_880 (and .def_847 .def_879)))
(let ((.def_882 (or .def_880 .def_881)))
(let ((.def_867 (and .def_748 .def_838)))
(let ((.def_868 (and .def_836 .def_867)))
(let ((.def_869 (and .def_835 .def_868)))
(let ((.def_870 (and .def_834 .def_869)))
(let ((.def_871 (and .def_833 .def_870)))
(let ((.def_872 (and .def_832 .def_871)))
(let ((.def_873 (and .def_847 .def_872)))
(let ((.def_883 (or .def_873 .def_882)))
(let ((.def_861 (and .def_744 .def_839)))
(let ((.def_862 (and .def_835 .def_861)))
(let ((.def_863 (and .def_834 .def_862)))
(let ((.def_864 (and .def_833 .def_863)))
(let ((.def_865 (and .def_832 .def_864)))
(let ((.def_866 (and .def_847 .def_865)))
(let ((.def_884 (or .def_866 .def_883)))
(let ((.def_856 (and .def_768 .def_840)))
(let ((.def_857 (and .def_834 .def_856)))
(let ((.def_858 (and .def_833 .def_857)))
(let ((.def_859 (and .def_832 .def_858)))
(let ((.def_860 (and .def_847 .def_859)))
(let ((.def_885 (or .def_860 .def_884)))
(let ((.def_852 (and .def_785 .def_841)))
(let ((.def_853 (and .def_833 .def_852)))
(let ((.def_854 (and .def_832 .def_853)))
(let ((.def_855 (and .def_847 .def_854)))
(let ((.def_886 (or .def_855 .def_885)))
(let ((.def_849 (and .def_741 .def_842)))
(let ((.def_850 (and .def_832 .def_849)))
(let ((.def_851 (and .def_847 .def_850)))
(let ((.def_887 (or .def_851 .def_886)))
(let ((.def_846 (and .def_737 .def_843)))
(let ((.def_848 (and .def_846 .def_847)))
(let ((.def_888 (or .def_848 .def_887)))
(let ((.def_845 (and .def_733 .def_844)))
(let ((.def_889 (or .def_845 .def_888)))
(let ((.def_826 (___z10z___ (- 1))))
(let ((.def_831 (<= 0 .def_826)))
(let ((.def_890 (and .def_831 .def_889)))
(let ((.def_829 (<= 5 .def_826)))
(let ((.def_830 (not .def_829)))
(let ((.def_891 (and .def_830 .def_890)))
(let ((.def_818 (___z27z___ (- 1))))
(let ((.def_892 (= .def_818 .def_891)))
.def_892
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(assert (let ((.def_760 (___z13z___ (- 2))))
(let ((.def_776 (= .def_760 0)))
(let ((.def_717 (___z12z___ (- 2))))
(let ((.def_718 (<= 1 .def_717)))
(let ((.def_777 (and .def_718 .def_776)))
(let ((.def_714 (___z15z___ (- 2))))
(let ((.def_775 (= .def_714 0)))
(let ((.def_778 (and .def_775 .def_777)))
(let ((.def_713 (___z14z___ (- 2))))
(let ((.def_774 (= .def_713 0)))
(let ((.def_779 (and .def_774 .def_778)))
(let ((.def_750 (___z18z___ (- 1))))
(let ((.def_893 (= .def_750 .def_779)))
.def_893
))))))))))))))
(assert (let ((.def_760 (___z13z___ (- 2))))
(let ((.def_796 (<= 1 .def_760)))
(let ((.def_717 (___z12z___ (- 2))))
(let ((.def_718 (<= 1 .def_717)))
(let ((.def_797 (and .def_718 .def_796)))
(let ((.def_746 (___z19z___ (- 1))))
(let ((.def_894 (= .def_746 .def_797)))
.def_894
))))))))
(push 1)
(assert (let ((.def_725 (___z11z___ (- 1))))
(let ((.def_538 (___z11z___ 0)))
(let ((.def_895 (and .def_538 .def_725)))
(let ((.def_754 (= _base (- 1))))
(let ((.def_817 (not .def_754)))
(let ((.def_896 (or .def_817 .def_895)))
(let ((.def_897 (not .def_896)))
.def_897
))))))))
(assert true
)
(check-sat)
(pop 1)
(assert (let ((.def_725 (___z11z___ (- 1))))
.def_725
))
(assert (let ((.def_898 (___z11z___ (- 2))))
.def_898
))
(push 1)
(assert (let ((.def_907 (___z20z___ _n)))
(let ((.def_899 (+ _n (- 1))))
(let ((.def_904 (___z12z___ .def_899)))
(let ((.def_905 (<= 1 .def_904)))
(let ((.def_901 (___z15z___ .def_899)))
(let ((.def_900 (___z14z___ .def_899)))
(let ((.def_902 (+ .def_900 .def_901)))
(let ((.def_903 (<= 1 .def_902)))
(let ((.def_906 (and .def_903 .def_905)))
(let ((.def_908 (= .def_906 .def_907)))
.def_908
)))))))))))
(assert (let ((.def_914 (___z11z___ _n)))
(let ((.def_911 (___z15z___ _n)))
(let ((.def_912 (<= 0 .def_911)))
(let ((.def_909 (___z16z___ _n)))
(let ((.def_910 (not .def_909)))
(let ((.def_913 (or .def_910 .def_912)))
(let ((.def_915 (= .def_913 .def_914)))
.def_915
))))))))
(assert (let ((.def_917 (___z21z___ _n)))
(let ((.def_899 (+ _n (- 1))))
(let ((.def_900 (___z14z___ .def_899)))
(let ((.def_916 (<= 1 .def_900)))
(let ((.def_918 (= .def_916 .def_917)))
.def_918
))))))
(assert (let ((.def_946 (___z12z___ _n)))
(let ((.def_899 (+ _n (- 1))))
(let ((.def_904 (___z12z___ .def_899)))
(let ((.def_919 (+ (- 1) .def_904)))
(let ((.def_920 (___z25z___ _n)))
(let ((.def_921 (ite .def_920 .def_919 .def_904)))
(let ((.def_922 (___z9z___ _n)))
(let ((.def_923 (ite .def_922 .def_921 .def_904)))
(let ((.def_924 (___z24z___ _n)))
(let ((.def_925 (ite .def_924 .def_919 .def_904)))
(let ((.def_926 (___z8z___ _n)))
(let ((.def_927 (ite .def_926 .def_925 .def_923)))
(let ((.def_928 (___z23z___ _n)))
(let ((.def_929 (ite .def_928 .def_919 .def_904)))
(let ((.def_930 (___z7z___ _n)))
(let ((.def_931 (ite .def_930 .def_929 .def_927)))
(let ((.def_907 (___z20z___ _n)))
(let ((.def_932 (ite .def_907 .def_919 .def_904)))
(let ((.def_933 (___z4z___ _n)))
(let ((.def_934 (ite .def_933 .def_932 .def_931)))
(let ((.def_935 (___z19z___ _n)))
(let ((.def_936 (ite .def_935 .def_919 .def_904)))
(let ((.def_937 (___z3z___ _n)))
(let ((.def_938 (ite .def_937 .def_936 .def_934)))
(let ((.def_939 (___z18z___ _n)))
(let ((.def_940 (ite .def_939 .def_919 .def_904)))
(let ((.def_941 (___z2z___ _n)))
(let ((.def_942 (ite .def_941 .def_940 .def_938)))
(let ((.def_943 (___z26z___ _n)))
(let ((.def_944 (= _n _base)))
(let ((.def_945 (ite .def_944 .def_943 .def_942)))
(let ((.def_947 (= .def_945 .def_946)))
.def_947
)))))))))))))))))))))))))))))))))
(assert (let ((.def_949 (___z22z___ _n)))
(let ((.def_899 (+ _n (- 1))))
(let ((.def_901 (___z15z___ .def_899)))
(let ((.def_948 (= .def_901 1)))
(let ((.def_950 (= .def_948 .def_949)))
.def_950
))))))
(assert (let ((.def_964 (___z13z___ _n)))
(let ((.def_899 (+ _n (- 1))))
(let ((.def_951 (___z13z___ .def_899)))
(let ((.def_952 (+ (- 1) .def_951)))
(let ((.def_924 (___z24z___ _n)))
(let ((.def_953 (ite .def_924 .def_952 .def_951)))
(let ((.def_926 (___z8z___ _n)))
(let ((.def_954 (ite .def_926 .def_953 .def_951)))
(let ((.def_928 (___z23z___ _n)))
(let ((.def_955 (ite .def_928 1 .def_951)))
(let ((.def_930 (___z7z___ _n)))
(let ((.def_956 (ite .def_930 .def_955 .def_954)))
(let ((.def_957 (+ 1 .def_951)))
(let ((.def_917 (___z21z___ _n)))
(let ((.def_958 (ite .def_917 .def_957 .def_951)))
(let ((.def_959 (___z5z___ _n)))
(let ((.def_960 (ite .def_959 .def_958 .def_956)))
(let ((.def_935 (___z19z___ _n)))
(let ((.def_961 (ite .def_935 .def_952 .def_951)))
(let ((.def_937 (___z3z___ _n)))
(let ((.def_962 (ite .def_937 .def_961 .def_960)))
(let ((.def_944 (= _n _base)))
(let ((.def_963 (ite .def_944 0 .def_962)))
(let ((.def_965 (= .def_963 .def_964)))
.def_965
)))))))))))))))))))))))))
(assert (let ((.def_899 (+ _n (- 1))))
(let ((.def_951 (___z13z___ .def_899)))
(let ((.def_968 (= .def_951 0)))
(let ((.def_904 (___z12z___ .def_899)))
(let ((.def_905 (<= 1 .def_904)))
(let ((.def_969 (and .def_905 .def_968)))
(let ((.def_901 (___z15z___ .def_899)))
(let ((.def_967 (= .def_901 0)))
(let ((.def_970 (and .def_967 .def_969)))
(let ((.def_900 (___z14z___ .def_899)))
(let ((.def_966 (= .def_900 0)))
(let ((.def_971 (and .def_966 .def_970)))
(let ((.def_928 (___z23z___ _n)))
(let ((.def_972 (= .def_928 .def_971)))
.def_972
)))))))))))))))
(assert (let ((.def_987 (___z14z___ _n)))
(let ((.def_899 (+ _n (- 1))))
(let ((.def_900 (___z14z___ .def_899)))
(let ((.def_920 (___z25z___ _n)))
(let ((.def_973 (ite .def_920 0 .def_900)))
(let ((.def_922 (___z9z___ _n)))
(let ((.def_974 (ite .def_922 .def_973 .def_900)))
(let ((.def_975 (+ 1 .def_900)))
(let ((.def_949 (___z22z___ _n)))
(let ((.def_976 (ite .def_949 .def_975 .def_900)))
(let ((.def_977 (___z6z___ _n)))
(let ((.def_978 (ite .def_977 .def_976 .def_974)))
(let ((.def_979 (+ (- 1) .def_900)))
(let ((.def_917 (___z21z___ _n)))
(let ((.def_980 (ite .def_917 .def_979 .def_900)))
(let ((.def_959 (___z5z___ _n)))
(let ((.def_981 (ite .def_959 .def_980 .def_978)))
(let ((.def_907 (___z20z___ _n)))
(let ((.def_982 (ite .def_907 0 .def_900)))
(let ((.def_933 (___z4z___ _n)))
(let ((.def_983 (ite .def_933 .def_982 .def_981)))
(let ((.def_939 (___z18z___ _n)))
(let ((.def_984 (ite .def_939 .def_975 .def_900)))
(let ((.def_941 (___z2z___ _n)))
(let ((.def_985 (ite .def_941 .def_984 .def_983)))
(let ((.def_944 (= _n _base)))
(let ((.def_986 (ite .def_944 0 .def_985)))
(let ((.def_988 (= .def_986 .def_987)))
.def_988
)))))))))))))))))))))))))))))
(assert (let ((.def_899 (+ _n (- 1))))
(let ((.def_951 (___z13z___ .def_899)))
(let ((.def_989 (<= 1 .def_951)))
(let ((.def_904 (___z12z___ .def_899)))
(let ((.def_905 (<= 1 .def_904)))
(let ((.def_990 (and .def_905 .def_989)))
(let ((.def_924 (___z24z___ _n)))
(let ((.def_991 (= .def_924 .def_990)))
.def_991
)))))))))
(assert (let ((.def_899 (+ _n (- 1))))
(let ((.def_901 (___z15z___ .def_899)))
(let ((.def_900 (___z14z___ .def_899)))
(let ((.def_902 (+ .def_900 .def_901)))
(let ((.def_992 (+ 1 .def_902)))
(let ((.def_920 (___z25z___ _n)))
(let ((.def_993 (ite .def_920 .def_992 .def_901)))
(let ((.def_922 (___z9z___ _n)))
(let ((.def_994 (ite .def_922 .def_993 .def_901)))
(let ((.def_995 (+ 2 .def_901)))
(let ((.def_924 (___z24z___ _n)))
(let ((.def_996 (ite .def_924 .def_995 .def_901)))
(let ((.def_926 (___z8z___ _n)))
(let ((.def_997 (ite .def_926 .def_996 .def_994)))
(let ((.def_949 (___z22z___ _n)))
(let ((.def_998 (ite .def_949 0 .def_901)))
(let ((.def_977 (___z6z___ _n)))
(let ((.def_999 (ite .def_977 .def_998 .def_997)))
(let ((.def_1000 (+ (- 1) .def_901)))
(let ((.def_1001 (+ .def_900 .def_1000)))
(let ((.def_1002 (+ 1 .def_1001)))
(let ((.def_907 (___z20z___ _n)))
(let ((.def_1003 (ite .def_907 .def_1002 .def_901)))
(let ((.def_933 (___z4z___ _n)))
(let ((.def_1004 (ite .def_933 .def_1003 .def_999)))
(let ((.def_935 (___z19z___ _n)))
(let ((.def_1005 (ite .def_935 .def_995 .def_901)))
(let ((.def_937 (___z3z___ _n)))
(let ((.def_1006 (ite .def_937 .def_1005 .def_1004)))
(let ((.def_944 (= _n _base)))
(let ((.def_1007 (ite .def_944 0 .def_1006)))
(let ((.def_911 (___z15z___ _n)))
(let ((.def_1008 (= .def_911 .def_1007)))
.def_1008
))))))))))))))))))))))))))))))))))
(assert (let ((.def_920 (___z25z___ _n)))
(let ((.def_899 (+ _n (- 1))))
(let ((.def_904 (___z12z___ .def_899)))
(let ((.def_905 (<= 1 .def_904)))
(let ((.def_901 (___z15z___ .def_899)))
(let ((.def_900 (___z14z___ .def_899)))
(let ((.def_902 (+ .def_900 .def_901)))
(let ((.def_903 (<= 1 .def_902)))
(let ((.def_906 (and .def_903 .def_905)))
(let ((.def_1009 (= .def_906 .def_920)))
.def_1009
)))))))))))
(assert (let ((.def_899 (+ _n (- 1))))
(let ((.def_1013 (___z16z___ .def_899)))
(let ((.def_1011 (___z27z___ _n)))
(let ((.def_1014 (or .def_1011 .def_1013)))
(let ((.def_944 (= _n _base)))
(let ((.def_1015 (or .def_944 .def_1014)))
(let ((.def_1010 (not .def_944)))
(let ((.def_1012 (or .def_1010 .def_1011)))
(let ((.def_1016 (and .def_1012 .def_1015)))
(let ((.def_909 (___z16z___ _n)))
(let ((.def_1017 (= .def_909 .def_1016)))
.def_1017
))))))))))))
(assert (let ((.def_899 (+ _n (- 1))))
(let ((.def_1018 (___z26z___ .def_899)))
(let ((.def_1019 (___z10z___ _n)))
(let ((.def_944 (= _n _base)))
(let ((.def_1020 (ite .def_944 .def_1019 .def_1018)))
(let ((.def_943 (___z26z___ _n)))
(let ((.def_1021 (= .def_943 .def_1020)))
.def_1021
))))))))
(assert (let ((.def_922 (___z9z___ _n)))
(let ((.def_1040 (not .def_922)))
(let ((.def_941 (___z2z___ _n)))
(let ((.def_1031 (not .def_941)))
(let ((.def_937 (___z3z___ _n)))
(let ((.def_1030 (not .def_937)))
(let ((.def_1032 (and .def_1030 .def_1031)))
(let ((.def_933 (___z4z___ _n)))
(let ((.def_1029 (not .def_933)))
(let ((.def_1033 (and .def_1029 .def_1032)))
(let ((.def_959 (___z5z___ _n)))
(let ((.def_1028 (not .def_959)))
(let ((.def_1034 (and .def_1028 .def_1033)))
(let ((.def_977 (___z6z___ _n)))
(let ((.def_1027 (not .def_977)))
(let ((.def_1035 (and .def_1027 .def_1034)))
(let ((.def_930 (___z7z___ _n)))
(let ((.def_1026 (not .def_930)))
(let ((.def_1036 (and .def_1026 .def_1035)))
(let ((.def_926 (___z8z___ _n)))
(let ((.def_1025 (not .def_926)))
(let ((.def_1037 (and .def_1025 .def_1036)))
(let ((.def_1074 (and .def_1037 .def_1040)))
(let ((.def_1067 (and .def_941 .def_1030)))
(let ((.def_1068 (and .def_1029 .def_1067)))
(let ((.def_1069 (and .def_1028 .def_1068)))
(let ((.def_1070 (and .def_1027 .def_1069)))
(let ((.def_1071 (and .def_1026 .def_1070)))
(let ((.def_1072 (and .def_1025 .def_1071)))
(let ((.def_1073 (and .def_1040 .def_1072)))
(let ((.def_1075 (or .def_1073 .def_1074)))
(let ((.def_1060 (and .def_937 .def_1031)))
(let ((.def_1061 (and .def_1029 .def_1060)))
(let ((.def_1062 (and .def_1028 .def_1061)))
(let ((.def_1063 (and .def_1027 .def_1062)))
(let ((.def_1064 (and .def_1026 .def_1063)))
(let ((.def_1065 (and .def_1025 .def_1064)))
(let ((.def_1066 (and .def_1040 .def_1065)))
(let ((.def_1076 (or .def_1066 .def_1075)))
(let ((.def_1054 (and .def_933 .def_1032)))
(let ((.def_1055 (and .def_1028 .def_1054)))
(let ((.def_1056 (and .def_1027 .def_1055)))
(let ((.def_1057 (and .def_1026 .def_1056)))
(let ((.def_1058 (and .def_1025 .def_1057)))
(let ((.def_1059 (and .def_1040 .def_1058)))
(let ((.def_1077 (or .def_1059 .def_1076)))
(let ((.def_1049 (and .def_959 .def_1033)))
(let ((.def_1050 (and .def_1027 .def_1049)))
(let ((.def_1051 (and .def_1026 .def_1050)))
(let ((.def_1052 (and .def_1025 .def_1051)))
(let ((.def_1053 (and .def_1040 .def_1052)))
(let ((.def_1078 (or .def_1053 .def_1077)))
(let ((.def_1045 (and .def_977 .def_1034)))
(let ((.def_1046 (and .def_1026 .def_1045)))
(let ((.def_1047 (and .def_1025 .def_1046)))
(let ((.def_1048 (and .def_1040 .def_1047)))
(let ((.def_1079 (or .def_1048 .def_1078)))
(let ((.def_1042 (and .def_930 .def_1035)))
(let ((.def_1043 (and .def_1025 .def_1042)))
(let ((.def_1044 (and .def_1040 .def_1043)))
(let ((.def_1080 (or .def_1044 .def_1079)))
(let ((.def_1039 (and .def_926 .def_1036)))
(let ((.def_1041 (and .def_1039 .def_1040)))
(let ((.def_1081 (or .def_1041 .def_1080)))
(let ((.def_1038 (and .def_922 .def_1037)))
(let ((.def_1082 (or .def_1038 .def_1081)))
(let ((.def_1019 (___z10z___ _n)))
(let ((.def_1024 (<= 0 .def_1019)))
(let ((.def_1083 (and .def_1024 .def_1082)))
(let ((.def_1022 (<= 5 .def_1019)))
(let ((.def_1023 (not .def_1022)))
(let ((.def_1084 (and .def_1023 .def_1083)))
(let ((.def_1011 (___z27z___ _n)))
(let ((.def_1085 (= .def_1011 .def_1084)))
.def_1085
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(assert (let ((.def_899 (+ _n (- 1))))
(let ((.def_951 (___z13z___ .def_899)))
(let ((.def_968 (= .def_951 0)))
(let ((.def_904 (___z12z___ .def_899)))
(let ((.def_905 (<= 1 .def_904)))
(let ((.def_969 (and .def_905 .def_968)))
(let ((.def_901 (___z15z___ .def_899)))
(let ((.def_967 (= .def_901 0)))
(let ((.def_970 (and .def_967 .def_969)))
(let ((.def_900 (___z14z___ .def_899)))
(let ((.def_966 (= .def_900 0)))
(let ((.def_971 (and .def_966 .def_970)))
(let ((.def_939 (___z18z___ _n)))
(let ((.def_1086 (= .def_939 .def_971)))
.def_1086
)))))))))))))))
(assert (let ((.def_899 (+ _n (- 1))))
(let ((.def_951 (___z13z___ .def_899)))
(let ((.def_989 (<= 1 .def_951)))
(let ((.def_904 (___z12z___ .def_899)))
(let ((.def_905 (<= 1 .def_904)))
(let ((.def_990 (and .def_905 .def_989)))
(let ((.def_935 (___z19z___ _n)))
(let ((.def_1087 (= .def_935 .def_990)))
.def_1087
)))))))))
(assert (let ((.def_899 (+ _n (- 1))))
(let ((.def_1096 (___z20z___ .def_899)))
(let ((.def_1088 (+ (- 1) .def_899)))
(let ((.def_1093 (___z12z___ .def_1088)))
(let ((.def_1094 (<= 1 .def_1093)))
(let ((.def_1090 (___z15z___ .def_1088)))
(let ((.def_1089 (___z14z___ .def_1088)))
(let ((.def_1091 (+ .def_1089 .def_1090)))
(let ((.def_1092 (<= 1 .def_1091)))
(let ((.def_1095 (and .def_1092 .def_1094)))
(let ((.def_1097 (= .def_1095 .def_1096)))
.def_1097
))))))))))))
(assert (let ((.def_899 (+ _n (- 1))))
(let ((.def_1101 (___z11z___ .def_899)))
(let ((.def_901 (___z15z___ .def_899)))
(let ((.def_1099 (<= 0 .def_901)))
(let ((.def_1013 (___z16z___ .def_899)))
(let ((.def_1098 (not .def_1013)))
(let ((.def_1100 (or .def_1098 .def_1099)))
(let ((.def_1102 (= .def_1100 .def_1101)))
.def_1102
)))))))))
(assert (let ((.def_899 (+ _n (- 1))))
(let ((.def_1104 (___z21z___ .def_899)))
(let ((.def_1088 (+ (- 1) .def_899)))
(let ((.def_1089 (___z14z___ .def_1088)))
(let ((.def_1103 (<= 1 .def_1089)))
(let ((.def_1105 (= .def_1103 .def_1104)))
.def_1105
)))))))
(assert (let ((.def_899 (+ _n (- 1))))
(let ((.def_1088 (+ (- 1) .def_899)))
(let ((.def_1093 (___z12z___ .def_1088)))
(let ((.def_1106 (+ (- 1) .def_1093)))
(let ((.def_1107 (___z25z___ .def_899)))
(let ((.def_1108 (ite .def_1107 .def_1106 .def_1093)))
(let ((.def_1109 (___z9z___ .def_899)))
(let ((.def_1110 (ite .def_1109 .def_1108 .def_1093)))
(let ((.def_1111 (___z24z___ .def_899)))
(let ((.def_1112 (ite .def_1111 .def_1106 .def_1093)))
(let ((.def_1113 (___z8z___ .def_899)))
(let ((.def_1114 (ite .def_1113 .def_1112 .def_1110)))
(let ((.def_1115 (___z23z___ .def_899)))
(let ((.def_1116 (ite .def_1115 .def_1106 .def_1093)))
(let ((.def_1117 (___z7z___ .def_899)))
(let ((.def_1118 (ite .def_1117 .def_1116 .def_1114)))
(let ((.def_1096 (___z20z___ .def_899)))
(let ((.def_1119 (ite .def_1096 .def_1106 .def_1093)))
(let ((.def_1120 (___z4z___ .def_899)))
(let ((.def_1121 (ite .def_1120 .def_1119 .def_1118)))
(let ((.def_1122 (___z19z___ .def_899)))
(let ((.def_1123 (ite .def_1122 .def_1106 .def_1093)))
(let ((.def_1124 (___z3z___ .def_899)))
(let ((.def_1125 (ite .def_1124 .def_1123 .def_1121)))
(let ((.def_1126 (___z18z___ .def_899)))
(let ((.def_1127 (ite .def_1126 .def_1106 .def_1093)))
(let ((.def_1128 (___z2z___ .def_899)))
(let ((.def_1129 (ite .def_1128 .def_1127 .def_1125)))
(let ((.def_1018 (___z26z___ .def_899)))
(let ((.def_1130 (* (- 1) _base)))
(let ((.def_1131 (+ _n .def_1130)))
(let ((.def_1132 (= .def_1131 1)))
(let ((.def_1133 (ite .def_1132 .def_1018 .def_1129)))
(let ((.def_904 (___z12z___ .def_899)))
(let ((.def_1134 (= .def_904 .def_1133)))
.def_1134
))))))))))))))))))))))))))))))))))))
(assert (let ((.def_899 (+ _n (- 1))))
(let ((.def_1136 (___z22z___ .def_899)))
(let ((.def_1088 (+ (- 1) .def_899)))
(let ((.def_1090 (___z15z___ .def_1088)))
(let ((.def_1135 (= .def_1090 1)))
(let ((.def_1137 (= .def_1135 .def_1136)))
.def_1137
)))))))
(assert (let ((.def_899 (+ _n (- 1))))
(let ((.def_1088 (+ (- 1) .def_899)))
(let ((.def_1138 (___z13z___ .def_1088)))
(let ((.def_1139 (+ (- 1) .def_1138)))
(let ((.def_1111 (___z24z___ .def_899)))
(let ((.def_1140 (ite .def_1111 .def_1139 .def_1138)))
(let ((.def_1113 (___z8z___ .def_899)))
(let ((.def_1141 (ite .def_1113 .def_1140 .def_1138)))
(let ((.def_1115 (___z23z___ .def_899)))
(let ((.def_1142 (ite .def_1115 1 .def_1138)))
(let ((.def_1117 (___z7z___ .def_899)))
(let ((.def_1143 (ite .def_1117 .def_1142 .def_1141)))
(let ((.def_1144 (+ 1 .def_1138)))
(let ((.def_1104 (___z21z___ .def_899)))
(let ((.def_1145 (ite .def_1104 .def_1144 .def_1138)))
(let ((.def_1146 (___z5z___ .def_899)))
(let ((.def_1147 (ite .def_1146 .def_1145 .def_1143)))
(let ((.def_1122 (___z19z___ .def_899)))
(let ((.def_1148 (ite .def_1122 .def_1139 .def_1138)))
(let ((.def_1124 (___z3z___ .def_899)))
(let ((.def_1149 (ite .def_1124 .def_1148 .def_1147)))
(let ((.def_1130 (* (- 1) _base)))
(let ((.def_1131 (+ _n .def_1130)))
(let ((.def_1132 (= .def_1131 1)))
(let ((.def_1150 (ite .def_1132 0 .def_1149)))
(let ((.def_951 (___z13z___ .def_899)))
(let ((.def_1151 (= .def_951 .def_1150)))
.def_1151
))))))))))))))))))))))))))))
(assert (let ((.def_899 (+ _n (- 1))))
(let ((.def_1088 (+ (- 1) .def_899)))
(let ((.def_1138 (___z13z___ .def_1088)))
(let ((.def_1154 (= .def_1138 0)))
(let ((.def_1093 (___z12z___ .def_1088)))
(let ((.def_1094 (<= 1 .def_1093)))
(let ((.def_1155 (and .def_1094 .def_1154)))
(let ((.def_1090 (___z15z___ .def_1088)))
(let ((.def_1153 (= .def_1090 0)))
(let ((.def_1156 (and .def_1153 .def_1155)))
(let ((.def_1089 (___z14z___ .def_1088)))
(let ((.def_1152 (= .def_1089 0)))
(let ((.def_1157 (and .def_1152 .def_1156)))
(let ((.def_1115 (___z23z___ .def_899)))
(let ((.def_1158 (= .def_1115 .def_1157)))
.def_1158
))))))))))))))))
(assert (let ((.def_899 (+ _n (- 1))))
(let ((.def_1088 (+ (- 1) .def_899)))
(let ((.def_1089 (___z14z___ .def_1088)))
(let ((.def_1107 (___z25z___ .def_899)))
(let ((.def_1159 (ite .def_1107 0 .def_1089)))
(let ((.def_1109 (___z9z___ .def_899)))
(let ((.def_1160 (ite .def_1109 .def_1159 .def_1089)))
(let ((.def_1161 (+ 1 .def_1089)))
(let ((.def_1136 (___z22z___ .def_899)))
(let ((.def_1162 (ite .def_1136 .def_1161 .def_1089)))
(let ((.def_1163 (___z6z___ .def_899)))
(let ((.def_1164 (ite .def_1163 .def_1162 .def_1160)))
(let ((.def_1165 (+ (- 1) .def_1089)))
(let ((.def_1104 (___z21z___ .def_899)))
(let ((.def_1166 (ite .def_1104 .def_1165 .def_1089)))
(let ((.def_1146 (___z5z___ .def_899)))
(let ((.def_1167 (ite .def_1146 .def_1166 .def_1164)))
(let ((.def_1096 (___z20z___ .def_899)))
(let ((.def_1168 (ite .def_1096 0 .def_1089)))
(let ((.def_1120 (___z4z___ .def_899)))
(let ((.def_1169 (ite .def_1120 .def_1168 .def_1167)))
(let ((.def_1126 (___z18z___ .def_899)))
(let ((.def_1170 (ite .def_1126 .def_1161 .def_1089)))
(let ((.def_1128 (___z2z___ .def_899)))
(let ((.def_1171 (ite .def_1128 .def_1170 .def_1169)))
(let ((.def_1130 (* (- 1) _base)))
(let ((.def_1131 (+ _n .def_1130)))
(let ((.def_1132 (= .def_1131 1)))
(let ((.def_1172 (ite .def_1132 0 .def_1171)))
(let ((.def_900 (___z14z___ .def_899)))
(let ((.def_1173 (= .def_900 .def_1172)))
.def_1173
))))))))))))))))))))))))))))))))
(assert (let ((.def_899 (+ _n (- 1))))
(let ((.def_1088 (+ (- 1) .def_899)))
(let ((.def_1138 (___z13z___ .def_1088)))
(let ((.def_1174 (<= 1 .def_1138)))
(let ((.def_1093 (___z12z___ .def_1088)))
(let ((.def_1094 (<= 1 .def_1093)))
(let ((.def_1175 (and .def_1094 .def_1174)))
(let ((.def_1111 (___z24z___ .def_899)))
(let ((.def_1176 (= .def_1111 .def_1175)))
.def_1176
))))))))))
(assert (let ((.def_899 (+ _n (- 1))))
(let ((.def_1088 (+ (- 1) .def_899)))
(let ((.def_1090 (___z15z___ .def_1088)))
(let ((.def_1089 (___z14z___ .def_1088)))
(let ((.def_1091 (+ .def_1089 .def_1090)))
(let ((.def_1177 (+ 1 .def_1091)))
(let ((.def_1107 (___z25z___ .def_899)))
(let ((.def_1178 (ite .def_1107 .def_1177 .def_1090)))
(let ((.def_1109 (___z9z___ .def_899)))
(let ((.def_1179 (ite .def_1109 .def_1178 .def_1090)))
(let ((.def_1180 (+ 2 .def_1090)))
(let ((.def_1111 (___z24z___ .def_899)))
(let ((.def_1181 (ite .def_1111 .def_1180 .def_1090)))
(let ((.def_1113 (___z8z___ .def_899)))
(let ((.def_1182 (ite .def_1113 .def_1181 .def_1179)))
(let ((.def_1136 (___z22z___ .def_899)))
(let ((.def_1183 (ite .def_1136 0 .def_1090)))
(let ((.def_1163 (___z6z___ .def_899)))
(let ((.def_1184 (ite .def_1163 .def_1183 .def_1182)))
(let ((.def_1185 (+ (- 1) .def_1090)))
(let ((.def_1186 (+ .def_1089 .def_1185)))
(let ((.def_1187 (+ 1 .def_1186)))
(let ((.def_1096 (___z20z___ .def_899)))
(let ((.def_1188 (ite .def_1096 .def_1187 .def_1090)))
(let ((.def_1120 (___z4z___ .def_899)))
(let ((.def_1189 (ite .def_1120 .def_1188 .def_1184)))
(let ((.def_1122 (___z19z___ .def_899)))
(let ((.def_1190 (ite .def_1122 .def_1180 .def_1090)))
(let ((.def_1124 (___z3z___ .def_899)))
(let ((.def_1191 (ite .def_1124 .def_1190 .def_1189)))
(let ((.def_1130 (* (- 1) _base)))
(let ((.def_1131 (+ _n .def_1130)))
(let ((.def_1132 (= .def_1131 1)))
(let ((.def_1192 (ite .def_1132 0 .def_1191)))
(let ((.def_901 (___z15z___ .def_899)))
(let ((.def_1193 (= .def_901 .def_1192)))
.def_1193
)))))))))))))))))))))))))))))))))))))
(assert (let ((.def_899 (+ _n (- 1))))
(let ((.def_1107 (___z25z___ .def_899)))
(let ((.def_1088 (+ (- 1) .def_899)))
(let ((.def_1093 (___z12z___ .def_1088)))
(let ((.def_1094 (<= 1 .def_1093)))
(let ((.def_1090 (___z15z___ .def_1088)))
(let ((.def_1089 (___z14z___ .def_1088)))
(let ((.def_1091 (+ .def_1089 .def_1090)))
(let ((.def_1092 (<= 1 .def_1091)))
(let ((.def_1095 (and .def_1092 .def_1094)))
(let ((.def_1194 (= .def_1095 .def_1107)))
.def_1194
))))))))))))
(assert (let ((.def_899 (+ _n (- 1))))
(let ((.def_1088 (+ (- 1) .def_899)))
(let ((.def_1198 (___z16z___ .def_1088)))
(let ((.def_1196 (___z27z___ .def_899)))
(let ((.def_1199 (or .def_1196 .def_1198)))
(let ((.def_1130 (* (- 1) _base)))
(let ((.def_1131 (+ _n .def_1130)))
(let ((.def_1132 (= .def_1131 1)))
(let ((.def_1200 (or .def_1132 .def_1199)))
(let ((.def_1195 (not .def_1132)))
(let ((.def_1197 (or .def_1195 .def_1196)))
(let ((.def_1201 (and .def_1197 .def_1200)))
(let ((.def_1013 (___z16z___ .def_899)))
(let ((.def_1202 (= .def_1013 .def_1201)))
.def_1202
)))))))))))))))
(assert (let ((.def_899 (+ _n (- 1))))
(let ((.def_1088 (+ (- 1) .def_899)))
(let ((.def_1203 (___z26z___ .def_1088)))
(let ((.def_1204 (___z10z___ .def_899)))
(let ((.def_1130 (* (- 1) _base)))
(let ((.def_1131 (+ _n .def_1130)))
(let ((.def_1132 (= .def_1131 1)))
(let ((.def_1205 (ite .def_1132 .def_1204 .def_1203)))
(let ((.def_1018 (___z26z___ .def_899)))
(let ((.def_1206 (= .def_1018 .def_1205)))
.def_1206
)))))))))))
(assert (let ((.def_899 (+ _n (- 1))))
(let ((.def_1109 (___z9z___ .def_899)))
(let ((.def_1225 (not .def_1109)))
(let ((.def_1128 (___z2z___ .def_899)))
(let ((.def_1216 (not .def_1128)))
(let ((.def_1124 (___z3z___ .def_899)))
(let ((.def_1215 (not .def_1124)))
(let ((.def_1217 (and .def_1215 .def_1216)))
(let ((.def_1120 (___z4z___ .def_899)))
(let ((.def_1214 (not .def_1120)))
(let ((.def_1218 (and .def_1214 .def_1217)))
(let ((.def_1146 (___z5z___ .def_899)))
(let ((.def_1213 (not .def_1146)))
(let ((.def_1219 (and .def_1213 .def_1218)))
(let ((.def_1163 (___z6z___ .def_899)))
(let ((.def_1212 (not .def_1163)))
(let ((.def_1220 (and .def_1212 .def_1219)))
(let ((.def_1117 (___z7z___ .def_899)))
(let ((.def_1211 (not .def_1117)))
(let ((.def_1221 (and .def_1211 .def_1220)))
(let ((.def_1113 (___z8z___ .def_899)))
(let ((.def_1210 (not .def_1113)))
(let ((.def_1222 (and .def_1210 .def_1221)))
(let ((.def_1259 (and .def_1222 .def_1225)))
(let ((.def_1252 (and .def_1128 .def_1215)))
(let ((.def_1253 (and .def_1214 .def_1252)))
(let ((.def_1254 (and .def_1213 .def_1253)))
(let ((.def_1255 (and .def_1212 .def_1254)))
(let ((.def_1256 (and .def_1211 .def_1255)))
(let ((.def_1257 (and .def_1210 .def_1256)))
(let ((.def_1258 (and .def_1225 .def_1257)))
(let ((.def_1260 (or .def_1258 .def_1259)))
(let ((.def_1245 (and .def_1124 .def_1216)))
(let ((.def_1246 (and .def_1214 .def_1245)))
(let ((.def_1247 (and .def_1213 .def_1246)))
(let ((.def_1248 (and .def_1212 .def_1247)))
(let ((.def_1249 (and .def_1211 .def_1248)))
(let ((.def_1250 (and .def_1210 .def_1249)))
(let ((.def_1251 (and .def_1225 .def_1250)))
(let ((.def_1261 (or .def_1251 .def_1260)))
(let ((.def_1239 (and .def_1120 .def_1217)))
(let ((.def_1240 (and .def_1213 .def_1239)))
(let ((.def_1241 (and .def_1212 .def_1240)))
(let ((.def_1242 (and .def_1211 .def_1241)))
(let ((.def_1243 (and .def_1210 .def_1242)))
(let ((.def_1244 (and .def_1225 .def_1243)))
(let ((.def_1262 (or .def_1244 .def_1261)))
(let ((.def_1234 (and .def_1146 .def_1218)))
(let ((.def_1235 (and .def_1212 .def_1234)))
(let ((.def_1236 (and .def_1211 .def_1235)))
(let ((.def_1237 (and .def_1210 .def_1236)))
(let ((.def_1238 (and .def_1225 .def_1237)))
(let ((.def_1263 (or .def_1238 .def_1262)))
(let ((.def_1230 (and .def_1163 .def_1219)))
(let ((.def_1231 (and .def_1211 .def_1230)))
(let ((.def_1232 (and .def_1210 .def_1231)))
(let ((.def_1233 (and .def_1225 .def_1232)))
(let ((.def_1264 (or .def_1233 .def_1263)))
(let ((.def_1227 (and .def_1117 .def_1220)))
(let ((.def_1228 (and .def_1210 .def_1227)))
(let ((.def_1229 (and .def_1225 .def_1228)))
(let ((.def_1265 (or .def_1229 .def_1264)))
(let ((.def_1224 (and .def_1113 .def_1221)))
(let ((.def_1226 (and .def_1224 .def_1225)))
(let ((.def_1266 (or .def_1226 .def_1265)))
(let ((.def_1223 (and .def_1109 .def_1222)))
(let ((.def_1267 (or .def_1223 .def_1266)))
(let ((.def_1204 (___z10z___ .def_899)))
(let ((.def_1209 (<= 0 .def_1204)))
(let ((.def_1268 (and .def_1209 .def_1267)))
(let ((.def_1207 (<= 5 .def_1204)))
(let ((.def_1208 (not .def_1207)))
(let ((.def_1269 (and .def_1208 .def_1268)))
(let ((.def_1196 (___z27z___ .def_899)))
(let ((.def_1270 (= .def_1196 .def_1269)))
.def_1270
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(assert (let ((.def_899 (+ _n (- 1))))
(let ((.def_1088 (+ (- 1) .def_899)))
(let ((.def_1138 (___z13z___ .def_1088)))
(let ((.def_1154 (= .def_1138 0)))
(let ((.def_1093 (___z12z___ .def_1088)))
(let ((.def_1094 (<= 1 .def_1093)))
(let ((.def_1155 (and .def_1094 .def_1154)))
(let ((.def_1090 (___z15z___ .def_1088)))
(let ((.def_1153 (= .def_1090 0)))
(let ((.def_1156 (and .def_1153 .def_1155)))
(let ((.def_1089 (___z14z___ .def_1088)))
(let ((.def_1152 (= .def_1089 0)))
(let ((.def_1157 (and .def_1152 .def_1156)))
(let ((.def_1126 (___z18z___ .def_899)))
(let ((.def_1271 (= .def_1126 .def_1157)))
.def_1271
))))))))))))))))
(assert (let ((.def_899 (+ _n (- 1))))
(let ((.def_1088 (+ (- 1) .def_899)))
(let ((.def_1138 (___z13z___ .def_1088)))
(let ((.def_1174 (<= 1 .def_1138)))
(let ((.def_1093 (___z12z___ .def_1088)))
(let ((.def_1094 (<= 1 .def_1093)))
(let ((.def_1175 (and .def_1094 .def_1174)))
(let ((.def_1122 (___z19z___ .def_899)))
(let ((.def_1272 (= .def_1122 .def_1175)))
.def_1272
))))))))))
(assert (let ((.def_899 (+ _n (- 1))))
(let ((.def_1101 (___z11z___ .def_899)))
.def_1101
)))
(assert (let ((.def_914 (___z11z___ _n)))
(let ((.def_754 (= _base (- 1))))
(let ((.def_817 (not .def_754)))
(let ((.def_1273 (or .def_817 .def_914)))
(let ((.def_1274 (not .def_1273)))
.def_1274
))))))
(assert true
)
(check-sat)
(pop 1)