============================== Mace4 =================================
Mace4 (32) version 2009-02A, February 2009.
Process 11174 was started by mccune on cleo,
Wed Feb 25 09:31:58 2009
The command was "/home/mccune/bin/mace4 -f ncg-48.in".
============================== end of head ===========================

============================== INPUT =================================

% Reading from file ncg-48.in

assign(domain_size,48).
    % assign(domain_size, 48) -> assign(start_size, 48).
    % assign(domain_size, 48) -> assign(end_size, 48).
clear(negprop).

formulas(assumptions).
e * x = x.
x' * x = e.
(x * y) * z = x * (y * z).
A * B != B * A.
end_of_list.

============================== end of input ==========================

============================== PROCESS NON-CLAUSAL FORMULAS ==========

% Formulas that are not ordinary clauses:

============================== end of process non-clausal formulas ===

============================== CLAUSES FOR SEARCH ====================

formulas(mace4_clauses).
e * x = x.
x' * x = e.
(x * y) * z = x * (y * z).
A * B != B * A.
end_of_list.

============================== end of clauses for search =============

% There are no natural numbers in the input.

============================== DOMAIN SIZE 48 ========================

============================== MODEL =================================

interpretation( 48, [number=1, seconds=0], [

        function(A, [ 0 ]),

        function(B, [ 1 ]),

        function(e, [ 2 ]),

        function('(_), [ 0, 1, 2, 4, 3, 5, 6, 7, 8,10, 9,11,12,13,14,16,15,17,18,19,20,22,21,23,24,25,26,28,27,29,30,31,32,34,33,35,36,37,38,40,39,41,42,43,44,46,45,47 ]),

        function(*(_,_), [
			   2, 3, 0, 1, 5, 4, 7, 6, 9, 8,11,10,13,12,15,14,17,16,19,18,21,20,23,22,25,24,27,26,29,28,31,30,33,32,35,34,37,36,39,38,41,40,43,42,45,44,47,46,
			   4, 2, 1, 5, 0, 3, 8,10, 6,11, 7, 9,14,16,12,17,13,15,20,22,18,23,19,21,26,28,24,29,25,27,32,34,30,35,31,33,38,40,36,41,37,39,44,46,42,47,43,45,
			   0, 1, 2, 3, 4, 5, 6, 7, 8, 9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,
			   5, 0, 3, 4, 2, 1, 9,11, 7,10, 6, 8,15,17,13,16,12,14,21,23,19,22,18,20,27,29,25,28,24,26,33,35,31,34,30,32,39,41,37,40,36,38,45,47,43,46,42,44,
			   1, 5, 4, 2, 3, 0,10, 8,11, 6, 9, 7,16,14,17,12,15,13,22,20,23,18,21,19,28,26,29,24,27,25,34,32,35,30,33,31,40,38,41,36,39,37,46,44,47,42,45,43,
			   3, 4, 5, 0, 1, 2,11, 9,10, 7, 8, 6,17,15,16,13,14,12,23,21,22,19,20,18,29,27,28,25,26,24,35,33,34,31,32,30,41,39,40,37,38,36,47,45,46,43,44,42,
			   7, 8, 6, 9,10,11, 2, 0, 1, 3, 4, 5,18,19,20,21,22,23,12,13,14,15,16,17,30,31,32,33,34,35,24,25,26,27,28,29,42,43,44,45,46,47,36,37,38,39,40,41,
			   6, 9, 7, 8,11,10, 0, 2, 3, 1, 5, 4,19,18,21,20,23,22,13,12,15,14,17,16,31,30,33,32,35,34,25,24,27,26,29,28,43,42,45,44,47,46,37,36,39,38,41,40,
			  10, 6, 8,11, 7, 9, 1, 4, 2, 5, 0, 3,20,22,18,23,19,21,14,16,12,17,13,15,32,34,30,35,31,33,26,28,24,29,25,27,44,46,42,47,43,45,38,40,36,41,37,39,
			  11, 7, 9,10, 6, 8, 3, 5, 0, 4, 2, 1,21,23,19,22,18,20,15,17,13,16,12,14,33,35,31,34,30,32,27,29,25,28,24,26,45,47,43,46,42,44,39,41,37,40,36,38,
			   8,11,10, 6, 9, 7, 4, 1, 5, 2, 3, 0,22,20,23,18,21,19,16,14,17,12,15,13,34,32,35,30,33,31,28,26,29,24,27,25,46,44,47,42,45,43,40,38,41,36,39,37,
			   9,10,11, 7, 8, 6, 5, 3, 4, 0, 1, 2,23,21,22,19,20,18,17,15,16,13,14,12,35,33,34,31,32,30,29,27,28,25,26,24,47,45,46,43,44,42,41,39,40,37,38,36,
			  13,14,12,15,16,17,18,19,20,21,22,23, 2, 0, 1, 3, 4, 5, 6, 7, 8, 9,10,11,36,37,38,39,40,41,42,43,44,45,46,47,24,25,26,27,28,29,30,31,32,33,34,35,
			  12,15,13,14,17,16,19,18,21,20,23,22, 0, 2, 3, 1, 5, 4, 7, 6, 9, 8,11,10,37,36,39,38,41,40,43,42,45,44,47,46,25,24,27,26,29,28,31,30,33,32,35,34,
			  16,12,14,17,13,15,20,22,18,23,19,21, 1, 4, 2, 5, 0, 3, 8,10, 6,11, 7, 9,38,40,36,41,37,39,44,46,42,47,43,45,26,28,24,29,25,27,32,34,30,35,31,33,
			  17,13,15,16,12,14,21,23,19,22,18,20, 3, 5, 0, 4, 2, 1, 9,11, 7,10, 6, 8,39,41,37,40,36,38,45,47,43,46,42,44,27,29,25,28,24,26,33,35,31,34,30,32,
			  14,17,16,12,15,13,22,20,23,18,21,19, 4, 1, 5, 2, 3, 0,10, 8,11, 6, 9, 7,40,38,41,36,39,37,46,44,47,42,45,43,28,26,29,24,27,25,34,32,35,30,33,31,
			  15,16,17,13,14,12,23,21,22,19,20,18, 5, 3, 4, 0, 1, 2,11, 9,10, 7, 8, 6,41,39,40,37,38,36,47,45,46,43,44,42,29,27,28,25,26,24,35,33,34,31,32,30,
			  19,20,18,21,22,23,12,13,14,15,16,17, 6, 7, 8, 9,10,11, 2, 0, 1, 3, 4, 5,42,43,44,45,46,47,36,37,38,39,40,41,30,31,32,33,34,35,24,25,26,27,28,29,
			  18,21,19,20,23,22,13,12,15,14,17,16, 7, 6, 9, 8,11,10, 0, 2, 3, 1, 5, 4,43,42,45,44,47,46,37,36,39,38,41,40,31,30,33,32,35,34,25,24,27,26,29,28,
			  22,18,20,23,19,21,14,16,12,17,13,15, 8,10, 6,11, 7, 9, 1, 4, 2, 5, 0, 3,44,46,42,47,43,45,38,40,36,41,37,39,32,34,30,35,31,33,26,28,24,29,25,27,
			  23,19,21,22,18,20,15,17,13,16,12,14, 9,11, 7,10, 6, 8, 3, 5, 0, 4, 2, 1,45,47,43,46,42,44,39,41,37,40,36,38,33,35,31,34,30,32,27,29,25,28,24,26,
			  20,23,22,18,21,19,16,14,17,12,15,13,10, 8,11, 6, 9, 7, 4, 1, 5, 2, 3, 0,46,44,47,42,45,43,40,38,41,36,39,37,34,32,35,30,33,31,28,26,29,24,27,25,
			  21,22,23,19,20,18,17,15,16,13,14,12,11, 9,10, 7, 8, 6, 5, 3, 4, 0, 1, 2,47,45,46,43,44,42,41,39,40,37,38,36,35,33,34,31,32,30,29,27,28,25,26,24,
			  25,26,24,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47, 2, 0, 1, 3, 4, 5, 6, 7, 8, 9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,
			  24,27,25,26,29,28,31,30,33,32,35,34,37,36,39,38,41,40,43,42,45,44,47,46, 0, 2, 3, 1, 5, 4, 7, 6, 9, 8,11,10,13,12,15,14,17,16,19,18,21,20,23,22,
			  28,24,26,29,25,27,32,34,30,35,31,33,38,40,36,41,37,39,44,46,42,47,43,45, 1, 4, 2, 5, 0, 3, 8,10, 6,11, 7, 9,14,16,12,17,13,15,20,22,18,23,19,21,
			  29,25,27,28,24,26,33,35,31,34,30,32,39,41,37,40,36,38,45,47,43,46,42,44, 3, 5, 0, 4, 2, 1, 9,11, 7,10, 6, 8,15,17,13,16,12,14,21,23,19,22,18,20,
			  26,29,28,24,27,25,34,32,35,30,33,31,40,38,41,36,39,37,46,44,47,42,45,43, 4, 1, 5, 2, 3, 0,10, 8,11, 6, 9, 7,16,14,17,12,15,13,22,20,23,18,21,19,
			  27,28,29,25,26,24,35,33,34,31,32,30,41,39,40,37,38,36,47,45,46,43,44,42, 5, 3, 4, 0, 1, 2,11, 9,10, 7, 8, 6,17,15,16,13,14,12,23,21,22,19,20,18,
			  31,32,30,33,34,35,24,25,26,27,28,29,42,43,44,45,46,47,36,37,38,39,40,41, 6, 7, 8, 9,10,11, 2, 0, 1, 3, 4, 5,18,19,20,21,22,23,12,13,14,15,16,17,
			  30,33,31,32,35,34,25,24,27,26,29,28,43,42,45,44,47,46,37,36,39,38,41,40, 7, 6, 9, 8,11,10, 0, 2, 3, 1, 5, 4,19,18,21,20,23,22,13,12,15,14,17,16,
			  34,30,32,35,31,33,26,28,24,29,25,27,44,46,42,47,43,45,38,40,36,41,37,39, 8,10, 6,11, 7, 9, 1, 4, 2, 5, 0, 3,20,22,18,23,19,21,14,16,12,17,13,15,
			  35,31,33,34,30,32,27,29,25,28,24,26,45,47,43,46,42,44,39,41,37,40,36,38, 9,11, 7,10, 6, 8, 3, 5, 0, 4, 2, 1,21,23,19,22,18,20,15,17,13,16,12,14,
			  32,35,34,30,33,31,28,26,29,24,27,25,46,44,47,42,45,43,40,38,41,36,39,37,10, 8,11, 6, 9, 7, 4, 1, 5, 2, 3, 0,22,20,23,18,21,19,16,14,17,12,15,13,
			  33,34,35,31,32,30,29,27,28,25,26,24,47,45,46,43,44,42,41,39,40,37,38,36,11, 9,10, 7, 8, 6, 5, 3, 4, 0, 1, 2,23,21,22,19,20,18,17,15,16,13,14,12,
			  37,38,36,39,40,41,42,43,44,45,46,47,24,25,26,27,28,29,30,31,32,33,34,35,12,13,14,15,16,17,18,19,20,21,22,23, 2, 0, 1, 3, 4, 5, 6, 7, 8, 9,10,11,
			  36,39,37,38,41,40,43,42,45,44,47,46,25,24,27,26,29,28,31,30,33,32,35,34,13,12,15,14,17,16,19,18,21,20,23,22, 0, 2, 3, 1, 5, 4, 7, 6, 9, 8,11,10,
			  40,36,38,41,37,39,44,46,42,47,43,45,26,28,24,29,25,27,32,34,30,35,31,33,14,16,12,17,13,15,20,22,18,23,19,21, 1, 4, 2, 5, 0, 3, 8,10, 6,11, 7, 9,
			  41,37,39,40,36,38,45,47,43,46,42,44,27,29,25,28,24,26,33,35,31,34,30,32,15,17,13,16,12,14,21,23,19,22,18,20, 3, 5, 0, 4, 2, 1, 9,11, 7,10, 6, 8,
			  38,41,40,36,39,37,46,44,47,42,45,43,28,26,29,24,27,25,34,32,35,30,33,31,16,14,17,12,15,13,22,20,23,18,21,19, 4, 1, 5, 2, 3, 0,10, 8,11, 6, 9, 7,
			  39,40,41,37,38,36,47,45,46,43,44,42,29,27,28,25,26,24,35,33,34,31,32,30,17,15,16,13,14,12,23,21,22,19,20,18, 5, 3, 4, 0, 1, 2,11, 9,10, 7, 8, 6,
			  43,44,42,45,46,47,36,37,38,39,40,41,30,31,32,33,34,35,24,25,26,27,28,29,18,19,20,21,22,23,12,13,14,15,16,17, 6, 7, 8, 9,10,11, 2, 0, 1, 3, 4, 5,
			  42,45,43,44,47,46,37,36,39,38,41,40,31,30,33,32,35,34,25,24,27,26,29,28,19,18,21,20,23,22,13,12,15,14,17,16, 7, 6, 9, 8,11,10, 0, 2, 3, 1, 5, 4,
			  46,42,44,47,43,45,38,40,36,41,37,39,32,34,30,35,31,33,26,28,24,29,25,27,20,22,18,23,19,21,14,16,12,17,13,15, 8,10, 6,11, 7, 9, 1, 4, 2, 5, 0, 3,
			  47,43,45,46,42,44,39,41,37,40,36,38,33,35,31,34,30,32,27,29,25,28,24,26,21,23,19,22,18,20,15,17,13,16,12,14, 9,11, 7,10, 6, 8, 3, 5, 0, 4, 2, 1,
			  44,47,46,42,45,43,40,38,41,36,39,37,34,32,35,30,33,31,28,26,29,24,27,25,22,20,23,18,21,19,16,14,17,12,15,13,10, 8,11, 6, 9, 7, 4, 1, 5, 2, 3, 0,
			  45,46,47,43,44,42,41,39,40,37,38,36,35,33,34,31,32,30,29,27,28,25,26,24,23,21,22,19,20,18,17,15,16,13,14,12,11, 9,10, 7, 8, 6, 5, 3, 4, 0, 1, 2 ])
]).

============================== end of model ==========================

============================== STATISTICS ============================

For domain size 48.

Current CPU time: 0.00 seconds (total CPU time: 0.42 seconds).
Ground clauses: seen=110689, kept=110689.
Selections=141, assignments=2715, propagations=30441, current_models=1.
Rewrite_terms=625831, rewrite_bools=116620, indexes=170605.
Rules_from_neg_clauses=0, cross_offs=7.

============================== end of statistics =====================

User_CPU=0.42, System_CPU=0.03, Wall_clock=0.

Exiting with 1 model.

Process 11174 exit (max_models) Wed Feb 25 09:31:58 2009
The process finished Wed Feb 25 09:31:58 2009