  I introduce an approach for automated reasoning in first order set theories
that are not finitely axiomatizable, such as $ZFC$, and describe its
implementation alongside the automated theorem proving software E. I then
compare the results of proof search in the class based set theory $NBG$ with
those of $ZFC$.
