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