% problem-set/puzzles/carroll/ggson.ver1.in
% created : 07/14/86
% revised : 07/15/88

% description:
%
% This run attempts to solve "The Great-grandson Problem" using
% hyper-resolution, binary resolution, and UR-resolution.
% NO PROOF
%
%    			  THE GREAT-GRANDSON PROBLEM
%
%  1. A man can always master his father.
%  2. An inferior of a man's uncle owes that man money.
%  3. The father of an enemy of a friend of a man owes that man nothing.
%  4. A man is always persecuted by his son's creditors.
%  5. An inferior of the master of a man's son is senior to that man.
%  6. A grandson of a man's junior is not his nephew.
%  7. A servant of an inferior of a friend of a man's enemy is never
%     persecuted by that man.
%  8. A friend of a superior of the master of a man's victim is that
%     man's enemy.
%  9. An enemy of a persecutor of a servant of a man's father is that 
%     man's friend.
%
%  The Problem is to deduce some facts about the great-grandsons.
%                  --- Lewis Carroll from "Symbolic Logic" p362.

% representation:
%

set(hyper_res).
set(binary_res).
set(UR_res).


list(axioms). 

-Father(x,y) | Master(y,x).
NotSuperior(x,y) | NotUncle(x,z) | -NotOwes(y,z).
-Father(x,y) | -Enemies(y,z) | -Friends(z,w) | NotOwes(x,w).
-Father(x,y) | NotOwes(y,z) | Persecutes(z,x).
NotSuperior(x,y) | -Master(x,z) | -Father(w,z) | Senior(y,w).
-Father(x,y) | -Father(y,z) | -Senior(w,x) | NotUncle(w,z).
-Master(x,y) | NotSuperior(z,x) | -Friends(z,w) | -Enemies(w,t) |
  -Persecutes(t,y).
-Friends(x,y) | NotSuperior(y,z) | -Master(z,w) | -Persecutes(t,w) |
  Enemies(x,t).
-Enemies(x,y) | -Persecutes(y,z) | -Master(w,z) | -Father(w,t) |
  Friends(x,t).

-Father(x,y) | -Father(y,z) | -Father(z,w) | Greatgrandson(x,w).
-Friends(x,y) | Friends(y,x).
-Enemies(x,y) | Enemies(y,x).
-Friends(x,y) | -Enemies(x,y).
Friends(x,y) | Enemies(x,y).

end_of_list.


list(sos).

Father(A,B).
Father(B,C).
Father(C,D).

end_of_list.
