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)