----- MACE4 2003-B, Aug 2003 -----
Built with library LADR 2003-B, Aug 2003.
The process was started by mccune on gyro.thornwood,
Wed Sep 10 15:13:13 2003
The command was "mace4 -N10".  The process ID is 12418.

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

clauses(theory).
f(f(f(x,y),y),f(f(f(z,y),f(x,y)),f(f(x,x),z))) = y.
end_of_list.

formulas(theory).
(all x all y exists z (f(x,z) = y)).
(all x all y exists z (f(z,x) = y)).
end_of_list.

% The preceding list of formulas produces the following list of clauses.

clauses(clausified_formulas).
f(x,$f1(x,y)) = y.
f($f2(x,y),x) = y.
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. ======

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

-------- Model 1 at 0.88 seconds --------

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

 $f1 :
      | 0 1 2 3 4 5 6
    --+--------------
    0 | 0 2 1 4 3 6 5
    1 | 6 4 5 3 1 2 0
    2 | 5 6 3 2 4 0 1
    3 | 1 0 4 6 2 5 3
    4 | 2 3 0 1 5 4 6
    5 | 3 5 2 0 6 1 4
    6 | 4 1 6 5 0 3 2

 $f2 :
      | 0 1 2 3 4 5 6
    --+--------------
    0 | 0 3 4 5 6 2 1
    1 | 3 6 0 4 1 5 2
    2 | 4 0 5 2 3 1 6
    3 | 5 4 2 1 0 6 3
    4 | 6 1 3 0 2 4 5
    5 | 2 5 1 6 4 3 0
    6 | 1 2 6 3 5 0 4

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

----- MAX_MODELS EXIT (1 model) -----
CPU time: 0.88 seconds.
The process finished Wed Sep 10 15:13:14 2003