(benchmark qf_ufidl_4
  :logic QF_UFIDL
  :extrafuns ((a Int) (b Int) (c Int) (f Int Int))
  :formula
  (and (<= b a) (<= (- a b) 1) (not (= (f a) (f b))) (not (= (f (- a 1)) (f b))) )
  :status unsat
)
