============================== Mace4 =================================
Mace4 (32) version 22-May-2007, May 2007.
Process 26984 was started by mccune on cleo,
Tue May 22 14:44:27 2007
The command was "/home/mccune/bin/mace4 -f group2.in".
============================== end of head ===========================

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

% Reading from file group2.in


formulas(assumptions).
(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 (exists e ((all x e * x = x) & (all x exists y y * x = e))) # label(non_clause).  [assumption].
2 (exists a exists b a * b != b * a) # label(non_clause).  [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 26984 exit (max_models) Tue May 22 14:44:27 2007
The process finished Tue May 22 14:44:27 2007