% est(K,Q) holds if query Q can be established from knowledge base K.
% This version performs Prolog back-chaining.
% It handles equality, negation, and variables.

est(_,[]).                                          % No query atoms
est(K,[eq(X,X)|T]) :- est(K,T).                     % Equality.
est(K,[not(A)|T]) :- \+ est(K,[A]), est(K,T).       % Negation.
est(K,[A|T]) :- member_copy([A|B],K), append(B,T,Q), est(K,Q).

% member_copy(X,L): X is an atomic element of L or a copy otherwise.
member_copy(X,L) :- member(X,L), X=[_].
member_copy(X,L) :- member(E,L), \+ E=[_], copy_term(E,X).
