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

assign(domain_size,8).
set(verbose).

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

% Finished reading the input.

% There are no domain elements in the input.

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

Initial partial model:

 A : -

 B : -

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

-------- Model 1 at 0.00 seconds --------

 A : 0

 B : 1

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

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

--------- statistics for domain size 8 ---------

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=513, kept=513.
Selections=37, assignments=133, propagations=52, current_models=1.
Rewrite_terms=4087, rewrite_bools=660, indexes=670.
Rules_from_neg_clauses=16, cross_offs=268.

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

Total malloced: 20 megabytes
  type (bytes each)        gets      frees     in use      bytes
chunk ( 104)                 68         68          0      0.0 K
string_buf (   8)            59         59          0      0.0 K
token (  20)                107        107          0      0.0 K
pterm (  16)                 50         50          0      0.0 K
ilist (   8)                  8          8          0      0.0 K
plist (   8)               1132       1026        106      0.8 K
mlist (  12)                  8          8          0      0.0 K
term (  16)                3899       3885         14      0.2 K
      term arg arrays:                                     0.1 K
literal (  12)                3          1          2      0.0 K
clause (  32)                 3          1          2      0.1 K
clist_pos (  20)              2          2          0      0.0 K
clist (  16)                  1          1          0      0.0 K
mclause (  20)              513        513          0      0.0 K (12.0 K high)
mstate (  16)               134        134          0      0.0 K
jnode (  28)                634        634          0      0.0 K
estack (3208)               137        137          0      0.0 K (avail=0, 0.0 K)

Memory report, 1 @ 20 = 20 megs (0.11 megs used).
List   2, length     513,      4.0 K
List   3, length       7,      0.1 K
List   4, length      24,      0.4 K
List   5, length      34,      0.7 K
List   6, length    4228,     99.1 K
List   7, length      50,      1.4 K
List   8, length       1,      0.0 K
List  26, length      16,      1.6 K

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

Exiting with 1 model.

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