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

