uninterestingVariablesAreObliterated

Solves a(X) against TestingClauseTheories.callsWithVariablesTheory (a(A) :- b(A), d(Z). and similar rules introducing intermediate variables Z/W); succeeds with X bound to 1, and the resulting substitution contains only X — the intermediate variables introduced along the way are obliterated from the final substitution once they are no longer needed.