(benchmark qf_arith9
  :logic UNKNOWN
  :extrafuns ((x Int) (y Int) (z Int))
  :extrapreds ((q Int Int))
  :formula
  (and (< (+ x y) 5) (>= (+ x y) 0) (>= x 0) (>= y 0)
    (not (q x y))
    (q 0 0)
    (q 0 2)
    (q 0 4)
    (q 1 1)
    (q 1 3)
    (q 2 0)
    (q 2 2)
    (q 3 1)
    (q 4 0)
    (= (+ (* 7 x) (* 7 y)) (* 2 z)))
  :status unsat
)
