(set-logic HORN)
(set-info :source |
  Benchmark: /home/atondwal/src/mist/mochi-tests/sum.ml
  Generated by MoCHi
|)
(set-info :status unknown)
(declare-fun |fail_55[0:0]| ( Int) Bool)
(declare-fun |sum[0:2][0:0]| ( Int) Bool)
(declare-fun |sum[0:0][0:1][0:0]| ( Int  Int) Bool)
(declare-fun |sum[0:1][0:1][0:0]| ( Int  Int) Bool)
(assert (not (exists ((x0 Int)) (|fail_55[0:0]| x0))))
(assert (forall ((x0 Int)(x4 Int)) (=> (and (|sum[0:2][0:0]| x4) (|sum[0:2][0:0]| 11)) (|fail_55[0:0]| x0))))
(assert (forall ((x0 Int)(var73 Int)(var74 Int)) (=> (and (|sum[0:0][0:1][0:0]| 0 var73) (and (|sum[0:1][0:1][0:0]| 0 var74) (= x0 (+ var73 var74)))) (|sum[0:2][0:0]| x0))))
(assert (forall ((x3 Int)(x4 Int)) (=> (|sum[0:2][0:0]| 11) (|sum[0:1][0:1][0:0]| x3 x4))))
(assert (forall ((x3 Int)(x4 Int)) (=> (|sum[0:2][0:0]| 11) (|sum[0:0][0:1][0:0]| x3 x4))))
(assert (forall ((x0 Int)(var76 Int)(var77 Int)) (=> (and (|sum[0:0][0:1][0:0]| 0 var76) (and (|sum[0:1][0:1][0:0]| 0 var77) (= x0 (+ var76 var77)))) (|sum[0:2][0:0]| x0))))
(assert (forall ((x0 Int)(x1 Int)) (=> (= x1 1) (|sum[0:1][0:1][0:0]| x0 x1))))
(assert (forall ((x0 Int)(x1 Int)) (=> (= x1 10) (|sum[0:0][0:1][0:0]| x0 x1))))
(check-sat)
(get-model)
(exit)