============================== Mace4 ================================= Mace4 (32) version 2009-11A, November 2009. Process 4325 was started by mccune on cleo, Tue Nov 3 09:38:44 2009 The command was "/home/mccune/LADR/bin/mace4 -f rw1.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file rw1.in formulas(assumptions). x ^ y = y ^ x. (x ^ y) ^ z = x ^ (y ^ z). x v y = y v x. (x v y) v z = x v (y v z). x v (x ^ y) = x. x ^ (x v y) = x. x ^ x = x. x v x = x. c(x) ^ x = 0. c(x) v x = 1. c(c(x)) = x. x ^ y = c(c(x) v c(y)). 1 v x = 1. 1 ^ x = x. 0 ^ x = 0. 0 v x = x. (c(x) ^ (x v y)) v (c(y) v (x ^ y)) = 1. A ^ (B v (A ^ (c(A) v (A ^ B)))) != A ^ (c(A) v (A ^ B)). 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 = y ^ x. (x ^ y) ^ z = x ^ (y ^ z). x v y = y v x. (x v y) v z = x v (y v z). x v (x ^ y) = x. x ^ (x v y) = x. x ^ x = x. x v x = x. c(x) ^ x = 0. c(x) v x = 1. c(c(x)) = x. x ^ y = c(c(x) v c(y)). 1 v x = 1. 1 ^ x = x. 0 ^ x = 0. 0 v x = x. (c(x) ^ (x v y)) v (c(y) v (x ^ y)) = 1. A ^ (B v (A ^ (c(A) v (A ^ B)))) != A ^ (c(A) v (A ^ B)). 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=59, kept=38. Selections=3, assignments=6, propagations=10, current_models=0. Rewrite_terms=166, rewrite_bools=41, indexes=14. Rules_from_neg_clauses=2, cross_offs=2. ============================== end of statistics ===================== ============================== DOMAIN SIZE 3 ========================= NOTE: unsatisfiability detected on input. ============================== STATISTICS ============================ For domain size 3. Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds). Ground clauses: seen=117, kept=112. Selections=0, assignments=0, propagations=17, current_models=0. Rewrite_terms=216, rewrite_bools=62, indexes=44. Rules_from_neg_clauses=2, cross_offs=8. ============================== 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=261, kept=228. Selections=4, assignments=13, propagations=36, current_models=0. Rewrite_terms=884, rewrite_bools=237, indexes=109. Rules_from_neg_clauses=3, cross_offs=21. ============================== 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=446, kept=424. Selections=4, assignments=13, propagations=47, current_models=0. Rewrite_terms=1108, rewrite_bools=263, indexes=229. Rules_from_neg_clauses=2, cross_offs=42. ============================== end of statistics ===================== ============================== DOMAIN SIZE 6 ========================= ============================== STATISTICS ============================ For domain size 6. Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds). Ground clauses: seen=703, kept=678. Selections=6, assignments=24, propagations=77, current_models=0. Rewrite_terms=2471, rewrite_bools=615, indexes=393. Rules_from_neg_clauses=6, cross_offs=115. ============================== 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=1044, kept=1016. Selections=6, assignments=24, propagations=76, current_models=0. Rewrite_terms=2362, rewrite_bools=499, indexes=546. Rules_from_neg_clauses=2, cross_offs=128. ============================== end of statistics ===================== ============================== DOMAIN SIZE 8 ========================= ============================== STATISTICS ============================ For domain size 8. Current CPU time: 0.00 seconds (total CPU time: 0.02 seconds). Ground clauses: seen=1481, kept=1450. Selections=9, assignments=46, propagations=206, current_models=0. Rewrite_terms=7743, rewrite_bools=2096, indexes=974. Rules_from_neg_clauses=24, cross_offs=453. ============================== end of statistics ===================== ============================== DOMAIN SIZE 9 ========================= ============================== STATISTICS ============================ For domain size 9. Current CPU time: 0.00 seconds (total CPU time: 0.03 seconds). Ground clauses: seen=2026, kept=1992. Selections=10, assignments=54, propagations=184, current_models=0. Rewrite_terms=7289, rewrite_bools=1727, indexes=1360. Rules_from_neg_clauses=6, cross_offs=654. ============================== end of statistics ===================== ============================== DOMAIN SIZE 10 ======================== ============================== STATISTICS ============================ For domain size 10. Current CPU time: 0.00 seconds (total CPU time: 0.04 seconds). Ground clauses: seen=2691, kept=2654. Selections=16, assignments=108, propagations=543, current_models=0. Rewrite_terms=21552, rewrite_bools=5910, indexes=2152. Rules_from_neg_clauses=50, cross_offs=1488. ============================== end of statistics ===================== ============================== DOMAIN SIZE 11 ======================== ============================== STATISTICS ============================ For domain size 11. Current CPU time: 0.00 seconds (total CPU time: 0.05 seconds). Ground clauses: seen=3488, kept=3448. Selections=19, assignments=138, propagations=456, current_models=0. Rewrite_terms=19192, rewrite_bools=4686, indexes=2897. Rules_from_neg_clauses=9, cross_offs=2010. ============================== end of statistics ===================== ============================== DOMAIN SIZE 12 ======================== ============================== STATISTICS ============================ For domain size 12. Current CPU time: 0.00 seconds (total CPU time: 0.07 seconds). Ground clauses: seen=4429, kept=4386. Selections=24, assignments=193, propagations=738, current_models=0. Rewrite_terms=31231, rewrite_bools=7666, indexes=4086. Rules_from_neg_clauses=37, cross_offs=3358. ============================== end of statistics ===================== ============================== DOMAIN SIZE 13 ======================== ============================== STATISTICS ============================ For domain size 13. Current CPU time: 0.00 seconds (total CPU time: 0.10 seconds). Ground clauses: seen=5526, kept=5480. Selections=29, assignments=253, propagations=812, current_models=0. Rewrite_terms=41463, rewrite_bools=10319, indexes=5396. Rules_from_neg_clauses=13, cross_offs=4719. ============================== end of statistics ===================== ============================== DOMAIN SIZE 14 ======================== ============================== STATISTICS ============================ For domain size 14. Current CPU time: 0.00 seconds (total CPU time: 0.15 seconds). Ground clauses: seen=6791, kept=6742. Selections=41, assignments=410, propagations=1664, current_models=0. Rewrite_terms=81043, rewrite_bools=21492, indexes=8116. Rules_from_neg_clauses=105, cross_offs=7636. ============================== end of statistics ===================== ============================== DOMAIN SIZE 15 ======================== ============================== STATISTICS ============================ For domain size 15. Current CPU time: 0.00 seconds (total CPU time: 0.21 seconds). Ground clauses: seen=8236, kept=8184. Selections=51, assignments=550, propagations=1794, current_models=0. Rewrite_terms=93292, rewrite_bools=23567, indexes=10663. Rules_from_neg_clauses=30, cross_offs=10300. ============================== end of statistics ===================== ============================== DOMAIN SIZE 16 ======================== ============================== STATISTICS ============================ For domain size 16. Current CPU time: 0.00 seconds (total CPU time: 0.35 seconds). Ground clauses: seen=9873, kept=9818. Selections=77, assignments=943, propagations=4271, current_models=0. Rewrite_terms=219182, rewrite_bools=59450, indexes=18426. Rules_from_neg_clauses=299, cross_offs=19636. ============================== end of statistics ===================== ============================== DOMAIN SIZE 17 ======================== ============================== STATISTICS ============================ For domain size 17. Current CPU time: 0.00 seconds (total CPU time: 0.53 seconds). Ground clauses: seen=11714, kept=11656. Selections=97, assignments=1263, propagations=4471, current_models=0. Rewrite_terms=260852, rewrite_bools=69294, indexes=24742. Rules_from_neg_clauses=87, cross_offs=26113. ============================== end of statistics ===================== ============================== DOMAIN SIZE 18 ======================== ============================== STATISTICS ============================ For domain size 18. Current CPU time: 0.00 seconds (total CPU time: 0.98 seconds). Ground clauses: seen=13771, kept=13710. Selections=157, assignments=2292, propagations=10983, current_models=0. Rewrite_terms=644765, rewrite_bools=182109, indexes=44581. Rules_from_neg_clauses=671, cross_offs=50581. ============================== end of statistics ===================== ============================== DOMAIN SIZE 19 ======================== ============================== STATISTICS ============================ For domain size 19. Current CPU time: 0.00 seconds (total CPU time: 1.50 seconds). Ground clauses: seen=16056, kept=15992. Selections=197, assignments=3012, propagations=11320, current_models=0. Rewrite_terms=696762, rewrite_bools=187243, indexes=59577. Rules_from_neg_clauses=318, cross_offs=66099. ============================== end of statistics ===================== ============================== DOMAIN SIZE 20 ======================== ============================== MODEL ================================= interpretation( 20, [number=1, seconds=1], [ function(A, [ 2 ]), function(B, [ 4 ]), function(c(_), [ 1, 0, 3, 2, 5, 4, 7, 6, 9, 8,11,10,13,12,15,14,17,16,19,18 ]), function(^(_,_), [ 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, 0, 2, 2, 0, 6, 0, 6, 9,12, 9,16, 0,12, 9,16, 0,16,18,18,16, 0, 3, 0, 3, 0, 0, 0, 3, 3, 0, 0, 0, 0, 3, 0, 0, 0, 3, 0, 3, 0, 4, 6, 0, 4, 0, 6,11, 6, 0, 6,11, 6,11, 4, 0, 6,11, 0, 6, 0, 5, 0, 0, 0, 5, 0, 5, 0, 0, 5, 0, 0,15, 0,15, 0,15, 0, 0, 0, 6, 6, 0, 6, 0, 6, 0, 6, 0, 6, 0, 6, 0, 6, 0, 6, 0, 0, 6, 0, 7, 9, 3,11, 5, 0, 7, 3, 9, 5,11, 0,13,11,15, 0,17,18, 3, 0, 8,12, 3, 6, 0, 6, 3, 8, 0,12, 0,12, 3,12, 0,12, 3, 0, 8, 0, 9, 9, 0, 0, 0, 0, 9, 0, 9, 0, 0, 0, 9, 0, 0, 0,18,18, 0, 0,10,16, 0, 6, 5, 6, 5,12, 0,10, 0,12,15,16,15,16,15, 0,16, 0,11, 0, 0,11, 0, 0,11, 0, 0, 0,11, 0,11,11, 0, 0,11, 0, 0, 0,12,12, 0, 6, 0, 6, 0,12, 0,12, 0,12, 0,12, 0,12, 0, 0,12, 0,13, 9, 3,11,15, 0,13, 3, 9,15,11, 0,13,11,15, 0,17,18, 3, 0,14,16, 0, 4, 0, 6,11,12, 0,16,11,12,11,14, 0,16,11, 0,16, 0,15, 0, 0, 0,15, 0,15, 0, 0,15, 0, 0,15, 0,15, 0,15, 0, 0, 0,16,16, 0, 6, 0, 6, 0,12, 0,16, 0,12, 0,16, 0,16, 0, 0,16, 0,17,18, 3,11,15, 0,17, 3,18,15,11, 0,17,11,15, 0,17,18, 3, 0,18,18, 0, 0, 0, 0,18, 0,18, 0, 0, 0,18, 0, 0, 0,18,18, 0, 0,19,16, 3, 6, 0, 6, 3, 8, 0,16, 0,12, 3,16, 0,16, 3, 0,19 ]), function(v(_,_), [ 0, 1, 2, 3, 4, 5, 6, 7, 8, 9,10,11,12,13,14,15,16,17,18,19, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 2, 1, 1, 2, 1, 1, 2, 1, 1, 1, 2, 1, 2, 1, 3, 1, 1, 3, 1, 7, 8, 7, 8,13, 1,17, 8,13, 1,17,19,17,17,19, 4, 1, 1, 1, 4, 1, 4, 1, 1, 1, 1, 4,14, 1,14, 1,14, 1, 1, 1, 5, 1, 1, 7, 1, 5,10, 7, 1, 7,10, 7,10, 7, 1, 5,10, 7, 7, 1, 6, 1, 2, 8, 4,10, 6, 1, 8, 2,10, 4,12, 1,14,10,16, 1, 2,19, 7, 1, 1, 7, 1, 7, 1, 7, 1, 7, 1, 7, 1, 7, 1, 7, 1, 7, 7, 1, 8, 1, 1, 8, 1, 1, 8, 1, 8, 1, 1, 1, 8, 1, 1, 1,19, 1, 1,19, 9, 1, 2,13, 1, 7, 2, 7, 1, 9, 1,13, 2,13, 1,13, 2,13, 9, 1, 10, 1, 1, 1, 1,10,10, 1, 1, 1,10, 1,10, 1, 1,10,10, 1, 1, 1, 11, 1, 1,17, 4, 7, 4, 7, 1,13, 1,11,14,13,14,17,14,17,17, 1, 12, 1, 2, 8,14,10,12, 1, 8, 2,10,14,12, 1,14,10,16, 1, 2,19, 13, 1, 1,13, 1, 7, 1, 7, 1,13, 1,13, 1,13, 1,13, 1,13,13, 1, 14, 1, 1, 1,14, 1,14, 1, 1, 1, 1,14,14, 1,14, 1,14, 1, 1, 1, 15, 1, 1,17, 1, 5,10, 7, 1,13,10,17,10,13, 1,15,10,17,17, 1, 16, 1, 2,19,14,10,16, 1,19, 2,10,14,16, 1,14,10,16, 1, 2,19, 17, 1, 1,17, 1, 7, 1, 7, 1,13, 1,17, 1,13, 1,17, 1,17,17, 1, 18, 1, 2,17, 1, 7, 2, 7, 1, 9, 1,17, 2,13, 1,17, 2,17,18, 1, 19, 1, 1,19, 1, 1,19, 1,19, 1, 1, 1,19, 1, 1, 1,19, 1, 1,19 ]) ]). ============================== end of model ========================== ============================== STATISTICS ============================ For domain size 20. Current CPU time: 0.00 seconds (total CPU time: 1.61 seconds). Ground clauses: seen=18581, kept=18514. Selections=34, assignments=305, propagations=1219, current_models=1. Rewrite_terms=92878, rewrite_bools=22938, indexes=12650. Rules_from_neg_clauses=59, cross_offs=11523. ============================== end of statistics ===================== User_CPU=1.61, System_CPU=0.01, Wall_clock=2. Exiting with 1 model. Process 4325 exit (max_models) Tue Nov 3 09:38:46 2009 The process finished Tue Nov 3 09:38:46 2009