============================== Mace4 =================================
Mace4 (32) version March-2007, March 2007.
Process 20549 was started by mccune on cleo,
Mon Mar 19 17:00:37 2007
The command was "/home/mccune/bin/mace4 -f ring19.in".
============================== end of head ===========================

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

% Reading from file ring19.in

assign(domain_size,11).
    % assign(domain_size, 11) -> assign(iterate_up_to, 0).
assign(iterate_up_to,41).
set(iterate_primes).
set(integer_ring).

formulas(theory).
g(x) = M * x.
f(x,y) = (H * x) + (K * y).
f(f(a,b),c) != f(a,f(b,c)).
end_of_list.

formulas(candidates).
g(f(g(f(y,f(x,z))),f(y,f(f(x,x),g(x))))) = z.
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).
g(x) = M * x.
f(x,y) = (H * x) + (K * y).
f(f(a,b),c) != f(a,f(b,c)).
g(f(g(f(x,f(y,z))),f(x,f(f(y,y),g(y))))) = z.
end_of_list.

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

% The maximum domain element in the input is 0.

============================== DOMAIN SIZE 11 ========================

Clearing flag lnh, because the least number heuristic
is not compatible with flag integer_ring.

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

For domain size 11.

Current CPU time: 0.00 seconds (total CPU time: 0.10 seconds).
Ground clauses: seen=1464, kept=1464.
Selections=266, assignments=2926, propagations=29282, current_models=0.
Rewrite_terms=923036, rewrite_bools=21251, indexes=161051.
Rules_from_neg_clauses=0, cross_offs=0.

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

============================== DOMAIN SIZE 13 ========================

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

For domain size 13.

Current CPU time: 0.00 seconds (total CPU time: 0.34 seconds).
Ground clauses: seen=2380, kept=2380.
Selections=366, assignments=4758, propagations=57122, current_models=0.
Rewrite_terms=2030641, rewrite_bools=39493, indexes=371293.
Rules_from_neg_clauses=0, cross_offs=0.

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

============================== DOMAIN SIZE 17 ========================

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

For domain size 17.

Current CPU time: 0.00 seconds (total CPU time: 1.60 seconds).
Ground clauses: seen=5220, kept=5220.
Selections=614, assignments=10438, propagations=167042, current_models=0.
Rewrite_terms=7281011, rewrite_bools=108017, indexes=1419857.
Rules_from_neg_clauses=0, cross_offs=0.

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

============================== DOMAIN SIZE 19 ========================

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

interpretation( 19, [number=1, seconds=3], [

        function(H, [17 ]),

        function(K, [14 ]),

        function(M, [ 7 ]),

        function(a, [ 0 ]),

        function(b, [ 0 ]),

        function(c, [ 1 ]),

        function(g(_), [ 0, 7,14, 2, 9,16, 4,11,18, 6,13, 1, 8,15, 3,10,17, 5,12 ]),

        function(*(_,_), [
			   0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
			   0, 1, 2, 3, 4, 5, 6, 7, 8, 9,10,11,12,13,14,15,16,17,18,
			   0, 2, 4, 6, 8,10,12,14,16,18, 1, 3, 5, 7, 9,11,13,15,17,
			   0, 3, 6, 9,12,15,18, 2, 5, 8,11,14,17, 1, 4, 7,10,13,16,
			   0, 4, 8,12,16, 1, 5, 9,13,17, 2, 6,10,14,18, 3, 7,11,15,
			   0, 5,10,15, 1, 6,11,16, 2, 7,12,17, 3, 8,13,18, 4, 9,14,
			   0, 6,12,18, 5,11,17, 4,10,16, 3, 9,15, 2, 8,14, 1, 7,13,
			   0, 7,14, 2, 9,16, 4,11,18, 6,13, 1, 8,15, 3,10,17, 5,12,
			   0, 8,16, 5,13, 2,10,18, 7,15, 4,12, 1, 9,17, 6,14, 3,11,
			   0, 9,18, 8,17, 7,16, 6,15, 5,14, 4,13, 3,12, 2,11, 1,10,
			   0,10, 1,11, 2,12, 3,13, 4,14, 5,15, 6,16, 7,17, 8,18, 9,
			   0,11, 3,14, 6,17, 9, 1,12, 4,15, 7,18,10, 2,13, 5,16, 8,
			   0,12, 5,17,10, 3,15, 8, 1,13, 6,18,11, 4,16, 9, 2,14, 7,
			   0,13, 7, 1,14, 8, 2,15, 9, 3,16,10, 4,17,11, 5,18,12, 6,
			   0,14, 9, 4,18,13, 8, 3,17,12, 7, 2,16,11, 6, 1,15,10, 5,
			   0,15,11, 7, 3,18,14,10, 6, 2,17,13, 9, 5, 1,16,12, 8, 4,
			   0,16,13,10, 7, 4, 1,17,14,11, 8, 5, 2,18,15,12, 9, 6, 3,
			   0,17,15,13,11, 9, 7, 5, 3, 1,18,16,14,12,10, 8, 6, 4, 2,
			   0,18,17,16,15,14,13,12,11,10, 9, 8, 7, 6, 5, 4, 3, 2, 1 ]),

        function(+(_,_), [
			   0, 1, 2, 3, 4, 5, 6, 7, 8, 9,10,11,12,13,14,15,16,17,18,
			   1, 2, 3, 4, 5, 6, 7, 8, 9,10,11,12,13,14,15,16,17,18, 0,
			   2, 3, 4, 5, 6, 7, 8, 9,10,11,12,13,14,15,16,17,18, 0, 1,
			   3, 4, 5, 6, 7, 8, 9,10,11,12,13,14,15,16,17,18, 0, 1, 2,
			   4, 5, 6, 7, 8, 9,10,11,12,13,14,15,16,17,18, 0, 1, 2, 3,
			   5, 6, 7, 8, 9,10,11,12,13,14,15,16,17,18, 0, 1, 2, 3, 4,
			   6, 7, 8, 9,10,11,12,13,14,15,16,17,18, 0, 1, 2, 3, 4, 5,
			   7, 8, 9,10,11,12,13,14,15,16,17,18, 0, 1, 2, 3, 4, 5, 6,
			   8, 9,10,11,12,13,14,15,16,17,18, 0, 1, 2, 3, 4, 5, 6, 7,
			   9,10,11,12,13,14,15,16,17,18, 0, 1, 2, 3, 4, 5, 6, 7, 8,
			  10,11,12,13,14,15,16,17,18, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9,
			  11,12,13,14,15,16,17,18, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9,10,
			  12,13,14,15,16,17,18, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9,10,11,
			  13,14,15,16,17,18, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9,10,11,12,
			  14,15,16,17,18, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9,10,11,12,13,
			  15,16,17,18, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9,10,11,12,13,14,
			  16,17,18, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9,10,11,12,13,14,15,
			  17,18, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9,10,11,12,13,14,15,16,
			  18, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9,10,11,12,13,14,15,16,17 ]),

        function(f(_,_), [
			   0,14, 9, 4,18,13, 8, 3,17,12, 7, 2,16,11, 6, 1,15,10, 5,
			  17,12, 7, 2,16,11, 6, 1,15,10, 5, 0,14, 9, 4,18,13, 8, 3,
			  15,10, 5, 0,14, 9, 4,18,13, 8, 3,17,12, 7, 2,16,11, 6, 1,
			  13, 8, 3,17,12, 7, 2,16,11, 6, 1,15,10, 5, 0,14, 9, 4,18,
			  11, 6, 1,15,10, 5, 0,14, 9, 4,18,13, 8, 3,17,12, 7, 2,16,
			   9, 4,18,13, 8, 3,17,12, 7, 2,16,11, 6, 1,15,10, 5, 0,14,
			   7, 2,16,11, 6, 1,15,10, 5, 0,14, 9, 4,18,13, 8, 3,17,12,
			   5, 0,14, 9, 4,18,13, 8, 3,17,12, 7, 2,16,11, 6, 1,15,10,
			   3,17,12, 7, 2,16,11, 6, 1,15,10, 5, 0,14, 9, 4,18,13, 8,
			   1,15,10, 5, 0,14, 9, 4,18,13, 8, 3,17,12, 7, 2,16,11, 6,
			  18,13, 8, 3,17,12, 7, 2,16,11, 6, 1,15,10, 5, 0,14, 9, 4,
			  16,11, 6, 1,15,10, 5, 0,14, 9, 4,18,13, 8, 3,17,12, 7, 2,
			  14, 9, 4,18,13, 8, 3,17,12, 7, 2,16,11, 6, 1,15,10, 5, 0,
			  12, 7, 2,16,11, 6, 1,15,10, 5, 0,14, 9, 4,18,13, 8, 3,17,
			  10, 5, 0,14, 9, 4,18,13, 8, 3,17,12, 7, 2,16,11, 6, 1,15,
			   8, 3,17,12, 7, 2,16,11, 6, 1,15,10, 5, 0,14, 9, 4,18,13,
			   6, 1,15,10, 5, 0,14, 9, 4,18,13, 8, 3,17,12, 7, 2,16,11,
			   4,18,13, 8, 3,17,12, 7, 2,16,11, 6, 1,15,10, 5, 0,14, 9,
			   2,16,11, 6, 1,15,10, 5, 0,14, 9, 4,18,13, 8, 3,17,12, 7 ])
]).

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

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

For domain size 19.

Current CPU time: 0.00 seconds (total CPU time: 3.98 seconds).
Ground clauses: seen=7240, kept=7240.
Selections=741, assignments=14010, propagations=243827, current_models=1.
Rewrite_terms=11696989, rewrite_bools=162188, indexes=2318342.
Rules_from_neg_clauses=0, cross_offs=0.

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

User_CPU=3.98, System_CPU=0.03, Wall_clock=4.

Exiting with 1 model.

Process 20549 exit (max_models) Mon Mar 19 17:00:41 2007
The process finished Mon Mar 19 17:00:41 2007