; This example illustrates basic arithmetic and
; uninterpreted functions

(declare-const h  Int)
(declare-const k  Int)
(declare-const l  Int)
(declare-const p  Int)
(declare-const r  Int)

;; All in range 1..5
(assert (< 0 h))
(assert (>= 5 h))
(assert (< 0 k))
(assert (>= 5 k))
(assert (< 0 l))
(assert (>= 5 l))
(assert (< 0 p))
(assert (>= 5 p))
(assert (< 0 r))
(assert (>= 5 r))

;; Different floors
(assert (not (= h k)))
(assert (not (= h l)))
(assert (not (= h p)))
(assert (not (= h r)))
(assert (not (= k r)))
(assert (not (= l p)))
(assert (not (= l r)))
(assert (not (= p r)))

;; Constraints
(assert (> 5 h))
(assert (< 1 k))
(assert (< 1 l))
(assert (> 5 l))
(assert (> p k))
(assert (< 1 (abs (- r l))))
(assert (< 1 (abs (- k l))))

(check-sat)
(get-model)
(exit)