============================== Mace4 =================================
Mace4 (32) version Dec-2007, Dec 2007.
Process 1012 was started by Alexei on Alexei-PC,
Sun Mar 17 00:29:15 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 * a5.
a3 = a2 * a7.
a4 = a3 * a8.
a5 = a4 * a1.
a6 = a5 * a10.
a7 = a6 * a9.
a8 = a7 * a4.
a9 = a8 * a3.
a10 = a9 * a6.
a1 = a10 * a2.
end_of_list.

formulas(goals).
a1 = a2 & a2 = a3 & a3 = a4 & a4 = a5 & a5 = a6 & a6 = a7 & a7 = a8 & a8 = a9 & a9 = a10.
end_of_list.

============================== end of input ==========================

% Enabling option dependencies (ignore applies only on input).

============================== PROCESS NON-CLAUSAL FORMULAS ==========

% Formulas that are not ordinary clauses:
1 a1 = a2 & a2 = a3 & a3 = a4 & a4 = a5 & a5 = a6 & a6 = a7 & a7 = a8 & a8 = a9 & a9 = a10 # label(non_clause) # label(goal).  [goal].

============================== end of process non-clausal formulas ===

============================== CLAUSES FOR SEARCH ====================

formulas(mace4_clauses).
x * x = x.
(x * y) * y = x.
(x * y) * z = (x * z) * (y * z).
a2 = a1 * a5.
a3 = a2 * a7.
a4 = a3 * a8.
a5 = a4 * a1.
a6 = a5 * a10.
a7 = a6 * a9.
a8 = a7 * a4.
a9 = a8 * a3.
a10 = a9 * a6.
a1 = a10 * a2.
a1 != a2 | a3 != a2 | a4 != a3 | a4 != a5 | a6 != a5 | a6 != a7 | a8 != a7 | 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=5, assignments=9, propagations=14, current_models=0.
Rewrite_terms=79, rewrite_bools=23, indexes=0.
Rules_from_neg_clauses=7, cross_offs=7.

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

============================== DOMAIN SIZE 3 =========================

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

For domain size 3.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=50, kept=44.
Selections=6, assignments=12, propagations=61, current_models=0.
Rewrite_terms=657, rewrite_bools=152, indexes=57.
Rules_from_neg_clauses=20, cross_offs=44.

============================== 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=14, assignments=41, propagations=104, current_models=0.
Rewrite_terms=1522, rewrite_bools=315, indexes=204.
Rules_from_neg_clauses=23, cross_offs=104.

============================== 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=20, assignments=72, propagations=188, current_models=0.
Rewrite_terms=2745, rewrite_bools=456, indexes=460.
Rules_from_neg_clauses=30, cross_offs=246.

============================== 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=22, assignments=85, propagations=321, current_models=0.
Rewrite_terms=6630, rewrite_bools=1230, indexes=818.
Rules_from_neg_clauses=48, cross_offs=501.

============================== 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=26, assignments=112, propagations=408, current_models=0.
Rewrite_terms=8006, rewrite_bools=1330, indexes=1170.
Rules_from_neg_clauses=46, cross_offs=747.

============================== 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=26, assignments=113, propagations=435, current_models=0.
Rewrite_terms=9593, rewrite_bools=1505, indexes=1382.
Rules_from_neg_clauses=46, cross_offs=1049.

============================== 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=30, assignments=148, propagations=645, current_models=0.
Rewrite_terms=15309, rewrite_bools=2464, indexes=2012.
Rules_from_neg_clauses=52, cross_offs=1541.

============================== 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=32, assignments=168, propagations=780, current_models=0.
Rewrite_terms=22669, rewrite_bools=4121, indexes=2727.
Rules_from_neg_clauses=76, cross_offs=2115.

============================== 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=35, assignments=200, propagations=988, current_models=0.
Rewrite_terms=29068, rewrite_bools=5117, indexes=3575.
Rules_from_neg_clauses=70, cross_offs=2861.

============================== 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=1895, kept=1871.
Selections=37, assignments=223, propagations=1225, current_models=0.
Rewrite_terms=40696, rewrite_bools=7397, indexes=4501.
Rules_from_neg_clauses=93, cross_offs=3793.

============================== 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=2390, kept=2364.
Selections=43, assignments=298, propagations=1738, current_models=0.
Rewrite_terms=53347, rewrite_bools=9149, indexes=6331.
Rules_from_neg_clauses=116, cross_offs=5339.

============================== 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=2965, kept=2937.
Selections=45, assignments=325, propagations=2051, current_models=0.
Rewrite_terms=64960, rewrite_bools=10920, indexes=7682.
Rules_from_neg_clauses=112, cross_offs=6813.

============================== 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=3626, kept=3596.
Selections=51, assignments=412, propagations=2954, current_models=0.
Rewrite_terms=91033, rewrite_bools=14981, indexes=10420.
Rules_from_neg_clauses=159, cross_offs=9167.

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

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

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

For domain size 16.

Current CPU time: 0.00 seconds (total CPU time: 0.16 seconds).
Ground clauses: seen=4379, kept=4347.
Selections=53, assignments=443, propagations=3302, current_models=0.
Rewrite_terms=99069, rewrite_bools=15239, indexes=12158.
Rules_from_neg_clauses=142, cross_offs=11105.

============================== 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=59, assignments=542, propagations=4465, current_models=0.
Rewrite_terms=128502, rewrite_bools=19218, indexes=16014.
Rules_from_neg_clauses=182, cross_offs=14267.

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

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

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

For domain size 18.

Current CPU time: 0.00 seconds (total CPU time: 0.28 seconds).
Ground clauses: seen=6185, kept=6149.
Selections=61, assignments=577, propagations=5118, current_models=0.
Rewrite_terms=154053, rewrite_bools=23096, indexes=18241.
Rules_from_neg_clauses=215, cross_offs=17347.

============================== 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=67, assignments=688, propagations=6455, current_models=0.
Rewrite_terms=186783, rewrite_bools=27027, indexes=22640.
Rules_from_neg_clauses=213, cross_offs=21014.

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

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

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

For domain size 20.

Current CPU time: 0.00 seconds (total CPU time: 0.50 seconds).
Ground clauses: seen=8431, kept=8391.
Selections=69, assignments=727, propagations=7300, current_models=0.
Rewrite_terms=231051, rewrite_bools=33947, indexes=26712.
Rules_from_neg_clauses=239, cross_offs=25047.

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

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

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

For domain size 21.

Current CPU time: 0.00 seconds (total CPU time: 0.69 seconds).
Ground clauses: seen=9734, kept=9692.
Selections=76, assignments=870, propagations=9488, current_models=0.
Rewrite_terms=289848, rewrite_bools=43608, indexes=32726.
Rules_from_neg_clauses=340, cross_offs=30780.

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

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

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

For domain size 22.

Current CPU time: 0.00 seconds (total CPU time: 0.88 seconds).
Ground clauses: seen=11165, kept=11121.
Selections=79, assignments=934, propagations=10459, current_models=0.
Rewrite_terms=313357, rewrite_bools=44973, indexes=36856.
Rules_from_neg_clauses=334, cross_offs=35755.

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

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

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

For domain size 23.

Current CPU time: 0.00 seconds (total CPU time: 1.14 seconds).
Ground clauses: seen=12730, kept=12684.
Selections=86, assignments=1091, propagations=12686, current_models=0.
Rewrite_terms=389263, rewrite_bools=56711, indexes=45173.
Rules_from_neg_clauses=342, cross_offs=43344.

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

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

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

For domain size 24.

Current CPU time: 0.00 seconds (total CPU time: 1.47 seconds).
Ground clauses: seen=14435, kept=14387.
Selections=88, assignments=1138, propagations=13492, current_models=0.
Rewrite_terms=446876, rewrite_bools=65415, indexes=50916.
Rules_from_neg_clauses=322, cross_offs=49922.

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

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

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

For domain size 25.

Current CPU time: 0.00 seconds (total CPU time: 1.89 seconds).
Ground clauses: seen=16286, kept=16236.
Selections=93, assignments=1261, propagations=15606, current_models=0.
Rewrite_terms=549778, rewrite_bools=85984, indexes=60278.
Rules_from_neg_clauses=329, cross_offs=58862.

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

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

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

For domain size 26.

Current CPU time: 0.00 seconds (total CPU time: 2.42 seconds).
Ground clauses: seen=18289, kept=18237.
Selections=93, assignments=1262, propagations=16023, current_models=0.
Rewrite_terms=638922, rewrite_bools=103732, indexes=66326.
Rules_from_neg_clauses=317, cross_offs=68239.

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

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

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

For domain size 27.

Current CPU time: 0.00 seconds (total CPU time: 3.02 seconds).
Ground clauses: seen=20450, kept=20396.
Selections=95, assignments=1316, propagations=17155, current_models=0.
Rewrite_terms=680638, rewrite_bools=101896, indexes=73974.
Rules_from_neg_clauses=382, cross_offs=78357.

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

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

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

For domain size 28.

Current CPU time: 0.00 seconds (total CPU time: 3.66 seconds).
Ground clauses: seen=22775, kept=22719.
Selections=95, assignments=1317, propagations=17449, current_models=0.
Rewrite_terms=702189, rewrite_bools=101100, indexes=79578.
Rules_from_neg_clauses=366, cross_offs=85597.

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

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

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

For domain size 29.

Current CPU time: 0.00 seconds (total CPU time: 4.39 seconds).
Ground clauses: seen=25270, kept=25212.
Selections=97, assignments=1375, propagations=18841, current_models=0.
Rewrite_terms=763836, rewrite_bools=107444, indexes=88084.
Rules_from_neg_clauses=406, cross_offs=95503.

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

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

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

For domain size 30.

Current CPU time: 0.00 seconds (total CPU time: 5.19 seconds).
Ground clauses: seen=27941, kept=27881.
Selections=97, assignments=1376, propagations=19119, current_models=0.
Rewrite_terms=802362, rewrite_bools=111018, indexes=94717.
Rules_from_neg_clauses=332, cross_offs=106246.

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

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

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

For domain size 31.

Current CPU time: 0.00 seconds (total CPU time: 6.12 seconds).
Ground clauses: seen=30794, kept=30732.
Selections=99, assignments=1438, propagations=20945, current_models=0.
Rewrite_terms=909524, rewrite_bools=122395, indexes=104672.
Rules_from_neg_clauses=493, cross_offs=119092.

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

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

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

For domain size 32.

Current CPU time: 0.00 seconds (total CPU time: 7.12 seconds).
Ground clauses: seen=33835, kept=33771.
Selections=99, assignments=1439, propagations=21314, current_models=0.
Rewrite_terms=938948, rewrite_bools=122504, indexes=111762.
Rules_from_neg_clauses=391, cross_offs=131544.

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

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

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

For domain size 33.

Current CPU time: 0.00 seconds (total CPU time: 8.33 seconds).
Ground clauses: seen=37070, kept=37004.
Selections=101, assignments=1505, propagations=23175, current_models=0.
Rewrite_terms=1063076, rewrite_bools=137140, indexes=123080.
Rules_from_neg_clauses=515, cross_offs=145821.

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

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

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

For domain size 34.

Current CPU time: 0.00 seconds (total CPU time: 9.62 seconds).
Ground clauses: seen=40505, kept=40437.
Selections=101, assignments=1506, propagations=23387, current_models=0.
Rewrite_terms=1106266, rewrite_bools=139305, indexes=131608.
Rules_from_neg_clauses=407, cross_offs=157813.

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

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

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

For domain size 35.

Current CPU time: 0.00 seconds (total CPU time: 11.20 seconds).
Ground clauses: seen=44146, kept=44076.
Selections=103, assignments=1576, propagations=25595, current_models=0.
Rewrite_terms=1266266, rewrite_bools=163280, indexes=142682.
Rules_from_neg_clauses=552, cross_offs=174976.

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

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

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

For domain size 36.

Current CPU time: 0.00 seconds (total CPU time: 12.89 seconds).
Ground clauses: seen=47999, kept=47927.
Selections=103, assignments=1577, propagations=26143, current_models=0.
Rewrite_terms=1321366, rewrite_bools=164269, indexes=153002.
Rules_from_neg_clauses=541, cross_offs=191411.

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

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

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

For domain size 37.

Current CPU time: 0.00 seconds (total CPU time: 14.81 seconds).
Ground clauses: seen=52070, kept=51996.
Selections=105, assignments=1651, propagations=28769, current_models=0.
Rewrite_terms=1446680, rewrite_bools=178989, indexes=167922.
Rules_from_neg_clauses=603, cross_offs=208637.

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

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

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

For domain size 38.

Current CPU time: 0.00 seconds (total CPU time: 16.81 seconds).
Ground clauses: seen=56365, kept=56289.
Selections=105, assignments=1652, propagations=28956, current_models=0.
Rewrite_terms=1473169, rewrite_bools=178991, indexes=176552.
Rules_from_neg_clauses=575, cross_offs=225307.

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

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

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

For domain size 39.

Current CPU time: 0.00 seconds (total CPU time: 19.27 seconds).
Ground clauses: seen=60890, kept=60812.
Selections=107, assignments=1730, propagations=31966, current_models=0.
Rewrite_terms=1703479, rewrite_bools=215378, indexes=192793.
Rules_from_neg_clauses=721, cross_offs=248004.

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

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

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

For domain size 40.

Current CPU time: 0.00 seconds (total CPU time: 21.64 seconds).
Ground clauses: seen=65651, kept=65571.
Selections=107, assignments=1731, propagations=31486, current_models=0.
Rewrite_terms=1654246, rewrite_bools=197733, indexes=202160.
Rules_from_neg_clauses=509, cross_offs=263456.

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

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

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

For domain size 41.

Current CPU time: 0.00 seconds (total CPU time: 24.36 seconds).
Ground clauses: seen=70654, kept=70572.
Selections=107, assignments=1731, propagations=31728, current_models=0.
Rewrite_terms=1772426, rewrite_bools=215680, indexes=215001.
Rules_from_neg_clauses=500, cross_offs=279300.

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

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

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

For domain size 42.

Current CPU time: 0.00 seconds (total CPU time: 27.45 seconds).
Ground clauses: seen=75905, kept=75821.
Selections=108, assignments=1772, propagations=33299, current_models=0.
Rewrite_terms=1881374, rewrite_bools=225398, indexes=232501.
Rules_from_neg_clauses=731, cross_offs=295419.

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

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

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

For domain size 43.

Current CPU time: 0.00 seconds (total CPU time: 30.67 seconds).
Ground clauses: seen=81410, kept=81324.
Selections=109, assignments=1814, propagations=34349, current_models=0.
Rewrite_terms=1935741, rewrite_bools=229253, indexes=244380.
Rules_from_neg_clauses=733, cross_offs=306744.

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

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

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

For domain size 44.

Current CPU time: 0.00 seconds (total CPU time: 34.09 seconds).
Ground clauses: seen=87175, kept=87087.
Selections=110, assignments=1857, propagations=35552, current_models=0.
Rewrite_terms=1991464, rewrite_bools=233448, indexes=256322.
Rules_from_neg_clauses=735, cross_offs=317895.

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

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

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

For domain size 45.

Current CPU time: 0.00 seconds (total CPU time: 37.56 seconds).
Ground clauses: seen=93206, kept=93116.
Selections=111, assignments=1901, propagations=36936, current_models=0.
Rewrite_terms=2051400, rewrite_bools=238790, indexes=268389.
Rules_from_neg_clauses=724, cross_offs=329157.

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

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

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

For domain size 46.

Current CPU time: 0.00 seconds (total CPU time: 41.22 seconds).
Ground clauses: seen=99509, kept=99417.
Selections=112, assignments=1946, propagations=38488, current_models=0.
Rewrite_terms=2113030, rewrite_bools=244665, indexes=280482.
Rules_from_neg_clauses=725, cross_offs=340504.

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

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

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

For domain size 47.

Current CPU time: 0.00 seconds (total CPU time: 45.11 seconds).
Ground clauses: seen=106090, kept=105996.
Selections=113, assignments=1992, propagations=40176, current_models=0.
Rewrite_terms=2178350, rewrite_bools=251631, indexes=292634.
Rules_from_neg_clauses=720, cross_offs=351731.

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

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

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

For domain size 48.

Current CPU time: 0.00 seconds (total CPU time: 49.31 seconds).
Ground clauses: seen=112955, kept=112859.
Selections=114, assignments=2039, propagations=41988, current_models=0.
Rewrite_terms=2246912, rewrite_bools=259906, indexes=304708.
Rules_from_neg_clauses=703, cross_offs=363168.

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

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

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

For domain size 49.

Current CPU time: 0.00 seconds (total CPU time: 53.66 seconds).
Ground clauses: seen=120110, kept=120012.
Selections=115, assignments=2087, propagations=43953, current_models=0.
Rewrite_terms=2320376, rewrite_bools=269809, indexes=316768.
Rules_from_neg_clauses=681, cross_offs=374573.

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

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

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

For domain size 50.

Current CPU time: 0.00 seconds (total CPU time: 58.17 seconds).
Ground clauses: seen=127561, kept=127461.
Selections=116, assignments=2136, propagations=46016, current_models=0.
Rewrite_terms=2394917, rewrite_bools=280021, indexes=328833.
Rules_from_neg_clauses=648, cross_offs=386041.

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

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

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

For domain size 51.

Current CPU time: 0.00 seconds (total CPU time: 62.84 seconds).
Ground clauses: seen=135314, kept=135212.
Selections=117, assignments=2186, propagations=48248, current_models=0.
Rewrite_terms=2473912, rewrite_bools=291878, indexes=340819.
Rules_from_neg_clauses=624, cross_offs=397520.

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

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

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

For domain size 52.

Current CPU time: 0.00 seconds (total CPU time: 67.86 seconds).
Ground clauses: seen=143375, kept=143271.
Selections=118, assignments=2237, propagations=50668, current_models=0.
Rewrite_terms=2557973, rewrite_bools=305857, indexes=352619.
Rules_from_neg_clauses=584, cross_offs=408959.

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

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

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

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

        function(a1, [ 0 ]),

        function(a10, [ 1 ]),

        function(a2, [ 2 ]),

        function(a3, [39 ]),

        function(a4, [ 5 ]),

        function(a5, [ 3 ]),

        function(a6, [11 ]),

        function(a7, [25 ]),

        function(a8, [35 ]),

        function(a9, [12 ]),

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

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

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

For domain size 53.

Current CPU time: 0.00 seconds (total CPU time: 73.41 seconds).
Ground clauses: seen=151750, kept=151644.
Selections=119, assignments=2289, propagations=53241, current_models=1.
Rewrite_terms=2750179, rewrite_bools=356583, indexes=364409.
Rules_from_neg_clauses=544, cross_offs=420541.

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

User_CPU=73.41, System_CPU=0.05, Wall_clock=74.

Exiting with 1 model.

Process 1012 exit (max_models) Sun Mar 17 00:30:29 2013
The process finished Sun Mar 17 00:30:29 2013