(benchmark qf_arith13
  :logic UNKNOWN
  :extrafuns ((a Int) (b Int) (c Int))
  :formula
  (and (> a 0) (< a 3) (> b 0) (< b 3) (> c 0) (< c 3)
    (not (= a b)) (not (= a c)) (not (= b c)))
  :status unsat
)
