–ALGORITMO
•3.3. Se o resolvente for uma cláusula vazia, então foi encontrada uma contradição. Se não for, acrescente-o ao conjunto de cláusulas disponíveis para o procedimento.
–Se a escolha de cláusulas a resolver em cada passo for feita de maneira sistemática, o procedimento de resolução encontrará uma contradição, se ela existir.
–EXEMPLO:
–Homem(Marco)
–Pompeiano(Marco)
–"x Pompeiano(x) ® Romano(x)
–Soberano(Cesar)
–"x Romano(x) ® (LealA(x,Cesar) v Odiar(x,Cesar))
–"x$y LealA(x,y)
–"x"y (Homem(x) ^ Soberano(y)) v (TentarAssassinar(x,y) ^ LealA(x,y)) 
–TentarAssassinar(Marco,Cesar)
–Logo, Odiar(Marco, Cesar)
•Primeiro convertemos os axiomas em cláusulas.
–1. Homem(Marco)
–2. Pompeiano(Marco)
–3. Ø Pompeiano(x1) v Romano(x1)
–4. Soberano(Cesar)
–5. Ø Romano(x2) v LealA(x2,Cesar) v Odiar(x2,Cesar)
–6. LealA(x3,f1(x3)
–7. Ø Homem(x4) v Ø Soberano(y1) v Ø TentarAssassinar(x4,y1) v Ø LealA(x4,y1)
–8. TentarAssassinar(Marco,Cesar)
–9. Ø Odiar(Marco,Cesar)