% RA: grupo.in
% Problema de grupos con paramodulación
% Departamento de Ciencias de la Computación e Inteligencia Artificial
% Universidad de Sevilla
%==============================================================================


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

set(para_into).
set(para_from).

op(400, xfy, *).
op(300, yf, ^).

list(usable).
 x = x.
 e * x = x.                     % Ax. 1
 x * e = x.                     % Ax. 2
 x^ * x = e.                    % Ax. 3
 x * x^ = e.                    % Ax. 4
 (x * y) * z = x * (y * z).     % Ax. 5
end_of_list.

list(sos).
 x * x = e.
 a * b != b * a.
end_of_list.

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