Major Section: MISCELLANEOUS
When ACL2 gives up it does not mean that the submitted conjecture is invalid, even if the last formula ACL2 printed in its proof attempt is manifestly false. Since ACL2 sometimes generalizes the goal being proved, it is possible it adopted an invalid subgoal as a legitimate (but doomed) strategy for proving a valid goal. Nevertheless, conjectures submitted to ACL2 are often invalid and the proof attempt often leads the careful reader to the realization that a hypothesis has been omitted or that some special case has been forgotten. It is good practice to ask yourself, when you see a proof attempt fail, whether the conjecture submitted is actually a theorem.
If you think the conjecture is a theorem, then you must figure out from ACL2's output what you know that ACL2 doesn't about the functions in the conjecture and how to impart that knowledge to ACL2 in the form of rules. However, see proof-tree for a utility that may be very helpful in locating parts of the failed proof that are of particular interest. See also the book ``Computer-Aided Reasoning: An Approach'' (Kaufmann, Manolios, Moore), as well as the discussion of how to read Nqthm proofs and how to use Nqthm rules in ``A Computational Logic Handbook'' by Boyer and Moore (Academic Press, 1988).
If the failure occurred during a forcing round,
see failed-forcing.