success with 4:)
[ar1516.git] / a2 / src / 4 / 4.model
diff --git a/a2/src/4/4.model b/a2/src/4/4.model
new file mode 100644 (file)
index 0000000..3b52ae7
--- /dev/null
@@ -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)
+