The notion of identity criteria marked the dawn of contemporary formal ontology. Despite a number of issues this notion has raised, the quest for them still seems to be worthwhile, in particular in the case of a formal ontology built in the context of information systems. In the current paper I investigate the benefits and costs of using automatic theorem provers in the task of identifying such criteria for formal ontologies that are expressed in a prover-processable language. To this end two detailed case studies were performed – each concerned an upper-level ontology presented in a recent volume of the Applied Ontology journal. The identity criteria found by the process described in this paper turned out to be not particularly illuminating. The respective theorems that define them are rather direct consequences of the axioms, so proofs and models provided by the prover do not provide any new insights into the actual conceptual contents of the formal ontologies.