(declare-fun a (Int) Int)
(declare-fun b (Int) Int)
(declare-fun c (Int) Int)
(declare-fun d () Int)
(declare-fun h () Int)
(declare-fun e () Int)
(declare-fun f () Int)
(declare-fun i () Int)
(assert
 (let ((g d)
       (j h)
       (bb i)
       (bi d)
       (bj 0)
       (cm (b h))
       (dw h)
       (dz (c f))
       (eb (+ d i))
       (ec (+ d h)))
  (and
   (or (and (distinct dz bb e) (= bi bj) (= cm f i)) (= dw f))
   (distinct d e)
   (distinct h e i)
   (< d 7)
   (< h 7)
   (< (c (ite (< eb 7) eb d)) (c (ite (< ec 7) ec d))))))
(check-sat)
(get-model)

(define-fun i () Int
    6)
  (define-fun h () Int
    1)
  (define-fun f () Int
    1)
  (define-fun e () Int
    3)
  (define-fun d () Int
    1)
  (define-fun c ((x!0 Int)) Int
    (ite (= x!0 2) 0
      6))
  (define-fun b ((x!0 Int)) Int
    4)
  (define-fun a ((x!0 Int)) Int
    0)