run instructions without prover output
(quiet induct prove)
(quiet &rest instruction-list)
Run the instruction-list through the top-level loop with no output.
See ACL2-pc::quiet; the two commands are equivalent, except that the
quiet! command additionally suppresses the printing of goal
identifiers (as with set-print-clause-ids).