% problem-set/puzzles/birds/bird2.ver1.in
% created : 06/28/88
% revised : 08/11/88

% description:
%
% This is an input file for Chapter 9 problem 2,
% 'Egocentric?'.
% There exists a mocking bird (Mock).  For all birds x and y, there exists 
% a bird z that composes x with y for all birds w.
% Hypothesis: There exists a bird x that is fond of itself.  

% representation:
%

set(para_from).
set(para_into).
set(para_from_left). 
set(para_from_right).


list(axioms).                                          

% There exists a mocking bird (Mock).
% Finding clause:
%    TEx FAy [response(x,y) = response(y,y)].
%    Letting Mock = x,
%    response(Mock,y) = response(y,y).
% Clause:

EQUAL(response(Mock,y),response(y,y)).

% x is equal to x.
% Clause:

EQUAL(x,x).

% For all birds x and y, there exists a bird z that composes
% x with y for all birds w.
% Finding clause:
%    FAx FAy TEz FAw [response(z,w) = response(x,response(y,w))].
%    Letting comp(x,y) = z,
%    response(comp(x,y),w) = response(x,response(y,w)).
% Clause:

EQUAL(response(comp(x,y),w),response(x,response(y,w))).

end_of_list.


list(sos).                                               

% Hypothesis: There exists a bird x that is fond of itself.  
% Finding clause:
%    -TEx [response(x,x) = x].
%    FAx -[response(x,x) = x].
% Denial clause:

-EQUAL(response(x,x),x) | $ans(x).

end_of_list.
