Reguła rozstrzygania dla klauzul pierwszego rzędu jest po prostu zniesioną wersją reguły rozwiązywania zdań podanej na stronie 226. Dwie klauzule, które z założenia są znormalizowane oddzielnie, tak że nie mają wspólnych zmiennych, mogą zostać rozwiązane, jeśli zawierają komplementarne literały. Literały zdaniowe są komplementarne, jeśli jeden jest negacją drugiego; Literały pierwszego rzędu są komplementarne, jeśli jeden łączy się z negacją drugiego. Tak więc mamy
gdzie 
. Na przykład możemy rozwiązać dwie klauzule
eliminując dopełniające się literały Loves (G(x),x) i ¬Loves(u,v) z unifikatorem
, wytworzyć klauzulę rezolucyjną
Ta reguła jest nazywana regułą rozwiązywania binarnego, ponieważ rozwiązuje dokładnie dwa literały. Sama reguła rozwiązywania binarnego nie daje pełnej procedury wnioskowania. Reguła pełnej rozdzielczości rozwiązuje podzbiory literałów w każdej klauzuli, które są unifikowalne. Alternatywnym podejściem jest rozszerzenie faktoringu – usunięcie zbędnych literałów – do przypadku pierwszego rzędu. Faktoring zdaniowy redukuje dwa literały do jednego, jeśli są identyczne; faktoring pierwszego rzędu redukuje dwa literały do jednego, jeśli są one unifikowalne. Unifikator musi być zastosowany do całej klauzuli. Połączenie rozdzielczości binarnej i faktoringu jest kompletne.