A quick skim over the code, shows it to be fairly small. ~1000 lines for the prover (little more in ACL2, little bit less in Scheme). And about another 1000 li

A quick skim over the code, shows it to be fairly small. ~1000 lines for the prover (little more in ACL2, little bit less in Scheme). And about another 1000 lines for all the examples from the book (they too would need to be redone)