(benchmark qf_arith14
  :logic UNKNOWN
  :extrafuns ((x Int) (y Int) (z Int))
  :extrapreds ((p Int))
  :formula
  (and (> x 0) (< y 2) (< z 3) (= x (+ z y)) (not (= x 2))
       (p 1) (p 3) (p 4) (not (p x)))
  :status unsat
)

