% RA: empresa.in
% Encuentros en la empresa
% Departamento de Ciencias de la Computación e Inteligencia Artificial
% Universidad de Sevilla
%==============================================================================


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

% Formalizar en OTTER la siguiente argumentación y comprobar su validez:
% "Todos los días los empleados de una empresa se encuentran en la cafetería,
% en la sala de descanso o en el aparcamiento. Todos los que han coincidido con
% Andrés en la cafetería se han encontrado con alguien en la sala de descanso.
% Nadie ha coincidido con Juan en la sala de descanso. Juan se ha encontrado
% en el parking con todos los que han coincidido con Daniel en la cafetería.
% Por tanto Juan se ha encontrado en el parking con Daniel."

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

% Configuración del sistema

set(auto2).

% Lenguaje del problema

% Constantes:

% Relaciones:

formula_list(sos).
  all x y (cafeteria(x,y) | descanso(x,y) | parking(x,y)).
  all x (parking(x,Andres) -> (exists y (descanso(x,y)))).
  all x (-descanso(x,Juan)).
  all x (cafeteria(x,Daniel) -> parking(x,Andres)).
  - parking(Juan,Daniel).

  all x y (cafeteria(x,y) -> cafeteria(y,x)).
  all x y (descanso(x,y) -> descanso(y,x)).
  all x y (parking(x,y) -> parking(y,x)).
end_of_list.

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