----- MACE4 2003-C, Nov 2003 -----
Built with library LADR 2003-C (working), Nov 2003.
The process was started by mccune on gyro.thornwood,
Wed Dec  3 14:37:49 2003
The command was "mace4".  The process ID is 25674.

set(print_models_portable).
assign(iterate_up_to,7).

clauses(theory).
d(d(d(x,x),d(d(y,z),u)),d(z,y)) = u.
d(x,x) = 0.
d(X,d(d(d(d(X,X),Y),Z),d(d(d(X,X),X),Z))) != Y.
end_of_list.

% The maximum domain element in the input is 0.

====== Starting search for domain size 2. ======

====== Starting search for domain size 3. ======

====== Starting search for domain size 4. ======

====== Starting search for domain size 5. ======

====== Starting search for domain size 6. ======

====== Starting search for domain size 7. ======

-------- Model 1 at 0.32 seconds --------
interpretation( 7, [

        function(X, [1]),

        function(Y, [2]),

        function(Z, [1]),

        function(d(_,_), [0,3,4,1,2,6,5,
			  1,0,5,3,6,4,2,
			  2,6,0,5,4,1,3,
			  3,1,6,0,5,2,4,
			  4,5,2,6,0,3,1,
			  5,2,3,4,1,0,6,
			  6,4,1,2,3,5,0])
]).

-------- end of model --------

----- MAX_MODELS EXIT (1 model) -----
CPU time: 0.32 seconds.
The process finished Wed Dec  3 14:37:49 2003