$a_i, b_i, c_i, t_i, l_i, d_i$ respectively for the capacity of city $A$,
city $B$, city $C$, the truck, the trucks location and a help variable to
record how much food is dumped in the city. The distance between two cities is
-described with the function $dist(x, y)$. For all cities except $S$ a variable
-is defined that states the maximum capacity.
-$$a_{\max}=120\wedge b_{\max}=120\wedge c_{\max}=200$$
+described with the function $dist(x, y)$. For all cities except $S$ and the
+truck a variable is defined that states the maximum capacity. We express all
+the constant values in the formula called $const$.
+$$a_{\max}=120\wedge b_{\max}=120\wedge c_{\max}=200\wedge t_{\max}=300$$
+
Iteration $0$ depicts the initial state and can be described with a simple
-conjuction:
+conjunction called $initial$.
$$a_0=40\wedge b_0=30\wedge c_0=145\wedge t_0=300\wedge l_0=S\wedge d_0=0$$
-After that all iterations can be formalized as
-$$\begin{array}{lrl}
- \bigwedge_{i\in I} \Bigg(
- % Bent in S
- & \Bigg[ & l_i=S\wedge d_i=0\wedge t_i=300\wedge\\
- & & \bigvee_{k\in\{A,B\}}
- \bigg(l_{i-1}=k\wedge
- \bigwedge_{s\in\{A,B,C\}}
- s_i=s_{i-1}-dist(S, k)\bigg)\Bigg]\vee\\
- % Bent in A,B,C
- & \bigvee_{k\in\{a,b,c\}}\Bigg[ & l_i=k\wedge\\
- & & d_i>0\wedge d_i<t_{i-1}\wedge d_i<k_{\max}-k_{i-1}\wedge\\
- & & t_i=t_{i-1}-d_i\wedge k_i=k_{i-1}+d_i\wedge\\
- & & \bigwedge_{k'\in\{k\}\setminus\{S,A,B,C\}}
- \bigg(l_{i-1}=k'\wedge
- \bigwedge_{s\in\{k\}\setminus\{A,B,C\}}
- s_i=s_{i-1}-dist(k, k')\bigg)\Bigg]\\
- & \Bigg)
-\end{array}$$
+In every iteration there are certain constraints that always have to hold. We
+call them $constraints$ and they are expressed as:
+$$d_i>0\wedge
+d_i\leq t_{\max}\wedge
+t_i\geq\wedge
+t_i\leq t_{\max}\wedge
+\bigwedge_{k\in\{A,B,C\}}k_i>0$$
-\begin{enumerate}
- \item This part of the formula describes what happens if the truck is in
- $S$. This is a special case of the generalized case dsecribed in $2$
- and $3$. The truck always gets a refill in $S$ and no food is dumped.
- The truck could either have come from $A$ or $B$ and thus the food
- stocks of $A,B$ and $C$ will drop accordingly.
- \item
-\end{enumerate}
+We reason about the new iteration $i$ from the things we know about iteration
+$i-1$. The crucial part is the location we were in iteration $i-1$ and we make
+a disjunction over all possible cities and describe the result in the following
+formula called $trans$. We introduce a function $conn(s)$ that returns the set
+of all cities connected to city $s$. $(2)$ deals with the fact that the truck
+can not dump any food in city $S$ and constraints the amount of food dumped in
+the city. $(3)$ deals with the fact that the dumped food is added to the
+current stock of the city. Subformula $(4)$ deals with the fact that if the
+truck is in $S$ it is replenished and otherwise the dumped load is subtracted
+from the trucks load. Finally $(5)$ deals with the other cities which will have
+their stock decremented with the distance traveled.
+
+\begin{align}
+ \bigvee_{k\in\{S\}\cup V}
+ l_{i-1}=k\wedge
+ \bigvee_{k'\in conn(k)} & l_i=k'\wedge\\
+ & (k'=S\wedge d_i=0)\vee(d_i\leq dist(k,k')+k'_{\max}-k'_{i-1}\wedge\\
+ & (k'\neq S\rightarrow k_i=k_i-dist(k,k')+d_i))\wedge\\
+ & (k'=S\wedge t_i=t_{\max})\vee t_i=t_{i-1}-d_i\wedge\\
+ & \bigwedge_{k''\in V\setminus\{k\}}
+ k''_i=k''_{i-1}-dist(k,k')
+\end{align}
+
+We tie all this together in one big formula that is as follows:
+$$const\wedge initial\wedge
+\bigwedge_{i\in I}\left(constraints\wedge trans\right)$$
\begin{enumerate}[a.]
\item \emph{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 \emph{Show that this is possible if the capacity of the truck is
increased to 320 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.)}
+ To show this we need to prove that there is a state in the statespace
+ that is exactly the same as some previous state. To do this we add the
+ following formula to the conjunction.
+ $$\bigvee_{i\in I}\bigvee_{j\in \{0\ldots i-1\}}\left(
+ t_i=t_j\wedge l_i=l_j\wedge\bigwedge_{k\in V}k_i=k_j\right)
+ $$
+
+ When we incrementally increase the number of iterations we see that
+ when we have more then $8$ iterations we encounter a cycle. This is
+ shown in the following table where iteration $2$ and iteration $9$ are
+ equal.
+ \begin{table}[H]
+ \centering
+ \begin{tabular}{ccccccc}
+ \toprule
+ $I$ & $A$ & $B$ & $C$ & Truck & Location & Dump\\
+ \midrule
+ $0$ & $40$ & $30$ & $145$ & $320$ & $0$ & $0$\\
+ $1$ & $19$ & $22$ & $124$ & $307$ & $2$ & $9$\\
+ $2$ & $96$ & $5$ & $107$ & $213$ & $1$ & $98$\\
+ $3$ & $79$ & $119$ & $90$ & $82$ & $2$ & $133$\\
+ $4$ & $58$ & $98$ & $69$ & $320$ & $0$ & $0$\\
+ $5$ & $108$ & $69$ & $40$ & $241$ & $1$ & $79$\\
+ $6$ & $76$ & $37$ & $194$ & $55$ & $3$ & $186$\\
+ $7$ & $39$ & $55$ & $157$ & $0$ & $2$ & $53$\\
+ $8$ & $18$ & $34$ & $136$ & $320$ & $0$ & $0$\\
+ $9$ & $96$ & $5$ & $107$ & $213$ & $1$ & $107$\\
+ \bottomrule
+ \end{tabular}
+ \end{table}
\item \emph{Figure out whether it is possible if the capacity of the truck
is set to $318$.}
\end{enumerate}
\section{Solving solitaire}
\subsection{Problem description}
-Standard \emph{Peg solitaire} is a game played with marbles or pegs on a board
-with $33$ holes as displayed in Figure~\ref{lst:pegs}. In the Figure dots
-represent a peg and o's represent a empty hole. The goal is to end up with the
-last peg in the middle hole and all other pegs removed from the board.
-To achieve this you have make moves that capture another peg. You can capture
-another peg by finding a peg bordering it in a certain direction and on the
-other side there needs to be an empty spot. The four possible moves are
-displayed in Figure~\ref{lst:moves}.
-
-Since there is no such thing as an empty move we know the game is always
-finished in $31$ steps. This is because in the start position there are $32$
-pegs on the playing field, every move we remove one peg, thus requiring $31$
-moves to end up with only one peg.
+Standard \emph{English Peg solitaire} is a single player game played on a board
+with $33$ holes and is played with $32$ pegs. In the initial position all holes
+are occupied except for the middle hole. A traditional board is shown in
+Figure~\ref{fig:sol}. The goal of the game is to remove all but one peg on the
+middle position. The player can remove a peg by jumping over the peg
+orthogonally to a position two holes away. The middle peg is then removed from
+the board. To visualize board configurations we use the symbol $\circ$ for a
+position occupied by a peg and the symbol $\times$ by a position not occupied.
+The initial board configuration and possible moves are shown in
+Figure~\ref{fig:init}.
Variations on the game exists with different board shapes such as triangles,
rotated squares or bigger crosses. There is also an alternative that makes the
-end condition more flexible. Instead of requiring the last peg to be in the
-middle of the board, the last peg can be anywhere on the board.
-
-\begin{lstlisting}[caption={Standard English peg solitaire starting
-position},label={lst:pegs}]
- ...
- ...
-.......
-...o...
-.......
- ...
- ...
-\end{lstlisting}
+end condition more flexible by allowing the last peg anywhere on the board.
+\begin{figure}[H]
+ \centering
+ \includegraphics[width=.2\linewidth]{board.jpg}
+ \caption{Peg solitaire board}\label{fig:sol}
+\end{figure}
-\begin{lstlisting}[caption={Moves in all possible directions},
-label={lst:moves}]
-right left down up
- . . o .
-..o->oo. o..->.oo . -> o . -> o
- o o . o
-\end{lstlisting}
+\begin{figure}[H]
+ $$\xymatrix@1@=1pt@M=1pt{
+ & 0 & 1 & 2 & 3 & 4 & 5 & 6\\
+ 0 & & & \circ & \circ & \circ & & & & & &
+ \circ\ar@/^/[rr] & \circ & \times & \rightarrow &
+ \times & \times & \circ\\
+ 1 & & & \circ & \circ & \circ\\
+ 2 & \circ & \circ & \circ & \circ & \circ & \circ & \circ & & & &
+ \times & \circ & \circ\ar@/_/[ll]& \rightarrow &
+ \circ & \times & \times\\
+ 3 & \circ & \circ & \circ & \times & \circ & \circ & \circ\\
+ 4 & \circ & \circ & \circ & \circ & \circ & \circ & \circ & & & &
+ \circ\ar@/_/[dd] & & \times & & \times & & \circ\\
+ 5 & & & \circ & \circ & \circ & & & & & &
+ \circ & \rightarrow & \times & & \circ & \rightarrow& \times\\
+ 6 & & & \circ & \circ & \circ & & & & & &
+ \times & & \circ & & \circ\ar@/^/[uu] & & \times\\
+ }$$
+ \caption{Initial board state and possible moves}\label{fig:init}
+\end{figure}
\subsection{Formalization}
-Basically there are two possible formalization techniques we can use.
-Formalization per position and formalization per peg.
+Because in every move a peg is captured the game ends in exactly $31$ moves
+since there are $32$ pegs and one is left with a sole peg. A position $p$ means
+the $x$ and the $y$ coordinate as shown in Figure~\ref{fig:init}. Stating for a
+point $p$, $p_x$ or $p_y$ it means the respective $x$ and $y$ component of the
+position.\\
-Formalization per position means that we keep track of all the board positions
-and model what the position would be in the next state considering all possible
-moves. Every move there are only three positions on the board that are updated.
-On the entire board there are only $76$ possible combinations of three
-positions that can result in a move. This means that the formalization results
-in a big disjunction of the $76$ different moves.
+Set $\mathcal{P}$ is the set of all legal board positions and can be defined
+as:
+$$\mathcal{P}=\left\{p\in \{0\ldots7\}^2|\text{where }\neg(
+ (p_x<2\wedge p_y<2)\vee
+ (p_x>4\wedge p_y>4)\vee
+ (p_x>4\wedge p_y<2)\vee
+ (p_x<2\wedge p_y>4)\right\}$$
-The second method would be to formalize the game in means of the pegs. For
-every peg we keep track of the location and when the peg is removed we put them
-in the bin. In this way when we end up with only one peg with a valid winning
-location and the rest in the bin the game is over. Expected is that this method
-has a much higher branching factor. Moves always consist of two pegs. So for
-every move we have to check every combination of pegs and every direction. This
-means that when there are $32$ pegs in the game there are
-$32\cdot31\cdot4=3968$ possible moves we should check. Ofcourse we can prune a
-lot of combinations very quickly because one of the pegs might already in the
-bin or the position of the pegs was not correct but it is still a very large
-branching factor. Because of the high branching factor we first attempt to
-solve the problem using the position based approach.
+Set $\mathcal{M}$ is the set of position triples that form a legal move. $s$
+denotes the start position, $m$ denotes the middle position and $e$ the final
+position.
+$$\begin{array}{l}
+ \mathcal{M}=\{(s,m,e)\in \{0\ldots7\}^3|\text{where }\\
+ \qquad\qquad(s_x=m_x\wedge m_x=e_x\wedge
+ (m_y=s_y+1\wedge e_y=m_y+1\vee m_y=s_y-1\wedge e_y=m_y-1)\vee\\
+ \qquad\qquad(s_y=m_y\wedge m_y=e_y\wedge
+ (m_x=s_x+1\wedge e_x=m_x+1\vee m_x=s_x-1\wedge e_x=m_x-1)\\
+\end{array}$$
-\begin{lstlisting}[caption={Coordinate system},label={lst:coord}]
- 0123456
-0 ooo
-1 ooo
-2ooooooo
-3ooooooo
-4ooooooo
-5 ooo
-6 ooo
-\end{lstlisting}
+For every iteration $i\in\{0\ldots32\}$ and for every position $p\in \mathcal{P}$
+we create a variable representing the state of occupation. We also define
+$g=\langle3,3\rangle$ as being the middle position. With these definitions we
+can describe the initial state $\mathcal{INIT}$ as follows:
+$$\neg i_0x_{g_x}y_{g_y}\wedge\bigwedge_{p\in \mathcal{P}\setminus\{g\}}
+i_0x_{p_x}y_{p_y}$$
-To represent each position, as in Listing~\ref{lst:coord}, we assign per
-iteration $i$ for $i\in I$ where $I=\{0..32\}$ a variable $i_ix_xy_y$ per
-position where $(x,y)\in P$ where $P=\{(x,y) | (x,y)\text{ position on the
-board}\}$. So for example for the topmost row we have for $i=0$ the variables
-$\{i_0x_2y_0, i_0x_2y_1, i_0x_3y_0, i_0x_3y_1, i_0x_4y_0, i_0x_4y_1\}$.
+Every iteration with $i>0$ we define with a function called $\mathcal{ITER}(i)$
+which for every move describes the updates for the positions. Only the
+positions involved in the move are updated when the rest stay the same. Part
+$(1)$ of the formula describes the preconditions for a move to be valid. $(2)$
+describes the result of the move and $(3)$ expresses the invariability of the
+other positions.
+$$\begin{array}{llr}
+ \bigvee_{(s,m,e)\in M} \Biggl[&
+ i_{i-1}x_{s_x}y_{s_y}\wedge
+ i_{i-1}x_{m_x}y_{m_y}\wedge
+ \neg i_{i-1}x_{e_x}y_{e_y}\wedge & (1)\\
+ & \neg i_{i}x_{s_x}y_{s_y}\wedge
+ \neg i_{i}x_{m_x}y_{m_y}\wedge
+ i_{i}x_{e_x}y_{e_y}\wedge & (2)\\
+ & \bigwedge_{o\in \mathcal{P}\setminus\{s,m,e\}}
+ i_ix_{o_x}y_{o_y}=i_{i-1}x_{o_x}y_{o_y}\quad\Biggr] & (3)
+\end{array}
+$$
-To iterate over all moves we have to distinguish start and end positions from
-the middle position. All positions from $P$ are legal start or end positions
-but some are excluded from being a legal middle position of a move. Basically
-all positions in $P$ except for the corners are legal middle positions and
-therefore we define $P'$ that only contains legal middle positions and
-therefore $P'=P\setminus\{(2,0), (4,0), (0,2), (0,4), (6,2), (6,4), (2,6),
-(4,6)\}$
+The final state should be an inversion of the initial state. All holes should
+be empty except the middle hole $g$. $\mathcal{POST}$ is defined as follows:
+$$i_0x_{g_x}y_{g_y}\wedge\bigwedge_{p\in \mathcal{P}\setminus\{g\}}
+\neg i_0x_{p_x}y_{p_y}$$
-\begin{align}
- \neg i_0x_3y_3\wedge\bigwedge_{(x,y)\in
-P\setminus\{(3,3)\}}\left(i_0x_xy_y\right)\wedge\\
- \bigwedge^{I}_{i=1}
- \bigvee_{(sx, sy)\in P}\bigvee_{(mx, my)\in P'}
- \bigvee_{(ex, ey)\in P}\Bigl(
- & \bigl((sy=my\wedge my=ey\wedge sx=mx+1\wedge mx=ex+1)\vee\\
- & \quad(sy=my\wedge my=ey\wedge sx=mx-1\wedge mx=ex-1)\vee\\
- & \quad(sx=mx\wedge mx=ex\wedge sy=my+1\wedge my=ey+1)\vee\\
- & \quad(sx=mx\wedge mx=ex\wedge sy=my-1\wedge my=ey-1)\bigr)\wedge\\
- & i_{i-1}x_{sx}y_{sy}\wedge
- i_{i-1}x_{mx}y_{my}\wedge
- \neg i_{i-1}x_{ex}y_{ey}\wedge\\
- & \neg i_{i}x_{sx}y_{sy}\wedge
- \neg i_{i}x_{mx}y_{my}\wedge
- i_{i}x_{ex}y_{ey}\wedge\\
- & \bigwedge_{(ox,oy)\in P\setminus\{(ex,ey),(mx,my),(sx,sy)\}}\left(
- i_ix_{ox}y_{oy}=i_{i-1}x_{ox}y_{oy}\right)\Bigr)\wedge\\
- i_{31}x_3y_3\wedge\bigwedge_{(x,y)\in P\setminus\{(3,3)\}}\neg i_{31}x_xy_y
-\end{align}
+All of this together in the following formula is satisfiable if
+and only if there is a solution to English \textit{Peg solitaire}. The model
+that satisfies the formula is the sequence of moves to be performed to win a
+game.
+$$\mathcal{INIT}\wedge\left(\bigwedge_{i=1}^{31}\mathcal{ITER}(i)\right)
+\wedge\mathcal{POST}$$
-\lstinputlisting[caption={Solution for peg solitaire},label={lst:sol}]
- {./src/4/a4.tex}
+\subsection{Solution}
+The conversion to SMT-Lib is trivial
\maketitle
\tableofcontents
+\newpage
\input{1.tex}
+\newpage
\input{2.tex}
+\newpage
\input{3.tex}
+\newpage
\input{4.tex}
\end{document}
\usepackage{amsmath} % For nice tables
\usepackage{listings} % For nice tables
\usepackage{float} % For nice tables
+\usepackage{graphicx}
+\usepackage{xypic}
\everymath{\displaystyle}
--- /dev/null
+#!/bin/bash
+YICES=~/projects/yices-2.4.2/bin/yices-smt
+AI=40
+BI=30
+CI=145
+AMAX=120
+BMAX=120
+CMAX=200
+
+function generate {
+ ITERATIONS=$1
+ TMAX=$2
+ cat<<GEN
+(benchmark a1.smt
+:logic QF_UFLIA
+:extrafuns (
+$( for i in $(seq 0 $ITERATIONS); do
+ echo -e "\t(a$i Int) (b$i Int) (c$i Int) (t$i Int) (l$i Int) (d$i Int) (p$i Int)"
+ done)
+)
+:formula
+(and
+ ;-- PRECONDITION
+ (and (= a0 $AI) (= b0 $BI) (= c0 $CI) (= t0 $TMAX) (= l0 0) (= d0 0) (= p0 0))
+GEN
+ for i in $(seq 1 $ITERATIONS); do
+ cat<<GEN
+ (> a$i 0)
+ (> b$i 0)
+ (> c$i 0)
+ (or ;-- ITERATION $i
+ (and ;-- SPECIAL CASE FOR STATE S(0)
+ (= l$i 0)
+ (= d$i 0)
+ (= t$i $TMAX)
+ (= a$i (- a$((i-1)) p$i))
+ (= b$i (- b$((i-1)) p$i))
+ (= c$i (- c$((i-1)) p$i))
+ (or
+ (and ;-- CAME FROM A
+ (= l$((i-1)) 1)
+ (= p$i 29)
+ )
+ (and ;-- CAME FROM B
+ (= l$((i-1)) 2)
+ (= p$i 21)
+ )
+ )
+ )
+ (and ;-- CASE FOR STATE A(1)
+ (= l$i 1)
+ (>= d$i 0) (<= d$i t$((i-1)))
+ (<= d$i (+ p$i (- $AMAX a$((i-1)))))
+ (= t$i (- t$((i-1)) d$i))
+ (= a$i (- (+ a$((i-1)) d$i) p$i))
+
+ (= b$i (- b$((i-1)) p$i))
+ (= c$i (- c$((i-1)) p$i))
+ (or
+ (and ;-- CAME FROM S(0)
+ (= l$((i-1)) 0)
+ (= p$i 29)
+ ) (and ;-- CAME FROM B(2)
+ (= p$i 17)
+ (= l$((i-1)) 2)
+ ) (and ;-- CAME FROM C(3)
+ (= p$i 32)
+ (= l$((i-1)) 3)
+ )
+ )
+ )
+ (and ;-- CASE FOR STATE B(2)
+ (= l$i 3)
+ (>= d$i 0) (<= d$i t$((i-1)))
+ (<= d$i (+ p$i (- $BMAX b$((i-1)))))
+ (= t$i (- t$((i-1)) d$i))
+ (= b$i (- (+ b$((i-1)) d$i) p$i))
+
+ (= a$i (- a$((i-1)) p$i))
+ (= c$i (- c$((i-1)) p$i))
+
+ (or
+ (and ;-- CAME FROM S(0)
+ (= l$((i-1)) 0)
+ (= p$i 21)
+ ) (and ;-- CAME FROM A(1)
+ (= l$((i-1)) 1)
+ (= p$i 17)
+ ) (and ;-- CAME FROM C(3)
+ (= l$((i-1)) 3)
+ (= p$i 37)
+ )
+ )
+ )
+ (and ;-- CASE FOR STATE C(3)
+ (= l$i 3)
+ (>= d$i 0) (<= d$i t$((i-1)))
+ (<= d$i (+ p$i (- $CMAX c$((i-1)))))
+ (= t$i (- t$((i-1)) d$i))
+ (= c$i (- (+ c$((i-1)) d$i) p$i))
+ (= a$i (- a$((i-1)) p$i))
+ (= b$i (- b$((i-1)) p$i))
+ (or
+ (and ;-- CAME FROM A(1)
+ (= l$((i-1)) 1)
+ (= p$i 32)
+ ) (and ;-- CAME FROM B(2)
+ (= l$((i-1)) 2)
+ (= p$i 37)
+ )
+ )
+ )
+ )
+GEN
+ done
+ cat<<GEN
+))
+GEN
+}
+it=1
+until generate $it 300 | $YICES | grep "unsat"
+do
+ echo $((it++))
+done
+generate 9 300 | $YICES -m | sort
+echo $it
+++ /dev/null
-#!/bin/bash
-AI=40
-BI=30
-CI=145
-TI=300
-AMAX=120
-BMAX=120
-CMAX=200
-TMAX=300
-
-ITERATIONS=1
-
-function generate {
- cat<<GEN
-(benchmark a1.smt
-:logic QF_UFLIA
-:extrafuns (
-$( for i in $(seq 0 $ITERATIONS); do
- echo -e "\t(a$i Int) (b$i Int) (c$i Int) (t$i Int) (l$i Int) (d$i Int)"
- done)
-)
-:formula
-(and
- -- PRECONDITION
- (and (= a0 $AI) (= b0 $BI) (= c0 $CI) (= t0 $TI) (= l0 0) (= d0 0))
-GEN
- for i in $(seq 1 $ITERATIONS); do
- cat<<GEN
- -- SPECIAL CASE FOR STATE S(0)
- (= l$i 0) (= d$i 0) (= t$i $TMAX)
- (or
- (and -- Comes from A
- (= l$((i-1)) 1)
- (= a$i (- a$((i-1)) 29)
- (= b$i (- b$((i-1)) 29)
- (= c$i (- c$((i-1)) 29)
- )
- (and -- Comes from B
- (= l$((i-1)) 2)
- (= a$i (- a$((i-1)) 21)
- (= b$i (- b$((i-1)) 21)
- (= c$i (- c$((i-1)) 21)
- )
- )
-GEN
- done
- echo "))"
-}
-#time generate | yices-smt -m | python3 src/a2.py > $1
-generate
--- /dev/null
+#!/bin/bash
+YICES=~/projects/yices-2.4.2/bin/yices-smt
+AI=40
+BI=30
+CI=145
+AMAX=120
+BMAX=120
+CMAX=200
+
+function generate {
+ ITERATIONS=$1
+ TMAX=$2
+ cat<<GEN
+(benchmark a1.smt
+:logic QF_UFLIA
+:extrafuns (
+$( for i in $(seq 0 $ITERATIONS); do
+ echo -e "\t(a$i Int) (b$i Int) (c$i Int) (t$i Int) (l$i Int) (d$i Int)"
+ done)
+)
+:formula
+(and
+ ;-- PRECONDITION
+ (and (= a0 $AI) (= b0 $BI) (= c0 $CI) (= t0 $TMAX) (= l0 0) (= d0 0))
+GEN
+ for i in $(seq 1 $ITERATIONS); do
+ cat<<GEN
+ (> a$i 0)
+ (> b$i 0)
+ (> c$i 0)
+ (>= d$i 0)
+ (<= d$i $TMAX)
+ (>= t$i 0)
+ (<= t$i $TMAX)
+ (or ;-- ITERATION $i
+ (and ;-- WAS IN S
+ (= l$((i-1)) 0)
+ (or
+ (and ; now in A
+ (= l$i 1)
+ (<= d$i (+ 29 (- $AMAX a$((i-1)))))
+ (= a$i (+ (- a$((i-1)) 29) d$i))
+
+ (= b$i (- b$((i-1)) 29))
+ (= c$i (- c$((i-1)) 29))
+
+ (= t$i (- t$((i-1)) d$i))
+ ) (and ; now in B
+ (= l$i 2)
+ (<= d$i (+ 21 (- $BMAX b$((i-1)))))
+ (= b$i (+ (- b$((i-1)) 21) d$i))
+
+ (= a$i (- a$((i-1)) 21))
+ (= c$i (- c$((i-1)) 21))
+
+ (= t$i (- t$((i-1)) d$i))
+ )
+ )
+ )
+ (and ;-- WAS IN A
+ (= l$((i-1)) 1)
+ (or
+ (and ; now in S
+ (= l$i 0)
+ (= d$i 0)
+
+ (= a$i (- a$((i-1)) 29))
+ (= b$i (- b$((i-1)) 29))
+ (= c$i (- c$((i-1)) 29))
+
+ (= t$i $TMAX)
+ ) (and ; now in B
+ (= l$i 2)
+ (<= d$i (+ 17 (- $BMAX b$((i-1)))))
+ (= b$i (+ (- b$((i-1)) 17) d$i))
+
+ (= a$i (- a$((i-1)) 17))
+ (= c$i (- c$((i-1)) 17))
+
+ (= t$i (- t$((i-1)) d$i))
+ ) (and ; now in C
+ (= l$i 3)
+
+ (<= d$i (+ 32 (- $CMAX c$((i-1)))))
+ (= c$i (+ (- c$((i-1)) 32) d$i))
+
+ (= a$i (- a$((i-1)) 32))
+ (= b$i (- b$((i-1)) 32))
+
+ (= t$i (- t$((i-1)) d$i))
+ )
+ )
+ )
+ (and ;-- WAS IN B
+ (= l$((i-1)) 2)
+ (or
+ (and ; now in S
+ (= l$i 0)
+ (= d$i 0)
+
+ (= a$i (- a$((i-1)) 21))
+ (= b$i (- b$((i-1)) 21))
+ (= c$i (- c$((i-1)) 21))
+
+ (= t$i $TMAX)
+ ) (and ; now in A
+ (= l$i 1)
+ (<= d$i (+ 17 (- $AMAX a$((i-1)))))
+ (= a$i (+ (- a$((i-1)) 17) d$i))
+
+ (= b$i (- b$((i-1)) 17))
+ (= c$i (- c$((i-1)) 17))
+
+ (= t$i (- t$((i-1)) d$i))
+ ) (and ; now in C
+ (= l$i 3)
+ (<= d$i (+ 37 (- $CMAX c$((i-1)))))
+ (= c$i (+ (- c$((i-1)) 37) d$i))
+
+ (= a$i (- a$((i-1)) 37))
+ (= b$i (- b$((i-1)) 37))
+
+ (= t$i (- t$((i-1)) d$i))
+ )
+ )
+ )
+ (and ;-- WAS IN C
+ (= l$((i-1)) 3)
+ (or
+ (and ; now in A
+ (= l$i 1)
+ (<= d$i (+ 32 (- $AMAX a$((i-1)))))
+ (= a$i (+ (- a$((i-1)) 32) d$i))
+
+ (= b$i (- b$((i-1)) 32))
+ (= c$i (- c$((i-1)) 32))
+
+ (= t$i (- t$((i-1)) d$i))
+ ) (and ; now in B
+ (= l$i 2)
+ (<= d$i (+ 37 (- $BMAX b$((i-1)))))
+ (= b$i (+ (- b$((i-1)) 37) d$i))
+
+ (= a$i (- a$((i-1)) 37))
+ (= c$i (- c$((i-1)) 37))
+
+ (= t$i (- t$((i-1)) d$i))
+ )
+ )
+ )
+ )
+GEN
+ done
+ echo "(or"
+ for i in $(seq 0 $ITERATIONS); do
+ for j in $(seq $((i+1)) $ITERATIONS); do
+ echo "(and (= t$i t$j) (= l$i l$j) (= a$i a$j) (= b$i b$j) (= c$i c$j))"
+ done
+ done
+ echo ")))"
+}
+it=1
+while generate $it 318 | $YICES -m | pee sort "grep -q unsat"
+do
+ echo $((it++))
+done
--- /dev/null
+#!/bin/bash
+YICES=~/projects/yices-2.4.2/bin/yices-smt
+AI=40
+BI=30
+CI=145
+AMAX=120
+BMAX=120
+CMAX=200
+
+function generate {
+ ITERATIONS=$1
+ TMAX=$2
+ cat<<GEN
+(benchmark a1.smt
+:logic QF_UFLIA
+:extrafuns (
+$( for i in $(seq 0 $ITERATIONS); do
+ echo -e "\t(a$i Int) (b$i Int) (c$i Int) (t$i Int) (l$i Int) (d$i Int)"
+ done)
+)
+:formula
+(and
+ ;-- PRECONDITION
+ (and (= a0 $AI) (= b0 $BI) (= c0 $CI) (= t0 $TMAX) (= l0 0) (= d0 0))
+GEN
+ for i in $(seq 1 $ITERATIONS); do
+ cat<<GEN
+ (> a$i 0)
+ (> b$i 0)
+ (> c$i 0)
+ (or ;-- ITERATION $i
+ (and ;-- SPECIAL CASE FOR STATE S(0)
+ (= l$i 0)
+ (= d$i 0)
+ (= t$i $TMAX)
+ (or
+ (and ;-- CAME FROM A
+ (= l$((i-1)) 1)
+ (= a$i (- a$((i-1)) 29))
+ (= b$i (- b$((i-1)) 29))
+ (= c$i (- c$((i-1)) 29))
+ )
+ (and ;-- CAME FROM B
+ (= l$((i-1)) 2)
+ (= a$i (- a$((i-1)) 21))
+ (= b$i (- b$((i-1)) 21))
+ (= c$i (- c$((i-1)) 21))
+ )
+ )
+ )
+ (and ;-- CASE FOR STATE A(1)
+ (= l$i 1)
+ (>= d$i 0) (<= d$i t$((i-1))) (<= d$i (- $AMAX a$((i-1))))
+ (= t$i (- t$((i-1)) d$i)) (= a$i (+ a$((i-1)) d$i))
+
+ (or
+ (and ;-- CAME FROM S(0)
+ (= l$((i-1)) 0)
+ (= b$i (- b$((i-1)) 29))
+ (= c$i (- c$((i-1)) 29))
+ ) (and ;-- CAME FROM B(2)
+ (= l$((i-1)) 2)
+ (= b$i (- b$((i-1)) 17))
+ (= c$i (- c$((i-1)) 17))
+ ) (and ;-- CAME FROM C(3)
+ (= l$((i-1)) 3)
+ (= b$i (- b$((i-1)) 32))
+ (= c$i (- c$((i-1)) 32))
+ )
+ )
+ )
+ (and ;-- CASE FOR STATE B(2)
+ (= l$i 2)
+ (>= d$i 0) (<= d$i t$((i-1))) (<= d$i (- $BMAX b$((i-1))))
+ (= t$i (- t$((i-1)) d$i)) (= b$i (+ b$((i-1)) d$i))
+
+ (or
+ (and ;-- CAME FROM S(0)
+ (= l$((i-1)) 0)
+ (= a$i (- a$((i-1)) 21))
+ (= c$i (- c$((i-1)) 21))
+ ) (and ;-- CAME FROM A(1)
+ (= l$((i-1)) 1)
+ (= a$i (- a$((i-1)) 17))
+ (= c$i (- c$((i-1)) 17))
+ ) (and ;-- CAME FROM C(3)
+ (= l$((i-1)) 3)
+ (= a$i (- a$((i-1)) 37))
+ (= c$i (- c$((i-1)) 37))
+ )
+ )
+ )
+ (and ;-- CASE FOR STATE C(3)
+ (= l$i 3)
+ (>= d$i 0) (<= d$i t$((i-1))) (<= d$i (- $CMAX c$((i-1))))
+ (= t$i (- t$((i-1)) d$i)) (= c$i (+ c$((i-1)) d$i))
+
+ (or
+ (and ;-- CAME FROM A(1)
+ (= l$((i-1)) 1)
+ (= a$i (- a$((i-1)) 32))
+ (= b$i (- b$((i-1)) 32))
+ ) (and ;-- CAME FROM B(2)
+ (= l$((i-1)) 2)
+ (= a$i (- a$((i-1)) 37))
+ (= b$i (- b$((i-1)) 37))
+ )
+ )
+ )
+ )
+GEN
+ done
+ echo "(or"
+ for i in $(seq 0 $ITERATIONS); do
+ for j in $(seq $((i+1)) $ITERATIONS); do
+ echo "(and (= t$i t$j) (= l$i l$j) (= a$i a$j) (= b$i b$j) (= c$i c$j))"
+ done
+ done
+ echo ")))"
+}
+
+it=1
+while generate $it 320 | $YICES -m | pee sort "grep unsat"
+do
+ it=$((it+1))
+done
+echo $it
-sat
-
-(= i1x2y0 true)
-(= i4x2y1 false)
-(= i1x2y3 true)
-(= i11x2y5 false)
-(= i31x6y2 false)
-(= i26x0y3 true)
-(= i10x3y6 true)
-(= i13x3y5 true)
-(= i20x0y4 false)
-(= i30x2y2 false)
-(= i6x2y3 true)
-(= i6x5y3 true)
-(= i0x4y0 true)
-(= i17x2y0 false)
-(= i20x3y1 false)
-(= i24x5y4 false)
-(= i16x4y6 false)
-(= i26x0y4 false)
-(= i26x2y5 false)
-(= i14x2y6 false)
-(= i29x1y4 true)
-(= i1x0y4 true)
-(= i21x3y3 false)
-(= i31x4y2 false)
-(= i18x6y3 false)
-(= i3x1y2 true)
-(= i4x3y6 true)
-(= i9x1y3 true)
-(= i16x6y4 false)
-(= i18x6y4 false)
-(= i19x1y4 true)
-(= i14x3y0 false)
-(= i9x3y3 false)
-(= i3x5y4 true)
-(= i21x4y5 false)
-(= i14x4y5 false)
-(= i30x5y2 false)
-(= i22x4y6 false)
-(= i6x0y3 true)
-(= i18x2y5 false)
-(= i27x1y2 false)
-(= i26x2y1 false)
-(= i24x4y6 false)
-(= i31x4y4 false)
-(= i19x5y3 false)
-(= i15x1y4 false)
-(= i9x3y6 true)
-(= i0x3y1 true)
-(= i14x6y2 false)
-(= i28x0y3 false)
-(= i0x6y2 true)
-(= i9x5y3 true)
-(= i13x0y4 true)
-(= i11x1y3 true)
-(= i7x3y3 false)
-(= i21x2y4 false)
-(= i15x5y4 false)
-(= i27x4y2 false)
-(= i6x0y2 true)
-(= i14x3y4 false)
-(= i9x0y4 true)
-(= i20x6y4 false)
-(= i7x1y4 true)
-(= i21x1y2 true)
-(= i24x4y5 false)
-(= i30x4y5 false)
-(= i31x1y4 false)
-(= i8x4y1 false)
-(= i1x3y5 true)
-(= i3x2y6 true)
-(= i13x1y4 true)
-(= i2x6y2 true)
-(= i9x4y1 false)
-(= i29x0y2 false)
-(= i15x0y4 false)
-(= i28x5y2 false)
-(= i24x3y6 false)
-(= i18x3y1 false)
-(= i19x4y6 false)
-(= i22x3y1 false)
-(= i19x4y1 false)
-(= i13x2y0 false)
-(= i27x3y3 false)
-(= i12x3y5 true)
-(= i16x2y0 false)
-(= i10x4y0 false)
-(= i27x2y0 false)
-(= i11x3y4 true)
-(= i9x3y0 true)
-(= i2x3y6 true)
-(= i12x6y2 true)
-(= i18x2y6 true)
-(= i23x3y4 false)
-(= i13x0y2 true)
-(= i31x2y4 false)
-(= i13x3y6 true)
-(= i2x0y4 true)
-(= i8x4y6 true)
-(= i17x5y4 true)
-(= i18x3y2 true)
-(= i6x1y2 true)
-(= i16x1y3 true)
-(= i18x3y3 false)
-(= i27x0y4 false)
-(= i6x2y5 true)
-(= i24x3y0 false)
-(= i9x3y1 false)
-(= i11x5y4 true)
-(= i3x2y3 true)
-(= i15x0y2 true)
-(= i27x3y2 false)
-(= i12x6y3 true)
-(= i5x0y2 true)
-(= i29x0y3 false)
-(= i30x4y6 false)
-(= i13x3y3 false)
-(= i28x4y5 false)
-(= i31x4y3 false)
-(= i2x4y5 true)
-(= i8x6y4 false)
-(= i13x3y1 false)
-(= i10x4y1 false)
-(= i17x2y1 false)
-(= i26x3y2 false)
-(= i30x4y0 false)
-(= i19x6y3 false)
-(= i24x2y1 false)
-(= i12x1y4 true)
-(= i29x3y6 false)
-(= i23x0y3 true)
-(= i6x4y3 true)
-(= i15x3y5 true)
-(= i23x0y4 false)
-(= i29x6y2 false)
-(= i21x4y4 false)
-(= i14x4y3 true)
-(= i29x3y0 false)
-(= i24x6y3 false)
-(= i25x3y3 false)
-(= i5x2y2 true)
-(= i30x5y4 false)
-(= i16x0y4 false)
-(= i2x5y3 false)
-(= i3x1y3 true)
-(= i12x2y0 false)
-(= i16x2y5 false)
-(= i25x2y6 true)
-(= i7x0y3 true)
-(= i10x3y2 true)
-(= i12x3y1 false)
-(= i26x6y3 false)
-(= i27x6y3 false)
-(= i6x1y4 true)
-(= i20x3y3 false)
-(= i27x6y4 false)
-(= i29x2y6 false)
-(= i3x6y3 true)
-(= i24x6y2 false)
-(= i1x5y4 true)
-(= i27x5y4 false)
-(= i10x2y4 true)
-(= i30x3y6 false)
-(= i26x2y3 false)
-(= i14x2y3 true)
-(= i28x3y5 true)
-(= i5x0y4 true)
-(= i24x1y2 true)
-(= i2x1y3 true)
-(= i4x1y3 true)
-(= i7x3y0 true)
-(= i15x3y4 false)
-(= i25x2y5 false)
-(= i12x3y2 true)
-(= i22x6y4 false)
-(= i14x4y6 true)
-(= i14x2y1 false)
-(= i22x4y1 false)
-(= i24x0y4 false)
-(= i26x3y5 true)
-(= i4x1y4 true)
-(= i23x5y2 false)
-(= i30x2y6 false)
-(= i16x4y4 true)
-(= i25x2y2 true)
-(= i0x4y3 true)
-(= i6x4y5 false)
-(= i20x3y2 true)
-(= i30x6y3 false)
-(= i20x2y0 false)
-(= i29x3y5 true)
-(= i12x4y3 true)
-(= i22x2y5 false)
-(= i12x5y3 true)
-(= i28x3y3 false)
-(= i23x4y1 false)
-(= i24x5y3 false)
-(= i20x3y5 true)
-(= i8x2y0 true)
-(= i17x3y0 false)
-(= i9x6y4 false)
-(= i2x4y6 true)
-(= i29x0y4 false)
-(= i13x0y3 true)
-(= i8x2y2 true)
-(= i14x2y5 false)
-(= i17x2y3 true)
-(= i11x3y0 false)
-(= i24x4y1 false)
-(= i14x4y0 true)
-(= i27x4y4 false)
-(= i4x5y4 true)
-(= i23x3y3 false)
-(= i9x1y2 true)
-(= i3x6y2 true)
-(= i30x0y2 false)
-(= i3x2y1 false)
-(= i11x4y4 false)
-(= i6x2y2 true)
-(= i15x2y4 true)
-(= i23x4y4 false)
-(= i26x1y3 true)
-(= i4x0y3 true)
-(= i28x0y4 false)
-(= i29x6y3 false)
-(= i2x4y0 true)
-(= i0x3y0 true)
-(= i14x3y3 false)
-(= i30x4y1 false)
-(= i11x6y4 false)
-(= i0x3y6 true)
-(= i12x1y3 true)
-(= i8x1y3 true)
-(= i28x2y2 false)
-(= i4x2y5 true)
-(= i26x1y4 true)
-(= i6x4y6 true)
-(= i21x0y3 true)
-(= i21x4y3 false)
-(= i26x4y0 false)
-(= i24x3y3 false)
-(= i18x4y1 false)
-(= i21x3y0 false)
-(= i25x2y1 false)
-(= i26x3y6 false)
-(= i27x1y4 true)
-(= i27x4y5 false)
-(= i28x2y6 true)
-(= i27x3y6 false)
-(= i19x2y6 true)
-(= i1x2y1 true)
-(= i0x0y3 true)
-(= i25x4y6 false)
-(= i4x1y2 true)
-(= i0x2y0 true)
-(= i17x6y3 false)
-(= i11x5y2 true)
-(= i7x6y3 true)
-(= i12x3y3 false)
-(= i9x0y2 true)
-(= i21x2y2 false)
-(= i4x2y3 true)
-(= i16x3y1 false)
-(= i21x3y1 false)
-(= i24x4y2 false)
-(= i4x0y4 true)
-(= i7x3y5 true)
-(= i11x4y3 true)
-(= i9x2y3 true)
-(= i20x2y6 true)
-(= i18x4y5 false)
-(= i2x0y2 true)
-(= i13x4y0 true)
-(= i25x3y6 false)
-(= i27x3y5 true)
-(= i4x3y3 true)
-(= i31x4y5 false)
-(= i10x0y2 true)
-(= i20x2y5 false)
-(= i9x4y6 true)
-(= i1x3y1 true)
-(= i28x1y2 false)
-(= i28x6y2 false)
-(= i20x6y2 false)
-(= i5x2y5 true)
-(= i1x0y2 true)
-(= i1x4y5 true)
-(= i1x1y3 true)
-(= i6x0y4 true)
-(= i14x5y2 true)
-(= i9x6y2 true)
-(= i19x0y3 true)
-(= i21x3y2 true)
-(= i26x4y2 false)
-(= i24x1y3 true)
-(= i20x4y1 false)
-(= i5x3y6 true)
-(= i23x1y4 true)
-(= i1x6y2 true)
-(= i23x5y3 false)
-(= i12x2y1 false)
-(= i2x0y3 true)
-(= i18x4y6 false)
-(= i7x4y0 false)
-(= i1x1y2 true)
-(= i0x2y1 true)
-(= i1x5y3 false)
-(= i1x3y0 true)
-(= i8x4y0 false)
-(= i10x5y4 true)
-(= i4x0y2 true)
-(= i26x3y3 false)
-(= i0x4y6 true)
-(= i7x6y2 true)
-(= i17x1y3 true)
-(= i13x4y4 false)
-(= i3x4y1 true)
-(= i5x3y4 true)
-(= i21x3y5 true)
-(= i28x4y0 false)
-(= i22x3y5 true)
-(= i14x3y6 true)
-(= i2x3y5 true)
-(= i29x4y6 false)
-(= i12x2y2 true)
-(= i30x3y3 false)
-(= i17x5y2 false)
-(= i4x3y5 true)
-(= i11x3y3 false)
-(= i30x3y5 true)
-(= i14x5y4 true)
-(= i8x5y2 true)
-(= i25x4y0 false)
-(= i9x4y4 false)
-(= i4x3y0 true)
-(= i3x4y3 true)
-(= i11x2y6 false)
-(= i18x3y5 true)
-(= i12x4y0 true)
-(= i11x3y5 true)
-(= i28x4y3 false)
-(= i14x3y2 true)
-(= i16x5y3 true)
-(= i6x5y4 true)
-(= i2x3y4 true)
-(= i19x5y4 false)
-(= i1x6y4 true)
-(= i15x5y2 true)
-(= i1x3y4 true)
-(= i3x2y5 true)
-(= i20x5y4 false)
-(= i23x0y2 true)
-(= i23x2y5 false)
-(= i3x4y6 true)
-(= i6x4y4 false)
-(= i7x2y1 false)
-(= i26x4y5 false)
-(= i25x4y1 false)
-(= i10x2y2 true)
-(= i23x2y1 true)
-(= i9x6y3 true)
-(= i8x3y1 false)
-(= i13x1y3 true)
-(= i14x2y0 false)
-(= i7x4y5 false)
-(= i15x1y2 true)
-(= i21x2y1 true)
-(= i1x2y6 true)
-(= i17x2y6 true)
-(= i12x1y2 true)
-(= i22x1y2 true)
-(= i12x5y4 true)
-(= i1x6y3 true)
-(= i25x2y4 false)
-(= i25x4y5 false)
-(= i7x3y4 true)
-(= i10x3y1 false)
-(= i25x4y2 false)
-(= i18x0y4 false)
-(= i26x5y3 false)
-(= i11x2y4 true)
-(= i10x2y1 false)
-(= i18x2y3 true)
-(= i24x2y4 false)
-(= i29x2y5 false)
-(= i28x2y5 true)
-(= i11x4y2 true)
-(= i7x3y2 true)
-(= i16x4y5 false)
-(= i27x0y3 false)
-(= i16x6y3 false)
-(= i19x3y2 true)
-(= i20x5y2 false)
-(= i12x3y6 true)
-(= i22x3y6 false)
-(= i27x2y1 false)
-(= i13x3y4 false)
-(= i24x3y1 false)
-(= i10x6y2 true)
-(= i0x3y5 true)
-(= i21x5y4 false)
-(= i17x0y4 false)
-(= i7x0y4 true)
-(= i8x6y2 true)
-(= i10x1y3 true)
-(= i11x3y2 true)
-(= i24x4y3 false)
-(= i13x4y5 false)
-(= i13x6y2 false)
-(= i25x5y3 false)
-(= i13x5y2 true)
-(= i13x6y4 true)
-(= i15x2y2 true)
-(= i31x2y6 false)
-(= i25x1y2 false)
-(= i18x0y3 true)
-(= i29x2y4 true)
-(= i0x2y5 true)
-(= i15x4y5 false)
-(= i16x2y1 false)
-(= i29x4y2 false)
-(= i30x3y1 false)
-(= i28x5y3 false)
-(= i13x4y1 false)
-(= i13x4y3 true)
-(= i22x5y2 false)
-(= i14x0y3 true)
-(= i20x6y3 false)
-(= i7x2y2 true)
-(= i22x2y6 true)
-(= i18x4y2 true)
-(= i10x4y3 true)
-(= i24x3y2 false)
-(= i16x4y2 true)
-(= i20x4y5 false)
-(= i24x2y6 true)
-(= i17x0y3 true)
-(= i26x2y2 false)
-(= i31x3y2 false)
-(= i23x2y4 false)
-(= i18x0y2 true)
-(= i24x2y0 false)
-(= i5x2y6 true)
-(= i25x1y4 true)
-(= i29x3y3 false)
-(= i13x5y3 true)
-(= i17x1y2 true)
-(= i27x2y5 false)
-(= i22x5y4 false)
-(= i8x2y6 true)
-(= i30x2y5 false)
-(= i6x6y2 true)
-(= i28x4y6 false)
-(= i3x6y4 true)
-(= i29x2y2 false)
-(= i22x5y3 false)
-(= i26x3y4 false)
-(= i11x0y2 true)
-(= i6x3y2 true)
-(= i11x2y2 true)
-(= i0x3y3 false)
-(= i1x4y1 true)
-(= i11x4y0 true)
-(= i12x0y4 true)
-(= i10x2y6 false)
-(= i28x6y4 false)
-(= i17x3y3 false)
-(= i20x2y4 false)
-(= i4x4y5 true)
-(= i5x1y3 true)
-(= i0x2y4 true)
-(= i15x2y1 false)
-(= i26x5y2 false)
-(= i25x3y4 false)
-(= i3x1y4 true)
-(= i26x3y1 false)
-(= i8x6y3 true)
-(= i19x0y2 true)
-(= i11x4y1 false)
-(= i19x3y4 false)
-(= i28x4y2 false)
-(= i2x5y4 true)
-(= i23x6y3 false)
-(= i21x4y6 false)
-(= i10x4y2 true)
-(= i26x3y0 false)
-(= i6x3y4 true)
-(= i25x3y5 true)
-(= i17x4y0 true)
-(= i27x2y3 true)
-(= i29x5y2 false)
-(= i12x2y4 false)
-(= i0x2y3 true)
-(= i24x4y0 false)
-(= i13x4y6 true)
-(= i31x2y5 false)
-(= i30x2y3 false)
-(= i4x4y3 true)
-(= i14x5y3 true)
-(= i7x3y1 false)
-(= i17x4y2 true)
-(= i22x2y1 true)
-(= i0x0y2 true)
-(= i11x4y6 true)
-(= i7x0y2 true)
-(= i4x2y6 true)
-(= i22x3y0 false)
-(= i9x4y0 false)
-(= i23x6y2 false)
-(= i9x2y0 true)
-(= i16x6y2 false)
-(= i15x2y0 false)
-(= i29x2y0 false)
-(= i2x3y1 true)
-(= i5x4y3 false)
-(= i3x3y5 true)
-(= i9x2y5 true)
-(= i27x6y2 false)
-(= i22x6y3 false)
-(= i1x1y4 true)
-(= i23x1y3 true)
-(= i5x5y3 true)
-(= i17x4y5 false)
-(= i17x0y2 true)
-(= i18x3y0 false)
-(= i6x4y2 true)
-(= i24x0y2 true)
-(= i0x2y2 true)
-(= i7x3y6 true)
-(= i20x2y3 false)
-(= i31x5y2 false)
-(= i22x3y4 false)
-(= i1x2y4 true)
-(= i16x4y0 true)
-(= i19x6y4 false)
-(= i8x4y4 false)
-(= i19x3y0 false)
-(= i30x6y4 false)
-(= i22x0y3 true)
-(= i4x4y1 false)
-(= i29x3y2 false)
-(= i8x5y4 true)
-(= i5x1y4 true)
-(= i29x1y3 false)
-(= i7x2y5 true)
-(= i10x0y4 true)
-(= i5x2y1 false)
-(= i8x1y4 true)
-(= i13x2y6 false)
-(= i14x2y4 true)
-(= i22x3y2 true)
-(= i22x4y3 false)
-(= i8x4y5 false)
-(= i24x2y3 true)
-(= i7x4y3 true)
-(= i7x4y4 true)
-(= i5x3y3 false)
-(= i28x4y4 false)
-(= i3x5y2 true)
-(= i30x0y3 false)
-(= i10x1y2 true)
-(= i8x5y3 true)
-(= i0x4y4 true)
-(= i3x4y0 true)
-(= i31x2y3 false)
-(= i18x4y4 false)
-(= i6x2y6 true)
-(= i28x3y4 false)
-(= i16x3y5 true)
-(= i19x3y1 false)
-(= i22x3y3 false)
-(= i24x2y2 false)
-(= i24x3y5 true)
-(= i5x4y0 false)
-(= i12x4y1 false)
-(= i17x2y2 true)
-(= i28x2y1 false)
-(= i16x2y4 true)
-(= i24x4y4 false)
-(= i6x6y3 true)
-(= i8x2y3 true)
-(= i3x3y4 true)
-(= i22x4y4 false)
-(= i1x2y2 true)
-(= i5x0y3 true)
-(= i8x4y3 true)
-(= i20x1y3 true)
-(= i21x6y3 false)
-(= i5x4y1 false)
-(= i8x0y2 true)
-(= i19x2y1 false)
-(= i21x4y0 true)
-(= i23x5y4 false)
-(= i15x0y3 true)
-(= i10x1y4 false)
-(= i29x6y4 false)
-(= i5x3y0 true)
-(= i13x4y2 true)
-(= i27x0y2 false)
-(= i17x4y3 true)
-(= i26x4y6 false)
-(= i10x5y3 true)
-(= i29x5y4 false)
-(= i18x4y3 true)
-(= i4x2y4 true)
-(= i1x4y0 true)
-(= i10x2y5 false)
-(= i25x0y4 false)
-(= i5x4y2 true)
-(= i30x4y3 false)
-(= i2x2y4 true)
-(= i25x3y1 false)
-(= i3x3y1 false)
-(= i12x3y4 false)
-(= i15x3y1 false)
-(= i2x1y2 true)
-(= i22x4y5 false)
-(= i17x4y4 true)
-(= i6x4y0 false)
-(= i17x6y2 false)
-(= i18x6y2 false)
-(= i5x3y2 true)
-(= i7x2y6 true)
-(= i21x6y4 false)
-(= i25x6y2 false)
-(= i2x4y2 false)
-(= i31x5y4 false)
-(= i3x3y3 true)
-(= i14x4y2 true)
-(= i19x6y2 false)
-(= i25x5y4 false)
-(= i19x3y5 true)
-(= i5x3y5 true)
-(= i7x2y4 true)
-(= i15x1y3 true)
-(= i16x4y1 false)
-(= i3x0y4 true)
-(= i8x2y5 true)
-(= i13x3y2 true)
-(= i25x0y3 true)
-(= i5x5y4 true)
-(= i13x2y3 true)
-(= i20x4y0 true)
-(= i4x6y2 true)
-(= i21x3y6 false)
-(= i22x1y3 true)
-(= i1x0y3 true)
-(= i1x4y3 false)
-(= i8x3y5 true)
-(= i25x2y0 false)
-(= i13x2y5 false)
-(= i4x6y4 true)
-(= i4x4y4 true)
-(= i20x2y2 false)
-(= i21x4y2 false)
-(= i4x2y2 true)
-(= i31x5y3 false)
-(= i15x4y2 true)
-(= i28x1y3 false)
-(= i25x5y2 false)
-(= i7x1y3 true)
-(= i13x3y0 false)
-(= i16x3y4 false)
-(= i23x3y5 true)
-(= i0x3y2 true)
-(= i15x3y3 false)
-(= i1x4y6 true)
-(= i2x3y3 true)
-(= i19x4y5 false)
-(= i7x5y3 true)
-(= i6x3y6 true)
-(= i19x4y0 true)
-(= i4x3y1 false)
-(= i16x1y4 false)
-(= i27x3y0 false)
-(= i13x6y3 false)
-(= i17x3y5 true)
-(= i6x6y4 true)
-(= i0x1y4 true)
-(= i23x4y6 false)
-(= i23x4y2 false)
-(= i16x0y3 true)
-(= i17x6y4 false)
-(= i29x4y0 false)
-(= i31x3y1 false)
-(= i13x2y2 true)
-(= i15x4y3 true)
-(= i18x1y3 true)
-(= i12x0y3 true)
-(= i15x4y4 true)
-(= i31x3y0 false)
-(= i11x2y3 true)
-(= i3x3y2 true)
-(= i15x2y3 true)
-(= i27x4y3 false)
-(= i27x5y3 false)
-(= i22x1y4 true)
-(= i19x2y2 true)
-(= i31x2y1 false)
-(= i21x0y4 false)
-(= i18x1y4 false)
-(= i10x3y0 true)
-(= i18x4y0 true)
-(= i3x2y2 true)
-(= i5x2y0 true)
-(= i10x0y3 true)
-(= i9x5y2 true)
-(= i0x5y3 true)
-(= i15x3y6 true)
-(= i18x1y2 true)
-(= i31x3y4 false)
-(= i19x3y3 false)
-(= i30x3y0 false)
-(= i27x4y1 false)
-(= i9x5y4 true)
-(= i4x2y0 true)
-(= i26x2y0 false)
-(= i3x2y4 true)
-(= i30x2y1 false)
-(= i22x0y4 false)
-(= i3x0y2 true)
-(= i15x4y1 false)
-(= i9x1y4 false)
-(= i26x4y3 false)
-(= i6x3y3 false)
-(= i8x2y1 false)
-(= i17x2y4 true)
-(= i19x2y3 true)
-(= i22x2y4 false)
-(= i31x3y6 false)
-(= i7x2y3 true)
-(= i29x4y4 false)
-(= i0x5y4 true)
-(= i21x2y3 false)
-(= i30x4y2 false)
-(= i4x5y2 true)
-(= i11x1y2 true)
-(= i22x2y3 false)
-(= i3x3y0 true)
-(= i17x3y1 false)
-(= i6x3y5 true)
-(= i26x4y1 false)
-(= i3x4y4 true)
-(= i29x3y4 false)
-(= i25x4y4 false)
-(= i4x4y0 false)
-(= i14x4y1 false)
-(= i19x3y6 false)
-(= i8x0y4 true)
-(= i23x4y3 false)
-(= i21x0y2 true)
-(= i6x5y2 true)
-(= i25x3y2 false)
-(= i16x2y6 true)
-(= i6x4y1 false)
-(= i14x1y3 true)
-(= i29x3y1 false)
-(= i0x1y3 true)
-(= i13x2y4 false)
-(= i18x3y4 true)
-(= i0x2y6 true)
-(= i2x3y2 true)
-(= i28x4y1 false)
-(= i2x1y4 true)
-(= i0x4y2 true)
-(= i28x3y6 false)
-(= i6x1y3 true)
-(= i18x2y2 true)
-(= i29x4y3 false)
-(= i30x0y4 false)
-(= i2x2y3 true)
-(= i15x2y5 false)
-(= i8x3y6 true)
-(= i19x2y4 false)
-(= i20x4y4 false)
-(= i3x2y0 true)
-(= i28x1y4 true)
-(= i22x2y2 false)
-(= i6x2y4 true)
-(= i31x3y5 false)
-(= i5x2y3 true)
-(= i13x2y1 false)
-(= i16x1y2 true)
-(= i1x4y4 true)
-(= i15x3y0 false)
-(= i20x4y3 true)
-(= i21x2y5 false)
-(= i25x4y3 false)
-(= i7x1y2 true)
-(= i24x6y4 false)
-(= i9x3y4 true)
-(= i19x4y3 true)
-(= i9x4y2 true)
-(= i5x5y2 true)
-(= i23x2y2 true)
-(= i26x4y4 false)
-(= i4x4y6 true)
-(= i28x3y0 false)
-(= i14x2y2 true)
-(= i5x4y6 true)
-(= i21x5y3 false)
-(= i5x4y4 true)
-(= i5x1y2 true)
-(= i5x6y3 true)
-(= i5x4y5 true)
-(= i19x2y0 false)
-(= i15x4y0 true)
-(= i16x3y3 false)
-(= i11x2y0 false)
-(= i9x4y5 false)
-(= i2x4y1 false)
-(= i8x2y4 true)
-(= i9x3y2 true)
-(= i16x3y0 false)
-(= i19x2y5 false)
-(= i30x1y2 false)
-(= i18x2y4 true)
-(= i30x2y0 false)
-(= i1x3y6 true)
-(= i10x6y4 false)
-(= i17x2y5 false)
-(= i28x5y4 false)
-(= i12x4y2 true)
-(= i14x1y4 false)
-(= i29x4y5 false)
-(= i1x2y5 true)
-(= i2x4y3 true)
-(= i7x4y1 false)
-(= i1x4y2 true)
-(= i24x0y3 true)
-(= i10x4y4 false)
-(= i6x2y1 false)
-(= i7x5y2 true)
-(= i8x1y2 true)
-(= i8x4y2 true)
-(= i10x6y3 true)
-(= i14x6y4 true)
-(= i10x2y0 true)
-(= i23x4y0 false)
-(= i28x3y1 false)
-(= i10x4y5 false)
-(= i31x6y4 false)
-(= i19x1y2 true)
-(= i7x4y2 true)
-(= i16x5y2 true)
-(= i24x2y5 false)
-(= i24x3y4 false)
-(= i2x2y1 true)
-(= i15x2y6 false)
-(= i2x5y2 true)
-(= i23x2y6 true)
-(= i30x5y3 false)
-(= i3x4y5 true)
-(= i10x3y5 true)
-(= i27x1y3 false)
-(= i26x2y6 true)
-(= i20x4y2 true)
-(= i2x2y2 true)
-(= i22x0y2 true)
-(= i19x0y4 false)
-(= i9x3y5 true)
-(= i24x1y4 true)
-(= i21x5y2 false)
-(= i5x3y1 false)
-(= i20x4y6 false)
-(= i30x6y2 false)
-(= i18x2y0 false)
-(= i31x4y6 false)
-(= i17x4y6 false)
-(= i27x2y4 true)
-(= i2x6y4 true)
-(= i26x0y2 false)
-(= i30x1y3 false)
-(= i14x3y5 true)
-(= i28x2y3 false)
-(= i31x0y2 false)
-(= i28x2y4 false)
-(= i12x2y6 false)
-(= i4x3y4 true)
-(= i31x2y2 false)
-(= i7x6y4 false)
-(= i8x3y2 true)
-(= i11x6y2 true)
-(= i17x4y1 false)
-(= i29x1y2 false)
-(= i12x4y5 false)
-(= i27x4y6 false)
-(= i22x4y0 false)
-(= i2x2y0 true)
-(= i9x2y4 false)
-(= i3x3y6 true)
-(= i11x3y6 true)
-(= i11x6y3 true)
-(= i9x2y1 false)
-(= i12x2y5 false)
-(= i23x4y5 false)
-(= i27x5y2 false)
-(= i23x3y6 false)
-(= i31x4y0 false)
-(= i8x0y3 true)
-(= i23x2y0 false)
-(= i28x0y2 false)
-(= i20x1y4 true)
-(= i0x4y5 true)
-(= i6x3y1 false)
-(= i12x5y2 true)
-(= i12x4y6 true)
-(= i18x3y6 false)
-(= i3x4y2 false)
-(= i2x6y3 true)
-(= i5x6y4 true)
-(= i21x6y2 false)
-(= i1x3y3 true)
-(= i16x0y2 true)
-(= i11x4y5 false)
-(= i26x6y4 false)
-(= i31x0y4 false)
-(= i20x5y3 false)
-(= i25x0y2 false)
-(= i31x0y3 false)
-(= i10x3y3 false)
-(= i10x2y3 true)
-(= i27x2y6 true)
-(= i11x5y3 true)
-(= i2x4y4 true)
-(= i16x3y2 true)
-(= i19x5y2 false)
-(= i1x3y2 true)
-(= i21x3y4 false)
-(= i10x3y4 true)
-(= i21x2y6 true)
-(= i30x2y4 false)
-(= i28x6y3 false)
-(= i27x3y1 false)
-(= i12x4y4 false)
-(= i22x2y0 false)
-(= i15x6y2 false)
-(= i29x2y1 false)
-(= i6x3y0 true)
-(= i11x2y1 false)
-(= i23x2y3 false)
-(= i10x4y6 true)
-(= i18x2y1 false)
-(= i10x5y2 true)
-(= i16x2y2 true)
-(= i2x2y5 true)
-(= i7x4y6 true)
-(= i25x3y0 false)
-(= i17x3y2 true)
-(= i31x1y2 false)
-(= i22x4y2 true)
-(= i26x5y4 false)
-(= i24x5y2 false)
-(= i0x6y4 true)
-(= i17x3y4 false)
-(= i29x2y3 false)
-(= i21x1y3 true)
-(= i23x1y2 true)
-(= i21x1y4 true)
-(= i5x2y4 true)
-(= i25x6y3 false)
-(= i11x1y4 false)
-(= i20x0y3 true)
-(= i16x5y4 false)
-(= i28x2y0 false)
-(= i5x6y2 true)
-(= i15x5y3 true)
-(= i31x6y3 false)
-(= i1x5y2 true)
-(= i17x3y6 false)
-(= i18x5y4 false)
-(= i13x5y4 true)
-(= i16x4y3 true)
-(= i6x2y0 true)
-(= i25x2y3 true)
-(= i19x4y4 false)
-(= i3x0y3 true)
-(= i30x3y4 true)
-(= i4x4y2 true)
-(= i18x5y2 false)
-(= i21x2y0 false)
-(= i29x5y3 false)
-(= i11x0y4 true)
-(= i31x3y3 true)
-(= i7x2y0 true)
-(= i20x2y1 true)
-(= i0x5y2 true)
-(= i14x0y2 true)
-(= i19x1y3 true)
-(= i11x0y3 true)
-(= i20x1y2 true)
-(= i25x1y3 true)
-(= i30x3y2 false)
-(= i16x3y6 false)
-(= i4x6y3 true)
-(= i8x3y4 false)
-(= i31x2y0 false)
-(= i20x3y0 false)
-(= i29x4y1 false)
-(= i0x4y1 true)
-(= i14x4y4 false)
-(= i0x1y2 true)
-(= i2x2y6 true)
-(= i26x2y4 true)
-(= i23x3y0 false)
-(= i14x6y3 false)
-(= i16x2y3 true)
-(= i19x4y2 true)
-(= i31x4y1 false)
-(= i20x3y4 false)
-(= i31x1y3 false)
-(= i22x6y2 false)
-(= i25x6y4 false)
-(= i17x1y4 false)
-(= i30x4y4 false)
-(= i9x0y3 true)
-(= i0x3y4 true)
-(= i20x0y2 true)
-(= i23x3y1 false)
-(= i3x5y3 false)
-(= i26x1y2 false)
-(= i11x3y1 false)
-(= i9x2y6 true)
-(= i14x0y4 false)
-(= i14x1y2 true)
-(= i20x3y6 false)
-(= i14x3y1 false)
-(= i9x4y3 true)
-(= i27x3y4 false)
-(= i27x2y2 false)
-(= i15x6y4 false)
-(= i12x3y0 false)
-(= i12x6y4 false)
-(= i26x6y2 false)
-(= i17x5y3 false)
-(= i23x3y2 false)
-(= i12x0y2 true)
-(= i18x5y3 false)
-(= i8x3y3 false)
-(= i2x3y0 true)
-(= i15x6y3 false)
-(= i0x0y4 true)
-(= i23x6y4 false)
-(= i4x3y2 true)
-(= i4x5y3 false)
-(= i9x2y2 true)
-(= i30x1y4 false)
-(= i28x3y2 false)
-(= i0x6y3 true)
-(= i7x5y4 false)
-(= i21x4y1 true)
-(= i8x3y0 true)
-(= i15x3y2 true)
-(= i27x4y0 false)
-(= i15x4y6 true)
-(= i13x1y2 true)
-(= i12x2y3 true)
-
--- /dev/null
+sat
+
+(= i1x2y0 true)
+(= i4x2y1 false)
+(= i1x2y3 true)
+(= i11x2y5 false)
+(= i31x6y2 false)
+(= i26x0y3 true)
+(= i10x3y6 true)
+(= i13x3y5 true)
+(= i20x0y4 false)
+(= i30x2y2 false)
+(= i6x2y3 true)
+(= i6x5y3 true)
+(= i0x4y0 true)
+(= i17x2y0 false)
+(= i20x3y1 false)
+(= i24x5y4 false)
+(= i16x4y6 false)
+(= i26x0y4 false)
+(= i26x2y5 false)
+(= i14x2y6 false)
+(= i29x1y4 true)
+(= i1x0y4 true)
+(= i21x3y3 false)
+(= i31x4y2 false)
+(= i18x6y3 false)
+(= i3x1y2 true)
+(= i4x3y6 true)
+(= i9x1y3 true)
+(= i16x6y4 false)
+(= i18x6y4 false)
+(= i19x1y4 true)
+(= i14x3y0 false)
+(= i9x3y3 false)
+(= i3x5y4 true)
+(= i21x4y5 false)
+(= i14x4y5 false)
+(= i30x5y2 false)
+(= i22x4y6 false)
+(= i6x0y3 true)
+(= i18x2y5 false)
+(= i27x1y2 false)
+(= i26x2y1 false)
+(= i24x4y6 false)
+(= i31x4y4 false)
+(= i19x5y3 false)
+(= i15x1y4 false)
+(= i9x3y6 true)
+(= i0x3y1 true)
+(= i14x6y2 false)
+(= i28x0y3 false)
+(= i0x6y2 true)
+(= i9x5y3 true)
+(= i13x0y4 true)
+(= i11x1y3 true)
+(= i7x3y3 false)
+(= i21x2y4 false)
+(= i15x5y4 false)
+(= i27x4y2 false)
+(= i6x0y2 true)
+(= i14x3y4 false)
+(= i9x0y4 true)
+(= i20x6y4 false)
+(= i7x1y4 true)
+(= i21x1y2 true)
+(= i24x4y5 false)
+(= i30x4y5 false)
+(= i31x1y4 false)
+(= i8x4y1 false)
+(= i1x3y5 true)
+(= i3x2y6 true)
+(= i13x1y4 true)
+(= i2x6y2 true)
+(= i9x4y1 false)
+(= i29x0y2 false)
+(= i15x0y4 false)
+(= i28x5y2 false)
+(= i24x3y6 false)
+(= i18x3y1 false)
+(= i19x4y6 false)
+(= i22x3y1 false)
+(= i19x4y1 false)
+(= i13x2y0 false)
+(= i27x3y3 false)
+(= i12x3y5 true)
+(= i16x2y0 false)
+(= i10x4y0 false)
+(= i27x2y0 false)
+(= i11x3y4 true)
+(= i9x3y0 true)
+(= i2x3y6 true)
+(= i12x6y2 true)
+(= i18x2y6 true)
+(= i23x3y4 false)
+(= i13x0y2 true)
+(= i31x2y4 false)
+(= i13x3y6 true)
+(= i2x0y4 true)
+(= i8x4y6 true)
+(= i17x5y4 true)
+(= i18x3y2 true)
+(= i6x1y2 true)
+(= i16x1y3 true)
+(= i18x3y3 false)
+(= i27x0y4 false)
+(= i6x2y5 true)
+(= i24x3y0 false)
+(= i9x3y1 false)
+(= i11x5y4 true)
+(= i3x2y3 true)
+(= i15x0y2 true)
+(= i27x3y2 false)
+(= i12x6y3 true)
+(= i5x0y2 true)
+(= i29x0y3 false)
+(= i30x4y6 false)
+(= i13x3y3 false)
+(= i28x4y5 false)
+(= i31x4y3 false)
+(= i2x4y5 true)
+(= i8x6y4 false)
+(= i13x3y1 false)
+(= i10x4y1 false)
+(= i17x2y1 false)
+(= i26x3y2 false)
+(= i30x4y0 false)
+(= i19x6y3 false)
+(= i24x2y1 false)
+(= i12x1y4 true)
+(= i29x3y6 false)
+(= i23x0y3 true)
+(= i6x4y3 true)
+(= i15x3y5 true)
+(= i23x0y4 false)
+(= i29x6y2 false)
+(= i21x4y4 false)
+(= i14x4y3 true)
+(= i29x3y0 false)
+(= i24x6y3 false)
+(= i25x3y3 false)
+(= i5x2y2 true)
+(= i30x5y4 false)
+(= i16x0y4 false)
+(= i2x5y3 false)
+(= i3x1y3 true)
+(= i12x2y0 false)
+(= i16x2y5 false)
+(= i25x2y6 true)
+(= i7x0y3 true)
+(= i10x3y2 true)
+(= i12x3y1 false)
+(= i26x6y3 false)
+(= i27x6y3 false)
+(= i6x1y4 true)
+(= i20x3y3 false)
+(= i27x6y4 false)
+(= i29x2y6 false)
+(= i3x6y3 true)
+(= i24x6y2 false)
+(= i1x5y4 true)
+(= i27x5y4 false)
+(= i10x2y4 true)
+(= i30x3y6 false)
+(= i26x2y3 false)
+(= i14x2y3 true)
+(= i28x3y5 true)
+(= i5x0y4 true)
+(= i24x1y2 true)
+(= i2x1y3 true)
+(= i4x1y3 true)
+(= i7x3y0 true)
+(= i15x3y4 false)
+(= i25x2y5 false)
+(= i12x3y2 true)
+(= i22x6y4 false)
+(= i14x4y6 true)
+(= i14x2y1 false)
+(= i22x4y1 false)
+(= i24x0y4 false)
+(= i26x3y5 true)
+(= i4x1y4 true)
+(= i23x5y2 false)
+(= i30x2y6 false)
+(= i16x4y4 true)
+(= i25x2y2 true)
+(= i0x4y3 true)
+(= i6x4y5 false)
+(= i20x3y2 true)
+(= i30x6y3 false)
+(= i20x2y0 false)
+(= i29x3y5 true)
+(= i12x4y3 true)
+(= i22x2y5 false)
+(= i12x5y3 true)
+(= i28x3y3 false)
+(= i23x4y1 false)
+(= i24x5y3 false)
+(= i20x3y5 true)
+(= i8x2y0 true)
+(= i17x3y0 false)
+(= i9x6y4 false)
+(= i2x4y6 true)
+(= i29x0y4 false)
+(= i13x0y3 true)
+(= i8x2y2 true)
+(= i14x2y5 false)
+(= i17x2y3 true)
+(= i11x3y0 false)
+(= i24x4y1 false)
+(= i14x4y0 true)
+(= i27x4y4 false)
+(= i4x5y4 true)
+(= i23x3y3 false)
+(= i9x1y2 true)
+(= i3x6y2 true)
+(= i30x0y2 false)
+(= i3x2y1 false)
+(= i11x4y4 false)
+(= i6x2y2 true)
+(= i15x2y4 true)
+(= i23x4y4 false)
+(= i26x1y3 true)
+(= i4x0y3 true)
+(= i28x0y4 false)
+(= i29x6y3 false)
+(= i2x4y0 true)
+(= i0x3y0 true)
+(= i14x3y3 false)
+(= i30x4y1 false)
+(= i11x6y4 false)
+(= i0x3y6 true)
+(= i12x1y3 true)
+(= i8x1y3 true)
+(= i28x2y2 false)
+(= i4x2y5 true)
+(= i26x1y4 true)
+(= i6x4y6 true)
+(= i21x0y3 true)
+(= i21x4y3 false)
+(= i26x4y0 false)
+(= i24x3y3 false)
+(= i18x4y1 false)
+(= i21x3y0 false)
+(= i25x2y1 false)
+(= i26x3y6 false)
+(= i27x1y4 true)
+(= i27x4y5 false)
+(= i28x2y6 true)
+(= i27x3y6 false)
+(= i19x2y6 true)
+(= i1x2y1 true)
+(= i0x0y3 true)
+(= i25x4y6 false)
+(= i4x1y2 true)
+(= i0x2y0 true)
+(= i17x6y3 false)
+(= i11x5y2 true)
+(= i7x6y3 true)
+(= i12x3y3 false)
+(= i9x0y2 true)
+(= i21x2y2 false)
+(= i4x2y3 true)
+(= i16x3y1 false)
+(= i21x3y1 false)
+(= i24x4y2 false)
+(= i4x0y4 true)
+(= i7x3y5 true)
+(= i11x4y3 true)
+(= i9x2y3 true)
+(= i20x2y6 true)
+(= i18x4y5 false)
+(= i2x0y2 true)
+(= i13x4y0 true)
+(= i25x3y6 false)
+(= i27x3y5 true)
+(= i4x3y3 true)
+(= i31x4y5 false)
+(= i10x0y2 true)
+(= i20x2y5 false)
+(= i9x4y6 true)
+(= i1x3y1 true)
+(= i28x1y2 false)
+(= i28x6y2 false)
+(= i20x6y2 false)
+(= i5x2y5 true)
+(= i1x0y2 true)
+(= i1x4y5 true)
+(= i1x1y3 true)
+(= i6x0y4 true)
+(= i14x5y2 true)
+(= i9x6y2 true)
+(= i19x0y3 true)
+(= i21x3y2 true)
+(= i26x4y2 false)
+(= i24x1y3 true)
+(= i20x4y1 false)
+(= i5x3y6 true)
+(= i23x1y4 true)
+(= i1x6y2 true)
+(= i23x5y3 false)
+(= i12x2y1 false)
+(= i2x0y3 true)
+(= i18x4y6 false)
+(= i7x4y0 false)
+(= i1x1y2 true)
+(= i0x2y1 true)
+(= i1x5y3 false)
+(= i1x3y0 true)
+(= i8x4y0 false)
+(= i10x5y4 true)
+(= i4x0y2 true)
+(= i26x3y3 false)
+(= i0x4y6 true)
+(= i7x6y2 true)
+(= i17x1y3 true)
+(= i13x4y4 false)
+(= i3x4y1 true)
+(= i5x3y4 true)
+(= i21x3y5 true)
+(= i28x4y0 false)
+(= i22x3y5 true)
+(= i14x3y6 true)
+(= i2x3y5 true)
+(= i29x4y6 false)
+(= i12x2y2 true)
+(= i30x3y3 false)
+(= i17x5y2 false)
+(= i4x3y5 true)
+(= i11x3y3 false)
+(= i30x3y5 true)
+(= i14x5y4 true)
+(= i8x5y2 true)
+(= i25x4y0 false)
+(= i9x4y4 false)
+(= i4x3y0 true)
+(= i3x4y3 true)
+(= i11x2y6 false)
+(= i18x3y5 true)
+(= i12x4y0 true)
+(= i11x3y5 true)
+(= i28x4y3 false)
+(= i14x3y2 true)
+(= i16x5y3 true)
+(= i6x5y4 true)
+(= i2x3y4 true)
+(= i19x5y4 false)
+(= i1x6y4 true)
+(= i15x5y2 true)
+(= i1x3y4 true)
+(= i3x2y5 true)
+(= i20x5y4 false)
+(= i23x0y2 true)
+(= i23x2y5 false)
+(= i3x4y6 true)
+(= i6x4y4 false)
+(= i7x2y1 false)
+(= i26x4y5 false)
+(= i25x4y1 false)
+(= i10x2y2 true)
+(= i23x2y1 true)
+(= i9x6y3 true)
+(= i8x3y1 false)
+(= i13x1y3 true)
+(= i14x2y0 false)
+(= i7x4y5 false)
+(= i15x1y2 true)
+(= i21x2y1 true)
+(= i1x2y6 true)
+(= i17x2y6 true)
+(= i12x1y2 true)
+(= i22x1y2 true)
+(= i12x5y4 true)
+(= i1x6y3 true)
+(= i25x2y4 false)
+(= i25x4y5 false)
+(= i7x3y4 true)
+(= i10x3y1 false)
+(= i25x4y2 false)
+(= i18x0y4 false)
+(= i26x5y3 false)
+(= i11x2y4 true)
+(= i10x2y1 false)
+(= i18x2y3 true)
+(= i24x2y4 false)
+(= i29x2y5 false)
+(= i28x2y5 true)
+(= i11x4y2 true)
+(= i7x3y2 true)
+(= i16x4y5 false)
+(= i27x0y3 false)
+(= i16x6y3 false)
+(= i19x3y2 true)
+(= i20x5y2 false)
+(= i12x3y6 true)
+(= i22x3y6 false)
+(= i27x2y1 false)
+(= i13x3y4 false)
+(= i24x3y1 false)
+(= i10x6y2 true)
+(= i0x3y5 true)
+(= i21x5y4 false)
+(= i17x0y4 false)
+(= i7x0y4 true)
+(= i8x6y2 true)
+(= i10x1y3 true)
+(= i11x3y2 true)
+(= i24x4y3 false)
+(= i13x4y5 false)
+(= i13x6y2 false)
+(= i25x5y3 false)
+(= i13x5y2 true)
+(= i13x6y4 true)
+(= i15x2y2 true)
+(= i31x2y6 false)
+(= i25x1y2 false)
+(= i18x0y3 true)
+(= i29x2y4 true)
+(= i0x2y5 true)
+(= i15x4y5 false)
+(= i16x2y1 false)
+(= i29x4y2 false)
+(= i30x3y1 false)
+(= i28x5y3 false)
+(= i13x4y1 false)
+(= i13x4y3 true)
+(= i22x5y2 false)
+(= i14x0y3 true)
+(= i20x6y3 false)
+(= i7x2y2 true)
+(= i22x2y6 true)
+(= i18x4y2 true)
+(= i10x4y3 true)
+(= i24x3y2 false)
+(= i16x4y2 true)
+(= i20x4y5 false)
+(= i24x2y6 true)
+(= i17x0y3 true)
+(= i26x2y2 false)
+(= i31x3y2 false)
+(= i23x2y4 false)
+(= i18x0y2 true)
+(= i24x2y0 false)
+(= i5x2y6 true)
+(= i25x1y4 true)
+(= i29x3y3 false)
+(= i13x5y3 true)
+(= i17x1y2 true)
+(= i27x2y5 false)
+(= i22x5y4 false)
+(= i8x2y6 true)
+(= i30x2y5 false)
+(= i6x6y2 true)
+(= i28x4y6 false)
+(= i3x6y4 true)
+(= i29x2y2 false)
+(= i22x5y3 false)
+(= i26x3y4 false)
+(= i11x0y2 true)
+(= i6x3y2 true)
+(= i11x2y2 true)
+(= i0x3y3 false)
+(= i1x4y1 true)
+(= i11x4y0 true)
+(= i12x0y4 true)
+(= i10x2y6 false)
+(= i28x6y4 false)
+(= i17x3y3 false)
+(= i20x2y4 false)
+(= i4x4y5 true)
+(= i5x1y3 true)
+(= i0x2y4 true)
+(= i15x2y1 false)
+(= i26x5y2 false)
+(= i25x3y4 false)
+(= i3x1y4 true)
+(= i26x3y1 false)
+(= i8x6y3 true)
+(= i19x0y2 true)
+(= i11x4y1 false)
+(= i19x3y4 false)
+(= i28x4y2 false)
+(= i2x5y4 true)
+(= i23x6y3 false)
+(= i21x4y6 false)
+(= i10x4y2 true)
+(= i26x3y0 false)
+(= i6x3y4 true)
+(= i25x3y5 true)
+(= i17x4y0 true)
+(= i27x2y3 true)
+(= i29x5y2 false)
+(= i12x2y4 false)
+(= i0x2y3 true)
+(= i24x4y0 false)
+(= i13x4y6 true)
+(= i31x2y5 false)
+(= i30x2y3 false)
+(= i4x4y3 true)
+(= i14x5y3 true)
+(= i7x3y1 false)
+(= i17x4y2 true)
+(= i22x2y1 true)
+(= i0x0y2 true)
+(= i11x4y6 true)
+(= i7x0y2 true)
+(= i4x2y6 true)
+(= i22x3y0 false)
+(= i9x4y0 false)
+(= i23x6y2 false)
+(= i9x2y0 true)
+(= i16x6y2 false)
+(= i15x2y0 false)
+(= i29x2y0 false)
+(= i2x3y1 true)
+(= i5x4y3 false)
+(= i3x3y5 true)
+(= i9x2y5 true)
+(= i27x6y2 false)
+(= i22x6y3 false)
+(= i1x1y4 true)
+(= i23x1y3 true)
+(= i5x5y3 true)
+(= i17x4y5 false)
+(= i17x0y2 true)
+(= i18x3y0 false)
+(= i6x4y2 true)
+(= i24x0y2 true)
+(= i0x2y2 true)
+(= i7x3y6 true)
+(= i20x2y3 false)
+(= i31x5y2 false)
+(= i22x3y4 false)
+(= i1x2y4 true)
+(= i16x4y0 true)
+(= i19x6y4 false)
+(= i8x4y4 false)
+(= i19x3y0 false)
+(= i30x6y4 false)
+(= i22x0y3 true)
+(= i4x4y1 false)
+(= i29x3y2 false)
+(= i8x5y4 true)
+(= i5x1y4 true)
+(= i29x1y3 false)
+(= i7x2y5 true)
+(= i10x0y4 true)
+(= i5x2y1 false)
+(= i8x1y4 true)
+(= i13x2y6 false)
+(= i14x2y4 true)
+(= i22x3y2 true)
+(= i22x4y3 false)
+(= i8x4y5 false)
+(= i24x2y3 true)
+(= i7x4y3 true)
+(= i7x4y4 true)
+(= i5x3y3 false)
+(= i28x4y4 false)
+(= i3x5y2 true)
+(= i30x0y3 false)
+(= i10x1y2 true)
+(= i8x5y3 true)
+(= i0x4y4 true)
+(= i3x4y0 true)
+(= i31x2y3 false)
+(= i18x4y4 false)
+(= i6x2y6 true)
+(= i28x3y4 false)
+(= i16x3y5 true)
+(= i19x3y1 false)
+(= i22x3y3 false)
+(= i24x2y2 false)
+(= i24x3y5 true)
+(= i5x4y0 false)
+(= i12x4y1 false)
+(= i17x2y2 true)
+(= i28x2y1 false)
+(= i16x2y4 true)
+(= i24x4y4 false)
+(= i6x6y3 true)
+(= i8x2y3 true)
+(= i3x3y4 true)
+(= i22x4y4 false)
+(= i1x2y2 true)
+(= i5x0y3 true)
+(= i8x4y3 true)
+(= i20x1y3 true)
+(= i21x6y3 false)
+(= i5x4y1 false)
+(= i8x0y2 true)
+(= i19x2y1 false)
+(= i21x4y0 true)
+(= i23x5y4 false)
+(= i15x0y3 true)
+(= i10x1y4 false)
+(= i29x6y4 false)
+(= i5x3y0 true)
+(= i13x4y2 true)
+(= i27x0y2 false)
+(= i17x4y3 true)
+(= i26x4y6 false)
+(= i10x5y3 true)
+(= i29x5y4 false)
+(= i18x4y3 true)
+(= i4x2y4 true)
+(= i1x4y0 true)
+(= i10x2y5 false)
+(= i25x0y4 false)
+(= i5x4y2 true)
+(= i30x4y3 false)
+(= i2x2y4 true)
+(= i25x3y1 false)
+(= i3x3y1 false)
+(= i12x3y4 false)
+(= i15x3y1 false)
+(= i2x1y2 true)
+(= i22x4y5 false)
+(= i17x4y4 true)
+(= i6x4y0 false)
+(= i17x6y2 false)
+(= i18x6y2 false)
+(= i5x3y2 true)
+(= i7x2y6 true)
+(= i21x6y4 false)
+(= i25x6y2 false)
+(= i2x4y2 false)
+(= i31x5y4 false)
+(= i3x3y3 true)
+(= i14x4y2 true)
+(= i19x6y2 false)
+(= i25x5y4 false)
+(= i19x3y5 true)
+(= i5x3y5 true)
+(= i7x2y4 true)
+(= i15x1y3 true)
+(= i16x4y1 false)
+(= i3x0y4 true)
+(= i8x2y5 true)
+(= i13x3y2 true)
+(= i25x0y3 true)
+(= i5x5y4 true)
+(= i13x2y3 true)
+(= i20x4y0 true)
+(= i4x6y2 true)
+(= i21x3y6 false)
+(= i22x1y3 true)
+(= i1x0y3 true)
+(= i1x4y3 false)
+(= i8x3y5 true)
+(= i25x2y0 false)
+(= i13x2y5 false)
+(= i4x6y4 true)
+(= i4x4y4 true)
+(= i20x2y2 false)
+(= i21x4y2 false)
+(= i4x2y2 true)
+(= i31x5y3 false)
+(= i15x4y2 true)
+(= i28x1y3 false)
+(= i25x5y2 false)
+(= i7x1y3 true)
+(= i13x3y0 false)
+(= i16x3y4 false)
+(= i23x3y5 true)
+(= i0x3y2 true)
+(= i15x3y3 false)
+(= i1x4y6 true)
+(= i2x3y3 true)
+(= i19x4y5 false)
+(= i7x5y3 true)
+(= i6x3y6 true)
+(= i19x4y0 true)
+(= i4x3y1 false)
+(= i16x1y4 false)
+(= i27x3y0 false)
+(= i13x6y3 false)
+(= i17x3y5 true)
+(= i6x6y4 true)
+(= i0x1y4 true)
+(= i23x4y6 false)
+(= i23x4y2 false)
+(= i16x0y3 true)
+(= i17x6y4 false)
+(= i29x4y0 false)
+(= i31x3y1 false)
+(= i13x2y2 true)
+(= i15x4y3 true)
+(= i18x1y3 true)
+(= i12x0y3 true)
+(= i15x4y4 true)
+(= i31x3y0 false)
+(= i11x2y3 true)
+(= i3x3y2 true)
+(= i15x2y3 true)
+(= i27x4y3 false)
+(= i27x5y3 false)
+(= i22x1y4 true)
+(= i19x2y2 true)
+(= i31x2y1 false)
+(= i21x0y4 false)
+(= i18x1y4 false)
+(= i10x3y0 true)
+(= i18x4y0 true)
+(= i3x2y2 true)
+(= i5x2y0 true)
+(= i10x0y3 true)
+(= i9x5y2 true)
+(= i0x5y3 true)
+(= i15x3y6 true)
+(= i18x1y2 true)
+(= i31x3y4 false)
+(= i19x3y3 false)
+(= i30x3y0 false)
+(= i27x4y1 false)
+(= i9x5y4 true)
+(= i4x2y0 true)
+(= i26x2y0 false)
+(= i3x2y4 true)
+(= i30x2y1 false)
+(= i22x0y4 false)
+(= i3x0y2 true)
+(= i15x4y1 false)
+(= i9x1y4 false)
+(= i26x4y3 false)
+(= i6x3y3 false)
+(= i8x2y1 false)
+(= i17x2y4 true)
+(= i19x2y3 true)
+(= i22x2y4 false)
+(= i31x3y6 false)
+(= i7x2y3 true)
+(= i29x4y4 false)
+(= i0x5y4 true)
+(= i21x2y3 false)
+(= i30x4y2 false)
+(= i4x5y2 true)
+(= i11x1y2 true)
+(= i22x2y3 false)
+(= i3x3y0 true)
+(= i17x3y1 false)
+(= i6x3y5 true)
+(= i26x4y1 false)
+(= i3x4y4 true)
+(= i29x3y4 false)
+(= i25x4y4 false)
+(= i4x4y0 false)
+(= i14x4y1 false)
+(= i19x3y6 false)
+(= i8x0y4 true)
+(= i23x4y3 false)
+(= i21x0y2 true)
+(= i6x5y2 true)
+(= i25x3y2 false)
+(= i16x2y6 true)
+(= i6x4y1 false)
+(= i14x1y3 true)
+(= i29x3y1 false)
+(= i0x1y3 true)
+(= i13x2y4 false)
+(= i18x3y4 true)
+(= i0x2y6 true)
+(= i2x3y2 true)
+(= i28x4y1 false)
+(= i2x1y4 true)
+(= i0x4y2 true)
+(= i28x3y6 false)
+(= i6x1y3 true)
+(= i18x2y2 true)
+(= i29x4y3 false)
+(= i30x0y4 false)
+(= i2x2y3 true)
+(= i15x2y5 false)
+(= i8x3y6 true)
+(= i19x2y4 false)
+(= i20x4y4 false)
+(= i3x2y0 true)
+(= i28x1y4 true)
+(= i22x2y2 false)
+(= i6x2y4 true)
+(= i31x3y5 false)
+(= i5x2y3 true)
+(= i13x2y1 false)
+(= i16x1y2 true)
+(= i1x4y4 true)
+(= i15x3y0 false)
+(= i20x4y3 true)
+(= i21x2y5 false)
+(= i25x4y3 false)
+(= i7x1y2 true)
+(= i24x6y4 false)
+(= i9x3y4 true)
+(= i19x4y3 true)
+(= i9x4y2 true)
+(= i5x5y2 true)
+(= i23x2y2 true)
+(= i26x4y4 false)
+(= i4x4y6 true)
+(= i28x3y0 false)
+(= i14x2y2 true)
+(= i5x4y6 true)
+(= i21x5y3 false)
+(= i5x4y4 true)
+(= i5x1y2 true)
+(= i5x6y3 true)
+(= i5x4y5 true)
+(= i19x2y0 false)
+(= i15x4y0 true)
+(= i16x3y3 false)
+(= i11x2y0 false)
+(= i9x4y5 false)
+(= i2x4y1 false)
+(= i8x2y4 true)
+(= i9x3y2 true)
+(= i16x3y0 false)
+(= i19x2y5 false)
+(= i30x1y2 false)
+(= i18x2y4 true)
+(= i30x2y0 false)
+(= i1x3y6 true)
+(= i10x6y4 false)
+(= i17x2y5 false)
+(= i28x5y4 false)
+(= i12x4y2 true)
+(= i14x1y4 false)
+(= i29x4y5 false)
+(= i1x2y5 true)
+(= i2x4y3 true)
+(= i7x4y1 false)
+(= i1x4y2 true)
+(= i24x0y3 true)
+(= i10x4y4 false)
+(= i6x2y1 false)
+(= i7x5y2 true)
+(= i8x1y2 true)
+(= i8x4y2 true)
+(= i10x6y3 true)
+(= i14x6y4 true)
+(= i10x2y0 true)
+(= i23x4y0 false)
+(= i28x3y1 false)
+(= i10x4y5 false)
+(= i31x6y4 false)
+(= i19x1y2 true)
+(= i7x4y2 true)
+(= i16x5y2 true)
+(= i24x2y5 false)
+(= i24x3y4 false)
+(= i2x2y1 true)
+(= i15x2y6 false)
+(= i2x5y2 true)
+(= i23x2y6 true)
+(= i30x5y3 false)
+(= i3x4y5 true)
+(= i10x3y5 true)
+(= i27x1y3 false)
+(= i26x2y6 true)
+(= i20x4y2 true)
+(= i2x2y2 true)
+(= i22x0y2 true)
+(= i19x0y4 false)
+(= i9x3y5 true)
+(= i24x1y4 true)
+(= i21x5y2 false)
+(= i5x3y1 false)
+(= i20x4y6 false)
+(= i30x6y2 false)
+(= i18x2y0 false)
+(= i31x4y6 false)
+(= i17x4y6 false)
+(= i27x2y4 true)
+(= i2x6y4 true)
+(= i26x0y2 false)
+(= i30x1y3 false)
+(= i14x3y5 true)
+(= i28x2y3 false)
+(= i31x0y2 false)
+(= i28x2y4 false)
+(= i12x2y6 false)
+(= i4x3y4 true)
+(= i31x2y2 false)
+(= i7x6y4 false)
+(= i8x3y2 true)
+(= i11x6y2 true)
+(= i17x4y1 false)
+(= i29x1y2 false)
+(= i12x4y5 false)
+(= i27x4y6 false)
+(= i22x4y0 false)
+(= i2x2y0 true)
+(= i9x2y4 false)
+(= i3x3y6 true)
+(= i11x3y6 true)
+(= i11x6y3 true)
+(= i9x2y1 false)
+(= i12x2y5 false)
+(= i23x4y5 false)
+(= i27x5y2 false)
+(= i23x3y6 false)
+(= i31x4y0 false)
+(= i8x0y3 true)
+(= i23x2y0 false)
+(= i28x0y2 false)
+(= i20x1y4 true)
+(= i0x4y5 true)
+(= i6x3y1 false)
+(= i12x5y2 true)
+(= i12x4y6 true)
+(= i18x3y6 false)
+(= i3x4y2 false)
+(= i2x6y3 true)
+(= i5x6y4 true)
+(= i21x6y2 false)
+(= i1x3y3 true)
+(= i16x0y2 true)
+(= i11x4y5 false)
+(= i26x6y4 false)
+(= i31x0y4 false)
+(= i20x5y3 false)
+(= i25x0y2 false)
+(= i31x0y3 false)
+(= i10x3y3 false)
+(= i10x2y3 true)
+(= i27x2y6 true)
+(= i11x5y3 true)
+(= i2x4y4 true)
+(= i16x3y2 true)
+(= i19x5y2 false)
+(= i1x3y2 true)
+(= i21x3y4 false)
+(= i10x3y4 true)
+(= i21x2y6 true)
+(= i30x2y4 false)
+(= i28x6y3 false)
+(= i27x3y1 false)
+(= i12x4y4 false)
+(= i22x2y0 false)
+(= i15x6y2 false)
+(= i29x2y1 false)
+(= i6x3y0 true)
+(= i11x2y1 false)
+(= i23x2y3 false)
+(= i10x4y6 true)
+(= i18x2y1 false)
+(= i10x5y2 true)
+(= i16x2y2 true)
+(= i2x2y5 true)
+(= i7x4y6 true)
+(= i25x3y0 false)
+(= i17x3y2 true)
+(= i31x1y2 false)
+(= i22x4y2 true)
+(= i26x5y4 false)
+(= i24x5y2 false)
+(= i0x6y4 true)
+(= i17x3y4 false)
+(= i29x2y3 false)
+(= i21x1y3 true)
+(= i23x1y2 true)
+(= i21x1y4 true)
+(= i5x2y4 true)
+(= i25x6y3 false)
+(= i11x1y4 false)
+(= i20x0y3 true)
+(= i16x5y4 false)
+(= i28x2y0 false)
+(= i5x6y2 true)
+(= i15x5y3 true)
+(= i31x6y3 false)
+(= i1x5y2 true)
+(= i17x3y6 false)
+(= i18x5y4 false)
+(= i13x5y4 true)
+(= i16x4y3 true)
+(= i6x2y0 true)
+(= i25x2y3 true)
+(= i19x4y4 false)
+(= i3x0y3 true)
+(= i30x3y4 true)
+(= i4x4y2 true)
+(= i18x5y2 false)
+(= i21x2y0 false)
+(= i29x5y3 false)
+(= i11x0y4 true)
+(= i31x3y3 true)
+(= i7x2y0 true)
+(= i20x2y1 true)
+(= i0x5y2 true)
+(= i14x0y2 true)
+(= i19x1y3 true)
+(= i11x0y3 true)
+(= i20x1y2 true)
+(= i25x1y3 true)
+(= i30x3y2 false)
+(= i16x3y6 false)
+(= i4x6y3 true)
+(= i8x3y4 false)
+(= i31x2y0 false)
+(= i20x3y0 false)
+(= i29x4y1 false)
+(= i0x4y1 true)
+(= i14x4y4 false)
+(= i0x1y2 true)
+(= i2x2y6 true)
+(= i26x2y4 true)
+(= i23x3y0 false)
+(= i14x6y3 false)
+(= i16x2y3 true)
+(= i19x4y2 true)
+(= i31x4y1 false)
+(= i20x3y4 false)
+(= i31x1y3 false)
+(= i22x6y2 false)
+(= i25x6y4 false)
+(= i17x1y4 false)
+(= i30x4y4 false)
+(= i9x0y3 true)
+(= i0x3y4 true)
+(= i20x0y2 true)
+(= i23x3y1 false)
+(= i3x5y3 false)
+(= i26x1y2 false)
+(= i11x3y1 false)
+(= i9x2y6 true)
+(= i14x0y4 false)
+(= i14x1y2 true)
+(= i20x3y6 false)
+(= i14x3y1 false)
+(= i9x4y3 true)
+(= i27x3y4 false)
+(= i27x2y2 false)
+(= i15x6y4 false)
+(= i12x3y0 false)
+(= i12x6y4 false)
+(= i26x6y2 false)
+(= i17x5y3 false)
+(= i23x3y2 false)
+(= i12x0y2 true)
+(= i18x5y3 false)
+(= i8x3y3 false)
+(= i2x3y0 true)
+(= i15x6y3 false)
+(= i0x0y4 true)
+(= i23x6y4 false)
+(= i4x3y2 true)
+(= i4x5y3 false)
+(= i9x2y2 true)
+(= i30x1y4 false)
+(= i28x3y2 false)
+(= i0x6y3 true)
+(= i7x5y4 false)
+(= i21x4y1 true)
+(= i8x3y0 true)
+(= i15x3y2 true)
+(= i27x4y0 false)
+(= i15x4y6 true)
+(= i13x1y2 true)
+(= i12x2y3 true)
+
#!/bin/env python
-#pylint: disable-msg=too-many-locals,invalid-name
-"""hi"""
+#pylint: disable-msg=too-many-locals,invalid-name,missing-docstring
-def generate():
- """Generates the yices code for peg solitaire"""
+if __name__ == '__main__':
pos = [(x, y) for x in range(7) for y in range(7) if
not ((x < 2 and y < 2) or # exclude topleft
(x > 4 and y > 4) or # exclude bottomright
(x > 4 and y < 2) or # exclude topright
(x < 2 and y > 4)) # exclude bottomleft
]
- ill_middles = [
- (2, 0), (4, 0), (0, 2), (0, 4), (6, 2), (6, 4), (2, 6), (4, 6)]
holes = [(3, 3)]
winning = (3, 3)
-
iterations = len(pos)-len(holes)
- posp = [p for p in pos if p not in ill_middles]
print """
(benchmark a1.smt
:logic QF_UF
print ';Iteration {}'.format(i)
print '(or'
for sx, sy in pos:
- for mx, my in posp:
+ for mx, my in pos:
if mx == sx and my == sy:
continue
for ex, ey in pos:
for x, y in pos if (x, y) != winning)
print '))'
-
-if __name__ == '__main__':
- generate()
repositories / ar1516.git / commitdiff
