============================== Mace4 ================================= Mace4 (32) version Dec-2007, Dec 2007. Process 3432 was started by Alexei on Alexei-PC, Sat Mar 16 12:34:17 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 * a7. a3 = a2 * a6. a4 = a3 * a10. a5 = a4 * a9. a6 = a5 * a8. a7 = a6 * a2. a8 = a7 * a1. a9 = a8 * a5. a10 = a9 * a4. 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 * a7. a3 = a2 * a6. a4 = a3 * a10. a5 = a4 * a9. a6 = a5 * a8. a7 = a6 * a2. a8 = a7 * a1. a9 = a8 * a5. a10 = a9 * a4. a1 = a10 * a3. a1 != a2 | a3 != a2 | a4 != a3 | a5 != a4 | a5 != a6 | 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=14, current_models=0. Rewrite_terms=74, rewrite_bools=22, 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=57, current_models=0. Rewrite_terms=594, rewrite_bools=137, indexes=42. Rules_from_neg_clauses=18, cross_offs=39. ============================== 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=10, assignments=28, propagations=99, current_models=0. Rewrite_terms=1282, rewrite_bools=260, indexes=140. Rules_from_neg_clauses=26, cross_offs=99. ============================== end of statistics ===================== ============================== DOMAIN SIZE 5 ========================= ============================== MODEL ================================= interpretation( 5, [number=1, seconds=0], [ function(a1, [ 0 ]), function(a10, [ 1 ]), function(a2, [ 4 ]), function(a3, [ 2 ]), function(a4, [ 4 ]), function(a5, [ 0 ]), function(a6, [ 1 ]), function(a7, [ 3 ]), function(a8, [ 2 ]), function(a9, [ 3 ]), function(*(_,_), [ 0, 3, 1, 4, 2, 4, 1, 0, 2, 3, 3, 4, 2, 1, 0, 2, 0, 4, 3, 1, 1, 2, 3, 0, 4 ]) ]). ============================== end of model ========================== ============================== STATISTICS ============================ For domain size 5. Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). Ground clauses: seen=166, kept=156. Selections=13, assignments=43, propagations=146, current_models=1. Rewrite_terms=2268, rewrite_bools=439, indexes=276. Rules_from_neg_clauses=30, cross_offs=206. ============================== end of statistics ===================== User_CPU=0.00, System_CPU=0.03, Wall_clock=0. Exiting with 1 model. Process 3432 exit (max_models) Sat Mar 16 12:34:17 2013 The process finished Sat Mar 16 12:34:17 2013