Equality is handled at unification time. It’s as if the KB had a unique names assumption: objects with different names are assumed to be not equal, unless you specifically override the assumption by asserting that two objects are equal, e.g. (equals Fred Joe). No inference concerning equality is done at unification time.

ASKs and Direction Home Overview of Cyc Inferencing