\documentclass[12pt]{article}
\usepackage{a4wide}
\usepackage{latexsym}
\usepackage{amsmath, amssymb}
\usepackage{epic}
\usepackage{graphicx}
\usepackage{gensymb}
\usepackage[table]{xcolor}
\usepackage{listings}
\usepackage{tikz}
\usetikzlibrary{automata,positioning}
\usepackage{hyperref}
\usepackage{float}
\usepackage{enumitem}
%\pagestyle{empty}
\newcommand{\tr}{\mbox{\sf true}}
\newcommand{\fa}{\mbox{\sf false}}
\newcommand{\bimp}{\leftrightarrow}     % bi-implication

\title{Assignment part 2 for Automated Reasoning 2IMF25}
\author{%
    Peter Wu (0783206)\\
    \texttt{s.p.wu@student.tue.nl}
\and
    Koen van der Heijden (0807929)\\
    \texttt{k.p.l.v.d.heijden@student.tue.nl}
}
\date{\today}

\begin{document}
\maketitle

\section*{Problem: food delivery}
Four non-self-supporting villages A, B, C and D in the middle of nowhere consume
one food package each per time unit. The required food packages are delivered by
a truck, having a capacity of 240 food packages. The truck has to pick up its
food packages at location S containing an unbounded supply. The locations of
this supply location and the villages and the roads between them are shown in
the following picture. Here every number indicates a distance, more precisely,
the number of time units the truck needs to travel from one village to another,
including loading and delivering. The villages only have a limited capacity to
store food packages: for A this capacity is 120, for B and D it is 160, and for
C it is 100. Initially, the truck is in S and is fully loaded, and in each of
the four villages there are 80 food packages.

\begin{figure*}
\centering
\begin{tikzpicture}[scale=.2]
\node[circle,draw] (A) at (0,0) {A};
\node[circle,draw] (B) at (17,0) {B};
\node[circle,draw] (C) at (9.794,-6.934) {C};
\node[circle,draw] (D) at (26.824,-17.421) {D};
\node[circle,draw] (S) at (-3.046,-14.687) {S};

\draw
    (A) edge node[above]        {17} (B)
    (A) edge node[above left]   {15} (S)
    (A) edge node[above right]  {12} (C)
    (S) edge node[below right]  {15} (C)
    (B) edge node[above left]   {10} (C)
    (B) edge node[above right]  {20} (D)
    (C) edge node[below left]   {20} (D)
    ;
\end{tikzpicture}
\end{figure*}

\begin{enumerate}
\item[(a)] Show that it is impossible to deliver food packages in such a way
that each of the villages consumes one food package per time unit forever.
\item[(b)] Show that this is possible if the capacity of the truck is increased
to 260 food packages. (Note that a finite graph contains an infinite path
starting in a node $v$ if and only if there is a path from $v$ to a node $w$ for
which there is a non-empty path from $w$ to itself.)
\end{enumerate}

\subsection*{Solution:}
\subsubsection*{(a)}
We generalize the problem as a graph $G=(V,E)$ where the vertices $V$ represent
villages and the supply location (denoted $S$) and edges $E$ represent the paths
between the vertices. We also define a weight function $cost : E \to
\mathbb{N}$. For brevity, we denote the villages (without the supply location)
by $V'=V \setminus \{S\}$.
The process of transporting and delivering food packages is modelled as state
transitions. The state after $0 \leq j \leq m$ steps consists of:
\begin{itemize}
\item Current location of truck: $l_j \in V$.
\item Remaining food stock at village $i \in V'$, denoted by $s_{i,j}$.
\item Remaining food stock in truck, denoted by $s_{T,j}$.
\end{itemize}

The truck (denoted as $T$) and villages have maximum capacities, let these be
defined by the function $capacity : (V' \cup \{T\}) \to \mathbb{N}$.
With these definitions in place, let us define the initial state for the
specific scenario where the truck starts at the supply location:
\begin{align}
\label{eq:food1}
l_0 = S
\land \bigwedge_{i \in V'} s_{i,0} = 80
\land s_{T,0} = capacity(T)
\end{align}

Now require that the truck capacity never drops below zero and that villages
always have some food to consume and are never overstocked:
\begin{align}
\label{eq:food2}
\bigwedge_{j=0}^m
0 \leq s_{T,j}
\land
\bigwedge_{i \in V' } 0 \leq s_{i,j} \leq capacity(i)
\end{align}

Finally we add the constraints for state transitions. At every state, any of
the enabled transitions can be taken (if this is not possible for any state,
then indeed it is impossible to deliver food packages in such a way without
starving some villages).
We add ingredients to express:
\begin{itemize}
\item Part~\ref{eq:food3}:
whether the target is reachable from the previous location.
\item Part~\ref{eq:food4}:
whether the village has sufficient food for consumption while the truck travels.
\item Part~\ref{eq:food5}:
villages (other than the target) eat some food (but are not restocked).
Note that this covers all villages if the next target is the supply location, so
the village stock $s_{i,j}$ is always defined.
\item Part~\ref{eq:food6}:
if target is village, eat some and optionally restock the village (as long as
the truck has some stock). For brevity, we define $drop(j) = s_{T,j-1} -
s_{T,j}$, expressing how much food is unloaded from the truck and dropped into
the village.
\item Part~\ref{eq:food7}:
if target is supply location, the truck is always fully restocked. (This and the
previous part ensures that $s_{T,j}$ is always defined.)
\end{itemize}
\begin{align}
\label{eq:food3}
\bigwedge_{j=1}^m
\bigvee_{(x, y) \in E}
&(l_{j-1}, l_j) = (x, y)
%
\\\label{eq:food4}
&\land
\bigwedge_{i \in V'} s_{i,j-1} \geq cost(x, y)
%
\\\label{eq:food5}
&\land
\bigwedge_{i \in V', i \neq y}
s_{i,j} = s_{i,j-1} - cost(x, y)
%
\\\label{eq:food6}
&\land
y \neq S \implies
    (s_{i,j} = s_{i,j-1} - cost(x, y) + drop(j)
    \land
    drop(j) \geq 0
    )
%
\\\label{eq:food7}
&\land
y = S \implies
s_{T,j} = capacity(T)
\end{align}

With the given path travelling costs $cost$, truck and villages $V$ and their
capacities $capacity$, we are able to build the route that the truck travels,
parameterized by the number of visited locations $m$.
We wrote a generator program in Python that outputs a SMT corresponding to
conjunction of the above ingredients (mapping $V=\{S,A,B,C,D\}$ to the indices
$0,1,2,3,4$), this is shown in Listing~\ref{lst:food}.

We picked (arbitrary) $m=30$ and applied Z3 to the generated SMT which resulted
in \texttt{unsat} after four seconds. Then we applied binary search and found
that for $m=22$ the output is still \texttt{unsat} (after four seconds)
while for $m=21$ a solution is found within a second. This shows that a valid
route with 21 visited locations can be obtained and that no route exists such
that 22 locations are visited. It is thus impossible to deliver food packages
in such a way that each of the villages can consume one food packge forever.

\begin{lstlisting}[
    caption={Generated SMT program for food delivery problem (a) with $m=30$.},
    label={lst:food},basicstyle=\scriptsize,language=lisp
]
(benchmark test.smt
:logic QF_UFLIA
:extrafuns (
(s0_0 Int) (s1_0 Int) ... (s4_0 Int) (l0 Int)
...
)
:formula (and
(= l0 0)
(= s1_0 80) (= s2_0 80) (= s3_0 80) (= s4_0 80) (= s0_0 240) (>= s0_0 0)
(>= s1_0 0) (<= s1_0 120) (>= s2_0 0) (<= s2_0 160)
(>= s3_0 0) (<= s3_0 100) (>= s4_0 0) (<= s4_0 160)
...
(or (and (= l0 0) (= l1 1)
         (>= s1_0 15) (>= s2_0 15) (>= s3_0 15) (>= s4_0 15)
         (>= (- s0_0 s0_1) 0)
         (= s1_1 (+ (- s1_0 15) (- s0_0 s0_1)))
         (= s2_1 (- s2_0 15))
         (= s3_1 (- s3_0 15))
         (= s4_1 (- s4_0 15)))
    ...
    (and (= l0 1) (= l1 0)
         (>= s1_0 15) (>= s2_0 15) (>= s3_0 15) (>= s4_0 15)
         (= s1_1 (- s1_0 15))
         (= s2_1 (- s2_0 15))
         (= s3_1 (- s3_0 15))
         (= s4_1 (- s4_0 15))
         (= s0_1 240))
    ...
) ...))
\end{lstlisting}

\subsubsection*{(b)}
In the solution to (a) we showed that an infinite series with the previous
requirements is already impossible. When the maximum truck capacity is increased
from $capacity(T)=240$ to $capacity(T)=260$, we shall add another ingredient
to check that villages can indeed consume food forever.

We do so by trying to find a state $k_1 \leq m$ where the stock of the truck and
the stock of each village is at least as high as a previous state $0 \leq k_0$
at the same location:
\begin{align}
\label{eq:food8}
\bigvee_{0 \leq k_0 < k_1 \leq m}
k_0 < k_1 \land l_{k_0} = l_{k_1} \land
s_{T,k_0} \leq s_{T,k_1}
\land
\bigwedge_{i \in V'} s_{i,k_0} \leq s_{i,k_1}
\end{align}

The SMT output generated by the augmented program includes two new variables and
adds Part~\ref{eq:food8} to the conjunction as shown in Listing~\ref{lst:foodB}.
For $m=12$ we obtained \texttt{unsat} after 9 seconds (showing that a loop was
not yet obtained) while for $m=13$ a satisfying assignment was found in 10
seconds. The resulting assignment is shown in Table~\ref{tbl:foodB}. Indeed, now
it is possible to deliver food in a way such that every village can consume food
forever.

\begin{lstlisting}[
    caption={Generated SMT program for food delivery problem (b) with $m=13$.},
    label={lst:foodB},basicstyle=\scriptsize,language=lisp
]
(benchmark test.smt
:logic QF_UFLIA
:extrafuns ( ... (k0 Int) (k1 Int))
:formula (and ...
(or (and (= k0 1) (= k1 2) (= l1 l2) (<= s0_1 s0_2) ... (<= s4_1 s4_2))
    (and (= k0 1) (= k1 3) (= l1 l3) (<= s0_1 s0_3) ... (<= s4_1 s4_3))
    ...
    (and (= k0 12) (= k1 13) (= l12 l13) (<= s0_12 s0_13) ... (<= s4_12 s4_13)))
))
\end{lstlisting}

\begin{table}[H]
\centering
\footnotesize
\begin{tabular}{r|r|rrrr|c}
    & \multicolumn{4}{c}{Stock at location} & \\
 $j$&     T &     A &     B &    C &      D & $l_j$ \\
\hline
  0 &   260 &    80 &    80 &    80 &    80 & S \\
  1 &   222 &\bf103 &    65 &    65 &    65 & A \\
  2 &   181 &    86 &\bf 89 &    48 &    48 & B \\
\rowcolor{lightgray}
  3 &    52 &    66 &    69 &    28 &\bf157 & D \\ % PAIR
  4 &     3 &    46 &    49 &\bf 57 &   137 & C \\
  5 &   260 &    31 &    34 &    42 &   122 & S \\
  6 &   219 &\bf 57 &    19 &    27 &   107 & A \\
  7 &    62 &    40 &\bf159 &    10 &    90 & B \\
  8 &     1 &    30 &   149 &\bf 61 &    80 & C \\
  9 &   260 &    15 &   134 &    46 &    65 & S \\
 10 &   144 &\bf116 &   119 &    31 &    50 & A \\
 11 &   260 &   101 &   104 &    16 &    35 & S \\
 12 &   213 &    86 &    89 &\bf 48 &    20 & C \\
\rowcolor{lightgray}
 13 &    56 &    66 &    69 &    28 &\bf157 & D \\ % PAIR
\end{tabular}
\caption{\label{tbl:foodB}The solution calculated by z3 for $m=13$, showing the
initial and following states (consisting of truck and village stock and current
location $l_j$) after $j$ transitions. State $j=13$ has greater or equal stocks
than state $j=13$ at location D.}
\end{table}

\section*{Problem: Nondeterministic finite automaton (NFA)}
Let an NFA be defined as in Wikipedia \\
\url{https://en.wikipedia.org/wiki/Nondeterministic_finite_automaton}\\
Find an NFA $M$ over $\sum = \{a, b\}$ with the least possible number of states
for which the only non-empty words in $L(M)$ of length $<$ 5 are $aa$, $bb$,
$aba$, $baa$, $abab$, $babb$ and $bbba$.

\subsection*{Solution:}

\begin{figure}[H]
\centering
\begin{tikzpicture}[>=latex,line join=bevel,scale=.8]
%%
\node (q1) at (349.84bp,107.75bp) [draw,circle] {q1};
  \node (q0) at (63.348bp,142.75bp) [draw,circle] {q0};
  \node (q3) at (250.34bp,26.748bp) [draw,circle, double] {q3};
  \node (q2) at (349.84bp,192.75bp) [draw,circle, double] {q2};
  \node (q5) at (449.33bp,192.75bp) [draw,circle, double] {q5};
  \node (q4) at (154.84bp,196.75bp) [draw,circle] {q4};
  \node (q7) at (250.34bp,196.75bp) [draw,circle] {q7};
  \node (q6) at (154.84bp,111.75bp) [draw,circle] {q6};
  \node (qi) at (1.8bp,142.75bp) [draw,circle, fill] {};
  \draw [->] (q4) ..controls (187.8bp,216.1bp) and (206.11bp,224.89bp)  .. (223.59bp,228.75bp) .. controls (289.99bp,243.41bp) and (310.37bp,244.23bp)  .. (376.58bp,228.75bp) .. controls (390.8bp,225.42bp) and (405.42bp,218.89bp)  .. (q5);
  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
  \pgfsetstrokecolor{strokecol}
  \draw (300.09bp,247.25bp) node {a};
  \draw [->] (q6) ..controls (183.11bp,118.1bp) and (189.56bp,119.16bp)  .. (195.59bp,119.75bp) .. controls (220.94bp,122.21bp) and (121.7bp,141.89bp)  .. (305.09bp,118.75bp) .. controls (309.28bp,118.22bp) and (313.66bp,117.44bp)  .. (q1);
  \draw (250.34bp,136.25bp) node {a};
  \draw [->] (q3) ..controls (283.88bp,45.478bp) and (295.45bp,52.911bp)  .. (305.09bp,60.748bp) .. controls (313.05bp,67.222bp) and (321.01bp,75.037bp)  .. (q1);
  \draw (300.09bp,68.248bp) node {b};
  \draw [->] (q4) ..controls (189.69bp,196.75bp) and (204.15bp,196.75bp)  .. (q7);
  \draw (200.59bp,204.25bp) node {b};
  \draw [->] (q0) ..controls (96.456bp,131.53bp) and (110.68bp,126.71bp)  .. (q6);
  \draw (109.1bp,136.25bp) node {b};
  \draw [->] (q1) ..controls (301.72bp,103.92bp) and (259.71bp,101.65bp)  .. (223.59bp,103.75bp) .. controls (211.74bp,104.44bp) and (198.81bp,105.78bp)  .. (q6);
  \draw (250.34bp,111.25bp) node {b};
  \draw [->] (q7) ..controls (285.1bp,195.35bp) and (299.58bp,194.77bp)  .. (q2);
  \draw (300.09bp,203.25bp) node {a};
  \draw [->] (q0) ..controls (95.791bp,161.9bp) and (112.28bp,171.63bp)  .. (q4);
  \draw (109.1bp,179.25bp) node {a};
  \draw [->] (q1) ..controls (382.04bp,135.26bp) and (403.75bp,153.81bp)  .. (q5);
  \draw (399.58bp,161.25bp) node {a};
  \draw [->] (qi) ..controls (8.2235bp,142.75bp) and (19.002bp,142.75bp)  .. (q0);
  \draw [->] (q2) ..controls (387.71bp,192.75bp) and (400.54bp,192.75bp)  .. (q5);
  \draw (399.58bp,200.25bp) node {b};
  \draw [->] (q6) ..controls (175.2bp,82.337bp) and (185.08bp,70.08bp)  .. (195.59bp,60.748bp) .. controls (202.27bp,54.82bp) and (210.1bp,49.285bp)  .. (q3);
  \draw (200.59bp,68.248bp) node {b};
%
\end{tikzpicture}
\end{figure}


\section*{Problem: }
The goal of this problem is to exploit the power of the recommended tools rather
than elaborating the questions by hand.
\begin{enumerate}
\item[(a)] For a binary operator a we have the idempotence, commutativity and
associativity rule, that is, the three rewrite rules
\[
a(x, x) \to x, a(x, y) \to a(y, x), a(x, a(y, z)) \to a(a(x, y), z).
\]
Figure out whether $a(p, a(q, a(p, a(q, a(p, a(q, p))))))$ rewrites to $a(p, q)$
in a finite number of steps, for constants $p$, $q$.
\item[(b)] In mathematics, a group is defined to be a set $G$ with an element
$I \in G$, a binary operator $*$ and a unary operator $inv$ satisfying
\[
    x * (y * z) = (x * y) * z,\ x * I = x \text{ and } x * inv(x) = I,
\]
for all $x, y, z \in G$. Determine whether in every group each of the four properties
\[
    I * x = x,\ inv(inv(x)) = x,\ inv(x) * x = I \text{ and } x * y = y * x
\]
holds for all $x, y \in G$. If a property does not hold, determine the size of
the smallest finite group for which it does not hold.
\end{enumerate}

\subsection*{Solution:}
\subsubsection*{(a)}
We want to prove that
\begin{enumerate}
  \item \label{itm:logic_a_1} $\forall p \forall q : a(p, a(q, a(p, a(q, a(p, a(q, p)))))) = a(p, q)$
\end{enumerate}
Using the assumptions
\begin{enumerate}[resume]
  \item \label{itm:logic_a_2} $a(x, x) = x$
  \item \label{itm:logic_a_3} $a(x, y) = a(y, x)$
  \item \label{itm:logic_a_4} $a(x, a(y, z)) = a(a(x, y), z)$
\end{enumerate}
We do this by finding a counterexample
\begin{enumerate}[resume]
  \item \label{itm:logic_a_5} $\exists c1, c2 : a(c1, a(c2, a(c1, a(c2, a(c1, a(c2, c1)))))) \neq a(c1, c2)$
\end{enumerate}
First, apply \ref{itm:logic_a_3} to \ref{itm:logic_a_5}
\begin{enumerate}[resume]
  \item \label{itm:logic_a_6} $\exists c1, c2 : a(c1, a(c2, a(c1, a(c2, a(c1, a(c1, c2)))))) \neq a(c1, c2)$
\end{enumerate}
Then, apply \ref{itm:logic_a_2} to \ref{itm:logic_a_4}, where $x \gets x, y \gets x, z \gets y$
\begin{enumerate}[resume]
  \item \label{itm:logic_a_7} $a(x, a(x, y)) = a(x, y)$
\end{enumerate}
On \ref{itm:logic_a_7}, we can then apply \ref{itm:logic_a_3} twice
\begin{enumerate}[resume]
  \item \label{itm:logic_a_8} $a(x, a(y, x)) = a(y, x)$
\end{enumerate}
Finally, we can recursively apply \ref{itm:logic_a_3}, \ref{itm:logic_a_7} and \ref{itm:logic_a_8} to \ref{itm:logic_a_6}, where $c1 \gets x$ and $c2 \gets y$
\begin{enumerate}[resume]
  \item \label{itm:logic_a_9} $a(x, a(y, a(x, a(y, a(x, a(y, x)))))) \neq a(x, a(y, a(x, a(y, a(x, a(y, x))))))$
\end{enumerate}
which evaluates to $FALSE$.\\
Therefore, we found that no counterexample exists, which proves that $a(p, a(q, a(p, a(q, a(p, a(q, p))))))$ indeed rewrites to $a(p, q)$.
\\
We derived this proof with \textit{prover9}, using the following input:
\begin{lstlisting}
formulas(sos).
	a(x,x)=x.
	a(x,y)=a(y,x).
	a(x,a(y,z))=a(a(x,y),z).
end_of_list.

formulas(goals).
	all p all q (a(p,a(q,a(p,a(q,a(p,a(q,p))))))=a(p,q)).
end_of_list.
\end{lstlisting}

\subsubsection*{(b)}
We want to prove 4 things:
\begin{enumerate}
  \item \label{itm:logic_b_1} $\forall x : I * x = x$
  \item \label{itm:logic_b_2} $\forall x : inv(inv(x)) = x$
  \item \label{itm:logic_b_3} $\forall x : inv(x) * x = I$
  \item \label{itm:logic_b_4} $\forall x \forall y : x * y = y * x$
\end{enumerate}
Using the assumptions
\begin{enumerate}[resume]
 \item \label{itm:logic_b_5} $x * (y * z) = (x * y) * z$
 \item \label{itm:logic_b_6} $x * I = x$
 \item \label{itm:logic_b_7} $x * inv(x) = I$
\end{enumerate}

To prove \ref{itm:logic_b_1}, \ref{itm:logic_b_2}, \ref{itm:logic_b_3} and \ref{itm:logic_b_4}, we created the following input:
\begin{lstlisting}
formulas(sos).
	(x*(y*z)=(x*y)*z).
	(x*I=x).
	(x*inv(x)=I).
end_of_list.

formulas(goals).
	all x (I*x=x).
	all x (inv(inv(x))=x).
	all x (inv(x)*x=I).
	all x all y (x*y=y*x).
end_of_list.
\end{lstlisting}

Running this input through \textit{prover9} generated the following proofs for \ref{itm:logic_b_1}, \ref{itm:logic_b_2} and \ref{itm:logic_b_3} respectively:
\begin{lstlisting}[caption=Proof for \ref{itm:logic_b_1}]
1 (all x I * x = x) # label(non_clause) # label(goal).  [goal].
5 x * (y * z) = (x * y) * z.  [assumption].
6 (x * y) * z = x * (y * z).  [copy(5),flip(a)].
7 x * I = x.  [assumption].
8 x * inv(x) = I.  [assumption].
9 I * c1 != c1.  [deny(1)].
13 x * (I * y) = x * y.  [para(7(a,1),6(a,1,1)),flip(a)].
14 x * (inv(x) * y) = I * y.  [para(8(a,1),6(a,1,1)),flip(a)].
19 I * inv(inv(x)) = x.  [para(8(a,1),14(a,1,2)),rewrite([7(2)]),flip(a)].
21 x * inv(inv(y)) = x * y.  [para(19(a,1),6(a,2,2)),rewrite([7(2)])].
22 I * x = x.  [para(19(a,1),13(a,2)),rewrite([21(5),13(4)])].
23 $F.  [resolve(22,a,9,a)].
\end{lstlisting}

\begin{lstlisting}[caption=Proof for \ref{itm:logic_b_2}]
2 (all x inv(inv(x)) = x) # label(non_clause) # label(goal).  [goal].
5 x * (y * z) = (x * y) * z.  [assumption].
6 (x * y) * z = x * (y * z).  [copy(5),flip(a)].
7 x * I = x.  [assumption].
8 x * inv(x) = I.  [assumption].
10 inv(inv(c2)) != c2.  [deny(2)].
13 x * (I * y) = x * y.  [para(7(a,1),6(a,1,1)),flip(a)].
14 x * (inv(x) * y) = I * y.  [para(8(a,1),6(a,1,1)),flip(a)].
19 I * inv(inv(x)) = x.  [para(8(a,1),14(a,1,2)),rewrite([7(2)]),flip(a)].
21 x * inv(inv(y)) = x * y.  [para(19(a,1),6(a,2,2)),rewrite([7(2)])].
22 I * x = x.  [para(19(a,1),13(a,2)),rewrite([21(5),13(4)])].
26 x * (inv(x) * y) = y.  [back_rewrite(14),rewrite([22(5)])].
30 inv(inv(x)) = x.  [para(8(a,1),26(a,1,2)),rewrite([7(2)]),flip(a)].
31 $F.  [resolve(30,a,10,a)].
\end{lstlisting}

\begin{lstlisting}[caption=Proof for \ref{itm:logic_b_3}]
3 (all x inv(x) * x = I) # label(non_clause) # label(goal).  [goal].
5 x * (y * z) = (x * y) * z.  [assumption].
6 (x * y) * z = x * (y * z).  [copy(5),flip(a)].
7 x * I = x.  [assumption].
8 x * inv(x) = I.  [assumption].
11 inv(c3) * c3 != I.  [deny(3)].
13 x * (I * y) = x * y.  [para(7(a,1),6(a,1,1)),flip(a)].
14 x * (inv(x) * y) = I * y.  [para(8(a,1),6(a,1,1)),flip(a)].
19 I * inv(inv(x)) = x.  [para(8(a,1),14(a,1,2)),rewrite([7(2)]),flip(a)].
21 x * inv(inv(y)) = x * y.  [para(19(a,1),6(a,2,2)),rewrite([7(2)])].
22 I * x = x.  [para(19(a,1),13(a,2)),rewrite([21(5),13(4)])].
26 x * (inv(x) * y) = y.  [back_rewrite(14),rewrite([22(5)])].
30 inv(inv(x)) = x.  [para(8(a,1),26(a,1,2)),rewrite([7(2)]),flip(a)].
34 inv(x) * x = I.  [para(30(a,1),8(a,1,2))].
35 $F.  [resolve(34,a,11,a)].
\end{lstlisting}

\textit{prover9} was not able to prover that $x * y = y * x$ holds for all finite groups. Therefor, we ran \ref{itm:logic_b_4} through \textit{mace4} to find the smallest group $G(I, *, inv)$ for which $x * y \neq y * x$.
The following input was used:
\begin{lstlisting}
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{lstlisting}
After running this input through \textit{mace4}, we retrieved the following finite group $G(I, *, inv)$:
\begin{verbatim}
 I: 0
 
 *:    | 0 1 2 3 4 5
     --*-------------
     0 | 0 1 2 3 4 5 
     1 | 1 0 3 2 5 4
     2 | 2 4 0 5 1 3
     3 | 3 5 1 4 0 2
     4 | 4 2 5 0 3 1
     5 | 5 3 4 1 2 0
 
 inv: 0 -> 0 
      1 -> 1
      2 -> 2
      3 -> 3
      4 -> 4
      5 -> 5
\end{verbatim}
We specify the row number in the $*$-operator table to be the left element, and the column number to be the right element.
Let $x \gets 2$ and $y \gets 1$. Then, we know that $x * y = 2 * 1 = 4$. Also, $y * x = 1 * 2 = 3$. Since $4 \neq 3$, we know that $x * y \neq y * x$, which proves that the property $x * y = y * x$ indeed does not hold for this group.

\section*{Problem: }
Give a precise description of a non-trivial problem of your own choice, and
encode this and solve it by one of the given programs.
Here `trivial problems' include both minor modifications of earlier problems and
single solutions of simply specified puzzles like sudokus. In case of doubt
please contact the lecturer.

\subsection*{Solution:}
We decided to choose a highscool room scheduling problem.

\begin{itemize}
 \item The highschool has $n$ classes
 \item The highschool only has $ceil(n * 0.7)$ rooms though
 \item Every class has to attend at least 1040 hours a year, which is equivalent to 26 hours per week
 \item Every day contains 8 timeslots of 1 hour, in which lectures can take place
 \item Lectures take place 5 days a week, giving a total of 40 timeslots per week
 \item There are 10 different courses:\\\\
 \begin{tabular}{l c r}
  English	  &	3 hours per week & \\
  German	  &	2 hours per week & \\
  Spanish	  &	2 hours per week & \\ 
  Math	  	  &	3 hours per week & \\
  Physics	  &	3 hours per week & \\
  Chemistry 	  &	3 hours per week & \\ 
  Biology	  &	3 hours per week & \\ 
  Art	  	  &	1 hour per week	 & \\ 
  Geography 	  &	3 hours per week & \\
  History	  &	3 hours per week & \\
 \end{tabular}
\end{itemize}

We want to schedule the rooms in such way that every class attends all required lessons per week, and the total amount of free hours inbetween 2 lectures is minimized.

\subsubsection*{Solution:}


\end{document}