============================== Mace4 =================================
Mace4 (32) version Dec-2007, Dec 2007.
Process 1500 was started by Alexei on Alexei-PC,
Mon Mar 25 22:36:13 2013
The command was "/cygdrive/c/Program Files (x86)/Prover9-Mace4/bin-win32/mace4 -c".
============================== end of head ===========================

============================== INPUT =================================
assign(report_stderr,2).
set(ignore_option_dependencies).
if(Prover9).
% Conditional input omitted.
end_if.
if(Mace4).
% Conditional input included.
assign(max_seconds,-1).
assign(max_megs,1800).
end_if.

formulas(assumptions).
x * x = x.
(x * y) * y = x.
(x * y) * z = (x * z) * (y * z).
a2 = a1 * a5.
a3 = a2 * a8.
a4 = a3 * a10.
a5 = a4 * a7.
a6 = a5 * a1.
a7 = a6 * a9.
a8 = a7 * a2.
a9 = a8 * a4.
a10 = a9 * a6.
a1 = a10 * a3.
end_of_list.

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

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

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

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

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

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

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

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

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

% There are no domain elements in the input.

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

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

For domain size 2.

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

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

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

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

For domain size 3.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=50, kept=44.
Selections=9, assignments=21, propagations=77, current_models=0.
Rewrite_terms=804, rewrite_bools=185, indexes=55.
Rules_from_neg_clauses=28, cross_offs=60.

============================== 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=20, assignments=65, propagations=171, current_models=0.
Rewrite_terms=2196, rewrite_bools=436, indexes=233.
Rules_from_neg_clauses=34, cross_offs=162.

============================== 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=28, assignments=102, propagations=287, current_models=0.
Rewrite_terms=4418, rewrite_bools=777, indexes=589.
Rules_from_neg_clauses=56, cross_offs=392.

============================== 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=51, assignments=230, propagations=626, current_models=0.
Rewrite_terms=11897, rewrite_bools=2193, indexes=1369.
Rules_from_neg_clauses=124, cross_offs=1041.

============================== 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=71, assignments=361, propagations=993, current_models=0.
Rewrite_terms=18592, rewrite_bools=3004, indexes=2740.
Rules_from_neg_clauses=153, cross_offs=1801.

============================== 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=115, assignments=687, propagations=1784, current_models=0.
Rewrite_terms=34012, rewrite_bools=4767, indexes=5522.
Rules_from_neg_clauses=278, cross_offs=3593.

============================== 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=830, kept=812.
Selections=153, assignments=1012, propagations=2846, current_models=0.
Rewrite_terms=62023, rewrite_bools=9006, indexes=9449.
Rules_from_neg_clauses=291, cross_offs=6398.

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

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

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

For domain size 10.

Current CPU time: 0.00 seconds (total CPU time: 0.05 seconds).
Ground clauses: seen=1121, kept=1101.
Selections=209, assignments=1548, propagations=4491, current_models=0.
Rewrite_terms=101421, rewrite_bools=13618, indexes=16172.
Rules_from_neg_clauses=474, cross_offs=11036.

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

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

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

For domain size 11.

Current CPU time: 0.00 seconds (total CPU time: 0.08 seconds).
Ground clauses: seen=1474, kept=1452.
Selections=280, assignments=2284, propagations=6682, current_models=0.
Rewrite_terms=152164, rewrite_bools=18623, indexes=27098.
Rules_from_neg_clauses=664, cross_offs=18392.

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

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

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

For domain size 12.

Current CPU time: 0.00 seconds (total CPU time: 0.12 seconds).
Ground clauses: seen=1895, kept=1871.
Selections=364, assignments=3251, propagations=9636, current_models=0.
Rewrite_terms=237655, rewrite_bools=28934, indexes=39709.
Rules_from_neg_clauses=760, cross_offs=30144.

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

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

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

For domain size 13.

Current CPU time: 0.00 seconds (total CPU time: 0.19 seconds).
Ground clauses: seen=2390, kept=2364.
Selections=453, assignments=4372, propagations=13976, current_models=0.
Rewrite_terms=344875, rewrite_bools=38847, indexes=60693.
Rules_from_neg_clauses=898, cross_offs=46465.

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

============================== DOMAIN SIZE 14 ========================

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

For domain size 14.

Current CPU time: 0.00 seconds (total CPU time: 0.31 seconds).
Ground clauses: seen=2965, kept=2937.
Selections=588, assignments=6197, propagations=20552, current_models=0.
Rewrite_terms=519691, rewrite_bools=55637, indexes=93403.
Rules_from_neg_clauses=1406, cross_offs=72243.

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

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

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

For domain size 15.

Current CPU time: 0.00 seconds (total CPU time: 0.52 seconds).
Ground clauses: seen=3626, kept=3596.
Selections=720, assignments=8126, propagations=28662, current_models=0.
Rewrite_terms=764264, rewrite_bools=80819, indexes=136697.
Rules_from_neg_clauses=1499, cross_offs=111836.

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

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

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

For domain size 16.

Current CPU time: 0.00 seconds (total CPU time: 0.80 seconds).
Ground clauses: seen=4379, kept=4347.
Selections=887, assignments=10746, propagations=39692, current_models=0.
Rewrite_terms=1077804, rewrite_bools=107069, indexes=195989.
Rules_from_neg_clauses=2082, cross_offs=169194.

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

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

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

For domain size 17.

Current CPU time: 0.00 seconds (total CPU time: 1.28 seconds).
Ground clauses: seen=5230, kept=5196.
Selections=1144, assignments=15032, propagations=59493, current_models=0.
Rewrite_terms=1601909, rewrite_bools=146044, indexes=314046.
Rules_from_neg_clauses=3065, cross_offs=268964.

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

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

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

For domain size 18.

Current CPU time: 0.00 seconds (total CPU time: 2.03 seconds).
Ground clauses: seen=6185, kept=6149.
Selections=1423, assignments=19998, propagations=82410, current_models=0.
Rewrite_terms=2309419, rewrite_bools=205913, indexes=460348.
Rules_from_neg_clauses=3969, cross_offs=420613.

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

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

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

For domain size 19.

Current CPU time: 0.00 seconds (total CPU time: 3.20 seconds).
Ground clauses: seen=7250, kept=7212.
Selections=1811, assignments=27283, propagations=120370, current_models=0.
Rewrite_terms=3412224, rewrite_bools=284828, indexes=712955.
Rules_from_neg_clauses=5382, cross_offs=671631.

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

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

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

For domain size 20.

Current CPU time: 0.00 seconds (total CPU time: 5.11 seconds).
Ground clauses: seen=8431, kept=8391.
Selections=2386, assignments=38648, propagations=179086, current_models=0.
Rewrite_terms=5095233, rewrite_bools=399306, indexes=1104210.
Rules_from_neg_clauses=8145, cross_offs=1083232.

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

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

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

For domain size 21.

Current CPU time: 0.00 seconds (total CPU time: 8.03 seconds).
Ground clauses: seen=9734, kept=9692.
Selections=3051, assignments=52499, propagations=255385, current_models=0.
Rewrite_terms=7368743, rewrite_bools=555220, indexes=1645443.
Rules_from_neg_clauses=10305, cross_offs=1666598.

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

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

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

For domain size 22.

Current CPU time: 0.00 seconds (total CPU time: 12.58 seconds).
Ground clauses: seen=11165, kept=11121.
Selections=3897, assignments=70941, propagations=363039, current_models=0.
Rewrite_terms=10623472, rewrite_bools=770001, indexes=2426314.
Rules_from_neg_clauses=14397, cross_offs=2543946.

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

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

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

For domain size 23.

Current CPU time: 0.00 seconds (total CPU time: 19.36 seconds).
Ground clauses: seen=12730, kept=12684.
Selections=5039, assignments=96936, propagations=514521, current_models=0.
Rewrite_terms=15056710, rewrite_bools=1040207, indexes=3540570.
Rules_from_neg_clauses=19266, cross_offs=3772133.

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

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

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

For domain size 24.

Current CPU time: 0.00 seconds (total CPU time: 30.34 seconds).
Ground clauses: seen=14435, kept=14387.
Selections=6464, assignments=130862, propagations=721275, current_models=0.
Rewrite_terms=21409179, rewrite_bools=1436391, indexes=5129593.
Rules_from_neg_clauses=26036, cross_offs=5583179.

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

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

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

For domain size 25.

Current CPU time: 0.00 seconds (total CPU time: 45.47 seconds).
Ground clauses: seen=16286, kept=16236.
Selections=8207, assignments=174150, propagations=992065, current_models=0.
Rewrite_terms=29536236, rewrite_bools=1912778, indexes=7231952.
Rules_from_neg_clauses=33223, cross_offs=8030214.

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

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

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

For domain size 26.

Current CPU time: 0.00 seconds (total CPU time: 68.59 seconds).
Ground clauses: seen=18289, kept=18237.
Selections=10516, assignments=233693, propagations=1375853, current_models=0.
Rewrite_terms=41367452, rewrite_bools=2611938, indexes=10269310.
Rules_from_neg_clauses=45531, cross_offs=11644234.

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

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

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

For domain size 27.

Current CPU time: 0.00 seconds (total CPU time: 101.59 seconds).
Ground clauses: seen=20450, kept=20396.
Selections=13298, assignments=308299, propagations=1866694, current_models=0.
Rewrite_terms=56225087, rewrite_bools=3460157, indexes=14172677.
Rules_from_neg_clauses=57206, cross_offs=16312080.

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

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

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

For domain size 28.

Current CPU time: 0.00 seconds (total CPU time: 147.34 seconds).
Ground clauses: seen=22775, kept=22719.
Selections=16968, assignments=410358, propagations=2567539, current_models=0.
Rewrite_terms=78177503, rewrite_bools=4724219, indexes=19912290.
Rules_from_neg_clauses=76558, cross_offs=23374699.

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

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

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

For domain size 29.

Current CPU time: 0.00 seconds (total CPU time: 207.39 seconds).
Ground clauses: seen=25270, kept=25212.
Selections=21379, assignments=537571, propagations=3431698, current_models=0.
Rewrite_terms=104041324, rewrite_bools=6110462, indexes=26863262.
Rules_from_neg_clauses=96292, cross_offs=31985124.

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

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

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

For domain size 30.

Current CPU time: 0.00 seconds (total CPU time: 293.38 seconds).
Ground clauses: seen=27941, kept=27881.
Selections=27087, assignments=707834, propagations=4647427, current_models=0.
Rewrite_terms=142294018, rewrite_bools=8242591, indexes=37044734.
Rules_from_neg_clauses=126465, cross_offs=45142002.

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

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

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

For domain size 31.

Current CPU time: 0.00 seconds (total CPU time: 416.01 seconds).
Ground clauses: seen=30794, kept=30732.
Selections=34060, assignments=923105, propagations=6160973, current_models=0.
Rewrite_terms=188019833, rewrite_bools=10663489, indexes=49469806.
Rules_from_neg_clauses=155748, cross_offs=61051344.

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

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

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

For domain size 32.

Current CPU time: 0.00 seconds (total CPU time: 605.86 seconds).
Ground clauses: seen=33835, kept=33771.
Selections=44011, assignments=1240182, propagations=8426026, current_models=0.
Rewrite_terms=259439293, rewrite_bools=14630076, indexes=68596455.
Rules_from_neg_clauses=212806, cross_offs=86074272.

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

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

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

For domain size 33.

Current CPU time: 0.00 seconds (total CPU time: 875.08 seconds).
Ground clauses: seen=37070, kept=37004.
Selections=57211, assignments=1675343, propagations=11478105, current_models=0.
Rewrite_terms=350689596, rewrite_bools=19439672, indexes=93460292.
Rules_from_neg_clauses=272882, cross_offs=118799042.

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

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

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

For domain size 34.

Current CPU time: 0.00 seconds (total CPU time: 1274.66 seconds).
Ground clauses: seen=40505, kept=40437.
Selections=86035, assignments=2655391, propagations=18044620, current_models=0.
Rewrite_terms=530046243, rewrite_bools=29039401, indexes=142625650.
Rules_from_neg_clauses=426031, cross_offs=178979770.

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

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

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

For domain size 35.

Current CPU time: 0.00 seconds (total CPU time: 1876.19 seconds).
Ground clauses: seen=44146, kept=44076.
Selections=160876, assignments=5285180, propagations=35388127, current_models=0.
Rewrite_terms=931066846, rewrite_bools=49918487, indexes=256954377.
Rules_from_neg_clauses=777143, cross_offs=298391409.

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

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

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

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

        function(a1, [ 0 ]),

        function(a10, [ 1 ]),

        function(a2, [ 5 ]),

        function(a3, [ 2 ]),

        function(a4, [ 4 ]),

        function(a5, [ 6 ]),

        function(a6, [ 9 ]),

        function(a7, [ 8 ]),

        function(a8, [ 7 ]),

        function(a9, [11 ]),

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

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

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

For domain size 36.

Current CPU time: 0.00 seconds (total CPU time: 2460.20 seconds).
Ground clauses: seen=47999, kept=47927.
Selections=260355, assignments=9264353, propagations=59899191, current_models=1.
Rewrite_terms=1213013994, rewrite_bools=65789343, indexes=353935640.
Rules_from_neg_clauses=1143070, cross_offs=282172342.

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

User_CPU=2460.20, System_CPU=2.75, Wall_clock=2478.

Exiting with 1 model.

Process 1500 exit (max_models) Mon Mar 25 23:17:31 2013
The process finished Mon Mar 25 23:17:31 2013