model main {
  var A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1, X1, Y1, Z1, A2, B2, C2, D2, E2, F2, G2, H2, I2, J2, K2, L2, M2, N2, O2, P2, Q2, R2, S2, T2, U2, V2, W2, X2, Y2, Z2, A3, B3, C3, D3, E3, F3;
  states f29, f34, f30, f35, f31, f32, f1, f11, f27, f12, f14, f15, f16, f17, f26;
  transition t0 := {
    from   := f29;
    to     := f34;
    guard  := A >= 0 && B > 0 && N2 > 1 && 0 > C && O2 >= N2 && 0 > P2 && D = 1;
    action := E' = N2, F' = P2, G' = 0, H' = I, D' = 1, J' = Q2, K' = 1 + I, L' = R2, M' = S2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t1 := {
    from   := f29;
    to     := f34;
    guard  := A >= 0 && B > 0 && N2 > 1 && 0 > C && O2 >= N2 && P2 > 0 && D = 1;
    action := E' = N2, F' = P2, G' = 0, H' = I, D' = 1, J' = Q2, K' = 1 + I, L' = R2, M' = S2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t2 := {
    from   := f29;
    to     := f34;
    guard  := A >= 0 && B > 0 && N2 > 1 && C > 0 && O2 >= N2 && 0 > P2 && D = 1;
    action := E' = N2, F' = P2, G' = 0, H' = I, D' = 1, J' = Q2, K' = 1 + I, L' = R2, M' = S2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t3 := {
    from   := f29;
    to     := f34;
    guard  := A >= 0 && B > 0 && N2 > 1 && C > 0 && O2 >= N2 && P2 > 0 && D = 1;
    action := E' = N2, F' = P2, G' = 0, H' = I, D' = 1, J' = Q2, K' = 1 + I, L' = R2, M' = S2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t4 := {
    from   := f29;
    to     := f29;
    guard  := A >= N2 && A >= 0 && B > 0 && N2 > 1 && 0 > R2 && 0 > P2;
    action := E' = N2, F' = C, B' = -1 + B, G' = P2, M' = Q2, N' = B, O' = A, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t5 := {
    from   := f29;
    to     := f29;
    guard  := A >= N2 && A >= 0 && B > 0 && N2 > 1 && 0 > R2 && P2 > 0;
    action := E' = N2, F' = C, B' = -1 + B, G' = P2, M' = Q2, N' = B, O' = A, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t6 := {
    from   := f29;
    to     := f29;
    guard  := A >= N2 && A >= 0 && B > 0 && N2 > 1 && R2 > 0 && 0 > P2;
    action := E' = N2, F' = C, B' = -1 + B, G' = P2, M' = Q2, N' = B, O' = A, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t7 := {
    from   := f29;
    to     := f29;
    guard  := A >= N2 && A >= 0 && B > 0 && N2 > 1 && R2 > 0 && P2 > 0;
    action := E' = N2, F' = C, B' = -1 + B, G' = P2, M' = Q2, N' = B, O' = A, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t8 := {
    from   := f30;
    to     := f35;
    guard  := B > 0 && I >= 0 && N2 > 1 && 0 > C && 0 > Q2 && 0 > P2 && H = I && D = 1;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, D' = 1, I' = H, M' = R2, P' = B, Q' = S2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t9 := {
    from   := f30;
    to     := f35;
    guard  := B > 0 && I >= 0 && N2 > 1 && 0 > C && 0 > Q2 && P2 > 0 && H = I && D = 1;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, D' = 1, I' = H, M' = R2, P' = B, Q' = S2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t10 := {
    from   := f30;
    to     := f35;
    guard  := B > 0 && I >= 0 && N2 > 1 && 0 > C && Q2 > 0 && 0 > P2 && H = I && D = 1;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, D' = 1, I' = H, M' = R2, P' = B, Q' = S2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t11 := {
    from   := f30;
    to     := f35;
    guard  := B > 0 && I >= 0 && N2 > 1 && 0 > C && Q2 > 0 && P2 > 0 && H = I && D = 1;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, D' = 1, I' = H, M' = R2, P' = B, Q' = S2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t12 := {
    from   := f30;
    to     := f35;
    guard  := B > 0 && I >= 0 && N2 > 1 && C > 0 && 0 > Q2 && 0 > P2 && H = I && D = 1;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, D' = 1, I' = H, M' = R2, P' = B, Q' = S2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t13 := {
    from   := f30;
    to     := f35;
    guard  := B > 0 && I >= 0 && N2 > 1 && C > 0 && 0 > Q2 && P2 > 0 && H = I && D = 1;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, D' = 1, I' = H, M' = R2, P' = B, Q' = S2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t14 := {
    from   := f30;
    to     := f35;
    guard  := B > 0 && I >= 0 && N2 > 1 && C > 0 && Q2 > 0 && 0 > P2 && H = I && D = 1;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, D' = 1, I' = H, M' = R2, P' = B, Q' = S2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t15 := {
    from   := f30;
    to     := f35;
    guard  := B > 0 && I >= 0 && N2 > 1 && C > 0 && Q2 > 0 && P2 > 0 && H = I && D = 1;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, D' = 1, I' = H, M' = R2, P' = B, Q' = S2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t16 := {
    from   := f30;
    to     := f34;
    guard  := B > 0 && H >= 0 && N2 > 1 && 0 > O2 && 0 > P2 && 0 > S2 && I + 1 = H && D = 2;
    action := E' = N2, F' = P2, G' = 0, D' = 2, I' = -1 + H, M' = Q2, R' = C, S' = R2, T' = S2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t17 := {
    from   := f30;
    to     := f34;
    guard  := B > 0 && H >= 0 && N2 > 1 && 0 > O2 && 0 > P2 && S2 > 0 && I + 1 = H && D = 2;
    action := E' = N2, F' = P2, G' = 0, D' = 2, I' = -1 + H, M' = Q2, R' = C, S' = R2, T' = S2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t18 := {
    from   := f30;
    to     := f34;
    guard  := B > 0 && H >= 0 && N2 > 1 && 0 > O2 && P2 > 0 && 0 > S2 && I + 1 = H && D = 2;
    action := E' = N2, F' = P2, G' = 0, D' = 2, I' = -1 + H, M' = Q2, R' = C, S' = R2, T' = S2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t19 := {
    from   := f30;
    to     := f34;
    guard  := B > 0 && H >= 0 && N2 > 1 && 0 > O2 && P2 > 0 && S2 > 0 && I + 1 = H && D = 2;
    action := E' = N2, F' = P2, G' = 0, D' = 2, I' = -1 + H, M' = Q2, R' = C, S' = R2, T' = S2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t20 := {
    from   := f30;
    to     := f34;
    guard  := B > 0 && H >= 0 && N2 > 1 && O2 > 0 && 0 > P2 && 0 > S2 && I + 1 = H && D = 2;
    action := E' = N2, F' = P2, G' = 0, D' = 2, I' = -1 + H, M' = Q2, R' = C, S' = R2, T' = S2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t21 := {
    from   := f30;
    to     := f34;
    guard  := B > 0 && H >= 0 && N2 > 1 && O2 > 0 && 0 > P2 && S2 > 0 && I + 1 = H && D = 2;
    action := E' = N2, F' = P2, G' = 0, D' = 2, I' = -1 + H, M' = Q2, R' = C, S' = R2, T' = S2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t22 := {
    from   := f30;
    to     := f34;
    guard  := B > 0 && H >= 0 && N2 > 1 && O2 > 0 && P2 > 0 && 0 > S2 && I + 1 = H && D = 2;
    action := E' = N2, F' = P2, G' = 0, D' = 2, I' = -1 + H, M' = Q2, R' = C, S' = R2, T' = S2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t23 := {
    from   := f30;
    to     := f34;
    guard  := B > 0 && H >= 0 && N2 > 1 && O2 > 0 && P2 > 0 && S2 > 0 && I + 1 = H && D = 2;
    action := E' = N2, F' = P2, G' = 0, D' = 2, I' = -1 + H, M' = Q2, R' = C, S' = R2, T' = S2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t24 := {
    from   := f31;
    to     := f35;
    guard  := B > 0 && H >= 0 && N2 > 1 && 0 > C && 0 > Q2 && 0 > S2 && 0 > P2 && I = H && D = 1;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, D' = 1, I' = H, M' = R2, U' = S2, V' = B, W' = J, X' = H, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t25 := {
    from   := f31;
    to     := f35;
    guard  := B > 0 && H >= 0 && N2 > 1 && 0 > C && 0 > Q2 && 0 > S2 && P2 > 0 && I = H && D = 1;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, D' = 1, I' = H, M' = R2, U' = S2, V' = B, W' = J, X' = H, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t26 := {
    from   := f31;
    to     := f35;
    guard  := B > 0 && H >= 0 && N2 > 1 && 0 > C && 0 > Q2 && S2 > 0 && 0 > P2 && I = H && D = 1;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, D' = 1, I' = H, M' = R2, U' = S2, V' = B, W' = J, X' = H, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t27 := {
    from   := f31;
    to     := f35;
    guard  := B > 0 && H >= 0 && N2 > 1 && 0 > C && 0 > Q2 && S2 > 0 && P2 > 0 && I = H && D = 1;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, D' = 1, I' = H, M' = R2, U' = S2, V' = B, W' = J, X' = H, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t28 := {
    from   := f31;
    to     := f35;
    guard  := B > 0 && H >= 0 && N2 > 1 && 0 > C && Q2 > 0 && 0 > S2 && 0 > P2 && I = H && D = 1;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, D' = 1, I' = H, M' = R2, U' = S2, V' = B, W' = J, X' = H, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t29 := {
    from   := f31;
    to     := f35;
    guard  := B > 0 && H >= 0 && N2 > 1 && 0 > C && Q2 > 0 && 0 > S2 && P2 > 0 && I = H && D = 1;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, D' = 1, I' = H, M' = R2, U' = S2, V' = B, W' = J, X' = H, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t30 := {
    from   := f31;
    to     := f35;
    guard  := B > 0 && H >= 0 && N2 > 1 && 0 > C && Q2 > 0 && S2 > 0 && 0 > P2 && I = H && D = 1;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, D' = 1, I' = H, M' = R2, U' = S2, V' = B, W' = J, X' = H, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t31 := {
    from   := f31;
    to     := f35;
    guard  := B > 0 && H >= 0 && N2 > 1 && 0 > C && Q2 > 0 && S2 > 0 && P2 > 0 && I = H && D = 1;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, D' = 1, I' = H, M' = R2, U' = S2, V' = B, W' = J, X' = H, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t32 := {
    from   := f31;
    to     := f35;
    guard  := B > 0 && H >= 0 && N2 > 1 && C > 0 && 0 > Q2 && 0 > S2 && 0 > P2 && I = H && D = 1;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, D' = 1, I' = H, M' = R2, U' = S2, V' = B, W' = J, X' = H, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t33 := {
    from   := f31;
    to     := f35;
    guard  := B > 0 && H >= 0 && N2 > 1 && C > 0 && 0 > Q2 && 0 > S2 && P2 > 0 && I = H && D = 1;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, D' = 1, I' = H, M' = R2, U' = S2, V' = B, W' = J, X' = H, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t34 := {
    from   := f31;
    to     := f35;
    guard  := B > 0 && H >= 0 && N2 > 1 && C > 0 && 0 > Q2 && S2 > 0 && 0 > P2 && I = H && D = 1;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, D' = 1, I' = H, M' = R2, U' = S2, V' = B, W' = J, X' = H, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t35 := {
    from   := f31;
    to     := f35;
    guard  := B > 0 && H >= 0 && N2 > 1 && C > 0 && 0 > Q2 && S2 > 0 && P2 > 0 && I = H && D = 1;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, D' = 1, I' = H, M' = R2, U' = S2, V' = B, W' = J, X' = H, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t36 := {
    from   := f31;
    to     := f35;
    guard  := B > 0 && H >= 0 && N2 > 1 && C > 0 && Q2 > 0 && 0 > S2 && 0 > P2 && I = H && D = 1;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, D' = 1, I' = H, M' = R2, U' = S2, V' = B, W' = J, X' = H, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t37 := {
    from   := f31;
    to     := f35;
    guard  := B > 0 && H >= 0 && N2 > 1 && C > 0 && Q2 > 0 && 0 > S2 && P2 > 0 && I = H && D = 1;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, D' = 1, I' = H, M' = R2, U' = S2, V' = B, W' = J, X' = H, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t38 := {
    from   := f31;
    to     := f35;
    guard  := B > 0 && H >= 0 && N2 > 1 && C > 0 && Q2 > 0 && S2 > 0 && 0 > P2 && I = H && D = 1;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, D' = 1, I' = H, M' = R2, U' = S2, V' = B, W' = J, X' = H, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t39 := {
    from   := f31;
    to     := f35;
    guard  := B > 0 && H >= 0 && N2 > 1 && C > 0 && Q2 > 0 && S2 > 0 && P2 > 0 && I = H && D = 1;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, D' = 1, I' = H, M' = R2, U' = S2, V' = B, W' = J, X' = H, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t40 := {
    from   := f31;
    to     := f34;
    guard  := B > 0 && H >= 0 && N2 > 1 && 0 > C && 0 > P2 && 0 > S2;
    action := E' = N2, F' = P2, G' = 0, M' = Q2, Y' = R2, Z' = S2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t41 := {
    from   := f31;
    to     := f34;
    guard  := B > 0 && H >= 0 && N2 > 1 && 0 > C && 0 > P2 && S2 > 0;
    action := E' = N2, F' = P2, G' = 0, M' = Q2, Y' = R2, Z' = S2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t42 := {
    from   := f31;
    to     := f34;
    guard  := B > 0 && H >= 0 && N2 > 1 && 0 > C && P2 > 0 && 0 > S2;
    action := E' = N2, F' = P2, G' = 0, M' = Q2, Y' = R2, Z' = S2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t43 := {
    from   := f31;
    to     := f34;
    guard  := B > 0 && H >= 0 && N2 > 1 && 0 > C && P2 > 0 && S2 > 0;
    action := E' = N2, F' = P2, G' = 0, M' = Q2, Y' = R2, Z' = S2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t44 := {
    from   := f31;
    to     := f34;
    guard  := B > 0 && H >= 0 && N2 > 1 && C > 0 && 0 > P2 && 0 > S2;
    action := E' = N2, F' = P2, G' = 0, M' = Q2, Y' = R2, Z' = S2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t45 := {
    from   := f31;
    to     := f34;
    guard  := B > 0 && H >= 0 && N2 > 1 && C > 0 && 0 > P2 && S2 > 0;
    action := E' = N2, F' = P2, G' = 0, M' = Q2, Y' = R2, Z' = S2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t46 := {
    from   := f31;
    to     := f34;
    guard  := B > 0 && H >= 0 && N2 > 1 && C > 0 && P2 > 0 && 0 > S2;
    action := E' = N2, F' = P2, G' = 0, M' = Q2, Y' = R2, Z' = S2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t47 := {
    from   := f31;
    to     := f34;
    guard  := B > 0 && H >= 0 && N2 > 1 && C > 0 && P2 > 0 && S2 > 0;
    action := E' = N2, F' = P2, G' = 0, M' = Q2, Y' = R2, Z' = S2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t48 := {
    from   := f32;
    to     := f32;
    guard  := B > 0 && 0 > Q2 && 0 > N2;
    action := E' = 1, F' = C, B' = -1 + B, G' = N2, M' = P2, A1' = B, B1' = C1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t49 := {
    from   := f32;
    to     := f32;
    guard  := B > 0 && 0 > Q2 && N2 > 0;
    action := E' = 1, F' = C, B' = -1 + B, G' = N2, M' = P2, A1' = B, B1' = C1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t50 := {
    from   := f32;
    to     := f32;
    guard  := B > 0 && Q2 > 0 && 0 > N2;
    action := E' = 1, F' = C, B' = -1 + B, G' = N2, M' = P2, A1' = B, B1' = C1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t51 := {
    from   := f32;
    to     := f32;
    guard  := B > 0 && Q2 > 0 && N2 > 0;
    action := E' = 1, F' = C, B' = -1 + B, G' = N2, M' = P2, A1' = B, B1' = C1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t52 := {
    from   := f34;
    to     := f35;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && 0 > C && 0 > Q2 && 0 > P2;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, M' = R2, D1' = B, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t53 := {
    from   := f34;
    to     := f35;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && 0 > C && 0 > Q2 && P2 > 0;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, M' = R2, D1' = B, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t54 := {
    from   := f34;
    to     := f35;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && 0 > C && Q2 > 0 && 0 > P2;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, M' = R2, D1' = B, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t55 := {
    from   := f34;
    to     := f35;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && 0 > C && Q2 > 0 && P2 > 0;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, M' = R2, D1' = B, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t56 := {
    from   := f34;
    to     := f35;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && C > 0 && 0 > Q2 && 0 > P2;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, M' = R2, D1' = B, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t57 := {
    from   := f34;
    to     := f35;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && C > 0 && 0 > Q2 && P2 > 0;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, M' = R2, D1' = B, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t58 := {
    from   := f34;
    to     := f35;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && C > 0 && Q2 > 0 && 0 > P2;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, M' = R2, D1' = B, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t59 := {
    from   := f34;
    to     := f35;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && C > 0 && Q2 > 0 && P2 > 0;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, M' = R2, D1' = B, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t60 := {
    from   := f34;
    to     := f34;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && 0 > O2 && 0 > P2 && 0 > S2;
    action := E' = N2, F' = P2, G' = 0, D' = 1 + D, I' = -1 + I, J' = Q2, M' = R2, E1' = C, F1' = S2, G1' = 1 + D, H1' = -1 + I, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t61 := {
    from   := f34;
    to     := f34;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && 0 > O2 && 0 > P2 && S2 > 0;
    action := E' = N2, F' = P2, G' = 0, D' = 1 + D, I' = -1 + I, J' = Q2, M' = R2, E1' = C, F1' = S2, G1' = 1 + D, H1' = -1 + I, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t62 := {
    from   := f34;
    to     := f34;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && 0 > O2 && P2 > 0 && 0 > S2;
    action := E' = N2, F' = P2, G' = 0, D' = 1 + D, I' = -1 + I, J' = Q2, M' = R2, E1' = C, F1' = S2, G1' = 1 + D, H1' = -1 + I, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t63 := {
    from   := f34;
    to     := f34;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && 0 > O2 && P2 > 0 && S2 > 0;
    action := E' = N2, F' = P2, G' = 0, D' = 1 + D, I' = -1 + I, J' = Q2, M' = R2, E1' = C, F1' = S2, G1' = 1 + D, H1' = -1 + I, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t64 := {
    from   := f34;
    to     := f34;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && O2 > 0 && 0 > P2 && 0 > S2;
    action := E' = N2, F' = P2, G' = 0, D' = 1 + D, I' = -1 + I, J' = Q2, M' = R2, E1' = C, F1' = S2, G1' = 1 + D, H1' = -1 + I, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t65 := {
    from   := f34;
    to     := f34;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && O2 > 0 && 0 > P2 && S2 > 0;
    action := E' = N2, F' = P2, G' = 0, D' = 1 + D, I' = -1 + I, J' = Q2, M' = R2, E1' = C, F1' = S2, G1' = 1 + D, H1' = -1 + I, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t66 := {
    from   := f34;
    to     := f34;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && O2 > 0 && P2 > 0 && 0 > S2;
    action := E' = N2, F' = P2, G' = 0, D' = 1 + D, I' = -1 + I, J' = Q2, M' = R2, E1' = C, F1' = S2, G1' = 1 + D, H1' = -1 + I, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t67 := {
    from   := f34;
    to     := f34;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && O2 > 0 && P2 > 0 && S2 > 0;
    action := E' = N2, F' = P2, G' = 0, D' = 1 + D, I' = -1 + I, J' = Q2, M' = R2, E1' = C, F1' = S2, G1' = 1 + D, H1' = -1 + I, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t68 := {
    from   := f35;
    to     := f35;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && 0 > C && 0 > Q2 && 0 > S2 && 0 > P2;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, M' = R2, I1' = S2, J1' = B, K1' = D, L1' = I, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t69 := {
    from   := f35;
    to     := f35;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && 0 > C && 0 > Q2 && 0 > S2 && P2 > 0;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, M' = R2, I1' = S2, J1' = B, K1' = D, L1' = I, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t70 := {
    from   := f35;
    to     := f35;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && 0 > C && 0 > Q2 && S2 > 0 && 0 > P2;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, M' = R2, I1' = S2, J1' = B, K1' = D, L1' = I, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t71 := {
    from   := f35;
    to     := f35;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && 0 > C && 0 > Q2 && S2 > 0 && P2 > 0;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, M' = R2, I1' = S2, J1' = B, K1' = D, L1' = I, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t72 := {
    from   := f35;
    to     := f35;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && 0 > C && Q2 > 0 && 0 > S2 && 0 > P2;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, M' = R2, I1' = S2, J1' = B, K1' = D, L1' = I, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t73 := {
    from   := f35;
    to     := f35;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && 0 > C && Q2 > 0 && 0 > S2 && P2 > 0;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, M' = R2, I1' = S2, J1' = B, K1' = D, L1' = I, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t74 := {
    from   := f35;
    to     := f35;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && 0 > C && Q2 > 0 && S2 > 0 && 0 > P2;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, M' = R2, I1' = S2, J1' = B, K1' = D, L1' = I, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t75 := {
    from   := f35;
    to     := f35;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && 0 > C && Q2 > 0 && S2 > 0 && P2 > 0;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, M' = R2, I1' = S2, J1' = B, K1' = D, L1' = I, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t76 := {
    from   := f35;
    to     := f35;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && C > 0 && 0 > Q2 && 0 > S2 && 0 > P2;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, M' = R2, I1' = S2, J1' = B, K1' = D, L1' = I, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t77 := {
    from   := f35;
    to     := f35;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && C > 0 && 0 > Q2 && 0 > S2 && P2 > 0;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, M' = R2, I1' = S2, J1' = B, K1' = D, L1' = I, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t78 := {
    from   := f35;
    to     := f35;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && C > 0 && 0 > Q2 && S2 > 0 && 0 > P2;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, M' = R2, I1' = S2, J1' = B, K1' = D, L1' = I, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t79 := {
    from   := f35;
    to     := f35;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && C > 0 && 0 > Q2 && S2 > 0 && P2 > 0;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, M' = R2, I1' = S2, J1' = B, K1' = D, L1' = I, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t80 := {
    from   := f35;
    to     := f35;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && C > 0 && Q2 > 0 && 0 > S2 && 0 > P2;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, M' = R2, I1' = S2, J1' = B, K1' = D, L1' = I, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t81 := {
    from   := f35;
    to     := f35;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && C > 0 && Q2 > 0 && 0 > S2 && P2 > 0;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, M' = R2, I1' = S2, J1' = B, K1' = D, L1' = I, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t82 := {
    from   := f35;
    to     := f35;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && C > 0 && Q2 > 0 && S2 > 0 && 0 > P2;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, M' = R2, I1' = S2, J1' = B, K1' = D, L1' = I, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t83 := {
    from   := f35;
    to     := f35;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && C > 0 && Q2 > 0 && S2 > 0 && P2 > 0;
    action := E' = N2, F' = P2, B' = -1 + B, G' = Q2, M' = R2, I1' = S2, J1' = B, K1' = D, L1' = I, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t84 := {
    from   := f35;
    to     := f34;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && 0 > T2 && 0 > O2 && 0 > P2 && 0 > S2;
    action := E' = N2, F' = P2, G' = 0, D' = 1 + D, I' = -1 + I, J' = Q2, M' = R2, I1' = S2, M1' = C, N1' = O2, O1' = 1 + D, P1' = -1 + I, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t85 := {
    from   := f35;
    to     := f34;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && 0 > T2 && 0 > O2 && 0 > P2 && S2 > 0;
    action := E' = N2, F' = P2, G' = 0, D' = 1 + D, I' = -1 + I, J' = Q2, M' = R2, I1' = S2, M1' = C, N1' = O2, O1' = 1 + D, P1' = -1 + I, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t86 := {
    from   := f35;
    to     := f34;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && 0 > T2 && 0 > O2 && P2 > 0 && 0 > S2;
    action := E' = N2, F' = P2, G' = 0, D' = 1 + D, I' = -1 + I, J' = Q2, M' = R2, I1' = S2, M1' = C, N1' = O2, O1' = 1 + D, P1' = -1 + I, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t87 := {
    from   := f35;
    to     := f34;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && 0 > T2 && 0 > O2 && P2 > 0 && S2 > 0;
    action := E' = N2, F' = P2, G' = 0, D' = 1 + D, I' = -1 + I, J' = Q2, M' = R2, I1' = S2, M1' = C, N1' = O2, O1' = 1 + D, P1' = -1 + I, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t88 := {
    from   := f35;
    to     := f34;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && 0 > T2 && O2 > 0 && 0 > P2 && 0 > S2;
    action := E' = N2, F' = P2, G' = 0, D' = 1 + D, I' = -1 + I, J' = Q2, M' = R2, I1' = S2, M1' = C, N1' = O2, O1' = 1 + D, P1' = -1 + I, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t89 := {
    from   := f35;
    to     := f34;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && 0 > T2 && O2 > 0 && 0 > P2 && S2 > 0;
    action := E' = N2, F' = P2, G' = 0, D' = 1 + D, I' = -1 + I, J' = Q2, M' = R2, I1' = S2, M1' = C, N1' = O2, O1' = 1 + D, P1' = -1 + I, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t90 := {
    from   := f35;
    to     := f34;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && 0 > T2 && O2 > 0 && P2 > 0 && 0 > S2;
    action := E' = N2, F' = P2, G' = 0, D' = 1 + D, I' = -1 + I, J' = Q2, M' = R2, I1' = S2, M1' = C, N1' = O2, O1' = 1 + D, P1' = -1 + I, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t91 := {
    from   := f35;
    to     := f34;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && 0 > T2 && O2 > 0 && P2 > 0 && S2 > 0;
    action := E' = N2, F' = P2, G' = 0, D' = 1 + D, I' = -1 + I, J' = Q2, M' = R2, I1' = S2, M1' = C, N1' = O2, O1' = 1 + D, P1' = -1 + I, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t92 := {
    from   := f35;
    to     := f34;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && T2 > 0 && 0 > O2 && 0 > P2 && 0 > S2;
    action := E' = N2, F' = P2, G' = 0, D' = 1 + D, I' = -1 + I, J' = Q2, M' = R2, I1' = S2, M1' = C, N1' = O2, O1' = 1 + D, P1' = -1 + I, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t93 := {
    from   := f35;
    to     := f34;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && T2 > 0 && 0 > O2 && 0 > P2 && S2 > 0;
    action := E' = N2, F' = P2, G' = 0, D' = 1 + D, I' = -1 + I, J' = Q2, M' = R2, I1' = S2, M1' = C, N1' = O2, O1' = 1 + D, P1' = -1 + I, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t94 := {
    from   := f35;
    to     := f34;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && T2 > 0 && 0 > O2 && P2 > 0 && 0 > S2;
    action := E' = N2, F' = P2, G' = 0, D' = 1 + D, I' = -1 + I, J' = Q2, M' = R2, I1' = S2, M1' = C, N1' = O2, O1' = 1 + D, P1' = -1 + I, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t95 := {
    from   := f35;
    to     := f34;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && T2 > 0 && 0 > O2 && P2 > 0 && S2 > 0;
    action := E' = N2, F' = P2, G' = 0, D' = 1 + D, I' = -1 + I, J' = Q2, M' = R2, I1' = S2, M1' = C, N1' = O2, O1' = 1 + D, P1' = -1 + I, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t96 := {
    from   := f35;
    to     := f34;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && T2 > 0 && O2 > 0 && 0 > P2 && 0 > S2;
    action := E' = N2, F' = P2, G' = 0, D' = 1 + D, I' = -1 + I, J' = Q2, M' = R2, I1' = S2, M1' = C, N1' = O2, O1' = 1 + D, P1' = -1 + I, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t97 := {
    from   := f35;
    to     := f34;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && T2 > 0 && O2 > 0 && 0 > P2 && S2 > 0;
    action := E' = N2, F' = P2, G' = 0, D' = 1 + D, I' = -1 + I, J' = Q2, M' = R2, I1' = S2, M1' = C, N1' = O2, O1' = 1 + D, P1' = -1 + I, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t98 := {
    from   := f35;
    to     := f34;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && T2 > 0 && O2 > 0 && P2 > 0 && 0 > S2;
    action := E' = N2, F' = P2, G' = 0, D' = 1 + D, I' = -1 + I, J' = Q2, M' = R2, I1' = S2, M1' = C, N1' = O2, O1' = 1 + D, P1' = -1 + I, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t99 := {
    from   := f35;
    to     := f34;
    guard  := D >= 0 && B > 0 && I >= 0 && N2 > 1 && T2 > 0 && O2 > 0 && P2 > 0 && S2 > 0;
    action := E' = N2, F' = P2, G' = 0, D' = 1 + D, I' = -1 + I, J' = Q2, M' = R2, I1' = S2, M1' = C, N1' = O2, O1' = 1 + D, P1' = -1 + I, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t100 := {
    from   := f1;
    to     := f1;
    guard  := Q1 > A && A >= 0;
    action := A' = 1 + A, R1' = S1, T1' = S1, S1' = N2, U1' = P2, V1' = A, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t101 := {
    from   := f1;
    to     := f29;
    guard  := A >= Q1 && A >= 0 && P2 >= N2 && N2 > 1;
    action := E' = N2, C' = R1, F' = R1, A' = P2, Q1' = Q2, R1' = R2, W1' = S2, T1' = O2, S1' = T2, X1' = U2, Y1' = V2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t102 := {
    from   := f11;
    to     := f27;
    guard  := 0 >= U2 && N2 > 1 && 0 > P2 && 0 > V2 && Z1 = A2;
    action := E' = N2, C' = P2, B2' = Q2, C2' = R2, D2' = S2, Z1' = O2, A2' = T2, F' = P2, B' = U2, G' = V2, Y1' = W2, E2' = X2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t103 := {
    from   := f11;
    to     := f27;
    guard  := 0 >= U2 && N2 > 1 && 0 > P2 && V2 > 0 && Z1 = A2;
    action := E' = N2, C' = P2, B2' = Q2, C2' = R2, D2' = S2, Z1' = O2, A2' = T2, F' = P2, B' = U2, G' = V2, Y1' = W2, E2' = X2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t104 := {
    from   := f11;
    to     := f27;
    guard  := 0 >= U2 && N2 > 1 && P2 > 0 && 0 > V2 && Z1 = A2;
    action := E' = N2, C' = P2, B2' = Q2, C2' = R2, D2' = S2, Z1' = O2, A2' = T2, F' = P2, B' = U2, G' = V2, Y1' = W2, E2' = X2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t105 := {
    from   := f11;
    to     := f27;
    guard  := 0 >= U2 && N2 > 1 && P2 > 0 && V2 > 0 && Z1 = A2;
    action := E' = N2, C' = P2, B2' = Q2, C2' = R2, D2' = S2, Z1' = O2, A2' = T2, F' = P2, B' = U2, G' = V2, Y1' = W2, E2' = X2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t106 := {
    from   := f12;
    to     := f27;
    guard  := 0 >= V2 && N2 > 1 && 0 > W2 && 0 > U2 && 0 > Y2 && Z2 > 0 && 0 > P2 && Z1 = A2;
    action := E' = N2, C' = P2, B2' = Q2, C2' = R2, D2' = S2, Z1' = O2, A2' = T2, F' = U2, B' = V2, G' = W2, Y1' = X2, E2' = Y2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t107 := {
    from   := f12;
    to     := f27;
    guard  := 0 >= V2 && N2 > 1 && 0 > W2 && 0 > U2 && 0 > Y2 && Z2 > 0 && P2 > 0 && Z1 = A2;
    action := E' = N2, C' = P2, B2' = Q2, C2' = R2, D2' = S2, Z1' = O2, A2' = T2, F' = U2, B' = V2, G' = W2, Y1' = X2, E2' = Y2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t108 := {
    from   := f12;
    to     := f27;
    guard  := 0 >= V2 && N2 > 1 && 0 > W2 && 0 > U2 && 0 > Y2 && 0 > Z2 && 0 > P2 && Z1 = A2;
    action := E' = N2, C' = P2, B2' = Q2, C2' = R2, D2' = S2, Z1' = O2, A2' = T2, F' = U2, B' = V2, G' = W2, Y1' = X2, E2' = Y2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t109 := {
    from   := f12;
    to     := f27;
    guard  := 0 >= V2 && N2 > 1 && 0 > W2 && 0 > U2 && 0 > Y2 && 0 > Z2 && P2 > 0 && Z1 = A2;
    action := E' = N2, C' = P2, B2' = Q2, C2' = R2, D2' = S2, Z1' = O2, A2' = T2, F' = U2, B' = V2, G' = W2, Y1' = X2, E2' = Y2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t110 := {
    from   := f12;
    to     := f27;
    guard  := 0 >= V2 && N2 > 1 && 0 > W2 && 0 > U2 && Y2 > 0 && Z2 > 0 && 0 > P2 && Z1 = A2;
    action := E' = N2, C' = P2, B2' = Q2, C2' = R2, D2' = S2, Z1' = O2, A2' = T2, F' = U2, B' = V2, G' = W2, Y1' = X2, E2' = Y2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t111 := {
    from   := f12;
    to     := f27;
    guard  := 0 >= V2 && N2 > 1 && 0 > W2 && 0 > U2 && Y2 > 0 && Z2 > 0 && P2 > 0 && Z1 = A2;
    action := E' = N2, C' = P2, B2' = Q2, C2' = R2, D2' = S2, Z1' = O2, A2' = T2, F' = U2, B' = V2, G' = W2, Y1' = X2, E2' = Y2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t112 := {
    from   := f12;
    to     := f27;
    guard  := 0 >= V2 && N2 > 1 && 0 > W2 && 0 > U2 && Y2 > 0 && 0 > Z2 && 0 > P2 && Z1 = A2;
    action := E' = N2, C' = P2, B2' = Q2, C2' = R2, D2' = S2, Z1' = O2, A2' = T2, F' = U2, B' = V2, G' = W2, Y1' = X2, E2' = Y2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t113 := {
    from   := f12;
    to     := f27;
    guard  := 0 >= V2 && N2 > 1 && 0 > W2 && 0 > U2 && Y2 > 0 && 0 > Z2 && P2 > 0 && Z1 = A2;
    action := E' = N2, C' = P2, B2' = Q2, C2' = R2, D2' = S2, Z1' = O2, A2' = T2, F' = U2, B' = V2, G' = W2, Y1' = X2, E2' = Y2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t114 := {
    from   := f12;
    to     := f27;
    guard  := 0 >= V2 && N2 > 1 && 0 > W2 && U2 > 0 && 0 > Y2 && Z2 > 0 && 0 > P2 && Z1 = A2;
    action := E' = N2, C' = P2, B2' = Q2, C2' = R2, D2' = S2, Z1' = O2, A2' = T2, F' = U2, B' = V2, G' = W2, Y1' = X2, E2' = Y2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t115 := {
    from   := f12;
    to     := f27;
    guard  := 0 >= V2 && N2 > 1 && 0 > W2 && U2 > 0 && 0 > Y2 && Z2 > 0 && P2 > 0 && Z1 = A2;
    action := E' = N2, C' = P2, B2' = Q2, C2' = R2, D2' = S2, Z1' = O2, A2' = T2, F' = U2, B' = V2, G' = W2, Y1' = X2, E2' = Y2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t116 := {
    from   := f12;
    to     := f27;
    guard  := 0 >= V2 && N2 > 1 && 0 > W2 && U2 > 0 && 0 > Y2 && 0 > Z2 && 0 > P2 && Z1 = A2;
    action := E' = N2, C' = P2, B2' = Q2, C2' = R2, D2' = S2, Z1' = O2, A2' = T2, F' = U2, B' = V2, G' = W2, Y1' = X2, E2' = Y2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t117 := {
    from   := f12;
    to     := f27;
    guard  := 0 >= V2 && N2 > 1 && 0 > W2 && U2 > 0 && 0 > Y2 && 0 > Z2 && P2 > 0 && Z1 = A2;
    action := E' = N2, C' = P2, B2' = Q2, C2' = R2, D2' = S2, Z1' = O2, A2' = T2, F' = U2, B' = V2, G' = W2, Y1' = X2, E2' = Y2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t118 := {
    from   := f12;
    to     := f27;
    guard  := 0 >= V2 && N2 > 1 && 0 > W2 && U2 > 0 && Y2 > 0 && Z2 > 0 && 0 > P2 && Z1 = A2;
    action := E' = N2, C' = P2, B2' = Q2, C2' = R2, D2' = S2, Z1' = O2, A2' = T2, F' = U2, B' = V2, G' = W2, Y1' = X2, E2' = Y2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t119 := {
    from   := f12;
    to     := f27;
    guard  := 0 >= V2 && N2 > 1 && 0 > W2 && U2 > 0 && Y2 > 0 && Z2 > 0 && P2 > 0 && Z1 = A2;
    action := E' = N2, C' = P2, B2' = Q2, C2' = R2, D2' = S2, Z1' = O2, A2' = T2, F' = U2, B' = V2, G' = W2, Y1' = X2, E2' = Y2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t120 := {
    from   := f12;
    to     := f27;
    guard  := 0 >= V2 && N2 > 1 && 0 > W2 && U2 > 0 && Y2 > 0 && 0 > Z2 && 0 > P2 && Z1 = A2;
    action := E' = N2, C' = P2, B2' = Q2, C2' = R2, D2' = S2, Z1' = O2, A2' = T2, F' = U2, B' = V2, G' = W2, Y1' = X2, E2' = Y2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t121 := {
    from   := f12;
    to     := f27;
    guard  := 0 >= V2 && N2 > 1 && 0 > W2 && U2 > 0 && Y2 > 0 && 0 > Z2 && P2 > 0 && Z1 = A2;
    action := E' = N2, C' = P2, B2' = Q2, C2' = R2, D2' = S2, Z1' = O2, A2' = T2, F' = U2, B' = V2, G' = W2, Y1' = X2, E2' = Y2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t122 := {
    from   := f12;
    to     := f27;
    guard  := 0 >= V2 && N2 > 1 && W2 > 0 && 0 > U2 && 0 > Y2 && Z2 > 0 && 0 > P2 && Z1 = A2;
    action := E' = N2, C' = P2, B2' = Q2, C2' = R2, D2' = S2, Z1' = O2, A2' = T2, F' = U2, B' = V2, G' = W2, Y1' = X2, E2' = Y2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t123 := {
    from   := f12;
    to     := f27;
    guard  := 0 >= V2 && N2 > 1 && W2 > 0 && 0 > U2 && 0 > Y2 && Z2 > 0 && P2 > 0 && Z1 = A2;
    action := E' = N2, C' = P2, B2' = Q2, C2' = R2, D2' = S2, Z1' = O2, A2' = T2, F' = U2, B' = V2, G' = W2, Y1' = X2, E2' = Y2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t124 := {
    from   := f12;
    to     := f27;
    guard  := 0 >= V2 && N2 > 1 && W2 > 0 && 0 > U2 && 0 > Y2 && 0 > Z2 && 0 > P2 && Z1 = A2;
    action := E' = N2, C' = P2, B2' = Q2, C2' = R2, D2' = S2, Z1' = O2, A2' = T2, F' = U2, B' = V2, G' = W2, Y1' = X2, E2' = Y2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t125 := {
    from   := f12;
    to     := f27;
    guard  := 0 >= V2 && N2 > 1 && W2 > 0 && 0 > U2 && 0 > Y2 && 0 > Z2 && P2 > 0 && Z1 = A2;
    action := E' = N2, C' = P2, B2' = Q2, C2' = R2, D2' = S2, Z1' = O2, A2' = T2, F' = U2, B' = V2, G' = W2, Y1' = X2, E2' = Y2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t126 := {
    from   := f12;
    to     := f27;
    guard  := 0 >= V2 && N2 > 1 && W2 > 0 && 0 > U2 && Y2 > 0 && Z2 > 0 && 0 > P2 && Z1 = A2;
    action := E' = N2, C' = P2, B2' = Q2, C2' = R2, D2' = S2, Z1' = O2, A2' = T2, F' = U2, B' = V2, G' = W2, Y1' = X2, E2' = Y2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t127 := {
    from   := f12;
    to     := f27;
    guard  := 0 >= V2 && N2 > 1 && W2 > 0 && 0 > U2 && Y2 > 0 && Z2 > 0 && P2 > 0 && Z1 = A2;
    action := E' = N2, C' = P2, B2' = Q2, C2' = R2, D2' = S2, Z1' = O2, A2' = T2, F' = U2, B' = V2, G' = W2, Y1' = X2, E2' = Y2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t128 := {
    from   := f12;
    to     := f27;
    guard  := 0 >= V2 && N2 > 1 && W2 > 0 && 0 > U2 && Y2 > 0 && 0 > Z2 && 0 > P2 && Z1 = A2;
    action := E' = N2, C' = P2, B2' = Q2, C2' = R2, D2' = S2, Z1' = O2, A2' = T2, F' = U2, B' = V2, G' = W2, Y1' = X2, E2' = Y2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t129 := {
    from   := f12;
    to     := f27;
    guard  := 0 >= V2 && N2 > 1 && W2 > 0 && 0 > U2 && Y2 > 0 && 0 > Z2 && P2 > 0 && Z1 = A2;
    action := E' = N2, C' = P2, B2' = Q2, C2' = R2, D2' = S2, Z1' = O2, A2' = T2, F' = U2, B' = V2, G' = W2, Y1' = X2, E2' = Y2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t130 := {
    from   := f12;
    to     := f27;
    guard  := 0 >= V2 && N2 > 1 && W2 > 0 && U2 > 0 && 0 > Y2 && Z2 > 0 && 0 > P2 && Z1 = A2;
    action := E' = N2, C' = P2, B2' = Q2, C2' = R2, D2' = S2, Z1' = O2, A2' = T2, F' = U2, B' = V2, G' = W2, Y1' = X2, E2' = Y2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t131 := {
    from   := f12;
    to     := f27;
    guard  := 0 >= V2 && N2 > 1 && W2 > 0 && U2 > 0 && 0 > Y2 && Z2 > 0 && P2 > 0 && Z1 = A2;
    action := E' = N2, C' = P2, B2' = Q2, C2' = R2, D2' = S2, Z1' = O2, A2' = T2, F' = U2, B' = V2, G' = W2, Y1' = X2, E2' = Y2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t132 := {
    from   := f12;
    to     := f27;
    guard  := 0 >= V2 && N2 > 1 && W2 > 0 && U2 > 0 && 0 > Y2 && 0 > Z2 && 0 > P2 && Z1 = A2;
    action := E' = N2, C' = P2, B2' = Q2, C2' = R2, D2' = S2, Z1' = O2, A2' = T2, F' = U2, B' = V2, G' = W2, Y1' = X2, E2' = Y2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t133 := {
    from   := f12;
    to     := f27;
    guard  := 0 >= V2 && N2 > 1 && W2 > 0 && U2 > 0 && 0 > Y2 && 0 > Z2 && P2 > 0 && Z1 = A2;
    action := E' = N2, C' = P2, B2' = Q2, C2' = R2, D2' = S2, Z1' = O2, A2' = T2, F' = U2, B' = V2, G' = W2, Y1' = X2, E2' = Y2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t134 := {
    from   := f12;
    to     := f27;
    guard  := 0 >= V2 && N2 > 1 && W2 > 0 && U2 > 0 && Y2 > 0 && Z2 > 0 && 0 > P2 && Z1 = A2;
    action := E' = N2, C' = P2, B2' = Q2, C2' = R2, D2' = S2, Z1' = O2, A2' = T2, F' = U2, B' = V2, G' = W2, Y1' = X2, E2' = Y2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t135 := {
    from   := f12;
    to     := f27;
    guard  := 0 >= V2 && N2 > 1 && W2 > 0 && U2 > 0 && Y2 > 0 && Z2 > 0 && P2 > 0 && Z1 = A2;
    action := E' = N2, C' = P2, B2' = Q2, C2' = R2, D2' = S2, Z1' = O2, A2' = T2, F' = U2, B' = V2, G' = W2, Y1' = X2, E2' = Y2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t136 := {
    from   := f12;
    to     := f27;
    guard  := 0 >= V2 && N2 > 1 && W2 > 0 && U2 > 0 && Y2 > 0 && 0 > Z2 && 0 > P2 && Z1 = A2;
    action := E' = N2, C' = P2, B2' = Q2, C2' = R2, D2' = S2, Z1' = O2, A2' = T2, F' = U2, B' = V2, G' = W2, Y1' = X2, E2' = Y2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t137 := {
    from   := f12;
    to     := f27;
    guard  := 0 >= V2 && N2 > 1 && W2 > 0 && U2 > 0 && Y2 > 0 && 0 > Z2 && P2 > 0 && Z1 = A2;
    action := E' = N2, C' = P2, B2' = Q2, C2' = R2, D2' = S2, Z1' = O2, A2' = T2, F' = U2, B' = V2, G' = W2, Y1' = X2, E2' = Y2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t138 := {
    from   := f14;
    to     := f15;
    guard  := R2 > A2 && F2 >= 0 && N2 > 1 && Q2 > 0 && P2 > R2 && 0 > P2 && Z1 = 0;
    action := E' = N2, C' = 0, B2' = P2, C2' = 0, D2' = P2, Z1' = 0, F' = P2, B' = Q2, G' = 0, E2' = A2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t139 := {
    from   := f14;
    to     := f15;
    guard  := R2 > A2 && F2 >= 0 && N2 > 1 && Q2 > 0 && P2 > R2 && P2 > 0 && Z1 = 0;
    action := E' = N2, C' = 0, B2' = P2, C2' = 0, D2' = P2, Z1' = 0, F' = P2, B' = Q2, G' = 0, E2' = A2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t140 := {
    from   := f14;
    to     := f15;
    guard  := R2 > A2 && F2 >= 0 && N2 > 1 && Q2 > 0 && R2 > P2 && 0 > P2 && Z1 = 0;
    action := E' = N2, C' = 0, B2' = P2, C2' = 0, D2' = P2, Z1' = 0, F' = P2, B' = Q2, G' = 0, E2' = A2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t141 := {
    from   := f14;
    to     := f15;
    guard  := R2 > A2 && F2 >= 0 && N2 > 1 && Q2 > 0 && R2 > P2 && P2 > 0 && Z1 = 0;
    action := E' = N2, C' = 0, B2' = P2, C2' = 0, D2' = P2, Z1' = 0, F' = P2, B' = Q2, G' = 0, E2' = A2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t142 := {
    from   := f14;
    to     := f15;
    guard  := A2 > R2 && F2 >= 0 && N2 > 1 && Q2 > 0 && P2 > R2 && 0 > P2 && Z1 = 0;
    action := E' = N2, C' = 0, B2' = P2, C2' = 0, D2' = P2, Z1' = 0, F' = P2, B' = Q2, G' = 0, E2' = A2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t143 := {
    from   := f14;
    to     := f15;
    guard  := A2 > R2 && F2 >= 0 && N2 > 1 && Q2 > 0 && P2 > R2 && P2 > 0 && Z1 = 0;
    action := E' = N2, C' = 0, B2' = P2, C2' = 0, D2' = P2, Z1' = 0, F' = P2, B' = Q2, G' = 0, E2' = A2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t144 := {
    from   := f14;
    to     := f15;
    guard  := A2 > R2 && F2 >= 0 && N2 > 1 && Q2 > 0 && R2 > P2 && 0 > P2 && Z1 = 0;
    action := E' = N2, C' = 0, B2' = P2, C2' = 0, D2' = P2, Z1' = 0, F' = P2, B' = Q2, G' = 0, E2' = A2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t145 := {
    from   := f14;
    to     := f15;
    guard  := A2 > R2 && F2 >= 0 && N2 > 1 && Q2 > 0 && R2 > P2 && P2 > 0 && Z1 = 0;
    action := E' = N2, C' = 0, B2' = P2, C2' = 0, D2' = P2, Z1' = 0, F' = P2, B' = Q2, G' = 0, E2' = A2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t146 := {
    from   := f14;
    to     := f27;
    guard  := F2 >= 0 && N2 > 1 && 0 > T2 && U2 > 0 && Z1 = A2;
    action := E' = N2, B2' = P2, C2' = Q2, D2' = R2, Z1' = S2, A2' = O2, F' = T2, B' = U2, Y1' = V2, E2' = W2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t147 := {
    from   := f14;
    to     := f27;
    guard  := F2 >= 0 && N2 > 1 && T2 > 0 && U2 > 0 && Z1 = A2;
    action := E' = N2, B2' = P2, C2' = Q2, D2' = R2, Z1' = S2, A2' = O2, F' = T2, B' = U2, Y1' = V2, E2' = W2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t148 := {
    from   := f15;
    to     := f15;
    guard  := S2 > A2 && G2 >= 0 && N2 > 1 && Q2 > 0 && P2 > S2 && 0 > P2 && Z1 = 0;
    action := E' = N2, C' = 0, B2' = P2, C2' = 0, D2' = P2, Z1' = 0, F' = P2, B' = Q2, G' = 0, J' = R2, E2' = A2, G2' = -1 + G2, H2' = -1 + G2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t149 := {
    from   := f15;
    to     := f15;
    guard  := S2 > A2 && G2 >= 0 && N2 > 1 && Q2 > 0 && P2 > S2 && P2 > 0 && Z1 = 0;
    action := E' = N2, C' = 0, B2' = P2, C2' = 0, D2' = P2, Z1' = 0, F' = P2, B' = Q2, G' = 0, J' = R2, E2' = A2, G2' = -1 + G2, H2' = -1 + G2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t150 := {
    from   := f15;
    to     := f15;
    guard  := S2 > A2 && G2 >= 0 && N2 > 1 && Q2 > 0 && S2 > P2 && 0 > P2 && Z1 = 0;
    action := E' = N2, C' = 0, B2' = P2, C2' = 0, D2' = P2, Z1' = 0, F' = P2, B' = Q2, G' = 0, J' = R2, E2' = A2, G2' = -1 + G2, H2' = -1 + G2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t151 := {
    from   := f15;
    to     := f15;
    guard  := S2 > A2 && G2 >= 0 && N2 > 1 && Q2 > 0 && S2 > P2 && P2 > 0 && Z1 = 0;
    action := E' = N2, C' = 0, B2' = P2, C2' = 0, D2' = P2, Z1' = 0, F' = P2, B' = Q2, G' = 0, J' = R2, E2' = A2, G2' = -1 + G2, H2' = -1 + G2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t152 := {
    from   := f15;
    to     := f15;
    guard  := A2 > S2 && G2 >= 0 && N2 > 1 && Q2 > 0 && P2 > S2 && 0 > P2 && Z1 = 0;
    action := E' = N2, C' = 0, B2' = P2, C2' = 0, D2' = P2, Z1' = 0, F' = P2, B' = Q2, G' = 0, J' = R2, E2' = A2, G2' = -1 + G2, H2' = -1 + G2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t153 := {
    from   := f15;
    to     := f15;
    guard  := A2 > S2 && G2 >= 0 && N2 > 1 && Q2 > 0 && P2 > S2 && P2 > 0 && Z1 = 0;
    action := E' = N2, C' = 0, B2' = P2, C2' = 0, D2' = P2, Z1' = 0, F' = P2, B' = Q2, G' = 0, J' = R2, E2' = A2, G2' = -1 + G2, H2' = -1 + G2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t154 := {
    from   := f15;
    to     := f15;
    guard  := A2 > S2 && G2 >= 0 && N2 > 1 && Q2 > 0 && S2 > P2 && 0 > P2 && Z1 = 0;
    action := E' = N2, C' = 0, B2' = P2, C2' = 0, D2' = P2, Z1' = 0, F' = P2, B' = Q2, G' = 0, J' = R2, E2' = A2, G2' = -1 + G2, H2' = -1 + G2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t155 := {
    from   := f15;
    to     := f15;
    guard  := A2 > S2 && G2 >= 0 && N2 > 1 && Q2 > 0 && S2 > P2 && P2 > 0 && Z1 = 0;
    action := E' = N2, C' = 0, B2' = P2, C2' = 0, D2' = P2, Z1' = 0, F' = P2, B' = Q2, G' = 0, J' = R2, E2' = A2, G2' = -1 + G2, H2' = -1 + G2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t156 := {
    from   := f15;
    to     := f27;
    guard  := G2 >= 0 && N2 > 1 && U2 > 0 && 0 > T2 && 0 > W2 && Z1 = A2;
    action := E' = N2, B2' = P2, C2' = Q2, D2' = R2, Z1' = S2, A2' = O2, F' = T2, B' = U2, Y1' = V2, E2' = W2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t157 := {
    from   := f15;
    to     := f27;
    guard  := G2 >= 0 && N2 > 1 && U2 > 0 && 0 > T2 && W2 > 0 && Z1 = A2;
    action := E' = N2, B2' = P2, C2' = Q2, D2' = R2, Z1' = S2, A2' = O2, F' = T2, B' = U2, Y1' = V2, E2' = W2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t158 := {
    from   := f15;
    to     := f27;
    guard  := G2 >= 0 && N2 > 1 && U2 > 0 && T2 > 0 && 0 > W2 && Z1 = A2;
    action := E' = N2, B2' = P2, C2' = Q2, D2' = R2, Z1' = S2, A2' = O2, F' = T2, B' = U2, Y1' = V2, E2' = W2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t159 := {
    from   := f15;
    to     := f27;
    guard  := G2 >= 0 && N2 > 1 && U2 > 0 && T2 > 0 && W2 > 0 && Z1 = A2;
    action := E' = N2, B2' = P2, C2' = Q2, D2' = R2, Z1' = S2, A2' = O2, F' = T2, B' = U2, Y1' = V2, E2' = W2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t160 := {
    from   := f16;
    to     := f17;
    guard  := R2 > A2 && I2 >= 0 && 0 >= Q2 && N2 > 1 && P2 > R2 && 0 > P2 && Z1 = 0;
    action := E' = N2, C' = P2, B2' = P2, C2' = 0, D2' = P2, Z1' = 0, F' = P2, B' = Q2, E2' = A2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t161 := {
    from   := f16;
    to     := f17;
    guard  := R2 > A2 && I2 >= 0 && 0 >= Q2 && N2 > 1 && P2 > R2 && P2 > 0 && Z1 = 0;
    action := E' = N2, C' = P2, B2' = P2, C2' = 0, D2' = P2, Z1' = 0, F' = P2, B' = Q2, E2' = A2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t162 := {
    from   := f16;
    to     := f17;
    guard  := R2 > A2 && I2 >= 0 && 0 >= Q2 && N2 > 1 && R2 > P2 && 0 > P2 && Z1 = 0;
    action := E' = N2, C' = P2, B2' = P2, C2' = 0, D2' = P2, Z1' = 0, F' = P2, B' = Q2, E2' = A2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t163 := {
    from   := f16;
    to     := f17;
    guard  := R2 > A2 && I2 >= 0 && 0 >= Q2 && N2 > 1 && R2 > P2 && P2 > 0 && Z1 = 0;
    action := E' = N2, C' = P2, B2' = P2, C2' = 0, D2' = P2, Z1' = 0, F' = P2, B' = Q2, E2' = A2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t164 := {
    from   := f16;
    to     := f17;
    guard  := A2 > R2 && I2 >= 0 && 0 >= Q2 && N2 > 1 && P2 > R2 && 0 > P2 && Z1 = 0;
    action := E' = N2, C' = P2, B2' = P2, C2' = 0, D2' = P2, Z1' = 0, F' = P2, B' = Q2, E2' = A2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t165 := {
    from   := f16;
    to     := f17;
    guard  := A2 > R2 && I2 >= 0 && 0 >= Q2 && N2 > 1 && P2 > R2 && P2 > 0 && Z1 = 0;
    action := E' = N2, C' = P2, B2' = P2, C2' = 0, D2' = P2, Z1' = 0, F' = P2, B' = Q2, E2' = A2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t166 := {
    from   := f16;
    to     := f17;
    guard  := A2 > R2 && I2 >= 0 && 0 >= Q2 && N2 > 1 && R2 > P2 && 0 > P2 && Z1 = 0;
    action := E' = N2, C' = P2, B2' = P2, C2' = 0, D2' = P2, Z1' = 0, F' = P2, B' = Q2, E2' = A2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t167 := {
    from   := f16;
    to     := f17;
    guard  := A2 > R2 && I2 >= 0 && 0 >= Q2 && N2 > 1 && R2 > P2 && P2 > 0 && Z1 = 0;
    action := E' = N2, C' = P2, B2' = P2, C2' = 0, D2' = P2, Z1' = 0, F' = P2, B' = Q2, E2' = A2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t168 := {
    from   := f16;
    to     := f27;
    guard  := I2 >= 0 && 0 >= U2 && 0 > P2 && N2 > 1 && Z1 = A2;
    action := E' = N2, C' = P2, B2' = Q2, C2' = R2, D2' = S2, Z1' = O2, A2' = T2, B' = U2, Y1' = V2, E2' = W2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t169 := {
    from   := f16;
    to     := f27;
    guard  := I2 >= 0 && 0 >= U2 && P2 > 0 && N2 > 1 && Z1 = A2;
    action := E' = N2, C' = P2, B2' = Q2, C2' = R2, D2' = S2, Z1' = O2, A2' = T2, B' = U2, Y1' = V2, E2' = W2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t170 := {
    from   := f17;
    to     := f17;
    guard  := S2 > A2 && J2 >= 0 && 0 >= Q2 && N2 > 1 && P2 > S2 && 0 > P2 && Z1 = 0;
    action := E' = N2, C' = P2, B2' = P2, C2' = 0, D2' = P2, Z1' = 0, F' = P2, B' = Q2, J' = R2, E2' = A2, J2' = -1 + J2, K2' = -1 + J2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t171 := {
    from   := f17;
    to     := f17;
    guard  := S2 > A2 && J2 >= 0 && 0 >= Q2 && N2 > 1 && P2 > S2 && P2 > 0 && Z1 = 0;
    action := E' = N2, C' = P2, B2' = P2, C2' = 0, D2' = P2, Z1' = 0, F' = P2, B' = Q2, J' = R2, E2' = A2, J2' = -1 + J2, K2' = -1 + J2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t172 := {
    from   := f17;
    to     := f17;
    guard  := S2 > A2 && J2 >= 0 && 0 >= Q2 && N2 > 1 && S2 > P2 && 0 > P2 && Z1 = 0;
    action := E' = N2, C' = P2, B2' = P2, C2' = 0, D2' = P2, Z1' = 0, F' = P2, B' = Q2, J' = R2, E2' = A2, J2' = -1 + J2, K2' = -1 + J2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t173 := {
    from   := f17;
    to     := f17;
    guard  := S2 > A2 && J2 >= 0 && 0 >= Q2 && N2 > 1 && S2 > P2 && P2 > 0 && Z1 = 0;
    action := E' = N2, C' = P2, B2' = P2, C2' = 0, D2' = P2, Z1' = 0, F' = P2, B' = Q2, J' = R2, E2' = A2, J2' = -1 + J2, K2' = -1 + J2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t174 := {
    from   := f17;
    to     := f17;
    guard  := A2 > S2 && J2 >= 0 && 0 >= Q2 && N2 > 1 && P2 > S2 && 0 > P2 && Z1 = 0;
    action := E' = N2, C' = P2, B2' = P2, C2' = 0, D2' = P2, Z1' = 0, F' = P2, B' = Q2, J' = R2, E2' = A2, J2' = -1 + J2, K2' = -1 + J2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t175 := {
    from   := f17;
    to     := f17;
    guard  := A2 > S2 && J2 >= 0 && 0 >= Q2 && N2 > 1 && P2 > S2 && P2 > 0 && Z1 = 0;
    action := E' = N2, C' = P2, B2' = P2, C2' = 0, D2' = P2, Z1' = 0, F' = P2, B' = Q2, J' = R2, E2' = A2, J2' = -1 + J2, K2' = -1 + J2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t176 := {
    from   := f17;
    to     := f17;
    guard  := A2 > S2 && J2 >= 0 && 0 >= Q2 && N2 > 1 && S2 > P2 && 0 > P2 && Z1 = 0;
    action := E' = N2, C' = P2, B2' = P2, C2' = 0, D2' = P2, Z1' = 0, F' = P2, B' = Q2, J' = R2, E2' = A2, J2' = -1 + J2, K2' = -1 + J2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t177 := {
    from   := f17;
    to     := f17;
    guard  := A2 > S2 && J2 >= 0 && 0 >= Q2 && N2 > 1 && S2 > P2 && P2 > 0 && Z1 = 0;
    action := E' = N2, C' = P2, B2' = P2, C2' = 0, D2' = P2, Z1' = 0, F' = P2, B' = Q2, J' = R2, E2' = A2, J2' = -1 + J2, K2' = -1 + J2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t178 := {
    from   := f17;
    to     := f27;
    guard  := J2 >= 0 && 0 >= U2 && N2 > 1 && 0 > P2 && 0 > W2 && Z1 = A2;
    action := E' = N2, C' = P2, B2' = Q2, C2' = R2, D2' = S2, Z1' = O2, A2' = T2, B' = U2, Y1' = V2, E2' = W2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t179 := {
    from   := f17;
    to     := f27;
    guard  := J2 >= 0 && 0 >= U2 && N2 > 1 && 0 > P2 && W2 > 0 && Z1 = A2;
    action := E' = N2, C' = P2, B2' = Q2, C2' = R2, D2' = S2, Z1' = O2, A2' = T2, B' = U2, Y1' = V2, E2' = W2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t180 := {
    from   := f17;
    to     := f27;
    guard  := J2 >= 0 && 0 >= U2 && N2 > 1 && P2 > 0 && 0 > W2 && Z1 = A2;
    action := E' = N2, C' = P2, B2' = Q2, C2' = R2, D2' = S2, Z1' = O2, A2' = T2, B' = U2, Y1' = V2, E2' = W2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t181 := {
    from   := f17;
    to     := f27;
    guard  := J2 >= 0 && 0 >= U2 && N2 > 1 && P2 > 0 && W2 > 0 && Z1 = A2;
    action := E' = N2, C' = P2, B2' = Q2, C2' = R2, D2' = S2, Z1' = O2, A2' = T2, B' = U2, Y1' = V2, E2' = W2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t182 := {
    from   := f29;
    to     := f17;
    guard  := Q2 >= N2 && 0 >= R2 && S2 > 1 && A >= S2 && 0 >= P2 && A >= 0 && N2 > 1 && 0 >= B && F > 0 && 0 > C && 0 > F;
    action := E' = N2, C' = F, B2' = F, C2' = 0, D2' = F, Z1' = 0, A2' = F, B' = P2, E2' = F, L2' = J2 + 1, I2' = J2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t183 := {
    from   := f29;
    to     := f17;
    guard  := Q2 >= N2 && 0 >= R2 && S2 > 1 && A >= S2 && 0 >= P2 && A >= 0 && N2 > 1 && 0 >= B && F > 0 && 0 > C;
    action := E' = N2, C' = F, B2' = F, C2' = 0, D2' = F, Z1' = 0, A2' = F, B' = P2, E2' = F, L2' = J2 + 1, I2' = J2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t184 := {
    from   := f29;
    to     := f17;
    guard  := Q2 >= N2 && 0 >= R2 && S2 > 1 && A >= S2 && 0 >= P2 && A >= 0 && N2 > 1 && 0 >= B && F > 0 && C > 0 && 0 > F;
    action := E' = N2, C' = F, B2' = F, C2' = 0, D2' = F, Z1' = 0, A2' = F, B' = P2, E2' = F, L2' = J2 + 1, I2' = J2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t185 := {
    from   := f29;
    to     := f17;
    guard  := Q2 >= N2 && 0 >= R2 && S2 > 1 && A >= S2 && 0 >= P2 && A >= 0 && N2 > 1 && 0 >= B && F > 0 && C > 0;
    action := E' = N2, C' = F, B2' = F, C2' = 0, D2' = F, Z1' = 0, A2' = F, B' = P2, E2' = F, L2' = J2 + 1, I2' = J2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t186 := {
    from   := f29;
    to     := f17;
    guard  := Q2 >= N2 && 0 >= R2 && S2 > 1 && A >= S2 && 0 >= P2 && A >= 0 && N2 > 1 && 0 >= B && 0 > F && 0 > C;
    action := E' = N2, C' = F, B2' = F, C2' = 0, D2' = F, Z1' = 0, A2' = F, B' = P2, E2' = F, L2' = J2 + 1, I2' = J2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t187 := {
    from   := f29;
    to     := f17;
    guard  := Q2 >= N2 && 0 >= R2 && S2 > 1 && A >= S2 && 0 >= P2 && A >= 0 && N2 > 1 && 0 >= B && 0 > F && 0 > C && F > 0;
    action := E' = N2, C' = F, B2' = F, C2' = 0, D2' = F, Z1' = 0, A2' = F, B' = P2, E2' = F, L2' = J2 + 1, I2' = J2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t188 := {
    from   := f29;
    to     := f17;
    guard  := Q2 >= N2 && 0 >= R2 && S2 > 1 && A >= S2 && 0 >= P2 && A >= 0 && N2 > 1 && 0 >= B && 0 > F && C > 0;
    action := E' = N2, C' = F, B2' = F, C2' = 0, D2' = F, Z1' = 0, A2' = F, B' = P2, E2' = F, L2' = J2 + 1, I2' = J2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t189 := {
    from   := f29;
    to     := f17;
    guard  := Q2 >= N2 && 0 >= R2 && S2 > 1 && A >= S2 && 0 >= P2 && A >= 0 && N2 > 1 && 0 >= B && 0 > F && C > 0 && F > 0;
    action := E' = N2, C' = F, B2' = F, C2' = 0, D2' = F, Z1' = 0, A2' = F, B' = P2, E2' = F, L2' = J2 + 1, I2' = J2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t190 := {
    from   := f30;
    to     := f15;
    guard  := P2 > 0 && N2 > 1 && F > 0 && Q2 > 0 && R2 > 1 && 0 > F && C = 0 && H = 0 && D = 1;
    action := E' = N2, C' = 0, B2' = F, C2' = 0, D2' = F, Z1' = 0, A2' = F, B' = P2, G' = 0, H' = 0, D' = G2 + 1, E2' = F, F2' = G2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t191 := {
    from   := f30;
    to     := f15;
    guard  := P2 > 0 && N2 > 1 && F > 0 && Q2 > 0 && R2 > 1 && C = 0 && H = 0 && D = 1;
    action := E' = N2, C' = 0, B2' = F, C2' = 0, D2' = F, Z1' = 0, A2' = F, B' = P2, G' = 0, H' = 0, D' = G2 + 1, E2' = F, F2' = G2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t192 := {
    from   := f30;
    to     := f15;
    guard  := P2 > 0 && N2 > 1 && 0 > F && Q2 > 0 && R2 > 1 && C = 0 && H = 0 && D = 1;
    action := E' = N2, C' = 0, B2' = F, C2' = 0, D2' = F, Z1' = 0, A2' = F, B' = P2, G' = 0, H' = 0, D' = G2 + 1, E2' = F, F2' = G2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t193 := {
    from   := f30;
    to     := f15;
    guard  := P2 > 0 && N2 > 1 && 0 > F && Q2 > 0 && R2 > 1 && F > 0 && C = 0 && H = 0 && D = 1;
    action := E' = N2, C' = 0, B2' = F, C2' = 0, D2' = F, Z1' = 0, A2' = F, B' = P2, G' = 0, H' = 0, D' = G2 + 1, E2' = F, F2' = G2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t194 := {
    from   := f34;
    to     := f15;
    guard  := Q2 > 0 && R2 > 1 && P2 > 0 && N2 > 1 && F > 0 && I >= 0 && D >= 0 && 0 > F && C = 0;
    action := E' = N2, C' = 0, B2' = F, C2' = 0, D2' = F, Z1' = 0, A2' = F, B' = P2, G' = 0, D' = G2 + 1, E2' = F, F2' = G2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t195 := {
    from   := f34;
    to     := f15;
    guard  := Q2 > 0 && R2 > 1 && P2 > 0 && N2 > 1 && F > 0 && I >= 0 && D >= 0 && C = 0;
    action := E' = N2, C' = 0, B2' = F, C2' = 0, D2' = F, Z1' = 0, A2' = F, B' = P2, G' = 0, D' = G2 + 1, E2' = F, F2' = G2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t196 := {
    from   := f34;
    to     := f15;
    guard  := Q2 > 0 && R2 > 1 && P2 > 0 && N2 > 1 && 0 > F && I >= 0 && D >= 0 && C = 0;
    action := E' = N2, C' = 0, B2' = F, C2' = 0, D2' = F, Z1' = 0, A2' = F, B' = P2, G' = 0, D' = G2 + 1, E2' = F, F2' = G2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t197 := {
    from   := f34;
    to     := f15;
    guard  := Q2 > 0 && R2 > 1 && P2 > 0 && N2 > 1 && 0 > F && I >= 0 && D >= 0 && F > 0 && C = 0;
    action := E' = N2, C' = 0, B2' = F, C2' = 0, D2' = F, Z1' = 0, A2' = F, B' = P2, G' = 0, D' = G2 + 1, E2' = F, F2' = G2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t198 := {
    from   := f26;
    to     := f1;
    guard  := N2 > 1;
    action := E' = N2, A' = 2, M' = P2, Q1' = N2, R1' = Q2, W1' = Q2, T1' = Q2, S1' = R2, M2' = S2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t199 := {
    from   := f26;
    to     := f32;
    guard  := true;
    action := E' = 1, C' = S1, F' = S1, A' = N2, M' = P2, Q1' = Q2, R1' = R2, W1' = S2, T1' = O2, S1' = T2, X1' = U2, Y1' = V2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
  transition t200 := {
    from   := f26;
    to     := f27;
    guard  := 0 >= N2 && 0 >= A3 && 0 >= B3 && 0 >= C3;
    action := E' = N2, C' = 0, B2' = P2, C2' = Q2, D2' = R2, Z1' = S2, A2' = O2, F' = 0, A' = T2, M' = U2, Q1' = V2, R1' = W2, W1' = X2, T1' = Y2, S1' = Z2, X1' = D3, Y1' = E3, E2' = F3, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?;
  };
}
strategy dumb {
  Region init := { state = f26 };
}