[YICES-HELP] quantification basics?

[Mark R. Tuttle]

Can anyone help me understand why YICES says "unknown" instead of
"unsat" for the following example?

(define-type elem)
(define-type set)
(define mem::(-> elem set bool))

(define S::set)
(define T::set)

(define equal_axiom::bool
   (forall (a::set b::set)
      (=> (not (= a b))
          (exists (x::elem) (not (= (mem x a) (mem x b)))))))

(define equal_claim::bool
      (=> (forall (x::elem) (= (mem x S) (mem x T)))
	  (= S T)))

(assert equal_axiom)
(assert (not equal_claim))
(check)

I was hoping that Skolemization and pattern matching would let YICES
simulate the reasoning

(forall (x::elem) (= (mem x S) (mem x T)))
(not (= S T))

then

(forall (x::elem) (= (mem x S) (mem x T)))
(exists (x::elem) (not (= (mem x S) (mem x T))))

then

(forall (x::elem) (= (mem x S) (mem x T)))
(not (= (mem SKL S) (mem SKL T)))

then

(= (mem SKL S) (mem SKL T))
(not (= (mem SKL S) (mem SKL T)))

then

false

I understand that quantification makes things only semi-decidable, I'm
just looking for a slightly deeper understanding of what YICES can do
with quantification.  I'm running 1.0.29.

Thanks
Mark Tuttle, tuttle at acm.org