============================== Mace4 =================================
Mace4 (32) version Dec-2007, Dec 2007.
Process 3284 was started by Alexei on Alexei-PC,
Sat Mar 16 17:53:40 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 * a10.
a4 = a3 * a9.
a5 = a4 * a8.
a6 = a5 * a2.
a7 = a6 * a1.
a8 = a7 * a3.
a9 = a8 * a4.
a10 = a9 * a5.
a1 = a10 * a7.
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 * a6.
a3 = a2 * a10.
a4 = a3 * a9.
a5 = a4 * a8.
a6 = a5 * a2.
a7 = a6 * a1.
a8 = a7 * a3.
a9 = a8 * a4.
a10 = a9 * a5.
a1 = a10 * a7.
a1 != a2 | a3 != a2 | a4 != a3 | a5 != a4 | a5 != a6 | a7 != a6 | a7 != a8 | a8 != a9 | 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=15, current_models=0.
Rewrite_terms=79, rewrite_bools=22, indexes=0.
Rules_from_neg_clauses=6, cross_offs=6.

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

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

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

For domain size 3.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=50, kept=44.
Selections=7, assignments=15, propagations=61, current_models=0.
Rewrite_terms=615, rewrite_bools=140, indexes=65.
Rules_from_neg_clauses=14, cross_offs=39.

============================== 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=13, assignments=37, propagations=118, current_models=0.
Rewrite_terms=1612, rewrite_bools=331, indexes=195.
Rules_from_neg_clauses=23, cross_offs=101.

============================== 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=18, assignments=62, propagations=188, current_models=0.
Rewrite_terms=2962, rewrite_bools=564, indexes=399.
Rules_from_neg_clauses=27, cross_offs=233.

============================== 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=269, kept=257.
Selections=20, assignments=75, propagations=318, current_models=0.
Rewrite_terms=5630, rewrite_bools=947, indexes=742.
Rules_from_neg_clauses=44, cross_offs=485.

============================== 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=25, assignments=109, propagations=460, current_models=0.
Rewrite_terms=8669, rewrite_bools=1440, indexes=1147.
Rules_from_neg_clauses=53, cross_offs=834.

============================== 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=118, propagations=540, current_models=0.
Rewrite_terms=11036, rewrite_bools=1700, indexes=1561.
Rules_from_neg_clauses=48, cross_offs=1176.

============================== 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=29, assignments=144, propagations=706, current_models=0.
Rewrite_terms=15627, rewrite_bools=2367, indexes=2015.
Rules_from_neg_clauses=64, cross_offs=1689.

============================== 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=30, assignments=154, propagations=802, current_models=0.
Rewrite_terms=19607, rewrite_bools=2881, indexes=2687.
Rules_from_neg_clauses=62, cross_offs=2193.

============================== 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=33, assignments=186, propagations=1025, current_models=0.
Rewrite_terms=24293, rewrite_bools=3312, indexes=3377.
Rules_from_neg_clauses=88, cross_offs=2946.

============================== 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=34, assignments=198, propagations=1211, current_models=0.
Rewrite_terms=30607, rewrite_bools=4133, indexes=4231.
Rules_from_neg_clauses=79, cross_offs=3721.

============================== 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=37, assignments=236, propagations=1418, current_models=0.
Rewrite_terms=35860, rewrite_bools=4846, indexes=5395.
Rules_from_neg_clauses=77, cross_offs=4684.

============================== 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=37, assignments=237, propagations=1431, current_models=0.
Rewrite_terms=38651, rewrite_bools=4950, indexes=5910.
Rules_from_neg_clauses=71, cross_offs=5492.

============================== 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=3626, kept=3596.
Selections=39, assignments=267, propagations=1855, current_models=0.
Rewrite_terms=46287, rewrite_bools=5400, indexes=7342.
Rules_from_neg_clauses=103, cross_offs=6703.

============================== 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=4379, kept=4347.
Selections=39, assignments=268, propagations=1998, current_models=0.
Rewrite_terms=55397, rewrite_bools=6245, indexes=8330.
Rules_from_neg_clauses=102, cross_offs=8160.

============================== 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=5230, kept=5196.
Selections=41, assignments=302, propagations=2446, current_models=0.
Rewrite_terms=66610, rewrite_bools=7104, indexes=10247.
Rules_from_neg_clauses=136, cross_offs=10120.

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

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

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

For domain size 18.

Current CPU time: 0.00 seconds (total CPU time: 0.17 seconds).
Ground clauses: seen=6185, kept=6149.
Selections=41, assignments=303, propagations=2645, current_models=0.
Rewrite_terms=84355, rewrite_bools=9866, indexes=11541.
Rules_from_neg_clauses=145, cross_offs=11633.

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

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

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

For domain size 19.

Current CPU time: 0.00 seconds (total CPU time: 0.22 seconds).
Ground clauses: seen=7250, kept=7212.
Selections=43, assignments=341, propagations=3170, current_models=0.
Rewrite_terms=89005, rewrite_bools=8737, indexes=13850.
Rules_from_neg_clauses=162, cross_offs=14380.

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

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

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

For domain size 20.

Current CPU time: 0.00 seconds (total CPU time: 0.30 seconds).
Ground clauses: seen=8431, kept=8391.
Selections=43, assignments=342, propagations=3440, current_models=0.
Rewrite_terms=119247, rewrite_bools=13665, indexes=15587.
Rules_from_neg_clauses=190, cross_offs=16767.

============================== 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=9734, kept=9692.
Selections=44, assignments=363, propagations=3530, current_models=0.
Rewrite_terms=127376, rewrite_bools=14313, indexes=17991.
Rules_from_neg_clauses=115, cross_offs=19726.

============================== 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=11165, kept=11121.
Selections=45, assignments=385, propagations=3892, current_models=0.
Rewrite_terms=135976, rewrite_bools=14535, indexes=20301.
Rules_from_neg_clauses=212, cross_offs=23830.

============================== 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=12730, kept=12684.
Selections=45, assignments=385, propagations=3822, current_models=0.
Rewrite_terms=139487, rewrite_bools=14537, indexes=21289.
Rules_from_neg_clauses=131, cross_offs=26342.

============================== 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=14435, kept=14387.
Selections=46, assignments=408, propagations=4208, current_models=0.
Rewrite_terms=148419, rewrite_bools=14861, indexes=23654.
Rules_from_neg_clauses=160, cross_offs=29051.

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

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

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

For domain size 25.

Current CPU time: 0.00 seconds (total CPU time: 0.78 seconds).
Ground clauses: seen=16286, kept=16236.
Selections=47, assignments=432, propagations=4555, current_models=0.
Rewrite_terms=157075, rewrite_bools=15146, indexes=26002.
Rules_from_neg_clauses=161, cross_offs=31199.

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

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

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

For domain size 26.

Current CPU time: 0.00 seconds (total CPU time: 0.91 seconds).
Ground clauses: seen=18289, kept=18237.
Selections=48, assignments=457, propagations=4932, current_models=0.
Rewrite_terms=166654, rewrite_bools=15487, indexes=28609.
Rules_from_neg_clauses=166, cross_offs=33436.

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

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

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

For domain size 27.

Current CPU time: 0.00 seconds (total CPU time: 1.05 seconds).
Ground clauses: seen=20450, kept=20396.
Selections=49, assignments=483, propagations=5361, current_models=0.
Rewrite_terms=176247, rewrite_bools=15833, indexes=31130.
Rules_from_neg_clauses=190, cross_offs=35816.

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

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

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

For domain size 28.

Current CPU time: 0.00 seconds (total CPU time: 1.20 seconds).
Ground clauses: seen=22775, kept=22719.
Selections=50, assignments=510, propagations=5838, current_models=0.
Rewrite_terms=186567, rewrite_bools=16255, indexes=33838.
Rules_from_neg_clauses=205, cross_offs=38319.

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

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

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

For domain size 29.

Current CPU time: 0.00 seconds (total CPU time: 1.38 seconds).
Ground clauses: seen=25270, kept=25212.
Selections=51, assignments=538, propagations=6263, current_models=0.
Rewrite_terms=197274, rewrite_bools=16676, indexes=36684.
Rules_from_neg_clauses=196, cross_offs=40847.

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

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

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

For domain size 30.

Current CPU time: 0.00 seconds (total CPU time: 1.56 seconds).
Ground clauses: seen=27941, kept=27881.
Selections=52, assignments=567, propagations=6841, current_models=0.
Rewrite_terms=209808, rewrite_bools=17213, indexes=39973.
Rules_from_neg_clauses=232, cross_offs=43546.

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

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

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

For domain size 31.

Current CPU time: 0.00 seconds (total CPU time: 1.76 seconds).
Ground clauses: seen=30794, kept=30732.
Selections=53, assignments=597, propagations=7353, current_models=0.
Rewrite_terms=229754, rewrite_bools=18327, indexes=43898.
Rules_from_neg_clauses=222, cross_offs=47617.

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

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

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

For domain size 32.

Current CPU time: 0.00 seconds (total CPU time: 2.00 seconds).
Ground clauses: seen=33835, kept=33771.
Selections=54, assignments=628, propagations=7935, current_models=0.
Rewrite_terms=244157, rewrite_bools=19292, indexes=47039.
Rules_from_neg_clauses=223, cross_offs=50464.

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

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

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

For domain size 33.

Current CPU time: 0.00 seconds (total CPU time: 2.27 seconds).
Ground clauses: seen=37070, kept=37004.
Selections=55, assignments=660, propagations=8482, current_models=0.
Rewrite_terms=260217, rewrite_bools=20495, indexes=50308.
Rules_from_neg_clauses=241, cross_offs=53438.

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

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

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

For domain size 34.

Current CPU time: 0.00 seconds (total CPU time: 2.56 seconds).
Ground clauses: seen=40505, kept=40437.
Selections=56, assignments=693, propagations=9194, current_models=0.
Rewrite_terms=277782, rewrite_bools=21738, indexes=53789.
Rules_from_neg_clauses=279, cross_offs=56501.

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

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

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

For domain size 35.

Current CPU time: 0.00 seconds (total CPU time: 2.89 seconds).
Ground clauses: seen=44146, kept=44076.
Selections=57, assignments=727, propagations=9843, current_models=0.
Rewrite_terms=297256, rewrite_bools=23239, indexes=57471.
Rules_from_neg_clauses=298, cross_offs=59716.

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

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

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

For domain size 36.

Current CPU time: 0.00 seconds (total CPU time: 3.25 seconds).
Ground clauses: seen=47999, kept=47927.
Selections=58, assignments=762, propagations=10565, current_models=0.
Rewrite_terms=317850, rewrite_bools=25013, indexes=61292.
Rules_from_neg_clauses=309, cross_offs=63007.

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

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

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

For domain size 37.

Current CPU time: 0.00 seconds (total CPU time: 3.66 seconds).
Ground clauses: seen=52070, kept=51996.
Selections=59, assignments=798, propagations=11258, current_models=0.
Rewrite_terms=340719, rewrite_bools=27212, indexes=65267.
Rules_from_neg_clauses=323, cross_offs=66337.

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

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

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

For domain size 38.

Current CPU time: 0.00 seconds (total CPU time: 4.11 seconds).
Ground clauses: seen=56365, kept=56289.
Selections=60, assignments=835, propagations=12157, current_models=0.
Rewrite_terms=365111, rewrite_bools=29811, indexes=69324.
Rules_from_neg_clauses=359, cross_offs=69781.

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

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

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

For domain size 39.

Current CPU time: 0.00 seconds (total CPU time: 4.64 seconds).
Ground clauses: seen=60890, kept=60812.
Selections=61, assignments=873, propagations=13080, current_models=0.
Rewrite_terms=393064, rewrite_bools=33340, indexes=73512.
Rules_from_neg_clauses=357, cross_offs=73123.

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

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

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

For domain size 40.

Current CPU time: 0.00 seconds (total CPU time: 5.22 seconds).
Ground clauses: seen=65651, kept=65571.
Selections=62, assignments=912, propagations=14193, current_models=0.
Rewrite_terms=422231, rewrite_bools=37181, indexes=77743.
Rules_from_neg_clauses=362, cross_offs=76535.

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

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

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

For domain size 41.

Current CPU time: 0.00 seconds (total CPU time: 5.88 seconds).
Ground clauses: seen=70654, kept=70572.
Selections=63, assignments=952, propagations=15440, current_models=0.
Rewrite_terms=454233, rewrite_bools=41781, indexes=82050.
Rules_from_neg_clauses=360, cross_offs=79965.

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

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

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

For domain size 42.

Current CPU time: 0.00 seconds (total CPU time: 6.62 seconds).
Ground clauses: seen=75905, kept=75821.
Selections=64, assignments=993, propagations=16785, current_models=0.
Rewrite_terms=488662, rewrite_bools=47136, indexes=86390.
Rules_from_neg_clauses=346, cross_offs=83247.

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

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

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

For domain size 43.

Current CPU time: 0.00 seconds (total CPU time: 7.44 seconds).
Ground clauses: seen=81410, kept=81324.
Selections=65, assignments=1035, propagations=18201, current_models=0.
Rewrite_terms=526475, rewrite_bools=53570, indexes=90743.
Rules_from_neg_clauses=326, cross_offs=86677.

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

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

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

For domain size 44.

Current CPU time: 0.00 seconds (total CPU time: 8.34 seconds).
Ground clauses: seen=87175, kept=87087.
Selections=66, assignments=1078, propagations=19777, current_models=0.
Rewrite_terms=568097, rewrite_bools=61467, indexes=95029.
Rules_from_neg_clauses=300, cross_offs=90113.

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

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

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

For domain size 45.

Current CPU time: 0.00 seconds (total CPU time: 9.36 seconds).
Ground clauses: seen=93206, kept=93116.
Selections=67, assignments=1122, propagations=21435, current_models=0.
Rewrite_terms=612097, rewrite_bools=70147, indexes=99309.
Rules_from_neg_clauses=280, cross_offs=93564.

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

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

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

For domain size 46.

Current CPU time: 0.00 seconds (total CPU time: 10.47 seconds).
Ground clauses: seen=99509, kept=99417.
Selections=68, assignments=1167, propagations=23305, current_models=0.
Rewrite_terms=660516, rewrite_bools=80634, indexes=103436.
Rules_from_neg_clauses=246, cross_offs=97075.

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

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

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

interpretation( 47, [number=1, seconds=11], [

        function(a1, [ 0 ]),

        function(a10, [ 1 ]),

        function(a2, [ 4 ]),

        function(a3, [10 ]),

        function(a4, [21 ]),

        function(a5, [ 5 ]),

        function(a6, [ 3 ]),

        function(a7, [ 2 ]),

        function(a8, [20 ]),

        function(a9, [13 ]),

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

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

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

For domain size 47.

Current CPU time: 0.00 seconds (total CPU time: 11.84 seconds).
Ground clauses: seen=106090, kept=105996.
Selections=69, assignments=1213, propagations=25353, current_models=1.
Rewrite_terms=793533, rewrite_bools=119756, indexes=107557.
Rules_from_neg_clauses=214, cross_offs=100735.

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

User_CPU=11.84, System_CPU=0.01, Wall_clock=12.

Exiting with 1 model.

Process 3284 exit (max_models) Sat Mar 16 17:53:52 2013
The process finished Sat Mar 16 17:53:52 2013