added time for z4 problem 4

diff --git a/a2/4.tex b/a2/4.tex
index b1e6641..81f3cd5 100644 (file)
--- 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 (file)
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 (file)
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<i>\d+)x(?P<x>\d+)y(?P<y>\d+) (?P<v>true|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)