============================== Mace4 ================================= Mace4 (32) version 2009-11A, November 2009. Process 4321 was started by mccune on cleo, Tue Nov 3 09:38:38 2009 The command was "/home/mccune/LADR/bin/mace4 -f noncommutative-ring.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file noncommutative-ring.in formulas(assumptions). 0 + x = x. x + 0 = x. -x + x = 0. x + -x = 0. (x + y) + z = x + (y + z). x + y = y + x. (x * y) * z = x * (y * z). x * (y + z) = (x * y) + (x * z). (y + z) * x = (y * x) + (z * x). --x = x. -0 = 0. 0 * x = 0. x * 0 = 0. 1 * x = x. x * 1 = x. 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). 0 + x = x. x + 0 = x. -x + x = 0. x + -x = 0. (x + y) + z = x + (y + z). x + y = y + x. (x * y) * z = x * (y * z). x * (y + z) = (x * y) + (x * z). (x + y) * z = (x * z) + (y * z). --x = x. -0 = 0. 0 * x = 0. x * 0 = 0. 1 * x = x. x * 1 = x. a * b != b * a. end_of_list. ============================== end of clauses for search ============= % The largest natural number in the input is 1. ============================== DOMAIN SIZE 2 ========================= ============================== STATISTICS ============================ For domain size 2. Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds). Ground clauses: seen=56, kept=34. Selections=3, assignments=6, propagations=10, current_models=0. Rewrite_terms=127, rewrite_bools=37, indexes=4. Rules_from_neg_clauses=2, cross_offs=2. ============================== 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=146, kept=126. Selections=5, assignments=15, propagations=25, current_models=0. Rewrite_terms=568, rewrite_bools=157, indexes=35. Rules_from_neg_clauses=4, cross_offs=11. ============================== 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=310, kept=285. Selections=12, assignments=44, propagations=54, current_models=0. Rewrite_terms=1781, rewrite_bools=469, indexes=103. Rules_from_neg_clauses=10, cross_offs=43. ============================== 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=572, kept=542. Selections=19, assignments=81, propagations=147, current_models=0. Rewrite_terms=3588, rewrite_bools=850, indexes=324. Rules_from_neg_clauses=39, cross_offs=157. ============================== end of statistics ===================== ============================== DOMAIN SIZE 6 ========================= ============================== STATISTICS ============================ For domain size 6. Current CPU time: 0.00 seconds (total CPU time: 0.02 seconds). Ground clauses: seen=956, kept=921. Selections=28, assignments=136, propagations=240, current_models=0. Rewrite_terms=6635, rewrite_bools=1516, indexes=584. Rules_from_neg_clauses=96, cross_offs=451. ============================== end of statistics ===================== ============================== DOMAIN SIZE 7 ========================= ============================== STATISTICS ============================ For domain size 7. Current CPU time: 0.00 seconds (total CPU time: 0.02 seconds). Ground clauses: seen=1486, kept=1446. Selections=48, assignments=266, propagations=547, current_models=0. Rewrite_terms=15614, rewrite_bools=3261, indexes=1867. Rules_from_neg_clauses=154, cross_offs=1098. ============================== end of statistics ===================== ============================== DOMAIN SIZE 8 ========================= ============================== MODEL ================================= interpretation( 8, [number=1, seconds=0], [ function(a, [ 2 ]), function(b, [ 4 ]), function(-(_), [ 0, 1, 2, 3, 4, 5, 6, 7 ]), function(*(_,_), [ 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 2, 3, 4, 5, 6, 7, 0, 2, 0, 2, 0, 2, 0, 2, 0, 3, 2, 1, 4, 7, 6, 5, 0, 4, 2, 6, 4, 0, 6, 2, 0, 5, 0, 5, 0, 5, 0, 5, 0, 6, 2, 4, 4, 2, 6, 0, 0, 7, 0, 7, 0, 7, 0, 7 ]), function(+(_,_), [ 0, 1, 2, 3, 4, 5, 6, 7, 1, 0, 3, 2, 5, 4, 7, 6, 2, 3, 0, 1, 6, 7, 4, 5, 3, 2, 1, 0, 7, 6, 5, 4, 4, 5, 6, 7, 0, 1, 2, 3, 5, 4, 7, 6, 1, 0, 3, 2, 6, 7, 4, 5, 2, 3, 0, 1, 7, 6, 5, 4, 3, 2, 1, 0 ]) ]). ============================== end of model ========================== ============================== STATISTICS ============================ For domain size 8. Current CPU time: 0.00 seconds (total CPU time: 0.03 seconds). Ground clauses: seen=2186, kept=2141. Selections=15, assignments=63, propagations=238, current_models=1. Rewrite_terms=11758, rewrite_bools=2551, indexes=1472. Rules_from_neg_clauses=20, cross_offs=561. ============================== end of statistics ===================== User_CPU=0.03, System_CPU=0.00, Wall_clock=0. Exiting with 1 model. Process 4321 exit (max_models) Tue Nov 3 09:38:38 2009 The process finished Tue Nov 3 09:38:38 2009