(benchmark arith_dl_46
  :logic QF_RDL
  :extrafuns ((a Real)
              (b Real)
              (c Real)
  )
  :formula
  (and
    (= a b)
    (= b c)
    (not (= (- a c) 0))
  )
  :status unsat
)
