============================== Mace4 =================================
Mace4 (32) version Dec-2007, Dec 2007.
Process 2604 was started by Alexei on Alexei-PC,
Sat Mar 16 11:30:36 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).
end_if.

formulas(assumptions).
x * x = x.
(x * y) * y = x.
(x * y) * z = (x * z) * (y * z).
a2 = a1 * a9.
a3 = a2 * a8.
a4 = a3 * a1.
a5 = a4 * a7.
a6 = a5 * a3.
a7 = a6 * a2.
a8 = a7 * a5.
a9 = a8 * a6.
a1 = a9 * a4.
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 * a9.
a3 = a2 * a8.
a4 = a3 * a1.
a5 = a4 * a7.
a6 = a5 * a3.
a7 = a6 * a2.
a8 = a7 * a5.
a9 = a8 * a6.
a1 = a9 * a4.
a1 != a2 | a3 != a2 | a4 != a3 | a5 != a4 | a6 != a5 | a6 != a7 | a7 != a8 | a8 != 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=24, kept=14.
Selections=4, assignments=7, propagations=14, current_models=0.
Rewrite_terms=69, rewrite_bools=20, indexes=0.
Rules_from_neg_clauses=6, cross_offs=6.

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

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

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

For domain size 3.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=49, kept=43.
Selections=6, assignments=13, propagations=43, current_models=0.
Rewrite_terms=402, rewrite_bools=85, indexes=46.
Rules_from_neg_clauses=15, cross_offs=38.

============================== 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=94, kept=86.
Selections=13, assignments=40, propagations=75, current_models=0.
Rewrite_terms=927, rewrite_bools=173, indexes=143.
Rules_from_neg_clauses=16, cross_offs=88.

============================== 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=165, kept=155.
Selections=16, assignments=55, propagations=155, current_models=0.
Rewrite_terms=2276, rewrite_bools=368, indexes=320.
Rules_from_neg_clauses=36, cross_offs=236.

============================== 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=268, kept=256.
Selections=22, assignments=89, propagations=251, current_models=0.
Rewrite_terms=5063, rewrite_bools=898, indexes=623.
Rules_from_neg_clauses=46, cross_offs=452.

============================== 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=409, kept=395.
Selections=28, assignments=128, propagations=380, current_models=0.
Rewrite_terms=7290, rewrite_bools=1144, indexes=1084.
Rules_from_neg_clauses=61, cross_offs=836.

============================== 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=594, kept=578.
Selections=36, assignments=188, propagations=527, current_models=0.
Rewrite_terms=11925, rewrite_bools=1810, indexes=1842.
Rules_from_neg_clauses=61, cross_offs=1382.

============================== 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=829, kept=811.
Selections=46, assignments=274, propagations=813, current_models=0.
Rewrite_terms=19564, rewrite_bools=2637, indexes=3359.
Rules_from_neg_clauses=89, cross_offs=2494.

============================== 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=52, assignments=331, propagations=994, current_models=0.
Rewrite_terms=26448, rewrite_bools=3515, indexes=4532.
Rules_from_neg_clauses=99, cross_offs=3567.

============================== 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=1473, kept=1451.
Selections=65, assignments=467, propagations=1863, current_models=0.
Rewrite_terms=41642, rewrite_bools=4644, indexes=7721.
Rules_from_neg_clauses=157, cross_offs=6226.

============================== 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=69, assignments=514, propagations=2103, current_models=0.
Rewrite_terms=53326, rewrite_bools=5915, indexes=9764.
Rules_from_neg_clauses=175, cross_offs=8670.

============================== 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=82, assignments=674, propagations=3042, current_models=0.
Rewrite_terms=81393, rewrite_bools=9464, indexes=13861.
Rules_from_neg_clauses=234, cross_offs=12672.

============================== 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=92, assignments=808, propagations=3796, current_models=0.
Rewrite_terms=107460, rewrite_bools=12787, indexes=18361.
Rules_from_neg_clauses=243, cross_offs=16590.

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

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

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

For domain size 15.

Current CPU time: 0.00 seconds (total CPU time: 0.12 seconds).
Ground clauses: seen=3625, kept=3595.
Selections=105, assignments=996, propagations=4942, current_models=0.
Rewrite_terms=139841, rewrite_bools=16085, indexes=24542.
Rules_from_neg_clauses=250, cross_offs=22476.

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

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

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

For domain size 16.

Current CPU time: 0.00 seconds (total CPU time: 0.19 seconds).
Ground clauses: seen=4378, kept=4346.
Selections=121, assignments=1245, propagations=6334, current_models=0.
Rewrite_terms=185229, rewrite_bools=21007, indexes=32489.
Rules_from_neg_clauses=331, cross_offs=30771.

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

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

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

For domain size 17.

Current CPU time: 0.00 seconds (total CPU time: 0.27 seconds).
Ground clauses: seen=5229, kept=5195.
Selections=133, assignments=1445, propagations=7487, current_models=0.
Rewrite_terms=227588, rewrite_bools=25554, indexes=40505.
Rules_from_neg_clauses=399, cross_offs=40107.

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

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

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

For domain size 18.

Current CPU time: 0.00 seconds (total CPU time: 0.39 seconds).
Ground clauses: seen=6184, kept=6148.
Selections=149, assignments=1727, propagations=9359, current_models=0.
Rewrite_terms=279911, rewrite_bools=29649, indexes=51760.
Rules_from_neg_clauses=458, cross_offs=52936.

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

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

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

For domain size 19.

Current CPU time: 0.00 seconds (total CPU time: 0.55 seconds).
Ground clauses: seen=7249, kept=7211.
Selections=163, assignments=1988, propagations=11825, current_models=0.
Rewrite_terms=353242, rewrite_bools=34876, indexes=67102.
Rules_from_neg_clauses=563, cross_offs=73347.

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

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

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

For domain size 20.

Current CPU time: 0.00 seconds (total CPU time: 0.73 seconds).
Ground clauses: seen=8430, kept=8390.
Selections=180, assignments=2320, propagations=14160, current_models=0.
Rewrite_terms=437796, rewrite_bools=42823, indexes=84722.
Rules_from_neg_clauses=608, cross_offs=94022.

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

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

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

For domain size 21.

Current CPU time: 0.00 seconds (total CPU time: 1.03 seconds).
Ground clauses: seen=9733, kept=9691.
Selections=206, assignments=2850, propagations=17831, current_models=0.
Rewrite_terms=573572, rewrite_bools=56835, indexes=108283.
Rules_from_neg_clauses=739, cross_offs=124771.

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

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

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

For domain size 22.

Current CPU time: 0.00 seconds (total CPU time: 1.39 seconds).
Ground clauses: seen=11164, kept=11120.
Selections=227, assignments=3301, propagations=21439, current_models=0.
Rewrite_terms=682266, rewrite_bools=64905, indexes=132107.
Rules_from_neg_clauses=886, cross_offs=154926.

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

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

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

For domain size 23.

Current CPU time: 0.00 seconds (total CPU time: 1.88 seconds).
Ground clauses: seen=12729, kept=12683.
Selections=249, assignments=3795, propagations=26610, current_models=0.
Rewrite_terms=860197, rewrite_bools=80004, indexes=166163.
Rules_from_neg_clauses=962, cross_offs=200347.

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

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

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

For domain size 24.

Current CPU time: 0.00 seconds (total CPU time: 2.50 seconds).
Ground clauses: seen=14434, kept=14386.
Selections=275, assignments=4405, propagations=31762, current_models=0.
Rewrite_terms=1042443, rewrite_bools=100094, indexes=200111.
Rules_from_neg_clauses=1094, cross_offs=242160.

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

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

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

For domain size 25.

Current CPU time: 0.00 seconds (total CPU time: 3.33 seconds).
Ground clauses: seen=16285, kept=16235.
Selections=299, assignments=4994, propagations=38750, current_models=0.
Rewrite_terms=1289114, rewrite_bools=126676, indexes=242423.
Rules_from_neg_clauses=1977, cross_offs=304990.

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

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

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

For domain size 26.

Current CPU time: 0.00 seconds (total CPU time: 4.28 seconds).
Ground clauses: seen=18288, kept=18236.
Selections=321, assignments=5558, propagations=43285, current_models=0.
Rewrite_terms=1452413, rewrite_bools=139775, indexes=278178.
Rules_from_neg_clauses=1320, cross_offs=350795.

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

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

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

For domain size 27.

Current CPU time: 0.00 seconds (total CPU time: 5.48 seconds).
Ground clauses: seen=20449, kept=20395.
Selections=346, assignments=6222, propagations=50551, current_models=0.
Rewrite_terms=1709686, rewrite_bools=162234, indexes=329458.
Rules_from_neg_clauses=1519, cross_offs=420536.

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

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

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

For domain size 28.

Current CPU time: 0.00 seconds (total CPU time: 6.89 seconds).
Ground clauses: seen=22774, kept=22718.
Selections=370, assignments=6881, propagations=57515, current_models=0.
Rewrite_terms=1940469, rewrite_bools=179246, indexes=379928.
Rules_from_neg_clauses=1669, cross_offs=496994.

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

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

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

For domain size 29.

Current CPU time: 0.00 seconds (total CPU time: 8.59 seconds).
Ground clauses: seen=25269, kept=25211.
Selections=401, assignments=7762, propagations=65289, current_models=0.
Rewrite_terms=2240227, rewrite_bools=203331, indexes=441527.
Rules_from_neg_clauses=1693, cross_offs=585582.

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

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

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

For domain size 30.

Current CPU time: 0.00 seconds (total CPU time: 10.58 seconds).
Ground clauses: seen=27940, kept=27880.
Selections=431, assignments=8650, propagations=74877, current_models=0.
Rewrite_terms=2565981, rewrite_bools=233641, indexes=514380.
Rules_from_neg_clauses=2031, cross_offs=675748.

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

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

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

For domain size 31.

Current CPU time: 0.00 seconds (total CPU time: 13.00 seconds).
Ground clauses: seen=30793, kept=30731.
Selections=461, assignments=9566, propagations=83931, current_models=0.
Rewrite_terms=2941960, rewrite_bools=266737, indexes=586081.
Rules_from_neg_clauses=2129, cross_offs=784487.

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

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

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

For domain size 32.

Current CPU time: 0.00 seconds (total CPU time: 15.72 seconds).
Ground clauses: seen=33834, kept=33770.
Selections=489, assignments=10447, propagations=93575, current_models=0.
Rewrite_terms=3261811, rewrite_bools=291666, indexes=654086.
Rules_from_neg_clauses=2465, cross_offs=897736.

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

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

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

For domain size 33.

Current CPU time: 0.00 seconds (total CPU time: 19.02 seconds).
Ground clauses: seen=37069, kept=37003.
Selections=532, assignments=11843, propagations=108251, current_models=0.
Rewrite_terms=3773455, rewrite_bools=339265, indexes=757580.
Rules_from_neg_clauses=2687, cross_offs=1047129.

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

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

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

For domain size 34.

Current CPU time: 0.00 seconds (total CPU time: 22.77 seconds).
Ground clauses: seen=40504, kept=40436.
Selections=563, assignments=12884, propagations=119212, current_models=0.
Rewrite_terms=4163383, rewrite_bools=364794, indexes=847376.
Rules_from_neg_clauses=2780, cross_offs=1178283.

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

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

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

For domain size 35.

Current CPU time: 0.00 seconds (total CPU time: 27.70 seconds).
Ground clauses: seen=44145, kept=44075.
Selections=598, assignments=14094, propagations=135653, current_models=0.
Rewrite_terms=5015792, rewrite_bools=463099, indexes=980719.
Rules_from_neg_clauses=3421, cross_offs=1385498.

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

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

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

For domain size 36.

Current CPU time: 0.00 seconds (total CPU time: 33.41 seconds).
Ground clauses: seen=47998, kept=47926.
Selections=628, assignments=15160, propagations=148939, current_models=0.
Rewrite_terms=5568624, rewrite_bools=506576, indexes=1093356.
Rules_from_neg_clauses=3705, cross_offs=1567910.

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

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

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

For domain size 37.

Current CPU time: 0.00 seconds (total CPU time: 40.03 seconds).
Ground clauses: seen=52069, kept=51995.
Selections=675, assignments=16873, propagations=167182, current_models=0.
Rewrite_terms=6289720, rewrite_bools=573702, indexes=1252821.
Rules_from_neg_clauses=3853, cross_offs=1797612.

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

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

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

For domain size 38.

Current CPU time: 0.00 seconds (total CPU time: 47.50 seconds).
Ground clauses: seen=56364, kept=56288.
Selections=715, assignments=18373, propagations=185992, current_models=0.
Rewrite_terms=6945246, rewrite_bools=618978, indexes=1410856.
Rules_from_neg_clauses=3985, cross_offs=2063061.

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

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

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

For domain size 39.

Current CPU time: 0.00 seconds (total CPU time: 56.33 seconds).
Ground clauses: seen=60889, kept=60811.
Selections=755, assignments=19911, propagations=205992, current_models=0.
Rewrite_terms=7913750, rewrite_bools=700787, indexes=1615487.
Rules_from_neg_clauses=4444, cross_offs=2370426.

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

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

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

For domain size 40.

Current CPU time: 0.00 seconds (total CPU time: 66.19 seconds).
Ground clauses: seen=65650, kept=65570.
Selections=795, assignments=21489, propagations=226579, current_models=0.
Rewrite_terms=8693187, rewrite_bools=738985, indexes=1827908.
Rules_from_neg_clauses=5003, cross_offs=2706138.

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

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

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

For domain size 41.

Current CPU time: 0.00 seconds (total CPU time: 77.52 seconds).
Ground clauses: seen=70653, kept=70571.
Selections=844, assignments=23471, propagations=250837, current_models=0.
Rewrite_terms=9667164, rewrite_bools=789750, indexes=2047569.
Rules_from_neg_clauses=5474, cross_offs=3055131.

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

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

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

For domain size 42.

Current CPU time: 0.00 seconds (total CPU time: 90.11 seconds).
Ground clauses: seen=75904, kept=75820.
Selections=883, assignments=25089, propagations=272375, current_models=0.
Rewrite_terms=10486934, rewrite_bools=826469, indexes=2247162.
Rules_from_neg_clauses=6047, cross_offs=3417786.

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

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

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

For domain size 43.

Current CPU time: 0.00 seconds (total CPU time: 103.83 seconds).
Ground clauses: seen=81409, kept=81323.
Selections=924, assignments=26829, propagations=294961, current_models=0.
Rewrite_terms=11312923, rewrite_bools=859302, indexes=2464304.
Rules_from_neg_clauses=5571, cross_offs=3818332.

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

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

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

For domain size 44.

Current CPU time: 0.00 seconds (total CPU time: 118.58 seconds).
Ground clauses: seen=87174, kept=87086.
Selections=961, assignments=28435, propagations=314169, current_models=0.
Rewrite_terms=11981869, rewrite_bools=882679, indexes=2657468.
Rules_from_neg_clauses=5456, cross_offs=4136845.

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

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

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

For domain size 45.

Current CPU time: 0.00 seconds (total CPU time: 134.88 seconds).
Ground clauses: seen=93205, kept=93115.
Selections=1001, assignments=30209, propagations=337750, current_models=0.
Rewrite_terms=12943610, rewrite_bools=926281, indexes=2890359.
Rules_from_neg_clauses=6150, cross_offs=4532783.

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

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

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

For domain size 46.

Current CPU time: 0.00 seconds (total CPU time: 152.48 seconds).
Ground clauses: seen=99508, kept=99416.
Selections=1039, assignments=31932, propagations=362926, current_models=0.
Rewrite_terms=13795311, rewrite_bools=971554, indexes=3092250.
Rules_from_neg_clauses=6698, cross_offs=4894170.

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

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

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

For domain size 47.

Current CPU time: 0.00 seconds (total CPU time: 171.76 seconds).
Ground clauses: seen=106089, kept=105995.
Selections=1076, assignments=33646, propagations=385013, current_models=0.
Rewrite_terms=14815646, rewrite_bools=1059122, indexes=3317001.
Rules_from_neg_clauses=6572, cross_offs=5274914.

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

============================== DOMAIN SIZE 48 ========================

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

For domain size 48.

Current CPU time: 0.00 seconds (total CPU time: 192.59 seconds).
Ground clauses: seen=112954, kept=112858.
Selections=1110, assignments=35253, propagations=405902, current_models=0.
Rewrite_terms=15664309, rewrite_bools=1113083, indexes=3531460.
Rules_from_neg_clauses=6799, cross_offs=5631953.

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

============================== DOMAIN SIZE 49 ========================

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

For domain size 49.

Current CPU time: 0.00 seconds (total CPU time: 215.25 seconds).
Ground clauses: seen=120109, kept=120011.
Selections=1151, assignments=37234, propagations=436395, current_models=0.
Rewrite_terms=16816630, rewrite_bools=1157315, indexes=3810885.
Rules_from_neg_clauses=7382, cross_offs=6110029.

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

============================== DOMAIN SIZE 50 ========================

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

For domain size 50.

Current CPU time: 0.00 seconds (total CPU time: 239.62 seconds).
Ground clauses: seen=127560, kept=127460.
Selections=1185, assignments=38912, propagations=462825, current_models=0.
Rewrite_terms=17802078, rewrite_bools=1191941, indexes=4060316.
Rules_from_neg_clauses=7606, cross_offs=6528405.

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

============================== DOMAIN SIZE 51 ========================

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

For domain size 51.

Current CPU time: 0.00 seconds (total CPU time: 267.33 seconds).
Ground clauses: seen=135313, kept=135211.
Selections=1221, assignments=40725, propagations=489633, current_models=0.
Rewrite_terms=19320845, rewrite_bools=1353072, indexes=4350470.
Rules_from_neg_clauses=7687, cross_offs=7026699.

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

============================== DOMAIN SIZE 52 ========================

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

For domain size 52.

Current CPU time: 0.00 seconds (total CPU time: 296.69 seconds).
Ground clauses: seen=143374, kept=143270.
Selections=1252, assignments=42313, propagations=512019, current_models=0.
Rewrite_terms=20209143, rewrite_bools=1394471, indexes=4569018.
Rules_from_neg_clauses=7576, cross_offs=7436634.

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

============================== DOMAIN SIZE 53 ========================

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

For domain size 53.

Current CPU time: 0.00 seconds (total CPU time: 328.12 seconds).
Ground clauses: seen=151749, kept=151643.
Selections=1298, assignments=44718, propagations=548938, current_models=0.
Rewrite_terms=21388573, rewrite_bools=1444042, indexes=4888033.
Rules_from_neg_clauses=8174, cross_offs=7982822.

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

============================== DOMAIN SIZE 54 ========================

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

For domain size 54.

Current CPU time: 0.00 seconds (total CPU time: 361.92 seconds).
Ground clauses: seen=160444, kept=160336.
Selections=1338, assignments=46853, propagations=584521, current_models=0.
Rewrite_terms=22625654, rewrite_bools=1511869, indexes=5200956.
Rules_from_neg_clauses=8703, cross_offs=8508310.

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

============================== DOMAIN SIZE 55 ========================

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

For domain size 55.

Current CPU time: 0.00 seconds (total CPU time: 397.94 seconds).
Ground clauses: seen=169465, kept=169355.
Selections=1374, assignments=48813, propagations=619230, current_models=0.
Rewrite_terms=23738213, rewrite_bools=1555535, indexes=5493293.
Rules_from_neg_clauses=9079, cross_offs=9038428.

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

============================== DOMAIN SIZE 56 ========================

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

For domain size 56.

Current CPU time: 0.00 seconds (total CPU time: 436.05 seconds).
Ground clauses: seen=178818, kept=178706.
Selections=1403, assignments=50418, propagations=648550, current_models=0.
Rewrite_terms=24714094, rewrite_bools=1595001, indexes=5728039.
Rules_from_neg_clauses=9385, cross_offs=9419330.

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

============================== DOMAIN SIZE 57 ========================

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

For domain size 57.

Current CPU time: 0.00 seconds (total CPU time: 476.42 seconds).
Ground clauses: seen=188509, kept=188395.
Selections=1442, assignments=52614, propagations=680097, current_models=0.
Rewrite_terms=25902922, rewrite_bools=1645173, indexes=6038848.
Rules_from_neg_clauses=8950, cross_offs=9955202.

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

============================== DOMAIN SIZE 58 ========================

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

For domain size 58.

Current CPU time: 0.00 seconds (total CPU time: 519.06 seconds).
Ground clauses: seen=198544, kept=198428.
Selections=1474, assignments=54447, propagations=714774, current_models=0.
Rewrite_terms=27041306, rewrite_bools=1689386, indexes=6337193.
Rules_from_neg_clauses=10277, cross_offs=10493918.

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

============================== DOMAIN SIZE 59 ========================

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

For domain size 59.

Current CPU time: 0.00 seconds (total CPU time: 565.72 seconds).
Ground clauses: seen=208929, kept=208811.
Selections=1520, assignments=57130, propagations=763125, current_models=0.
Rewrite_terms=28889252, rewrite_bools=1795037, indexes=6786968.
Rules_from_neg_clauses=10740, cross_offs=11308914.

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

============================== DOMAIN SIZE 60 ========================

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

For domain size 60.

Current CPU time: 0.00 seconds (total CPU time: 616.94 seconds).
Ground clauses: seen=219670, kept=219550.
Selections=1553, assignments=59089, propagations=797825, current_models=0.
Rewrite_terms=30627402, rewrite_bools=2022139, indexes=7088465.
Rules_from_neg_clauses=10150, cross_offs=11827297.

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

============================== DOMAIN SIZE 61 ========================

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

interpretation( 61, [number=1, seconds=669], [

        function(a1, [ 0 ]),

        function(a2, [ 1 ]),

        function(a3, [ 5 ]),

        function(a4, [ 3 ]),

        function(a5, [39 ]),

        function(a6, [ 9 ]),

        function(a7, [43 ]),

        function(a8, [ 6 ]),

        function(a9, [ 2 ]),

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

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

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

For domain size 61.

Current CPU time: 0.00 seconds (total CPU time: 670.03 seconds).
Ground clauses: seen=230773, kept=230651.
Selections=1553, assignments=59193, propagations=793921, current_models=1.
Rewrite_terms=31101265, rewrite_bools=2085739, indexes=7132720.
Rules_from_neg_clauses=8899, cross_offs=12036242.

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

User_CPU=670.03, System_CPU=0.25, Wall_clock=673.

Exiting with 1 model.

Process 2604 exit (max_models) Sat Mar 16 11:41:49 2013
The process finished Sat Mar 16 11:41:49 2013