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

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

% Reading from file group2.in

assign(iterate_up_to,12).

formulas(theory).
(all x all y all z ((x * y) * z = x * (y * z))).
(exists e ((all x (e * x = x)) & (all x exists y (y * x = e)))).
(exists a exists b (a * b != b * a)).
end_of_list.

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

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

% Formulas that are not ordinary clauses:
1 (all x all y all z ((x * y) * z = x * (y * z))).  [assumption].
2 (exists e ((all x (e * x = x)) & (all x exists y (y * x = e)))).  [assumption].
3 (exists a exists b (a * b != b * a)).  [assumption].

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

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

formulas(mace4_clauses).
(x * y) * z = x * (y * z).
c1 * x = x.
f1(x) * x = c1.
c3 * c2 != c2 * c3.
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=13, kept=13.
Selections=7, assignments=14, propagations=12, current_models=0.
Rewrite_terms=124, rewrite_bools=32, indexes=15.
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=34, kept=34.
Selections=13, assignments=36, propagations=52, current_models=0.
Rewrite_terms=575, rewrite_bools=140, indexes=84.
Rules_from_neg_clauses=15, cross_offs=40.

============================== 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=73, kept=73.
Selections=31, assignments=109, propagations=238, current_models=0.
Rewrite_terms=2863, rewrite_bools=654, indexes=450.
Rules_from_neg_clauses=51, cross_offs=214.

============================== 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=136, kept=136.
Selections=63, assignments=263, propagations=561, current_models=0.
Rewrite_terms=6624, rewrite_bools=1284, indexes=1592.
Rules_from_neg_clauses=82, cross_offs=593.

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

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

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

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

        function(c1, [ 0]),

        function(c2, [ 1]),

        function(c3, [ 2]),

        function(f1(_), [ 0, 1, 2, 4, 3, 5]),

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

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

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

For domain size 6.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=229, kept=229.
Selections=14, assignments=44, propagations=95, current_models=1.
Rewrite_terms=1596, rewrite_bools=347, indexes=379.
Rules_from_neg_clauses=9, cross_offs=141.

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

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

Exiting with 1 model.

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