============================== Mace4 =================================
Mace4 (32) version Dec-2007, Dec 2007.
Process 2492 was started by Alexei on Alexei-PC,
Sun Mar 17 21:22: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 * a4.
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 * 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 * a6.
a4 = a3 * a1.
a5 = a4 * a7.
a6 = a5 * a9.
a7 = a6 * a3.
a8 = a7 * a10.
a9 = a8 * a5.
a10 = a9 * a8.
a1 = a10 * a2.
a1 != a2 | a3 != a2 | a3 != a4 | a5 != a4 | a5 != a6 | a7 != a6 | 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.01 seconds).
Ground clauses: seen=25, kept=15.
Selections=6, assignments=11, propagations=15, current_models=0.
Rewrite_terms=86, rewrite_bools=25, 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.01 seconds).
Ground clauses: seen=50, kept=44.
Selections=7, assignments=14, propagations=59, current_models=0.
Rewrite_terms=625, rewrite_bools=136, indexes=62.
Rules_from_neg_clauses=22, cross_offs=44.

============================== 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=17, assignments=50, propagations=109, current_models=0.
Rewrite_terms=1765, rewrite_bools=378, indexes=195.
Rules_from_neg_clauses=17, cross_offs=91.

============================== 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=23, assignments=79, propagations=210, current_models=0.
Rewrite_terms=3302, rewrite_bools=575, indexes=430.
Rules_from_neg_clauses=29, cross_offs=225.

============================== 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=27, assignments=103, propagations=316, current_models=0.
Rewrite_terms=7027, rewrite_bools=1394, indexes=815.
Rules_from_neg_clauses=40, cross_offs=440.

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

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

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

For domain size 7.

Current CPU time: 0.00 seconds (total CPU time: 0.03 seconds).
Ground clauses: seen=410, kept=396.
Selections=37, assignments=169, propagations=547, current_models=0.
Rewrite_terms=10908, rewrite_bools=1783, indexes=1553.
Rules_from_neg_clauses=65, cross_offs=819.

============================== 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=44, assignments=224, propagations=695, current_models=0.
Rewrite_terms=15718, rewrite_bools=2453, indexes=2223.
Rules_from_neg_clauses=54, cross_offs=1338.

============================== 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=55, assignments=321, propagations=1197, current_models=0.
Rewrite_terms=28884, rewrite_bools=4538, indexes=4074.
Rules_from_neg_clauses=86, cross_offs=2259.

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

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

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

For domain size 10.

Current CPU time: 0.00 seconds (total CPU time: 0.05 seconds).
Ground clauses: seen=1121, kept=1101.
Selections=61, assignments=380, propagations=1488, current_models=0.
Rewrite_terms=37301, rewrite_bools=5530, indexes=5791.
Rules_from_neg_clauses=107, cross_offs=3284.

============================== 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=72, assignments=495, propagations=2016, current_models=0.
Rewrite_terms=49439, rewrite_bools=6891, indexes=7510.
Rules_from_neg_clauses=127, cross_offs=5201.

============================== 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=86, assignments=656, propagations=2952, current_models=0.
Rewrite_terms=76790, rewrite_bools=10802, indexes=11515.
Rules_from_neg_clauses=159, cross_offs=8070.

============================== 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=100, assignments=834, propagations=3680, current_models=0.
Rewrite_terms=99451, rewrite_bools=13289, indexes=15382.
Rules_from_neg_clauses=155, cross_offs=11093.

============================== 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=106, assignments=915, propagations=4442, current_models=0.
Rewrite_terms=130017, rewrite_bools=17765, indexes=19078.
Rules_from_neg_clauses=260, cross_offs=15393.

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

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

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

For domain size 15.

Current CPU time: 0.00 seconds (total CPU time: 0.17 seconds).
Ground clauses: seen=3626, kept=3596.
Selections=121, assignments=1131, propagations=5602, current_models=0.
Rewrite_terms=154078, rewrite_bools=18661, indexes=24852.
Rules_from_neg_clauses=272, cross_offs=20455.

============================== 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=136, assignments=1363, propagations=6961, current_models=0.
Rewrite_terms=209301, rewrite_bools=27003, indexes=32663.
Rules_from_neg_clauses=393, cross_offs=27326.

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

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

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

For domain size 17.

Current CPU time: 0.00 seconds (total CPU time: 0.34 seconds).
Ground clauses: seen=5230, kept=5196.
Selections=153, assignments=1643, propagations=8872, current_models=0.
Rewrite_terms=264742, rewrite_bools=32913, indexes=41882.
Rules_from_neg_clauses=343, cross_offs=35385.

============================== 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=169, assignments=1923, propagations=11084, current_models=0.
Rewrite_terms=338215, rewrite_bools=42751, indexes=54677.
Rules_from_neg_clauses=485, cross_offs=45144.

============================== 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=187, assignments=2257, propagations=13377, current_models=0.
Rewrite_terms=407044, rewrite_bools=51155, indexes=66474.
Rules_from_neg_clauses=404, cross_offs=55593.

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

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

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

For domain size 20.

Current CPU time: 0.00 seconds (total CPU time: 0.92 seconds).
Ground clauses: seen=8431, kept=8391.
Selections=200, assignments=2509, propagations=16149, current_models=0.
Rewrite_terms=528827, rewrite_bools=71001, indexes=79321.
Rules_from_neg_clauses=701, cross_offs=70009.

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

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

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

For domain size 21.

Current CPU time: 0.00 seconds (total CPU time: 1.23 seconds).
Ground clauses: seen=9734, kept=9692.
Selections=222, assignments=2958, propagations=19505, current_models=0.
Rewrite_terms=637194, rewrite_bools=84271, indexes=97942.
Rules_from_neg_clauses=687, cross_offs=85884.

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

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

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

For domain size 22.

Current CPU time: 0.00 seconds (total CPU time: 1.62 seconds).
Ground clauses: seen=11165, kept=11121.
Selections=240, assignments=3343, propagations=22250, current_models=0.
Rewrite_terms=712881, rewrite_bools=89119, indexes=113204.
Rules_from_neg_clauses=821, cross_offs=104017.

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

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

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

For domain size 23.

Current CPU time: 0.00 seconds (total CPU time: 2.12 seconds).
Ground clauses: seen=12730, kept=12684.
Selections=258, assignments=3745, propagations=24977, current_models=0.
Rewrite_terms=855266, rewrite_bools=109863, indexes=132474.
Rules_from_neg_clauses=999, cross_offs=123809.

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

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

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

For domain size 24.

Current CPU time: 0.00 seconds (total CPU time: 2.72 seconds).
Ground clauses: seen=14435, kept=14387.
Selections=275, assignments=4144, propagations=28515, current_models=0.
Rewrite_terms=995568, rewrite_bools=126431, indexes=158622.
Rules_from_neg_clauses=934, cross_offs=148400.

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

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

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

For domain size 25.

Current CPU time: 0.00 seconds (total CPU time: 3.42 seconds).
Ground clauses: seen=16286, kept=16236.
Selections=293, assignments=4588, propagations=33058, current_models=0.
Rewrite_terms=1107784, rewrite_bools=132057, indexes=183055.
Rules_from_neg_clauses=920, cross_offs=174549.

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

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

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

For domain size 26.

Current CPU time: 0.00 seconds (total CPU time: 4.23 seconds).
Ground clauses: seen=18289, kept=18237.
Selections=301, assignments=4791, propagations=35805, current_models=0.
Rewrite_terms=1220113, rewrite_bools=143997, indexes=201711.
Rules_from_neg_clauses=1212, cross_offs=199246.

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

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

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

For domain size 27.

Current CPU time: 0.00 seconds (total CPU time: 5.25 seconds).
Ground clauses: seen=20450, kept=20396.
Selections=319, assignments=5265, propagations=41143, current_models=0.
Rewrite_terms=1448344, rewrite_bools=172354, indexes=235545.
Rules_from_neg_clauses=1083, cross_offs=239348.

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

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

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

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

        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: 5.51 seconds).
Ground clauses: seen=22775, kept=22719.
Selections=89, assignments=1109, propagations=9134, current_models=1.
Rewrite_terms=321297, rewrite_bools=43833, indexes=49276.
Rules_from_neg_clauses=436, cross_offs=57205.

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

User_CPU=5.51, System_CPU=0.00, Wall_clock=5.

Exiting with 1 model.

Process 2492 exit (max_models) Sun Mar 17 21:22:53 2013
The process finished Sun Mar 17 21:22:53 2013