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

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

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

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

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

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

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

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

formulas(mace4_clauses).
x * x = x.
(x * y) * y = x.
(x * y) * z = (x * z) * (y * z).
a2 = a1 * a5.
a3 = a2 * a7.
a4 = a3 * a8.
a5 = a4 * a6.
a6 = a5 * a1.
a7 = a6 * a9.
a8 = a7 * a4.
a9 = a8 * a3.
a1 = a9 * a2.
a1 != a2 | a3 != a2 | a4 != a3 | a4 != a5 | a6 != a5 | a6 != a7 | a8 != a7 | a9 != a8.
end_of_list.

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

% There are no domain elements in the input.

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

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

For domain size 2.

Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
Ground clauses: seen=24, kept=14.
Selections=3, assignments=5, propagations=12, current_models=0.
Rewrite_terms=62, rewrite_bools=19, indexes=0.
Rules_from_neg_clauses=8, cross_offs=8.

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

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

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

For domain size 3.

Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
Ground clauses: seen=49, kept=43.
Selections=5, assignments=11, propagations=40, current_models=0.
Rewrite_terms=413, rewrite_bools=95, indexes=32.
Rules_from_neg_clauses=11, cross_offs=29.

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

============================== DOMAIN SIZE 4 =========================

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

For domain size 4.

Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
Ground clauses: seen=94, kept=86.
Selections=9, assignments=27, propagations=79, current_models=0.
Rewrite_terms=1107, rewrite_bools=239, indexes=119.
Rules_from_neg_clauses=15, cross_offs=74.

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

============================== DOMAIN SIZE 5 =========================

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

For domain size 5.

Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
Ground clauses: seen=165, kept=155.
Selections=14, assignments=53, propagations=143, current_models=0.
Rewrite_terms=2239, rewrite_bools=398, indexes=311.
Rules_from_neg_clauses=18, cross_offs=165.

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

============================== DOMAIN SIZE 6 =========================

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

For domain size 6.

Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
Ground clauses: seen=268, kept=256.
Selections=15, assignments=61, propagations=209, current_models=0.
Rewrite_terms=4053, rewrite_bools=720, indexes=523.
Rules_from_neg_clauses=30, cross_offs=290.

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

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

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

For domain size 7.

Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
Ground clauses: seen=409, kept=395.
Selections=19, assignments=88, propagations=296, current_models=0.
Rewrite_terms=5866, rewrite_bools=991, indexes=866.
Rules_from_neg_clauses=31, cross_offs=474.

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

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

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

For domain size 8.

Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
Ground clauses: seen=594, kept=578.
Selections=19, assignments=89, propagations=364, current_models=0.
Rewrite_terms=7423, rewrite_bools=1125, indexes=1095.
Rules_from_neg_clauses=27, cross_offs=721.

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

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

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

For domain size 9.

Current CPU time: 0.00 seconds (total CPU time: 0.03 seconds).
Ground clauses: seen=829, kept=811.
Selections=22, assignments=116, propagations=495, current_models=0.
Rewrite_terms=11497, rewrite_bools=1784, indexes=1615.
Rules_from_neg_clauses=30, cross_offs=1105.

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

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

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

For domain size 10.

Current CPU time: 0.00 seconds (total CPU time: 0.03 seconds).
Ground clauses: seen=1120, kept=1100.
Selections=22, assignments=117, propagations=599, current_models=0.
Rewrite_terms=15608, rewrite_bools=2418, indexes=2052.
Rules_from_neg_clauses=52, cross_offs=1563.

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

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

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

For domain size 11.

Current CPU time: 0.00 seconds (total CPU time: 0.03 seconds).
Ground clauses: seen=1473, kept=1451.
Selections=27, assignments=170, propagations=936, current_models=0.
Rewrite_terms=22978, rewrite_bools=3505, indexes=3061.
Rules_from_neg_clauses=51, cross_offs=2233.

============================== 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=1894, kept=1870.
Selections=28, assignments=182, propagations=1161, current_models=0.
Rewrite_terms=32730, rewrite_bools=5045, indexes=3894.
Rules_from_neg_clauses=73, cross_offs=3105.

============================== 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=2389, kept=2363.
Selections=34, assignments=257, propagations=1844, current_models=0.
Rewrite_terms=44409, rewrite_bools=6620, indexes=5691.
Rules_from_neg_clauses=101, cross_offs=4280.

============================== 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=2964, kept=2936.
Selections=35, assignments=271, propagations=2073, current_models=0.
Rewrite_terms=58601, rewrite_bools=9241, indexes=6682.
Rules_from_neg_clauses=114, cross_offs=5641.

============================== 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=3625, kept=3595.
Selections=41, assignments=358, propagations=2942, current_models=0.
Rewrite_terms=83711, rewrite_bools=13777, indexes=9095.
Rules_from_neg_clauses=118, cross_offs=7479.

============================== 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=4378, kept=4346.
Selections=42, assignments=374, propagations=3265, current_models=0.
Rewrite_terms=96103, rewrite_bools=14555, indexes=10951.
Rules_from_neg_clauses=140, cross_offs=9467.

============================== 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=5229, kept=5195.
Selections=47, assignments=457, propagations=4134, current_models=0.
Rewrite_terms=128574, rewrite_bools=21239, indexes=14097.
Rules_from_neg_clauses=144, cross_offs=12094.

============================== 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=6184, kept=6148.
Selections=48, assignments=475, propagations=4439, current_models=0.
Rewrite_terms=146893, rewrite_bools=23586, indexes=16384.
Rules_from_neg_clauses=131, cross_offs=14724.

============================== 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=7249, kept=7211.
Selections=51, assignments=531, propagations=5186, current_models=0.
Rewrite_terms=183405, rewrite_bools=29837, indexes=19792.
Rules_from_neg_clauses=216, cross_offs=18851.

============================== 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=8430, kept=8390.
Selections=51, assignments=532, propagations=5369, current_models=0.
Rewrite_terms=217161, rewrite_bools=35098, indexes=22974.
Rules_from_neg_clauses=174, cross_offs=22225.

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

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

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

For domain size 21.

Current CPU time: 0.00 seconds (total CPU time: 0.64 seconds).
Ground clauses: seen=9733, kept=9691.
Selections=53, assignments=574, propagations=6024, current_models=0.
Rewrite_terms=232350, rewrite_bools=35117, indexes=26319.
Rules_from_neg_clauses=194, cross_offs=25977.

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

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

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

For domain size 22.

Current CPU time: 0.00 seconds (total CPU time: 0.80 seconds).
Ground clauses: seen=11164, kept=11120.
Selections=53, assignments=575, propagations=6265, current_models=0.
Rewrite_terms=244227, rewrite_bools=35560, indexes=29363.
Rules_from_neg_clauses=172, cross_offs=30116.

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

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

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

For domain size 23.

Current CPU time: 0.00 seconds (total CPU time: 1.00 seconds).
Ground clauses: seen=12729, kept=12683.
Selections=55, assignments=621, propagations=7335, current_models=0.
Rewrite_terms=287781, rewrite_bools=39604, indexes=34094.
Rules_from_neg_clauses=250, cross_offs=36007.

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

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

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

For domain size 24.

Current CPU time: 0.00 seconds (total CPU time: 1.23 seconds).
Ground clauses: seen=14434, kept=14386.
Selections=55, assignments=622, propagations=7471, current_models=0.
Rewrite_terms=321210, rewrite_bools=43853, indexes=37103.
Rules_from_neg_clauses=217, cross_offs=40362.

============================== 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=16285, kept=16235.
Selections=57, assignments=672, propagations=8434, current_models=0.
Rewrite_terms=328310, rewrite_bools=41444, indexes=42029.
Rules_from_neg_clauses=259, cross_offs=46254.

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

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

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

For domain size 26.

Current CPU time: 0.00 seconds (total CPU time: 1.75 seconds).
Ground clauses: seen=18288, kept=18236.
Selections=57, assignments=673, propagations=8861, current_models=0.
Rewrite_terms=360646, rewrite_bools=43943, indexes=45838.
Rules_from_neg_clauses=261, cross_offs=52454.

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

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

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

For domain size 27.

Current CPU time: 0.00 seconds (total CPU time: 2.09 seconds).
Ground clauses: seen=20449, kept=20395.
Selections=59, assignments=727, propagations=10179, current_models=0.
Rewrite_terms=407468, rewrite_bools=48880, indexes=51729.
Rules_from_neg_clauses=357, cross_offs=59605.

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

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

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

For domain size 28.

Current CPU time: 0.00 seconds (total CPU time: 2.52 seconds).
Ground clauses: seen=22774, kept=22718.
Selections=59, assignments=728, propagations=10449, current_models=0.
Rewrite_terms=461364, rewrite_bools=56751, indexes=56190.
Rules_from_neg_clauses=298, cross_offs=66480.

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

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

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

For domain size 29.

Current CPU time: 0.00 seconds (total CPU time: 3.02 seconds).
Ground clauses: seen=25269, kept=25211.
Selections=61, assignments=786, propagations=11727, current_models=0.
Rewrite_terms=523291, rewrite_bools=63324, indexes=63989.
Rules_from_neg_clauses=333, cross_offs=76373.

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

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

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

For domain size 30.

Current CPU time: 0.00 seconds (total CPU time: 3.53 seconds).
Ground clauses: seen=27940, kept=27880.
Selections=61, assignments=787, propagations=11935, current_models=0.
Rewrite_terms=544384, rewrite_bools=64583, indexes=68061.
Rules_from_neg_clauses=369, cross_offs=83646.

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

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

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

For domain size 31.

Current CPU time: 0.00 seconds (total CPU time: 4.19 seconds).
Ground clauses: seen=30793, kept=30731.
Selections=63, assignments=849, propagations=13705, current_models=0.
Rewrite_terms=635242, rewrite_bools=81023, indexes=76009.
Rules_from_neg_clauses=395, cross_offs=91573.

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

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

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

For domain size 32.

Current CPU time: 0.00 seconds (total CPU time: 4.83 seconds).
Ground clauses: seen=33834, kept=33770.
Selections=63, assignments=850, propagations=14125, current_models=0.
Rewrite_terms=619265, rewrite_bools=67599, indexes=81500.
Rules_from_neg_clauses=397, cross_offs=102711.

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

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

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

For domain size 33.

Current CPU time: 0.00 seconds (total CPU time: 5.64 seconds).
Ground clauses: seen=37069, kept=37003.
Selections=65, assignments=916, propagations=16016, current_models=0.
Rewrite_terms=721053, rewrite_bools=78976, indexes=89940.
Rules_from_neg_clauses=456, cross_offs=113157.

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

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

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

For domain size 34.

Current CPU time: 0.00 seconds (total CPU time: 6.45 seconds).
Ground clauses: seen=40504, kept=40436.
Selections=65, assignments=917, propagations=16515, current_models=0.
Rewrite_terms=723534, rewrite_bools=73916, indexes=96208.
Rules_from_neg_clauses=443, cross_offs=125679.

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

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

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

For domain size 35.

Current CPU time: 0.00 seconds (total CPU time: 7.48 seconds).
Ground clauses: seen=44145, kept=44075.
Selections=67, assignments=987, propagations=18687, current_models=0.
Rewrite_terms=847591, rewrite_bools=87395, indexes=106259.
Rules_from_neg_clauses=497, cross_offs=140508.

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

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

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

For domain size 36.

Current CPU time: 0.00 seconds (total CPU time: 8.48 seconds).
Ground clauses: seen=47998, kept=47926.
Selections=67, assignments=988, propagations=18495, current_models=0.
Rewrite_terms=819189, rewrite_bools=79926, indexes=111477.
Rules_from_neg_clauses=383, cross_offs=151309.

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

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

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

For domain size 37.

Current CPU time: 0.00 seconds (total CPU time: 9.72 seconds).
Ground clauses: seen=52069, kept=51995.
Selections=68, assignments=1025, propagations=19823, current_models=0.
Rewrite_terms=958062, rewrite_bools=99337, indexes=122733.
Rules_from_neg_clauses=410, cross_offs=164796.

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

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

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

For domain size 38.

Current CPU time: 0.00 seconds (total CPU time: 11.14 seconds).
Ground clauses: seen=56364, kept=56288.
Selections=68, assignments=1025, propagations=20014, current_models=0.
Rewrite_terms=1044484, rewrite_bools=113195, indexes=131131.
Rules_from_neg_clauses=382, cross_offs=177279.

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

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

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

For domain size 39.

Current CPU time: 0.00 seconds (total CPU time: 12.84 seconds).
Ground clauses: seen=60889, kept=60811.
Selections=69, assignments=1063, propagations=21715, current_models=0.
Rewrite_terms=1166879, rewrite_bools=131917, indexes=144014.
Rules_from_neg_clauses=499, cross_offs=188060.

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

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

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

For domain size 40.

Current CPU time: 0.00 seconds (total CPU time: 14.62 seconds).
Ground clauses: seen=65650, kept=65570.
Selections=70, assignments=1102, propagations=22989, current_models=0.
Rewrite_terms=1213114, rewrite_bools=138063, indexes=151749.
Rules_from_neg_clauses=478, cross_offs=195398.

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

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

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

For domain size 41.

Current CPU time: 0.00 seconds (total CPU time: 16.56 seconds).
Ground clauses: seen=70653, kept=70571.
Selections=71, assignments=1142, propagations=24339, current_models=0.
Rewrite_terms=1261483, rewrite_bools=144902, indexes=159482.
Rules_from_neg_clauses=461, cross_offs=202608.

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

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

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

For domain size 42.

Current CPU time: 0.00 seconds (total CPU time: 18.58 seconds).
Ground clauses: seen=75904, kept=75820.
Selections=72, assignments=1183, propagations=25930, current_models=0.
Rewrite_terms=1313832, rewrite_bools=153337, indexes=167083.
Rules_from_neg_clauses=434, cross_offs=209892.

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

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

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

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

        function(a1, [ 0 ]),

        function(a2, [ 1 ]),

        function(a3, [28 ]),

        function(a4, [ 7 ]),

        function(a5, [ 2 ]),

        function(a6, [ 6 ]),

        function(a7, [18 ]),

        function(a8, [36 ]),

        function(a9, [ 3 ]),

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

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

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

For domain size 43.

Current CPU time: 0.00 seconds (total CPU time: 20.83 seconds).
Ground clauses: seen=81409, kept=81323.
Selections=73, assignments=1225, propagations=27629, current_models=1.
Rewrite_terms=1436677, rewrite_bools=185565, indexes=174689.
Rules_from_neg_clauses=403, cross_offs=217309.

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

User_CPU=20.83, System_CPU=0.01, Wall_clock=20.

Exiting with 1 model.

Process 3756 exit (max_models) Sat Mar 16 02:57:05 2013
The process finished Sat Mar 16 02:57:05 2013