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