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

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

% representation:
%

% x is equal to x.
% Clause:

EQUAL(x,x).

% First part of denial clause: there exists a bird which is fond
% of some other bird. 

EQUAL(response(A,B),B).        

% Hypothesis: Any bird that is fond of at least one bird must be happy.
% Finding clause:
%   - FAx [If TEy (xy = y) then TEz TEw (xz = w) and (xw = z)].
%   TEx -[- TEy (xy = y) | TEz TEw ((xz = w) and (xw = z))].
%   TEx [ TEy (xy = y) and - TEz TEw ((xz = w) and (xw = z)) ].
%   TEx [ TEy (xy = y) and FAz FAw -((xz = w) and (xw = z)) ].
%   Letting A = x,
%   TEy (Ay = y) and FAz FAw -[(Az = w) and (Aw = z)].
%   Letting B = y,
%   (AB = B) and [-(Az = w) | -(Aw = z)].
% Denial clause:
%   Placing (AB = B) in the list of axiom, we have:

-EQUAL(response(A,z),w) | -EQUAL(response(A,w),z).