============================== Mace4 =================================
Mace4 (32) version Dec-2007, Dec 2007.
Process 3700 was started by Alexei on Alexei-PC,
Wed Apr 17 21:57:04 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 * a4.
a3 = a2 * a7.
a4 = a3 * a1.
a5 = a4 * a7.
a6 = a5 * a9.
a7 = a6 * a2.
a8 = a7 * a10.
a9 = a8 * a5.
a10 = a9 * a8.
a1 = a10 * a2.
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 * a4.
a3 = a2 * a7.
a4 = a3 * a1.
a5 = a4 * a7.
a6 = a5 * a9.
a7 = a6 * a2.
a8 = a7 * a10.
a9 = a8 * a5.
a10 = a9 * a8.
a1 = a10 * a2.
a1 != a2 | a3 != a2 | a3 != a4 | a5 != a4 | a6 != a5 | a6 != a7 | a8 != a7 | a8 != a9 | a10 != a9.
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=6, assignments=11, propagations=15, current_models=0.
Rewrite_terms=84, rewrite_bools=24, indexes=0.
Rules_from_neg_clauses=7, cross_offs=7.

============================== 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=7, assignments=14, propagations=54, current_models=0.
Rewrite_terms=522, rewrite_bools=113, indexes=51.
Rules_from_neg_clauses=20, cross_offs=43.

============================== 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=50, propagations=101, current_models=0.
Rewrite_terms=1379, rewrite_bools=281, indexes=160.
Rules_from_neg_clauses=22, cross_offs=102.

============================== 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=22, assignments=74, propagations=184, current_models=0.
Rewrite_terms=2584, rewrite_bools=442, indexes=367.
Rules_from_neg_clauses=28, cross_offs=243.

============================== 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=26, assignments=98, propagations=277, current_models=0.
Rewrite_terms=5123, rewrite_bools=937, indexes=725.
Rules_from_neg_clauses=33, cross_offs=417.

============================== 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=34, assignments=150, propagations=445, current_models=0.
Rewrite_terms=8860, rewrite_bools=1473, indexes=1306.
Rules_from_neg_clauses=65, cross_offs=842.

============================== 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=43, assignments=219, propagations=584, current_models=0.
Rewrite_terms=12335, rewrite_bools=1896, indexes=1958.
Rules_from_neg_clauses=42, cross_offs=1301.

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

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

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

For domain size 9.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=830, kept=812.
Selections=49, assignments=273, propagations=880, current_models=0.
Rewrite_terms=19539, rewrite_bools=2788, indexes=3170.
Rules_from_neg_clauses=75, cross_offs=2076.

============================== 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=341, propagations=1229, current_models=0.
Rewrite_terms=29311, rewrite_bools=4363, indexes=4716.
Rules_from_neg_clauses=96, cross_offs=3083.

============================== 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=61, assignments=396, propagations=1480, current_models=0.
Rewrite_terms=36133, rewrite_bools=4952, indexes=6144.
Rules_from_neg_clauses=87, cross_offs=4715.

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

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

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

For domain size 12.

Current CPU time: 0.00 seconds (total CPU time: 0.03 seconds).
Ground clauses: seen=1895, kept=1871.
Selections=69, assignments=488, propagations=2059, current_models=0.
Rewrite_terms=50443, rewrite_bools=6391, indexes=8700.
Rules_from_neg_clauses=144, cross_offs=6907.

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

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

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

For domain size 13.

Current CPU time: 0.00 seconds (total CPU time: 0.06 seconds).
Ground clauses: seen=2390, kept=2364.
Selections=81, assignments=637, propagations=2904, current_models=0.
Rewrite_terms=71944, rewrite_bools=9114, indexes=11617.
Rules_from_neg_clauses=181, cross_offs=9604.

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

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

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

For domain size 14.

Current CPU time: 0.00 seconds (total CPU time: 0.09 seconds).
Ground clauses: seen=2965, kept=2937.
Selections=89, assignments=745, propagations=3560, current_models=0.
Rewrite_terms=96482, rewrite_bools=12565, indexes=15670.
Rules_from_neg_clauses=181, cross_offs=13215.

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

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

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

For domain size 15.

Current CPU time: 0.00 seconds (total CPU time: 0.12 seconds).
Ground clauses: seen=3626, kept=3596.
Selections=99, assignments=889, propagations=4462, current_models=0.
Rewrite_terms=117935, rewrite_bools=14425, indexes=19662.
Rules_from_neg_clauses=217, cross_offs=17543.

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

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

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

For domain size 16.

Current CPU time: 0.00 seconds (total CPU time: 0.19 seconds).
Ground clauses: seen=4379, kept=4347.
Selections=109, assignments=1043, propagations=5424, current_models=0.
Rewrite_terms=154201, rewrite_bools=19740, indexes=24420.
Rules_from_neg_clauses=247, cross_offs=22825.

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

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

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

For domain size 17.

Current CPU time: 0.00 seconds (total CPU time: 0.27 seconds).
Ground clauses: seen=5230, kept=5196.
Selections=121, assignments=1240, propagations=6934, current_models=0.
Rewrite_terms=199728, rewrite_bools=24725, indexes=31563.
Rules_from_neg_clauses=302, cross_offs=29550.

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

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

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

For domain size 18.

Current CPU time: 0.00 seconds (total CPU time: 0.36 seconds).
Ground clauses: seen=6185, kept=6149.
Selections=132, assignments=1433, propagations=8257, current_models=0.
Rewrite_terms=252035, rewrite_bools=32584, indexes=40521.
Rules_from_neg_clauses=306, cross_offs=36749.

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

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

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

For domain size 19.

Current CPU time: 0.00 seconds (total CPU time: 0.50 seconds).
Ground clauses: seen=7250, kept=7212.
Selections=143, assignments=1638, propagations=9732, current_models=0.
Rewrite_terms=302770, rewrite_bools=39501, indexes=48750.
Rules_from_neg_clauses=352, cross_offs=44422.

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

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

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

For domain size 20.

Current CPU time: 0.00 seconds (total CPU time: 0.69 seconds).
Ground clauses: seen=8431, kept=8391.
Selections=151, assignments=1793, propagations=11234, current_models=0.
Rewrite_terms=372937, rewrite_bools=49103, indexes=56605.
Rules_from_neg_clauses=469, cross_offs=53723.

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

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

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

For domain size 21.

Current CPU time: 0.00 seconds (total CPU time: 0.89 seconds).
Ground clauses: seen=9734, kept=9692.
Selections=163, assignments=2036, propagations=12828, current_models=0.
Rewrite_terms=418800, rewrite_bools=53045, indexes=67137.
Rules_from_neg_clauses=411, cross_offs=64167.

============================== 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=175, assignments=2293, propagations=14660, current_models=0.
Rewrite_terms=483903, rewrite_bools=60932, indexes=78032.
Rules_from_neg_clauses=442, cross_offs=74799.

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

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

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

For domain size 23.

Current CPU time: 0.00 seconds (total CPU time: 1.48 seconds).
Ground clauses: seen=12730, kept=12684.
Selections=185, assignments=2517, propagations=17056, current_models=0.
Rewrite_terms=562860, rewrite_bools=68048, indexes=91562.
Rules_from_neg_clauses=608, cross_offs=88202.

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

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

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

For domain size 24.

Current CPU time: 0.00 seconds (total CPU time: 1.84 seconds).
Ground clauses: seen=14435, kept=14387.
Selections=196, assignments=2775, propagations=19033, current_models=0.
Rewrite_terms=639657, rewrite_bools=76930, indexes=106248.
Rules_from_neg_clauses=507, cross_offs=100919.

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

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

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

For domain size 25.

Current CPU time: 0.00 seconds (total CPU time: 2.33 seconds).
Ground clauses: seen=16286, kept=16236.
Selections=208, assignments=3070, propagations=22765, current_models=0.
Rewrite_terms=762670, rewrite_bools=90754, indexes=125345.
Rules_from_neg_clauses=717, cross_offs=122205.

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

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

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

For domain size 26.

Current CPU time: 0.00 seconds (total CPU time: 2.92 seconds).
Ground clauses: seen=18289, kept=18237.
Selections=215, assignments=3247, propagations=24758, current_models=0.
Rewrite_terms=843886, rewrite_bools=100165, indexes=139738.
Rules_from_neg_clauses=754, cross_offs=139503.

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

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

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

For domain size 27.

Current CPU time: 0.00 seconds (total CPU time: 3.66 seconds).
Ground clauses: seen=20450, kept=20396.
Selections=228, assignments=3589, propagations=29112, current_models=0.
Rewrite_terms=1029142, rewrite_bools=122119, indexes=166671.
Rules_from_neg_clauses=849, cross_offs=170621.

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

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

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

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

        function(a1, [ 0 ]),

        function(a10, [ 1 ]),

        function(a2, [ 2 ]),

        function(a3, [ 2 ]),

        function(a4, [ 1 ]),

        function(a5, [ 8 ]),

        function(a6, [ 3 ]),

        function(a7, [ 3 ]),

        function(a8, [ 5 ]),

        function(a9, [ 6 ]),

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

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

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

For domain size 28.

Current CPU time: 0.00 seconds (total CPU time: 3.80 seconds).
Ground clauses: seen=22775, kept=22719.
Selections=45, assignments=442, propagations=3272, current_models=1.
Rewrite_terms=136614, rewrite_bools=23634, indexes=14523.
Rules_from_neg_clauses=107, cross_offs=14488.

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

User_CPU=3.80, System_CPU=0.01, Wall_clock=4.

Exiting with 1 model.

Process 3700 exit (max_models) Wed Apr 17 21:57:08 2013
The process finished Wed Apr 17 21:57:08 2013