============================== Mace4 =================================
Mace4 (32) version August-2006A, August 2006.
Process 10699 was started by mccune on cleo.thornwood,
Sat Aug 12 20:58:11 2006
The command was "/home/mccune/bin/mace4 -f noncommutative-ring.in".
============================== end of head ===========================

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

% Reading from file noncommutative-ring.in

assign(iterate_up_to,8).

formulas(theory).
0 + x = x.
x + 0 = x.
-x + x = 0.
x + -x = 0.
(x + y) + z = x + (y + z).
x + y = y + x.
(x * y) * z = x * (y * z).
x * (y + z) = (x * y) + (x * z).
(y + z) * x = (y * x) + (z * x).
--x = x.
-0 = 0.
0 * x = 0.
x * 0 = 0.
1 * x = x.
x * 1 = x.
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).
0 + x = x.
x + 0 = x.
-x + x = 0.
x + -x = 0.
(x + y) + z = x + (y + z).
x + y = y + x.
(x * y) * z = x * (y * z).
x * (y + z) = (x * y) + (x * z).
(x + y) * z = (x * z) + (y * z).
--x = x.
-0 = 0.
0 * x = 0.
x * 0 = 0.
1 * x = x.
x * 1 = x.
a * b != b * a.
end_of_list.

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

% The maximum domain element in the input is 1.

============================== DOMAIN SIZE 2 =========================

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

For domain size 2.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=56, kept=34.
Selections=3, assignments=6, propagations=10, current_models=0.
Rewrite_terms=127, rewrite_bools=37, indexes=4.
Rules_from_neg_clauses=2, cross_offs=2.

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

============================== DOMAIN SIZE 3 =========================

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

For domain size 3.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=146, kept=126.
Selections=5, assignments=15, propagations=25, current_models=0.
Rewrite_terms=568, rewrite_bools=157, indexes=35.
Rules_from_neg_clauses=4, cross_offs=11.

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

============================== DOMAIN SIZE 4 =========================

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

For domain size 4.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=310, kept=285.
Selections=12, assignments=44, propagations=54, current_models=0.
Rewrite_terms=1781, rewrite_bools=469, indexes=103.
Rules_from_neg_clauses=10, cross_offs=43.

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

============================== DOMAIN SIZE 5 =========================

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

For domain size 5.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=572, kept=542.
Selections=19, assignments=81, propagations=147, current_models=0.
Rewrite_terms=3588, rewrite_bools=850, indexes=324.
Rules_from_neg_clauses=39, cross_offs=157.

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

============================== DOMAIN SIZE 6 =========================

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

For domain size 6.

Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
Ground clauses: seen=956, kept=921.
Selections=28, assignments=136, propagations=240, current_models=0.
Rewrite_terms=6635, rewrite_bools=1516, indexes=584.
Rules_from_neg_clauses=96, cross_offs=451.

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

============================== DOMAIN SIZE 7 =========================

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

For domain size 7.

Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
Ground clauses: seen=1486, kept=1446.
Selections=48, assignments=266, propagations=547, current_models=0.
Rewrite_terms=15614, rewrite_bools=3261, indexes=1867.
Rules_from_neg_clauses=154, cross_offs=1098.

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

============================== DOMAIN SIZE 8 =========================

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

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

        function(a, [ 2]),

        function(b, [ 4]),

        function(-(_), [ 0, 1, 2, 3, 4, 5, 6, 7]),

        function(*(_,_), [ 0, 0, 0, 0, 0, 0, 0, 0,
			   0, 1, 2, 3, 4, 5, 6, 7,
			   0, 2, 0, 2, 0, 2, 0, 2,
			   0, 3, 2, 1, 4, 7, 6, 5,
			   0, 4, 2, 6, 4, 0, 6, 2,
			   0, 5, 0, 5, 0, 5, 0, 5,
			   0, 6, 2, 4, 4, 2, 6, 0,
			   0, 7, 0, 7, 0, 7, 0, 7]),

        function(+(_,_), [ 0, 1, 2, 3, 4, 5, 6, 7,
			   1, 0, 3, 2, 5, 4, 7, 6,
			   2, 3, 0, 1, 6, 7, 4, 5,
			   3, 2, 1, 0, 7, 6, 5, 4,
			   4, 5, 6, 7, 0, 1, 2, 3,
			   5, 4, 7, 6, 1, 0, 3, 2,
			   6, 7, 4, 5, 2, 3, 0, 1,
			   7, 6, 5, 4, 3, 2, 1, 0])
]).

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

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

For domain size 8.

Current CPU time: 0.00 seconds (total CPU time: 0.02 seconds).
Ground clauses: seen=2186, kept=2141.
Selections=15, assignments=63, propagations=238, current_models=1.
Rewrite_terms=11758, rewrite_bools=2551, indexes=1472.
Rules_from_neg_clauses=20, cross_offs=561.

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

User_CPU=0.02, System_CPU=0.00, Wall_clock=0.

Exiting with 1 model.

Process 10699 exit (max_models) Sat Aug 12 20:58:11 2006
The process finished Sat Aug 12 20:58:11 2006