============================== Mace4 =================================
Mace4 (32) version Dec-2007, Dec 2007.
Process 3120 was started by Alexei on Alexei-PC,
Wed Apr 17 23:59:32 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 * a8.
a6 = a5 * a3.
a7 = a6 * a9.
a8 = a7 * a5.
a9 = a8 * a10.
a10 = a9 * a7.
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 * a8.
a6 = a5 * a3.
a7 = a6 * a9.
a8 = a7 * a5.
a9 = a8 * a10.
a10 = a9 * a7.
a1 = a10 * a3.
a1 != a2 | a3 != a2 | a4 != a3 | a5 != a4 | a5 != a6 | 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.01 seconds).
Ground clauses: seen=25, kept=15.
Selections=5, assignments=9, propagations=17, current_models=0.
Rewrite_terms=88, rewrite_bools=25, 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.01 seconds).
Ground clauses: seen=50, kept=44.
Selections=7, assignments=15, propagations=59, current_models=0.
Rewrite_terms=684, rewrite_bools=160, indexes=55.
Rules_from_neg_clauses=18, cross_offs=38.

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

============================== DOMAIN SIZE 4 =========================

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

For domain size 4.

Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
Ground clauses: seen=95, kept=87.
Selections=15, assignments=45, propagations=101, current_models=0.
Rewrite_terms=1532, rewrite_bools=315, indexes=166.
Rules_from_neg_clauses=24, cross_offs=103.

============================== 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=18, assignments=58, propagations=154, current_models=0.
Rewrite_terms=2395, rewrite_bools=431, indexes=333.
Rules_from_neg_clauses=28, cross_offs=223.

============================== 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=25, assignments=95, propagations=248, current_models=0.
Rewrite_terms=5279, rewrite_bools=959, indexes=706.
Rules_from_neg_clauses=36, cross_offs=432.

============================== 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=34, assignments=154, propagations=444, current_models=0.
Rewrite_terms=9881, rewrite_bools=1720, indexes=1379.
Rules_from_neg_clauses=52, cross_offs=897.

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

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

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

For domain size 8.

Current CPU time: 0.00 seconds (total CPU time: 0.03 seconds).
Ground clauses: seen=595, kept=579.
Selections=42, assignments=216, propagations=690, current_models=0.
Rewrite_terms=16091, rewrite_bools=2550, indexes=2350.
Rules_from_neg_clauses=84, cross_offs=1614.

============================== 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=53, assignments=310, propagations=1163, current_models=0.
Rewrite_terms=28608, rewrite_bools=4462, indexes=4161.
Rules_from_neg_clauses=124, cross_offs=3084.

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

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

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

For domain size 10.

Current CPU time: 0.00 seconds (total CPU time: 0.03 seconds).
Ground clauses: seen=1121, kept=1101.
Selections=65, assignments=424, propagations=1586, current_models=0.
Rewrite_terms=38276, rewrite_bools=5733, indexes=6100.
Rules_from_neg_clauses=133, cross_offs=4477.

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

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

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

For domain size 11.

Current CPU time: 0.00 seconds (total CPU time: 0.05 seconds).
Ground clauses: seen=1474, kept=1452.
Selections=78, assignments=560, propagations=2218, current_models=0.
Rewrite_terms=55335, rewrite_bools=8016, indexes=8750.
Rules_from_neg_clauses=209, cross_offs=6954.

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

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

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

For domain size 12.

Current CPU time: 0.00 seconds (total CPU time: 0.06 seconds).
Ground clauses: seen=1895, kept=1871.
Selections=90, assignments=698, propagations=2718, current_models=0.
Rewrite_terms=76229, rewrite_bools=11164, indexes=11936.
Rules_from_neg_clauses=168, cross_offs=9881.

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

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

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

For domain size 13.

Current CPU time: 0.00 seconds (total CPU time: 0.09 seconds).
Ground clauses: seen=2390, kept=2364.
Selections=105, assignments=886, propagations=3811, current_models=0.
Rewrite_terms=98893, rewrite_bools=12828, indexes=16836.
Rules_from_neg_clauses=295, cross_offs=13694.

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

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

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

For domain size 14.

Current CPU time: 0.00 seconds (total CPU time: 0.12 seconds).
Ground clauses: seen=2965, kept=2937.
Selections=117, assignments=1048, propagations=4602, current_models=0.
Rewrite_terms=125224, rewrite_bools=16296, indexes=21704.
Rules_from_neg_clauses=225, cross_offs=17681.

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

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

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

For domain size 15.

Current CPU time: 0.00 seconds (total CPU time: 0.19 seconds).
Ground clauses: seen=3626, kept=3596.
Selections=133, assignments=1281, propagations=5964, current_models=0.
Rewrite_terms=166539, rewrite_bools=20600, indexes=29972.
Rules_from_neg_clauses=272, cross_offs=24996.

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

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

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

For domain size 16.

Current CPU time: 0.00 seconds (total CPU time: 0.25 seconds).
Ground clauses: seen=4379, kept=4347.
Selections=156, assignments=1642, propagations=7512, current_models=0.
Rewrite_terms=213110, rewrite_bools=26366, indexes=39250.
Rules_from_neg_clauses=298, cross_offs=31544.

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

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

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

For domain size 17.

Current CPU time: 0.00 seconds (total CPU time: 0.36 seconds).
Ground clauses: seen=5230, kept=5196.
Selections=176, assignments=1977, propagations=9724, current_models=0.
Rewrite_terms=276417, rewrite_bools=32860, indexes=50858.
Rules_from_neg_clauses=423, cross_offs=42524.

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

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

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

For domain size 18.

Current CPU time: 0.00 seconds (total CPU time: 0.48 seconds).
Ground clauses: seen=6185, kept=6149.
Selections=198, assignments=2367, propagations=11876, current_models=0.
Rewrite_terms=339022, rewrite_bools=38009, indexes=64753.
Rules_from_neg_clauses=441, cross_offs=56191.

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

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

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

For domain size 19.

Current CPU time: 0.00 seconds (total CPU time: 0.67 seconds).
Ground clauses: seen=7250, kept=7212.
Selections=226, assignments=2889, propagations=15104, current_models=0.
Rewrite_terms=439598, rewrite_bools=49973, indexes=82640.
Rules_from_neg_clauses=620, cross_offs=73855.

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

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

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

For domain size 20.

Current CPU time: 0.00 seconds (total CPU time: 0.91 seconds).
Ground clauses: seen=8431, kept=8391.
Selections=249, assignments=3339, propagations=18057, current_models=0.
Rewrite_terms=523894, rewrite_bools=56822, indexes=101253.
Rules_from_neg_clauses=666, cross_offs=92318.

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

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

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

For domain size 21.

Current CPU time: 0.00 seconds (total CPU time: 1.22 seconds).
Ground clauses: seen=9734, kept=9692.
Selections=278, assignments=3931, propagations=23048, current_models=0.
Rewrite_terms=660045, rewrite_bools=68954, indexes=127625.
Rules_from_neg_clauses=800, cross_offs=118400.

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

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

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

For domain size 22.

Current CPU time: 0.00 seconds (total CPU time: 1.61 seconds).
Ground clauses: seen=11165, kept=11121.
Selections=317, assignments=4768, propagations=29069, current_models=0.
Rewrite_terms=825719, rewrite_bools=85124, indexes=162429.
Rules_from_neg_clauses=975, cross_offs=149223.

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

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

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

For domain size 23.

Current CPU time: 0.00 seconds (total CPU time: 2.16 seconds).
Ground clauses: seen=12730, kept=12684.
Selections=350, assignments=5507, propagations=34739, current_models=0.
Rewrite_terms=1029682, rewrite_bools=109921, indexes=195740.
Rules_from_neg_clauses=1332, cross_offs=180686.

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

============================== DOMAIN SIZE 24 ========================

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

For domain size 24.

Current CPU time: 0.00 seconds (total CPU time: 2.89 seconds).
Ground clauses: seen=14435, kept=14387.
Selections=400, assignments=6678, propagations=43865, current_models=0.
Rewrite_terms=1307327, rewrite_bools=134186, indexes=250996.
Rules_from_neg_clauses=1553, cross_offs=242514.

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

============================== DOMAIN SIZE 25 ========================

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

For domain size 25.

Current CPU time: 0.00 seconds (total CPU time: 3.89 seconds).
Ground clauses: seen=16286, kept=16236.
Selections=445, assignments=7778, propagations=53210, current_models=0.
Rewrite_terms=1661582, rewrite_bools=173620, indexes=308331.
Rules_from_neg_clauses=1769, cross_offs=304910.

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

============================== DOMAIN SIZE 26 ========================

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

For domain size 26.

Current CPU time: 0.00 seconds (total CPU time: 5.05 seconds).
Ground clauses: seen=18289, kept=18237.
Selections=489, assignments=8891, propagations=62987, current_models=0.
Rewrite_terms=1883142, rewrite_bools=189271, indexes=360686.
Rules_from_neg_clauses=1950, cross_offs=358146.

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

============================== DOMAIN SIZE 27 ========================

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

For domain size 27.

Current CPU time: 0.00 seconds (total CPU time: 6.58 seconds).
Ground clauses: seen=20450, kept=20396.
Selections=546, assignments=10393, propagations=76425, current_models=0.
Rewrite_terms=2350094, rewrite_bools=237722, indexes=444605.
Rules_from_neg_clauses=2365, cross_offs=448858.

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

============================== DOMAIN SIZE 28 ========================

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

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

        function(a1, [ 0 ]),

        function(a10, [ 1 ]),

        function(a2, [ 2 ]),

        function(a3, [ 2 ]),

        function(a4, [ 1 ]),

        function(a5, [ 3 ]),

        function(a6, [ 3 ]),

        function(a7, [ 7 ]),

        function(a8, [ 4 ]),

        function(a9, [16 ]),

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

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

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

For domain size 28.

Current CPU time: 0.00 seconds (total CPU time: 6.72 seconds).
Ground clauses: seen=22775, kept=22719.
Selections=51, assignments=491, propagations=4332, current_models=1.
Rewrite_terms=139605, rewrite_bools=23949, indexes=16271.
Rules_from_neg_clauses=66, cross_offs=14227.

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

User_CPU=6.72, System_CPU=0.06, Wall_clock=7.

Exiting with 1 model.

Process 3120 exit (max_models) Wed Apr 17 23:59:39 2013
The process finished Wed Apr 17 23:59:39 2013