============================== Mace4 =================================
Mace4 (32) version Dec-2007, Dec 2007.
Process 1488 was started by Alexei on Alexei-PC,
Mon Mar 25 21:54:12 2013
The command was "/cygdrive/c/Program Files (x86)/Prover9-Mace4/bin-win32/mace4 -c".
============================== end of head ===========================

============================== INPUT =================================
assign(report_stderr,2).
set(ignore_option_dependencies).
if(Prover9).
% Conditional input omitted.
end_if.
if(Mace4).
% Conditional input included.
assign(max_seconds,60).
end_if.

formulas(assumptions).
x * x = x.
(x * y) * y = x.
(x * y) * z = (x * z) * (y * z).
a2 = a1 * a5.
a3 = a2 * a10.
a4 = a3 * a8.
a5 = a4 * a9.
a6 = a5 * a2.
a7 = a6 * a3.
a8 = a7 * a1.
a9 = a8 * a4.
a10 = a9 * a6.
a1 = a10 * a7.
end_of_list.

formulas(goals).
a1 = a2 & a2 = a3 & a3 = a4 & a4 = a5 & a5 = a6 & a6 = a7 & a7 = a8 & a8 = a9 & a9 = a10.
end_of_list.

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

% Enabling option dependencies (ignore applies only on input).

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

% Formulas that are not ordinary clauses:
1 a1 = a2 & a2 = a3 & a3 = a4 & a4 = a5 & a5 = a6 & a6 = a7 & a7 = a8 & a8 = a9 & a9 = a10 # label(non_clause) # label(goal).  [goal].

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

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

formulas(mace4_clauses).
x * x = x.
(x * y) * y = x.
(x * y) * z = (x * z) * (y * z).
a2 = a1 * a5.
a3 = a2 * a10.
a4 = a3 * a8.
a5 = a4 * a9.
a6 = a5 * a2.
a7 = a6 * a3.
a8 = a7 * a1.
a9 = a8 * a4.
a10 = a9 * a6.
a1 = a10 * a7.
a1 != a2 | a3 != a2 | a4 != a3 | a4 != a5 | a6 != a5 | a7 != a6 | a7 != a8 | a9 != a8 | a9 != a10.
end_of_list.

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

% There are no domain elements in the input.

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

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

For domain size 2.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=25, kept=15.
Selections=5, assignments=9, propagations=15, current_models=0.
Rewrite_terms=80, rewrite_bools=23, indexes=0.
Rules_from_neg_clauses=6, cross_offs=6.

============================== 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=50, kept=44.
Selections=10, assignments=24, propagations=85, current_models=0.
Rewrite_terms=896, rewrite_bools=202, indexes=63.
Rules_from_neg_clauses=27, cross_offs=57.

============================== 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=95, kept=87.
Selections=18, assignments=57, propagations=176, current_models=0.
Rewrite_terms=2299, rewrite_bools=477, indexes=213.
Rules_from_neg_clauses=24, cross_offs=127.

============================== 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=166, kept=156.
Selections=28, assignments=109, propagations=333, current_models=0.
Rewrite_terms=5384, rewrite_bools=975, indexes=621.
Rules_from_neg_clauses=42, cross_offs=357.

============================== 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=269, kept=257.
Selections=44, assignments=208, propagations=670, current_models=0.
Rewrite_terms=13016, rewrite_bools=2406, indexes=1521.
Rules_from_neg_clauses=81, cross_offs=887.

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

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

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

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

        function(a1, [ 0 ]),

        function(a10, [ 1 ]),

        function(a2, [ 5 ]),

        function(a3, [ 6 ]),

        function(a4, [ 6 ]),

        function(a5, [ 6 ]),

        function(a6, [ 3 ]),

        function(a7, [ 2 ]),

        function(a8, [ 6 ]),

        function(a9, [ 6 ]),

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

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

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

For domain size 7.

Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
Ground clauses: seen=410, kept=396.
Selections=68, assignments=371, propagations=1256, current_models=1.
Rewrite_terms=24445, rewrite_bools=4031, indexes=3366.
Rules_from_neg_clauses=146, cross_offs=1984.

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

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

Exiting with 1 model.

Process 1488 exit (max_models) Mon Mar 25 21:54:12 2013
The process finished Mon Mar 25 21:54:12 2013