обработать( да, Цель,_, Перем, Трасса, правда, N) :-

след_индекс( Инд),

% Получить новый индекс для "сказано"

Инд1 is Инд + 1,

( запрос_перем( Перем),

assertz( сказано( Цель, правда, Инд) );

% Запись решения

копия( Цель, Копия), % Копирование цели

ответпольз( Цель, Копия, Трасса, Ответ, Инд1) ).

% Есть еще решения?

обработать( нет, Цель, _, _, _, ложь, N) :-

копия( Цель, Копия),

сказано( Копия, правда, _), !,

% 'нет' означает, больше нет решений

assertz( конец_ответов( Цель) ),

% Отметить конец ответов

fail;

след_индекс( Инд),

% Следующий свободный индекс для "сказано"

assertz( сказано( Цель, ложь, Инд) ).

% 'нет' означает нет ни одного решения

формат( Пер, Имя, Имя, Перем, [Пер/Имя | Перем]) :-

var( Пер), !.

формат( Атом, Имя, Атом, Перем, Перем) :-

atomic( Атом), !,

atomic( Имя).

формат( Цель, Форм, Вопрос, Перем0, Перем) :-

Цель =.. [Функтор | Apг1],

Форм =.. [Функтор | Форм1],

формвсе( Apг1, Форм1, Арг2, Перем0, Перем),

Вопрос =.. [Функтор | Арг2].

формвсе( [ ], [ ], [ ], Перем, Перем).

формвсе( [Х | СпХ], [Ф | СпФ], [В | СпВ], Перем0, Перем) :-

формвсе( СпХ, СпФ, СпВ, Перем0, Перем1),

формат( X, Ф, В, Перем1, Перем).

запрос_перем( [ ]).

запрос_перем( [Переменная/Имя | Переменные]) :-

nl, write( Имя), write( '='),

read( Переменная),

запрос_перем( Переменные).

выд_трассу( [ ]) :-

nl, write( 'Это был ваш вопрос'), nl.

выд_трассу( [Цель по Прав | Трасса] ) :-

nl, write( 'Чтобы проверить по' ),

write( Прав), write( ', что'),

write( Цель),

выд_трассу( Трасса).

конкретный( Терм) :-

нумпер( Терм, 0, 0). % Нет переменных в Терм'е

% конкретизация( Т1, Т2) означает, что Т2 - конкретизация Т1,

% т.е. терм Т1 - более общий, чем Т2, или той же степени

% общности, что и Т2