============================== Mace4 ================================= Mace4 (32) version 2009-11A, November 2009. Process 4320 was started by mccune on cleo, Tue Nov 3 09:38:38 2009 The command was "/home/mccune/LADR/bin/mace4 -f ncg-48.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file ncg-48.in assign(domain_size,48). % assign(domain_size, 48) -> assign(start_size, 48). % assign(domain_size, 48) -> assign(end_size, 48). clear(negprop). formulas(assumptions). e * x = x. x' * x = e. (x * y) * z = x * (y * z). A * B != B * A. end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: ============================== end of process non-clausal formulas === ============================== CLAUSES FOR SEARCH ==================== formulas(mace4_clauses). e * x = x. x' * x = e. (x * y) * z = x * (y * z). A * B != B * A. end_of_list. ============================== end of clauses for search ============= % There are no natural numbers in the input. ============================== DOMAIN SIZE 48 ======================== ============================== MODEL ================================= interpretation( 48, [number=1, seconds=0], [ function(A, [ 0 ]), function(B, [ 1 ]), function(e, [ 2 ]), function('(_), [ 0, 1, 2, 4, 3, 5, 6, 7, 8,10, 9,11,12,13,14,16,15,17,18,19,20,22,21,23,24,25,26,28,27,29,30,31,32,34,33,35,36,37,38,40,39,41,42,43,44,46,45,47 ]), function(*(_,_), [ 2, 3, 0, 1, 5, 4, 7, 6, 9, 8,11,10,13,12,15,14,17,16,19,18,21,20,23,22,25,24,27,26,29,28,31,30,33,32,35,34,37,36,39,38,41,40,43,42,45,44,47,46, 4, 2, 1, 5, 0, 3, 8,10, 6,11, 7, 9,14,16,12,17,13,15,20,22,18,23,19,21,26,28,24,29,25,27,32,34,30,35,31,33,38,40,36,41,37,39,44,46,42,47,43,45, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47, 5, 0, 3, 4, 2, 1, 9,11, 7,10, 6, 8,15,17,13,16,12,14,21,23,19,22,18,20,27,29,25,28,24,26,33,35,31,34,30,32,39,41,37,40,36,38,45,47,43,46,42,44, 1, 5, 4, 2, 3, 0,10, 8,11, 6, 9, 7,16,14,17,12,15,13,22,20,23,18,21,19,28,26,29,24,27,25,34,32,35,30,33,31,40,38,41,36,39,37,46,44,47,42,45,43, 3, 4, 5, 0, 1, 2,11, 9,10, 7, 8, 6,17,15,16,13,14,12,23,21,22,19,20,18,29,27,28,25,26,24,35,33,34,31,32,30,41,39,40,37,38,36,47,45,46,43,44,42, 7, 8, 6, 9,10,11, 2, 0, 1, 3, 4, 5,18,19,20,21,22,23,12,13,14,15,16,17,30,31,32,33,34,35,24,25,26,27,28,29,42,43,44,45,46,47,36,37,38,39,40,41, 6, 9, 7, 8,11,10, 0, 2, 3, 1, 5, 4,19,18,21,20,23,22,13,12,15,14,17,16,31,30,33,32,35,34,25,24,27,26,29,28,43,42,45,44,47,46,37,36,39,38,41,40, 10, 6, 8,11, 7, 9, 1, 4, 2, 5, 0, 3,20,22,18,23,19,21,14,16,12,17,13,15,32,34,30,35,31,33,26,28,24,29,25,27,44,46,42,47,43,45,38,40,36,41,37,39, 11, 7, 9,10, 6, 8, 3, 5, 0, 4, 2, 1,21,23,19,22,18,20,15,17,13,16,12,14,33,35,31,34,30,32,27,29,25,28,24,26,45,47,43,46,42,44,39,41,37,40,36,38, 8,11,10, 6, 9, 7, 4, 1, 5, 2, 3, 0,22,20,23,18,21,19,16,14,17,12,15,13,34,32,35,30,33,31,28,26,29,24,27,25,46,44,47,42,45,43,40,38,41,36,39,37, 9,10,11, 7, 8, 6, 5, 3, 4, 0, 1, 2,23,21,22,19,20,18,17,15,16,13,14,12,35,33,34,31,32,30,29,27,28,25,26,24,47,45,46,43,44,42,41,39,40,37,38,36, 13,14,12,15,16,17,18,19,20,21,22,23, 2, 0, 1, 3, 4, 5, 6, 7, 8, 9,10,11,36,37,38,39,40,41,42,43,44,45,46,47,24,25,26,27,28,29,30,31,32,33,34,35, 12,15,13,14,17,16,19,18,21,20,23,22, 0, 2, 3, 1, 5, 4, 7, 6, 9, 8,11,10,37,36,39,38,41,40,43,42,45,44,47,46,25,24,27,26,29,28,31,30,33,32,35,34, 16,12,14,17,13,15,20,22,18,23,19,21, 1, 4, 2, 5, 0, 3, 8,10, 6,11, 7, 9,38,40,36,41,37,39,44,46,42,47,43,45,26,28,24,29,25,27,32,34,30,35,31,33, 17,13,15,16,12,14,21,23,19,22,18,20, 3, 5, 0, 4, 2, 1, 9,11, 7,10, 6, 8,39,41,37,40,36,38,45,47,43,46,42,44,27,29,25,28,24,26,33,35,31,34,30,32, 14,17,16,12,15,13,22,20,23,18,21,19, 4, 1, 5, 2, 3, 0,10, 8,11, 6, 9, 7,40,38,41,36,39,37,46,44,47,42,45,43,28,26,29,24,27,25,34,32,35,30,33,31, 15,16,17,13,14,12,23,21,22,19,20,18, 5, 3, 4, 0, 1, 2,11, 9,10, 7, 8, 6,41,39,40,37,38,36,47,45,46,43,44,42,29,27,28,25,26,24,35,33,34,31,32,30, 19,20,18,21,22,23,12,13,14,15,16,17, 6, 7, 8, 9,10,11, 2, 0, 1, 3, 4, 5,42,43,44,45,46,47,36,37,38,39,40,41,30,31,32,33,34,35,24,25,26,27,28,29, 18,21,19,20,23,22,13,12,15,14,17,16, 7, 6, 9, 8,11,10, 0, 2, 3, 1, 5, 4,43,42,45,44,47,46,37,36,39,38,41,40,31,30,33,32,35,34,25,24,27,26,29,28, 22,18,20,23,19,21,14,16,12,17,13,15, 8,10, 6,11, 7, 9, 1, 4, 2, 5, 0, 3,44,46,42,47,43,45,38,40,36,41,37,39,32,34,30,35,31,33,26,28,24,29,25,27, 23,19,21,22,18,20,15,17,13,16,12,14, 9,11, 7,10, 6, 8, 3, 5, 0, 4, 2, 1,45,47,43,46,42,44,39,41,37,40,36,38,33,35,31,34,30,32,27,29,25,28,24,26, 20,23,22,18,21,19,16,14,17,12,15,13,10, 8,11, 6, 9, 7, 4, 1, 5, 2, 3, 0,46,44,47,42,45,43,40,38,41,36,39,37,34,32,35,30,33,31,28,26,29,24,27,25, 21,22,23,19,20,18,17,15,16,13,14,12,11, 9,10, 7, 8, 6, 5, 3, 4, 0, 1, 2,47,45,46,43,44,42,41,39,40,37,38,36,35,33,34,31,32,30,29,27,28,25,26,24, 25,26,24,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47, 2, 0, 1, 3, 4, 5, 6, 7, 8, 9,10,11,12,13,14,15,16,17,18,19,20,21,22,23, 24,27,25,26,29,28,31,30,33,32,35,34,37,36,39,38,41,40,43,42,45,44,47,46, 0, 2, 3, 1, 5, 4, 7, 6, 9, 8,11,10,13,12,15,14,17,16,19,18,21,20,23,22, 28,24,26,29,25,27,32,34,30,35,31,33,38,40,36,41,37,39,44,46,42,47,43,45, 1, 4, 2, 5, 0, 3, 8,10, 6,11, 7, 9,14,16,12,17,13,15,20,22,18,23,19,21, 29,25,27,28,24,26,33,35,31,34,30,32,39,41,37,40,36,38,45,47,43,46,42,44, 3, 5, 0, 4, 2, 1, 9,11, 7,10, 6, 8,15,17,13,16,12,14,21,23,19,22,18,20, 26,29,28,24,27,25,34,32,35,30,33,31,40,38,41,36,39,37,46,44,47,42,45,43, 4, 1, 5, 2, 3, 0,10, 8,11, 6, 9, 7,16,14,17,12,15,13,22,20,23,18,21,19, 27,28,29,25,26,24,35,33,34,31,32,30,41,39,40,37,38,36,47,45,46,43,44,42, 5, 3, 4, 0, 1, 2,11, 9,10, 7, 8, 6,17,15,16,13,14,12,23,21,22,19,20,18, 31,32,30,33,34,35,24,25,26,27,28,29,42,43,44,45,46,47,36,37,38,39,40,41, 6, 7, 8, 9,10,11, 2, 0, 1, 3, 4, 5,18,19,20,21,22,23,12,13,14,15,16,17, 30,33,31,32,35,34,25,24,27,26,29,28,43,42,45,44,47,46,37,36,39,38,41,40, 7, 6, 9, 8,11,10, 0, 2, 3, 1, 5, 4,19,18,21,20,23,22,13,12,15,14,17,16, 34,30,32,35,31,33,26,28,24,29,25,27,44,46,42,47,43,45,38,40,36,41,37,39, 8,10, 6,11, 7, 9, 1, 4, 2, 5, 0, 3,20,22,18,23,19,21,14,16,12,17,13,15, 35,31,33,34,30,32,27,29,25,28,24,26,45,47,43,46,42,44,39,41,37,40,36,38, 9,11, 7,10, 6, 8, 3, 5, 0, 4, 2, 1,21,23,19,22,18,20,15,17,13,16,12,14, 32,35,34,30,33,31,28,26,29,24,27,25,46,44,47,42,45,43,40,38,41,36,39,37,10, 8,11, 6, 9, 7, 4, 1, 5, 2, 3, 0,22,20,23,18,21,19,16,14,17,12,15,13, 33,34,35,31,32,30,29,27,28,25,26,24,47,45,46,43,44,42,41,39,40,37,38,36,11, 9,10, 7, 8, 6, 5, 3, 4, 0, 1, 2,23,21,22,19,20,18,17,15,16,13,14,12, 37,38,36,39,40,41,42,43,44,45,46,47,24,25,26,27,28,29,30,31,32,33,34,35,12,13,14,15,16,17,18,19,20,21,22,23, 2, 0, 1, 3, 4, 5, 6, 7, 8, 9,10,11, 36,39,37,38,41,40,43,42,45,44,47,46,25,24,27,26,29,28,31,30,33,32,35,34,13,12,15,14,17,16,19,18,21,20,23,22, 0, 2, 3, 1, 5, 4, 7, 6, 9, 8,11,10, 40,36,38,41,37,39,44,46,42,47,43,45,26,28,24,29,25,27,32,34,30,35,31,33,14,16,12,17,13,15,20,22,18,23,19,21, 1, 4, 2, 5, 0, 3, 8,10, 6,11, 7, 9, 41,37,39,40,36,38,45,47,43,46,42,44,27,29,25,28,24,26,33,35,31,34,30,32,15,17,13,16,12,14,21,23,19,22,18,20, 3, 5, 0, 4, 2, 1, 9,11, 7,10, 6, 8, 38,41,40,36,39,37,46,44,47,42,45,43,28,26,29,24,27,25,34,32,35,30,33,31,16,14,17,12,15,13,22,20,23,18,21,19, 4, 1, 5, 2, 3, 0,10, 8,11, 6, 9, 7, 39,40,41,37,38,36,47,45,46,43,44,42,29,27,28,25,26,24,35,33,34,31,32,30,17,15,16,13,14,12,23,21,22,19,20,18, 5, 3, 4, 0, 1, 2,11, 9,10, 7, 8, 6, 43,44,42,45,46,47,36,37,38,39,40,41,30,31,32,33,34,35,24,25,26,27,28,29,18,19,20,21,22,23,12,13,14,15,16,17, 6, 7, 8, 9,10,11, 2, 0, 1, 3, 4, 5, 42,45,43,44,47,46,37,36,39,38,41,40,31,30,33,32,35,34,25,24,27,26,29,28,19,18,21,20,23,22,13,12,15,14,17,16, 7, 6, 9, 8,11,10, 0, 2, 3, 1, 5, 4, 46,42,44,47,43,45,38,40,36,41,37,39,32,34,30,35,31,33,26,28,24,29,25,27,20,22,18,23,19,21,14,16,12,17,13,15, 8,10, 6,11, 7, 9, 1, 4, 2, 5, 0, 3, 47,43,45,46,42,44,39,41,37,40,36,38,33,35,31,34,30,32,27,29,25,28,24,26,21,23,19,22,18,20,15,17,13,16,12,14, 9,11, 7,10, 6, 8, 3, 5, 0, 4, 2, 1, 44,47,46,42,45,43,40,38,41,36,39,37,34,32,35,30,33,31,28,26,29,24,27,25,22,20,23,18,21,19,16,14,17,12,15,13,10, 8,11, 6, 9, 7, 4, 1, 5, 2, 3, 0, 45,46,47,43,44,42,41,39,40,37,38,36,35,33,34,31,32,30,29,27,28,25,26,24,23,21,22,19,20,18,17,15,16,13,14,12,11, 9,10, 7, 8, 6, 5, 3, 4, 0, 1, 2 ]) ]). ============================== end of model ========================== ============================== STATISTICS ============================ For domain size 48. Current CPU time: 0.00 seconds (total CPU time: 0.42 seconds). Ground clauses: seen=110689, kept=110689. Selections=141, assignments=2715, propagations=30441, current_models=1. Rewrite_terms=625831, rewrite_bools=116620, indexes=170605. Rules_from_neg_clauses=0, cross_offs=7. ============================== end of statistics ===================== User_CPU=0.42, System_CPU=0.04, Wall_clock=0. Exiting with 1 model. Process 4320 exit (max_models) Tue Nov 3 09:38:38 2009 The process finished Tue Nov 3 09:38:38 2009