(benchmark qf_arith7
  :logic UNKNOWN
  :extrafuns ((x Int) (y 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 1)
    (q 0 2)
    (q 0 4)
    (q 1 1)
    (q 1 2)
    (q 2 0)
    (q 2 1)
    (q 2 2)
    (q 3 0)
    (q 3 1)
    (q 4 0))
  :status sat
)
