============================== Mace4 ================================= Mace4 (32) version Dec-2007, Dec 2007. Process 3876 was started by Alexei on Alexei-PC, Sun Mar 17 22:02:33 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 * a7. a4 = a3 * a1. a5 = a4 * a2. a6 = a5 * a9. a7 = a6 * a8. a8 = a7 * a3. a9 = a8 * a5. a10 = a9 * a6. a1 = a10 * a4. 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 * a7. a4 = a3 * a1. a5 = a4 * a2. a6 = a5 * a9. a7 = a6 * a8. a8 = a7 * a3. a9 = a8 * a5. a10 = a9 * a6. a1 = a10 * a4. a1 != a2 | a3 != a2 | a4 != a3 | a5 != a4 | a6 != a5 | a6 != a7 | a8 != a7 | a8 != a9 | 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=4, assignments=7, propagations=15, current_models=0. Rewrite_terms=79, rewrite_bools=23, indexes=0. Rules_from_neg_clauses=7, cross_offs=7. ============================== 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=6, assignments=13, propagations=52, current_models=0. Rewrite_terms=567, rewrite_bools=134, indexes=46. Rules_from_neg_clauses=14, cross_offs=35. ============================== 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=11, assignments=32, propagations=101, current_models=0. Rewrite_terms=1468, rewrite_bools=318, indexes=158. Rules_from_neg_clauses=18, cross_offs=75. ============================== 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=15, assignments=51, propagations=170, current_models=0. Rewrite_terms=2495, rewrite_bools=456, indexes=332. Rules_from_neg_clauses=26, cross_offs=188. ============================== 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=18, assignments=68, propagations=275, current_models=0. Rewrite_terms=6728, rewrite_bools=1488, indexes=587. Rules_from_neg_clauses=49, cross_offs=399. ============================== 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=27, assignments=128, propagations=418, current_models=0. Rewrite_terms=9603, rewrite_bools=1705, indexes=1109. Rules_from_neg_clauses=62, cross_offs=681. ============================== 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=32, assignments=168, propagations=606, current_models=0. Rewrite_terms=14229, rewrite_bools=2229, indexes=1958. Rules_from_neg_clauses=63, cross_offs=1140. ============================== end of statistics ===================== ============================== DOMAIN SIZE 9 ========================= ============================== STATISTICS ============================ For domain size 9. Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). Ground clauses: seen=830, kept=812. Selections=40, assignments=239, propagations=945, current_models=0. Rewrite_terms=22897, rewrite_bools=3403, indexes=3318. Rules_from_neg_clauses=75, cross_offs=1840. ============================== 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=45, assignments=288, propagations=1307, current_models=0. Rewrite_terms=35975, rewrite_bools=5694, indexes=4958. Rules_from_neg_clauses=115, cross_offs=3056. ============================== 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=56, assignments=403, propagations=1895, current_models=0. Rewrite_terms=47691, rewrite_bools=6568, indexes=7177. Rules_from_neg_clauses=136, cross_offs=4935. ============================== 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=65, assignments=506, propagations=2628, current_models=0. Rewrite_terms=73174, rewrite_bools=10802, indexes=10128. Rules_from_neg_clauses=213, cross_offs=7270. ============================== 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=81, assignments=708, propagations=3681, current_models=0. Rewrite_terms=108546, rewrite_bools=16479, indexes=14704. Rules_from_neg_clauses=195, cross_offs=10250. ============================== 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=89, assignments=816, propagations=4456, current_models=0. Rewrite_terms=130543, rewrite_bools=18312, indexes=18445. Rules_from_neg_clauses=284, cross_offs=14024. ============================== end of statistics ===================== ============================== DOMAIN SIZE 15 ======================== ============================== MODEL ================================= interpretation( 15, [number=1, seconds=0], [ function(a1, [ 0 ]), function(a10, [ 1 ]), function(a2, [ 3 ]), function(a3, [ 3 ]), function(a4, [ 2 ]), function(a5, [ 1 ]), function(a6, [ 5 ]), function(a7, [ 5 ]), function(a8, [ 5 ]), function(a9, [ 7 ]), function(*(_,_), [ 0, 3, 1, 4, 2, 9,12, 0,11, 6,13, 8, 5,10, 0, 4, 1, 0, 2, 3, 7,13, 5,14, 1,12, 1,10, 8, 6, 3, 4, 2, 1, 0, 8, 2,12, 5,14, 2,13,11, 7, 9, 2, 0, 4, 3, 1, 3,11, 9,10, 8, 7, 6,14, 3,12, 1, 2, 3, 0, 4,10, 7, 6, 4,13,11,14, 4, 9, 5, 6, 7, 8, 5,11, 5, 9, 1, 2,12,14,10, 0, 5, 4, 5, 8, 6,11, 7,12, 6, 4,13, 0, 6, 3, 9,14, 1, 7, 5,11, 8, 6, 1, 4, 7, 9,10, 3,12,13, 2, 7, 11, 6, 5, 7, 8, 2,14,10, 8, 3, 9, 0, 8, 1,13, 12, 9,14,10,13, 0, 5, 3, 7, 9, 8, 9, 6, 4, 2, 13,12,10, 9,14, 4,10, 8, 3, 7,10, 5, 1, 0,11, 8,11, 7, 6, 5,14, 3,13, 0,11, 4,11, 2,12,10, 9,10,13,14,12, 6, 0, 2,12, 5, 1, 7,12,11, 3, 10,14,12,13, 9,13, 1,11, 6, 4, 0, 2, 7,13, 8, 14,13, 9,12,10,11, 8,14, 1, 2, 5, 4, 3, 6,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=50, assignments=388, propagations=1940, current_models=1. Rewrite_terms=56081, rewrite_bools=8142, indexes=8222. Rules_from_neg_clauses=92, cross_offs=6081. ============================== end of statistics ===================== User_CPU=0.12, System_CPU=0.01, Wall_clock=1. Exiting with 1 model. Process 3876 exit (max_models) Sun Mar 17 22:02:34 2013 The process finished Sun Mar 17 22:02:34 2013