 If two or more literals occurring in a clause C share an mgu θ then Cθ is a factor of C. For example, in R(x,a) ∨ ~K(f(x),b) ∨ R(c,y) the literals R(x,a) and R(c,y) unify with mgu {x ← c, y ← a} and, hence, R(c,a) ∨ ~K(f(c),b) is a factor of the original clause. 