Okay I did some more experiments and I was now, interestingly enough,
completely unable to reproduce the situation where Green /didn't/
timeout. So I have no idea what was going on there; perhaps I made a
mistake in testing it. I don't know.
It might be wise to remove "continuous_on_discrete"
This trace doesn’t tell us much because it’s only blast’s internal search.
Looks like every “continuous_on” goal is immediately solved. But after this
search exits, the reconstructed Isabelle proof will fail. Blast will re-enter
but it will only find these unsound proofs, and probably won’t
