============================== Mace4 ================================= Mace4 (32) version 2009-02A, February 2009. Process 11128 was started by mccune on cleo, Wed Feb 25 09:30:43 2009 The command was "/home/mccune/bin/mace4 -f cand23.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file cand23.in assign(iterate_up_to,100). % assign(iterate_up_to, 100) -> assign(end_size, 100). set(iterate_primes). % set(iterate_primes) -> clear(iterate_nonprimes). % set(iterate_primes) -> assign(iterate, primes). set(integer_ring). % set(integer_ring) -> clear(lnh). formulas(theory). g(x) = A * x. f(x,y) = (B * x) + (C * y). f(f(y,g(y)),f(g(f(x,f(g(f(z,z)),z))),x)) = z # label(candidate_23). end_of_list. formulas(goals). f(f(x,y),z) = f(x,f(y,z)). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 f(f(x,y),z) = f(x,f(y,z)) # label(non_clause) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== CLAUSES FOR SEARCH ==================== formulas(mace4_clauses). g(x) = A * x. f(x,y) = (B * x) + (C * y). f(f(x,g(x)),f(g(f(y,f(g(f(z,z)),z))),y)) = z # label(candidate_23). f(f(c1,c2),c3) != f(c1,f(c2,c3)). 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=15, kept=15. Selections=14, assignments=28, propagations=36, current_models=0. Rewrite_terms=503, rewrite_bools=49, indexes=16. 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=40, kept=40. Selections=26, assignments=78, propagations=252, current_models=0. Rewrite_terms=3090, rewrite_bools=159, indexes=81. 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.02 seconds). Ground clauses: seen=156, kept=156. Selections=62, assignments=310, propagations=3150, current_models=0. Rewrite_terms=34124, rewrite_bools=687, indexes=625. Rules_from_neg_clauses=0, cross_offs=0. ============================== end of statistics ===================== ============================== DOMAIN SIZE 7 ========================= ============================== STATISTICS ============================ For domain size 7. Current CPU time: 0.00 seconds (total CPU time: 0.04 seconds). Ground clauses: seen=400, kept=400. Selections=114, assignments=798, propagations=16856, current_models=0. Rewrite_terms=174622, rewrite_bools=1831, indexes=2401. 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.30 seconds). Ground clauses: seen=1464, kept=1464. Selections=266, assignments=2926, propagations=161172, current_models=0. Rewrite_terms=1622666, rewrite_bools=6927, indexes=14641. 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.90 seconds). Ground clauses: seen=2380, kept=2380. Selections=366, assignments=4758, propagations=371462, current_models=0. Rewrite_terms=3721060, rewrite_bools=11359, indexes=28561. 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: 3.22 seconds). Ground clauses: seen=5220, kept=5220. Selections=614, assignments=10438, propagations=1420146, current_models=0. Rewrite_terms=14161472, rewrite_bools=25191, indexes=83521. 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: 7.32 seconds). Ground clauses: seen=7240, kept=7240. Selections=762, assignments=14478, propagations=2476460, current_models=0. Rewrite_terms=24669826, rewrite_bools=35071, indexes=130321. Rules_from_neg_clauses=0, cross_offs=0. ============================== end of statistics ===================== ============================== DOMAIN SIZE 23 ======================== ============================== MODEL ================================= interpretation( 23, [number=1, seconds=10], [ function(A, [ 5 ]), function(B, [12 ]), function(C, [16 ]), function(c1, [ 0 ]), function(c2, [ 0 ]), function(c3, [ 1 ]), function(g(_), [ 0, 5,10,15,20, 2, 7,12,17,22, 4, 9,14,19, 1, 6,11,16,21, 3, 8,13,18 ]), function(*(_,_), [ 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9,10,11,12,13,14,15,16,17,18,19,20,21,22, 0, 2, 4, 6, 8,10,12,14,16,18,20,22, 1, 3, 5, 7, 9,11,13,15,17,19,21, 0, 3, 6, 9,12,15,18,21, 1, 4, 7,10,13,16,19,22, 2, 5, 8,11,14,17,20, 0, 4, 8,12,16,20, 1, 5, 9,13,17,21, 2, 6,10,14,18,22, 3, 7,11,15,19, 0, 5,10,15,20, 2, 7,12,17,22, 4, 9,14,19, 1, 6,11,16,21, 3, 8,13,18, 0, 6,12,18, 1, 7,13,19, 2, 8,14,20, 3, 9,15,21, 4,10,16,22, 5,11,17, 0, 7,14,21, 5,12,19, 3,10,17, 1, 8,15,22, 6,13,20, 4,11,18, 2, 9,16, 0, 8,16, 1, 9,17, 2,10,18, 3,11,19, 4,12,20, 5,13,21, 6,14,22, 7,15, 0, 9,18, 4,13,22, 8,17, 3,12,21, 7,16, 2,11,20, 6,15, 1,10,19, 5,14, 0,10,20, 7,17, 4,14, 1,11,21, 8,18, 5,15, 2,12,22, 9,19, 6,16, 3,13, 0,11,22,10,21, 9,20, 8,19, 7,18, 6,17, 5,16, 4,15, 3,14, 2,13, 1,12, 0,12, 1,13, 2,14, 3,15, 4,16, 5,17, 6,18, 7,19, 8,20, 9,21,10,22,11, 0,13, 3,16, 6,19, 9,22,12, 2,15, 5,18, 8,21,11, 1,14, 4,17, 7,20,10, 0,14, 5,19,10, 1,15, 6,20,11, 2,16, 7,21,12, 3,17, 8,22,13, 4,18, 9, 0,15, 7,22,14, 6,21,13, 5,20,12, 4,19,11, 3,18,10, 2,17, 9, 1,16, 8, 0,16, 9, 2,18,11, 4,20,13, 6,22,15, 8, 1,17,10, 3,19,12, 5,21,14, 7, 0,17,11, 5,22,16,10, 4,21,15, 9, 3,20,14, 8, 2,19,13, 7, 1,18,12, 6, 0,18,13, 8, 3,21,16,11, 6, 1,19,14, 9, 4,22,17,12, 7, 2,20,15,10, 5, 0,19,15,11, 7, 3,22,18,14,10, 6, 2,21,17,13, 9, 5, 1,20,16,12, 8, 4, 0,20,17,14,11, 8, 5, 2,22,19,16,13,10, 7, 4, 1,21,18,15,12, 9, 6, 3, 0,21,19,17,15,13,11, 9, 7, 5, 3, 1,22,20,18,16,14,12,10, 8, 6, 4, 2, 0,22,21,20,19,18,17,16,15,14,13,12,11,10, 9, 8, 7, 6, 5, 4, 3, 2, 1 ]), function(+(_,_), [ 0, 1, 2, 3, 4, 5, 6, 7, 8, 9,10,11,12,13,14,15,16,17,18,19,20,21,22, 1, 2, 3, 4, 5, 6, 7, 8, 9,10,11,12,13,14,15,16,17,18,19,20,21,22, 0, 2, 3, 4, 5, 6, 7, 8, 9,10,11,12,13,14,15,16,17,18,19,20,21,22, 0, 1, 3, 4, 5, 6, 7, 8, 9,10,11,12,13,14,15,16,17,18,19,20,21,22, 0, 1, 2, 4, 5, 6, 7, 8, 9,10,11,12,13,14,15,16,17,18,19,20,21,22, 0, 1, 2, 3, 5, 6, 7, 8, 9,10,11,12,13,14,15,16,17,18,19,20,21,22, 0, 1, 2, 3, 4, 6, 7, 8, 9,10,11,12,13,14,15,16,17,18,19,20,21,22, 0, 1, 2, 3, 4, 5, 7, 8, 9,10,11,12,13,14,15,16,17,18,19,20,21,22, 0, 1, 2, 3, 4, 5, 6, 8, 9,10,11,12,13,14,15,16,17,18,19,20,21,22, 0, 1, 2, 3, 4, 5, 6, 7, 9,10,11,12,13,14,15,16,17,18,19,20,21,22, 0, 1, 2, 3, 4, 5, 6, 7, 8, 10,11,12,13,14,15,16,17,18,19,20,21,22, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11,12,13,14,15,16,17,18,19,20,21,22, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9,10, 12,13,14,15,16,17,18,19,20,21,22, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9,10,11, 13,14,15,16,17,18,19,20,21,22, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9,10,11,12, 14,15,16,17,18,19,20,21,22, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9,10,11,12,13, 15,16,17,18,19,20,21,22, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9,10,11,12,13,14, 16,17,18,19,20,21,22, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9,10,11,12,13,14,15, 17,18,19,20,21,22, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9,10,11,12,13,14,15,16, 18,19,20,21,22, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9,10,11,12,13,14,15,16,17, 19,20,21,22, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9,10,11,12,13,14,15,16,17,18, 20,21,22, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9,10,11,12,13,14,15,16,17,18,19, 21,22, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9,10,11,12,13,14,15,16,17,18,19,20, 22, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9,10,11,12,13,14,15,16,17,18,19,20,21 ]), function(f(_,_), [ 0,16, 9, 2,18,11, 4,20,13, 6,22,15, 8, 1,17,10, 3,19,12, 5,21,14, 7, 12, 5,21,14, 7, 0,16, 9, 2,18,11, 4,20,13, 6,22,15, 8, 1,17,10, 3,19, 1,17,10, 3,19,12, 5,21,14, 7, 0,16, 9, 2,18,11, 4,20,13, 6,22,15, 8, 13, 6,22,15, 8, 1,17,10, 3,19,12, 5,21,14, 7, 0,16, 9, 2,18,11, 4,20, 2,18,11, 4,20,13, 6,22,15, 8, 1,17,10, 3,19,12, 5,21,14, 7, 0,16, 9, 14, 7, 0,16, 9, 2,18,11, 4,20,13, 6,22,15, 8, 1,17,10, 3,19,12, 5,21, 3,19,12, 5,21,14, 7, 0,16, 9, 2,18,11, 4,20,13, 6,22,15, 8, 1,17,10, 15, 8, 1,17,10, 3,19,12, 5,21,14, 7, 0,16, 9, 2,18,11, 4,20,13, 6,22, 4,20,13, 6,22,15, 8, 1,17,10, 3,19,12, 5,21,14, 7, 0,16, 9, 2,18,11, 16, 9, 2,18,11, 4,20,13, 6,22,15, 8, 1,17,10, 3,19,12, 5,21,14, 7, 0, 5,21,14, 7, 0,16, 9, 2,18,11, 4,20,13, 6,22,15, 8, 1,17,10, 3,19,12, 17,10, 3,19,12, 5,21,14, 7, 0,16, 9, 2,18,11, 4,20,13, 6,22,15, 8, 1, 6,22,15, 8, 1,17,10, 3,19,12, 5,21,14, 7, 0,16, 9, 2,18,11, 4,20,13, 18,11, 4,20,13, 6,22,15, 8, 1,17,10, 3,19,12, 5,21,14, 7, 0,16, 9, 2, 7, 0,16, 9, 2,18,11, 4,20,13, 6,22,15, 8, 1,17,10, 3,19,12, 5,21,14, 19,12, 5,21,14, 7, 0,16, 9, 2,18,11, 4,20,13, 6,22,15, 8, 1,17,10, 3, 8, 1,17,10, 3,19,12, 5,21,14, 7, 0,16, 9, 2,18,11, 4,20,13, 6,22,15, 20,13, 6,22,15, 8, 1,17,10, 3,19,12, 5,21,14, 7, 0,16, 9, 2,18,11, 4, 9, 2,18,11, 4,20,13, 6,22,15, 8, 1,17,10, 3,19,12, 5,21,14, 7, 0,16, 21,14, 7, 0,16, 9, 2,18,11, 4,20,13, 6,22,15, 8, 1,17,10, 3,19,12, 5, 10, 3,19,12, 5,21,14, 7, 0,16, 9, 2,18,11, 4,20,13, 6,22,15, 8, 1,17, 22,15, 8, 1,17,10, 3,19,12, 5,21,14, 7, 0,16, 9, 2,18,11, 4,20,13, 6, 11, 4,20,13, 6,22,15, 8, 1,17,10, 3,19,12, 5,21,14, 7, 0,16, 9, 2,18 ]) ]). ============================== end of model ========================== ============================== STATISTICS ============================ For domain size 23. Current CPU time: 0.00 seconds (total CPU time: 10.20 seconds). Ground clauses: seen=12720, kept=12720. Selections=138, assignments=3076, propagations=1554340, current_models=1. Rewrite_terms=15527377, rewrite_bools=21303, indexes=73002. Rules_from_neg_clauses=0, cross_offs=0. ============================== end of statistics ===================== User_CPU=10.20, System_CPU=0.01, Wall_clock=11. Exiting with 1 model. Process 11128 exit (max_models) Wed Feb 25 09:30:54 2009 The process finished Wed Feb 25 09:30:54 2009