mtzguido

Indeed. Most engines are pretty bad without their opening books. There was surprisingly little stress on this.

Sadly not yet. You can see each individual intermediate state but the thing runs fully. We certainly plan to add such a feature though!

We've been mostly studying hammer-like tactics to, say, apply some theorems at specific places in the goal (which the SMT might be bad at), and not for chaining small rewriting or logical steps (which the SMT is good at).