Good idea from David Greenberg. It's probably possible to do tracing and visualization by creating a tracing Substitution. This substitution would implement IBind & IMplus so that the search tree is constructed. Of course some things should perhaps be ignored - recursions, unification.