Description
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?
ProverBox Specification (download file)
CONST BOX, FRUIT : TYPE
boxA, boxB, boxC : BOX
apples, bananas, oranges : FRUIT
equalB : PRED [BOX, BOX]
equalF : PRED [FRUIT, FRUIT]
label, contains : PRED [BOX, FRUIT]
VAR B, B1, B2 : BOX
F, F1, F2 : FRUIT
AXIOM reflexivity : equalB(B, B) /\ equalF(F, F)
AXIOM equality : ~equalB(boxA, boxB) /\ ~equalB(boxA, boxC) /\
~equalB(boxB, boxC) /\ ~equalF(apples, bananas) /\
~equalF(apples, oranges) /\ ~equalF(bananas, oranges)
AXIOM labelIncorrect : label(B, F) => ~contains(B, F)
AXIOM fruitInBox : contains(boxA, F) \/ contains(boxB, F) \/
contains(boxC, F)
AXIOM boxHasFruit : contains(B, apples) \/ contains(B, bananas) \/
contains(B, oranges)
AXIOM wellDefined1 : contains(B, F1) /\ contains(B, F2) => equalF(F1, F2)
AXIOM wellDefined2 : contains(B1, F) /\ contains(B2, F) => equalB(B1, B2)
AXIOM givenLabels : label(boxA, apples) /\ label(boxB, oranges) /\
label(boxC, bananas)
AXIOM known : contains(boxB, apples)
THEOREM solution : exists InA, InC : FRUIT.
contains(boxA, InA) /\ contains(boxC, InC)