% RA: 03-fichas.in
% Puzle de fichas en línea
% Departamento de Ciencias de la Computación e Inteligencia Artificial
% Universidad de Sevilla
%==============================================================================


%==============================================================================
% Enunciado
%==============================================================================

%   Un puzle está compuesto por las siguientes cuatro fichas:

%   Utilizar Otter para encontrar todas las maneras posibles de colocar estas
% cuatro fichas en un cuadrado de dimensión 2x2, sin repetir, de forma que los 
% colores de los lados adyacentes coincidan. En este caso las fichas se pueden 
% girar.

%==============================================================================
% Formalización
%==============================================================================

% Lenguaje:
% ficha(x,y,z,u,v) - La ficha x tiene el color y a la izquierda, el color z 
%                    hacia abajo, el color u a la derecha y el color v hacia 
%                    arriba.
% posicion(x1,x2,x3,x4)
%   Las fichas x1, x2, x3, x4 son distintas y se pueden colocar en un cuadrado 
%   2x2 de forma que los colores de los lados adyacentes coinciden.

set(hyper_res).
set(para_into).
set(para_from).
assign(max_proofs,-1).

formula_list(sos).
 all x1 x2 x3 x4 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
  ((ficha(x1,y1,y2,y3,y4) & ficha(x2,y3,y5,y6,y7) &
    ficha(x3,y8,y9,y10,y2) & ficha(x4,y10,y11,y12,y5) &
    x1 != x2 & x1 != x3 & x1 != x4 & 
    x2 != x3 & x2 != x4 & x3 != x4) -> posicion(x1,x2,x3,x4)).

 ficha(1,rojo,verde,verde,blanco).
 ficha(2,verde,blanco,rojo,rojo).
 ficha(3,azul,blanco,verde,azul).
 ficha(4,rojo,rojo,azul,blanco).

% ficha(1,verde,rojo).
% ficha(2,rojo,verde).
% ficha(3,verde,azul).
% ficha(4,azul,rojo).

 all x y z v w (ficha(x,y,z,v,w) -> 
                (ficha(x,w,y,z,v) & ficha(x,v,w,y,z) & ficha(x,z,v,w,y)).

 1 != 2.
 1 != 3.
 1 != 4.
 2 != 3.
 2 != 4.
 3 != 4.

 1 = 1.
 2 = 2.
 3 = 3.
 4 = 4.
end_of_list.

formula_list(passive).
 all x1 x2 x3 x4
   (posicion(x1,x2,x3,x4) -> $ANS(x1,x2,x3,x4)).
end_of_list.

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