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