(benchmark qf_ufidl_1
  :logic QF_UFLA
  :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 b)) (f 1))) )
  :status unsat
)
