Less grounding by (syntactix/semantic) shared Tseitin introduction.

[Broes De Cat]

Will allow to solve for example the specification theory T : V { !x: P(x) | Q(x). !x: P(x) | Q(x) | !y z: R(x,y,z). } without grounding the latter sentence.

[Broes De Cat]

And also for variable introduction when unnesting terms.