% problem-set/puzzles/carroll/pigs.ver1.clauses 
% created : 07/19/88
% revised : 07/19/88 

% description:
%
% This run solves "The Pigs and Balloons Puzzle" by Lewis Carroll
% using UR-resolution. 
%
%				 The Pigs and Balloons Puzzle
%
% (1) All, who neither dance on tight ropes nor eat penny-buns,
%     are old.
% (2) Pigs, that are liable to giddiness, are treated with respect.
% (3) A wise balloonist takes an umbrella with him.
% (4) No one ought to lunch in public who looks ridiculous and eats
%     penny-buns.
% (5) Young creatures, who go up in balloons, are liable to 
%     giddiness.
% (6) Fat creatures, who look ridiculous, may lunch in
%     public, provided that they do not dance on tight ropes.
% (7) No wise creatures dance on tight ropes, if liable to giddiness.
% (8) A pig looks ridiculous, carrying an umbrella.
% (9) All, who do not dance on tight ropes, and who are treated
%     with respect are fat.
%     Show that no wise young pigs go up in balloons.
%							-Lewis Carroll, Symbolic Logic, p. 378

% representation:
%
                  

% problem in clause form.

Dances_on_tightropes(x) | Eats_pennybuns(x) | Old(x).
-Pig(x)|-Liable_to_giddiness(x) | Treated_with_respect(x).
-Wise(x) | -Balloonist(x) | Has_umbrella(x).
-Looks_ridiculous(x) | -Eats_pennybuns(x) | -Eats_lunch_in_public(x).
-Balloonist(x) | -Young(x) | Liable_to_giddiness(x).
-Fat(x) | -Looks_ridiculous(x) | Dances_on_tightropes(x) |
Eats_lunch_in_public(x).
-Liable_to_giddiness(x) | -Wise(x) | -Dances_on_tightropes(x).
-Pig(x) | -Has_umbrella(x) | Looks_ridiculous(x).
Dances_on_tightropes(x) | -Treated_with_respect(x) | Fat(x).

% Everyone is young or old.

Young(x) | Old(x).
-Young(x) | -Old(x).
Wise(PIGGY).
Young(PIGGY).
Pig(PIGGY).
Balloonist(PIGGY).