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

============================== end of clauses for search =============

% There are no domain elements in the input.

============================== DOMAIN SIZE 2 =========================

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

For domain size 2.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=25, kept=15.
Selections=5, assignments=9, propagations=13, current_models=0.
Rewrite_terms=78, rewrite_bools=23, indexes=0.
Rules_from_neg_clauses=9, cross_offs=9.

============================== 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=57, current_models=0.
Rewrite_terms=591, rewrite_bools=131, indexes=50.
Rules_from_neg_clauses=26, cross_offs=55.

============================== 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=95, current_models=0.
Rewrite_terms=1419, rewrite_bools=301, indexes=178.
Rules_from_neg_clauses=28, cross_offs=116.

============================== 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=19, assignments=68, propagations=197, current_models=0.
Rewrite_terms=3111, rewrite_bools=553, indexes=452.
Rules_from_neg_clauses=37, cross_offs=262.

============================== 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=20, assignments=76, propagations=272, current_models=0.
Rewrite_terms=5016, rewrite_bools=845, indexes=698.
Rules_from_neg_clauses=45, cross_offs=492.

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

============================== DOMAIN SIZE 7 =========================

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

For domain size 7.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=410, kept=396.
Selections=24, assignments=103, propagations=379, current_models=0.
Rewrite_terms=7451, rewrite_bools=1232, indexes=1046.
Rules_from_neg_clauses=47, cross_offs=707.

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

============================== DOMAIN SIZE 8 =========================

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

For domain size 8.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=595, kept=579.
Selections=24, assignments=104, propagations=424, current_models=0.
Rewrite_terms=9072, rewrite_bools=1384, indexes=1314.
Rules_from_neg_clauses=55, cross_offs=1005.

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

============================== DOMAIN SIZE 9 =========================

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

For domain size 9.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=830, kept=812.
Selections=29, assignments=147, propagations=689, current_models=0.
Rewrite_terms=16449, rewrite_bools=2701, indexes=2019.
Rules_from_neg_clauses=70, cross_offs=1570.

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

============================== DOMAIN SIZE 10 ========================

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

For domain size 10.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=1121, kept=1101.
Selections=31, assignments=167, propagations=773, current_models=0.
Rewrite_terms=20029, rewrite_bools=3089, indexes=2625.
Rules_from_neg_clauses=78, cross_offs=2157.

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

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

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

For domain size 11.

Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
Ground clauses: seen=1474, kept=1452.
Selections=34, assignments=199, propagations=981, current_models=0.
Rewrite_terms=27279, rewrite_bools=4337, indexes=3557.
Rules_from_neg_clauses=78, cross_offs=2898.

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

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

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

For domain size 12.

Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
Ground clauses: seen=1895, kept=1871.
Selections=36, assignments=222, propagations=1210, current_models=0.
Rewrite_terms=37422, rewrite_bools=6392, indexes=4286.
Rules_from_neg_clauses=101, cross_offs=3853.

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

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

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

For domain size 13.

Current CPU time: 0.00 seconds (total CPU time: 0.03 seconds).
Ground clauses: seen=2390, kept=2364.
Selections=41, assignments=285, propagations=1580, current_models=0.
Rewrite_terms=44618, rewrite_bools=6675, indexes=6021.
Rules_from_neg_clauses=130, cross_offs=5078.

============================== 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=41, assignments=286, propagations=1726, current_models=0.
Rewrite_terms=56660, rewrite_bools=8410, indexes=7126.
Rules_from_neg_clauses=108, cross_offs=6748.

============================== 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=43, assignments=316, propagations=2096, current_models=0.
Rewrite_terms=70056, rewrite_bools=10129, indexes=8791.
Rules_from_neg_clauses=157, cross_offs=8704.

============================== 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=43, assignments=317, propagations=2216, current_models=0.
Rewrite_terms=78651, rewrite_bools=10772, indexes=10044.
Rules_from_neg_clauses=121, cross_offs=10272.

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

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

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

For domain size 17.

Current CPU time: 0.00 seconds (total CPU time: 0.16 seconds).
Ground clauses: seen=5230, kept=5196.
Selections=46, assignments=367, propagations=2712, current_models=0.
Rewrite_terms=92330, rewrite_bools=12065, indexes=12167.
Rules_from_neg_clauses=161, cross_offs=12610.

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

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

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

For domain size 18.

Current CPU time: 0.00 seconds (total CPU time: 0.22 seconds).
Ground clauses: seen=6185, kept=6149.
Selections=46, assignments=368, propagations=2927, current_models=0.
Rewrite_terms=115967, rewrite_bools=16061, indexes=14415.
Rules_from_neg_clauses=171, cross_offs=14814.

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

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

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

For domain size 19.

Current CPU time: 0.00 seconds (total CPU time: 0.30 seconds).
Ground clauses: seen=7250, kept=7212.
Selections=50, assignments=443, propagations=3639, current_models=0.
Rewrite_terms=133361, rewrite_bools=17945, indexes=17057.
Rules_from_neg_clauses=219, cross_offs=17690.

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

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

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

For domain size 20.

Current CPU time: 0.00 seconds (total CPU time: 0.39 seconds).
Ground clauses: seen=8431, kept=8391.
Selections=51, assignments=463, propagations=3976, current_models=0.
Rewrite_terms=169051, rewrite_bools=24247, indexes=19659.
Rules_from_neg_clauses=189, cross_offs=20904.

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

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

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

For domain size 21.

Current CPU time: 0.00 seconds (total CPU time: 0.52 seconds).
Ground clauses: seen=9734, kept=9692.
Selections=55, assignments=546, propagations=5133, current_models=0.
Rewrite_terms=197765, rewrite_bools=27487, indexes=24166.
Rules_from_neg_clauses=347, cross_offs=26017.

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

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

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

For domain size 22.

Current CPU time: 0.00 seconds (total CPU time: 0.67 seconds).
Ground clauses: seen=11165, kept=11121.
Selections=56, assignments=568, propagations=5542, current_models=0.
Rewrite_terms=234411, rewrite_bools=33617, indexes=27035.
Rules_from_neg_clauses=240, cross_offs=29533.

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

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

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

For domain size 23.

Current CPU time: 0.00 seconds (total CPU time: 0.89 seconds).
Ground clauses: seen=12730, kept=12684.
Selections=61, assignments=681, propagations=7237, current_models=0.
Rewrite_terms=293547, rewrite_bools=44471, indexes=32769.
Rules_from_neg_clauses=667, cross_offs=37761.

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

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

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

For domain size 24.

Current CPU time: 0.00 seconds (total CPU time: 1.14 seconds).
Ground clauses: seen=14435, kept=14387.
Selections=63, assignments=728, propagations=7545, current_models=0.
Rewrite_terms=324366, rewrite_bools=45635, indexes=37453.
Rules_from_neg_clauses=340, cross_offs=44956.

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

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

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

For domain size 25.

Current CPU time: 0.00 seconds (total CPU time: 1.47 seconds).
Ground clauses: seen=16286, kept=16236.
Selections=67, assignments=826, propagations=9127, current_models=0.
Rewrite_terms=407847, rewrite_bools=61928, indexes=44321.
Rules_from_neg_clauses=350, cross_offs=52610.

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

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

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

For domain size 26.

Current CPU time: 0.00 seconds (total CPU time: 1.89 seconds).
Ground clauses: seen=18289, kept=18237.
Selections=68, assignments=852, propagations=9803, current_models=0.
Rewrite_terms=479407, rewrite_bools=75003, indexes=50761.
Rules_from_neg_clauses=374, cross_offs=60784.

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

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

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

For domain size 27.

Current CPU time: 0.00 seconds (total CPU time: 2.31 seconds).
Ground clauses: seen=20450, kept=20396.
Selections=69, assignments=879, propagations=10002, current_models=0.
Rewrite_terms=486826, rewrite_bools=71034, indexes=55972.
Rules_from_neg_clauses=332, cross_offs=68284.

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

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

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

For domain size 28.

Current CPU time: 0.00 seconds (total CPU time: 2.75 seconds).
Ground clauses: seen=22775, kept=22719.
Selections=69, assignments=879, propagations=9931, current_models=0.
Rewrite_terms=499703, rewrite_bools=71103, indexes=59691.
Rules_from_neg_clauses=253, cross_offs=75434.

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

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

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

For domain size 29.

Current CPU time: 0.00 seconds (total CPU time: 3.27 seconds).
Ground clauses: seen=25270, kept=25212.
Selections=70, assignments=907, propagations=10472, current_models=0.
Rewrite_terms=525064, rewrite_bools=72186, indexes=65478.
Rules_from_neg_clauses=350, cross_offs=81948.

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

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

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

For domain size 30.

Current CPU time: 0.00 seconds (total CPU time: 3.80 seconds).
Ground clauses: seen=27941, kept=27881.
Selections=71, assignments=936, propagations=10978, current_models=0.
Rewrite_terms=545068, rewrite_bools=72934, indexes=70436.
Rules_from_neg_clauses=365, cross_offs=86977.

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

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

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

For domain size 31.

Current CPU time: 0.00 seconds (total CPU time: 4.39 seconds).
Ground clauses: seen=30794, kept=30732.
Selections=72, assignments=966, propagations=11484, current_models=0.
Rewrite_terms=566727, rewrite_bools=73966, indexes=75554.
Rules_from_neg_clauses=377, cross_offs=92099.

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

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

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

For domain size 32.

Current CPU time: 0.00 seconds (total CPU time: 5.01 seconds).
Ground clauses: seen=33835, kept=33771.
Selections=73, assignments=997, propagations=12254, current_models=0.
Rewrite_terms=590256, rewrite_bools=75216, indexes=80908.
Rules_from_neg_clauses=420, cross_offs=97226.

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

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

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

For domain size 33.

Current CPU time: 0.00 seconds (total CPU time: 5.70 seconds).
Ground clauses: seen=37070, kept=37004.
Selections=74, assignments=1029, propagations=12987, current_models=0.
Rewrite_terms=615103, rewrite_bools=76680, indexes=86370.
Rules_from_neg_clauses=437, cross_offs=102476.

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

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

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

For domain size 34.

Current CPU time: 0.00 seconds (total CPU time: 6.42 seconds).
Ground clauses: seen=40505, kept=40437.
Selections=75, assignments=1062, propagations=13747, current_models=0.
Rewrite_terms=641883, rewrite_bools=78454, indexes=91990.
Rules_from_neg_clauses=455, cross_offs=107841.

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

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

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

For domain size 35.

Current CPU time: 0.00 seconds (total CPU time: 7.20 seconds).
Ground clauses: seen=44146, kept=44076.
Selections=76, assignments=1096, propagations=14480, current_models=0.
Rewrite_terms=669865, rewrite_bools=80767, indexes=97641.
Rules_from_neg_clauses=460, cross_offs=113297.

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

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

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

For domain size 36.

Current CPU time: 0.00 seconds (total CPU time: 8.05 seconds).
Ground clauses: seen=47999, kept=47927.
Selections=77, assignments=1131, propagations=15303, current_models=0.
Rewrite_terms=700975, rewrite_bools=83842, indexes=103417.
Rules_from_neg_clauses=456, cross_offs=118546.

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

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

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

For domain size 37.

Current CPU time: 0.00 seconds (total CPU time: 8.95 seconds).
Ground clauses: seen=52070, kept=51996.
Selections=78, assignments=1167, propagations=16168, current_models=0.
Rewrite_terms=732692, rewrite_bools=87112, indexes=109191.
Rules_from_neg_clauses=460, cross_offs=123927.

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

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

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

For domain size 38.

Current CPU time: 0.00 seconds (total CPU time: 9.94 seconds).
Ground clauses: seen=56365, kept=56289.
Selections=79, assignments=1204, propagations=17202, current_models=0.
Rewrite_terms=767022, rewrite_bools=91080, indexes=115055.
Rules_from_neg_clauses=447, cross_offs=129445.

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

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

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

For domain size 39.

Current CPU time: 0.00 seconds (total CPU time: 11.00 seconds).
Ground clauses: seen=60890, kept=60812.
Selections=80, assignments=1242, propagations=18339, current_models=0.
Rewrite_terms=804332, rewrite_bools=95969, indexes=120938.
Rules_from_neg_clauses=438, cross_offs=134824.

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

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

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

For domain size 40.

Current CPU time: 0.00 seconds (total CPU time: 12.14 seconds).
Ground clauses: seen=65651, kept=65571.
Selections=81, assignments=1281, propagations=19673, current_models=0.
Rewrite_terms=845308, rewrite_bools=102174, indexes=126805.
Rules_from_neg_clauses=422, cross_offs=140273.

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

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

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

For domain size 41.

Current CPU time: 0.00 seconds (total CPU time: 13.36 seconds).
Ground clauses: seen=70654, kept=70572.
Selections=82, assignments=1321, propagations=21124, current_models=0.
Rewrite_terms=887860, rewrite_bools=108921, indexes=132645.
Rules_from_neg_clauses=400, cross_offs=145681.

============================== 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=1362, propagations=22532, current_models=0.
Rewrite_terms=934065, rewrite_bools=117054, indexes=138409.
Rules_from_neg_clauses=371, cross_offs=151224.

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

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

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

interpretation( 43, [number=1, seconds=16], [

        function(a1, [ 0 ]),

        function(a10, [ 1 ]),

        function(a2, [ 2 ]),

        function(a3, [26 ]),

        function(a4, [13 ]),

        function(a5, [ 5 ]),

        function(a6, [ 3 ]),

        function(a7, [12 ]),

        function(a8, [25 ]),

        function(a9, [23 ]),

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

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

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

For domain size 43.

Current CPU time: 0.00 seconds (total CPU time: 16.22 seconds).
Ground clauses: seen=81410, kept=81324.
Selections=84, assignments=1404, propagations=24244, current_models=1.
Rewrite_terms=1052007, rewrite_bools=149617, indexes=144079.
Rules_from_neg_clauses=342, cross_offs=156845.

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

User_CPU=16.22, System_CPU=0.03, Wall_clock=16.

Exiting with 1 model.

Process 1428 exit (max_models) Sat Mar 16 17:51:56 2013
The process finished Sat Mar 16 17:51:56 2013