constant | variable | function | |

constant | SUCCESS if constants are the same, FAIL otherwise | {variable/constant} | FAIL |

variable | {variable/constant} | {variable/variable} | {variable/function} if variable does not occur in function, FAIL otherwise |

function | FAIL | {variable/function} if variable does not occur in function, FAIL otherwise | the result of unifying the arguments if the functions are the same and the arguments unify, FAIL otherwise |

- P(x) unifies with P(A) using the substitution {x/A}
- P(f(x), y, g(y)) unifies with P(f(w), z, g(A)) using the substitutions {x/w, y/z, z/A}
- P(f(x), y, g(y)) fails to unify with P(f(w), B, g(A)) since y is unified with B and so it cannot be unified with A
- P(f(x), y, g(y)) fails to unify with P(f(w), f(A), g(A)) since y is unified with f(A) and so it cannot be unified with A