Occur check in unification in the tableau prover made it impossible to solve formulas such as
$$
\forall x. D(x) \land \neg D(f(x))
$$
A workarround is used where variables in positive literals are renamed before unification, and maped back after.
A further issue was that when a found substitution substitutes more than one variable, an arbitrary order of substitution might not work; it is necessary to instantiate the most outer quantifier first. This is now tracked.
The PR also includes additional test cases that rely on these behaviours.
Occur check in unification in the tableau prover made it impossible to solve formulas such as $$ \forall x. D(x) \land \neg D(f(x)) $$ A workarround is used where variables in positive literals are renamed before unification, and maped back after.
A further issue was that when a found substitution substitutes more than one variable, an arbitrary order of substitution might not work; it is necessary to instantiate the most outer quantifier first. This is now tracked.
The PR also includes additional test cases that rely on these behaviours.