  In this note we observe that automated theorem provers (ATPs) that
recursively enumerate theorems in a particular way will fail to identify some
valid theorems for a reason that is analogous to how G\"odel proved the
existence of what are now referred to as G\"odel statements. This observation
has no significant practical or theoretical implications, but it may be of
pedagogical value for honing the intuition of students about recursive
enumeration in the context of ATP.
