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