============================== Mace4 =================================
Mace4 (32) version Dec-2007, Dec 2007.
Process 3948 was started by Alexei on Alexei-PC,
Wed Apr 17 21:53:48 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 * a10.
a3 = a2 * a6.
a4 = a3 * a1.
a5 = a4 * a7.
a6 = a5 * a9.
a7 = a6 * a3.
a8 = a7 * a10.
a9 = a8 * a5.
a10 = a9 * a8.
a1 = a10 * a3.
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 * a10.
a3 = a2 * a6.
a4 = a3 * a1.
a5 = a4 * a7.
a6 = a5 * a9.
a7 = a6 * a3.
a8 = a7 * a10.
a9 = a8 * a5.
a10 = a9 * a8.
a1 = a10 * a3.
a1 != a2 | a3 != a2 | a4 != a3 | a5 != a4 | a5 != a6 | a7 != a6 | a8 != a7 | a8 != a9 | 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=88, rewrite_bools=26, 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=6, assignments=12, propagations=56, current_models=0.
Rewrite_terms=601, rewrite_bools=140, indexes=54.
Rules_from_neg_clauses=18, cross_offs=36.

============================== 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=13, assignments=37, propagations=102, current_models=0.
Rewrite_terms=1550, rewrite_bools=339, indexes=162.
Rules_from_neg_clauses=14, cross_offs=73.

============================== 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=18, assignments=61, propagations=180, current_models=0.
Rewrite_terms=3093, rewrite_bools=600, indexes=381.
Rules_from_neg_clauses=22, cross_offs=173.

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

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

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

For domain size 6.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=269, kept=257.
Selections=22, assignments=84, propagations=297, current_models=0.
Rewrite_terms=6585, rewrite_bools=1317, indexes=748.
Rules_from_neg_clauses=36, cross_offs=370.

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

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

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

For domain size 7.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=410, kept=396.
Selections=31, assignments=144, propagations=511, current_models=0.
Rewrite_terms=10795, rewrite_bools=1868, indexes=1475.
Rules_from_neg_clauses=56, cross_offs=752.

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

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

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

For domain size 8.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=595, kept=579.
Selections=36, assignments=184, propagations=709, current_models=0.
Rewrite_terms=17480, rewrite_bools=3066, indexes=2168.
Rules_from_neg_clauses=72, cross_offs=1475.

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

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

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

For domain size 9.

Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
Ground clauses: seen=830, kept=812.
Selections=49, assignments=298, propagations=1225, current_models=0.
Rewrite_terms=28168, rewrite_bools=4480, indexes=3963.
Rules_from_neg_clauses=93, cross_offs=2524.

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

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

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

For domain size 10.

Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
Ground clauses: seen=1121, kept=1101.
Selections=56, assignments=366, propagations=1534, current_models=0.
Rewrite_terms=38392, rewrite_bools=6216, indexes=5579.
Rules_from_neg_clauses=127, cross_offs=3570.

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

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

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

For domain size 11.

Current CPU time: 0.00 seconds (total CPU time: 0.03 seconds).
Ground clauses: seen=1474, kept=1452.
Selections=67, assignments=482, propagations=2063, current_models=0.
Rewrite_terms=50612, rewrite_bools=7400, indexes=7480.
Rules_from_neg_clauses=137, cross_offs=5380.

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

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

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

For domain size 12.

Current CPU time: 0.00 seconds (total CPU time: 0.05 seconds).
Ground clauses: seen=1895, kept=1871.
Selections=77, assignments=599, propagations=2836, current_models=0.
Rewrite_terms=74695, rewrite_bools=10872, indexes=10806.
Rules_from_neg_clauses=171, cross_offs=8228.

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

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

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

For domain size 13.

Current CPU time: 0.00 seconds (total CPU time: 0.08 seconds).
Ground clauses: seen=2390, kept=2364.
Selections=89, assignments=752, propagations=3489, current_models=0.
Rewrite_terms=93478, rewrite_bools=12860, indexes=14203.
Rules_from_neg_clauses=183, cross_offs=11307.

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

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

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

For domain size 14.

Current CPU time: 0.00 seconds (total CPU time: 0.11 seconds).
Ground clauses: seen=2965, kept=2937.
Selections=97, assignments=861, propagations=4330, current_models=0.
Rewrite_terms=124582, rewrite_bools=17515, indexes=18446.
Rules_from_neg_clauses=253, cross_offs=15624.

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

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

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

For domain size 15.

Current CPU time: 0.00 seconds (total CPU time: 0.16 seconds).
Ground clauses: seen=3626, kept=3596.
Selections=107, assignments=1007, propagations=5082, current_models=0.
Rewrite_terms=143784, rewrite_bools=18530, indexes=22991.
Rules_from_neg_clauses=273, cross_offs=20233.

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

============================== DOMAIN SIZE 16 ========================

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

For domain size 16.

Current CPU time: 0.00 seconds (total CPU time: 0.22 seconds).
Ground clauses: seen=4379, kept=4347.
Selections=117, assignments=1162, propagations=6146, current_models=0.
Rewrite_terms=179100, rewrite_bools=22973, indexes=28674.
Rules_from_neg_clauses=310, cross_offs=25652.

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

============================== DOMAIN SIZE 17 ========================

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

For domain size 17.

Current CPU time: 0.00 seconds (total CPU time: 0.30 seconds).
Ground clauses: seen=5230, kept=5196.
Selections=127, assignments=1327, propagations=7243, current_models=0.
Rewrite_terms=210488, rewrite_bools=25011, indexes=35395.
Rules_from_neg_clauses=242, cross_offs=32484.

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

============================== DOMAIN SIZE 18 ========================

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

For domain size 18.

Current CPU time: 0.00 seconds (total CPU time: 0.41 seconds).
Ground clauses: seen=6185, kept=6149.
Selections=140, assignments=1556, propagations=9152, current_models=0.
Rewrite_terms=265830, rewrite_bools=31701, indexes=46834.
Rules_from_neg_clauses=408, cross_offs=40026.

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

============================== DOMAIN SIZE 19 ========================

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

For domain size 19.

Current CPU time: 0.00 seconds (total CPU time: 0.53 seconds).
Ground clauses: seen=7250, kept=7212.
Selections=149, assignments=1727, propagations=10457, current_models=0.
Rewrite_terms=310125, rewrite_bools=35575, indexes=55325.
Rules_from_neg_clauses=344, cross_offs=47421.

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

============================== DOMAIN SIZE 20 ========================

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

For domain size 20.

Current CPU time: 0.00 seconds (total CPU time: 0.70 seconds).
Ground clauses: seen=8431, kept=8391.
Selections=155, assignments=1845, propagations=12175, current_models=0.
Rewrite_terms=369244, rewrite_bools=41811, indexes=64214.
Rules_from_neg_clauses=554, cross_offs=58645.

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

============================== DOMAIN SIZE 21 ========================

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

For domain size 21.

Current CPU time: 0.00 seconds (total CPU time: 0.91 seconds).
Ground clauses: seen=9734, kept=9692.
Selections=169, assignments=2132, propagations=14627, current_models=0.
Rewrite_terms=428663, rewrite_bools=45665, indexes=76165.
Rules_from_neg_clauses=550, cross_offs=72190.

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

============================== DOMAIN SIZE 22 ========================

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

For domain size 22.

Current CPU time: 0.00 seconds (total CPU time: 1.16 seconds).
Ground clauses: seen=11165, kept=11121.
Selections=183, assignments=2433, propagations=17279, current_models=0.
Rewrite_terms=495357, rewrite_bools=51463, indexes=90218.
Rules_from_neg_clauses=711, cross_offs=90057.

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

============================== DOMAIN SIZE 23 ========================

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

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

        function(a1, [ 0 ]),

        function(a10, [ 1 ]),

        function(a2, [ 3 ]),

        function(a3, [ 2 ]),

        function(a4, [ 9 ]),

        function(a5, [ 0 ]),

        function(a6, [ 5 ]),

        function(a7, [13 ]),

        function(a8, [14 ]),

        function(a9, [11 ]),

        function(*(_,_), [
			   0, 3, 1,15, 8,10, 4,16,18, 7,22, 5,21, 9,19,14,17,11, 2,20, 6,13,12,
			   7, 1, 0, 8, 3, 4, 2,21,22,16,15,18,17,12,11, 5, 6,10, 9,14,13,19,20,
			   9, 4, 2,11,10, 3, 1,20,13,12,19, 6,14, 7,15,17, 5, 8, 0,21,18,22,16,
			  16, 0, 7, 3, 1, 2, 9,17,15,21, 8,22, 6,20,10,18,13, 4,12, 5,19,11,14,
			  12, 2, 9,10, 4, 1, 0,14,19,20,11,13, 5,16, 8, 6,18, 3, 7,17,22,15,21,
			  19, 6,13,21,17, 5,18,10, 7,11,16, 0, 4,15,20, 1, 2,14,22, 3, 9,12, 8,
			  22, 5,18,20,14,17, 6, 8, 9,15,12, 2, 3,19,16, 4, 1,21,13,10, 0, 7,11,
			   1, 8, 3,22,15,11,10, 7, 5, 0,18,14,16, 2,13,20,21,19, 4,12,17, 6, 9,
			  21, 7,16, 1, 0, 9,12, 6, 8,17, 3,15,13,14, 4,22,19, 2,20,18,11,10, 5,
			   2,10, 4,19,11, 8, 3,12, 6, 9,13,17,20, 0,22,21,14,15, 1,16, 5,18, 7,
			  20, 9,12, 4, 2, 0, 7, 5,11,14,10,19,18,21, 3,13,22, 1,16, 6,15, 8,17,
			  14,12,20, 2, 9, 7,16,18,10, 5, 4,11,22,17, 1,19,15, 0,21,13, 8, 3, 6,
			   4,11,10,13,19,15, 8, 9,17, 2, 6,21,12, 1,18,16,20,22, 3, 7,14, 5, 0,
			  18,14, 5,12,20,21,17,15, 2,22, 9, 4, 8,13, 7,10, 3,16, 6,11, 1, 0,19,
			  11,13,19,17, 6,18,22, 4,16,10,21, 7, 2, 8,14, 0, 9, 5,15, 1,12,20, 3,
			  17,16,21, 0, 7,12,20,13, 3, 6, 1, 8,19, 5, 2,15,11, 9,14,22,10, 4,18,
			   3,15, 8,18,22,19,11, 0,14, 1, 5,20, 7, 4, 6,12,16,13,10, 9,21,17, 2,
			  15,18,22,14, 5, 6,13, 3,12, 8,20, 9, 1,11,21, 2, 0,17,19, 4, 7,16,10,
			  13,17, 6,16,21,14, 5,11, 0,19, 7, 1,10,22,12, 3, 4,20,18, 8, 2, 9,15,
			   5,20,14, 9,12,16,21,22, 4,18, 2,10,15, 6, 0,11, 8, 7,17,19, 3, 1,13,
			  10,19,11, 6,13,22,15, 2,21, 4,17,16, 9, 3, 5, 7,12,18, 8, 0,20,14, 1,
			   8,22,15, 5,18,13,19, 1,20, 3,14,12, 0,10,17, 9, 7, 6,11, 2,16,21, 4,
			   6,21,17, 7,16,20,14,19, 1,13, 0, 3,11,18, 9, 8,10,12, 5,15, 4, 2,22 ])
]).

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

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

For domain size 23.

Current CPU time: 0.00 seconds (total CPU time: 1.50 seconds).
Ground clauses: seen=12730, kept=12684.
Selections=194, assignments=2678, propagations=19656, current_models=1.
Rewrite_terms=602562, rewrite_bools=67561, indexes=104541.
Rules_from_neg_clauses=619, cross_offs=103181.

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

User_CPU=1.50, System_CPU=0.03, Wall_clock=1.

Exiting with 1 model.

Process 3948 exit (max_models) Wed Apr 17 21:53:49 2013
The process finished Wed Apr 17 21:53:49 2013