(benchmark arith_dl_7
  :logic UNKNOWN
  :extrafuns ((x Int) (y Int) (z Int) (a Int) (b Int) (c Int) (d Int) (e Int))
  :extrapreds ((p Int) (q Int Int))
  :formula
  (and (not (= (- x z) 2)) (<= (- x y) 1) (<= (- y x) (~ 1)) (<= (- y z) 1) (<= (- z y) (~ 1)))
  :status unsat
)
