(benchmark qf_arith2
  :logic UNKNOWN
  :extrafuns ((x Int) (y Int) (f Int Int) (h Int Int))
  :extrapreds ((P Int))
  :formula
  (and (<= x y) (<= y x)
       (P (- (h x) (h y)))
       (not (P 0))
       (= (f x) 0))
  )
