Improvements to using the proof processor

[maartenflippo]

This PR should be rebase-merged instead of squash merged.

We make two changes:

1. Use clap-verbosity-flag to control the log level via the command line. By default, we set it to info, -v goes to debug, -vv or -v -v goes to trace.
2. Log number of proof stages before and after trimming, as well as the number of inferences (see screenshot)
   .

Review re-requested