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