----- MACE4 2005-A, 30 June 2005 -----
Built with library LADR July-2005, 30 June 2005.
The process was started by mccune on theorem.mcs.anl.gov,
Tue Jul  5 21:30:24 2005
The command was "../bin/mace4".  The process ID is 8594.

assign(domain_size,3).
set(print_models_portable).
set(verbose).

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

% Finished reading the input.

% There are no domain elements in the input.

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

Initial partial model:

 A : -

 B : -

 g :
        0 1 2
    ---------
        - - -
Sorry, no pretty printing yet for arity 3.
f(x,x,x) = 0.
f(x,x,y) = 0.
f(x,x,z) = 0.
f(x,y,x) = 0.
f(x,y,y) = -.
f(x,y,z) = -.
f(x,z,x) = 0.
f(x,z,y) = -.
f(x,z,z) = -.
f(y,x,x) = -.
f(y,x,y) = 1.
f(y,x,z) = -.
f(y,y,x) = 1.
f(y,y,y) = 1.
f(y,y,z) = 1.
f(y,z,x) = -.
f(y,z,y) = 1.
f(y,z,z) = -.
f(z,x,x) = -.
f(z,x,y) = -.
f(z,x,z) = 2.
f(z,y,x) = -.
f(z,y,y) = -.
f(z,y,z) = 2.
f(z,z,x) = 2.
f(z,z,y) = 2.
f(z,z,z) = 2.

-------- Model 1 at 0.01 seconds --------
interpretation( 3, [

        function(A, [0]),

        function(B, [2]),

        function(g(_), [1,0,1]),

        function(f(_,_,_), [0,0,0,
			  0,1,2,
			  0,0,0,
			  0,1,2,
			  1,1,1,
			  0,1,2,
			  2,2,2,
			  2,1,2,
			  2,2,2])
]).

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

--------- statistics for domain size 3 ---------

Current CPU time: 0.01 seconds (total CPU time: 0.01 seconds).
Ground clauses: seen=271, kept=269.
Selections=6, assignments=12, propagations=29, current_models=1.
Rewrite_terms=1349, rewrite_bools=289, indexes=169.
Rules_from_neg_clauses=2, cross_offs=8.

------------- memory usage (for entire run) -------------------

Total malloced: 20 megabytes
  type (bytes each)        gets      frees     in use      bytes
chunk ( 104)                103        103          0      0.0 K
string_buf (   8)           103        103          0      0.0 K
token (  20)                129        129          0      0.0 K
pterm (  16)                 88         88          0      0.0 K
ilist (   8)                 10         10          0      0.0 K
plist (   8)                657        538        119      0.9 K
mlist (  12)                 10         10          0      0.0 K
term (  16)                1893       1873         20      0.3 K
      term arg arrays:                                     0.2 K
literal (  12)                6          1          5      0.1 K
clause (  32)                 6          1          5      0.2 K
clist_pos (  20)              5          5          0      0.0 K
clist (  16)                  1          1          0      0.0 K
mclause (  20)              269        269          0      0.0 K (6.3 K high)
mstate (  16)                13         13          0      0.0 K
jnode (  28)                333        333          0      0.0 K
estack (3208)                17         17          0      0.0 K (avail=0, 0.0 K)

Memory report, 1 @ 20 = 20 megs (0.05 megs used).
List   2, length     270,      2.1 K
List   3, length       9,      0.1 K
List   4, length      34,      0.5 K
List   5, length      37,      0.7 K
List   6, length     547,     12.8 K
List   7, length    1293,     35.4 K
List   8, length       1,      0.0 K
List  26, length      19,      1.9 K

User_CPU=0.01, System_CPU=0.00, Wall_clock=0.

Exiting with 1 model.

Process 8594 exit (max_models) Tue Jul  5 21:30:24 2005
The process finished Tue Jul  5 21:30:24 2005