(set-logic HORN)
(set-info :source |
  Benchmark: /home/atondwal/src/mist/mochi-tests/forSigma.ml
  Generated by MoCHi
|)
(set-info :status unknown)
(declare-fun |fail_88[0:0]| ( Int) Bool)
(declare-fun |thenn[0:2][0:0][0:1][0:1]| ( Int  Int  Int) Bool)
(declare-fun |thenn[0:1][0:1][0:1]| ( Int  Int  Int) Bool)
(declare-fun |loop[0:2][0:0][0:1][0:0][0:1][0:1]| ( Int  Int  Int  Int  Int) Bool)
(declare-fun |thenn[0:1][0:0]| ( Int) Bool)
(declare-fun |thenn[0:0][0:1][0:1]| ( Int  Int  Int) Bool)
(declare-fun |loop[0:0][0:1][0:0][0:1][0:1]| ( Int  Int  Int  Int) Bool)
(declare-fun |bind[0:2][0:0][0:1][0:1]| ( Int  Int  Int) Bool)
(declare-fun |bind[0:1][0:1][0:0][0:1][0:1]| ( Int  Int  Int  Int) Bool)
(declare-fun |bind[0:1][0:0]| ( Int) Bool)
(declare-fun |bind[0:2][0:0][0:0]| ( Int) Bool)
(declare-fun |bind[0:0][0:1][0:1]| ( Int  Int  Int) Bool)
(declare-fun |loop[0:0][0:1][0:0][0:0]| ( Int  Int) Bool)
(declare-fun |loop[0:2][0:0][0:1][0:0][0:0]| ( Int  Int  Int) Bool)
(declare-fun |thenn[0:0][0:0]| ( Int) Bool)
(declare-fun |thenn[0:2][0:0][0:0]| ( Int) Bool)
(declare-fun |loop[0:0][0:0]| ( Int) Bool)
(declare-fun |loop[0:2][0:0][0:0]| ( Int  Int) Bool)
(declare-fun |loop[0:1]| ( Int) Bool)
(assert (not (exists ((x0 Int)) (|fail_88[0:0]| x0))))
(assert (forall ((x0 Int)(x2 Int)) (=> (|bind[0:1][0:0]| x2) (|fail_88[0:0]| x0))))
(assert (forall ((x0 Int)(var622 Int)(var623 Int)) (=> (and (|bind[0:2][0:0][0:0]| var622) (|bind[0:0][0:1][0:1]| var622 x0 var623)) (|bind[0:1][0:0]| x0))))
(assert (forall ((x1 Int)(x2 Int)(x3 Int)) (=> (and (= x3 x2) (= x3 x1)) (|bind[0:0][0:1][0:1]| x1 x2 x3))))
(assert (forall ((x1 Int)) (=> (|thenn[0:1][0:0]| x1) (|bind[0:2][0:0][0:0]| x1))))
(assert (forall ((x0 Int)(var624 Int)(var625 Int)) (=> (and (|thenn[0:2][0:0][0:0]| var624) (|thenn[0:0][0:1][0:1]| var624 var625 x0)) (|thenn[0:1][0:0]| x0))))
(assert (forall ((x1 Int)(x2 Int)(x3 Int)) (=> (|thenn[0:2][0:0][0:1][0:1]| x1 x2 x3) (|thenn[0:0][0:1][0:1]| x1 x2 x3))))
(assert (forall ((x0 Int)(x1 Int)(x2 Int)(var627 Int)(var626 Int)) (=> (and (|thenn[0:2][0:0][0:0]| x0) (and (|thenn[0:1][0:1][0:1]| var627 x1 x2) (|thenn[0:0][0:1][0:1]| x0 var626 var627))) (|thenn[0:2][0:0][0:1][0:1]| x0 x1 x2))))
(assert (forall ((x1 Int)(x2 Int)(x3 Int)) (=> (|loop[0:2][0:0][0:1][0:0][0:1][0:1]| 9 0 x1 x2 x3) (|thenn[0:1][0:1][0:1]| x1 x2 x3))))
(assert (forall ((x0 Int)(x1 Int)(x2 Int)(x3 Int)(x4 Int)) (=> (and (|thenn[0:2][0:0][0:1][0:1]| x2 x3 x4) (and (|loop[0:1]| x0) (and (|loop[0:2][0:0][0:0]| x0 x1) (not (= x0 0))))) (|loop[0:2][0:0][0:1][0:0][0:1][0:1]| x0 x1 x2 x3 x4))))
(assert (forall ((x0 Int)(x1 Int)(x2 Int)(var629 Int)(var628 Int)) (=> (and (|thenn[0:2][0:0][0:0]| x0) (and (|thenn[0:1][0:1][0:1]| var629 x1 x2) (|thenn[0:0][0:1][0:1]| x0 var628 var629))) (|thenn[0:2][0:0][0:1][0:1]| x0 x1 x2))))
(assert (forall ((x2 Int)(x3 Int)(x4 Int)(var630 Int)(x1 Int)(x0 Int)) (=> (and (|loop[0:2][0:0][0:1][0:0][0:1][0:1]| var630 0 x2 x3 x4) (and (|loop[0:1]| x1) (and (|loop[0:2][0:0][0:0]| x1 x0) (and (= (+ 1 var630) x1) (not (= x1 0)))))) (|thenn[0:1][0:1][0:1]| x2 x3 x4))))
(assert (forall ((x0 Int)(x1 Int)(x2 Int)(x3 Int)(x4 Int)) (=> (and (|loop[0:2][0:0][0:0]| x0 x1) (and (|loop[0:1]| x0) (and (|loop[0:0][0:1][0:0][0:1][0:1]| 0 x2 x3 x4) (= x0 0)))) (|loop[0:2][0:0][0:1][0:0][0:1][0:1]| x0 x1 x2 x3 x4))))
(assert (forall ((x2 Int)(x3 Int)(x4 Int)(x5 Int)(x1 Int)(x0 Int)) (=> (and (|loop[0:2][0:0][0:0]| x1 x0) (and (|loop[0:1]| x1) (and (|loop[0:0][0:1][0:0][0:1][0:1]| x2 x3 x4 x5) (not (= x1 0))))) (|loop[0:0][0:1][0:0][0:1][0:1]| x2 x3 x4 x5))))
(assert (forall ((x1 Int)(x2 Int)(x3 Int)(x4 Int)) (=> (and (|bind[0:2][0:0][0:1][0:1]| x2 x3 x4) (|loop[0:0][0:0]| x1)) (|loop[0:0][0:1][0:0][0:1][0:1]| x1 x2 x3 x4))))
(assert (forall ((x0 Int)(x1 Int)(x2 Int)(var631 Int)(var632 Int)) (=> (and (|bind[0:1][0:1][0:0][0:1][0:1]| var631 var632 x1 x2) (and (|bind[0:2][0:0][0:0]| x0) (|bind[0:0][0:1][0:1]| x0 var631 var632))) (|bind[0:2][0:0][0:1][0:1]| x0 x1 x2))))
(assert (forall ((x1 Int)(x2 Int)(x3 Int)(x4 Int)(var633 Int)(x0 Int)) (=> (and (|bind[0:1][0:0]| var633) (and (|loop[0:0][0:0]| x0) (and (|bind[0:1][0:0]| x1) (and (= x4 (+ 1 var633)) (= x4 (+ 1 x1)))))) (|bind[0:1][0:1][0:0][0:1][0:1]| x1 x2 x3 x4))))
(assert (forall ((x0 Int)(var637 Int)(var638 Int)) (=> (and (|bind[0:2][0:0][0:0]| var637) (|bind[0:0][0:1][0:1]| var637 x0 var638)) (|bind[0:1][0:0]| x0))))
(assert (forall ((x1 Int)(x2 Int)(x3 Int)(x0 Int)) (=> (and (|loop[0:0][0:0]| x0) (and (= x3 x2) (= x3 x1))) (|bind[0:0][0:1][0:1]| x1 x2 x3))))
(assert (forall ((x1 Int)(x0 Int)) (=> (and (|loop[0:0][0:1][0:0][0:0]| x0 x1) (|loop[0:0][0:0]| x0)) (|bind[0:2][0:0][0:0]| x1))))
(assert (forall ((x2 Int)(x1 Int)(x0 Int)(var641 Int)) (=> (and (|loop[0:2][0:0][0:0]| x0 var641) (and (|loop[0:0][0:1][0:0][0:0]| x2 x1) (and (|loop[0:0][0:0]| x2) (and (|loop[0:1]| x0) (not (= x0 0)))))) (|loop[0:0][0:1][0:0][0:0]| x2 x1))))
(assert (forall ((x1 Int)(x0 Int)(var643 Int)) (=> (and (|loop[0:2][0:0][0:1][0:0][0:0]| 0 var643 x0) (and (|loop[0:2][0:0][0:0]| 0 var643) (and (|loop[0:0][0:0]| x1) (and (|loop[0:1]| 0) (= x1 0))))) (|loop[0:0][0:1][0:0][0:0]| x1 x0))))
(assert (forall ((x3 Int)(x4 Int)(x2 Int)(x1 Int)(x0 Int)) (=> (and (|loop[0:1]| x3) (and (|loop[0:2][0:0][0:0]| x3 x4) (and (|thenn[0:1][0:0]| x2) (and (|loop[0:1]| x1) (and (|loop[0:2][0:0][0:0]| x1 x0) (and (= x4 0) (and (= (+ 1 x3) x1) (not (= x1 0))))))))) (|loop[0:2][0:0][0:1][0:0][0:0]| x3 x4 x2))))
(assert (forall ((x0 Int)(var644 Int)(var645 Int)) (=> (and (|thenn[0:2][0:0][0:0]| var644) (|thenn[0:0][0:1][0:1]| var644 var645 x0)) (|thenn[0:1][0:0]| x0))))
(assert (forall ((x2 Int)(x3 Int)(x4 Int)(x1 Int)(x0 Int)) (=> (and (|loop[0:0][0:1][0:0][0:1][0:1]| 0 x2 x3 x4) (and (|loop[0:1]| x1) (and (|loop[0:2][0:0][0:0]| x1 x0) (not (= x1 0))))) (|thenn[0:0][0:1][0:1]| x2 x3 x4))))
(assert (forall ((x1 Int)(x2 Int)(x3 Int)(x4 Int)) (=> (and (|bind[0:2][0:0][0:1][0:1]| x2 x3 x4) (|loop[0:0][0:0]| x1)) (|loop[0:0][0:1][0:0][0:1][0:1]| x1 x2 x3 x4))))
(assert (forall ((x0 Int)(x1 Int)(x2 Int)(var646 Int)(var647 Int)) (=> (and (|bind[0:1][0:1][0:0][0:1][0:1]| var646 var647 x1 x2) (and (|bind[0:2][0:0][0:0]| x0) (|bind[0:0][0:1][0:1]| x0 var646 var647))) (|bind[0:2][0:0][0:1][0:1]| x0 x1 x2))))
(assert (forall ((x1 Int)(x2 Int)(x3 Int)(x4 Int)(var648 Int)(x0 Int)) (=> (and (|bind[0:1][0:0]| var648) (and (|loop[0:0][0:0]| x0) (and (|bind[0:1][0:0]| x1) (and (= x4 (+ 1 var648)) (= x4 (+ 1 x1)))))) (|bind[0:1][0:1][0:0][0:1][0:1]| x1 x2 x3 x4))))
(assert (forall ((x0 Int)(var652 Int)(var653 Int)) (=> (and (|bind[0:2][0:0][0:0]| var652) (|bind[0:0][0:1][0:1]| var652 x0 var653)) (|bind[0:1][0:0]| x0))))
(assert (forall ((x1 Int)(x2 Int)(x3 Int)(x0 Int)) (=> (and (|loop[0:0][0:0]| x0) (and (= x3 x2) (= x3 x1))) (|bind[0:0][0:1][0:1]| x1 x2 x3))))
(assert (forall ((x1 Int)(x0 Int)) (=> (and (|loop[0:0][0:1][0:0][0:0]| x0 x1) (|loop[0:0][0:0]| x0)) (|bind[0:2][0:0][0:0]| x1))))
(assert (forall ((x2 Int)(x1 Int)(x0 Int)(var656 Int)) (=> (and (|loop[0:2][0:0][0:0]| x0 var656) (and (|loop[0:0][0:0]| x2) (and (|thenn[0:0][0:0]| x1) (and (|loop[0:1]| x0) (and (= x2 0) (not (= x0 0))))))) (|loop[0:0][0:1][0:0][0:0]| x2 x1))))
(assert (forall ((x0 Int)) (=> (|thenn[0:2][0:0][0:0]| x0) (|thenn[0:0][0:0]| x0))))
(assert (forall ((x2 Int)(x1 Int)(x0 Int)) (=> (and (|loop[0:2][0:0][0:1][0:0][0:0]| x1 x0 x2) (and (|loop[0:1]| x1) (and (|loop[0:2][0:0][0:0]| x1 x0) (not (= x1 0))))) (|thenn[0:2][0:0][0:0]| x2))))
(assert (forall ((x2 Int)(x3 Int)(x1 Int)) (=> (and (|loop[0:1]| x2) (and (|loop[0:2][0:0][0:0]| x2 x3) (and (|thenn[0:1][0:0]| x1) (and (= x2 9) (= x3 0))))) (|loop[0:2][0:0][0:1][0:0][0:0]| x2 x3 x1))))
(assert (forall ((x0 Int)(var657 Int)(var658 Int)) (=> (and (|thenn[0:2][0:0][0:0]| var657) (|thenn[0:0][0:1][0:1]| var657 var658 x0)) (|thenn[0:1][0:0]| x0))))
(assert (forall ((x1 Int)(x2 Int)(x3 Int)) (=> (|loop[0:2][0:0][0:1][0:0][0:1][0:1]| 8 0 x1 x2 x3) (|thenn[0:0][0:1][0:1]| x1 x2 x3))))
(assert (forall ((x0 Int)(x1 Int)(x2 Int)(x3 Int)(x4 Int)) (=> (and (|thenn[0:2][0:0][0:1][0:1]| x2 x3 x4) (and (|loop[0:1]| x0) (and (|loop[0:2][0:0][0:0]| x0 x1) (not (= x0 0))))) (|loop[0:2][0:0][0:1][0:0][0:1][0:1]| x0 x1 x2 x3 x4))))
(assert (forall ((x0 Int)(x1 Int)(x2 Int)(var660 Int)(var659 Int)) (=> (and (|thenn[0:2][0:0][0:0]| x0) (and (|thenn[0:1][0:1][0:1]| var660 x1 x2) (|thenn[0:0][0:1][0:1]| x0 var659 var660))) (|thenn[0:2][0:0][0:1][0:1]| x0 x1 x2))))
(assert (forall ((x2 Int)(x3 Int)(x4 Int)(var661 Int)(x1 Int)(x0 Int)) (=> (and (|loop[0:2][0:0][0:1][0:0][0:1][0:1]| var661 0 x2 x3 x4) (and (|loop[0:1]| x1) (and (|loop[0:2][0:0][0:0]| x1 x0) (and (= (+ 1 var661) x1) (not (= x1 0)))))) (|thenn[0:1][0:1][0:1]| x2 x3 x4))))
(assert (forall ((x0 Int)(x1 Int)(x2 Int)(x3 Int)(x4 Int)) (=> (and (|loop[0:2][0:0][0:0]| x0 x1) (and (|loop[0:1]| x0) (and (|loop[0:0][0:1][0:0][0:1][0:1]| 0 x2 x3 x4) (= x0 0)))) (|loop[0:2][0:0][0:1][0:0][0:1][0:1]| x0 x1 x2 x3 x4))))
(assert (forall ((x2 Int)(x3 Int)(x4 Int)(x5 Int)(x1 Int)(x0 Int)) (=> (and (|loop[0:2][0:0][0:0]| x1 x0) (and (|loop[0:1]| x1) (and (|loop[0:0][0:1][0:0][0:1][0:1]| x2 x3 x4 x5) (not (= x1 0))))) (|loop[0:0][0:1][0:0][0:1][0:1]| x2 x3 x4 x5))))
(assert (forall ((x1 Int)(x2 Int)(x3 Int)(x4 Int)) (=> (and (|bind[0:2][0:0][0:1][0:1]| x2 x3 x4) (|loop[0:0][0:0]| x1)) (|loop[0:0][0:1][0:0][0:1][0:1]| x1 x2 x3 x4))))
(assert (forall ((x0 Int)(x1 Int)(x2 Int)(var662 Int)(var663 Int)) (=> (and (|bind[0:1][0:1][0:0][0:1][0:1]| var662 var663 x1 x2) (and (|bind[0:2][0:0][0:0]| x0) (|bind[0:0][0:1][0:1]| x0 var662 var663))) (|bind[0:2][0:0][0:1][0:1]| x0 x1 x2))))
(assert (forall ((x1 Int)(x2 Int)(x3 Int)(x4 Int)(var664 Int)(x0 Int)) (=> (and (|bind[0:1][0:0]| var664) (and (|loop[0:0][0:0]| x0) (and (|bind[0:1][0:0]| x1) (and (= x4 (+ 4 var664)) (= x4 (+ 4 x1)))))) (|bind[0:1][0:1][0:0][0:1][0:1]| x1 x2 x3 x4))))
(assert (forall ((x0 Int)(var668 Int)(var669 Int)) (=> (and (|bind[0:2][0:0][0:0]| var668) (|bind[0:0][0:1][0:1]| var668 x0 var669)) (|bind[0:1][0:0]| x0))))
(assert (forall ((x1 Int)(x2 Int)(x3 Int)(x0 Int)) (=> (and (|loop[0:0][0:0]| x0) (and (= x3 x2) (= x3 x1))) (|bind[0:0][0:1][0:1]| x1 x2 x3))))
(assert (forall ((x1 Int)(x0 Int)) (=> (and (|loop[0:0][0:1][0:0][0:0]| x0 x1) (|loop[0:0][0:0]| x0)) (|bind[0:2][0:0][0:0]| x1))))
(assert (forall ((x2 Int)(x1 Int)(x0 Int)(var672 Int)) (=> (and (|loop[0:2][0:0][0:0]| x0 var672) (and (|loop[0:0][0:1][0:0][0:0]| x2 x1) (and (|loop[0:0][0:0]| x2) (and (|loop[0:1]| x0) (not (= x0 0)))))) (|loop[0:0][0:1][0:0][0:0]| x2 x1))))
(assert (forall ((x1 Int)(x0 Int)(var674 Int)) (=> (and (|loop[0:2][0:0][0:1][0:0][0:0]| 0 var674 x0) (and (|loop[0:2][0:0][0:0]| 0 var674) (and (|loop[0:0][0:0]| x1) (and (|loop[0:1]| 0) (= x1 0))))) (|loop[0:0][0:1][0:0][0:0]| x1 x0))))
(assert (forall ((x3 Int)(x4 Int)(x2 Int)(x1 Int)(x0 Int)) (=> (and (|loop[0:1]| x3) (and (|loop[0:2][0:0][0:0]| x3 x4) (and (|thenn[0:1][0:0]| x2) (and (|loop[0:1]| x1) (and (|loop[0:2][0:0][0:0]| x1 x0) (and (= x4 0) (and (= (+ 1 x3) x1) (not (= x1 0))))))))) (|loop[0:2][0:0][0:1][0:0][0:0]| x3 x4 x2))))
(assert (forall ((x0 Int)(var675 Int)(var676 Int)) (=> (and (|thenn[0:2][0:0][0:0]| var675) (|thenn[0:0][0:1][0:1]| var675 var676 x0)) (|thenn[0:1][0:0]| x0))))
(assert (forall ((x2 Int)(x3 Int)(x4 Int)(x1 Int)(x0 Int)) (=> (and (|loop[0:0][0:1][0:0][0:1][0:1]| 0 x2 x3 x4) (and (|loop[0:1]| x1) (and (|loop[0:2][0:0][0:0]| x1 x0) (not (= x1 0))))) (|thenn[0:0][0:1][0:1]| x2 x3 x4))))
(assert (forall ((x1 Int)(x2 Int)(x3 Int)(x4 Int)) (=> (and (|bind[0:2][0:0][0:1][0:1]| x2 x3 x4) (|loop[0:0][0:0]| x1)) (|loop[0:0][0:1][0:0][0:1][0:1]| x1 x2 x3 x4))))
(assert (forall ((x0 Int)(x1 Int)(x2 Int)(var677 Int)(var678 Int)) (=> (and (|bind[0:1][0:1][0:0][0:1][0:1]| var677 var678 x1 x2) (and (|bind[0:2][0:0][0:0]| x0) (|bind[0:0][0:1][0:1]| x0 var677 var678))) (|bind[0:2][0:0][0:1][0:1]| x0 x1 x2))))
(assert (forall ((x1 Int)(x2 Int)(x3 Int)(x4 Int)(var679 Int)(x0 Int)) (=> (and (|bind[0:1][0:0]| var679) (and (|loop[0:0][0:0]| x0) (and (|bind[0:1][0:0]| x1) (and (= x4 (+ 4 var679)) (= x4 (+ 4 x1)))))) (|bind[0:1][0:1][0:0][0:1][0:1]| x1 x2 x3 x4))))
(assert (forall ((x0 Int)(var683 Int)(var684 Int)) (=> (and (|bind[0:2][0:0][0:0]| var683) (|bind[0:0][0:1][0:1]| var683 x0 var684)) (|bind[0:1][0:0]| x0))))
(assert (forall ((x1 Int)(x2 Int)(x3 Int)(x0 Int)) (=> (and (|loop[0:0][0:0]| x0) (and (= x3 x2) (= x3 x1))) (|bind[0:0][0:1][0:1]| x1 x2 x3))))
(assert (forall ((x1 Int)(x0 Int)) (=> (and (|loop[0:0][0:1][0:0][0:0]| x0 x1) (|loop[0:0][0:0]| x0)) (|bind[0:2][0:0][0:0]| x1))))
(assert (forall ((x2 Int)(x1 Int)(x0 Int)(var687 Int)) (=> (and (|loop[0:2][0:0][0:0]| x0 var687) (and (|loop[0:0][0:0]| x2) (and (|thenn[0:0][0:0]| x1) (and (|loop[0:1]| x0) (and (= x2 0) (not (= x0 0))))))) (|loop[0:0][0:1][0:0][0:0]| x2 x1))))
(assert (forall ((x0 Int)) (=> (|thenn[0:2][0:0][0:0]| x0) (|thenn[0:0][0:0]| x0))))
(assert (forall ((x2 Int)(x1 Int)(x0 Int)) (=> (and (|loop[0:2][0:0][0:1][0:0][0:0]| x1 x0 x2) (and (|loop[0:1]| x1) (and (|loop[0:2][0:0][0:0]| x1 x0) (not (= x1 0))))) (|thenn[0:2][0:0][0:0]| x2))))
(assert (forall ((x2 Int)(x3 Int)(x1 Int)) (=> (and (|loop[0:1]| x2) (and (|loop[0:2][0:0][0:0]| x2 x3) (and (|thenn[0:0][0:0]| x1) (and (= x2 8) (= x3 0))))) (|loop[0:2][0:0][0:1][0:0][0:0]| x2 x3 x1))))
(assert (forall ((x0 Int)) (=> (|thenn[0:2][0:0][0:0]| x0) (|thenn[0:0][0:0]| x0))))
(assert (forall ((x1 Int)) (=> (|thenn[0:0][0:0]| x1) (|thenn[0:2][0:0][0:0]| x1))))
(assert (forall ((x0 Int)) (=> (|thenn[0:2][0:0][0:0]| x0) (|thenn[0:0][0:0]| x0))))
(assert (forall ((x1 Int)) (|thenn[0:2][0:0][0:0]| x1)))
(assert (forall ((x1 Int)(x0 Int)(var688 Int)) (=> (and (|loop[0:1]| x0) (and (|loop[0:2][0:0][0:0]| x0 var688) (and (= x1 0) (not (= x0 0))))) (|loop[0:0][0:0]| x1))))
(assert (forall ((x1 Int)(x0 Int)(var689 Int)) (=> (and (|loop[0:0][0:0]| x1) (and (|loop[0:1]| x0) (and (|loop[0:2][0:0][0:0]| x0 var689) (not (= x0 0))))) (|loop[0:0][0:0]| x1))))
(assert (forall ((x0 Int)(var690 Int)) (=> (and (|loop[0:1]| 0) (and (|loop[0:2][0:0][0:0]| 0 var690) (= x0 0))) (|loop[0:0][0:0]| x0))))
(assert (forall ((x3 Int)(x2 Int)(x1 Int)(x0 Int)) (=> (and (|loop[0:1]| x3) (and (|loop[0:1]| x1) (and (|loop[0:2][0:0][0:0]| x1 x0) (and (= x2 0) (and (= (+ 1 x3) x1) (not (= x1 0))))))) (|loop[0:2][0:0][0:0]| x3 x2))))
(assert (forall ((x0 Int)(x1 Int)(x2 Int)) (=> (and (|loop[0:1]| x1) (and (|loop[0:2][0:0][0:0]| x1 x2) (and (= (+ 1 x0) x1) (not (= x1 0))))) (|loop[0:1]| x0))))
(assert (forall ((x2 Int)(x1 Int)) (=> (and (|loop[0:1]| x2) (and (= x2 8) (= x1 0))) (|loop[0:2][0:0][0:0]| x2 x1))))
(assert (forall ((x0 Int)) (=> (= x0 8) (|loop[0:1]| x0))))
(assert (forall ((x1 Int)(x0 Int)(var691 Int)) (=> (and (|loop[0:1]| x0) (and (|loop[0:2][0:0][0:0]| x0 var691) (and (= x1 0) (not (= x0 0))))) (|loop[0:0][0:0]| x1))))
(assert (forall ((x1 Int)(x0 Int)(var692 Int)) (=> (and (|loop[0:0][0:0]| x1) (and (|loop[0:1]| x0) (and (|loop[0:2][0:0][0:0]| x0 var692) (not (= x0 0))))) (|loop[0:0][0:0]| x1))))
(assert (forall ((x0 Int)(var693 Int)) (=> (and (|loop[0:1]| 0) (and (|loop[0:2][0:0][0:0]| 0 var693) (= x0 0))) (|loop[0:0][0:0]| x0))))
(assert (forall ((x3 Int)(x2 Int)(x1 Int)(x0 Int)) (=> (and (|loop[0:1]| x3) (and (|loop[0:1]| x1) (and (|loop[0:2][0:0][0:0]| x1 x0) (and (= x2 0) (and (= (+ 1 x3) x1) (not (= x1 0))))))) (|loop[0:2][0:0][0:0]| x3 x2))))
(assert (forall ((x0 Int)(x1 Int)(x2 Int)) (=> (and (|loop[0:1]| x1) (and (|loop[0:2][0:0][0:0]| x1 x2) (and (= (+ 1 x0) x1) (not (= x1 0))))) (|loop[0:1]| x0))))
(assert (forall ((x2 Int)(x1 Int)) (=> (and (|loop[0:1]| x2) (and (= x2 9) (= x1 0))) (|loop[0:2][0:0][0:0]| x2 x1))))
(assert (forall ((x0 Int)) (=> (= x0 9) (|loop[0:1]| x0))))
(check-sat)
(get-model)
(exit)