final model a4

diff --git a/a2/4.tex b/a2/4.tex
index cfec0ab..1147320 100644 (file)
--- a/a2/4.tex
+++ b/a2/4.tex
@@ -24,19 +24,19 @@ end condition more flexible by allowing the last peg anywhere on the board.
        $$\xymatrix@1@=1pt@M=1pt{
                & 0 & 1 & 2 & 3 & 4 & 5 & 6\\
                0 & & & \circ & \circ & \circ & & & & & & 
-                       \circ\ar@/^/[rr] & \circ & \times & \rightarrow &
+                       \circ\ar@{-)}[rr] & \circ & \times & \rightarrow &
                                \times & \times & \circ\\
                1 & & & \circ & \circ & \circ\\
                2 & \circ & \circ & \circ & \circ & \circ & \circ & \circ & & & &
-                       \times & \circ & \circ\ar@/_/[ll]& \rightarrow &
+                       \times & \circ & \circ\ar@{-)}[ll]& \rightarrow &
                                \circ & \times & \times\\
                3 & \circ & \circ & \circ & \times & \circ & \circ & \circ\\
                4 & \circ & \circ & \circ & \circ & \circ & \circ & \circ & & & &
-                       \circ\ar@/_/[dd] & & \times & & \times & & \circ\\
+                       \circ\ar@{-)}[dd] & & \times & & \times & & \circ\\
                5 & & & \circ & \circ & \circ & & & & & & 
                        \circ & \rightarrow & \times & & \circ & \rightarrow& \times\\
                6 & & & \circ & \circ & \circ & & & & & & 
-                       \times & & \circ & & \circ\ar@/^/[uu] & & \times\\
+                       \times & & \circ & & \circ\ar@{-)}[uu] & & \times\\
        }$$
        \caption{Initial board state and possible moves}\label{fig:init}
 \end{figure}
@@ -106,4 +106,7 @@ $$\mathcal{INIT}\wedge\left(\bigwedge_{i=1}^{31}\mathcal{ITER}(i)\right)
 \wedge\mathcal{POST}$$
 
 \subsection{Solution}
-The conversion to SMT-Lib is trivial 
+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 a solution.
+
+\input{src/4/a4.tex}

diff --git a/a2/src/4/1.tex b/a2/src/4/1.tex
new file mode 100644 (file)
index 0000000..e69de29

diff --git a/a2/src/4/4.model b/a2/src/4/4.model
index e69de29..3b52ae7 100644 (file)
--- a/a2/src/4/4.model
+++ b/a2/src/4/4.model
@@ -0,0 +1,1059 @@
+sat
+
+(= i1x2y0 true)
+(= i4x2y1 false)
+(= i1x2y3 true)
+(= i11x2y5 false)
+(= i31x6y2 false)
+(= i26x0y3 true)
+(= i10x3y6 true)
+(= i13x3y5 true)
+(= i20x0y4 false)
+(= i30x2y2 false)
+(= i6x2y3 true)
+(= i6x5y3 true)
+(= i0x4y0 true)
+(= i17x2y0 false)
+(= i20x3y1 false)
+(= i24x5y4 false)
+(= i16x4y6 false)
+(= i26x0y4 false)
+(= i26x2y5 false)
+(= i14x2y6 false)
+(= i29x1y4 true)
+(= i1x0y4 true)
+(= i21x3y3 false)
+(= i31x4y2 false)
+(= i18x6y3 false)
+(= i3x1y2 true)
+(= i4x3y6 true)
+(= i9x1y3 true)
+(= i16x6y4 false)
+(= i18x6y4 false)
+(= i19x1y4 true)
+(= i14x3y0 false)
+(= i9x3y3 false)
+(= i3x5y4 true)
+(= i21x4y5 false)
+(= i14x4y5 false)
+(= i30x5y2 false)
+(= i22x4y6 false)
+(= i6x0y3 true)
+(= i18x2y5 false)
+(= i27x1y2 false)
+(= i26x2y1 false)
+(= i24x4y6 false)
+(= i31x4y4 false)
+(= i19x5y3 false)
+(= i15x1y4 false)
+(= i9x3y6 true)
+(= i0x3y1 true)
+(= i14x6y2 false)
+(= i28x0y3 false)
+(= i0x6y2 true)
+(= i9x5y3 true)
+(= i13x0y4 true)
+(= i11x1y3 true)
+(= i7x3y3 false)
+(= i21x2y4 false)
+(= i15x5y4 false)
+(= i27x4y2 false)
+(= i6x0y2 true)
+(= i14x3y4 false)
+(= i9x0y4 true)
+(= i20x6y4 false)
+(= i7x1y4 true)
+(= i21x1y2 true)
+(= i24x4y5 false)
+(= i30x4y5 false)
+(= i31x1y4 false)
+(= i8x4y1 false)
+(= i1x3y5 true)
+(= i3x2y6 true)
+(= i13x1y4 true)
+(= i2x6y2 true)
+(= i9x4y1 false)
+(= i29x0y2 false)
+(= i15x0y4 false)
+(= i28x5y2 false)
+(= i24x3y6 false)
+(= i18x3y1 false)
+(= i19x4y6 false)
+(= i22x3y1 false)
+(= i19x4y1 false)
+(= i13x2y0 false)
+(= i27x3y3 false)
+(= i12x3y5 true)
+(= i16x2y0 false)
+(= i10x4y0 false)
+(= i27x2y0 false)
+(= i11x3y4 true)
+(= i9x3y0 true)
+(= i2x3y6 true)
+(= i12x6y2 true)
+(= i18x2y6 true)
+(= i23x3y4 false)
+(= i13x0y2 true)
+(= i31x2y4 false)
+(= i13x3y6 true)
+(= i2x0y4 true)
+(= i8x4y6 true)
+(= i17x5y4 true)
+(= i18x3y2 true)
+(= i6x1y2 true)
+(= i16x1y3 true)
+(= i18x3y3 false)
+(= i27x0y4 false)
+(= i6x2y5 true)
+(= i24x3y0 false)
+(= i9x3y1 false)
+(= i11x5y4 true)
+(= i3x2y3 true)
+(= i15x0y2 true)
+(= i27x3y2 false)
+(= i12x6y3 true)
+(= i5x0y2 true)
+(= i29x0y3 false)
+(= i30x4y6 false)
+(= i13x3y3 false)
+(= i28x4y5 false)
+(= i31x4y3 false)
+(= i2x4y5 true)
+(= i8x6y4 false)
+(= i13x3y1 false)
+(= i10x4y1 false)
+(= i17x2y1 false)
+(= i26x3y2 false)
+(= i30x4y0 false)
+(= i19x6y3 false)
+(= i24x2y1 false)
+(= i12x1y4 true)
+(= i29x3y6 false)
+(= i23x0y3 true)
+(= i6x4y3 true)
+(= i15x3y5 true)
+(= i23x0y4 false)
+(= i29x6y2 false)
+(= i21x4y4 false)
+(= i14x4y3 true)
+(= i29x3y0 false)
+(= i24x6y3 false)
+(= i25x3y3 false)
+(= i5x2y2 true)
+(= i30x5y4 false)
+(= i16x0y4 false)
+(= i2x5y3 false)
+(= i3x1y3 true)
+(= i12x2y0 false)
+(= i16x2y5 false)
+(= i25x2y6 true)
+(= i7x0y3 true)
+(= i10x3y2 true)
+(= i12x3y1 false)
+(= i26x6y3 false)
+(= i27x6y3 false)
+(= i6x1y4 true)
+(= i20x3y3 false)
+(= i27x6y4 false)
+(= i29x2y6 false)
+(= i3x6y3 true)
+(= i24x6y2 false)
+(= i1x5y4 true)
+(= i27x5y4 false)
+(= i10x2y4 true)
+(= i30x3y6 false)
+(= i26x2y3 false)
+(= i14x2y3 true)
+(= i28x3y5 true)
+(= i5x0y4 true)
+(= i24x1y2 true)
+(= i2x1y3 true)
+(= i4x1y3 true)
+(= i7x3y0 true)
+(= i15x3y4 false)
+(= i25x2y5 false)
+(= i12x3y2 true)
+(= i22x6y4 false)
+(= i14x4y6 true)
+(= i14x2y1 false)
+(= i22x4y1 false)
+(= i24x0y4 false)
+(= i26x3y5 true)
+(= i4x1y4 true)
+(= i23x5y2 false)
+(= i30x2y6 false)
+(= i16x4y4 true)
+(= i25x2y2 true)
+(= i0x4y3 true)
+(= i6x4y5 false)
+(= i20x3y2 true)
+(= i30x6y3 false)
+(= i20x2y0 false)
+(= i29x3y5 true)
+(= i12x4y3 true)
+(= i22x2y5 false)
+(= i12x5y3 true)
+(= i28x3y3 false)
+(= i23x4y1 false)
+(= i24x5y3 false)
+(= i20x3y5 true)
+(= i8x2y0 true)
+(= i17x3y0 false)
+(= i9x6y4 false)
+(= i2x4y6 true)
+(= i29x0y4 false)
+(= i13x0y3 true)
+(= i8x2y2 true)
+(= i14x2y5 false)
+(= i17x2y3 true)
+(= i11x3y0 false)
+(= i24x4y1 false)
+(= i14x4y0 true)
+(= i27x4y4 false)
+(= i4x5y4 true)
+(= i23x3y3 false)
+(= i9x1y2 true)
+(= i3x6y2 true)
+(= i30x0y2 false)
+(= i3x2y1 false)
+(= i11x4y4 false)
+(= i6x2y2 true)
+(= i15x2y4 true)
+(= i23x4y4 false)
+(= i26x1y3 true)
+(= i4x0y3 true)
+(= i28x0y4 false)
+(= i29x6y3 false)
+(= i2x4y0 true)
+(= i0x3y0 true)
+(= i14x3y3 false)
+(= i30x4y1 false)
+(= i11x6y4 false)
+(= i0x3y6 true)
+(= i12x1y3 true)
+(= i8x1y3 true)
+(= i28x2y2 false)
+(= i4x2y5 true)
+(= i26x1y4 true)
+(= i6x4y6 true)
+(= i21x0y3 true)
+(= i21x4y3 false)
+(= i26x4y0 false)
+(= i24x3y3 false)
+(= i18x4y1 false)
+(= i21x3y0 false)
+(= i25x2y1 false)
+(= i26x3y6 false)
+(= i27x1y4 true)
+(= i27x4y5 false)
+(= i28x2y6 true)
+(= i27x3y6 false)
+(= i19x2y6 true)
+(= i1x2y1 true)
+(= i0x0y3 true)
+(= i25x4y6 false)
+(= i4x1y2 true)
+(= i0x2y0 true)
+(= i17x6y3 false)
+(= i11x5y2 true)
+(= i7x6y3 true)
+(= i12x3y3 false)
+(= i9x0y2 true)
+(= i21x2y2 false)
+(= i4x2y3 true)
+(= i16x3y1 false)
+(= i21x3y1 false)
+(= i24x4y2 false)
+(= i4x0y4 true)
+(= i7x3y5 true)
+(= i11x4y3 true)
+(= i9x2y3 true)
+(= i20x2y6 true)
+(= i18x4y5 false)
+(= i2x0y2 true)
+(= i13x4y0 true)
+(= i25x3y6 false)
+(= i27x3y5 true)
+(= i4x3y3 true)
+(= i31x4y5 false)
+(= i10x0y2 true)
+(= i20x2y5 false)
+(= i9x4y6 true)
+(= i1x3y1 true)
+(= i28x1y2 false)
+(= i28x6y2 false)
+(= i20x6y2 false)
+(= i5x2y5 true)
+(= i1x0y2 true)
+(= i1x4y5 true)
+(= i1x1y3 true)
+(= i6x0y4 true)
+(= i14x5y2 true)
+(= i9x6y2 true)
+(= i19x0y3 true)
+(= i21x3y2 true)
+(= i26x4y2 false)
+(= i24x1y3 true)
+(= i20x4y1 false)
+(= i5x3y6 true)
+(= i23x1y4 true)
+(= i1x6y2 true)
+(= i23x5y3 false)
+(= i12x2y1 false)
+(= i2x0y3 true)
+(= i18x4y6 false)
+(= i7x4y0 false)
+(= i1x1y2 true)
+(= i0x2y1 true)
+(= i1x5y3 false)
+(= i1x3y0 true)
+(= i8x4y0 false)
+(= i10x5y4 true)
+(= i4x0y2 true)
+(= i26x3y3 false)
+(= i0x4y6 true)
+(= i7x6y2 true)
+(= i17x1y3 true)
+(= i13x4y4 false)
+(= i3x4y1 true)
+(= i5x3y4 true)
+(= i21x3y5 true)
+(= i28x4y0 false)
+(= i22x3y5 true)
+(= i14x3y6 true)
+(= i2x3y5 true)
+(= i29x4y6 false)
+(= i12x2y2 true)
+(= i30x3y3 false)
+(= i17x5y2 false)
+(= i4x3y5 true)
+(= i11x3y3 false)
+(= i30x3y5 true)
+(= i14x5y4 true)
+(= i8x5y2 true)
+(= i25x4y0 false)
+(= i9x4y4 false)
+(= i4x3y0 true)
+(= i3x4y3 true)
+(= i11x2y6 false)
+(= i18x3y5 true)
+(= i12x4y0 true)
+(= i11x3y5 true)
+(= i28x4y3 false)
+(= i14x3y2 true)
+(= i16x5y3 true)
+(= i6x5y4 true)
+(= i2x3y4 true)
+(= i19x5y4 false)
+(= i1x6y4 true)
+(= i15x5y2 true)
+(= i1x3y4 true)
+(= i3x2y5 true)
+(= i20x5y4 false)
+(= i23x0y2 true)
+(= i23x2y5 false)
+(= i3x4y6 true)
+(= i6x4y4 false)
+(= i7x2y1 false)
+(= i26x4y5 false)
+(= i25x4y1 false)
+(= i10x2y2 true)
+(= i23x2y1 true)
+(= i9x6y3 true)
+(= i8x3y1 false)
+(= i13x1y3 true)
+(= i14x2y0 false)
+(= i7x4y5 false)
+(= i15x1y2 true)
+(= i21x2y1 true)
+(= i1x2y6 true)
+(= i17x2y6 true)
+(= i12x1y2 true)
+(= i22x1y2 true)
+(= i12x5y4 true)
+(= i1x6y3 true)
+(= i25x2y4 false)
+(= i25x4y5 false)
+(= i7x3y4 true)
+(= i10x3y1 false)
+(= i25x4y2 false)
+(= i18x0y4 false)
+(= i26x5y3 false)
+(= i11x2y4 true)
+(= i10x2y1 false)
+(= i18x2y3 true)
+(= i24x2y4 false)
+(= i29x2y5 false)
+(= i28x2y5 true)
+(= i11x4y2 true)
+(= i7x3y2 true)
+(= i16x4y5 false)
+(= i27x0y3 false)
+(= i16x6y3 false)
+(= i19x3y2 true)
+(= i20x5y2 false)
+(= i12x3y6 true)
+(= i22x3y6 false)
+(= i27x2y1 false)
+(= i13x3y4 false)
+(= i24x3y1 false)
+(= i10x6y2 true)
+(= i0x3y5 true)
+(= i21x5y4 false)
+(= i17x0y4 false)
+(= i7x0y4 true)
+(= i8x6y2 true)
+(= i10x1y3 true)
+(= i11x3y2 true)
+(= i24x4y3 false)
+(= i13x4y5 false)
+(= i13x6y2 false)
+(= i25x5y3 false)
+(= i13x5y2 true)
+(= i13x6y4 true)
+(= i15x2y2 true)
+(= i31x2y6 false)
+(= i25x1y2 false)
+(= i18x0y3 true)
+(= i29x2y4 true)
+(= i0x2y5 true)
+(= i15x4y5 false)
+(= i16x2y1 false)
+(= i29x4y2 false)
+(= i30x3y1 false)
+(= i28x5y3 false)
+(= i13x4y1 false)
+(= i13x4y3 true)
+(= i22x5y2 false)
+(= i14x0y3 true)
+(= i20x6y3 false)
+(= i7x2y2 true)
+(= i22x2y6 true)
+(= i18x4y2 true)
+(= i10x4y3 true)
+(= i24x3y2 false)
+(= i16x4y2 true)
+(= i20x4y5 false)
+(= i24x2y6 true)
+(= i17x0y3 true)
+(= i26x2y2 false)
+(= i31x3y2 false)
+(= i23x2y4 false)
+(= i18x0y2 true)
+(= i24x2y0 false)
+(= i5x2y6 true)
+(= i25x1y4 true)
+(= i29x3y3 false)
+(= i13x5y3 true)
+(= i17x1y2 true)
+(= i27x2y5 false)
+(= i22x5y4 false)
+(= i8x2y6 true)
+(= i30x2y5 false)
+(= i6x6y2 true)
+(= i28x4y6 false)
+(= i3x6y4 true)
+(= i29x2y2 false)
+(= i22x5y3 false)
+(= i26x3y4 false)
+(= i11x0y2 true)
+(= i6x3y2 true)
+(= i11x2y2 true)
+(= i0x3y3 false)
+(= i1x4y1 true)
+(= i11x4y0 true)
+(= i12x0y4 true)
+(= i10x2y6 false)
+(= i28x6y4 false)
+(= i17x3y3 false)
+(= i20x2y4 false)
+(= i4x4y5 true)
+(= i5x1y3 true)
+(= i0x2y4 true)
+(= i15x2y1 false)
+(= i26x5y2 false)
+(= i25x3y4 false)
+(= i3x1y4 true)
+(= i26x3y1 false)
+(= i8x6y3 true)
+(= i19x0y2 true)
+(= i11x4y1 false)
+(= i19x3y4 false)
+(= i28x4y2 false)
+(= i2x5y4 true)
+(= i23x6y3 false)
+(= i21x4y6 false)
+(= i10x4y2 true)
+(= i26x3y0 false)
+(= i6x3y4 true)
+(= i25x3y5 true)
+(= i17x4y0 true)
+(= i27x2y3 true)
+(= i29x5y2 false)
+(= i12x2y4 false)
+(= i0x2y3 true)
+(= i24x4y0 false)
+(= i13x4y6 true)
+(= i31x2y5 false)
+(= i30x2y3 false)
+(= i4x4y3 true)
+(= i14x5y3 true)
+(= i7x3y1 false)
+(= i17x4y2 true)
+(= i22x2y1 true)
+(= i0x0y2 true)
+(= i11x4y6 true)
+(= i7x0y2 true)
+(= i4x2y6 true)
+(= i22x3y0 false)
+(= i9x4y0 false)
+(= i23x6y2 false)
+(= i9x2y0 true)
+(= i16x6y2 false)
+(= i15x2y0 false)
+(= i29x2y0 false)
+(= i2x3y1 true)
+(= i5x4y3 false)
+(= i3x3y5 true)
+(= i9x2y5 true)
+(= i27x6y2 false)
+(= i22x6y3 false)
+(= i1x1y4 true)
+(= i23x1y3 true)
+(= i5x5y3 true)
+(= i17x4y5 false)
+(= i17x0y2 true)
+(= i18x3y0 false)
+(= i6x4y2 true)
+(= i24x0y2 true)
+(= i0x2y2 true)
+(= i7x3y6 true)
+(= i20x2y3 false)
+(= i31x5y2 false)
+(= i22x3y4 false)
+(= i1x2y4 true)
+(= i16x4y0 true)
+(= i19x6y4 false)
+(= i8x4y4 false)
+(= i19x3y0 false)
+(= i30x6y4 false)
+(= i22x0y3 true)
+(= i4x4y1 false)
+(= i29x3y2 false)
+(= i8x5y4 true)
+(= i5x1y4 true)
+(= i29x1y3 false)
+(= i7x2y5 true)
+(= i10x0y4 true)
+(= i5x2y1 false)
+(= i8x1y4 true)
+(= i13x2y6 false)
+(= i14x2y4 true)
+(= i22x3y2 true)
+(= i22x4y3 false)
+(= i8x4y5 false)
+(= i24x2y3 true)
+(= i7x4y3 true)
+(= i7x4y4 true)
+(= i5x3y3 false)
+(= i28x4y4 false)
+(= i3x5y2 true)
+(= i30x0y3 false)
+(= i10x1y2 true)
+(= i8x5y3 true)
+(= i0x4y4 true)
+(= i3x4y0 true)
+(= i31x2y3 false)
+(= i18x4y4 false)
+(= i6x2y6 true)
+(= i28x3y4 false)
+(= i16x3y5 true)
+(= i19x3y1 false)
+(= i22x3y3 false)
+(= i24x2y2 false)
+(= i24x3y5 true)
+(= i5x4y0 false)
+(= i12x4y1 false)
+(= i17x2y2 true)
+(= i28x2y1 false)
+(= i16x2y4 true)
+(= i24x4y4 false)
+(= i6x6y3 true)
+(= i8x2y3 true)
+(= i3x3y4 true)
+(= i22x4y4 false)
+(= i1x2y2 true)
+(= i5x0y3 true)
+(= i8x4y3 true)
+(= i20x1y3 true)
+(= i21x6y3 false)
+(= i5x4y1 false)
+(= i8x0y2 true)
+(= i19x2y1 false)
+(= i21x4y0 true)
+(= i23x5y4 false)
+(= i15x0y3 true)
+(= i10x1y4 false)
+(= i29x6y4 false)
+(= i5x3y0 true)
+(= i13x4y2 true)
+(= i27x0y2 false)
+(= i17x4y3 true)
+(= i26x4y6 false)
+(= i10x5y3 true)
+(= i29x5y4 false)
+(= i18x4y3 true)
+(= i4x2y4 true)
+(= i1x4y0 true)
+(= i10x2y5 false)
+(= i25x0y4 false)
+(= i5x4y2 true)
+(= i30x4y3 false)
+(= i2x2y4 true)
+(= i25x3y1 false)
+(= i3x3y1 false)
+(= i12x3y4 false)
+(= i15x3y1 false)
+(= i2x1y2 true)
+(= i22x4y5 false)
+(= i17x4y4 true)
+(= i6x4y0 false)
+(= i17x6y2 false)
+(= i18x6y2 false)
+(= i5x3y2 true)
+(= i7x2y6 true)
+(= i21x6y4 false)
+(= i25x6y2 false)
+(= i2x4y2 false)
+(= i31x5y4 false)
+(= i3x3y3 true)
+(= i14x4y2 true)
+(= i19x6y2 false)
+(= i25x5y4 false)
+(= i19x3y5 true)
+(= i5x3y5 true)
+(= i7x2y4 true)
+(= i15x1y3 true)
+(= i16x4y1 false)
+(= i3x0y4 true)
+(= i8x2y5 true)
+(= i13x3y2 true)
+(= i25x0y3 true)
+(= i5x5y4 true)
+(= i13x2y3 true)
+(= i20x4y0 true)
+(= i4x6y2 true)
+(= i21x3y6 false)
+(= i22x1y3 true)
+(= i1x0y3 true)
+(= i1x4y3 false)
+(= i8x3y5 true)
+(= i25x2y0 false)
+(= i13x2y5 false)
+(= i4x6y4 true)
+(= i4x4y4 true)
+(= i20x2y2 false)
+(= i21x4y2 false)
+(= i4x2y2 true)
+(= i31x5y3 false)
+(= i15x4y2 true)
+(= i28x1y3 false)
+(= i25x5y2 false)
+(= i7x1y3 true)
+(= i13x3y0 false)
+(= i16x3y4 false)
+(= i23x3y5 true)
+(= i0x3y2 true)
+(= i15x3y3 false)
+(= i1x4y6 true)
+(= i2x3y3 true)
+(= i19x4y5 false)
+(= i7x5y3 true)
+(= i6x3y6 true)
+(= i19x4y0 true)
+(= i4x3y1 false)
+(= i16x1y4 false)
+(= i27x3y0 false)
+(= i13x6y3 false)
+(= i17x3y5 true)
+(= i6x6y4 true)
+(= i0x1y4 true)
+(= i23x4y6 false)
+(= i23x4y2 false)
+(= i16x0y3 true)
+(= i17x6y4 false)
+(= i29x4y0 false)
+(= i31x3y1 false)
+(= i13x2y2 true)
+(= i15x4y3 true)
+(= i18x1y3 true)
+(= i12x0y3 true)
+(= i15x4y4 true)
+(= i31x3y0 false)
+(= i11x2y3 true)
+(= i3x3y2 true)
+(= i15x2y3 true)
+(= i27x4y3 false)
+(= i27x5y3 false)
+(= i22x1y4 true)
+(= i19x2y2 true)
+(= i31x2y1 false)
+(= i21x0y4 false)
+(= i18x1y4 false)
+(= i10x3y0 true)
+(= i18x4y0 true)
+(= i3x2y2 true)
+(= i5x2y0 true)
+(= i10x0y3 true)
+(= i9x5y2 true)
+(= i0x5y3 true)
+(= i15x3y6 true)
+(= i18x1y2 true)
+(= i31x3y4 false)
+(= i19x3y3 false)
+(= i30x3y0 false)
+(= i27x4y1 false)
+(= i9x5y4 true)
+(= i4x2y0 true)
+(= i26x2y0 false)
+(= i3x2y4 true)
+(= i30x2y1 false)
+(= i22x0y4 false)
+(= i3x0y2 true)
+(= i15x4y1 false)
+(= i9x1y4 false)
+(= i26x4y3 false)
+(= i6x3y3 false)
+(= i8x2y1 false)
+(= i17x2y4 true)
+(= i19x2y3 true)
+(= i22x2y4 false)
+(= i31x3y6 false)
+(= i7x2y3 true)
+(= i29x4y4 false)
+(= i0x5y4 true)
+(= i21x2y3 false)
+(= i30x4y2 false)
+(= i4x5y2 true)
+(= i11x1y2 true)
+(= i22x2y3 false)
+(= i3x3y0 true)
+(= i17x3y1 false)
+(= i6x3y5 true)
+(= i26x4y1 false)
+(= i3x4y4 true)
+(= i29x3y4 false)
+(= i25x4y4 false)
+(= i4x4y0 false)
+(= i14x4y1 false)
+(= i19x3y6 false)
+(= i8x0y4 true)
+(= i23x4y3 false)
+(= i21x0y2 true)
+(= i6x5y2 true)
+(= i25x3y2 false)
+(= i16x2y6 true)
+(= i6x4y1 false)
+(= i14x1y3 true)
+(= i29x3y1 false)
+(= i0x1y3 true)
+(= i13x2y4 false)
+(= i18x3y4 true)
+(= i0x2y6 true)
+(= i2x3y2 true)
+(= i28x4y1 false)
+(= i2x1y4 true)
+(= i0x4y2 true)
+(= i28x3y6 false)
+(= i6x1y3 true)
+(= i18x2y2 true)
+(= i29x4y3 false)
+(= i30x0y4 false)
+(= i2x2y3 true)
+(= i15x2y5 false)
+(= i8x3y6 true)
+(= i19x2y4 false)
+(= i20x4y4 false)
+(= i3x2y0 true)
+(= i28x1y4 true)
+(= i22x2y2 false)
+(= i6x2y4 true)
+(= i31x3y5 false)
+(= i5x2y3 true)
+(= i13x2y1 false)
+(= i16x1y2 true)
+(= i1x4y4 true)
+(= i15x3y0 false)
+(= i20x4y3 true)
+(= i21x2y5 false)
+(= i25x4y3 false)
+(= i7x1y2 true)
+(= i24x6y4 false)
+(= i9x3y4 true)
+(= i19x4y3 true)
+(= i9x4y2 true)
+(= i5x5y2 true)
+(= i23x2y2 true)
+(= i26x4y4 false)
+(= i4x4y6 true)
+(= i28x3y0 false)
+(= i14x2y2 true)
+(= i5x4y6 true)
+(= i21x5y3 false)
+(= i5x4y4 true)
+(= i5x1y2 true)
+(= i5x6y3 true)
+(= i5x4y5 true)
+(= i19x2y0 false)
+(= i15x4y0 true)
+(= i16x3y3 false)
+(= i11x2y0 false)
+(= i9x4y5 false)
+(= i2x4y1 false)
+(= i8x2y4 true)
+(= i9x3y2 true)
+(= i16x3y0 false)
+(= i19x2y5 false)
+(= i30x1y2 false)
+(= i18x2y4 true)
+(= i30x2y0 false)
+(= i1x3y6 true)
+(= i10x6y4 false)
+(= i17x2y5 false)
+(= i28x5y4 false)
+(= i12x4y2 true)
+(= i14x1y4 false)
+(= i29x4y5 false)
+(= i1x2y5 true)
+(= i2x4y3 true)
+(= i7x4y1 false)
+(= i1x4y2 true)
+(= i24x0y3 true)
+(= i10x4y4 false)
+(= i6x2y1 false)
+(= i7x5y2 true)
+(= i8x1y2 true)
+(= i8x4y2 true)
+(= i10x6y3 true)
+(= i14x6y4 true)
+(= i10x2y0 true)
+(= i23x4y0 false)
+(= i28x3y1 false)
+(= i10x4y5 false)
+(= i31x6y4 false)
+(= i19x1y2 true)
+(= i7x4y2 true)
+(= i16x5y2 true)
+(= i24x2y5 false)
+(= i24x3y4 false)
+(= i2x2y1 true)
+(= i15x2y6 false)
+(= i2x5y2 true)
+(= i23x2y6 true)
+(= i30x5y3 false)
+(= i3x4y5 true)
+(= i10x3y5 true)
+(= i27x1y3 false)
+(= i26x2y6 true)
+(= i20x4y2 true)
+(= i2x2y2 true)
+(= i22x0y2 true)
+(= i19x0y4 false)
+(= i9x3y5 true)
+(= i24x1y4 true)
+(= i21x5y2 false)
+(= i5x3y1 false)
+(= i20x4y6 false)
+(= i30x6y2 false)
+(= i18x2y0 false)
+(= i31x4y6 false)
+(= i17x4y6 false)
+(= i27x2y4 true)
+(= i2x6y4 true)
+(= i26x0y2 false)
+(= i30x1y3 false)
+(= i14x3y5 true)
+(= i28x2y3 false)
+(= i31x0y2 false)
+(= i28x2y4 false)
+(= i12x2y6 false)
+(= i4x3y4 true)
+(= i31x2y2 false)
+(= i7x6y4 false)
+(= i8x3y2 true)
+(= i11x6y2 true)
+(= i17x4y1 false)
+(= i29x1y2 false)
+(= i12x4y5 false)
+(= i27x4y6 false)
+(= i22x4y0 false)
+(= i2x2y0 true)
+(= i9x2y4 false)
+(= i3x3y6 true)
+(= i11x3y6 true)
+(= i11x6y3 true)
+(= i9x2y1 false)
+(= i12x2y5 false)
+(= i23x4y5 false)
+(= i27x5y2 false)
+(= i23x3y6 false)
+(= i31x4y0 false)
+(= i8x0y3 true)
+(= i23x2y0 false)
+(= i28x0y2 false)
+(= i20x1y4 true)
+(= i0x4y5 true)
+(= i6x3y1 false)
+(= i12x5y2 true)
+(= i12x4y6 true)
+(= i18x3y6 false)
+(= i3x4y2 false)
+(= i2x6y3 true)
+(= i5x6y4 true)
+(= i21x6y2 false)
+(= i1x3y3 true)
+(= i16x0y2 true)
+(= i11x4y5 false)
+(= i26x6y4 false)
+(= i31x0y4 false)
+(= i20x5y3 false)
+(= i25x0y2 false)
+(= i31x0y3 false)
+(= i10x3y3 false)
+(= i10x2y3 true)
+(= i27x2y6 true)
+(= i11x5y3 true)
+(= i2x4y4 true)
+(= i16x3y2 true)
+(= i19x5y2 false)
+(= i1x3y2 true)
+(= i21x3y4 false)
+(= i10x3y4 true)
+(= i21x2y6 true)
+(= i30x2y4 false)
+(= i28x6y3 false)
+(= i27x3y1 false)
+(= i12x4y4 false)
+(= i22x2y0 false)
+(= i15x6y2 false)
+(= i29x2y1 false)
+(= i6x3y0 true)
+(= i11x2y1 false)
+(= i23x2y3 false)
+(= i10x4y6 true)
+(= i18x2y1 false)
+(= i10x5y2 true)
+(= i16x2y2 true)
+(= i2x2y5 true)
+(= i7x4y6 true)
+(= i25x3y0 false)
+(= i17x3y2 true)
+(= i31x1y2 false)
+(= i22x4y2 true)
+(= i26x5y4 false)
+(= i24x5y2 false)
+(= i0x6y4 true)
+(= i17x3y4 false)
+(= i29x2y3 false)
+(= i21x1y3 true)
+(= i23x1y2 true)
+(= i21x1y4 true)
+(= i5x2y4 true)
+(= i25x6y3 false)
+(= i11x1y4 false)
+(= i20x0y3 true)
+(= i16x5y4 false)
+(= i28x2y0 false)
+(= i5x6y2 true)
+(= i15x5y3 true)
+(= i31x6y3 false)
+(= i1x5y2 true)
+(= i17x3y6 false)
+(= i18x5y4 false)
+(= i13x5y4 true)
+(= i16x4y3 true)
+(= i6x2y0 true)
+(= i25x2y3 true)
+(= i19x4y4 false)
+(= i3x0y3 true)
+(= i30x3y4 true)
+(= i4x4y2 true)
+(= i18x5y2 false)
+(= i21x2y0 false)
+(= i29x5y3 false)
+(= i11x0y4 true)
+(= i31x3y3 true)
+(= i7x2y0 true)
+(= i20x2y1 true)
+(= i0x5y2 true)
+(= i14x0y2 true)
+(= i19x1y3 true)
+(= i11x0y3 true)
+(= i20x1y2 true)
+(= i25x1y3 true)
+(= i30x3y2 false)
+(= i16x3y6 false)
+(= i4x6y3 true)
+(= i8x3y4 false)
+(= i31x2y0 false)
+(= i20x3y0 false)
+(= i29x4y1 false)
+(= i0x4y1 true)
+(= i14x4y4 false)
+(= i0x1y2 true)
+(= i2x2y6 true)
+(= i26x2y4 true)
+(= i23x3y0 false)
+(= i14x6y3 false)
+(= i16x2y3 true)
+(= i19x4y2 true)
+(= i31x4y1 false)
+(= i20x3y4 false)
+(= i31x1y3 false)
+(= i22x6y2 false)
+(= i25x6y4 false)
+(= i17x1y4 false)
+(= i30x4y4 false)
+(= i9x0y3 true)
+(= i0x3y4 true)
+(= i20x0y2 true)
+(= i23x3y1 false)
+(= i3x5y3 false)
+(= i26x1y2 false)
+(= i11x3y1 false)
+(= i9x2y6 true)
+(= i14x0y4 false)
+(= i14x1y2 true)
+(= i20x3y6 false)
+(= i14x3y1 false)
+(= i9x4y3 true)
+(= i27x3y4 false)
+(= i27x2y2 false)
+(= i15x6y4 false)
+(= i12x3y0 false)
+(= i12x6y4 false)
+(= i26x6y2 false)
+(= i17x5y3 false)
+(= i23x3y2 false)
+(= i12x0y2 true)
+(= i18x5y3 false)
+(= i8x3y3 false)
+(= i2x3y0 true)
+(= i15x6y3 false)
+(= i0x0y4 true)
+(= i23x6y4 false)
+(= i4x3y2 true)
+(= i4x5y3 false)
+(= i9x2y2 true)
+(= i30x1y4 false)
+(= i28x3y2 false)
+(= i0x6y3 true)
+(= i7x5y4 false)
+(= i21x4y1 true)
+(= i8x3y0 true)
+(= i15x3y2 true)
+(= i27x4y0 false)
+(= i15x4y6 true)
+(= i13x1y2 true)
+(= i12x2y3 true)
+

diff --git a/a2/src/4/a4.tex b/a2/src/4/a4.tex
index 5ea01b1..b21ec5f 100644 (file)
--- a/a2/src/4/a4.tex
+++ b/a2/src/4/a4.tex
@@ -1,31 +1,258 @@
-  ...      ...      ...      ...      ..o      ..o      ..o      ..o   
-  ...      ...      ..o      oo.      ooo      ooo      ooo      ooo   
-.......  .......  ....o..  ....o..  .......  .......  .......  ....... 
-...o...  ....oo.  .....o.  .....o.  .....o.  ...oo..  ...o...  ...o... 
-.......  .......  .......  .......  .......  .......  ....o..  .....oo 
-  ...      ...      ...      ...      ...      ...      ..o      ..o   
-  ...      ...      ...      ...      ...      ...      ...      ...   
-
-  ..o      ..o      ..o      oo.      oo.      oo.      oo.      oo.   
-  ooo      ooo      ooo      ooo      ooo      ooo      ooo      ooo   
-.......  .......  .......  .......  .......  ......o  ......o  ......o 
-...o...  ...o...  ...o...  ...o...  ...o...  ...o..o  ...o..o  ...o..o 
-...oo.o  .oo.o.o  .o..o.o  .o..o.o  ..ooo.o  ..ooo..  oo.oo..  oo.o.oo 
-  ..o      ..o      o.o      o.o      o.o      o.o      o.o      o.o   
-  ...      ...      o..      o..      o..      o..      o..      o..   
-
-  oo.      oo.      oo.      oo.      oo.      oo.      ooo      ooo   
-  ooo      ooo      ooo      ooo      .oo      .o.      .oo      .oo   
-......o  .....oo  .....oo  .....oo  ..o..oo  ..o.ooo  ..o..oo  ...oooo 
-...o..o  ...o.oo  ...o.oo  ...o.oo  ..oo.oo  ..ooooo  ..ooooo  ..ooooo 
-oo.o.oo  oo.o..o  oo..ooo  o.ooooo  o.ooooo  o.ooooo  o.ooooo  o.ooooo 
-  o.o      o.o      o.o      o.o      o.o      o.o      o.o      o.o   
-  .oo      .oo      .oo      .oo      .oo      .oo      .oo      .oo   
-
-  ooo      ooo      ooo      ooo      ooo      ooo      ooo      ooo   
-  ooo      ooo      ooo      ooo      ooo      ooo      ooo      ooo   
-..ooooo  oo.oooo  ooooooo  ooooooo  ooooooo  ooooooo  ooooooo  ooooooo 
-...oooo  ...oooo  ..ooooo  oo.oooo  ooooooo  ooooooo  ooooooo  ooo.ooo 
-o.ooooo  o.ooooo  o..oooo  o..oooo  o.ooooo  o..oooo  ooo.ooo  ooooooo 
-  o.o      o.o      o.o      o.o      ..o      o.o      o.o      ooo   
-  .oo      .oo      .oo      .oo      .oo      ooo      ooo      ooo   
+\begin{tabular}{cccccc}
+$\xymatrix@=1.2pt@M=1.2pt{&&\circ &\circ &\circ &&&\\
+&&\circ &\circ &\circ &&&\\
+\circ &\circ &\circ &\circ &\circ &\circ &\circ &\\
+\circ &\circ &\circ &\times &\circ &\circ \ar@{-)}[ll]&\circ &\\
+\circ &\circ &\circ &\circ &\circ &\circ &\circ &\\
+&&\circ &\circ &\circ &&&\\
+&&\circ &\circ &\circ &&&\\
+}$
+ & $\xymatrix@=1.2pt@M=1.2pt{&&\circ &\circ &\circ &&&\\
+&&\circ &\circ &\circ \ar@{-)}[dd]&&&\\
+\circ &\circ &\circ &\circ &\circ &\circ &\circ &\\
+\circ &\circ &\circ &\circ &\times &\times &\circ &\\
+\circ &\circ &\circ &\circ &\circ &\circ &\circ &\\
+&&\circ &\circ &\circ &&&\\
+&&\circ &\circ &\circ &&&\\
+}$
+ & $\xymatrix@=1.2pt@M=1.2pt{&&\circ &\circ &\circ &&&\\
+&&\circ \ar@{-)}[rr]&\circ &\times &&&\\
+\circ &\circ &\circ &\circ &\times &\circ &\circ &\\
+\circ &\circ &\circ &\circ &\circ &\times &\circ &\\
+\circ &\circ &\circ &\circ &\circ &\circ &\circ &\\
+&&\circ &\circ &\circ &&&\\
+&&\circ &\circ &\circ &&&\\
+}$
+ & $\xymatrix@=1.2pt@M=1.2pt{&&\circ &\circ &\circ \ar@{-)}[dd]&&&\\
+&&\times &\times &\circ &&&\\
+\circ &\circ &\circ &\circ &\times &\circ &\circ &\\
+\circ &\circ &\circ &\circ &\circ &\times &\circ &\\
+\circ &\circ &\circ &\circ &\circ &\circ &\circ &\\
+&&\circ &\circ &\circ &&&\\
+&&\circ &\circ &\circ &&&\\
+}$
+ & $\xymatrix@=1.2pt@M=1.2pt{&&\circ &\circ &\times &&&\\
+&&\times &\times &\times &&&\\
+\circ &\circ &\circ &\circ &\circ &\circ &\circ &\\
+\circ &\circ &\circ &\circ \ar@{-)}[rr]&\circ &\times &\circ &\\
+\circ &\circ &\circ &\circ &\circ &\circ &\circ &\\
+&&\circ &\circ &\circ &&&\\
+&&\circ &\circ &\circ &&&\\
+}$
+ & \\\\$\xymatrix@=1.2pt@M=1.2pt{&&\circ &\circ &\times &&&\\
+&&\times &\times &\times &&&\\
+\circ &\circ &\circ &\circ &\circ &\circ &\circ &\\
+\circ &\circ &\circ &\times &\times &\circ &\circ &\\
+\circ &\circ &\circ &\circ &\circ &\circ &\circ &\\
+&&\circ &\circ &\circ \ar@{-)}[uu]&&&\\
+&&\circ &\circ &\circ &&&\\
+}$
+ & $\xymatrix@=1.2pt@M=1.2pt{&&\circ &\circ &\times &&&\\
+&&\times &\times &\times &&&\\
+\circ &\circ &\circ &\circ &\circ &\circ &\circ &\\
+\circ &\circ &\circ &\times &\circ &\circ &\circ &\\
+\circ &\circ &\circ &\circ &\times &\circ &\circ \ar@{-)}[ll]&\\
+&&\circ &\circ &\times &&&\\
+&&\circ &\circ &\circ &&&\\
+}$
+ & $\xymatrix@=1.2pt@M=1.2pt{&&\circ &\circ &\times &&&\\
+&&\times &\times &\times &&&\\
+\circ &\circ &\circ &\circ &\circ &\circ &\circ &\\
+\circ &\circ &\circ &\times &\circ &\circ &\circ &\\
+\circ &\circ &\circ &\circ \ar@{-)}[rr]&\circ &\times &\times &\\
+&&\circ &\circ &\times &&&\\
+&&\circ &\circ &\circ &&&\\
+}$
+ & $\xymatrix@=1.2pt@M=1.2pt{&&\circ &\circ &\times &&&\\
+&&\times &\times &\times &&&\\
+\circ &\circ &\circ &\circ &\circ &\circ &\circ &\\
+\circ &\circ &\circ &\times &\circ &\circ &\circ &\\
+\circ &\circ \ar@{-)}[rr]&\circ &\times &\times &\circ &\times &\\
+&&\circ &\circ &\times &&&\\
+&&\circ &\circ &\circ &&&\\
+}$
+ & $\xymatrix@=1.2pt@M=1.2pt{&&\circ &\circ &\times &&&\\
+&&\times &\times &\times &&&\\
+\circ &\circ &\circ &\circ &\circ &\circ &\circ &\\
+\circ &\circ &\circ &\times &\circ &\circ &\circ &\\
+\circ &\times &\times &\circ &\times &\circ &\times &\\
+&&\circ &\circ &\times &&&\\
+&&\circ \ar@{-)}[uu]&\circ &\circ &&&\\
+}$
+ & \\\\$\xymatrix@=1.2pt@M=1.2pt{&&\circ \ar@{-)}[rr]&\circ &\times &&&\\
+&&\times &\times &\times &&&\\
+\circ &\circ &\circ &\circ &\circ &\circ &\circ &\\
+\circ &\circ &\circ &\times &\circ &\circ &\circ &\\
+\circ &\times &\circ &\circ &\times &\circ &\times &\\
+&&\times &\circ &\times &&&\\
+&&\times &\circ &\circ &&&\\
+}$
+ & $\xymatrix@=1.2pt@M=1.2pt{&&\times &\times &\circ &&&\\
+&&\times &\times &\times &&&\\
+\circ &\circ &\circ &\circ &\circ &\circ &\circ &\\
+\circ &\circ &\circ &\times &\circ &\circ &\circ &\\
+\circ &\times &\circ &\circ \ar@{-)}[ll]&\times &\circ &\times &\\
+&&\times &\circ &\times &&&\\
+&&\times &\circ &\circ &&&\\
+}$
+ & $\xymatrix@=1.2pt@M=1.2pt{&&\times &\times &\circ &&&\\
+&&\times &\times &\times &&&\\
+\circ &\circ &\circ &\circ &\circ &\circ &\circ \ar@{-)}[dd]&\\
+\circ &\circ &\circ &\times &\circ &\circ &\circ &\\
+\circ &\circ &\times &\times &\times &\circ &\times &\\
+&&\times &\circ &\times &&&\\
+&&\times &\circ &\circ &&&\\
+}$
+ & $\xymatrix@=1.2pt@M=1.2pt{&&\times &\times &\circ &&&\\
+&&\times &\times &\times &&&\\
+\circ &\circ &\circ &\circ &\circ &\circ &\times &\\
+\circ &\circ &\circ &\times &\circ &\circ &\times &\\
+\circ \ar@{-)}[rr]&\circ &\times &\times &\times &\circ &\circ &\\
+&&\times &\circ &\times &&&\\
+&&\times &\circ &\circ &&&\\
+}$
+ & $\xymatrix@=1.2pt@M=1.2pt{&&\times &\times &\circ &&&\\
+&&\times &\times &\times &&&\\
+\circ &\circ &\circ &\circ &\circ &\circ &\times &\\
+\circ &\circ &\circ &\times &\circ &\circ &\times &\\
+\times &\times &\circ &\times &\times &\circ &\circ \ar@{-)}[ll]&\\
+&&\times &\circ &\times &&&\\
+&&\times &\circ &\circ &&&\\
+}$
+ & \\\\$\xymatrix@=1.2pt@M=1.2pt{&&\times &\times &\circ &&&\\
+&&\times &\times &\times &&&\\
+\circ &\circ &\circ &\circ &\circ &\circ &\times &\\
+\circ &\circ &\circ &\times &\circ &\circ &\times &\\
+\times &\times &\circ &\times &\circ &\times &\times &\\
+&&\times &\circ &\times &&&\\
+&&\times &\circ &\circ \ar@{-)}[ll]&&&\\
+}$
+ & $\xymatrix@=1.2pt@M=1.2pt{&&\times &\times &\circ &&&\\
+&&\times &\times &\times &&&\\
+\circ &\circ &\circ &\circ &\circ &\circ \ar@{-)}[dd]&\times &\\
+\circ &\circ &\circ &\times &\circ &\circ &\times &\\
+\times &\times &\circ &\times &\circ &\times &\times &\\
+&&\times &\circ &\times &&&\\
+&&\circ &\times &\times &&&\\
+}$
+ & $\xymatrix@=1.2pt@M=1.2pt{&&\times &\times &\circ &&&\\
+&&\times &\times &\times &&&\\
+\circ &\circ &\circ &\circ &\circ &\times &\times &\\
+\circ &\circ &\circ &\times &\circ &\times &\times &\\
+\times &\times &\circ &\times &\circ &\circ \ar@{-)}[ll]&\times &\\
+&&\times &\circ &\times &&&\\
+&&\circ &\times &\times &&&\\
+}$
+ & $\xymatrix@=1.2pt@M=1.2pt{&&\times &\times &\circ &&&\\
+&&\times &\times &\times &&&\\
+\circ &\circ &\circ &\circ &\circ &\times &\times &\\
+\circ &\circ &\circ &\times &\circ &\times &\times &\\
+\times &\times &\circ &\circ \ar@{-)}[ll]&\times &\times &\times &\\
+&&\times &\circ &\times &&&\\
+&&\circ &\times &\times &&&\\
+}$
+ & $\xymatrix@=1.2pt@M=1.2pt{&&\times &\times &\circ &&&\\
+&&\times &\times &\times &&&\\
+\circ &\circ &\circ &\circ &\circ &\times &\times &\\
+\circ &\circ &\circ \ar@{-)}[uu]&\times &\circ &\times &\times &\\
+\times &\circ &\times &\times &\times &\times &\times &\\
+&&\times &\circ &\times &&&\\
+&&\circ &\times &\times &&&\\
+}$
+ & \\\\$\xymatrix@=1.2pt@M=1.2pt{&&\times &\times &\circ &&&\\
+&&\circ &\times &\times &&&\\
+\circ &\circ &\times &\circ &\circ &\times &\times &\\
+\circ &\circ &\times &\times &\circ \ar@{-)}[uu]&\times &\times &\\
+\times &\circ &\times &\times &\times &\times &\times &\\
+&&\times &\circ &\times &&&\\
+&&\circ &\times &\times &&&\\
+}$
+ & $\xymatrix@=1.2pt@M=1.2pt{&&\times &\times &\circ \ar@{-)}[dd]&&&\\
+&&\circ &\times &\circ &&&\\
+\circ &\circ &\times &\circ &\times &\times &\times &\\
+\circ &\circ &\times &\times &\times &\times &\times &\\
+\times &\circ &\times &\times &\times &\times &\times &\\
+&&\times &\circ &\times &&&\\
+&&\circ &\times &\times &&&\\
+}$
+ & $\xymatrix@=1.2pt@M=1.2pt{&&\times &\times &\times &&&\\
+&&\circ &\times &\times &&&\\
+\circ &\circ &\times &\circ &\circ \ar@{-)}[ll]&\times &\times &\\
+\circ &\circ &\times &\times &\times &\times &\times &\\
+\times &\circ &\times &\times &\times &\times &\times &\\
+&&\times &\circ &\times &&&\\
+&&\circ &\times &\times &&&\\
+}$
+ & $\xymatrix@=1.2pt@M=1.2pt{&&\times &\times &\times &&&\\
+&&\circ \ar@{-)}[dd]&\times &\times &&&\\
+\circ &\circ &\circ &\times &\times &\times &\times &\\
+\circ &\circ &\times &\times &\times &\times &\times &\\
+\times &\circ &\times &\times &\times &\times &\times &\\
+&&\times &\circ &\times &&&\\
+&&\circ &\times &\times &&&\\
+}$
+ & $\xymatrix@=1.2pt@M=1.2pt{&&\times &\times &\times &&&\\
+&&\times &\times &\times &&&\\
+\circ \ar@{-)}[rr]&\circ &\times &\times &\times &\times &\times &\\
+\circ &\circ &\circ &\times &\times &\times &\times &\\
+\times &\circ &\times &\times &\times &\times &\times &\\
+&&\times &\circ &\times &&&\\
+&&\circ &\times &\times &&&\\
+}$
+ & \\\\$\xymatrix@=1.2pt@M=1.2pt{&&\times &\times &\times &&&\\
+&&\times &\times &\times &&&\\
+\times &\times &\circ \ar@{-)}[dd]&\times &\times &\times &\times &\\
+\circ &\circ &\circ &\times &\times &\times &\times &\\
+\times &\circ &\times &\times &\times &\times &\times &\\
+&&\times &\circ &\times &&&\\
+&&\circ &\times &\times &&&\\
+}$
+ & $\xymatrix@=1.2pt@M=1.2pt{&&\times &\times &\times &&&\\
+&&\times &\times &\times &&&\\
+\times &\times &\times &\times &\times &\times &\times &\\
+\circ \ar@{-)}[rr]&\circ &\times &\times &\times &\times &\times &\\
+\times &\circ &\circ &\times &\times &\times &\times &\\
+&&\times &\circ &\times &&&\\
+&&\circ &\times &\times &&&\\
+}$
+ & $\xymatrix@=1.2pt@M=1.2pt{&&\times &\times &\times &&&\\
+&&\times &\times &\times &&&\\
+\times &\times &\times &\times &\times &\times &\times &\\
+\times &\times &\circ \ar@{-)}[dd]&\times &\times &\times &\times &\\
+\times &\circ &\circ &\times &\times &\times &\times &\\
+&&\times &\circ &\times &&&\\
+&&\circ &\times &\times &&&\\
+}$
+ & $\xymatrix@=1.2pt@M=1.2pt{&&\times &\times &\times &&&\\
+&&\times &\times &\times &&&\\
+\times &\times &\times &\times &\times &\times &\times &\\
+\times &\times &\times &\times &\times &\times &\times &\\
+\times &\circ &\times &\times &\times &\times &\times &\\
+&&\circ &\circ &\times &&&\\
+&&\circ \ar@{-)}[uu]&\times &\times &&&\\
+}$
+ & $\xymatrix@=1.2pt@M=1.2pt{&&\times &\times &\times &&&\\
+&&\times &\times &\times &&&\\
+\times &\times &\times &\times &\times &\times &\times &\\
+\times &\times &\times &\times &\times &\times &\times &\\
+\times &\circ \ar@{-)}[rr]&\circ &\times &\times &\times &\times &\\
+&&\times &\circ &\times &&&\\
+&&\times &\times &\times &&&\\
+}$
+ & \\\\$\xymatrix@=1.2pt@M=1.2pt{&&\times &\times &\times &&&\\
+&&\times &\times &\times &&&\\
+\times &\times &\times &\times &\times &\times &\times &\\
+\times &\times &\times &\times &\times &\times &\times &\\
+\times &\times &\times &\circ &\times &\times &\times &\\
+&&\times &\circ \ar@{-)}[uu]&\times &&&\\
+&&\times &\times &\times &&&\\
+}$
+ & $\xymatrix@=1.2pt@M=1.2pt{&&\times &\times &\times &&&\\
+&&\times &\times &\times &&&\\
+\times &\times &\times &\times &\times &\times &\times &\\
+\times &\times &\times &\circ &\times &\times &\times &\\
+\times &\times &\times &\times &\times &\times &\times &\\
+&&\times &\times &\times &&&\\
+&&\times &\times &\times &&&\\
+}$
+\end{tabular}

diff --git a/a2/src/4/print4.py b/a2/src/4/print4.py
index c0fcfdd..e3eed1f 100644 (file)
--- a/a2/src/4/print4.py
+++ b/a2/src/4/print4.py
@@ -6,16 +6,50 @@ import re
 
 PAT = r'\(= i(?P<i>\d+)x(?P<x>\d+)y(?P<y>\d+) (?P<v>true|false)\)'
 
-def print_board(data, tofile):
+def print_board(previous, data, tofile):
     """Prints a peg solitaire board"""
-    for yco in range(8):
-        for xco in range(8):
-            pos = [d for d in data if d[0] == xco and d[1] == yco]
+    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(' ')
+                tofile.write('&')
             else:
-                tofile.write('.' if pos[0][2] else 'o')
-        tofile.write('\n')
+                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"""
@@ -29,9 +63,19 @@ def parse(lines, output):
                 data[ite] = []
             data[ite].append((int(match.group('x')), int(match.group('y')),
                               match.group('v') == 'true'))
-    for _, dat in sorted(data.items()):
-        print_board(dat, output)
-
+    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: