X = джон, Y = брунхильда;
X = мармадук, Y = гризелда;
X = мармадук, Y = эрминтруда;
X = мармадук, Y = брунхильда;
X = бертрам, Y = гризелда;
X = бертрам, Y = эрминтруда;
X = бертрам, Y = брунхильда;
X = чарлз, Y = гризелда;
X = чарлз, Y = эрминтруда;
X = чарлз, Y = брунхильда.
Вы должны быть уверены, что понимаете, почему Пролог породил решения в таком порядке. Прежде всего он ищет сопоставление для цели парень(X) и находит, что первым парнем является джон. Затем он находит сопоставление для цели девушка(Y), выбирая гризелда в качестве первой девушки. В этом месте мы запрашиваем новое решение, вводя ';'. Пролог поэтому считает, что последнее доказательство согласованности цели потерпело неудачу, и делает попытку вновь доказать согласованность последней из рассматривавшихся целей. Этой целью является утверждение девушка, встретившееся при доказательстве согласованности целевого утверждения возможная_пара. Обнаруживается альтернативный вариант эрминтруда, и, следовательно, следующим решением является пара джон и эрминтруда. Аналогично порождается пара джон и брунхильда в качестве третьего решения. При следующей попытке доказать согласованность целевого утверждения девушка(Y) Пролог обнаружит, что маркер, соответствующий этому целевому утверждению, находится в конце базы данных и, следовательно, попытка найти новое сопоставление для этого целевого утверждения терпит неудачу. Тогда делается попытка вновь доказать согласованность целевого утверждения парень(Х), маркер которого был установлен на первый факт предиката парень, и, следовательно, следующим найденным решением, соответствующим второму парню, является мармадук. Теперь, когда для этого целевого утверждения найдено новое решение, Пролог определяет, что следует делать далее – он должен найти сопоставление для цели девушка(Y), осуществляя поиск решения с самого начала базы данных. Так что он выбирает гризелда в качестве первой девушки. Следующие три решения содержат мармадук и имена трех девушек. Очередная попытка найти альтернативное решение для цели девушка заканчивается неудачей. Поэтому ищется другой парень, а поиск среди девушек производится с начала базы данных. Аналогичным образом происходит выполнение программы и далее.
В конце концов сложится ситуация, когда доказательство согласованности целевого утверждения девушка закончится неудачей и при этом будут также исчерпаны все решения для целевого утверждения парень.
