----- MACE 2.2, August 2003 -----
The process was started by mccune on gyro.thornwood,
Tue Aug 19 14:47:19 2003
The command was "../../bin/mace2 -n11 -x -m1000".

list(usable).
1 [] f(x,x)=x.
2 [] f(f(f(x,y),x),x)=y.
3 [] f(x,f(f(y,x),x))=y.
4 [] f(f(x,f(y,x)),x)=y.
end_of_list.

list(mace_constraints).
0 [] property(f(_,_),quasigroup).
end_of_list.

list(flattened_and_parted_clauses).
1 [] f(x,x)=x.
2 [] f(x,y)!=z|f(z,x)!=u|f(u,x)=y.
3 [] f(x,y)!=z|f(z,y)!=u|f(y,u)=x.
4 [] f(x,y)!=z|f(y,z)!=u|f(u,y)=x.
end_of_list.

--- Starting search for models of size 11 ---

Adding basic QG constraints on last column of f.
function f quasigroup.

64428 clauses were generated; 40098 of those survived the first stage
of unit preprocessing; there are 1452 atoms.

After all unit preprocessing, 824 atoms are still unassigned;
28488 clauses remain; 312 of those are non-Horn (selectable);
4924 K allocated; cpu time so far for this domain size: 0.04 sec.

The 1st model has been found.

The search is complete.  The set is satisfiable (5 model(s) found).


----- statistics for domain size 11 ----
Input:
    Clauses input                 40098
    Literal occurrences input    103170
    Greatest atom                  1452
Unit preprocess:
    Preprocess unit assignments     628
    Clauses after subsumption     28488
    Literal occ. after subsump.   76077
    Selectable clauses              312
Decide:
    Splits                          112
    Unit assignments              18310
    Failed paths                    108
Memory:
    Memory malloced                42 K
    Memory MACE_tp_alloced       4882 K
Time (seconds):
    Generate ground clauses        0.03
    DPLL                           0.08

=======================================
Total times for run (seconds):
    user CPU time                  0.11   (0 hr, 0 min, 0 sec)
    system CPU time                0.00   (0 hr, 0 min, 0 sec)
    wall-clock time                1      (0 hr, 0 min, 1 sec)

The search is complete.  The set is satisfiable (5 model(s) found).

The job finished Tue Aug 19 14:47:20 2003