(benchmark qnt_5
  :logic UNKNOWN
  :extrasorts (U)
  :extrafuns ((a U) (b U) (f U U))
  :extrapreds ((p U) (q U U))
  :status unsat
  :formula
  (and (forall (?x U) (implies (q ?x ?x) (p ?x))) 
       (= a b)
       (q (f b) (f b))
       (not (p (f a))))
  :status unsat
)
