(benchmark qnt17
:status unsat
:difficulty { 0 }
:logic AUFLIA
:extrasorts (U)
:extrapreds ((p U))
:extrafuns ((a U) (b U))
:formula
(and
 (p a)
 (p b)
 (forall (?x U) (or (= a ?x) (= b ?x)))
 (exists (?x U) (not (p ?x)))))
