Which formalism is best suited for automated theorem proving in set theory?
There are numerous ways of formalizing set theory:


ZFC uses first-order logic and a primitive relation $\in$
NBG uses first-order logic, a primitive relation $\in$, and a primitive predicate $S$
Church's type theory is multi-sorted and uses infintely many types
Type theory is similar to set theory, but not quite the same
Second-order arithmetic, through some coding tricks, can express many things we usually want to express in analysis
etc.


But this is all quite irrelevant to what you are doing. You seem to be using automated theorem provers as "black boxes" to prove simple theorems in set theory. This is a hit-and-miss activity: some theorem provers will prove some simple things, and others will prove other simple things, but they will all fail on statements that mathematicians consider "completely trivial". Such is the state of automated theorem proving.

Rather than worrying which particular formalism you are using, you should investigate which automated theorem prover is good for what. It is also very likely that you do not actually need set theory. It would be helpful if you described what you're doing, but not here, this should go on cstheory.stackexchange.com. There perhaps we can suggest a good way of formalizing whatever you are doing.