Thin out the substitutions?

[jvoigtlaender]

Possibly controlled by a parameter (whether or not to thin out substitions).

I assume (but not having thought very deeply about this) it always makes sense to drop variable assignments from a substitution where that the variable itself does neither appear in the query above nor appear in the query below the connection at which the unifier is printed.

For example, in

this would allow to drop the assignments for C1, N2, F1, G1, C2, N3, C4, N5,

[jvoigtlaender]

The part

nor appear in the query below the connection at which the unifier is printed

is likely superfluous.

A variable X / ... should never appear in the query to which a connection with that in its substitution leads. (Unless weird things happen with unification-without-occurs-check, which I don't actually know whether or not this check is done in the implementation of unification here.)