============================== Mace4 =================================
Mace4 (32) version Dec-2007, Dec 2007.
Process 2480 was started by Alexei on Alexei-PC,
Sat Mar 16 02:11:17 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 * a6.
a3 = a2 * a8.
a4 = a3 * a9.
a5 = a4 * a7.
a6 = a5 * a1.
a7 = a6 * a5.
a8 = a7 * a4.
a9 = a8 * a3.
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 * a6.
a3 = a2 * a8.
a4 = a3 * a9.
a5 = a4 * a7.
a6 = a5 * a1.
a7 = a6 * a5.
a8 = a7 * a4.
a9 = a8 * a3.
a1 = a9 * a2.
a1 != a2 | a3 != a2 | a4 != a3 | a5 != a4 | a5 != a6 | a7 != a6 | a7 != a8 | a9 != a8.
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=24, kept=14.
Selections=3, assignments=5, propagations=13, current_models=0.
Rewrite_terms=63, rewrite_bools=19, 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=49, kept=43.
Selections=4, assignments=8, propagations=41, current_models=0.
Rewrite_terms=407, rewrite_bools=93, indexes=33.
Rules_from_neg_clauses=11, cross_offs=29.

============================== 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=94, kept=86.
Selections=6, assignments=15, propagations=64, current_models=0.
Rewrite_terms=907, rewrite_bools=196, indexes=93.
Rules_from_neg_clauses=16, cross_offs=63.

============================== 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=165, kept=155.
Selections=9, assignments=30, propagations=109, current_models=0.
Rewrite_terms=1469, rewrite_bools=257, indexes=188.
Rules_from_neg_clauses=23, cross_offs=145.

============================== 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=268, kept=256.
Selections=9, assignments=31, propagations=166, current_models=0.
Rewrite_terms=2679, rewrite_bools=463, indexes=302.
Rules_from_neg_clauses=36, cross_offs=295.

============================== 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=409, kept=395.
Selections=14, assignments=64, propagations=297, current_models=0.
Rewrite_terms=5399, rewrite_bools=908, indexes=729.
Rules_from_neg_clauses=37, cross_offs=491.

============================== 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=594, kept=578.
Selections=14, assignments=65, propagations=325, current_models=0.
Rewrite_terms=7431, rewrite_bools=1280, indexes=921.
Rules_from_neg_clauses=40, cross_offs=759.

============================== 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=829, kept=811.
Selections=19, assignments=108, propagations=600, current_models=0.
Rewrite_terms=15201, rewrite_bools=2923, indexes=1613.
Rules_from_neg_clauses=67, cross_offs=1333.

============================== 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=20, assignments=118, propagations=610, current_models=0.
Rewrite_terms=14679, rewrite_bools=2362, indexes=2046.
Rules_from_neg_clauses=54, cross_offs=1768.

============================== 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=1473, kept=1451.
Selections=23, assignments=150, propagations=857, current_models=0.
Rewrite_terms=22167, rewrite_bools=3412, indexes=2799.
Rules_from_neg_clauses=74, cross_offs=2653.

============================== 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=1894, kept=1870.
Selections=23, assignments=151, propagations=957, current_models=0.
Rewrite_terms=26574, rewrite_bools=4027, indexes=3409.
Rules_from_neg_clauses=84, cross_offs=3320.

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

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

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

For domain size 13.

Current CPU time: 0.00 seconds (total CPU time: 0.05 seconds).
Ground clauses: seen=2389, kept=2363.
Selections=27, assignments=202, propagations=1376, current_models=0.
Rewrite_terms=30747, rewrite_bools=4211, indexes=4424.
Rules_from_neg_clauses=234, cross_offs=4639.

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

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

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

For domain size 14.

Current CPU time: 0.00 seconds (total CPU time: 0.06 seconds).
Ground clauses: seen=2964, kept=2936.
Selections=27, assignments=203, propagations=1369, current_models=0.
Rewrite_terms=39347, rewrite_bools=5438, indexes=5181.
Rules_from_neg_clauses=102, cross_offs=5514.

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

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

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

For domain size 15.

Current CPU time: 0.00 seconds (total CPU time: 0.08 seconds).
Ground clauses: seen=3625, kept=3595.
Selections=31, assignments=262, propagations=1879, current_models=0.
Rewrite_terms=48510, rewrite_bools=6300, indexes=6740.
Rules_from_neg_clauses=190, cross_offs=7073.

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

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

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

For domain size 16.

Current CPU time: 0.00 seconds (total CPU time: 0.11 seconds).
Ground clauses: seen=4378, kept=4346.
Selections=31, assignments=263, propagations=1998, current_models=0.
Rewrite_terms=61946, rewrite_bools=8267, indexes=7996.
Rules_from_neg_clauses=113, cross_offs=8291.

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

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

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

For domain size 17.

Current CPU time: 0.00 seconds (total CPU time: 0.14 seconds).
Ground clauses: seen=5229, kept=5195.
Selections=34, assignments=314, propagations=2418, current_models=0.
Rewrite_terms=73967, rewrite_bools=9609, indexes=9646.
Rules_from_neg_clauses=155, cross_offs=10319.

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

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

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

For domain size 18.

Current CPU time: 0.00 seconds (total CPU time: 0.19 seconds).
Ground clauses: seen=6184, kept=6148.
Selections=34, assignments=315, propagations=2642, current_models=0.
Rewrite_terms=88586, rewrite_bools=11363, indexes=11022.
Rules_from_neg_clauses=141, cross_offs=12134.

============================== 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=36, assignments=352, propagations=2952, current_models=0.
Rewrite_terms=98151, rewrite_bools=12608, indexes=13311.
Rules_from_neg_clauses=114, cross_offs=14501.

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

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

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

For domain size 20.

Current CPU time: 0.00 seconds (total CPU time: 0.31 seconds).
Ground clauses: seen=8430, kept=8390.
Selections=36, assignments=352, propagations=2951, current_models=0.
Rewrite_terms=109892, rewrite_bools=14244, indexes=14783.
Rules_from_neg_clauses=100, cross_offs=16309.

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

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

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

For domain size 21.

Current CPU time: 0.00 seconds (total CPU time: 0.38 seconds).
Ground clauses: seen=9733, kept=9691.
Selections=37, assignments=372, propagations=2998, current_models=0.
Rewrite_terms=114272, rewrite_bools=14344, indexes=16150.
Rules_from_neg_clauses=115, cross_offs=17802.

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

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

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

For domain size 22.

Current CPU time: 0.00 seconds (total CPU time: 0.47 seconds).
Ground clauses: seen=11164, kept=11120.
Selections=38, assignments=393, propagations=3363, current_models=0.
Rewrite_terms=126789, rewrite_bools=15159, indexes=18553.
Rules_from_neg_clauses=166, cross_offs=20402.

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

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

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

For domain size 23.

Current CPU time: 0.00 seconds (total CPU time: 0.56 seconds).
Ground clauses: seen=12729, kept=12683.
Selections=39, assignments=415, propagations=3711, current_models=0.
Rewrite_terms=136472, rewrite_bools=15852, indexes=20532.
Rules_from_neg_clauses=177, cross_offs=22226.

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

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

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

For domain size 24.

Current CPU time: 0.00 seconds (total CPU time: 0.67 seconds).
Ground clauses: seen=14434, kept=14386.
Selections=40, assignments=438, propagations=4015, current_models=0.
Rewrite_terms=147208, rewrite_bools=16858, indexes=22560.
Rules_from_neg_clauses=185, cross_offs=24090.

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

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

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

For domain size 25.

Current CPU time: 0.00 seconds (total CPU time: 0.80 seconds).
Ground clauses: seen=16285, kept=16235.
Selections=41, assignments=462, propagations=4522, current_models=0.
Rewrite_terms=159409, rewrite_bools=18178, indexes=24672.
Rules_from_neg_clauses=194, cross_offs=25993.

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

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

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

For domain size 26.

Current CPU time: 0.00 seconds (total CPU time: 0.94 seconds).
Ground clauses: seen=18288, kept=18236.
Selections=42, assignments=487, propagations=4983, current_models=0.
Rewrite_terms=173024, rewrite_bools=19893, indexes=26807.
Rules_from_neg_clauses=185, cross_offs=27875.

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

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

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

For domain size 27.

Current CPU time: 0.00 seconds (total CPU time: 1.11 seconds).
Ground clauses: seen=20449, kept=20395.
Selections=43, assignments=513, propagations=5530, current_models=0.
Rewrite_terms=188147, rewrite_bools=22092, indexes=28966.
Rules_from_neg_clauses=178, cross_offs=29748.

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

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

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

For domain size 28.

Current CPU time: 0.00 seconds (total CPU time: 1.30 seconds).
Ground clauses: seen=22774, kept=22718.
Selections=44, assignments=540, propagations=6114, current_models=0.
Rewrite_terms=205044, rewrite_bools=24812, indexes=31143.
Rules_from_neg_clauses=164, cross_offs=31658.

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

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

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

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

        function(a1, [ 0 ]),

        function(a2, [ 1 ]),

        function(a3, [19 ]),

        function(a4, [ 9 ]),

        function(a5, [ 3 ]),

        function(a6, [ 2 ]),

        function(a7, [ 8 ]),

        function(a8, [18 ]),

        function(a9, [ 5 ]),

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

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

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

For domain size 29.

Current CPU time: 0.00 seconds (total CPU time: 1.53 seconds).
Ground clauses: seen=25269, kept=25211.
Selections=45, assignments=568, propagations=6869, current_models=1.
Rewrite_terms=254216, rewrite_bools=38393, indexes=33275.
Rules_from_neg_clauses=149, cross_offs=33643.

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

User_CPU=1.53, System_CPU=0.00, Wall_clock=1.

Exiting with 1 model.

Process 2480 exit (max_models) Sat Mar 16 02:11:18 2013
The process finished Sat Mar 16 02:11:18 2013