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

assign(domain_size,5).
assign(max_models,- 1).
clear(print_models).
set(verbose).

clauses(theory).
x * (x \ y) = y.
x \ (x * y) = y.
(x / y) * y = x.
(x * y) / y = x.
end_of_list.

% Finished reading the input.

% There are no domain elements in the input.

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

Initial partial model:

 * :
      | 0 1 2 3 4
    --+----------
    0 | - - - - -
    1 | - - - - -
    2 | - - - - -
    3 | - - - - -
    4 | - - - - -

 / :
      | 0 1 2 3 4
    --+----------
    0 | - - - - -
    1 | - - - - -
    2 | - - - - -
    3 | - - - - -
    4 | - - - - -

 \ :
      | 0 1 2 3 4
    --+----------
    0 | - - - - -
    1 | - - - - -
    2 | - - - - -
    3 | - - - - -
    4 | - - - - -

Model 1 has been found.

Model 10 has been found.

Model 100 has been found.

Model 1000 has been found.

Model 10000 has been found.

--------- statistics for domain size 5 ---------

Current CPU time: 0.81 seconds (total CPU time: 0.81 seconds).
Ground clauses: seen=100, kept=100.
Selections=10691, assignments=53390, propagations=319455, current_models=10944.
Rewrite_terms=946380, rewrite_bools=468844, indexes=199567.
Rules_from_neg_clauses=119888, cross_offs=246763.

------------- 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)            67         67          0      0.0 K
token (  20)                109        109          0      0.0 K
pterm (  16)                 53         53          0      0.0 K
ilist (   8)                  8          8          0      0.0 K
plist (   8)                314        200        114      0.9 K
mlist (  12)                  8          8          0      0.0 K
term (  16)                 580        568         12      0.2 K
      term arg arrays:                                     0.1 K
literal (  12)                5          1          4      0.0 K
clause (  32)                 5          1          4      0.1 K
clist_pos (  20)              4          4          0      0.0 K
clist (  16)                  1          1          0      0.0 K
mclause (  20)              100        100          0      0.0 K (2.3 K high)
mstate (  16)             53391      53391          0      0.0 K
jnode (  28)             619708     619708          0      0.0 K
estack (3208)             53391      53391          0      0.0 K (avail=0, 0.0 K)

Memory report, 1 @ 20 = 20 megs (0.02 megs used).
List   2, length     100,      0.8 K
List   3, length       7,      0.1 K
List   4, length      16,      0.2 K
List   5, length      13,      0.3 K
List   6, length     500,     11.7 K
List   7, length      35,      1.0 K
List   8, length       1,      0.0 K
List  26, length       9,      0.9 K

User_CPU=0.81, System_CPU=0.00, Wall_clock=1.

Exiting with 10944 models.

Process 8590 exit (all_models) Tue Jul  5 21:30:22 2005
The process finished Tue Jul  5 21:30:22 2005