
The backward chaining inference engine is started to look for any set of bindings which satisfy goal-to-prove . Using those bindings, pattern-to-instantiate is instantiated and returned.
 Two values are returned. The second value indicates with T that a proof was found, or with nil that no proof exists. In the former case, the first value is the instantiated version of  pattern-to-instantiate , in the latter case, the first value is nil .