a2/src/4/4.smv

   1
   2 MODULE main
   3 VAR
   4 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;
   5 INIT
   6 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
   7 TRANS
   8 case
   9 x0y2=TRUE & x0y3=TRUE & x0y4=FALSE:
  10 (next(x0y2)=FALSE & next(x0y3)=FALSE & next(x0y4)=TRUE &
  11 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
  12 );
  13 x0y2=TRUE & x1y2=TRUE & x2y2=FALSE:
  14 (next(x0y2)=FALSE & next(x1y2)=FALSE & next(x2y2)=TRUE &
  15 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
  16 );
  17 x0y3=TRUE & x1y3=TRUE & x2y3=FALSE:
  18 (next(x0y3)=FALSE & next(x1y3)=FALSE & next(x2y3)=TRUE &
  19 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
  20 );
  21 x0y4=TRUE & x0y3=TRUE & x0y2=FALSE:
  22 (next(x0y4)=FALSE & next(x0y3)=FALSE & next(x0y2)=TRUE &
  23 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
  24 );
  25 x0y4=TRUE & x1y4=TRUE & x2y4=FALSE:
  26 (next(x0y4)=FALSE & next(x1y4)=FALSE & next(x2y4)=TRUE &
  27 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
  28 );
  29 x1y2=TRUE & x1y3=TRUE & x1y4=FALSE:
  30 (next(x1y2)=FALSE & next(x1y3)=FALSE & next(x1y4)=TRUE &
  31 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
  32 );
  33 x1y2=TRUE & x2y2=TRUE & x3y2=FALSE:
  34 (next(x1y2)=FALSE & next(x2y2)=FALSE & next(x3y2)=TRUE &
  35 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
  36 );
  37 x1y3=TRUE & x2y3=TRUE & x3y3=FALSE:
  38 (next(x1y3)=FALSE & next(x2y3)=FALSE & next(x3y3)=TRUE &
  39 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
  40 );
  41 x1y4=TRUE & x1y3=TRUE & x1y2=FALSE:
  42 (next(x1y4)=FALSE & next(x1y3)=FALSE & next(x1y2)=TRUE &
  43 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
  44 );
  45 x1y4=TRUE & x2y4=TRUE & x3y4=FALSE:
  46 (next(x1y4)=FALSE & next(x2y4)=FALSE & next(x3y4)=TRUE &
  47 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
  48 );
  49 x2y0=TRUE & x2y1=TRUE & x2y2=FALSE:
  50 (next(x2y0)=FALSE & next(x2y1)=FALSE & next(x2y2)=TRUE &
  51 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
  52 );
  53 x2y0=TRUE & x3y0=TRUE & x4y0=FALSE:
  54 (next(x2y0)=FALSE & next(x3y0)=FALSE & next(x4y0)=TRUE &
  55 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
  56 );
  57 x2y1=TRUE & x2y2=TRUE & x2y3=FALSE:
  58 (next(x2y1)=FALSE & next(x2y2)=FALSE & next(x2y3)=TRUE &
  59 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
  60 );
  61 x2y1=TRUE & x3y1=TRUE & x4y1=FALSE:
  62 (next(x2y1)=FALSE & next(x3y1)=FALSE & next(x4y1)=TRUE &
  63 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
  64 );
  65 x2y2=TRUE & x1y2=TRUE & x0y2=FALSE:
  66 (next(x2y2)=FALSE & next(x1y2)=FALSE & next(x0y2)=TRUE &
  67 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
  68 );
  69 x2y2=TRUE & x2y1=TRUE & x2y0=FALSE:
  70 (next(x2y2)=FALSE & next(x2y1)=FALSE & next(x2y0)=TRUE &
  71 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
  72 );
  73 x2y2=TRUE & x2y3=TRUE & x2y4=FALSE:
  74 (next(x2y2)=FALSE & next(x2y3)=FALSE & next(x2y4)=TRUE &
  75 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
  76 );
  77 x2y2=TRUE & x3y2=TRUE & x4y2=FALSE:
  78 (next(x2y2)=FALSE & next(x3y2)=FALSE & next(x4y2)=TRUE &
  79 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
  80 );
  81 x2y3=TRUE & x1y3=TRUE & x0y3=FALSE:
  82 (next(x2y3)=FALSE & next(x1y3)=FALSE & next(x0y3)=TRUE &
  83 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
  84 );
  85 x2y3=TRUE & x2y2=TRUE & x2y1=FALSE:
  86 (next(x2y3)=FALSE & next(x2y2)=FALSE & next(x2y1)=TRUE &
  87 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
  88 );
  89 x2y3=TRUE & x2y4=TRUE & x2y5=FALSE:
  90 (next(x2y3)=FALSE & next(x2y4)=FALSE & next(x2y5)=TRUE &
  91 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
  92 );
  93 x2y3=TRUE & x3y3=TRUE & x4y3=FALSE:
  94 (next(x2y3)=FALSE & next(x3y3)=FALSE & next(x4y3)=TRUE &
  95 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
  96 );
  97 x2y4=TRUE & x1y4=TRUE & x0y4=FALSE:
  98 (next(x2y4)=FALSE & next(x1y4)=FALSE & next(x0y4)=TRUE &
  99 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
 100 );
 101 x2y4=TRUE & x2y3=TRUE & x2y2=FALSE:
 102 (next(x2y4)=FALSE & next(x2y3)=FALSE & next(x2y2)=TRUE &
 103 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
 104 );
 105 x2y4=TRUE & x2y5=TRUE & x2y6=FALSE:
 106 (next(x2y4)=FALSE & next(x2y5)=FALSE & next(x2y6)=TRUE &
 107 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
 108 );
 109 x2y4=TRUE & x3y4=TRUE & x4y4=FALSE:
 110 (next(x2y4)=FALSE & next(x3y4)=FALSE & next(x4y4)=TRUE &
 111 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
 112 );
 113 x2y5=TRUE & x2y4=TRUE & x2y3=FALSE:
 114 (next(x2y5)=FALSE & next(x2y4)=FALSE & next(x2y3)=TRUE &
 115 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
 116 );
 117 x2y5=TRUE & x3y5=TRUE & x4y5=FALSE:
 118 (next(x2y5)=FALSE & next(x3y5)=FALSE & next(x4y5)=TRUE &
 119 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
 120 );
 121 x2y6=TRUE & x2y5=TRUE & x2y4=FALSE:
 122 (next(x2y6)=FALSE & next(x2y5)=FALSE & next(x2y4)=TRUE &
 123 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
 124 );
 125 x2y6=TRUE & x3y6=TRUE & x4y6=FALSE:
 126 (next(x2y6)=FALSE & next(x3y6)=FALSE & next(x4y6)=TRUE &
 127 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
 128 );
 129 x3y0=TRUE & x3y1=TRUE & x3y2=FALSE:
 130 (next(x3y0)=FALSE & next(x3y1)=FALSE & next(x3y2)=TRUE &
 131 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
 132 );
 133 x3y1=TRUE & x3y2=TRUE & x3y3=FALSE:
 134 (next(x3y1)=FALSE & next(x3y2)=FALSE & next(x3y3)=TRUE &
 135 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
 136 );
 137 x3y2=TRUE & x2y2=TRUE & x1y2=FALSE:
 138 (next(x3y2)=FALSE & next(x2y2)=FALSE & next(x1y2)=TRUE &
 139 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
 140 );
 141 x3y2=TRUE & x3y1=TRUE & x3y0=FALSE:
 142 (next(x3y2)=FALSE & next(x3y1)=FALSE & next(x3y0)=TRUE &
 143 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
 144 );
 145 x3y2=TRUE & x3y3=TRUE & x3y4=FALSE:
 146 (next(x3y2)=FALSE & next(x3y3)=FALSE & next(x3y4)=TRUE &
 147 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
 148 );
 149 x3y2=TRUE & x4y2=TRUE & x5y2=FALSE:
 150 (next(x3y2)=FALSE & next(x4y2)=FALSE & next(x5y2)=TRUE &
 151 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
 152 );
 153 x3y3=TRUE & x2y3=TRUE & x1y3=FALSE:
 154 (next(x3y3)=FALSE & next(x2y3)=FALSE & next(x1y3)=TRUE &
 155 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
 156 );
 157 x3y3=TRUE & x3y2=TRUE & x3y1=FALSE:
 158 (next(x3y3)=FALSE & next(x3y2)=FALSE & next(x3y1)=TRUE &
 159 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
 160 );
 161 x3y3=TRUE & x3y4=TRUE & x3y5=FALSE:
 162 (next(x3y3)=FALSE & next(x3y4)=FALSE & next(x3y5)=TRUE &
 163 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
 164 );
 165 x3y3=TRUE & x4y3=TRUE & x5y3=FALSE:
 166 (next(x3y3)=FALSE & next(x4y3)=FALSE & next(x5y3)=TRUE &
 167 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
 168 );
 169 x3y4=TRUE & x2y4=TRUE & x1y4=FALSE:
 170 (next(x3y4)=FALSE & next(x2y4)=FALSE & next(x1y4)=TRUE &
 171 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
 172 );
 173 x3y4=TRUE & x3y3=TRUE & x3y2=FALSE:
 174 (next(x3y4)=FALSE & next(x3y3)=FALSE & next(x3y2)=TRUE &
 175 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
 176 );
 177 x3y4=TRUE & x3y5=TRUE & x3y6=FALSE:
 178 (next(x3y4)=FALSE & next(x3y5)=FALSE & next(x3y6)=TRUE &
 179 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
 180 );
 181 x3y4=TRUE & x4y4=TRUE & x5y4=FALSE:
 182 (next(x3y4)=FALSE & next(x4y4)=FALSE & next(x5y4)=TRUE &
 183 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
 184 );
 185 x3y5=TRUE & x3y4=TRUE & x3y3=FALSE:
 186 (next(x3y5)=FALSE & next(x3y4)=FALSE & next(x3y3)=TRUE &
 187 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
 188 );
 189 x3y6=TRUE & x3y5=TRUE & x3y4=FALSE:
 190 (next(x3y6)=FALSE & next(x3y5)=FALSE & next(x3y4)=TRUE &
 191 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
 192 );
 193 x4y0=TRUE & x3y0=TRUE & x2y0=FALSE:
 194 (next(x4y0)=FALSE & next(x3y0)=FALSE & next(x2y0)=TRUE &
 195 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
 196 );
 197 x4y0=TRUE & x4y1=TRUE & x4y2=FALSE:
 198 (next(x4y0)=FALSE & next(x4y1)=FALSE & next(x4y2)=TRUE &
 199 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
 200 );
 201 x4y1=TRUE & x3y1=TRUE & x2y1=FALSE:
 202 (next(x4y1)=FALSE & next(x3y1)=FALSE & next(x2y1)=TRUE &
 203 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
 204 );
 205 x4y1=TRUE & x4y2=TRUE & x4y3=FALSE:
 206 (next(x4y1)=FALSE & next(x4y2)=FALSE & next(x4y3)=TRUE &
 207 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
 208 );
 209 x4y2=TRUE & x3y2=TRUE & x2y2=FALSE:
 210 (next(x4y2)=FALSE & next(x3y2)=FALSE & next(x2y2)=TRUE &
 211 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
 212 );
 213 x4y2=TRUE & x4y1=TRUE & x4y0=FALSE:
 214 (next(x4y2)=FALSE & next(x4y1)=FALSE & next(x4y0)=TRUE &
 215 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
 216 );
 217 x4y2=TRUE & x4y3=TRUE & x4y4=FALSE:
 218 (next(x4y2)=FALSE & next(x4y3)=FALSE & next(x4y4)=TRUE &
 219 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
 220 );
 221 x4y2=TRUE & x5y2=TRUE & x6y2=FALSE:
 222 (next(x4y2)=FALSE & next(x5y2)=FALSE & next(x6y2)=TRUE &
 223 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
 224 );
 225 x4y3=TRUE & x3y3=TRUE & x2y3=FALSE:
 226 (next(x4y3)=FALSE & next(x3y3)=FALSE & next(x2y3)=TRUE &
 227 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
 228 );
 229 x4y3=TRUE & x4y2=TRUE & x4y1=FALSE:
 230 (next(x4y3)=FALSE & next(x4y2)=FALSE & next(x4y1)=TRUE &
 231 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
 232 );
 233 x4y3=TRUE & x4y4=TRUE & x4y5=FALSE:
 234 (next(x4y3)=FALSE & next(x4y4)=FALSE & next(x4y5)=TRUE &
 235 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
 236 );
 237 x4y3=TRUE & x5y3=TRUE & x6y3=FALSE:
 238 (next(x4y3)=FALSE & next(x5y3)=FALSE & next(x6y3)=TRUE &
 239 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
 240 );
 241 x4y4=TRUE & x3y4=TRUE & x2y4=FALSE:
 242 (next(x4y4)=FALSE & next(x3y4)=FALSE & next(x2y4)=TRUE &
 243 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
 244 );
 245 x4y4=TRUE & x4y3=TRUE & x4y2=FALSE:
 246 (next(x4y4)=FALSE & next(x4y3)=FALSE & next(x4y2)=TRUE &
 247 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
 248 );
 249 x4y4=TRUE & x4y5=TRUE & x4y6=FALSE:
 250 (next(x4y4)=FALSE & next(x4y5)=FALSE & next(x4y6)=TRUE &
 251 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
 252 );
 253 x4y4=TRUE & x5y4=TRUE & x6y4=FALSE:
 254 (next(x4y4)=FALSE & next(x5y4)=FALSE & next(x6y4)=TRUE &
 255 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
 256 );
 257 x4y5=TRUE & x3y5=TRUE & x2y5=FALSE:
 258 (next(x4y5)=FALSE & next(x3y5)=FALSE & next(x2y5)=TRUE &
 259 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
 260 );
 261 x4y5=TRUE & x4y4=TRUE & x4y3=FALSE:
 262 (next(x4y5)=FALSE & next(x4y4)=FALSE & next(x4y3)=TRUE &
 263 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
 264 );
 265 x4y6=TRUE & x3y6=TRUE & x2y6=FALSE:
 266 (next(x4y6)=FALSE & next(x3y6)=FALSE & next(x2y6)=TRUE &
 267 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
 268 );
 269 x4y6=TRUE & x4y5=TRUE & x4y4=FALSE:
 270 (next(x4y6)=FALSE & next(x4y5)=FALSE & next(x4y4)=TRUE &
 271 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
 272 );
 273 x5y2=TRUE & x4y2=TRUE & x3y2=FALSE:
 274 (next(x5y2)=FALSE & next(x4y2)=FALSE & next(x3y2)=TRUE &
 275 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
 276 );
 277 x5y2=TRUE & x5y3=TRUE & x5y4=FALSE:
 278 (next(x5y2)=FALSE & next(x5y3)=FALSE & next(x5y4)=TRUE &
 279 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
 280 );
 281 x5y3=TRUE & x4y3=TRUE & x3y3=FALSE:
 282 (next(x5y3)=FALSE & next(x4y3)=FALSE & next(x3y3)=TRUE &
 283 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
 284 );
 285 x5y4=TRUE & x4y4=TRUE & x3y4=FALSE:
 286 (next(x5y4)=FALSE & next(x4y4)=FALSE & next(x3y4)=TRUE &
 287 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
 288 );
 289 x5y4=TRUE & x5y3=TRUE & x5y2=FALSE:
 290 (next(x5y4)=FALSE & next(x5y3)=FALSE & next(x5y2)=TRUE &
 291 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
 292 );
 293 x6y2=TRUE & x5y2=TRUE & x4y2=FALSE:
 294 (next(x6y2)=FALSE & next(x5y2)=FALSE & next(x4y2)=TRUE &
 295 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
 296 );
 297 x6y2=TRUE & x6y3=TRUE & x6y4=FALSE:
 298 (next(x6y2)=FALSE & next(x6y3)=FALSE & next(x6y4)=TRUE &
 299 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
 300 );
 301 x6y3=TRUE & x5y3=TRUE & x4y3=FALSE:
 302 (next(x6y3)=FALSE & next(x5y3)=FALSE & next(x4y3)=TRUE &
 303 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
 304 );
 305 x6y4=TRUE & x5y4=TRUE & x4y4=FALSE:
 306 (next(x6y4)=FALSE & next(x5y4)=FALSE & next(x4y4)=TRUE &
 307 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
 308 );
 309 x6y4=TRUE & x6y3=TRUE & x6y2=FALSE:
 310 (next(x6y4)=FALSE & next(x6y3)=FALSE & next(x6y2)=TRUE &
 311 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
 312 );
 313 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);
 314 esac
 315 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)