(benchmark qf_arith26
  :logic UNKNOWN
  :extrafuns ((x Int) (y Int) (z Int))
  :extrapreds ((P Int))
  :status unsat
  :formula
  (and (= x z)
       (not (P x))
       (P y)
       (<= x y)
       (<= y z)
       )
)
