From: Mart Lubbers Date: Mon, 4 Jan 2016 20:08:24 +0000 (+0100) Subject: added time for z4 problem 4 X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=769aa952c5e41e0c45d71da841452f4413d79838;p=ar1516.git added time for z4 problem 4 --- diff --git a/a2/4.tex b/a2/4.tex index b1e6641..81f3cd5 100644 --- a/a2/4.tex +++ b/a2/4.tex @@ -107,8 +107,8 @@ $$\mathcal{INIT}\wedge\left(\bigwedge_{i=1}^{31}\mathcal{ITER}(i)\right) \subsection{Solution} The conversion to SMT-Lib is trivial however on a $3.8Ghz$ processor running \textsc{yices} it takes about $4$ hours and $15$ minutes to find the solution -listed in Table~\ref{tab:sol}. - +listed in Table~\ref{tab:sol}. \textsc{z3} finds a solution in $10$ minutes and +$37$ seconds. \begin{table}[h] \centering diff --git a/a2/src/4/4.smv b/a2/src/4/4.smv new file mode 100644 index 0000000..4e4c581 --- /dev/null +++ b/a2/src/4/4.smv @@ -0,0 +1,315 @@ + +MODULE main +VAR +x0y2: boolean; x0y3: boolean; x0y4: boolean; x1y2: boolean; x1y3: boolean; x1y4: boolean; x2y0: boolean; x2y1: boolean; x2y2: boolean; x2y3: boolean; x2y4: boolean; x2y5: boolean; x2y6: boolean; x3y0: boolean; x3y1: boolean; x3y2: boolean; x3y3: boolean; x3y4: boolean; x3y5: boolean; x3y6: boolean; x4y0: boolean; x4y1: boolean; x4y2: boolean; x4y3: boolean; x4y4: boolean; x4y5: boolean; x4y6: boolean; x5y2: boolean; x5y3: boolean; x5y4: boolean; x6y2: boolean; x6y3: boolean; x6y4: boolean; +INIT +x0y2=TRUE & x0y3=TRUE & x0y4=TRUE & x1y2=TRUE & x1y3=TRUE & x1y4=TRUE & x2y0=TRUE & x2y1=TRUE & x2y2=TRUE & x2y3=TRUE & x2y4=TRUE & x2y5=TRUE & x2y6=TRUE & x3y0=TRUE & x3y1=TRUE & x3y2=TRUE & x3y3=FALSE & x3y4=TRUE & x3y5=TRUE & x3y6=TRUE & x4y0=TRUE & x4y1=TRUE & x4y2=TRUE & x4y3=TRUE & x4y4=TRUE & x4y5=TRUE & x4y6=TRUE & x5y2=TRUE & x5y3=TRUE & x5y4=TRUE & x6y2=TRUE & x6y3=TRUE & x6y4=TRUE +TRANS +case +x0y2=TRUE & x0y3=TRUE & x0y4=FALSE: +(next(x0y2)=FALSE & next(x0y3)=FALSE & next(x0y4)=TRUE & +next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x0y2=TRUE & x1y2=TRUE & x2y2=FALSE: +(next(x0y2)=FALSE & next(x1y2)=FALSE & next(x2y2)=TRUE & +next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x0y3=TRUE & x1y3=TRUE & x2y3=FALSE: +(next(x0y3)=FALSE & next(x1y3)=FALSE & next(x2y3)=TRUE & +next(x0y2)=x0y2 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x0y4=TRUE & x0y3=TRUE & x0y2=FALSE: +(next(x0y4)=FALSE & next(x0y3)=FALSE & next(x0y2)=TRUE & +next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x0y4=TRUE & x1y4=TRUE & x2y4=FALSE: +(next(x0y4)=FALSE & next(x1y4)=FALSE & next(x2y4)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x1y2=TRUE & x1y3=TRUE & x1y4=FALSE: +(next(x1y2)=FALSE & next(x1y3)=FALSE & next(x1y4)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x1y2=TRUE & x2y2=TRUE & x3y2=FALSE: +(next(x1y2)=FALSE & next(x2y2)=FALSE & next(x3y2)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x1y3=TRUE & x2y3=TRUE & x3y3=FALSE: +(next(x1y3)=FALSE & next(x2y3)=FALSE & next(x3y3)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x1y4=TRUE & x1y3=TRUE & x1y2=FALSE: +(next(x1y4)=FALSE & next(x1y3)=FALSE & next(x1y2)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x1y4=TRUE & x2y4=TRUE & x3y4=FALSE: +(next(x1y4)=FALSE & next(x2y4)=FALSE & next(x3y4)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x2y0=TRUE & x2y1=TRUE & x2y2=FALSE: +(next(x2y0)=FALSE & next(x2y1)=FALSE & next(x2y2)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x2y0=TRUE & x3y0=TRUE & x4y0=FALSE: +(next(x2y0)=FALSE & next(x3y0)=FALSE & next(x4y0)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x2y1=TRUE & x2y2=TRUE & x2y3=FALSE: +(next(x2y1)=FALSE & next(x2y2)=FALSE & next(x2y3)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x2y1=TRUE & x3y1=TRUE & x4y1=FALSE: +(next(x2y1)=FALSE & next(x3y1)=FALSE & next(x4y1)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x2y2=TRUE & x1y2=TRUE & x0y2=FALSE: +(next(x2y2)=FALSE & next(x1y2)=FALSE & next(x0y2)=TRUE & +next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x2y2=TRUE & x2y1=TRUE & x2y0=FALSE: +(next(x2y2)=FALSE & next(x2y1)=FALSE & next(x2y0)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x2y2=TRUE & x2y3=TRUE & x2y4=FALSE: +(next(x2y2)=FALSE & next(x2y3)=FALSE & next(x2y4)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x2y2=TRUE & x3y2=TRUE & x4y2=FALSE: +(next(x2y2)=FALSE & next(x3y2)=FALSE & next(x4y2)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x2y3=TRUE & x1y3=TRUE & x0y3=FALSE: +(next(x2y3)=FALSE & next(x1y3)=FALSE & next(x0y3)=TRUE & +next(x0y2)=x0y2 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x2y3=TRUE & x2y2=TRUE & x2y1=FALSE: +(next(x2y3)=FALSE & next(x2y2)=FALSE & next(x2y1)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x2y3=TRUE & x2y4=TRUE & x2y5=FALSE: +(next(x2y3)=FALSE & next(x2y4)=FALSE & next(x2y5)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x2y3=TRUE & x3y3=TRUE & x4y3=FALSE: +(next(x2y3)=FALSE & next(x3y3)=FALSE & next(x4y3)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x2y4=TRUE & x1y4=TRUE & x0y4=FALSE: +(next(x2y4)=FALSE & next(x1y4)=FALSE & next(x0y4)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x2y4=TRUE & x2y3=TRUE & x2y2=FALSE: +(next(x2y4)=FALSE & next(x2y3)=FALSE & next(x2y2)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x2y4=TRUE & x2y5=TRUE & x2y6=FALSE: +(next(x2y4)=FALSE & next(x2y5)=FALSE & next(x2y6)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x2y4=TRUE & x3y4=TRUE & x4y4=FALSE: +(next(x2y4)=FALSE & next(x3y4)=FALSE & next(x4y4)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x2y5=TRUE & x2y4=TRUE & x2y3=FALSE: +(next(x2y5)=FALSE & next(x2y4)=FALSE & next(x2y3)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x2y5=TRUE & x3y5=TRUE & x4y5=FALSE: +(next(x2y5)=FALSE & next(x3y5)=FALSE & next(x4y5)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x2y6=TRUE & x2y5=TRUE & x2y4=FALSE: +(next(x2y6)=FALSE & next(x2y5)=FALSE & next(x2y4)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x2y6=TRUE & x3y6=TRUE & x4y6=FALSE: +(next(x2y6)=FALSE & next(x3y6)=FALSE & next(x4y6)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x3y0=TRUE & x3y1=TRUE & x3y2=FALSE: +(next(x3y0)=FALSE & next(x3y1)=FALSE & next(x3y2)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x3y1=TRUE & x3y2=TRUE & x3y3=FALSE: +(next(x3y1)=FALSE & next(x3y2)=FALSE & next(x3y3)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x3y2=TRUE & x2y2=TRUE & x1y2=FALSE: +(next(x3y2)=FALSE & next(x2y2)=FALSE & next(x1y2)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x3y2=TRUE & x3y1=TRUE & x3y0=FALSE: +(next(x3y2)=FALSE & next(x3y1)=FALSE & next(x3y0)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x3y2=TRUE & x3y3=TRUE & x3y4=FALSE: +(next(x3y2)=FALSE & next(x3y3)=FALSE & next(x3y4)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x3y2=TRUE & x4y2=TRUE & x5y2=FALSE: +(next(x3y2)=FALSE & next(x4y2)=FALSE & next(x5y2)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x3y3=TRUE & x2y3=TRUE & x1y3=FALSE: +(next(x3y3)=FALSE & next(x2y3)=FALSE & next(x1y3)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x3y3=TRUE & x3y2=TRUE & x3y1=FALSE: +(next(x3y3)=FALSE & next(x3y2)=FALSE & next(x3y1)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x3y3=TRUE & x3y4=TRUE & x3y5=FALSE: +(next(x3y3)=FALSE & next(x3y4)=FALSE & next(x3y5)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x3y3=TRUE & x4y3=TRUE & x5y3=FALSE: +(next(x3y3)=FALSE & next(x4y3)=FALSE & next(x5y3)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x3y4=TRUE & x2y4=TRUE & x1y4=FALSE: +(next(x3y4)=FALSE & next(x2y4)=FALSE & next(x1y4)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x3y4=TRUE & x3y3=TRUE & x3y2=FALSE: +(next(x3y4)=FALSE & next(x3y3)=FALSE & next(x3y2)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x3y4=TRUE & x3y5=TRUE & x3y6=FALSE: +(next(x3y4)=FALSE & next(x3y5)=FALSE & next(x3y6)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x3y4=TRUE & x4y4=TRUE & x5y4=FALSE: +(next(x3y4)=FALSE & next(x4y4)=FALSE & next(x5y4)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x3y5=TRUE & x3y4=TRUE & x3y3=FALSE: +(next(x3y5)=FALSE & next(x3y4)=FALSE & next(x3y3)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x3y6=TRUE & x3y5=TRUE & x3y4=FALSE: +(next(x3y6)=FALSE & next(x3y5)=FALSE & next(x3y4)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x4y0=TRUE & x3y0=TRUE & x2y0=FALSE: +(next(x4y0)=FALSE & next(x3y0)=FALSE & next(x2y0)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x4y0=TRUE & x4y1=TRUE & x4y2=FALSE: +(next(x4y0)=FALSE & next(x4y1)=FALSE & next(x4y2)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x4y1=TRUE & x3y1=TRUE & x2y1=FALSE: +(next(x4y1)=FALSE & next(x3y1)=FALSE & next(x2y1)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x4y1=TRUE & x4y2=TRUE & x4y3=FALSE: +(next(x4y1)=FALSE & next(x4y2)=FALSE & next(x4y3)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x4y2=TRUE & x3y2=TRUE & x2y2=FALSE: +(next(x4y2)=FALSE & next(x3y2)=FALSE & next(x2y2)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x4y2=TRUE & x4y1=TRUE & x4y0=FALSE: +(next(x4y2)=FALSE & next(x4y1)=FALSE & next(x4y0)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x4y2=TRUE & x4y3=TRUE & x4y4=FALSE: +(next(x4y2)=FALSE & next(x4y3)=FALSE & next(x4y4)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x4y2=TRUE & x5y2=TRUE & x6y2=FALSE: +(next(x4y2)=FALSE & next(x5y2)=FALSE & next(x6y2)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x4y3=TRUE & x3y3=TRUE & x2y3=FALSE: +(next(x4y3)=FALSE & next(x3y3)=FALSE & next(x2y3)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x4y3=TRUE & x4y2=TRUE & x4y1=FALSE: +(next(x4y3)=FALSE & next(x4y2)=FALSE & next(x4y1)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x4y3=TRUE & x4y4=TRUE & x4y5=FALSE: +(next(x4y3)=FALSE & next(x4y4)=FALSE & next(x4y5)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x4y3=TRUE & x5y3=TRUE & x6y3=FALSE: +(next(x4y3)=FALSE & next(x5y3)=FALSE & next(x6y3)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y4)=x6y4 +); +x4y4=TRUE & x3y4=TRUE & x2y4=FALSE: +(next(x4y4)=FALSE & next(x3y4)=FALSE & next(x2y4)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x4y4=TRUE & x4y3=TRUE & x4y2=FALSE: +(next(x4y4)=FALSE & next(x4y3)=FALSE & next(x4y2)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x4y4=TRUE & x4y5=TRUE & x4y6=FALSE: +(next(x4y4)=FALSE & next(x4y5)=FALSE & next(x4y6)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x4y4=TRUE & x5y4=TRUE & x6y4=FALSE: +(next(x4y4)=FALSE & next(x5y4)=FALSE & next(x6y4)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x6y2)=x6y2 & next(x6y3)=x6y3 +); +x4y5=TRUE & x3y5=TRUE & x2y5=FALSE: +(next(x4y5)=FALSE & next(x3y5)=FALSE & next(x2y5)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x4y5=TRUE & x4y4=TRUE & x4y3=FALSE: +(next(x4y5)=FALSE & next(x4y4)=FALSE & next(x4y3)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x4y6=TRUE & x3y6=TRUE & x2y6=FALSE: +(next(x4y6)=FALSE & next(x3y6)=FALSE & next(x2y6)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x4y6=TRUE & x4y5=TRUE & x4y4=FALSE: +(next(x4y6)=FALSE & next(x4y5)=FALSE & next(x4y4)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x5y2=TRUE & x4y2=TRUE & x3y2=FALSE: +(next(x5y2)=FALSE & next(x4y2)=FALSE & next(x3y2)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x5y2=TRUE & x5y3=TRUE & x5y4=FALSE: +(next(x5y2)=FALSE & next(x5y3)=FALSE & next(x5y4)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x5y3=TRUE & x4y3=TRUE & x3y3=FALSE: +(next(x5y3)=FALSE & next(x4y3)=FALSE & next(x3y3)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x5y4=TRUE & x4y4=TRUE & x3y4=FALSE: +(next(x5y4)=FALSE & next(x4y4)=FALSE & next(x3y4)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x5y4=TRUE & x5y3=TRUE & x5y2=FALSE: +(next(x5y4)=FALSE & next(x5y3)=FALSE & next(x5y2)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x6y2=TRUE & x5y2=TRUE & x4y2=FALSE: +(next(x6y2)=FALSE & next(x5y2)=FALSE & next(x4y2)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y3)=x6y3 & next(x6y4)=x6y4 +); +x6y2=TRUE & x6y3=TRUE & x6y4=FALSE: +(next(x6y2)=FALSE & next(x6y3)=FALSE & next(x6y4)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 +); +x6y3=TRUE & x5y3=TRUE & x4y3=FALSE: +(next(x6y3)=FALSE & next(x5y3)=FALSE & next(x4y3)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y4)=x6y4 +); +x6y4=TRUE & x5y4=TRUE & x4y4=FALSE: +(next(x6y4)=FALSE & next(x5y4)=FALSE & next(x4y4)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x6y2)=x6y2 & next(x6y3)=x6y3 +); +x6y4=TRUE & x6y3=TRUE & x6y2=FALSE: +(next(x6y4)=FALSE & next(x6y3)=FALSE & next(x6y2)=TRUE & +next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 +); +TRUE: (next(x0y2)=x0y2 & next(x0y3)=x0y3 & next(x0y4)=x0y4 & next(x1y2)=x1y2 & next(x1y3)=x1y3 & next(x1y4)=x1y4 & next(x2y0)=x2y0 & next(x2y1)=x2y1 & next(x2y2)=x2y2 & next(x2y3)=x2y3 & next(x2y4)=x2y4 & next(x2y5)=x2y5 & next(x2y6)=x2y6 & next(x3y0)=x3y0 & next(x3y1)=x3y1 & next(x3y2)=x3y2 & next(x3y3)=x3y3 & next(x3y4)=x3y4 & next(x3y5)=x3y5 & next(x3y6)=x3y6 & next(x4y0)=x4y0 & next(x4y1)=x4y1 & next(x4y2)=x4y2 & next(x4y3)=x4y3 & next(x4y4)=x4y4 & next(x4y5)=x4y5 & next(x4y6)=x4y6 & next(x5y2)=x5y2 & next(x5y3)=x5y3 & next(x5y4)=x5y4 & next(x6y2)=x6y2 & next(x6y3)=x6y3 & next(x6y4)=x6y4); +esac +LTLSPEC G !(x0y2=FALSE & x0y3=FALSE & x0y4=FALSE & x1y2=FALSE & x1y3=FALSE & x1y4=FALSE & x2y0=FALSE & x2y1=FALSE & x2y2=FALSE & x2y3=FALSE & x2y4=FALSE & x2y5=FALSE & x2y6=FALSE & x3y0=FALSE & x3y1=FALSE & x3y2=FALSE & x3y3=TRUE & x3y4=FALSE & x3y5=FALSE & x3y6=FALSE & x4y0=FALSE & x4y1=FALSE & x4y2=FALSE & x4y3=FALSE & x4y4=FALSE & x4y5=FALSE & x4y6=FALSE & x5y2=FALSE & x5y3=FALSE & x5y4=FALSE & x6y2=FALSE & x6y3=FALSE & x6y4=FALSE) diff --git a/a2/src/4/print4z3.py b/a2/src/4/print4z3.py new file mode 100644 index 0000000..e3eed1f --- /dev/null +++ b/a2/src/4/print4z3.py @@ -0,0 +1,88 @@ +#!/bin/env python +"""hi""" + +import sys +import re + +PAT = r'\(= i(?P\d+)x(?P\d+)y(?P\d+) (?Ptrue|false)\)' + +def print_board(previous, data, tofile): + """Prints a peg solitaire board""" + tofile.write('$\\xymatrix@=1.2pt@M=1.2pt{') + begin = None + if data is not None: + end = None + begin = [] + for yco in range(7): + for xco in range(7): + pos = [d for d in data if d[0] == xco and d[1] == yco] + poso = [d for d in previous if d[0] == xco and d[1] == yco] + if pos and poso: + if pos[0][2] and not poso[0][2]: + end = pos[0] + elif pos[0][2] != poso[0][2]: + begin.append(pos[0]) + if begin and end: + if begin[0][0] < end[0]: + direction = 'rr' + begin = min(begin, key=lambda x: x[0]) + elif begin[0][0] > end[0]: + direction = 'll' + begin = max(begin, key=lambda x: x[0]) + elif begin[0][1] < end[1]: + direction = 'dd' + begin = min(begin, key=lambda x: x[1]) + elif begin[0][1] > end[1]: + direction = 'uu' + begin = max(begin, key=lambda x: x[1]) + else: + direction = None + + for yco in range(7): + for xco in range(7): + pos = [d for d in previous if d[0] == xco and d[1] == yco] + if not pos: + tofile.write('&') + else: + tofile.write('\\circ ' if pos[0][2] else '\\times ') + if begin and pos[0][0] == begin[0] and pos[0][1] == begin[1]: + tofile.write('\\ar@{{-)}}[{}]'.format(direction)) + tofile.write('&') + tofile.write('\\\\\n') + tofile.write('}$\n') + +def parse(lines, output): + """Parse the model from yices""" + data = {} + for line in lines: + line = line.strip() + match = re.match(PAT, line) + if match: + ite = int(match.group('i')) + if ite not in data: + data[ite] = [] + data[ite].append((int(match.group('x')), int(match.group('y')), + match.group('v') == 'true')) + output.write('\\begin{tabular}{cccccc}\n') + prev = None + for i, (_, dat) in enumerate(sorted(data.items())): + if prev is None: + prev = dat + else: + print_board(prev, dat, output) + prev = dat + output.write(' & ') + if i % 5 == 0: + output.write('\\\\\\\\') + print_board(prev, None, output) + output.write('\\end{tabular}\n') + +if __name__ == '__main__': + if len(sys.argv) == 1: + parse(sys.stdin, sys.stdout) + elif len(sys.argv) == 2: + with open(sys.argv[1], 'r') as fin: + parse(fin, sys.stdout) + else: + with open(sys.argv[1], 'r') as fin, open(sys.argv[2], 'w') as fout: + parse(fin, fout)