(benchmark arith_dl_42
  :logic UNKNOWN
  :extrafuns ((x Int) (y Int) (a Int) (b Int))
  :formula
  (and (= x a) (= y b) (= (- y x) 0) (= 0 (- a b))
       (<= 0 (- a b)) (>= (- y x) 1))
  :status unsat
)
