% problem-set/puzzles/miscell/boxes.ver1.in
% created : 07/09/86
% revised : 07/05/88
       
% description:
%
% This run solves a puzzle called "The Mislabeled Boxes" using
% UR-resolution.
%
%            The Mislabeled Boxes
%       
%   There are three boxes a, b, and c on a table.
%   Each box contains apples or bananas or oranges.
%   No two boxes contain the same thing.
%   Each box has a label that says it contains apples
%   or says it contains bananas or says it contains
%   oranges.
%   No box contains what it says on its label.
%   The label on box a says "apples".
%   The label on box b says "oranges".
%   The label on box c says "bananas".
%   You pick up box b and it contains apples.
%   What do the other two boxes contain?

% representation:
%
% declare_predicates(2,[EQB,EQF,LABEL,CONTAINS]).
% declare_variables([x,y,z]).
% declare_constants([boxa,boxb,boxc,ap,or,ban]).
%
% Declarative version
% PREDICATES:
%    EQB = Same boxe; EQF = Same fruit.             
%    LABEL(x,y) = The label on box 'x' is 'y'.      
%    CONTAINS(x,y) = The contents of box 'x' is 'y'.
%    boxa,boxb,boxc = The different box #s a,b,c.   
%    ap = apples; or = oranges; ban = bananas.      

set(UR_res).


list(axioms).

% Equality axioms .

EQF(x,x).
EQB(x,x).

% The boxes are mislabelled .

-LABEL(x,y) | -CONTAINS(x,y).

% Each box has at least one fruit, and each fruit is in at least one box

CONTAINS(boxa,x) | CONTAINS(boxb,x) | CONTAINS(boxc,x).
CONTAINS(x,ap) | CONTAINS(x,ban) | CONTAINS(x,or).

% A box has at most one fruit, and a fruit is in at most one box.

-CONTAINS(x,y) | -CONTAINS(x,z) | EQF(y,z).
-CONTAINS(x,y) | -CONTAINS(z,y) | EQB(x,z).

% The boxes are unique .

-EQB(boxa,boxb).
-EQB(boxb,boxc).
-EQB(boxa,boxc).

% The fruits are unique .

-EQF(ap,ban).
-EQF(ban,or).
-EQF(ap,or).

end_of_list.


list(sos).

% Given clauses .

LABEL(boxa,ap).
LABEL(boxb,or).
LABEL(boxc,ban).

CONTAINS(boxb,ap).

end_of_list.
