============================== Mace4 =================================
Mace4 (32) version Dec-2007, Dec 2007.
Process 3796 was started by Alexei on Alexei-PC,
Sat Mar 16 02:28:16 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 * a6.
a4 = a3 * a8.
a5 = a4 * a7.
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 * a6.
a4 = a3 * a8.
a5 = a4 * a7.
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 | a7 != a6 | a7 != a8 | 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=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.01 seconds).
Ground clauses: seen=49, kept=43.
Selections=4, assignments=8, propagations=36, current_models=0.
Rewrite_terms=353, rewrite_bools=82, indexes=31.
Rules_from_neg_clauses=9, cross_offs=24.

============================== 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=8, assignments=23, propagations=67, current_models=0.
Rewrite_terms=963, rewrite_bools=210, indexes=105.
Rules_from_neg_clauses=11, cross_offs=55.

============================== 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=9, assignments=28, propagations=87, current_models=0.
Rewrite_terms=1369, rewrite_bools=249, indexes=169.
Rules_from_neg_clauses=12, cross_offs=116.

============================== 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=10, assignments=34, propagations=139, current_models=0.
Rewrite_terms=2901, rewrite_bools=547, indexes=305.
Rules_from_neg_clauses=22, cross_offs=216.

============================== 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=13, assignments=54, propagations=226, current_models=0.
Rewrite_terms=4095, rewrite_bools=683, indexes=561.
Rules_from_neg_clauses=25, cross_offs=381.

============================== 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=13, assignments=55, propagations=264, current_models=0.
Rewrite_terms=5584, rewrite_bools=871, indexes=735.
Rules_from_neg_clauses=32, cross_offs=573.

============================== 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=829, kept=811.
Selections=15, assignments=73, propagations=395, current_models=0.
Rewrite_terms=9592, rewrite_bools=1550, indexes=1048.
Rules_from_neg_clauses=31, cross_offs=895.

============================== 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=1120, kept=1100.
Selections=15, assignments=74, propagations=402, current_models=0.
Rewrite_terms=10239, rewrite_bools=1547, indexes=1359.
Rules_from_neg_clauses=27, cross_offs=1178.

============================== 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=16, assignments=85, propagations=535, current_models=0.
Rewrite_terms=13398, rewrite_bools=1853, indexes=1770.
Rules_from_neg_clauses=43, cross_offs=1595.

============================== 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=1894, kept=1870.
Selections=17, assignments=97, propagations=670, current_models=0.
Rewrite_terms=20267, rewrite_bools=3147, indexes=2352.
Rules_from_neg_clauses=47, cross_offs=2124.

============================== 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=2389, kept=2363.
Selections=19, assignments=123, propagations=964, current_models=0.
Rewrite_terms=24912, rewrite_bools=3408, indexes=3157.
Rules_from_neg_clauses=73, cross_offs=2865.

============================== 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=2964, kept=2936.
Selections=19, assignments=124, propagations=1097, current_models=0.
Rewrite_terms=36452, rewrite_bools=5384, indexes=4083.
Rules_from_neg_clauses=67, cross_offs=3856.

============================== 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=3625, kept=3595.
Selections=21, assignments=154, propagations=1412, current_models=0.
Rewrite_terms=44930, rewrite_bools=6575, indexes=5090.
Rules_from_neg_clauses=74, cross_offs=4938.

============================== 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=4378, kept=4346.
Selections=21, assignments=155, propagations=1595, current_models=0.
Rewrite_terms=58169, rewrite_bools=8318, indexes=6421.
Rules_from_neg_clauses=93, cross_offs=6286.

============================== 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=5229, kept=5195.
Selections=23, assignments=189, propagations=1994, current_models=0.
Rewrite_terms=72497, rewrite_bools=11043, indexes=7757.
Rules_from_neg_clauses=109, cross_offs=7902.

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

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

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

For domain size 18.

Current CPU time: 0.00 seconds (total CPU time: 0.19 seconds).
Ground clauses: seen=6184, kept=6148.
Selections=23, assignments=190, propagations=2090, current_models=0.
Rewrite_terms=81115, rewrite_bools=12030, indexes=9281.
Rules_from_neg_clauses=85, cross_offs=9543.

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

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

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

For domain size 19.

Current CPU time: 0.00 seconds (total CPU time: 0.25 seconds).
Ground clauses: seen=7249, kept=7211.
Selections=25, assignments=228, propagations=2771, current_models=0.
Rewrite_terms=105700, rewrite_bools=14933, indexes=11581.
Rules_from_neg_clauses=141, cross_offs=12261.

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

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

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

For domain size 20.

Current CPU time: 0.00 seconds (total CPU time: 0.34 seconds).
Ground clauses: seen=8430, kept=8390.
Selections=25, assignments=229, propagations=2986, current_models=0.
Rewrite_terms=131776, rewrite_bools=18917, indexes=13507.
Rules_from_neg_clauses=144, cross_offs=15107.

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

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

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

For domain size 21.

Current CPU time: 0.00 seconds (total CPU time: 0.42 seconds).
Ground clauses: seen=9733, kept=9691.
Selections=27, assignments=271, propagations=3614, current_models=0.
Rewrite_terms=132025, rewrite_bools=16842, indexes=16118.
Rules_from_neg_clauses=226, cross_offs=18243.

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

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

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

For domain size 22.

Current CPU time: 0.00 seconds (total CPU time: 0.53 seconds).
Ground clauses: seen=11164, kept=11120.
Selections=27, assignments=272, propagations=3722, current_models=0.
Rewrite_terms=152134, rewrite_bools=19309, indexes=18193.
Rules_from_neg_clauses=219, cross_offs=21686.

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

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

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

For domain size 23.

Current CPU time: 0.00 seconds (total CPU time: 0.66 seconds).
Ground clauses: seen=12729, kept=12683.
Selections=27, assignments=272, propagations=3717, current_models=0.
Rewrite_terms=162853, rewrite_bools=21181, indexes=20021.
Rules_from_neg_clauses=115, cross_offs=24339.

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

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

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

For domain size 24.

Current CPU time: 0.00 seconds (total CPU time: 0.78 seconds).
Ground clauses: seen=14434, kept=14386.
Selections=28, assignments=295, propagations=3842, current_models=0.
Rewrite_terms=170095, rewrite_bools=21438, indexes=22113.
Rules_from_neg_clauses=140, cross_offs=26460.

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

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

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

For domain size 25.

Current CPU time: 0.00 seconds (total CPU time: 0.94 seconds).
Ground clauses: seen=16285, kept=16235.
Selections=29, assignments=319, propagations=4302, current_models=0.
Rewrite_terms=183607, rewrite_bools=22085, indexes=25048.
Rules_from_neg_clauses=174, cross_offs=30030.

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

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

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

For domain size 26.

Current CPU time: 0.00 seconds (total CPU time: 1.11 seconds).
Ground clauses: seen=18288, kept=18236.
Selections=30, assignments=344, propagations=4627, current_models=0.
Rewrite_terms=194645, rewrite_bools=22722, indexes=27525.
Rules_from_neg_clauses=170, cross_offs=32417.

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

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

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

For domain size 27.

Current CPU time: 0.00 seconds (total CPU time: 1.28 seconds).
Ground clauses: seen=20449, kept=20395.
Selections=31, assignments=370, propagations=5061, current_models=0.
Rewrite_terms=206692, rewrite_bools=23517, indexes=30063.
Rules_from_neg_clauses=227, cross_offs=34938.

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

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

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

For domain size 28.

Current CPU time: 0.00 seconds (total CPU time: 1.50 seconds).
Ground clauses: seen=22774, kept=22718.
Selections=32, assignments=397, propagations=5524, current_models=0.
Rewrite_terms=219796, rewrite_bools=24410, indexes=32750.
Rules_from_neg_clauses=240, cross_offs=37508.

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

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

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

For domain size 29.

Current CPU time: 0.00 seconds (total CPU time: 1.72 seconds).
Ground clauses: seen=25269, kept=25211.
Selections=33, assignments=425, propagations=6008, current_models=0.
Rewrite_terms=235055, rewrite_bools=25631, indexes=35626.
Rules_from_neg_clauses=253, cross_offs=40128.

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

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

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

For domain size 30.

Current CPU time: 0.00 seconds (total CPU time: 1.98 seconds).
Ground clauses: seen=27940, kept=27880.
Selections=34, assignments=454, propagations=6552, current_models=0.
Rewrite_terms=250877, rewrite_bools=27042, indexes=38564.
Rules_from_neg_clauses=263, cross_offs=42908.

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

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

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

For domain size 31.

Current CPU time: 0.00 seconds (total CPU time: 2.25 seconds).
Ground clauses: seen=30793, kept=30731.
Selections=35, assignments=484, propagations=7190, current_models=0.
Rewrite_terms=268658, rewrite_bools=28862, indexes=41623.
Rules_from_neg_clauses=263, cross_offs=45666.

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

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

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

For domain size 32.

Current CPU time: 0.00 seconds (total CPU time: 2.58 seconds).
Ground clauses: seen=33834, kept=33770.
Selections=36, assignments=515, propagations=7880, current_models=0.
Rewrite_terms=288956, rewrite_bools=31448, indexes=44718.
Rules_from_neg_clauses=263, cross_offs=48329.

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

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

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

For domain size 33.

Current CPU time: 0.00 seconds (total CPU time: 2.94 seconds).
Ground clauses: seen=37069, kept=37003.
Selections=37, assignments=547, propagations=8764, current_models=0.
Rewrite_terms=310342, rewrite_bools=34328, indexes=47853.
Rules_from_neg_clauses=252, cross_offs=51023.

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

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

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

For domain size 34.

Current CPU time: 0.00 seconds (total CPU time: 3.34 seconds).
Ground clauses: seen=40504, kept=40436.
Selections=38, assignments=580, propagations=9646, current_models=0.
Rewrite_terms=335133, rewrite_bools=38333, indexes=50994.
Rules_from_neg_clauses=238, cross_offs=53737.

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

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

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

For domain size 35.

Current CPU time: 0.00 seconds (total CPU time: 3.78 seconds).
Ground clauses: seen=44145, kept=44075.
Selections=39, assignments=614, propagations=10665, current_models=0.
Rewrite_terms=362347, rewrite_bools=43308, indexes=54087.
Rules_from_neg_clauses=225, cross_offs=56493.

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

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

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

For domain size 36.

Current CPU time: 0.00 seconds (total CPU time: 4.28 seconds).
Ground clauses: seen=47998, kept=47926.
Selections=40, assignments=649, propagations=11766, current_models=0.
Rewrite_terms=391202, rewrite_bools=48601, indexes=57238.
Rules_from_neg_clauses=201, cross_offs=59325.

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

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

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

interpretation( 37, [number=1, seconds=4], [

        function(a1, [ 0 ]),

        function(a2, [ 1 ]),

        function(a3, [ 7 ]),

        function(a4, [22 ]),

        function(a5, [ 2 ]),

        function(a6, [ 6 ]),

        function(a7, [18 ]),

        function(a8, [21 ]),

        function(a9, [ 3 ]),

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

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

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

For domain size 37.

Current CPU time: 0.00 seconds (total CPU time: 4.91 seconds).
Ground clauses: seen=52069, kept=51995.
Selections=41, assignments=685, propagations=13013, current_models=1.
Rewrite_terms=472669, rewrite_bools=71759, indexes=60304.
Rules_from_neg_clauses=179, cross_offs=62228.

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

User_CPU=4.91, System_CPU=0.00, Wall_clock=4.

Exiting with 1 model.

Process 3796 exit (max_models) Sat Mar 16 02:28:20 2013
The process finished Sat Mar 16 02:28:20 2013