============================== Mace4 ================================= Mace4 (32) version Dec-2007, Dec 2007. Process 2724 was started by Alexei on Alexei-PC, Sat Mar 16 12:03:58 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 * a4. a3 = a2 * a5. a4 = a3 * a6. a5 = a4 * a1. a6 = a5 * a8. a7 = a6 * a4. a8 = a7 * a5. a9 = a8 * a7. a1 = a9 * a2. end_of_list. formulas(goals). a1 = a2 & a2 = a3 & a3 = a4 & a4 = a5 & a5 = a6 & a6 = a7 & a7 = a8 & a8 = a9. 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 # 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 * a4. a3 = a2 * a5. a4 = a3 * a6. a5 = a4 * a1. a6 = a5 * a8. a7 = a6 * a4. a8 = a7 * a5. a9 = a8 * a7. a1 = a9 * a2. a1 != a2 | a3 != a2 | a3 != a4 | a5 != a4 | a6 != a5 | a7 != a6 | a7 != a8 | a9 != a8. 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.01 seconds). Ground clauses: seen=24, kept=14. Selections=5, assignments=9, propagations=14, current_models=0. Rewrite_terms=76, 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.01 seconds). Ground clauses: seen=49, kept=43. Selections=6, assignments=12, propagations=49, current_models=0. Rewrite_terms=533, rewrite_bools=121, indexes=56. Rules_from_neg_clauses=16, cross_offs=34. ============================== 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=94, kept=86. Selections=13, assignments=37, propagations=89, current_models=0. Rewrite_terms=1347, rewrite_bools=279, indexes=163. Rules_from_neg_clauses=13, cross_offs=73. ============================== 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=165, kept=155. Selections=16, assignments=50, propagations=120, current_models=0. Rewrite_terms=1987, rewrite_bools=337, indexes=285. Rules_from_neg_clauses=16, cross_offs=164. ============================== 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=268, kept=256. Selections=21, assignments=77, propagations=214, current_models=0. Rewrite_terms=4792, rewrite_bools=936, indexes=514. Rules_from_neg_clauses=31, cross_offs=329. ============================== 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=409, kept=395. Selections=26, assignments=109, propagations=325, current_models=0. Rewrite_terms=6770, rewrite_bools=1232, indexes=872. Rules_from_neg_clauses=39, cross_offs=565. ============================== end of statistics ===================== ============================== DOMAIN SIZE 8 ========================= ============================== STATISTICS ============================ For domain size 8. Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds). Ground clauses: seen=594, kept=578. Selections=32, assignments=154, propagations=448, current_models=0. Rewrite_terms=10778, rewrite_bools=1943, indexes=1448. Rules_from_neg_clauses=48, cross_offs=924. ============================== 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=829, kept=811. Selections=37, assignments=196, propagations=616, current_models=0. Rewrite_terms=15127, rewrite_bools=2457, indexes=1985. Rules_from_neg_clauses=58, cross_offs=1429. ============================== 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=1120, kept=1100. Selections=43, assignments=252, propagations=759, current_models=0. Rewrite_terms=19505, rewrite_bools=3191, indexes=2723. Rules_from_neg_clauses=67, cross_offs=2095. ============================== end of statistics ===================== ============================== DOMAIN SIZE 11 ======================== ============================== STATISTICS ============================ For domain size 11. Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds). Ground clauses: seen=1473, kept=1451. Selections=50, assignments=324, propagations=1035, current_models=0. Rewrite_terms=28421, rewrite_bools=4685, indexes=4030. Rules_from_neg_clauses=66, cross_offs=3121. ============================== end of statistics ===================== ============================== DOMAIN SIZE 12 ======================== ============================== STATISTICS ============================ For domain size 12. Current CPU time: 0.00 seconds (total CPU time: 0.03 seconds). Ground clauses: seen=1894, kept=1870. Selections=56, assignments=393, propagations=1268, current_models=0. Rewrite_terms=36609, rewrite_bools=5725, indexes=5131. Rules_from_neg_clauses=66, cross_offs=4155. ============================== end of statistics ===================== ============================== DOMAIN SIZE 13 ======================== ============================== STATISTICS ============================ For domain size 13. Current CPU time: 0.00 seconds (total CPU time: 0.05 seconds). Ground clauses: seen=2389, kept=2363. Selections=62, assignments=467, propagations=1827, current_models=0. Rewrite_terms=48594, rewrite_bools=7273, indexes=7041. Rules_from_neg_clauses=109, cross_offs=5718. ============================== end of statistics ===================== ============================== DOMAIN SIZE 14 ======================== ============================== STATISTICS ============================ For domain size 14. Current CPU time: 0.00 seconds (total CPU time: 0.08 seconds). Ground clauses: seen=2964, kept=2936. Selections=67, assignments=534, propagations=2230, current_models=0. Rewrite_terms=68337, rewrite_bools=11063, indexes=8603. Rules_from_neg_clauses=110, cross_offs=7490. ============================== end of statistics ===================== ============================== DOMAIN SIZE 15 ======================== ============================== MODEL ================================= interpretation( 15, [number=1, seconds=0], [ function(a1, [ 0 ]), function(a2, [ 1 ]), function(a3, [ 2 ]), function(a4, [ 2 ]), function(a5, [ 3 ]), function(a6, [ 5 ]), function(a7, [ 5 ]), function(a8, [ 6 ]), function(a9, [ 3 ]), function(*(_,_), [ 0, 3, 1, 4, 2, 7, 9,10,14, 6,13, 0, 0, 5, 8, 4, 1, 0, 2, 3, 8, 1,14, 9,12,11,10, 5, 1, 7, 3, 4, 2, 1, 0, 2, 8, 6,11,10, 9, 7,13,12, 2, 2, 0, 4, 3, 1, 6, 5,12, 3,14, 3,13, 7, 9,11, 1, 2, 3, 0, 4,11,12, 4,13, 4,14, 5,10, 8, 6, 10, 9, 5, 6,11, 5, 3,13,12, 8, 7, 4, 1, 0, 5, 9, 6,11, 5,10, 3, 6, 2, 7, 0,12, 8,14, 6, 4, 13,14, 8,12, 7, 0,11, 7, 6, 7, 5, 2, 3,10, 1, 14,12, 7, 8,13, 1, 2,11, 8, 5, 8, 6, 9, 4, 0, 6, 5,10,11, 9,12, 0, 9, 1, 9, 2,14, 8, 3,13, 5,11, 9,10, 6,13,14, 0,10, 2,10, 1, 4, 7,12, 11,10, 6, 9, 5, 4, 7, 8, 2,13, 1,11,11,14, 3, 12, 8,13, 7,14, 9, 4, 3, 5, 1, 6,12,12, 2,10, 7,13,12,14, 8,10,13, 5, 4,11, 0, 3, 2,13, 9, 8, 7,14,13,12,14,10, 1, 0, 3, 4, 9, 6,11,14 ]) ]). ============================== end of model ========================== ============================== STATISTICS ============================ For domain size 15. Current CPU time: 0.00 seconds (total CPU time: 0.08 seconds). Ground clauses: seen=3625, kept=3595. Selections=37, assignments=215, propagations=755, current_models=1. Rewrite_terms=24890, rewrite_bools=4374, indexes=2980. Rules_from_neg_clauses=25, cross_offs=2643. ============================== end of statistics ===================== User_CPU=0.08, System_CPU=0.05, Wall_clock=1. Exiting with 1 model. Process 2724 exit (max_models) Sat Mar 16 12:03:59 2013 The process finished Sat Mar 16 12:03:59 2013