풀이 트리의 각 노드는 제약 조건의 집합 C, 가정의 집합 H, 목표들의 큐 G를 가지고 있음.

맨 처음에는 루트 노드 밖에 없고, 루트 노드의 C와 H는 공집합으로 G는 주어진 질의만 들어 있는 큐로 각각 초기화됨.

G에서 목표 하나를 꺼내서 H를 이용하여 귀납법을 시도해봄.

실패하면 매칭되는 공리마다 자식 노드를 만들고 각 자식노드의 G에 공리의 머리부분의 식(추가 목표)을 넣어준 다음 제약조건을 추가함.

성공하면 매칭되는 가정마다 자식 노드를 만들고 각 자식노드의 C에 제약 조건을 추가한 뒤 다시 목표 하나를 꺼냄.

G에서 목표를 다 꺼내면 답임.