----- MACE4 2003-B, Aug 2003 -----
Built with library LADR 2003-B, Aug 2003.
The process was started by mccune on theorem.mcs.anl.gov,
Thu Sep 11 09:15:40 2003
The command was "mace4 -N10".  The process ID is 28257.

% From the command line: assign(iterate_up_to, 10).

clauses(theory).
f(f(f(x,f(x,x)),y),f(z,f(f(u,y),f(y,x)))) = y.
f(f(x,x),f(x,x)) = x.
f(A,B) != f(B,A).
end_of_list.

% There are no domain elements in the input.

====== 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. ======

-------- Model 1 at 0.25 seconds --------

 A : 0

 B : 1

 f :
      | 0 1 2 3 4 5
    --+------------
    0 | 2 2 4 4 2 4
    1 | 3 3 4 4 3 4
    2 | 4 4 0 0 0 4
    3 | 4 4 1 1 1 4
    4 | 2 3 0 1 5 4
    5 | 4 4 4 4 4 4

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

----- MAX_MODELS EXIT (1 model) -----
CPU time: 0.25 seconds.
The process finished Thu Sep 11 09:15:41 2003