% problem-set/puzzles/miscell/houses.ver1.clauses
% created : 08/02/88
% revised : 08/11/88 

% description:
%
% This run solves "The Houses" puzzle using binary-resolution
% and UR-resolution, factoring, unit-deletion, and weighting. 
%
%                        The Houses   
%
%   There are 5 houses, 5 people, 5 colors, 5 drinks, 5 games,
%   and 4 pets. Each house has a person, a color, a drink, and
%   game, and all but one of the houses has a pet. The problem
%   is to match each house with as many properties as possible.
%   House 1 is at the left end and house 5 is at the right end.
%   The Englishman lives in the Red house. The White house is
%   left of the Green house. The Italian has a Guppy. Lemonade
%   is drunk in the Green house. The Swede lives in the house
%   where Coffee is drunk. The Toad lives in the house where
%   Backgammon is played. Racquetball is played in the Yellow
%   house. Milk is drunk in the third house. The Russian lives
%   in the first house. The Camel lives next to the house where
%   Quoits is played. The Rat lives next to the house where
%   Racquetball is played. Solitaire is played in the house
%   where Vodka is drunk. The American lives in the house
%   where Charades is played. The Russian lives next to the Blue
%   house.

% representation:
%
% Predicates: 
% samehouse, sameperson, samecolor, samedrink, samegame, and 
%     samepet predicates indicate that both arguments are
%     identical items.
% nextto(x,y) indicates that house x is immediately next to
%     house y, on either side.
% left(x,y) indicates that house x is to the immediate left 
%     of house y.
% hasperson, hascolor, hasdrink, hasgame, haspet predicates 
%     indicate that the house identified by the first argument
%     has the item indicated by the second argument.

% definition of samehouse

samehouse(x,x).
-samehouse(1,2).
-samehouse(1,3).
-samehouse(1,4).
-samehouse(1,5).
-samehouse(2,3).
-samehouse(2,4).
-samehouse(2,5).
-samehouse(3,4).
-samehouse(3,5).
-samehouse(4,5).

% definition of sameperson

sameperson(x,x).
-sameperson(Englishman,Italian).
-sameperson(Englishman,Swede).
-sameperson(Englishman,Russian).
-sameperson(Englishman,American).
-sameperson(Italian,Swede).
-sameperson(Italian,Russian).
-sameperson(Italian,American).
-sameperson(Swede,Russian).
-sameperson(Swede,American).
-sameperson(Russian,American).
 
 % definition of samecolor

samecolor(x,x).
-samecolor(Red,White).
-samecolor(Red,Green).
-samecolor(Red,Yellow).
-samecolor(Red,Blue).
-samecolor(White,Green).
-samecolor(White,Yellow).
-samecolor(White,Blue).
-samecolor(Green,Yellow).
-samecolor(Green,Blue).
-samecolor(Yellow,Blue).
 
 % definition of samedrink

samedrink(x,x).
-samedrink(Lemonade,Coffee).
-samedrink(Lemonade,Milk).
-samedrink(Lemonade,Vodka).
-samedrink(Lemonade,Unknowndrink).
-samedrink(Coffee,Milk).
-samedrink(Coffee,Vodka).
-samedrink(Coffee,Unknowndrink).
-samedrink(Milk,Vodka).
-samedrink(Milk,Unknowndrink).
-samedrink(Vodka,Unknowndrink).

% definition of samegame 

samegame(x,x).
-samegame(Backgammon,Racquetball).
-samegame(Backgammon,Quoits).
-samegame(Backgammon,Solitaire).
-samegame(Backgammon,Charades).
-samegame(Racquetball,Quoits).
-samegame(Racquetball,Solitaire).
-samegame(Racquetball,Charades).
-samegame(Quoits,Solitaire).
-samegame(Quoits,Charades).
-samegame(Solitaire,Charades).

% definition of samepet

samepet(x,x).
-samepet(Guppy,Toad).
-samepet(Guppy,Camel).
-samepet(Guppy,Rat).
-samepet(Guppy,No_pet).
-samepet(Toad,Camel).
-samepet(Toad,Rat).
-samepet(Toad,No_pet).
-samepet(Camel,Rat).
-samepet(Camel,No_pet).
-samepet(Rat,No_pet).

% Definition and properties of nextto and left

-nextto(x,y) | nextto(y,x).
-left(x,y) | -left(y,x).

-nextto(x,y) | left(x,y) | left(y,x).
-left(x,y) |  nextto(x,y).

-samehouse(x,y) | -nextto(x,y).

-left(x,x).
-nextto(x,x).

% Each house has a person and each person has a house:

hasperson(x,Englishman) | hasperson(x,Italian) |
hasperson(x,Swede) | hasperson(x,Russian) | hasperson(x,American). 

hasperson(1,y) | hasperson(2,y) | hasperson(3,y) |
hasperson(4,y) | hasperson(5,y).


% Each house has a color and each color has a house:

hascolor(x,Red) | hascolor(x,White) |
hascolor(x,Green) | hascolor(x,Yellow) | hascolor(x,Blue). 

hascolor(1,y) | hascolor(2,y) | hascolor(3,y) |
hascolor(4,y) | hascolor(5,y).


% Each house has a drink and each drink has a house:

hasdrink(x,Lemonade) | hasdrink(x,Coffee) |
hasdrink(x,Milk) | hasdrink(x,Vodka) | hasdrink(x,Unknowndrink). 

hasdrink(1,y) | hasdrink(2,y) | hasdrink(3,y) |
hasdrink(4,y) | hasdrink(5,y).


% Each house has a game and each game has a house:

hasgame(x,Backgammon) | hasgame(x,Racquetball) |
hasgame(x,Quoits) | hasgame(x,Solitaire) | hasgame(x,Charades). 

hasgame(1,y) | hasgame(2,y) | hasgame(3,y) |
hasgame(4,y) | hasgame(5,y).


% Each house has a pet and each pet has a house:

haspet(x,Guppy) | haspet(x,Toad) |
haspet(x,Camel) | haspet(x,Rat) | haspet(x,No_pet). 

haspet(1,y) | haspet(2,y) | haspet(3,y) |
haspet(4,y) | haspet(5,y).


% Unique items to each house:

samehouse(x1,x2) | -hascolor(x1,y) | -hascolor(x2,y).
samehouse(x1,x2) | -hasperson(x1,y) | -hasperson(x2,y).
samehouse(x1,x2) | -hasdrink(x1,y) | -hasdrink(x2,y).
samehouse(x1,x2) | -hasgame(x1,y) | -hasgame(x2,y).
samehouse(x1,x2) | -haspet(x1,y) | -haspet(x2,y).

sameperson(x1,x2) | -hasperson(y,x1) | -hasperson(y,x2).
samecolor(x1,x2) | -hascolor(y,x1) | -hascolor(y,x2).
samedrink(x1,x2) | -hasdrink(y,x1) | -hasdrink(y,x2).
samegame(x1,x2) | -hasgame(y,x1) | -hasgame(y,x2).
samepet(x1,x2) | -haspet(y,x1) | -haspet(y,x2).

% The Englishman lives in the Red house

-hasperson(x,Englishman) | hascolor(x,Red).
hasperson(x,Englishman) | -hascolor(x,Red).

% The White house is left of the Green house.

-hascolor(x,White) | -hascolor(y,Green) | left(x,y).
-hascolor(x,White) | hascolor(y,Green) | -left(x,y).
hascolor(x,White) | -hascolor(y,Green) | -left(x,y).

% The Italian has a Guppy.

-hasperson(x,Italian) | haspet(x,Guppy).
hasperson(x,Italian) | -haspet(x,Guppy).

% Lemonade is drunk is the Green house.

-hasdrink(x,Lemonade) | hascolor(x,Green).
hasdrink(x,Lemonade) | -hascolor(x,Green).

% The Swede lives in the house where Coffee is drunk.

-hasperson(x,Swede) | hasdrink(x,Coffee).
hasperson(x,Swede) | -hasdrink(x,Coffee).

% The Toad lives in the house where Backgammon is played.

-haspet(x,Toad) | hasgame(x,Backgammon).
haspet(x,Toad) | -hasgame(x,Backgammon).

% Racquetball is played in the Yellow house.

-hasgame(x,Racquetball) | hascolor(x,Yellow).
hasgame(x,Racquetball) | -hascolor(x,Yellow).

% The Camel lives next to the house where Quoits is played.

-haspet(x,Camel) | samehouse(y,z) | -nextto(x,y) | -nextto(x,z) |
hasgame(y,Quoits) | hasgame(z,Quoits).
-haspet(x,Camel) | -samehouse(1,x) | -nextto(x,y) | hasgame(y,Quoits).
-haspet(x,Camel) | -samehouse(x,5) | -nextto(x,y) | hasgame(y,Quoits).

-haspet(x,Camel) | nextto(x,y) | -hasgame(y,Quoits).

samehouse(y,z) | -nextto(x,y) | -nextto(x,z) | -hasgame(x,Quoits) |
haspet(y,Camel) | haspet(z,Camel).
-samehouse(1,x) | -nextto(x,y) | -hasgame(x,Quoits) | haspet(y,Camel).
-samehouse(x,5) | -nextto(x,y) | -hasgame(x,Quoits) | haspet(y,Camel).

% The Rat lives next to the house where Racquetball is played.

-haspet(x,Rat) | samehouse(y,z)  | -nextto(x,y) | -nextto(x,z) |
hasgame(y,Racquetball) | hasgame(z,Racquetball).
-haspet(x,Rat) | -nextto(x,y) | -samehouse(1,x) |
hasgame(y,Racquetball).
-haspet(x,Rat) | -nextto(x,y) | -samehouse(x,5) |
hasgame(y,Racquetball).

-haspet(x,Rat) | nextto(x,y) | -hasgame(y,Racquetball).

samehouse(y,z) | -nextto(x,y) | -nextto(x,z) |
-hasgame(x,Racquetball) | haspet(y,Rat) | haspet(z,Rat).
-nextto(x,y) | -samehouse(1,x) | -hasgame(x,Racquetball) |
haspet(y,Rat).
-nextto(x,y) | -samehouse(x,5) | -hasgame(x,Racquetball) |
haspet(y,Rat).

% Solitaire is played in the house where Vodka is drunk.

-hasgame(x,Solitaire) | hasdrink(x,Vodka).
hasgame(x,Solitaire) | -hasdrink(x,Vodka).

% The American lives in the house where Charades is played.

-hasperson(x,American) | hasgame(x,Charades).
hasperson(x,American) | -hasgame(x,Charades).

% The Russian lives next to the Blue house.

-hasperson(x,Russian) | samehouse(y,z) | -nextto(x,y)  | -nextto(x,z)
| hascolor(y,Blue) | hascolor(z,Blue).
-hasperson(x,Russian) | -samehouse(1,x) | -nextto(x,y) |
hascolor(y,Blue).
-hasperson(x,Russian) | -samehouse(x,5) | -nextto(x,y) |
hascolor(y,Blue).

-hasperson(x,Russian) | nextto(x,y) | -hascolor(y,Blue).

samehouse(y,z) | -nextto(x,y) | -nextto(x,z) | -hascolor(x,Blue) |
hasperson(y,Russian)| hasperson(z,Russian).
-nextto(x,y) | -hascolor(x,Blue) | -samehouse(1,x) |
hasperson(y,Russian).
-nextto(x,y) | -hascolor(x,Blue) | -samehouse(x,5) |
hasperson(y,Russian).

% denial: 

-hasperson(2,x1) | -hasperson(3,x2) | -hasperson(4,x3) |
-hasperson(5,x4) | 
-hascolor(1,x5) | -hascolor(2,x6) | -hascolor(3,x7) | -hascolor(4,x8) | 
-hascolor(5,x9) | -hasdrink(1,x10) | -hasdrink(2,x11) |
-hasdrink(4,x12) | 
-hasdrink(5,x13) | -hasgame(1,x14) | -hasgame(2,x15) | -hasgame(3,x16) |
-hasgame(4,x17) | -hasgame(5,x18) | -haspet(1,x19) | -haspet(2,x20) | 
-haspet(3,x21) | -haspet(4,x22) | -haspet(5,x23) | SOLVED(PROBLEM,x)
| $ANSWER(
hasperson(2,x1),hasperson(3,x2),hasperson(4,x3),hasperson(5,x4),
hascolor(1,x5),hascolor(2,x6),hascolor(3,x7),hascolor(4,x8),
hascolor(5,x9),hasdrink(1,x10),hasdrink(2,x11),hasdrink(4,x12),
hasdrink(5,x13),hasgame(1,x14),hasgame(2,x15),hasgame(3,x16),
hasgame(4,x17),hasgame(5,x18),haspet(1,x19),haspet(2,x20),
haspet(3,x21),haspet(4,x22),haspet(5,x23)).

-SOLVED(x,HOUSES).

-left(x,1).
-left(5,x).
left(1,2).
left(2,3).
left(3,4).
left(4,5).
-nextto(1,3).
-nextto(1,4).
-nextto(1,5).
-nextto(2,4).
-nextto(2,5).
-nextto(3,5).

% Milk is drunk in the 3rd house.

hasdrink(3,Milk).

% The Russian lives in the 1st house.

hasperson(1,Russian).