----- 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:20 2005
The command was "../bin/mace4".  The process ID is 8584.

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

clauses(theory).
- P(e(x,y)) | - P(x) | P(y).
P(e(e(x,y),e(e(y,z),e(z,x)))).
- P(e(a,a)).
end_of_list.

% Finished reading the input.

% There are no domain elements in the input.

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

Initial partial model:

 a : -

 e :
      | 0 1 2 3
    --+--------
    0 | - - - -
    1 | - - - -
    2 | - - - -
    3 | - - - -

 P :
        0 1 2 3
    -----------
        - - - -

-------- Model 1 at 0.01 seconds --------

 a : 0

 e :
      | 0 1 2 3
    --+--------
    0 | 1 2 0 3
    1 | 0 3 1 2
    2 | 3 0 2 1
    3 | 2 1 3 0

 P :
        0 1 2 3
    -----------
        0 0 1 0

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

--------- statistics for domain size 4 ---------

Current CPU time: 0.01 seconds (total CPU time: 0.01 seconds).
Ground clauses: seen=81, kept=81.
Selections=170, assignments=649, propagations=182, current_models=1.
Rewrite_terms=7039, rewrite_bools=1426, indexes=1126.
Rules_from_neg_clauses=111, cross_offs=550.

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

Total malloced: 20 megabytes
  type (bytes each)        gets      frees     in use      bytes
chunk ( 104)                 55         55          0      0.0 K
string_buf (   8)            54         54          0      0.0 K
token (  20)                 94         94          0      0.0 K
pterm (  16)                 60         60          0      0.0 K
ilist (   8)                  6          6          0      0.0 K
plist (   8)                303        194        109      0.9 K
mlist (  12)                  6          6          0      0.0 K
term (  16)                 761        747         14      0.2 K
      term arg arrays:                                     0.1 K
literal (  12)                6          1          5      0.1 K
clause (  32)                 4          1          3      0.1 K
clist_pos (  20)              3          3          0      0.0 K
clist (  16)                  1          1          0      0.0 K
mclause (  20)               81         81          0      0.0 K (2.0 K high)
mstate (  16)               650        650          0      0.0 K
jnode (  28)               1894       1894          0      0.0 K
estack (3208)               649        649          0      0.0 K (avail=0, 0.0 K)

Memory report, 1 @ 20 = 20 megs (0.02 megs used).
List   2, length      83,      0.6 K
List   3, length       5,      0.1 K
List   4, length      29,      0.5 K
List   5, length     119,      2.3 K
List   6, length     436,     10.2 K
List   7, length      13,      0.4 K
List   8, length      16,      0.5 K
List  26, length      14,      1.4 K

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

Exiting with 1 model.

Process 8584 exit (max_models) Tue Jul  5 21:30:20 2005
The process finished Tue Jul  5 21:30:20 2005