============================== Mace4 ================================= Mace4 (32) version 22-May-2007, May 2007. Process 26991 was started by mccune on cleo, Tue May 22 14:44:32 2007 The command was "/home/mccune/bin/mace4 -f nonmodular-oml.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file nonmodular-oml.in assign(iterate_up_to,10). formulas(theory). 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. x v (c(x) ^ (x v y)) = x v y. A v (B ^ (A v C)) != (A v B) ^ (A v C). 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. x v (c(x) ^ (x v y)) = x v y. A v (B ^ (A v C)) != (A v B) ^ (A v C). end_of_list. ============================== end of clauses for search ============= % The maximum domain element in the input is 1. ============================== DOMAIN SIZE 2 ========================= ============================== STATISTICS ============================ For domain size 2. Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). Ground clauses: seen=59, kept=38. Selections=7, assignments=14, propagations=10, current_models=0. Rewrite_terms=180, rewrite_bools=45, 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.00 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.00 seconds). Ground clauses: seen=261, kept=228. Selections=14, assignments=49, propagations=36, current_models=0. Rewrite_terms=1041, rewrite_bools=263, 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.00 seconds). Ground clauses: seen=446, kept=418. Selections=10, assignments=33, propagations=58, current_models=0. Rewrite_terms=1242, rewrite_bools=294, indexes=242. Rules_from_neg_clauses=4, cross_offs=44. ============================== end of statistics ===================== ============================== DOMAIN SIZE 6 ========================= ============================== STATISTICS ============================ For domain size 6. Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). Ground clauses: seen=703, kept=670. Selections=31, assignments=152, propagations=283, current_models=0. Rewrite_terms=9025, rewrite_bools=2714, indexes=510. Rules_from_neg_clauses=49, cross_offs=307. ============================== end of statistics ===================== ============================== DOMAIN SIZE 7 ========================= ============================== STATISTICS ============================ For domain size 7. Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds). Ground clauses: seen=1044, kept=1006. Selections=23, assignments=104, propagations=123, current_models=0. Rewrite_terms=3630, rewrite_bools=745, indexes=652. Rules_from_neg_clauses=7, cross_offs=193. ============================== 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=1438. Selections=46, assignments=271, propagations=911, current_models=0. Rewrite_terms=32276, rewrite_bools=9591, indexes=2191. Rules_from_neg_clauses=98, cross_offs=2215. ============================== 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=1978. Selections=52, assignments=319, propagations=776, current_models=0. Rewrite_terms=29175, rewrite_bools=7706, indexes=3336. Rules_from_neg_clauses=40, cross_offs=3285. ============================== end of statistics ===================== ============================== DOMAIN SIZE 10 ======================== ============================== MODEL ================================= interpretation( 10, [number=1, seconds=0], [ function(A, [ 2 ]), function(B, [ 4 ]), function(C, [ 6 ]), function(c(_), [ 1, 0, 3, 2, 5, 4, 7, 6, 9, 8 ]), function(^(_,_), [ 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 0, 2, 2, 0, 0, 0, 0, 2, 2, 0, 0, 3, 0, 3, 0, 0, 6, 9, 6, 9, 0, 4, 0, 0, 4, 0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 5, 0, 0, 0, 0, 0, 6, 0, 6, 0, 0, 6, 0, 6, 0, 0, 7, 2, 9, 0, 0, 0, 7, 2, 9, 0, 8, 2, 6, 0, 0, 6, 2, 8, 0, 0, 9, 0, 9, 0, 0, 0, 9, 0, 9 ]), function(v(_,_), [ 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 8, 7, 8, 7, 3, 1, 1, 3, 1, 1, 3, 1, 1, 3, 4, 1, 1, 1, 4, 1, 1, 1, 1, 1, 5, 1, 1, 1, 1, 5, 1, 1, 1, 1, 6, 1, 8, 3, 1, 1, 6, 1, 8, 3, 7, 1, 7, 1, 1, 1, 1, 7, 1, 7, 8, 1, 8, 1, 1, 1, 8, 1, 8, 1, 9, 1, 7, 3, 1, 1, 3, 7, 1, 9 ]) ]). ============================== end of model ========================== ============================== STATISTICS ============================ For domain size 10. Current CPU time: 0.00 seconds (total CPU time: 0.04 seconds). Ground clauses: seen=2691, kept=2638. Selections=51, assignments=290, propagations=831, current_models=1. Rewrite_terms=33975, rewrite_bools=8673, indexes=3737. Rules_from_neg_clauses=71, cross_offs=4282. ============================== end of statistics ===================== User_CPU=0.04, System_CPU=0.00, Wall_clock=0. Exiting with 1 model. Process 26991 exit (max_models) Tue May 22 14:44:32 2007 The process finished Tue May 22 14:44:32 2007