============================== Mace4 =================================
Mace4 (32) version Dec-2007, Dec 2007.
Process 4064 was started by Alexei on Alexei-PC,
Sun Mar 17 21:18:19 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,-1).
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 * a8.
a6 = a5 * a3.
a7 = a6 * a10.
a8 = a7 * a9.
a9 = a8 * a5.
a10 = a9 * a7.
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 * a8.
a6 = a5 * a3.
a7 = a6 * a10.
a8 = a7 * a9.
a9 = a8 * a5.
a10 = a9 * a7.
a1 = a10 * a2.
a1 != a2 | a3 != a2 | a3 != a4 | 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.03 seconds).
Ground clauses: seen=25, kept=15.
Selections=5, assignments=9, propagations=15, current_models=0.
Rewrite_terms=80, rewrite_bools=23, 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.03 seconds).
Ground clauses: seen=50, kept=44.
Selections=7, assignments=15, propagations=58, current_models=0.
Rewrite_terms=620, rewrite_bools=135, indexes=51.
Rules_from_neg_clauses=21, cross_offs=44.

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

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

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

For domain size 4.

Current CPU time: 0.00 seconds (total CPU time: 0.03 seconds).
Ground clauses: seen=95, kept=87.
Selections=15, assignments=45, propagations=107, current_models=0.
Rewrite_terms=1556, rewrite_bools=318, indexes=172.
Rules_from_neg_clauses=26, cross_offs=113.

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

============================== DOMAIN SIZE 5 =========================

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

For domain size 5.

Current CPU time: 0.00 seconds (total CPU time: 0.03 seconds).
Ground clauses: seen=166, kept=156.
Selections=18, assignments=59, propagations=172, current_models=0.
Rewrite_terms=2194, rewrite_bools=343, indexes=316.
Rules_from_neg_clauses=35, cross_offs=248.

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

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

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

For domain size 6.

Current CPU time: 0.00 seconds (total CPU time: 0.03 seconds).
Ground clauses: seen=269, kept=257.
Selections=23, assignments=86, propagations=251, current_models=0.
Rewrite_terms=5111, rewrite_bools=942, indexes=673.
Rules_from_neg_clauses=39, cross_offs=437.

============================== 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=31, assignments=138, propagations=413, current_models=0.
Rewrite_terms=8372, rewrite_bools=1375, indexes=1159.
Rules_from_neg_clauses=59, cross_offs=812.

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

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

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

For domain size 8.

Current CPU time: 0.00 seconds (total CPU time: 0.05 seconds).
Ground clauses: seen=595, kept=579.
Selections=37, assignments=184, propagations=547, current_models=0.
Rewrite_terms=10980, rewrite_bools=1520, indexes=1885.
Rules_from_neg_clauses=62, cross_offs=1263.

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

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

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

For domain size 9.

Current CPU time: 0.00 seconds (total CPU time: 0.05 seconds).
Ground clauses: seen=830, kept=812.
Selections=48, assignments=279, propagations=982, current_models=0.
Rewrite_terms=20661, rewrite_bools=2545, indexes=3532.
Rules_from_neg_clauses=96, cross_offs=2269.

============================== 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=55, assignments=350, propagations=1208, current_models=0.
Rewrite_terms=27909, rewrite_bools=3338, indexes=5085.
Rules_from_neg_clauses=102, cross_offs=3154.

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

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

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

For domain size 11.

Current CPU time: 0.00 seconds (total CPU time: 0.06 seconds).
Ground clauses: seen=1474, kept=1452.
Selections=61, assignments=414, propagations=1498, current_models=0.
Rewrite_terms=40214, rewrite_bools=4876, indexes=7166.
Rules_from_neg_clauses=117, cross_offs=5003.

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

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

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

For domain size 12.

Current CPU time: 0.00 seconds (total CPU time: 0.08 seconds).
Ground clauses: seen=1895, kept=1871.
Selections=78, assignments=611, propagations=2508, current_models=0.
Rewrite_terms=71503, rewrite_bools=9468, indexes=11468.
Rules_from_neg_clauses=177, cross_offs=7962.

============================== 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=89, assignments=750, propagations=3167, current_models=0.
Rewrite_terms=93918, rewrite_bools=11877, indexes=15556.
Rules_from_neg_clauses=254, cross_offs=11686.

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

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

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

For domain size 14.

Current CPU time: 0.00 seconds (total CPU time: 0.14 seconds).
Ground clauses: seen=2965, kept=2937.
Selections=104, assignments=954, propagations=4160, current_models=0.
Rewrite_terms=125151, rewrite_bools=15403, indexes=21101.
Rules_from_neg_clauses=241, cross_offs=15822.

============================== 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=125, assignments=1261, propagations=5591, current_models=0.
Rewrite_terms=170609, rewrite_bools=20209, indexes=31003.
Rules_from_neg_clauses=314, cross_offs=22916.

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

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

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

For domain size 16.

Current CPU time: 0.00 seconds (total CPU time: 0.27 seconds).
Ground clauses: seen=4379, kept=4347.
Selections=145, assignments=1574, propagations=7352, current_models=0.
Rewrite_terms=222776, rewrite_bools=25815, indexes=41237.
Rules_from_neg_clauses=335, cross_offs=30896.

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

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

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

For domain size 17.

Current CPU time: 0.00 seconds (total CPU time: 0.38 seconds).
Ground clauses: seen=5230, kept=5196.
Selections=169, assignments=1972, propagations=9704, current_models=0.
Rewrite_terms=302098, rewrite_bools=34915, indexes=54179.
Rules_from_neg_clauses=455, cross_offs=42085.

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

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

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

For domain size 18.

Current CPU time: 0.00 seconds (total CPU time: 0.52 seconds).
Ground clauses: seen=6185, kept=6149.
Selections=197, assignments=2466, propagations=12424, current_models=0.
Rewrite_terms=390264, rewrite_bools=44082, indexes=73083.
Rules_from_neg_clauses=579, cross_offs=57995.

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

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

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

For domain size 19.

Current CPU time: 0.00 seconds (total CPU time: 0.72 seconds).
Ground clauses: seen=7250, kept=7212.
Selections=228, assignments=3047, propagations=16160, current_models=0.
Rewrite_terms=497736, rewrite_bools=55143, indexes=94811.
Rules_from_neg_clauses=681, cross_offs=76337.

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

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

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

For domain size 20.

Current CPU time: 0.00 seconds (total CPU time: 1.00 seconds).
Ground clauses: seen=8431, kept=8391.
Selections=260, assignments=3674, propagations=20022, current_models=0.
Rewrite_terms=632232, rewrite_bools=67728, indexes=120399.
Rules_from_neg_clauses=914, cross_offs=102377.

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

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

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

For domain size 21.

Current CPU time: 0.00 seconds (total CPU time: 1.36 seconds).
Ground clauses: seen=9734, kept=9692.
Selections=306, assignments=4622, propagations=26179, current_models=0.
Rewrite_terms=819533, rewrite_bools=85156, indexes=161917.
Rules_from_neg_clauses=1042, cross_offs=139400.

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

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

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

For domain size 22.

Current CPU time: 0.00 seconds (total CPU time: 1.84 seconds).
Ground clauses: seen=11165, kept=11121.
Selections=357, assignments=5730, propagations=33305, current_models=0.
Rewrite_terms=1017958, rewrite_bools=101607, indexes=206778.
Rules_from_neg_clauses=1214, cross_offs=178915.

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

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

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

For domain size 23.

Current CPU time: 0.00 seconds (total CPU time: 2.48 seconds).
Ground clauses: seen=12730, kept=12684.
Selections=412, assignments=6980, propagations=40930, current_models=0.
Rewrite_terms=1273027, rewrite_bools=121930, indexes=262526.
Rules_from_neg_clauses=1465, cross_offs=237226.

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

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

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

For domain size 24.

Current CPU time: 0.00 seconds (total CPU time: 3.42 seconds).
Ground clauses: seen=14435, kept=14387.
Selections=481, assignments=8617, propagations=53283, current_models=0.
Rewrite_terms=1718934, rewrite_bools=174824, indexes=337743.
Rules_from_neg_clauses=1639, cross_offs=323357.

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

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

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

For domain size 25.

Current CPU time: 0.00 seconds (total CPU time: 4.67 seconds).
Ground clauses: seen=16286, kept=16236.
Selections=565, assignments=10697, propagations=67608, current_models=0.
Rewrite_terms=2182724, rewrite_bools=218337, indexes=435895.
Rules_from_neg_clauses=1993, cross_offs=424027.

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

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

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

For domain size 26.

Current CPU time: 0.00 seconds (total CPU time: 6.20 seconds).
Ground clauses: seen=18289, kept=18237.
Selections=640, assignments=12623, propagations=82403, current_models=0.
Rewrite_terms=2620174, rewrite_bools=244574, indexes=538975.
Rules_from_neg_clauses=2413, cross_offs=555120.

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

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

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

For domain size 27.

Current CPU time: 0.00 seconds (total CPU time: 8.31 seconds).
Ground clauses: seen=20450, kept=20396.
Selections=784, assignments=16465, propagations=109217, current_models=0.
Rewrite_terms=3502464, rewrite_bools=319518, indexes=721433.
Rules_from_neg_clauses=3106, cross_offs=789781.

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

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

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

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

        function(a1, [ 0 ]),

        function(a10, [ 1 ]),

        function(a2, [ 2 ]),

        function(a3, [ 2 ]),

        function(a4, [ 1 ]),

        function(a5, [ 3 ]),

        function(a6, [ 3 ]),

        function(a7, [ 9 ]),

        function(a8, [ 4 ]),

        function(a9, [16 ]),

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

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

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

For domain size 28.

Current CPU time: 0.00 seconds (total CPU time: 8.53 seconds).
Ground clauses: seen=22775, kept=22719.
Selections=91, assignments=1367, propagations=9958, current_models=1.
Rewrite_terms=288876, rewrite_bools=32691, indexes=52956.
Rules_from_neg_clauses=231, cross_offs=53701.

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

User_CPU=8.53, System_CPU=0.06, Wall_clock=8.

Exiting with 1 model.

Process 4064 exit (max_models) Sun Mar 17 21:18:27 2013
The process finished Sun Mar 17 21:18:27 2013