% THE MERCHANT CHALLENGE 
% (from *Automated Reasoning* by Wos et al.
%  McGraw Hill 1992, Chapter One)
% 
% coded, manipulated, tested
% by Selmer Bringsjord
% Intro to Logic Programming and AI
% Spring 1998
%
% Condensed:
% A merchant, wishing to sell you some fruit, places three
% covered boxes on a table.  The merchant tells you that each
% box is	mislabeled.  Box a is labeled APPLES, box b ORANGES,
% and  box c BANANAS.  The merchant loves to gamble and offers
% you the chance to win all of the fruit if you can figure out
% what is in each box.  You accept on the condition that you
% are allowed to look inside the box labeled ORANGES.  He
% agrees, and you look inside and find that this box contains
% APPLES.  You then turn to the merchant and announce
% correctly the contents of the other two boxes, and win the
% fruit?  What is you answer and how did you do it?

set(auto).
assign(max_seconds,60).

formula_list(usable).

% ====================
% Facts learned from direct visual observation:

Contains(b,apples).

Label(a,apples).
Label(b,oranges).
Label(c,bananas).
% ====================

% ====================
% Each box contains one of the three types of fruit:

Contains(a,apples) | Contains(a,bananas) |
Contains(a,oranges).

Contains(b,apples) | Contains(b,bananas) |
Contains(b,oranges).

Contains(c,apples) | Contains(c,bananas) |
Contains(c,oranges).
% ====================

% ====================
% If a box contains a type of fruit, no other
% box contains that type of fruit:

all x all y all z ((Contains(x,y) & z != x) ->
-Contains(z,y)).

% ====================

% ====================
% The boxes are distinct:
(a != b) & (b !=c) & (a != c).
% ====================

% ====================
% All the boxes are mislabeled:
all x all y (Label(x,y) -> -Contains(x,y)).
% ====================

% ====================
% Include the denial of that which is to be proved:

% Contains(c,apples).
% Contains(c,bananas).
% -Contains(c,oranges).
% Contains(a,apples).
% Contains(a,oranges).
% -Contains(a,bananas).

% -(exists x (Contains(x,bananas))).
 -(exists x (Contains(x,oranges))).
% ====================

end_of_list.