============================== Mace4 =================================
Mace4 (32) version Dec-2007, Dec 2007.
Process 4032 was started by Alexei on Alexei-PC,
Sat Mar 16 01:35:47 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 * a5.
a3 = a2 * a6.
a4 = a3 * a7.
a5 = a4 * a1.
a6 = a5 * a8.
a7 = a6 * a4.
a8 = a7 * a3.
a1 = a8 * a2.
end_of_list.

formulas(goals).
a1 = a2 & a2 = a3 & a3 = a4 & a4 = a5 & a5 = a6 & a6 = a7 & a7 = a8.
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 # 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 * a5.
a3 = a2 * a6.
a4 = a3 * a7.
a5 = a4 * a1.
a6 = a5 * a8.
a7 = a6 * a4.
a8 = a7 * a3.
a1 = a8 * a2.
a1 != a2 | a3 != a2 | a4 != a3 | a4 != a5 | a6 != a5 | a7 != a6 | a8 != a7.
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=23, kept=13.
Selections=3, assignments=5, propagations=11, current_models=0.
Rewrite_terms=56, rewrite_bools=17, 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=48, kept=42.
Selections=4, assignments=8, propagations=33, current_models=0.
Rewrite_terms=360, rewrite_bools=88, indexes=28.
Rules_from_neg_clauses=7, cross_offs=20.

============================== 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=93, kept=85.
Selections=7, assignments=19, propagations=56, current_models=0.
Rewrite_terms=894, rewrite_bools=202, indexes=90.
Rules_from_neg_clauses=10, cross_offs=46.

============================== 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=164, kept=154.
Selections=9, assignments=29, propagations=86, current_models=0.
Rewrite_terms=1171, rewrite_bools=201, indexes=155.
Rules_from_neg_clauses=13, cross_offs=112.

============================== 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=267, kept=255.
Selections=9, assignments=30, propagations=128, current_models=0.
Rewrite_terms=1900, rewrite_bools=299, indexes=240.
Rules_from_neg_clauses=17, cross_offs=199.

============================== 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=408, kept=394.
Selections=13, assignments=57, propagations=232, current_models=0.
Rewrite_terms=3887, rewrite_bools=589, indexes=550.
Rules_from_neg_clauses=17, cross_offs=338.

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

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

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

For domain size 8.

Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
Ground clauses: seen=593, kept=577.
Selections=13, assignments=58, propagations=270, current_models=0.
Rewrite_terms=5277, rewrite_bools=752, indexes=761.
Rules_from_neg_clauses=22, cross_offs=529.

============================== 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=828, kept=810.
Selections=18, assignments=101, propagations=550, current_models=0.
Rewrite_terms=11460, rewrite_bools=1771, indexes=1350.
Rules_from_neg_clauses=47, cross_offs=972.

============================== 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=1119, kept=1099.
Selections=19, assignments=111, propagations=659, current_models=0.
Rewrite_terms=15327, rewrite_bools=2435, indexes=1821.
Rules_from_neg_clauses=43, cross_offs=1360.

============================== 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=1472, kept=1450.
Selections=23, assignments=154, propagations=986, current_models=0.
Rewrite_terms=22633, rewrite_bools=3495, indexes=2720.
Rules_from_neg_clauses=55, cross_offs=2026.

============================== 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=1893, kept=1869.
Selections=24, assignments=166, propagations=1217, current_models=0.
Rewrite_terms=32674, rewrite_bools=5261, indexes=3505.
Rules_from_neg_clauses=71, cross_offs=2838.

============================== 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=2388, kept=2362.
Selections=29, assignments=229, propagations=1791, current_models=0.
Rewrite_terms=43715, rewrite_bools=6948, indexes=5094.
Rules_from_neg_clauses=92, cross_offs=3973.

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

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

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

For domain size 14.

Current CPU time: 0.00 seconds (total CPU time: 0.08 seconds).
Ground clauses: seen=2963, kept=2935.
Selections=29, assignments=230, propagations=1885, current_models=0.
Rewrite_terms=53280, rewrite_bools=7976, indexes=6172.
Rules_from_neg_clauses=96, cross_offs=5363.

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

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

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

For domain size 15.

Current CPU time: 0.00 seconds (total CPU time: 0.11 seconds).
Ground clauses: seen=3624, kept=3594.
Selections=32, assignments=274, propagations=2330, current_models=0.
Rewrite_terms=61402, rewrite_bools=8632, indexes=7628.
Rules_from_neg_clauses=105, cross_offs=6957.

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

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

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

For domain size 16.

Current CPU time: 0.00 seconds (total CPU time: 0.14 seconds).
Ground clauses: seen=4377, kept=4345.
Selections=32, assignments=275, propagations=2482, current_models=0.
Rewrite_terms=74482, rewrite_bools=10293, indexes=9033.
Rules_from_neg_clauses=90, cross_offs=8689.

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

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

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

For domain size 17.

Current CPU time: 0.00 seconds (total CPU time: 0.17 seconds).
Ground clauses: seen=5228, kept=5194.
Selections=34, assignments=309, propagations=2901, current_models=0.
Rewrite_terms=86118, rewrite_bools=11031, indexes=10972.
Rules_from_neg_clauses=115, cross_offs=10839.

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

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

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

For domain size 18.

Current CPU time: 0.00 seconds (total CPU time: 0.20 seconds).
Ground clauses: seen=6183, kept=6147.
Selections=34, assignments=310, propagations=3071, current_models=0.
Rewrite_terms=96767, rewrite_bools=12034, indexes=12382.
Rules_from_neg_clauses=117, cross_offs=12675.

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

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

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

For domain size 19.

Current CPU time: 0.00 seconds (total CPU time: 0.28 seconds).
Ground clauses: seen=7248, kept=7210.
Selections=36, assignments=348, propagations=3753, current_models=0.
Rewrite_terms=117905, rewrite_bools=15073, indexes=14984.
Rules_from_neg_clauses=167, cross_offs=15207.

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

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

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

For domain size 20.

Current CPU time: 0.00 seconds (total CPU time: 0.36 seconds).
Ground clauses: seen=8429, kept=8389.
Selections=36, assignments=349, propagations=3879, current_models=0.
Rewrite_terms=145905, rewrite_bools=19552, indexes=17141.
Rules_from_neg_clauses=131, cross_offs=17957.

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

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

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

For domain size 21.

Current CPU time: 0.00 seconds (total CPU time: 0.47 seconds).
Ground clauses: seen=9732, kept=9690.
Selections=38, assignments=391, propagations=4563, current_models=0.
Rewrite_terms=158300, rewrite_bools=19553, indexes=19637.
Rules_from_neg_clauses=186, cross_offs=21031.

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

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

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

For domain size 22.

Current CPU time: 0.00 seconds (total CPU time: 0.58 seconds).
Ground clauses: seen=11163, kept=11119.
Selections=38, assignments=392, propagations=4707, current_models=0.
Rewrite_terms=176419, rewrite_bools=21656, indexes=22012.
Rules_from_neg_clauses=184, cross_offs=24415.

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

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

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

For domain size 23.

Current CPU time: 0.00 seconds (total CPU time: 0.72 seconds).
Ground clauses: seen=12728, kept=12682.
Selections=39, assignments=415, propagations=5026, current_models=0.
Rewrite_terms=192417, rewrite_bools=23675, indexes=24899.
Rules_from_neg_clauses=137, cross_offs=27783.

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

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

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

For domain size 24.

Current CPU time: 0.00 seconds (total CPU time: 0.88 seconds).
Ground clauses: seen=14433, kept=14385.
Selections=39, assignments=415, propagations=5125, current_models=0.
Rewrite_terms=213641, rewrite_bools=26824, indexes=27435.
Rules_from_neg_clauses=137, cross_offs=30872.

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

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

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

For domain size 25.

Current CPU time: 0.00 seconds (total CPU time: 1.08 seconds).
Ground clauses: seen=16284, kept=16234.
Selections=40, assignments=439, propagations=5699, current_models=0.
Rewrite_terms=239822, rewrite_bools=29756, indexes=31211.
Rules_from_neg_clauses=204, cross_offs=34396.

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

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

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

For domain size 26.

Current CPU time: 0.00 seconds (total CPU time: 1.30 seconds).
Ground clauses: seen=18287, kept=18235.
Selections=41, assignments=464, propagations=6145, current_models=0.
Rewrite_terms=255015, rewrite_bools=31354, indexes=33983.
Rules_from_neg_clauses=193, cross_offs=36852.

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

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

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

For domain size 27.

Current CPU time: 0.00 seconds (total CPU time: 1.53 seconds).
Ground clauses: seen=20448, kept=20394.
Selections=42, assignments=490, propagations=6664, current_models=0.
Rewrite_terms=272154, rewrite_bools=33519, indexes=36794.
Rules_from_neg_clauses=189, cross_offs=39332.

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

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

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

For domain size 28.

Current CPU time: 0.00 seconds (total CPU time: 1.80 seconds).
Ground clauses: seen=22773, kept=22717.
Selections=43, assignments=517, propagations=7313, current_models=0.
Rewrite_terms=291632, rewrite_bools=36552, indexes=39568.
Rules_from_neg_clauses=174, cross_offs=41868.

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

============================== DOMAIN SIZE 29 ========================

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

interpretation( 29, [number=1, seconds=2], [

        function(a1, [ 0 ]),

        function(a2, [ 1 ]),

        function(a3, [22 ]),

        function(a4, [ 3 ]),

        function(a5, [ 2 ]),

        function(a6, [14 ]),

        function(a7, [20 ]),

        function(a8, [ 5 ]),

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

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

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

For domain size 29.

Current CPU time: 0.00 seconds (total CPU time: 2.11 seconds).
Ground clauses: seen=25268, kept=25210.
Selections=44, assignments=545, propagations=8065, current_models=1.
Rewrite_terms=342352, rewrite_bools=49934, indexes=42358.
Rules_from_neg_clauses=160, cross_offs=44506.

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

User_CPU=2.11, System_CPU=0.01, Wall_clock=2.

Exiting with 1 model.

Process 4032 exit (max_models) Sat Mar 16 01:35:49 2013
The process finished Sat Mar 16 01:35:49 2013