============================== Mace4 =================================
Mace4 (32) version Dec-2007, Dec 2007.
Process 4004 was started by Alexei on Alexei-PC,
Mon Mar 25 21:48:31 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 * a1.
a6 = a5 * a9.
a7 = a6 * a2.
a8 = a7 * a4.
a9 = a8 * a3.
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 * a1.
a6 = a5 * a9.
a7 = a6 * a2.
a8 = a7 * a4.
a9 = a8 * a3.
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=16, current_models=0.
Rewrite_terms=80, rewrite_bools=22, 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=9, assignments=21, propagations=78, current_models=0.
Rewrite_terms=818, rewrite_bools=192, indexes=60.
Rules_from_neg_clauses=26, cross_offs=59.

============================== 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=17, assignments=53, propagations=154, current_models=0.
Rewrite_terms=2006, rewrite_bools=419, indexes=208.
Rules_from_neg_clauses=51, cross_offs=180.

============================== 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=166, kept=156.
Selections=28, assignments=108, propagations=282, current_models=0.
Rewrite_terms=4164, rewrite_bools=778, indexes=533.
Rules_from_neg_clauses=78, cross_offs=467.

============================== 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=42, assignments=194, propagations=604, current_models=0.
Rewrite_terms=11240, rewrite_bools=2116, indexes=1372.
Rules_from_neg_clauses=174, cross_offs=1226.

============================== 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=410, kept=396.
Selections=70, assignments=393, propagations=1213, current_models=0.
Rewrite_terms=23647, rewrite_bools=3946, indexes=3396.
Rules_from_neg_clauses=230, cross_offs=2501.

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

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

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

For domain size 8.

Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
Ground clauses: seen=595, kept=579.
Selections=102, assignments=655, propagations=2016, current_models=0.
Rewrite_terms=44341, rewrite_bools=6996, indexes=6720.
Rules_from_neg_clauses=374, cross_offs=5163.

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

============================== DOMAIN SIZE 9 =========================

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

For domain size 9.

Current CPU time: 0.00 seconds (total CPU time: 0.03 seconds).
Ground clauses: seen=830, kept=812.
Selections=181, assignments=1368, propagations=4321, current_models=0.
Rewrite_terms=101957, rewrite_bools=15126, indexes=15863.
Rules_from_neg_clauses=565, cross_offs=10346.

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

============================== DOMAIN SIZE 10 ========================

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

For domain size 10.

Current CPU time: 0.00 seconds (total CPU time: 0.08 seconds).
Ground clauses: seen=1121, kept=1101.
Selections=272, assignments=2287, propagations=7518, current_models=0.
Rewrite_terms=192372, rewrite_bools=26921, indexes=31896.
Rules_from_neg_clauses=953, cross_offs=21052.

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

============================== DOMAIN SIZE 11 ========================

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

For domain size 11.

Current CPU time: 0.00 seconds (total CPU time: 0.12 seconds).
Ground clauses: seen=1474, kept=1452.
Selections=402, assignments=3719, propagations=12404, current_models=0.
Rewrite_terms=323339, rewrite_bools=42218, indexes=57451.
Rules_from_neg_clauses=1219, cross_offs=36405.

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

============================== DOMAIN SIZE 12 ========================

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

For domain size 12.

Current CPU time: 0.00 seconds (total CPU time: 0.25 seconds).
Ground clauses: seen=1895, kept=1871.
Selections=623, assignments=6333, propagations=21963, current_models=0.
Rewrite_terms=617685, rewrite_bools=80059, indexes=108089.
Rules_from_neg_clauses=2095, cross_offs=72398.

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

============================== DOMAIN SIZE 13 ========================

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

For domain size 13.

Current CPU time: 0.00 seconds (total CPU time: 0.44 seconds).
Ground clauses: seen=2390, kept=2364.
Selections=917, assignments=10124, propagations=35493, current_models=0.
Rewrite_terms=965181, rewrite_bools=113430, indexes=182010.
Rules_from_neg_clauses=2601, cross_offs=114744.

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

============================== DOMAIN SIZE 14 ========================

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

For domain size 14.

Current CPU time: 0.00 seconds (total CPU time: 0.81 seconds).
Ground clauses: seen=2965, kept=2937.
Selections=1341, assignments=15979, propagations=58233, current_models=0.
Rewrite_terms=1706055, rewrite_bools=202338, indexes=318225.
Rules_from_neg_clauses=4092, cross_offs=210902.

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

============================== DOMAIN SIZE 15 ========================

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

interpretation( 15, [number=1, seconds=1], [

        function(a1, [ 0 ]),

        function(a10, [ 1 ]),

        function(a2, [ 3 ]),

        function(a3, [10 ]),

        function(a4, [ 5 ]),

        function(a5, [ 4 ]),

        function(a6, [ 7 ]),

        function(a7, [ 2 ]),

        function(a8, [11 ]),

        function(a9, [ 9 ]),

        function(*(_,_), [
			   0, 2, 1, 5, 3, 6, 4,13, 0, 0,12,14,10,11, 7,
			   2, 1, 0, 8, 7, 1,11, 9,10,12,14, 6, 4, 1, 3,
			   1, 0, 2, 7, 2,11, 8, 3,12,10, 5, 9,13, 6, 2,
			   6,10, 7, 3, 0, 4, 5, 2,14,13, 8, 3, 3, 9, 1,
			   5, 9, 4, 6, 4, 3, 0,12,11, 7,13, 8, 1,10, 4,
			   4, 5, 9, 0, 6, 5, 3, 8, 7,11, 2,10,14, 5,12,
			   3,11,12, 4, 5, 0, 6, 6,13,14, 6, 1, 8, 2, 9,
			  11,12, 3, 2, 1, 8, 7, 7, 5, 4, 7,13, 9,14, 0,
			   8,14,13, 1,11, 7, 2, 5, 8, 8, 3, 4, 6,12,10,
			   9, 4, 5,13,12,10,14, 1, 9, 9,11, 2, 7, 3, 6,
			  12, 3,11,14,13, 9,10,10, 1, 2,10, 5, 0, 4, 8,
			   7, 6,10,11, 8, 2, 1,14, 4, 5, 9,11,11, 0,13,
			  10, 7, 6,12, 9,14,13, 4, 2, 1, 0,12,12, 8, 5,
			  14,13, 8, 9,10,13,12, 0, 6, 3, 4, 7, 2,13,11,
			  13, 8,14,10,14,12, 9,11, 3, 6, 1, 0, 5, 7,14 ])
]).

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

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

For domain size 15.

Current CPU time: 0.00 seconds (total CPU time: 1.01 seconds).
Ground clauses: seen=3626, kept=3596.
Selections=607, assignments=7160, propagations=25409, current_models=1.
Rewrite_terms=775272, rewrite_bools=89753, indexes=146550.
Rules_from_neg_clauses=1278, cross_offs=99515.

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

User_CPU=1.01, System_CPU=0.00, Wall_clock=1.

Exiting with 1 model.

Process 4004 exit (max_models) Mon Mar 25 21:48:32 2013
The process finished Mon Mar 25 21:48:32 2013