% Started on theorem.mcs.anl.gov at Thu Jul 29 12:00:16 CDT 2004.
% Here is the mace head file head.da10.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% set(print_models_portable).
% 
% assign(iterate_up_to, 10).
% 
% clauses(theory).
% 
% f(x,y) != f(x,z) | y = z.
% f(y,x) != f(z,x) | y = z.
% 
% f(0,x) = x.
% f(x,0) = x.
% f(g(x),x) = 0.
% f(x,g(x)) = 0.
% g(g(x)) = x.
% g(0) = 0.
% g(f(x,y)) = f(g(y),g(x)).
% f(x,f(g(x),y)) = y.
% f(g(x),f(x,y)) = y.
% 
% f(f(x,x),y) = f(x,f(x,y)).
% f(f(x,y),x) = f(x,f(y,x)).
% f(f(y,x),x) = f(y,f(x,x)).
% 
% f(f(A,B),C) != f(A,f(B,C)).
% 
% end_of_list.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% f(f(g(f(x,x)),y),g(f(g(f(x,f(x,z))),y))) = z.  % candidate 2

interpretation( 10, [

        function(A, [1]),

        function(B, [2]),

        function(C, [4]),

        function(g(_), [0,1,2,3,4,5,6,7,8,9]),

        function(f(_,_), [0,1,2,3,4,5,6,7,8,9,
			  1,0,3,2,5,4,8,9,6,7,
			  2,3,0,1,6,9,4,8,7,5,
			  3,2,1,0,7,8,9,4,5,6,
			  4,5,6,7,0,1,2,3,9,8,
			  5,4,9,8,1,0,7,6,3,2,
			  6,8,4,9,2,7,0,5,1,3,
			  7,9,8,4,3,6,5,0,2,1,
			  8,6,7,5,9,3,1,2,0,4,
			  9,7,5,6,8,2,3,1,4,0])
]).

% Checked 132, passed 50, new_interps 1.
% Finished Thu Jul 29 12:00:47 CDT 2004.