Starting with "G" being the unification problem to be solved and "S" being the identity substitution, rules are applied nondeterministically until the empty set appears as the actual "G", in which case the actual "S" is a unifying substitution. Depending on the order the paramodulation rules are applied, on the choice of the actual equation from "G", and on the choice of "R"’s rules in "mutate", different computations paths are possible. Only some lead to a solution, while others end at a "G" ≠ {} where no further rule is applicable (e.g. "G" = { "f"(...) ≐ "g"(...) }).