/* 

  Mislabeled boxes problem in Picat.

  This is a classic theorem proving problem.

  From http://www.ub-net.de/cms/proverbox-ex-boxes.html
  """
  File     : THIS SPECIFICATION IS A VARIANT OF THE FOLLOWING TPTP PROBLEM:
             PUZ012-1 : TPTP v2.5.0. Bugfixed v1.2.1.
  Domain   : Puzzles
  Problem  : The Mislabeled Boxes
  Version  : Especial.
  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]
           : boxes.ver1.in [ANL]
  """

  Also see TPTP, Thousands of Problems for Theorem Provers)
  http://www.cs.miami.edu/~tptp/

  This Picat model was created by Hakan Kjellerstrand, hakank@gmail.com
  See also my Picat page: http://www.hakank.org/picat/

*/

import cp.

main => go.


go ?=>
  N = 3,
  
  % boxes
  [A,B,C] = [1,2,3],

  % labels and the fruits
  [Apples,Oranges,Bananas] = [1,2,3],

  % The label on box a says "apples". 
  % The label on box b says "oranges". 
  % The label on box c says "bananas". 
  Labels = [apples,oranges,bananas],

  % What does the boxes contain?
  X = new_list(N),
  X :: 1..N,

  % constraints
  all_different(X),
    
  % No box contains what it says on its label. 
  % (i.e. fixpoint)
  foreach(I in 1..N)
    X[I] #!= I
  end,  

  % You pick up box b and it contains apples. 
  X[B] #= Apples,

  % What do the other two boxes contain?
  solve(X),
  println(x=X),
  println([Labels[X[I]] : I in 1..3]),

  fail,

  nl.


go => true.