(benchmark qfuf_3
  :status unsat
  :logic QF_UF
  :extrafuns ((a U) (b U) (c U) (f U U))
  :extrapreds ((p U))
  :formula 
  (and
    (= a c)
    (= c b)
    (or (not (= (f a) (f b)))
        (and (p a) (not (p b)))))
)
