% RA: Relación 02
% OTTER: tinajas.in
% Departamento de Ciencias de la Computación e Inteligencia Artificial
%==============================================================================


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

% Se dispone de tres tinajas, una de 8 litros de capacidad, otra de 5 y una
% tercera de 3. Ninguna de ellas tiene marcas de medición y la de 8 litros está
% llena de aceite. Averiguar cómo se puede lograr tener exactamente 4 litros de
% aceite en la tinaja de 8 litros de capacidad y otros 4 en la tinaja de 5
% litros.

% Utilizar OTTER para encontrar una solución al problema.

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

% Lenguaje del problema:
% tinajas(x,y,z): Se puede llegar a la situación en la que hay 'x' litros en la
% tinaja de 8l de capacidad, 'y' litros en la de 5l de capacidad y 'z' litros en
% la de 3l de capacidad.

make_evaluable(_+_, $SUM(_,_)).
make_evaluable(_-_, $DIFF(_,_)).
make_evaluable(_<=_, $LE(_,_)).
make_evaluable(_>_, $GT(_,_)).

formula_list(sos).

% Estado inicial:

 tinajas(8,0,0).

% Estado final:

 -tinajas(4,4,0).

% Operadores:

all x y z
  (tinajas(x,y,z) -> tinajas(x+y-min(x+y,5),min(x+y,5),z)).

all x y z
  (tinajas(x,y,z) -> tinajas(x+z-min(x+z,3),y,min(x+z,3))).

all x y z
  (tinajas(x,y,z) -> tinajas(min(x+y,8),x+y-min(x+y,8),z)).

all x y z
  (tinajas(x,y,z) -> tinajas(x,y+z-min(y+z,3),min(y+z,3))).

all x y z
  (tinajas(x,y,z) -> tinajas(x,min(y+z,5),y+z-min(y+z,5))).

all x y z
  (tinajas(x,y,z) -> tinajas(min(x+z,8),y,x+z-min(x+z,8))).

end_of_list.

list(demodulators).
 min(x,y) = $IF(x<=y,x,y).
end_of_list.

set(hyper_res).
