============================== Mace4 ================================= Mace4 (32) version Dec-2007, Dec 2007. Process 1524 was started by Alexei on Alexei-PC, Wed Apr 17 23:55:56 2013 The command was "/cygdrive/c/Program Files (x86)/Prover9-Mace4/bin-win32/mace4 -c". ============================== end of head =========================== ============================== INPUT ================================= assign(report_stderr,2). set(ignore_option_dependencies). if(Prover9). % Conditional input omitted. end_if. if(Mace4). % Conditional input included. assign(max_seconds,60). end_if. formulas(assumptions). x * x = x. (x * y) * y = x. (x * y) * z = (x * z) * (y * z). a2 = a1 * a10. a3 = a2 * a6. a4 = a3 * a1. a5 = a4 * a8. a6 = a5 * a3. a7 = a6 * a9. a8 = a7 * a10. a9 = a8 * a5. a10 = a9 * a7. a1 = a10 * a3. end_of_list. formulas(goals). a1 = a2 & a2 = a3 & a3 = a4 & a4 = a5 & a5 = a6 & a6 = a7 & a7 = a8 & a8 = a9 & a9 = a10. end_of_list. ============================== end of input ========================== % Enabling option dependencies (ignore applies only on input). ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 a1 = a2 & a2 = a3 & a3 = a4 & a4 = a5 & a5 = a6 & a6 = a7 & a7 = a8 & a8 = a9 & a9 = a10 # label(non_clause) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== CLAUSES FOR SEARCH ==================== formulas(mace4_clauses). x * x = x. (x * y) * y = x. (x * y) * z = (x * z) * (y * z). a2 = a1 * a10. a3 = a2 * a6. a4 = a3 * a1. a5 = a4 * a8. a6 = a5 * a3. a7 = a6 * a9. a8 = a7 * a10. a9 = a8 * a5. a10 = a9 * a7. a1 = a10 * a3. a1 != a2 | a3 != a2 | a4 != a3 | a5 != a4 | a5 != a6 | a7 != a6 | a7 != a8 | a9 != a8 | a9 != a10. end_of_list. ============================== end of clauses for search ============= % There are no domain elements in the input. ============================== DOMAIN SIZE 2 ========================= ============================== STATISTICS ============================ For domain size 2. Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). Ground clauses: seen=25, kept=15. Selections=5, assignments=9, propagations=17, current_models=0. Rewrite_terms=88, rewrite_bools=25, indexes=0. Rules_from_neg_clauses=6, cross_offs=6. ============================== end of statistics ===================== ============================== DOMAIN SIZE 3 ========================= ============================== STATISTICS ============================ For domain size 3. Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). Ground clauses: seen=50, kept=44. Selections=7, assignments=15, propagations=59, current_models=0. Rewrite_terms=688, rewrite_bools=161, indexes=55. Rules_from_neg_clauses=17, cross_offs=37. ============================== 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=95, kept=87. Selections=15, assignments=45, propagations=100, current_models=0. Rewrite_terms=1534, rewrite_bools=318, indexes=165. Rules_from_neg_clauses=24, cross_offs=104. ============================== 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=166, kept=156. Selections=18, assignments=58, propagations=152, current_models=0. Rewrite_terms=2393, rewrite_bools=431, indexes=334. Rules_from_neg_clauses=28, cross_offs=228. ============================== 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=269, kept=257. Selections=25, assignments=95, propagations=246, current_models=0. Rewrite_terms=5480, rewrite_bools=1034, indexes=708. Rules_from_neg_clauses=35, cross_offs=436. ============================== end of statistics ===================== ============================== DOMAIN SIZE 7 ========================= ============================== STATISTICS ============================ For domain size 7. Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). Ground clauses: seen=410, kept=396. Selections=33, assignments=147, propagations=426, current_models=0. Rewrite_terms=10191, rewrite_bools=1796, indexes=1406. Rules_from_neg_clauses=55, cross_offs=899. ============================== end of statistics ===================== ============================== DOMAIN SIZE 8 ========================= ============================== STATISTICS ============================ For domain size 8. Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). Ground clauses: seen=595, kept=579. Selections=41, assignments=209, propagations=673, current_models=0. Rewrite_terms=15954, rewrite_bools=2551, indexes=2320. Rules_from_neg_clauses=81, cross_offs=1587. ============================== end of statistics ===================== ============================== DOMAIN SIZE 9 ========================= ============================== STATISTICS ============================ For domain size 9. Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds). Ground clauses: seen=830, kept=812. Selections=53, assignments=311, propagations=1089, current_models=0. Rewrite_terms=27226, rewrite_bools=4276, indexes=3981. Rules_from_neg_clauses=111, cross_offs=2919. ============================== end of statistics ===================== ============================== DOMAIN SIZE 10 ======================== ============================== STATISTICS ============================ For domain size 10. Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds). Ground clauses: seen=1121, kept=1101. Selections=64, assignments=415, propagations=1569, current_models=0. Rewrite_terms=38620, rewrite_bools=5870, indexes=6111. Rules_from_neg_clauses=145, cross_offs=4389. ============================== end of statistics ===================== ============================== DOMAIN SIZE 11 ======================== ============================== STATISTICS ============================ For domain size 11. Current CPU time: 0.00 seconds (total CPU time: 0.03 seconds). Ground clauses: seen=1474, kept=1452. Selections=78, assignments=560, propagations=2217, current_models=0. Rewrite_terms=56374, rewrite_bools=8309, indexes=8708. Rules_from_neg_clauses=232, cross_offs=6787. ============================== end of statistics ===================== ============================== DOMAIN SIZE 12 ======================== ============================== STATISTICS ============================ For domain size 12. Current CPU time: 0.00 seconds (total CPU time: 0.05 seconds). Ground clauses: seen=1895, kept=1871. Selections=92, assignments=718, propagations=2926, current_models=0. Rewrite_terms=82789, rewrite_bools=12668, indexes=12091. Rules_from_neg_clauses=252, cross_offs=10119. ============================== end of statistics ===================== ============================== DOMAIN SIZE 13 ======================== ============================== STATISTICS ============================ For domain size 13. Current CPU time: 0.00 seconds (total CPU time: 0.08 seconds). Ground clauses: seen=2390, kept=2364. Selections=106, assignments=893, propagations=3828, current_models=0. Rewrite_terms=104314, rewrite_bools=14232, indexes=16554. Rules_from_neg_clauses=312, cross_offs=14115. ============================== end of statistics ===================== ============================== DOMAIN SIZE 14 ======================== ============================== STATISTICS ============================ For domain size 14. Current CPU time: 0.00 seconds (total CPU time: 0.11 seconds). Ground clauses: seen=2965, kept=2937. Selections=115, assignments=1015, propagations=4575, current_models=0. Rewrite_terms=129704, rewrite_bools=17601, indexes=20897. Rules_from_neg_clauses=252, cross_offs=17716. ============================== end of statistics ===================== ============================== DOMAIN SIZE 15 ======================== ============================== MODEL ================================= interpretation( 15, [number=1, seconds=0], [ function(a1, [ 0 ]), function(a10, [ 1 ]), function(a2, [ 2 ]), function(a3, [ 2 ]), function(a4, [ 1 ]), function(a5, [ 3 ]), function(a6, [ 3 ]), function(a7, [ 6 ]), function(a8, [ 4 ]), function(a9, [ 7 ]), function(*(_,_), [ 0, 2, 1, 8,10,12, 5, 0, 9,11, 4, 3,13, 6, 0, 2, 1, 0, 6, 3, 1, 7, 4,14, 1,13,12,11, 8,10, 1, 0, 2, 2, 5,11, 8,10, 6,12, 9,14, 7, 2, 4, 9, 7, 3, 3, 1,10, 4, 6,11, 8, 5, 0,14, 3,12, 10, 6,11, 7, 4,14, 3, 1, 4,13, 0, 5, 4, 9, 2, 13, 5,14,10, 2, 5, 0, 8, 7, 5, 3, 4, 6,12,11, 12, 4, 8, 1, 7,13, 6, 3, 2,14, 6, 6, 5, 0, 9, 7, 3, 9, 4, 6, 8, 1, 7, 5,10,12,13, 2,11, 7, 11,10, 6, 0, 8, 7, 2, 5, 8, 3,14, 9, 8, 1,13, 3, 9, 7,11,13, 9,14,12, 0, 9, 2, 8,10, 4, 6, 4, 8,12, 5, 0, 3,10, 2,13, 7,10,10, 9,14, 1, 8,12, 4, 9,14, 2,11,13, 3, 0,11,11, 1, 7, 5, 6,11,10,14,12, 0,13, 9,12, 2, 7, 1,12, 5, 3, 5,14,13,13, 9, 6,12,11,10, 4, 1, 7, 0,13, 8, 14,13, 5,12,11, 4, 9,14, 1, 6, 8, 2, 3,10,14 ]) ]). ============================== end of model ========================== ============================== STATISTICS ============================ For domain size 15. Current CPU time: 0.00 seconds (total CPU time: 0.12 seconds). Ground clauses: seen=3626, kept=3596. Selections=39, assignments=235, propagations=967, current_models=1. Rewrite_terms=32913, rewrite_bools=5353, indexes=4314. Rules_from_neg_clauses=48, cross_offs=3768. ============================== end of statistics ===================== User_CPU=0.12, System_CPU=0.01, Wall_clock=0. Exiting with 1 model. Process 1524 exit (max_models) Wed Apr 17 23:55:56 2013 The process finished Wed Apr 17 23:55:56 2013