part 3 done

3 files changed, 180 insertions, 0 deletions

diff --git a/logic/logic_a.in.aux b/logic/logic_a.in.aux
new file mode 100644
index 0000000..e467de7
--- /dev/null
+++ b/logic/logic_a.in.aux
@@ -0,0 +1,28 @@
+\relax 
+\providecommand\hyper@newdestlabel[2]{}
+\@setckpt{logic/logic_a.in}{
+\setcounter{page}{7}
+\setcounter{equation}{8}
+\setcounter{enumi}{9}
+\setcounter{enumii}{0}
+\setcounter{enumiii}{0}
+\setcounter{enumiv}{0}
+\setcounter{footnote}{0}
+\setcounter{mpfootnote}{0}
+\setcounter{part}{0}
+\setcounter{section}{0}
+\setcounter{subsection}{0}
+\setcounter{subsubsection}{0}
+\setcounter{paragraph}{0}
+\setcounter{subparagraph}{0}
+\setcounter{figure}{0}
+\setcounter{table}{1}
+\setcounter{parentequation}{0}
+\setcounter{lstnumber}{10}
+\setcounter{Item}{9}
+\setcounter{Hfootnote}{0}
+\setcounter{bookmark@seq@number}{0}
+\setcounter{float@type}{8}
+\setcounter{lstlisting}{2}
+\setcounter{section@level}{0}
+}
diff --git a/logic/logic_b.m4.in b/logic/logic_b.m4.in
new file mode 100644
index 0000000..8cc7b75
--- /dev/null
+++ b/logic/logic_b.m4.in
@@ -0,0 +1,9 @@
+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.
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