(benchmark qnt_6
  :logic UNKNOWN
  :extrasorts (ELEMENT)
  :extrafuns ((a ELEMENT)(b ELEMENT)(c ELEMENT))
  :extrapreds ((p ELEMENT))
  :status unsat
  :formula
  (and
    (forall (?x ELEMENT) (p ?x))
    (or (not (p a)) (not (p b))))
  :status unsat
  )
