diff options
Diffstat (limited to 'logic/logic_b.m4.out')
-rw-r--r-- | logic/logic_b.m4.out | 143 |
1 files changed, 143 insertions, 0 deletions
diff --git a/logic/logic_b.m4.out b/logic/logic_b.m4.out new file mode 100644 index 0000000..43b07fd --- /dev/null +++ b/logic/logic_b.m4.out @@ -0,0 +1,143 @@ +============================== Mace4 ================================= +Mace4 (64) version 2009-11A, November 2009. +Process 3232 was started by koen on vdheijden-arch, +Sun Jan 15 16:43:42 2017 +The command was "mace4 -f logic_b.m4.in". +============================== end of head =========================== + +============================== INPUT ================================= + +% Reading from file logic_b.m4.in + + +formulas(sos). +x * (y * z) = (x * y) * z. +x * I = x. +x * inv(x) = I. +end_of_list. + +formulas(goals). +(all x all y x * y = y * x). +end_of_list. + +============================== end of input ========================== + +============================== PROCESS NON-CLAUSAL FORMULAS ========== + +% Formulas that are not ordinary clauses: +1 (all x all y x * y = y * x) # label(non_clause) # label(goal). [goal]. + +============================== end of process non-clausal formulas === + +============================== CLAUSES FOR SEARCH ==================== + +formulas(mace4_clauses). +x * (y * z) = (x * y) * z. +x * I = x. +x * inv(x) = I. +c2 * c1 != c1 * c2. +end_of_list. + +============================== end of clauses for search ============= + +% There are no natural numbers 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=13, kept=13. +Selections=4, assignments=7, propagations=6, current_models=0. +Rewrite_terms=62, rewrite_bools=16, indexes=8. +Rules_from_neg_clauses=2, cross_offs=2. + +============================== 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=34, kept=34. +Selections=7, assignments=17, propagations=30, current_models=0. +Rewrite_terms=298, rewrite_bools=71, indexes=52. +Rules_from_neg_clauses=8, cross_offs=24. + +============================== 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=73, kept=73. +Selections=14, assignments=45, propagations=110, current_models=0. +Rewrite_terms=1132, rewrite_bools=232, indexes=206. +Rules_from_neg_clauses=18, cross_offs=98. + +============================== 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=136, kept=136. +Selections=24, assignments=91, propagations=201, current_models=0. +Rewrite_terms=2416, rewrite_bools=472, indexes=582. +Rules_from_neg_clauses=31, cross_offs=228. + +============================== end of statistics ===================== + +============================== DOMAIN SIZE 6 ========================= + +============================== MODEL ================================= + +interpretation( 6, [number=1, seconds=0], [ + + function(I, [ 0 ]), + + function(c1, [ 1 ]), + + function(c2, [ 2 ]), + + function(inv(_), [ 0, 1, 2, 4, 3, 5 ]), + + function(*(_,_), [ + 0, 1, 2, 3, 4, 5, + 1, 0, 3, 2, 5, 4, + 2, 4, 0, 5, 1, 3, + 3, 5, 1, 4, 0, 2, + 4, 2, 5, 0, 3, 1, + 5, 3, 4, 1, 2, 0 ]) +]). + +============================== end of model ========================== + +============================== STATISTICS ============================ + +For domain size 6. + +Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds). +Ground clauses: seen=229, kept=229. +Selections=14, assignments=44, propagations=94, current_models=1. +Rewrite_terms=1566, rewrite_bools=339, indexes=370. +Rules_from_neg_clauses=8, cross_offs=138. + +============================== end of statistics ===================== + +User_CPU=0.01, System_CPU=0.00, Wall_clock=0. + +Exiting with 1 model. + +Process 3232 exit (max_models) Sun Jan 15 16:43:42 2017 +The process finished Sun Jan 15 16:43:42 2017 |