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