% English  : 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?

% Refs     : [WO+92] Wos et al. (1992), Automated Reasoning: Introduction a
%          : [Wos88] Wos (1988), Automated Reasoning - 33 Basic Research Pr
% Source   : [ANL]
% Names    : Boxes-of-fruit [WO+92]
%          : Boxes-of-fruit [Wos88]
set(prolog_style_variables).
set(auto).
clear(print_given).

list(usable).

% reflexivity_for_fruits, axiom.
 equal_fruits(X,X).

% reflexivity_for_boxes, axiom.
 equal_boxes(X,X).

% label_is_wrong, axiom.
-label(X,Y) |
-contains(X,Y).

% each_thing_is_in_a_box, axiom.
 contains(boxa,X) |
 contains(boxb,X) |
 contains(boxc,X).

% each_box_contains_something, axiom.
 contains(X,apples) |
 contains(X,bananas) |
 contains(X,oranges).

% contains_is_well_defined1, axiom.
-contains(X,Y) |
-contains(X,Z) |
 equal_fruits(Y,Z).

% contains_is_well_defined2, axiom.
-contains(X,Y) |
-contains(Z,Y) |
 equal_boxes(X,Z).

% boxa_not_boxb, axiom.
-equal_boxes(boxa,boxb).

% boxb_not_boxc, axiom.
-equal_boxes(boxb,boxc).

% boxa_not_boxc, axiom.
-equal_boxes(boxa,boxc).

% apples_not_bananas, axiom.
-equal_fruits(apples,bananas).

% bananas_not_oranges, axiom.
-equal_fruits(bananas,oranges).

% apples_not_oranges, axiom.
-equal_fruits(apples,oranges).

% boxa_labelled_apples, hypothesis.
 label(boxa,apples).

% boxb_labelled_oranges, hypothesis.
 label(boxb,oranges).

% boxc_labelled_bananas, hypothesis.
 label(boxc,bananas).

% boxb_contains_apples, hypothesis.
 contains(boxb,apples).

% prove_boxa_contains_bananas_and_boxc_oranges, negated_conjecture.
%-contains(boxa,bananas) |
%-contains(boxc,oranges).
-contains(boxa,X) | -contains(boxc,Y) | $ans(boxA(X),boxC(Y)).
end_of_list.

%------------------------------------------------------------------------------
