Изложим последовательность действий.
Находим первый (и единственный) предикат цели дядя (X, Y). Заменяем найденный предикат правой частью процедуры с этим именем, записанной в БЗ. Получим трансформированную цель — фрейм:
брат (X, Р), родитель (Р, Y).
С первым предикатом этого фрейма действуем аналогично, получаем фрейм:
мужчина (X), родитель (Q, X), родитель (Q, Р), Х<>Р, родитель (Р, Y).
При этом во избежание коллизии, развивая фрейм цели, вводим новые переменные, отличные от тех, которые уже были использованы в записях БЗ.
Вновь входим в процедуру с именем первого предиката цели и начинаем первый уровень ветвления, используя первый клоз процедуры — факт мужчина (иван). С его помощью производим первое связывание переменных, т.е. подстановку конкретного значения.
Предикат цели, породивший это связывание, из трансформируемой цели исключается, т.е. заменяется своей «пустой» правой частью:
родитель (Q, иван), родитель (Q, Р), иван <>Р, родитель (P,Y).
Обращаемся к процедуре "родитель", начиная второй уровень ветвления. Первый клоз этой процедуры родитель (марья, иван) определяет дальнейшее связывание переменных:
родитель (марья, Р), иван <> Р, родитель (Р, Y).
Вновь входим в процедуру "родитель" (третий уровень ветвления), находим клоз родитель (марья, иван). Трансформируем цель, получаем новый фрейм:
иван <> иван, родитель (иван, Y).
Возникает противоречие, т.е. унификация не проходит.
Ищем на данном шаге ветвления другой вариант связывания, находим следующий клоз:
родитель (марья, василий).
