============================== Mace4 ================================= Mace4 (32) version 2009-11A, November 2009. Process 4305 was started by mccune on cleo, Tue Nov 3 09:37:33 2009 The command was "/home/mccune/LADR/bin/mace4 -f ring.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file ring.in assign(iterate_up_to,25). % assign(iterate_up_to, 25) -> assign(end_size, 25). assign(max_models,1000). set(integer_ring). % set(integer_ring) -> clear(lnh). formulas(theory). x @ y = (A * x) + (B * y). (x @ e) @ x = x. x @ (x @ y) = y. (x @ y) @ (z @ u) = (x @ z) @ (y @ u). ((x @ x) @ x) @ x = e. 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). x @ y = (A * x) + (B * y). (x @ e) @ x = x. x @ (x @ y) = y. (x @ y) @ (z @ u) = (x @ z) @ (y @ u). ((x @ x) @ x) @ x = e. end_of_list. ============================== end of clauses for search ============= % There are no natural numbers 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=28, kept=28. Selections=3, assignments=6, propagations=20, current_models=0. Rewrite_terms=230, rewrite_bools=28, indexes=0. Rules_from_neg_clauses=0, cross_offs=0. ============================== 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=105, kept=105. Selections=4, assignments=12, propagations=90, current_models=0. Rewrite_terms=885, rewrite_bools=56, indexes=0. Rules_from_neg_clauses=0, cross_offs=0. ============================== 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=296, kept=296. Selections=5, assignments=20, propagations=272, current_models=0. Rewrite_terms=2760, rewrite_bools=108, indexes=0. Rules_from_neg_clauses=0, cross_offs=0. ============================== 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=685, kept=685. Selections=6, assignments=30, propagations=650, current_models=0. Rewrite_terms=5825, rewrite_bools=154, indexes=0. Rules_from_neg_clauses=0, cross_offs=0. ============================== 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=1380, kept=1380. Selections=7, assignments=42, propagations=1332, current_models=0. Rewrite_terms=10896, rewrite_bools=164, indexes=0. Rules_from_neg_clauses=0, cross_offs=0. ============================== end of statistics ===================== ============================== DOMAIN SIZE 7 ========================= ============================== MODEL ================================= interpretation( 7, [number=1, seconds=0], [ function(A, [ 3 ]), function(B, [ 6 ]), function(e, [ 0 ]), function(*(_,_), [ 0, 0, 0, 0, 0, 0, 0, 0, 1, 2, 3, 4, 5, 6, 0, 2, 4, 6, 1, 3, 5, 0, 3, 6, 2, 5, 1, 4, 0, 4, 1, 5, 2, 6, 3, 0, 5, 3, 1, 6, 4, 2, 0, 6, 5, 4, 3, 2, 1 ]), function(+(_,_), [ 0, 1, 2, 3, 4, 5, 6, 1, 2, 3, 4, 5, 6, 0, 2, 3, 4, 5, 6, 0, 1, 3, 4, 5, 6, 0, 1, 2, 4, 5, 6, 0, 1, 2, 3, 5, 6, 0, 1, 2, 3, 4, 6, 0, 1, 2, 3, 4, 5 ]), function(@(_,_), [ 0, 6, 5, 4, 3, 2, 1, 3, 2, 1, 0, 6, 5, 4, 6, 5, 4, 3, 2, 1, 0, 2, 1, 0, 6, 5, 4, 3, 5, 4, 3, 2, 1, 0, 6, 1, 0, 6, 5, 4, 3, 2, 4, 3, 2, 1, 0, 6, 5 ]) ]). ============================== end of model ========================== ============================== STATISTICS ============================ For domain size 7. Current CPU time: 0.00 seconds (total CPU time: 0.04 seconds). Ground clauses: seen=2513, kept=2513. Selections=8, assignments=56, propagations=2450, current_models=1. Rewrite_terms=36217, rewrite_bools=2829, indexes=0. Rules_from_neg_clauses=0, cross_offs=0. ============================== end of statistics ===================== ============================== DOMAIN SIZE 8 ========================= ============================== STATISTICS ============================ For domain size 8. Current CPU time: 0.00 seconds (total CPU time: 0.05 seconds). Ground clauses: seen=4240, kept=4240. Selections=9, assignments=72, propagations=4160, current_models=0. Rewrite_terms=39576, rewrite_bools=420, indexes=0. Rules_from_neg_clauses=0, cross_offs=0. ============================== end of statistics ===================== ============================== DOMAIN SIZE 9 ========================= ============================== STATISTICS ============================ For domain size 9. Current CPU time: 0.00 seconds (total CPU time: 0.08 seconds). Ground clauses: seen=6741, kept=6741. Selections=10, assignments=90, propagations=6642, current_models=0. Rewrite_terms=58177, rewrite_bools=488, indexes=0. Rules_from_neg_clauses=0, cross_offs=0. ============================== end of statistics ===================== ============================== DOMAIN SIZE 10 ======================== ============================== STATISTICS ============================ For domain size 10. Current CPU time: 0.00 seconds (total CPU time: 0.12 seconds). Ground clauses: seen=10220, kept=10220. Selections=11, assignments=110, propagations=10100, current_models=0. Rewrite_terms=78490, rewrite_bools=454, indexes=0. Rules_from_neg_clauses=0, cross_offs=0. ============================== end of statistics ===================== ============================== DOMAIN SIZE 11 ======================== ============================== STATISTICS ============================ For domain size 11. Current CPU time: 0.00 seconds (total CPU time: 0.18 seconds). Ground clauses: seen=14905, kept=14905. Selections=12, assignments=132, propagations=14762, current_models=0. Rewrite_terms=117509, rewrite_bools=736, indexes=0. Rules_from_neg_clauses=0, cross_offs=0. ============================== end of statistics ===================== ============================== DOMAIN SIZE 12 ======================== ============================== STATISTICS ============================ For domain size 12. Current CPU time: 0.00 seconds (total CPU time: 0.28 seconds). Ground clauses: seen=21048, kept=21048. Selections=13, assignments=156, propagations=20880, current_models=0. Rewrite_terms=165120, rewrite_bools=652, indexes=0. Rules_from_neg_clauses=0, cross_offs=0. ============================== end of statistics ===================== ============================== DOMAIN SIZE 13 ======================== ============================== STATISTICS ============================ For domain size 13. Current CPU time: 0.00 seconds (total CPU time: 0.40 seconds). Ground clauses: seen=28925, kept=28925. Selections=14, assignments=182, propagations=28730, current_models=0. Rewrite_terms=224625, rewrite_bools=1026, indexes=0. Rules_from_neg_clauses=0, cross_offs=0. ============================== end of statistics ===================== ============================== DOMAIN SIZE 14 ======================== ============================== STATISTICS ============================ For domain size 14. Current CPU time: 0.00 seconds (total CPU time: 0.56 seconds). Ground clauses: seen=38836, kept=38836. Selections=15, assignments=210, propagations=38612, current_models=0. Rewrite_terms=313582, rewrite_bools=1002, indexes=0. Rules_from_neg_clauses=0, cross_offs=0. ============================== end of statistics ===================== ============================== DOMAIN SIZE 15 ======================== ============================== STATISTICS ============================ For domain size 15. Current CPU time: 0.00 seconds (total CPU time: 0.77 seconds). Ground clauses: seen=51105, kept=51105. Selections=16, assignments=240, propagations=50850, current_models=0. Rewrite_terms=381085, rewrite_bools=1024, indexes=0. Rules_from_neg_clauses=0, cross_offs=0. ============================== end of statistics ===================== ============================== DOMAIN SIZE 16 ======================== ============================== STATISTICS ============================ For domain size 16. Current CPU time: 0.00 seconds (total CPU time: 1.07 seconds). Ground clauses: seen=66080, kept=66080. Selections=17, assignments=272, propagations=65792, current_models=0. Rewrite_terms=543948, rewrite_bools=1416, indexes=0. Rules_from_neg_clauses=0, cross_offs=0. ============================== end of statistics ===================== ============================== DOMAIN SIZE 17 ======================== ============================== STATISTICS ============================ For domain size 17. Current CPU time: 0.00 seconds (total CPU time: 1.43 seconds). Ground clauses: seen=84133, kept=84133. Selections=18, assignments=306, propagations=83810, current_models=0. Rewrite_terms=677969, rewrite_bools=1888, indexes=0. Rules_from_neg_clauses=0, cross_offs=0. ============================== end of statistics ===================== ============================== DOMAIN SIZE 18 ======================== ============================== STATISTICS ============================ For domain size 18. Current CPU time: 0.00 seconds (total CPU time: 1.90 seconds). Ground clauses: seen=105660, kept=105660. Selections=19, assignments=342, propagations=105300, current_models=0. Rewrite_terms=823816, rewrite_bools=1460, indexes=0. Rules_from_neg_clauses=0, cross_offs=0. ============================== end of statistics ===================== ============================== DOMAIN SIZE 19 ======================== ============================== STATISTICS ============================ For domain size 19. Current CPU time: 0.00 seconds (total CPU time: 2.47 seconds). Ground clauses: seen=131081, kept=131081. Selections=20, assignments=380, propagations=130682, current_models=0. Rewrite_terms=988821, rewrite_bools=2184, indexes=0. Rules_from_neg_clauses=0, cross_offs=0. ============================== end of statistics ===================== ============================== DOMAIN SIZE 20 ======================== ============================== STATISTICS ============================ For domain size 20. Current CPU time: 0.00 seconds (total CPU time: 3.18 seconds). Ground clauses: seen=160840, kept=160840. Selections=21, assignments=420, propagations=160400, current_models=0. Rewrite_terms=1215540, rewrite_bools=1808, indexes=0. Rules_from_neg_clauses=0, cross_offs=0. ============================== end of statistics ===================== ============================== DOMAIN SIZE 21 ======================== ============================== STATISTICS ============================ For domain size 21. Current CPU time: 0.00 seconds (total CPU time: 4.08 seconds). Ground clauses: seen=195405, kept=195405. Selections=22, assignments=462, propagations=194922, current_models=0. Rewrite_terms=1507537, rewrite_bools=2192, indexes=0. Rules_from_neg_clauses=0, cross_offs=0. ============================== end of statistics ===================== ============================== DOMAIN SIZE 22 ======================== ============================== STATISTICS ============================ For domain size 22. Current CPU time: 0.00 seconds (total CPU time: 5.17 seconds). Ground clauses: seen=235268, kept=235268. Selections=23, assignments=506, propagations=234740, current_models=0. Rewrite_terms=1730296, rewrite_bools=2188, indexes=0. Rules_from_neg_clauses=0, cross_offs=0. ============================== end of statistics ===================== ============================== DOMAIN SIZE 23 ======================== ============================== STATISTICS ============================ For domain size 23. Current CPU time: 0.00 seconds (total CPU time: 6.64 seconds). Ground clauses: seen=280945, kept=280945. Selections=24, assignments=552, propagations=280370, current_models=0. Rewrite_terms=2189897, rewrite_bools=3382, indexes=0. Rules_from_neg_clauses=0, cross_offs=0. ============================== end of statistics ===================== ============================== DOMAIN SIZE 24 ======================== ============================== STATISTICS ============================ For domain size 24. Current CPU time: 0.00 seconds (total CPU time: 8.41 seconds). Ground clauses: seen=332976, kept=332976. Selections=25, assignments=600, propagations=332352, current_models=0. Rewrite_terms=2586616, rewrite_bools=2596, indexes=0. Rules_from_neg_clauses=0, cross_offs=0. ============================== end of statistics ===================== ============================== DOMAIN SIZE 25 ======================== ============================== STATISTICS ============================ For domain size 25. Current CPU time: 0.00 seconds (total CPU time: 10.66 seconds). Ground clauses: seen=391925, kept=391925. Selections=26, assignments=650, propagations=391250, current_models=0. Rewrite_terms=3130409, rewrite_bools=3762, indexes=0. Rules_from_neg_clauses=0, cross_offs=0. ============================== end of statistics ===================== User_CPU=10.66, System_CPU=0.09, Wall_clock=11. Exiting with 1 model. Process 4305 exit (all_models) Tue Nov 3 09:37:44 2009 The process finished Tue Nov 3 09:37:44 2009