(benchmark qf_arith8
  :logic UNKNOWN
  :extrafuns ((x Int) (y Int))
  :extrapreds ((q Int Int))
  :formula
  (and (= (+ x y) 5) (>= x 0) (>= y 0)
    (not (q x y))
    (q 0 5)
    (q 1 4)
    (q 2 3)
    (q 4 1)
    (q 5 0))
  :status sat
)
