Recall that the satisfaction process generates an instantiation for the variables in the top-level query. We can visualize the behavior of the Prolog evaluator as the exploration of a computation tree . Each edge is labeled with the unifier that leads to the child. Sucessful evaluation of a query amounts to a traversal of the tree beginning at the root and eventually reaching a success leaf. The values of the query variables corresponding to such an evaluation are determined by composing the substitutions on the edges of the path from root to success leaf.
Every valid solution is somewhere in the search tree.
Prolog always searches the tree in depth-first order . It defines the order of branches to be the same as the order of clauses in the Prolog source program. I.e., the clause listed first gets used first, and its consequences are completely explored before using the next clause. So search order can determine whether or not a search succeeds or runs forever. Other orderings will lead to finding one or both solutions.