Considere as cláusulas C1 e C2, representadas, respectivamente, pelos conjuntos { ¬ A(x),B(x)} e { A(g(y)),B(y)}.
Um resolvente dessas cláusulas é