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