Um, I don’t see value in excluding statements that have e.g. a forall-exists-forall-exists sequence of quantifiers at the outer level?
I just wanted to show it seems possible to do better and that was easier to do considering only a subset of statements.
Ah, ok.
I just wanted to show it seems possible to do better and that was easier to do considering only a subset of statements.
Ah, ok.