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

% description:
%
% This is an input file for Chapter 9 problem 6, 
% 'Compatible Birds'.

% representation:
%

% There exists a mockingbird (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))).

% Hypothesis: Any two birds are compatible.
% Finding clause (using xy to replace response(x,y) for compactness):
%    -FAx FAy TEw TEz [(xw = z) and (yz = w)].
%    TEx TEy FAw FAz -[(xw = z) and (yz = w)].
%    Letting A = x, B = y, x = w, and y = z,
%    -(Ax = y) | -(By = x).
% Denial clause:

-EQUAL(response(A,x),y) | -EQUAL(response(B,y),x).