(benchmark qnt_7
  :logic UNKNOWN
  :extrasorts (ELEMENT)
  :extrafuns ((a ELEMENT)(b ELEMENT)(c ELEMENT))
  :extrapreds ((p ELEMENT) (q ELEMENT))
  :status sat
  :formula
  (and
    (forall (?x ELEMENT) (implies (p ?x) (q ?x)))
    (or (not (p a)) (not (p b)) (not (p c))))
  :status sat
  )
