A simple overview of how the prover works
Six built-in proof techniques are used by ACL2 to decompose the goal formula into subgoals.
But you can add additional techniques, called clause processors.
The various techniques are tried in turn, with simplification first and induction last. Each technique reports one of three outcomes: it found nothing to change (i.e., the technique doesn't apply to that subgoal), it decided to abort the proof attempt (typically because there is reason to believe the proof is failing), or it decomposed the goal into k subgoals.
The last outcome has a special case: if k is 0 then the technique proved the goal. Whenever k is non-0, the process starts over again with simplification on each of the k subgoals. However, it saves up all the subgoals for which induction is the only proof technique left to try. That way you see how it performs on every base case and induction step of one induction before it launches into another induction.
It runs until you or one of the proof techniques aborts the proof attempt or until all subgoals have been proved.
Note that if simplification produces a subgoal, that subgoal is re-simplified. This process continues until the subgoal cannot be simplified further. Only then is the next proof technique is tried. Such subgoals are said to be stable under simplification.
While this is happening, the prover prints an English narrative describing the process. Basically, after each goal is printed, the system prints an English paragraph that names the next applicable proof technique, gives a brief description of what that technique does to the subgoal, and says how many new subgoals are produced. Then each subgoal is dealt with in turn.
If the proof is successful, you could read this log as a proof of the conjecture. But output from successful proofs is generally never read because it is not important to The Method described in introduction-to-the-theorem-prover.
The output of an unsuccessful proof attempt concludes with some key checkpoints which usually bear looking at.
For more information about how ACL2 orchestrates its proof techniques, see hints-and-the-waterfall.