Create overnight version

[madvorak]

I believe it is possible to create a stronger version of Aesop that runs much longer and has a slightly higher success rate. The motivation is that the tactic could be used to run overnight to search for a proof. It should be the ? version because the call to this tactic cannot stay in the "production" code.

Imagine you run aesop with unlimited heartbeats. How can we use the available time instead of halting early as aesop normally does? One thing to try is to use every imported lemma with some unsafe probability. The search space will explode, and there will be a chance (albeit small) to find a proof that aesop missed.

Note that we currently don't have any long-running tactic, hence the new tactic wouldn't have to be cost-effective in order to be pareto-optimal.