(benchmark qf_arith4
  :logic UNKNOWN
  :extrafuns ((a Int) (b Int) (x Int) (f Int Int))
  :extrapreds ((p Int))
  :formula
  (and (<= a b)
       (<= b (+ a x))
       (= x 0)
       (or (= (f a) (f b)) (and (p a) (not (p (+ b x))))))
  :status unsat
)
