Grounding performance issue when using functions

[Broes De Cat]

Apparently, unnesting of terms does not check for existing occurrences before introducing a new variable. It is even worse if the user intended to take care of this himself by introducing the variable.

Example:

!x y ...: f(x)=y & ... => p(y,y,y,y).

This is first nested (by ReplaceVariableUsingEqualities) to

!x y ...: ... => p(f(x), f(x), f(x), f(x))

and then unnested (by UnnestTerms) to

!x y a1 a2 a3 a4 ...: f(x)=a1 & f(x)=a2 & f(x)=a3 & f(x)=a4 & ... => p(a1,a2,a3,a4)

End result: grounding takes ages and contains a lots of duplicate subformulas.