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