----- MACE4 2003-B, Aug 2003 -----
Built with library LADR 2003-B, Oct 2003.
The process was started by mccune on gyro.thornwood,
Fri Oct 17 13:41:57 2003
The command was "mace4 -N6".  The process ID is 11085.

op(400,infix,^).
op(400,infix,v).
% From the command line: assign(iterate_up_to, 6).

clauses(sos).
x v (y v z) = y v (x v z).
x v (x ^ y) = x.
x ^ y = c(c(x) v c(y)).
c(c(x)) = x.
x v c(x) = y v c(y).
A v (B ^ (A v C)) != A v (C ^ (A v B)).
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.05 seconds --------

 A : 0

 B : 1

 C : 2

 c :
        0 1 2 3 4 5
    ---------------
        1 0 3 2 5 4

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

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

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

----- MAX_MODELS EXIT (1 model) -----
CPU time: 0.05 seconds.
The process finished Fri Oct 17 13:41:57 2003