There have been attempts to (partially) translate expressive onotologies such as SUMO or Cyc to first-order logic and to use first-order automated theorem provers for detecting errors and inconsistencies. Claims have been made that these translation results are now ready for use within practival applications. This paper adopts a critical attitude: The fact that a translation of an expressive ontology into a target logic (be it first-order or higher-order or modal, etc.) exists for which satisfiability can be shown does not imply that the approach is ready for application. What might still be missing is a guarantee of the faithfulness of the translation. The issue is illustrated in connection with a (knowingly) unfaithful translation of SUMO into classical higher-order logic. The focus is on a small provably satisfiable subset of this translated SUMO ontology. By adding some intuitively compatible and sound ABox axioms the unfaithfulness of the translation can easily be revealed with automated theorem provers. Without he ABox content, however, the problem remains undetected. We thus argue for the extensive integration of ABox information into automated consistency checking for expressive ontologies, in particular, when logic translations are involved and when faithfulness has not or cannot be formally ensured.