big update, better formalization for pegsol

[ar1516.git] / a2 / src / 4 / 4.model.bak

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)