(set-logic HORN)
(set-info :source |
  Benchmark: /home/atondwal/src/mist/mochi-tests/acl.ml
  Generated by MoCHi
|)
(set-info :status unknown)
(declare-fun |fail_63[0:0]| ( Int) Bool)
(declare-fun |bind_21[0:1][0:1][0:1][0:0]| ( Int  Int  Bool) Bool)
(declare-fun |bind_21[0:0][0:1][0:1][0:1][0:0]| ( Int  Int  Bool) Bool)
(declare-fun |bind_21[0:0][0:0][0:1][0:0]| ( Int  Bool) Bool)
(declare-fun |bind_21[0:2][0:1][0:0]| ( Int  Bool) Bool)
(declare-fun |bind_21[0:2][0:0]| ( Int) Bool)
(declare-fun |bind_21[0:0][0:0][0:0]| ( Int) Bool)
(declare-fun |bind_21[0:0][0:1][0:1][0:0]| ( Int  Int) Bool)
(declare-fun |bind_21[0:1][0:1][0:0]| ( Int  Int) Bool)
(declare-fun |bind_21[0:1][0:0]| ( Int) Bool)
(declare-fun |bind_21[0:0][0:1][0:0]| ( Int) Bool)
(assert (not (exists ((x0 Int)) (|fail_63[0:0]| x0))))
(assert (forall ((x0 Int)(var326 Int)(x1 Int)) (=> (and (|bind_21[0:1][0:1][0:1][0:0]| var326 x1 false) (|bind_21[0:1][0:0]| var326)) (|fail_63[0:0]| x0))))
(assert (forall ((x2 Int)(x0 Int)(x1 Bool)(var328 Int)) (=> (and (|bind_21[0:0][0:1][0:1][0:1][0:0]| var328 x0 x1) (and (|bind_21[0:0][0:1][0:0]| var328) (|bind_21[0:1][0:0]| x2))) (|bind_21[0:1][0:1][0:1][0:0]| x2 x0 x1))))
(assert (forall ((x3 Int)(x1 Int)(x2 Bool)(var329 Int)) (=> (and (|bind_21[0:0][0:1][0:0]| x3) (and (|bind_21[0:0][0:1][0:1][0:0]| var329 x1) (|bind_21[0:0][0:0][0:1][0:0]| x1 x2))) (|bind_21[0:0][0:1][0:1][0:1][0:0]| x3 x1 x2))))
(assert (forall ((x0 Int)(x1 Bool)) (=> (|bind_21[0:2][0:1][0:0]| x0 x1) (|bind_21[0:0][0:0][0:1][0:0]| x0 x1))))
(assert (forall ((x1 Int)(x2 Bool)) (=> (|bind_21[0:2][0:0]| x1) (|bind_21[0:2][0:1][0:0]| x1 x2))))
(assert (forall ((x0 Int)) (=> (|bind_21[0:0][0:0][0:0]| x0) (|bind_21[0:2][0:0]| x0))))
(assert (forall ((x1 Int)(var330 Int)) (=> (|bind_21[0:0][0:1][0:1][0:0]| var330 x1) (|bind_21[0:0][0:0][0:0]| x1))))
(assert (forall ((x0 Int)(x1 Int)(var331 Int)) (=> (and (|bind_21[0:0][0:1][0:0]| x0) (|bind_21[0:1][0:1][0:0]| var331 x1)) (|bind_21[0:0][0:1][0:1][0:0]| x0 x1))))
(assert (forall ((x1 Int)(x2 Int)) (=> (|bind_21[0:1][0:0]| x1) (|bind_21[0:1][0:1][0:0]| x1 x2))))
(assert (forall ((x0 Int)(var332 Int)) (=> (|bind_21[0:0][0:1][0:0]| var332) (|bind_21[0:1][0:0]| x0))))
(assert (forall ((x1 Int)) (|bind_21[0:0][0:1][0:0]| x1)))
(check-sat)
(get-model)
(exit)