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

formulas(goals).
a1 = a2 & a2 = a3 & a3 = a4 & a4 = a5 & a5 = a6 & a6 = a7 & a7 = a8 & a8 = a9.
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 # 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 * a9.
a6 = a5 * a8.
a7 = a6 * a3.
a8 = a7 * a6.
a9 = a8 * a5.
a1 = a9 * a2.
a1 != a2 | a3 != a2 | a3 != a4 | a5 != a4 | a6 != a5 | a6 != a7 | a8 != a7 | a8 != 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=24, kept=14.
Selections=3, assignments=5, propagations=13, current_models=0.
Rewrite_terms=63, rewrite_bools=19, 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.00 seconds).
Ground clauses: seen=49, kept=43.
Selections=5, assignments=11, propagations=36, current_models=0.
Rewrite_terms=316, rewrite_bools=65, indexes=28.
Rules_from_neg_clauses=11, cross_offs=30.

============================== 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=94, kept=86.
Selections=7, assignments=19, propagations=60, current_models=0.
Rewrite_terms=791, rewrite_bools=160, indexes=92.
Rules_from_neg_clauses=13, cross_offs=64.

============================== 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=165, kept=155.
Selections=8, assignments=24, propagations=86, current_models=0.
Rewrite_terms=1321, rewrite_bools=246, indexes=152.
Rules_from_neg_clauses=12, cross_offs=128.

============================== 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=268, kept=256.
Selections=9, assignments=30, propagations=129, current_models=0.
Rewrite_terms=2514, rewrite_bools=460, indexes=322.
Rules_from_neg_clauses=25, cross_offs=235.

============================== 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=409, kept=395.
Selections=12, assignments=50, propagations=221, current_models=0.
Rewrite_terms=3787, rewrite_bools=522, indexes=562.
Rules_from_neg_clauses=32, cross_offs=473.

============================== 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=594, kept=578.
Selections=14, assignments=66, propagations=324, current_models=0.
Rewrite_terms=6334, rewrite_bools=884, indexes=979.
Rules_from_neg_clauses=48, cross_offs=848.

============================== 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=829, kept=811.
Selections=16, assignments=85, propagations=458, current_models=0.
Rewrite_terms=9781, rewrite_bools=1335, indexes=1534.
Rules_from_neg_clauses=65, cross_offs=1420.

============================== 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=1120, kept=1100.
Selections=16, assignments=86, propagations=524, current_models=0.
Rewrite_terms=11952, rewrite_bools=1468, indexes=2034.
Rules_from_neg_clauses=65, cross_offs=2196.

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

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

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

For domain size 11.

Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
Ground clauses: seen=1473, kept=1451.
Selections=21, assignments=140, propagations=803, current_models=0.
Rewrite_terms=20378, rewrite_bools=2450, indexes=3240.
Rules_from_neg_clauses=76, cross_offs=3392.

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

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

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

For domain size 12.

Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
Ground clauses: seen=1894, kept=1870.
Selections=22, assignments=153, propagations=1015, current_models=0.
Rewrite_terms=24114, rewrite_bools=2598, indexes=4180.
Rules_from_neg_clauses=99, cross_offs=4367.

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

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

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

For domain size 13.

Current CPU time: 0.00 seconds (total CPU time: 0.03 seconds).
Ground clauses: seen=2389, kept=2363.
Selections=25, assignments=191, propagations=1320, current_models=0.
Rewrite_terms=32314, rewrite_bools=3352, indexes=5517.
Rules_from_neg_clauses=107, cross_offs=5955.

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

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

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

For domain size 14.

Current CPU time: 0.00 seconds (total CPU time: 0.05 seconds).
Ground clauses: seen=2964, kept=2936.
Selections=27, assignments=219, propagations=1586, current_models=0.
Rewrite_terms=39326, rewrite_bools=3813, indexes=7093.
Rules_from_neg_clauses=123, cross_offs=7481.

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

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

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

For domain size 15.

Current CPU time: 0.00 seconds (total CPU time: 0.06 seconds).
Ground clauses: seen=3625, kept=3595.
Selections=29, assignments=249, propagations=1946, current_models=0.
Rewrite_terms=53022, rewrite_bools=5094, indexes=9192.
Rules_from_neg_clauses=130, cross_offs=9330.

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

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

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

For domain size 16.

Current CPU time: 0.00 seconds (total CPU time: 0.09 seconds).
Ground clauses: seen=4378, kept=4346.
Selections=31, assignments=281, propagations=2422, current_models=0.
Rewrite_terms=71038, rewrite_bools=7076, indexes=11626.
Rules_from_neg_clauses=146, cross_offs=11794.

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

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

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

For domain size 17.

Current CPU time: 0.00 seconds (total CPU time: 0.12 seconds).
Ground clauses: seen=5229, kept=5195.
Selections=32, assignments=298, propagations=2659, current_models=0.
Rewrite_terms=75995, rewrite_bools=7044, indexes=13465.
Rules_from_neg_clauses=159, cross_offs=14155.

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

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

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

For domain size 18.

Current CPU time: 0.00 seconds (total CPU time: 0.17 seconds).
Ground clauses: seen=6184, kept=6148.
Selections=34, assignments=333, propagations=2951, current_models=0.
Rewrite_terms=98770, rewrite_bools=10182, indexes=16728.
Rules_from_neg_clauses=173, cross_offs=16876.

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

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

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

For domain size 19.

Current CPU time: 0.00 seconds (total CPU time: 0.25 seconds).
Ground clauses: seen=7249, kept=7211.
Selections=38, assignments=407, propagations=3718, current_models=0.
Rewrite_terms=124878, rewrite_bools=12981, indexes=20289.
Rules_from_neg_clauses=231, cross_offs=21714.

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

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

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

For domain size 20.

Current CPU time: 0.00 seconds (total CPU time: 0.34 seconds).
Ground clauses: seen=8430, kept=8390.
Selections=41, assignments=465, propagations=4748, current_models=0.
Rewrite_terms=177039, rewrite_bools=21162, indexes=25377.
Rules_from_neg_clauses=340, cross_offs=27620.

============================== 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=9733, kept=9691.
Selections=45, assignments=547, propagations=5378, current_models=0.
Rewrite_terms=202000, rewrite_bools=22836, indexes=30082.
Rules_from_neg_clauses=287, cross_offs=34488.

============================== 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=11164, kept=11120.
Selections=45, assignments=548, propagations=5274, current_models=0.
Rewrite_terms=189709, rewrite_bools=17365, indexes=32175.
Rules_from_neg_clauses=219, cross_offs=38021.

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

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

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

For domain size 23.

Current CPU time: 0.00 seconds (total CPU time: 0.75 seconds).
Ground clauses: seen=12729, kept=12683.
Selections=47, assignments=594, propagations=6020, current_models=0.
Rewrite_terms=243334, rewrite_bools=23318, indexes=38136.
Rules_from_neg_clauses=280, cross_offs=45307.

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

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

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

For domain size 24.

Current CPU time: 0.00 seconds (total CPU time: 0.95 seconds).
Ground clauses: seen=14434, kept=14386.
Selections=47, assignments=595, propagations=6575, current_models=0.
Rewrite_terms=289114, rewrite_bools=28951, indexes=43154.
Rules_from_neg_clauses=342, cross_offs=51874.

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

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

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

For domain size 25.

Current CPU time: 0.00 seconds (total CPU time: 1.25 seconds).
Ground clauses: seen=16285, kept=16235.
Selections=50, assignments=669, propagations=7627, current_models=0.
Rewrite_terms=395390, rewrite_bools=48639, indexes=50818.
Rules_from_neg_clauses=411, cross_offs=63905.

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

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

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

For domain size 26.

Current CPU time: 0.00 seconds (total CPU time: 1.55 seconds).
Ground clauses: seen=18288, kept=18236.
Selections=50, assignments=670, propagations=7418, current_models=0.
Rewrite_terms=388733, rewrite_bools=46132, indexes=55583.
Rules_from_neg_clauses=297, cross_offs=68827.

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

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

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

For domain size 27.

Current CPU time: 0.00 seconds (total CPU time: 1.89 seconds).
Ground clauses: seen=20449, kept=20395.
Selections=50, assignments=670, propagations=7486, current_models=0.
Rewrite_terms=398375, rewrite_bools=45613, indexes=58821.
Rules_from_neg_clauses=322, cross_offs=74865.

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

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

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

For domain size 28.

Current CPU time: 0.00 seconds (total CPU time: 2.28 seconds).
Ground clauses: seen=22774, kept=22718.
Selections=51, assignments=697, propagations=8317, current_models=0.
Rewrite_terms=456088, rewrite_bools=53414, indexes=66275.
Rules_from_neg_clauses=400, cross_offs=80856.

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

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

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

For domain size 29.

Current CPU time: 0.00 seconds (total CPU time: 2.72 seconds).
Ground clauses: seen=25269, kept=25211.
Selections=52, assignments=725, propagations=8961, current_models=0.
Rewrite_terms=479706, rewrite_bools=56108, indexes=70689.
Rules_from_neg_clauses=389, cross_offs=85029.

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

============================== DOMAIN SIZE 30 ========================

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

For domain size 30.

Current CPU time: 0.00 seconds (total CPU time: 3.20 seconds).
Ground clauses: seen=27940, kept=27880.
Selections=53, assignments=754, propagations=9709, current_models=0.
Rewrite_terms=505574, rewrite_bools=59475, indexes=75125.
Rules_from_neg_clauses=373, cross_offs=89226.

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

============================== DOMAIN SIZE 31 ========================

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

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

        function(a1, [ 0 ]),

        function(a2, [ 1 ]),

        function(a3, [ 3 ]),

        function(a4, [ 2 ]),

        function(a5, [22 ]),

        function(a6, [ 7 ]),

        function(a7, [ 4 ]),

        function(a8, [25 ]),

        function(a9, [ 9 ]),

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

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

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

For domain size 31.

Current CPU time: 0.00 seconds (total CPU time: 3.77 seconds).
Ground clauses: seen=30793, kept=30731.
Selections=54, assignments=784, propagations=10537, current_models=1.
Rewrite_terms=567532, rewrite_bools=75002, indexes=79503.
Rules_from_neg_clauses=355, cross_offs=93487.

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

User_CPU=3.77, System_CPU=0.00, Wall_clock=3.

Exiting with 1 model.

Process 288 exit (max_models) Sat Mar 16 02:14:22 2013
The process finished Sat Mar 16 02:14:22 2013