============================== Mace4 =================================
Mace4 (32) version Dec-2007, Dec 2007.
Process 1864 was started by Alexei on Alexei-PC,
Sun Mar 17 09:33:22 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 * a10.
a3 = a2 * a8.
a4 = a3 * a5.
a5 = a4 * a1.
a6 = a5 * a3.
a7 = a6 * a9.
a8 = a7 * a2.
a9 = a8 * a7.
a10 = a9 * a6.
a1 = a10 * a4.
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 * a10.
a3 = a2 * a8.
a4 = a3 * a5.
a5 = a4 * a1.
a6 = a5 * a3.
a7 = a6 * a9.
a8 = a7 * a2.
a9 = a8 * a7.
a10 = a9 * a6.
a1 = a10 * a4.
a1 != a2 | a3 != a2 | a4 != a3 | a5 != a4 | a6 != a5 | 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.00 seconds).
Ground clauses: seen=25, kept=15.
Selections=4, assignments=7, propagations=14, current_models=0.
Rewrite_terms=80, rewrite_bools=24, indexes=0.
Rules_from_neg_clauses=5, cross_offs=5.

============================== 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=50, kept=44.
Selections=6, assignments=13, propagations=54, current_models=0.
Rewrite_terms=512, rewrite_bools=117, indexes=38.
Rules_from_neg_clauses=15, cross_offs=36.

============================== 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=95, kept=87.
Selections=10, assignments=28, propagations=86, current_models=0.
Rewrite_terms=1131, rewrite_bools=244, indexes=120.
Rules_from_neg_clauses=16, cross_offs=79.

============================== 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=166, kept=156.
Selections=13, assignments=43, propagations=122, current_models=0.
Rewrite_terms=1754, rewrite_bools=308, indexes=226.
Rules_from_neg_clauses=20, cross_offs=171.

============================== 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=269, kept=257.
Selections=14, assignments=49, propagations=185, current_models=0.
Rewrite_terms=3555, rewrite_bools=650, indexes=408.
Rules_from_neg_clauses=31, cross_offs=330.

============================== 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=410, kept=396.
Selections=19, assignments=82, propagations=288, current_models=0.
Rewrite_terms=5123, rewrite_bools=828, indexes=753.
Rules_from_neg_clauses=43, cross_offs=556.

============================== 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=595, kept=579.
Selections=20, assignments=90, propagations=353, current_models=0.
Rewrite_terms=6908, rewrite_bools=1088, indexes=1028.
Rules_from_neg_clauses=33, cross_offs=864.

============================== 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=830, kept=812.
Selections=22, assignments=107, propagations=446, current_models=0.
Rewrite_terms=9931, rewrite_bools=1495, indexes=1371.
Rules_from_neg_clauses=37, cross_offs=1220.

============================== 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=1121, kept=1101.
Selections=23, assignments=117, propagations=498, current_models=0.
Rewrite_terms=12338, rewrite_bools=1749, indexes=1833.
Rules_from_neg_clauses=43, cross_offs=1648.

============================== 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=1474, kept=1452.
Selections=27, assignments=160, propagations=779, current_models=0.
Rewrite_terms=21154, rewrite_bools=2840, indexes=3016.
Rules_from_neg_clauses=71, cross_offs=2753.

============================== 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=1895, kept=1871.
Selections=28, assignments=172, propagations=959, current_models=0.
Rewrite_terms=25315, rewrite_bools=2962, indexes=3938.
Rules_from_neg_clauses=87, cross_offs=3861.

============================== 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=2390, kept=2364.
Selections=34, assignments=246, propagations=1620, current_models=0.
Rewrite_terms=42999, rewrite_bools=5862, indexes=5958.
Rules_from_neg_clauses=115, cross_offs=5741.

============================== 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=2965, kept=2937.
Selections=38, assignments=300, propagations=2014, current_models=0.
Rewrite_terms=51252, rewrite_bools=5999, indexes=7925.
Rules_from_neg_clauses=120, cross_offs=7723.

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

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

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

For domain size 15.

Current CPU time: 0.00 seconds (total CPU time: 0.09 seconds).
Ground clauses: seen=3626, kept=3596.
Selections=42, assignments=358, propagations=2825, current_models=0.
Rewrite_terms=79520, rewrite_bools=10246, indexes=10626.
Rules_from_neg_clauses=185, cross_offs=10966.

============================== 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=4379, kept=4347.
Selections=47, assignments=435, propagations=3509, current_models=0.
Rewrite_terms=106835, rewrite_bools=14885, indexes=13962.
Rules_from_neg_clauses=190, cross_offs=14528.

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

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

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

For domain size 17.

Current CPU time: 0.00 seconds (total CPU time: 0.20 seconds).
Ground clauses: seen=5230, kept=5196.
Selections=49, assignments=469, propagations=3991, current_models=0.
Rewrite_terms=131494, rewrite_bools=18326, indexes=16667.
Rules_from_neg_clauses=164, cross_offs=18161.

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

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

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

For domain size 18.

Current CPU time: 0.00 seconds (total CPU time: 0.27 seconds).
Ground clauses: seen=6185, kept=6149.
Selections=50, assignments=487, propagations=4176, current_models=0.
Rewrite_terms=147515, rewrite_bools=20367, indexes=19063.
Rules_from_neg_clauses=168, cross_offs=21450.

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

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

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

For domain size 19.

Current CPU time: 0.00 seconds (total CPU time: 0.38 seconds).
Ground clauses: seen=7250, kept=7212.
Selections=55, assignments=580, propagations=5118, current_models=0.
Rewrite_terms=184852, rewrite_bools=25124, indexes=23556.
Rules_from_neg_clauses=240, cross_offs=26664.

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

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

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

For domain size 20.

Current CPU time: 0.00 seconds (total CPU time: 0.48 seconds).
Ground clauses: seen=8431, kept=8391.
Selections=55, assignments=581, propagations=5329, current_models=0.
Rewrite_terms=206636, rewrite_bools=27315, indexes=26832.
Rules_from_neg_clauses=222, cross_offs=30891.

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

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

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

For domain size 21.

Current CPU time: 0.00 seconds (total CPU time: 0.64 seconds).
Ground clauses: seen=9734, kept=9692.
Selections=59, assignments=664, propagations=6296, current_models=0.
Rewrite_terms=250745, rewrite_bools=33927, indexes=32203.
Rules_from_neg_clauses=247, cross_offs=37014.

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

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

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

For domain size 22.

Current CPU time: 0.00 seconds (total CPU time: 0.81 seconds).
Ground clauses: seen=11165, kept=11121.
Selections=60, assignments=686, propagations=6706, current_models=0.
Rewrite_terms=274660, rewrite_bools=36376, indexes=35924.
Rules_from_neg_clauses=283, cross_offs=42457.

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

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

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

For domain size 23.

Current CPU time: 0.00 seconds (total CPU time: 1.03 seconds).
Ground clauses: seen=12730, kept=12684.
Selections=63, assignments=754, propagations=8040, current_models=0.
Rewrite_terms=325568, rewrite_bools=41323, indexes=41848.
Rules_from_neg_clauses=323, cross_offs=49371.

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

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

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

For domain size 24.

Current CPU time: 0.00 seconds (total CPU time: 1.31 seconds).
Ground clauses: seen=14435, kept=14387.
Selections=63, assignments=755, propagations=8499, current_models=0.
Rewrite_terms=380171, rewrite_bools=50521, indexes=46798.
Rules_from_neg_clauses=360, cross_offs=57026.

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

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

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

For domain size 25.

Current CPU time: 0.00 seconds (total CPU time: 1.62 seconds).
Ground clauses: seen=16286, kept=16236.
Selections=65, assignments=805, propagations=9414, current_models=0.
Rewrite_terms=422800, rewrite_bools=54692, indexes=53399.
Rules_from_neg_clauses=398, cross_offs=68703.

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

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

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

For domain size 26.

Current CPU time: 0.00 seconds (total CPU time: 1.97 seconds).
Ground clauses: seen=18289, kept=18237.
Selections=66, assignments=831, propagations=9916, current_models=0.
Rewrite_terms=450446, rewrite_bools=56686, indexes=58454.
Rules_from_neg_clauses=407, cross_offs=78001.

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

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

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

For domain size 27.

Current CPU time: 0.00 seconds (total CPU time: 2.44 seconds).
Ground clauses: seen=20450, kept=20396.
Selections=69, assignments=910, propagations=10297, current_models=0.
Rewrite_terms=541408, rewrite_bools=74853, indexes=64751.
Rules_from_neg_clauses=446, cross_offs=86468.

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

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

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

For domain size 28.

Current CPU time: 0.00 seconds (total CPU time: 2.92 seconds).
Ground clauses: seen=22775, kept=22719.
Selections=69, assignments=910, propagations=10195, current_models=0.
Rewrite_terms=555924, rewrite_bools=74897, indexes=69153.
Rules_from_neg_clauses=335, cross_offs=93098.

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

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

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

For domain size 29.

Current CPU time: 0.00 seconds (total CPU time: 3.44 seconds).
Ground clauses: seen=25270, kept=25212.
Selections=70, assignments=938, propagations=10439, current_models=0.
Rewrite_terms=582915, rewrite_bools=76048, indexes=76109.
Rules_from_neg_clauses=374, cross_offs=101287.

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

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

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

For domain size 30.

Current CPU time: 0.00 seconds (total CPU time: 4.00 seconds).
Ground clauses: seen=27941, kept=27881.
Selections=71, assignments=967, propagations=10730, current_models=0.
Rewrite_terms=602517, rewrite_bools=76485, indexes=81502.
Rules_from_neg_clauses=379, cross_offs=106797.

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

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

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

For domain size 31.

Current CPU time: 0.00 seconds (total CPU time: 4.59 seconds).
Ground clauses: seen=30794, kept=30732.
Selections=72, assignments=997, propagations=11036, current_models=0.
Rewrite_terms=623993, rewrite_bools=77255, indexes=87098.
Rules_from_neg_clauses=418, cross_offs=112325.

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

============================== DOMAIN SIZE 32 ========================

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

For domain size 32.

Current CPU time: 0.00 seconds (total CPU time: 5.23 seconds).
Ground clauses: seen=33835, kept=33771.
Selections=73, assignments=1028, propagations=11294, current_models=0.
Rewrite_terms=644495, rewrite_bools=77759, indexes=92615.
Rules_from_neg_clauses=396, cross_offs=118125.

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

============================== DOMAIN SIZE 33 ========================

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

For domain size 33.

Current CPU time: 0.00 seconds (total CPU time: 5.92 seconds).
Ground clauses: seen=37070, kept=37004.
Selections=74, assignments=1060, propagations=11651, current_models=0.
Rewrite_terms=667158, rewrite_bools=78520, indexes=98477.
Rules_from_neg_clauses=408, cross_offs=123955.

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

============================== DOMAIN SIZE 34 ========================

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

For domain size 34.

Current CPU time: 0.00 seconds (total CPU time: 6.66 seconds).
Ground clauses: seen=40505, kept=40437.
Selections=75, assignments=1093, propagations=12023, current_models=0.
Rewrite_terms=691342, rewrite_bools=79598, indexes=104484.
Rules_from_neg_clauses=447, cross_offs=129804.

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

============================== DOMAIN SIZE 35 ========================

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

For domain size 35.

Current CPU time: 0.00 seconds (total CPU time: 7.45 seconds).
Ground clauses: seen=44146, kept=44076.
Selections=76, assignments=1127, propagations=12610, current_models=0.
Rewrite_terms=715606, rewrite_bools=80468, indexes=110598.
Rules_from_neg_clauses=474, cross_offs=136011.

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

============================== DOMAIN SIZE 36 ========================

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

For domain size 36.

Current CPU time: 0.00 seconds (total CPU time: 8.28 seconds).
Ground clauses: seen=47999, kept=47927.
Selections=77, assignments=1162, propagations=13117, current_models=0.
Rewrite_terms=741908, rewrite_bools=81678, indexes=116946.
Rules_from_neg_clauses=535, cross_offs=142366.

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

============================== DOMAIN SIZE 37 ========================

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

For domain size 37.

Current CPU time: 0.00 seconds (total CPU time: 9.19 seconds).
Ground clauses: seen=52070, kept=51996.
Selections=78, assignments=1198, propagations=13671, current_models=0.
Rewrite_terms=769244, rewrite_bools=83012, indexes=123439.
Rules_from_neg_clauses=528, cross_offs=148722.

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

============================== DOMAIN SIZE 38 ========================

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

For domain size 38.

Current CPU time: 0.00 seconds (total CPU time: 10.14 seconds).
Ground clauses: seen=56365, kept=56289.
Selections=79, assignments=1235, propagations=14262, current_models=0.
Rewrite_terms=798312, rewrite_bools=84621, indexes=130164.
Rules_from_neg_clauses=511, cross_offs=155111.

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

============================== DOMAIN SIZE 39 ========================

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

For domain size 39.

Current CPU time: 0.00 seconds (total CPU time: 11.17 seconds).
Ground clauses: seen=60890, kept=60812.
Selections=80, assignments=1273, propagations=14948, current_models=0.
Rewrite_terms=830208, rewrite_bools=86993, indexes=137035.
Rules_from_neg_clauses=522, cross_offs=161475.

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

============================== DOMAIN SIZE 40 ========================

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

For domain size 40.

Current CPU time: 0.00 seconds (total CPU time: 12.25 seconds).
Ground clauses: seen=65651, kept=65571.
Selections=81, assignments=1312, propagations=15958, current_models=0.
Rewrite_terms=862697, rewrite_bools=89143, indexes=144052.
Rules_from_neg_clauses=549, cross_offs=168034.

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

============================== DOMAIN SIZE 41 ========================

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

For domain size 41.

Current CPU time: 0.00 seconds (total CPU time: 13.41 seconds).
Ground clauses: seen=70654, kept=70572.
Selections=82, assignments=1352, propagations=17009, current_models=0.
Rewrite_terms=897793, rewrite_bools=91902, indexes=151165.
Rules_from_neg_clauses=586, cross_offs=174815.

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

============================== DOMAIN SIZE 42 ========================

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

For domain size 42.

Current CPU time: 0.00 seconds (total CPU time: 14.67 seconds).
Ground clauses: seen=75905, kept=75821.
Selections=83, assignments=1393, propagations=18068, current_models=0.
Rewrite_terms=934226, rewrite_bools=95068, indexes=158429.
Rules_from_neg_clauses=512, cross_offs=181480.

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

============================== DOMAIN SIZE 43 ========================

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

For domain size 43.

Current CPU time: 0.00 seconds (total CPU time: 16.02 seconds).
Ground clauses: seen=81410, kept=81324.
Selections=84, assignments=1435, propagations=19321, current_models=0.
Rewrite_terms=973820, rewrite_bools=99192, indexes=165784.
Rules_from_neg_clauses=631, cross_offs=188162.

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

============================== DOMAIN SIZE 44 ========================

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

For domain size 44.

Current CPU time: 0.00 seconds (total CPU time: 17.48 seconds).
Ground clauses: seen=87175, kept=87087.
Selections=85, assignments=1478, propagations=20681, current_models=0.
Rewrite_terms=1015429, rewrite_bools=103566, indexes=173253.
Rules_from_neg_clauses=629, cross_offs=195213.

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

============================== DOMAIN SIZE 45 ========================

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

For domain size 45.

Current CPU time: 0.00 seconds (total CPU time: 19.05 seconds).
Ground clauses: seen=93206, kept=93116.
Selections=86, assignments=1522, propagations=22114, current_models=0.
Rewrite_terms=1059895, rewrite_bools=108702, indexes=180781.
Rules_from_neg_clauses=648, cross_offs=202127.

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

============================== DOMAIN SIZE 46 ========================

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

For domain size 46.

Current CPU time: 0.00 seconds (total CPU time: 20.73 seconds).
Ground clauses: seen=99509, kept=99417.
Selections=87, assignments=1567, propagations=23597, current_models=0.
Rewrite_terms=1107873, rewrite_bools=114560, indexes=188489.
Rules_from_neg_clauses=635, cross_offs=208990.

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

============================== DOMAIN SIZE 47 ========================

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

For domain size 47.

Current CPU time: 0.00 seconds (total CPU time: 22.55 seconds).
Ground clauses: seen=106090, kept=105996.
Selections=88, assignments=1613, propagations=25250, current_models=0.
Rewrite_terms=1158724, rewrite_bools=121395, indexes=196220.
Rules_from_neg_clauses=617, cross_offs=215920.

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

============================== DOMAIN SIZE 48 ========================

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

For domain size 48.

Current CPU time: 0.00 seconds (total CPU time: 24.52 seconds).
Ground clauses: seen=112955, kept=112859.
Selections=89, assignments=1660, propagations=26972, current_models=0.
Rewrite_terms=1212711, rewrite_bools=129124, indexes=203971.
Rules_from_neg_clauses=596, cross_offs=222957.

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

============================== DOMAIN SIZE 49 ========================

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

For domain size 49.

Current CPU time: 0.00 seconds (total CPU time: 26.64 seconds).
Ground clauses: seen=120110, kept=120012.
Selections=90, assignments=1708, propagations=28878, current_models=0.
Rewrite_terms=1272145, rewrite_bools=139144, indexes=211570.
Rules_from_neg_clauses=572, cross_offs=229793.

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

============================== DOMAIN SIZE 50 ========================

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

For domain size 50.

Current CPU time: 0.00 seconds (total CPU time: 28.89 seconds).
Ground clauses: seen=127561, kept=127461.
Selections=91, assignments=1757, propagations=31068, current_models=0.
Rewrite_terms=1332706, rewrite_bools=149303, indexes=219278.
Rules_from_neg_clauses=550, cross_offs=236825.

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

============================== DOMAIN SIZE 51 ========================

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

For domain size 51.

Current CPU time: 0.00 seconds (total CPU time: 31.34 seconds).
Ground clauses: seen=135314, kept=135212.
Selections=92, assignments=1807, propagations=33332, current_models=0.
Rewrite_terms=1397328, rewrite_bools=160878, indexes=226925.
Rules_from_neg_clauses=513, cross_offs=243847.

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

============================== DOMAIN SIZE 52 ========================

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

For domain size 52.

Current CPU time: 0.00 seconds (total CPU time: 33.95 seconds).
Ground clauses: seen=143375, kept=143271.
Selections=93, assignments=1858, propagations=35797, current_models=0.
Rewrite_terms=1466257, rewrite_bools=174105, indexes=234456.
Rules_from_neg_clauses=475, cross_offs=251003.

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

============================== DOMAIN SIZE 53 ========================

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

interpretation( 53, [number=1, seconds=36], [

        function(a1, [ 0 ]),

        function(a10, [ 1 ]),

        function(a2, [ 3 ]),

        function(a3, [ 7 ]),

        function(a4, [ 2 ]),

        function(a5, [ 6 ]),

        function(a6, [14 ]),

        function(a7, [26 ]),

        function(a8, [ 8 ]),

        function(a9, [25 ]),

        function(*(_,_), [
			   0, 3, 1,15,11, 9, 5,12, 2,16, 6,33,25,19,20,47,50,43,48,32,38,34,37,30,35,36,45,17, 4,23,22,14,49,31,51,21,13,52,44,18, 7,24,46,28,10,27,39,29,40, 8,41,42,26,
			   5, 1, 0,11, 3,12, 9,16, 6,20, 7,19,48,15,25,43,37,33,50,34,35,47,38,32,36, 8,44,13, 2,21,24,18,46,30,26,17, 4,45,23,22,14,49,51,10,31,28,41,27,39,40,42,52,29,
			   6, 4, 2,17,13,14, 7,18, 0,22, 5,23,49,21,24,45,51,44,46,42,29,52,26,41,27,28,43,11, 1,19,20,12,48,39,37,15, 3,47,33,16, 9,25,50, 8,40,36,30,35,31,10,32,34,38,
			   9, 0, 5, 3, 1,16,12,20, 7,25,14,15,50,11,48,33,38,19,37,47,36,43,35,34, 8,40,23, 4, 6,17,49,22,51,32,29,13, 2,44,21,24,18,46,26,31,30,10,42,28,41,39,52,45,27,
			   7, 2, 6,13, 4,18,14,22, 5,24, 9,21,46,17,49,44,26,23,51,52,27,45,29,42,28,10,33, 3, 0,15,25,16,50,41,38,11, 1,43,19,20,12,48,37,40,39, 8,32,36,30,31,34,47,35,
			   1,11, 3,19,15, 5, 0, 9, 4,12, 2,43,20,33,16,34,48,47,25,30,37,32,50,31,38,35,52,21,13,44,18, 7,24,10,46,23,17,42,45,14, 6,22,49,27,28,29,40,26, 8,36,39,41,51,
			   2,13, 4,21,17, 7, 6,14, 1,18, 0,44,24,23,22,52,46,45,49,41,26,42,51,39,29,27,47,15, 3,33,16, 9,25,40,50,19,11,34,43,12, 5,20,48,36, 8,35,31,38,10,28,30,32,37,
			   4,17,13,23,21, 6, 2, 7, 3,14, 1,45,22,44,18,42,49,52,24,39,51,41,46,40,26,29,34,19,11,43,12, 5,20, 8,48,33,15,32,47, 9, 0,16,25,35,36,38,10,37,28,27,31,30,50,
			  10,27,28,26,29,30,31,32, 8,34,40,46,43,51,47,24,19,49,33,18,11,22,15,14, 3, 1,25,38,36,50,52,41,44, 7,21,37,35,20,48,42,39,45,23, 2, 6, 4, 9,13, 5, 0,12,16,17,
			   3,15,11,33,19, 0, 1, 5,13, 9, 4,47,16,43,12,32,25,34,20,31,50,30,48,10,37,38,42,23,17,45,14, 6,22,28,49,44,21,41,52, 7, 2,18,24,29,27,26, 8,51,36,35,40,39,46,
			   8,35,36,37,38,39,40,41,28,42,10,48,45,50,52,20,23,25,44,12,17,16,21, 9,13, 4,24,26,27,46,34,30,43, 5,19,51,29,22,49,32,31,47,33, 1, 0, 3, 7,11, 6, 2,14,18,15,
			  12, 5, 9, 1, 0,20,16,25,14,48,18,11,37, 3,50,19,35,15,38,43, 8,33,36,47,40,39,21, 2, 7,13,46,24,26,34,27, 4, 6,23,17,49,22,51,29,30,32,31,52,10,42,41,45,44,28,
			  11,19,15,43,33, 1, 3, 0,17, 5,13,34,12,47, 9,30,20,32,16,10,48,31,25,28,50,37,41,44,21,52, 7, 2,18,27,24,45,23,39,42, 6, 4,14,22,26,29,51,36,46,35,38, 8,40,49,
			  14, 6, 7, 4, 2,22,18,24, 9,49,12,17,51,13,46,23,29,21,26,45,28,44,27,52,10,31,19, 1, 5,11,48,20,37,42,35, 3, 0,33,15,25,16,50,38,39,41,40,34, 8,32,30,47,43,36,
			  13,21,17,44,23, 2, 4, 6,11, 7, 3,52,18,45,14,41,24,42,22,40,46,39,49, 8,51,26,32,33,15,47, 9, 0,16,36,25,43,19,30,34, 5, 1,12,20,38,35,37,28,50,27,29,10,31,48,
			  16, 9,12, 0, 5,25,20,48,18,50,22, 3,38, 1,37,15,36,11,35,33,40,19, 8,43,39,41,17, 6,14, 4,51,49,29,47,28, 2, 7,21,13,46,24,26,27,32,34,30,45,31,52,42,44,23,10,
			  15,33,19,47,43, 3,11, 1,21, 0,17,32, 9,34, 5,31,16,30,12,28,25,10,20,27,48,50,39,45,23,42, 6, 4,14,29,22,52,44,40,41, 2,13, 7,18,51,26,46,35,49,38,37,36, 8,24,
			  18, 7,14, 2, 6,24,22,49,12,46,16,13,26, 4,51,21,27,17,29,44,10,23,28,45,31,30,15, 0, 9, 3,50,25,38,52,36, 1, 5,19,11,48,20,37,35,41,42,39,47,40,34,32,43,33, 8,
			  17,23,21,45,44, 4,13, 2,15, 6,11,42,14,52, 7,39,22,41,18, 8,49,40,24,36,46,51,30,43,19,34, 5, 1,12,35,20,47,33,31,32, 0, 3, 9,16,37,38,50,27,48,29,26,28,10,25,
			  20,12,16, 5, 9,48,25,50,22,37,24, 1,35, 0,38,11, 8, 3,36,19,39,15,40,33,41,42,13, 7,18, 2,26,46,27,43,10, 6,14,17, 4,51,49,29,28,34,47,32,44,30,45,52,23,21,31,
			  19,43,33,34,47,11,15, 3,23, 1,21,30, 5,32, 0,10,12,31, 9,27,20,28,16,29,25,48,40,52,44,41, 2,13, 7,26,18,42,45, 8,39, 4,17, 6,14,46,51,49,38,24,37,50,35,36,22,
			  22,14,18, 6, 7,49,24,46,16,51,20, 4,29, 2,26,17,28,13,27,23,31,21,10,44,30,32,11, 5,12, 1,37,48,35,45, 8, 0, 9,15, 3,50,25,38,36,42,52,41,43,39,47,34,33,19,40,
			  21,44,23,52,45,13,17, 4,19, 2,15,41, 7,42, 6,40,18,39,14,36,24, 8,22,35,49,46,31,47,33,32, 0, 3, 9,38,16,34,43,10,30, 1,11, 5,12,50,37,48,29,25,26,51,27,28,20,
			  24,18,22, 7,14,46,49,51,20,26,25, 2,27, 6,29,13,10, 4,28,21,30,17,31,23,32,34, 3, 9,16, 0,38,50,36,44,40, 5,12,11, 1,37,48,35, 8,52,45,42,33,41,43,47,19,15,39,
			  23,45,44,42,52,17,21,13,33, 4,19,39, 6,41, 2, 8,14,40, 7,35,22,36,18,38,24,49,10,34,43,30, 1,11, 5,37,12,32,47,28,31, 3,15, 0, 9,48,50,25,26,20,51,46,29,27,16,
			  33,47,43,32,34,15,19,11,44, 3,23,31, 0,30, 1,28, 9,10, 5,29,16,27,12,26,20,25, 8,42,45,39, 4,17, 6,51,14,41,52,36,40,13,21, 2, 7,49,46,24,37,22,50,48,38,35,18,
			  42,39,41, 8,40,45,52,44,32,23,34,35,17,36,21,37, 4,38,13,48, 6,50, 2,25, 7,14,26,10,30,27,19,43,11,20, 1,28,31,51,29,33,47,15, 3,12,16, 9,24, 5,22,18,49,46, 0,
			  39, 8,40,35,36,42,41,52,31,45,30,37,23,38,44,48,17,50,21,20, 4,25,13,16, 2, 6,46,27,10,26,43,34,19,12,11,29,28,49,51,47,32,33,15, 5, 9, 0,18, 1,14, 7,22,24, 3,
			  40,36, 8,38,35,41,39,42,10,52,31,50,44,37,45,25,21,48,23,16,13,20,17,12, 4, 2,49,29,28,51,47,32,33, 9,15,26,27,24,46,34,30,43,19, 0, 5, 1,14, 3, 7, 6,18,22,11,
			  41,40,39,36, 8,52,42,45,30,44,32,38,21,35,23,50,13,37,17,25, 2,48, 4,20, 6, 7,51,28,31,29,33,47,15,16, 3,27,10,46,26,43,34,19,11, 9,12, 5,22, 0,18,14,24,49, 1,
			  35,37,38,48,50, 8,36,40,29,39,27,20,42,25,41,12,45,16,52, 5,23, 9,44, 0,21,17,18,46,26,24,30,10,34, 1,43,49,51,14,22,31,28,32,47,11, 3,15, 2,19, 4,13, 6, 7,33,
			  36,38,35,50,37,40, 8,39,27,41,28,25,52,48,42,16,44,20,45, 9,21,12,23, 5,17,13,22,51,29,49,32,31,47, 0,33,46,26,18,24,30,10,34,43, 3, 1,11, 6,15, 2, 4, 7,14,19,
			  38,50,37,25,48,36,35, 8,26,40,29,16,41,20,39, 9,52,12,42, 0,44, 5,45, 1,23,21,14,49,51,22,31,28,32, 3,47,24,46, 7,18,10,27,30,34,15,11,19, 4,33,13,17, 2, 6,43,
			  25,16,20, 9,12,50,48,37,24,38,49, 0,36, 5,35, 3,40, 1, 8,15,41,11,39,19,42,52, 4,14,22, 6,29,51,28,33,31, 7,18,13, 2,26,46,27,10,47,43,34,23,32,44,45,21,17,30,
			  37,48,50,20,25,35,38,36,51, 8,26,12,39,16,40, 5,42, 9,41, 1,45, 0,52, 3,44,23, 7,24,46,18,10,27,30,11,34,22,49, 6,14,28,29,31,32,19,15,33,13,43,17,21, 4, 2,47,
			  30,10,31,27,28,34,32,47,39,43,41,26,19,29,33,46,11,51,15,24, 1,49, 3,22, 0, 5,50,36,40,38,44,52,21,18,13,35, 8,48,37,45,42,23,17, 7,14, 6,16, 2,12, 9,20,25, 4,
			  31,28,10,29,27,32,30,34,40,47,39,51,33,26,43,49,15,46,19,22, 3,24,11,18, 1, 0,48,35, 8,37,45,42,23,14,17,38,36,25,50,52,41,44,21, 6, 7, 2,12, 4, 9, 5,16,20,13,
			  34,30,32,10,31,43,47,33,42,19,52,27,11,28,15,26, 1,29, 3,46, 5,51, 0,49, 9,12,38,40,41,36,21,44,13,24, 2, 8,39,37,35,23,45,17, 4,18,22,14,25, 7,20,16,48,50, 6,
			  32,31,30,28,10,47,34,43,41,33,42,29,15,27,19,51, 3,26,11,49, 0,46, 1,24, 5, 9,37, 8,39,35,23,45,17,22, 4,36,40,50,38,44,52,21,13,14,18, 7,20, 6,16,12,25,48, 2,
			  27,26,29,46,51,10,28,31,35,30,36,24,34,49,32,18,43,22,47, 7,19,14,33, 6,15,11,16,50,38,25,41,40,52, 2,44,48,37,12,20,39, 8,42,45,13, 4,17, 0,21, 1, 3, 5, 9,23,
			  28,29,27,51,26,31,10,30,36,32, 8,49,47,46,34,22,33,24,43,14,15,18,19, 7,11, 3,20,37,35,48,42,39,45, 6,23,50,38,16,25,41,40,52,44, 4, 2,13, 5,17, 0, 1, 9,12,21,
			  29,51,26,49,46,28,27,10,38,31,35,22,32,24,30,14,47,18,34, 6,33, 7,43, 2,19,15,12,48,37,20,39, 8,42, 4,45,25,50, 9,16,40,36,41,52,17,13,21, 1,23, 3,11, 0, 5,44,
			  26,46,51,24,49,27,29,28,37,10,38,18,30,22,31, 7,34,14,32, 2,43, 6,47, 4,33,19, 9,25,50,16,40,36,41,13,52,20,48, 5,12, 8,35,39,42,21,17,23, 3,44,11,15, 1, 0,45,
			  48,20,25,12,16,37,50,38,49,35,46, 5, 8, 9,36, 1,39, 0,40,11,42, 3,41,15,52,45, 2,18,24, 7,27,26,10,19,30,14,22, 4, 6,29,51,28,31,43,33,47,21,34,23,44,17,13,32,
			  49,22,24,14,18,51,46,26,25,29,48, 6,28, 7,27, 4,31, 2,10,17,32,13,30,21,34,47, 1,12,20, 5,35,37, 8,23,39, 9,16, 3, 0,38,50,36,40,45,44,52,19,42,33,43,15,11,41,
			  46,24,49,18,22,26,51,29,48,27,50, 7,10,14,28, 2,30, 6,31,13,34, 4,32,17,47,43, 0,16,25, 9,36,38,40,21,41,12,20, 1, 5,35,37, 8,39,44,23,45,15,52,19,33,11, 3,42,
			  45,42,52,39,41,23,44,21,47,17,43, 8, 4,40,13,35, 6,36, 2,37,14,38, 7,50,18,22,27,30,34,10,11,19, 1,48, 5,31,32,29,28,15,33, 3, 0,20,25,16,46,12,49,24,51,26, 9,
			  50,25,48,16,20,38,37,35,46,36,51, 9,40,12, 8, 0,41, 5,39, 3,52, 1,42,11,45,44, 6,22,49,14,28,29,31,15,32,18,24, 2, 7,27,26,10,30,33,19,43,17,47,21,23,13, 4,34,
			  43,34,47,30,32,19,33,15,45,11,44,10, 1,31, 3,27, 5,28, 0,26,12,29, 9,51,16,20,36,41,52,40,13,21, 2,46, 7,39,42,35, 8,17,23, 4, 6,24,49,22,50,18,48,25,37,38,14,
			  44,52,45,41,42,21,23,17,43,13,33,40, 2,39, 4,36, 7, 8, 6,38,18,35,14,37,22,24,28,32,47,31, 3,15, 0,50, 9,30,34,27,10,11,19, 1, 5,25,48,20,51,16,46,49,26,29,12,
			  47,32,34,31,30,33,43,19,52,15,45,28, 3,10,11,29, 0,27, 1,51, 9,26, 5,46,12,16,35,39,42, 8,17,23, 4,49, 6,40,41,38,36,21,44,13, 2,22,24,18,48,14,25,20,50,37, 7,
			  52,41,42,40,39,44,45,23,34,21,47,36,13, 8,17,38, 2,35, 4,50, 7,37, 6,48,14,18,29,31,32,28,15,33, 3,25, 0,10,30,26,27,19,43,11, 1,16,20,12,49, 9,24,22,46,51, 5,
			  51,49,46,22,24,29,26,27,50,28,37,14,31,18,10, 6,32, 7,30, 4,47, 2,34,13,43,33, 5,20,48,12, 8,35,39,17,42,16,25, 0, 9,36,38,40,41,23,21,44,11,45,15,19, 3, 1,52 ])
]).

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

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

For domain size 53.

Current CPU time: 0.00 seconds (total CPU time: 36.98 seconds).
Ground clauses: seen=151750, kept=151644.
Selections=94, assignments=1910, propagations=38418, current_models=1.
Rewrite_terms=1644799, rewrite_bools=224845, indexes=241859.
Rules_from_neg_clauses=435, cross_offs=258314.

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

User_CPU=36.98, System_CPU=0.09, Wall_clock=37.

Exiting with 1 model.

Process 1864 exit (max_models) Sun Mar 17 09:33:59 2013
The process finished Sun Mar 17 09:33:59 2013