Only Patrick answered this one (and he did that correctly :-)

By the way - sorry for being so late. I just realized that I have about a week
to finish a huge amount of work...

> Write down the Circumscription formula.
> Circumscribe P in the following theory
> 
> T = { P(A), P(B), A=/=B }
> 

The circumscription formula (for formula circumscription) has many variants,
all equivalent. One of the variants is:

For a theory A, a formula P, and an n-tuple of predicate or literal constant
names Z, the circumscription of P in A varying Z (denoted Circ[A;P;Z]) is
A(P,Z) & \forall p,z (A(p,z) => \neg (p P(x))) & (\exists x (P(x) & \neg p(x))))


Take A=T, which means A= P(A) & P(B) & A=/=B. The minimal P that satisfies that
is P={A,B}. It is obvious that such a $P$ satisfies A(P), and also simple
to show that it is minimal.
Thus, Circ[A;P] \equiv "A=/=B & P={A,B}"
(we omit Z when there is nothing varied)
Comment : what I gave is not a formal proof, but it suffices for most
purposes (like taking the Qual :-)

Eyal