A successful example computation path for the unification problem { "app"("x","app"("y","x")) ≐ "a"."a"."nil" } is shown below. To avoid variable name clashes, rewrite rules are consistently renamed each time before their use by rule "mutate"; "v"2, "v"3, ... are computer-generated variable names for this purpose. In each line, the chosen equation from "G" is highlighted in red. Each time the "mutate" rule is applied, the chosen rewrite rule ("1" or "2") is indicated in parentheses. From the last line, the unifying substitution "S" = { "y" ↦ "nil", "x" ↦ "a"."nil" } can be obtained. In fact,