============================== Mace4 =================================
Mace4 (32) version August-2006A, August 2006.
Process 10606 was started by mccune on cleo.thornwood,
Sat Aug 12 20:57:15 2006
The command was "/home/mccune/bin/mace4 -c -N20 -f na-ring-2.in".
============================== end of head ===========================

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

% Reading from file na-ring-2.in


formulas(sos).
x + 0 = x.
x + -x = 0.
(x + y) + z = x + (y + z).
x + y = y + x.
x * (y + z) = (x * y) + (x * z).
(x + y) * z = (x * z) + (y * z).
(x * x) * y = x * (x * y).
(B * A) * A != B * (A * A).
end_of_list.

% From the command line: assign(iterate_up_to, 20).

============================== 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).
x + 0 = x.
x + -x = 0.
(x + y) + z = x + (y + z).
x + y = y + x.
x * (y + z) = (x * y) + (x * z).
(x + y) * z = (x * z) + (y * z).
(x * x) * y = x * (x * y).
(B * A) * A != B * (A * A).
end_of_list.

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

% The maximum domain element in the input is 0.

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

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

For domain size 2.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=37, kept=29.
Selections=13, assignments=26, propagations=7, current_models=0.
Rewrite_terms=270, rewrite_bools=48, indexes=28.
Rules_from_neg_clauses=4, cross_offs=4.

============================== 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=106, kept=100.
Selections=19, assignments=54, propagations=57, current_models=0.
Rewrite_terms=1610, rewrite_bools=299, indexes=215.
Rules_from_neg_clauses=11, cross_offs=24.

============================== 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=233, kept=225.
Selections=75, assignments=280, propagations=362, current_models=0.
Rewrite_terms=12844, rewrite_bools=2511, indexes=928.
Rules_from_neg_clauses=42, cross_offs=144.

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

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

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

For domain size 5.

Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
Ground clauses: seen=436, kept=426.
Selections=70, assignments=289, propagations=652, current_models=0.
Rewrite_terms=19423, rewrite_bools=3090, indexes=2419.
Rules_from_neg_clauses=101, cross_offs=451.

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

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

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

For domain size 6.

Current CPU time: 0.00 seconds (total CPU time: 0.02 seconds).
Ground clauses: seen=733, kept=721.
Selections=211, assignments=1094, propagations=2425, current_models=0.
Rewrite_terms=81948, rewrite_bools=12326, indexes=7868.
Rules_from_neg_clauses=350, cross_offs=1656.

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

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

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

For domain size 7.

Current CPU time: 0.00 seconds (total CPU time: 0.05 seconds).
Ground clauses: seen=1142, kept=1128.
Selections=223, assignments=1210, propagations=4467, current_models=0.
Rewrite_terms=134446, rewrite_bools=19046, indexes=16069.
Rules_from_neg_clauses=609, cross_offs=4479.

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

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

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

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

        function(A, [ 1]),

        function(B, [ 2]),

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

        function(*(_,_), [ 0, 0, 0, 0, 0, 0, 0, 0,
			   0, 0, 4, 4, 0, 0, 4, 4,
			   0, 2, 0, 2, 0, 2, 0, 2,
			   0, 2, 4, 6, 0, 2, 4, 6,
			   0, 6, 0, 6, 0, 6, 0, 6,
			   0, 6, 4, 2, 0, 6, 4, 2,
			   0, 4, 0, 4, 0, 4, 0, 4,
			   0, 4, 4, 0, 0, 4, 4, 0]),

        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.06 seconds).
Ground clauses: seen=1681, kept=1665.
Selections=67, assignments=285, propagations=572, current_models=1.
Rewrite_terms=24122, rewrite_bools=3671, indexes=5122.
Rules_from_neg_clauses=42, cross_offs=1089.

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

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

Exiting with 1 model.

Process 10606 exit (max_models) Sat Aug 12 20:57:15 2006
The process finished Sat Aug 12 20:57:15 2006