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, G3, H3, I3, J3, K3;
  states f16, f2, f4, f3, f13, f14, f1, f0;
  transition t0 := {
    from   := f16;
    to     := f16;
    guard  := A > B && B >= 0;
    action := C' = D, B' = 1 + B, E' = D, D' = N2, F' = O2, G' = B, H' = I, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t1 := {
    from   := f2;
    to     := f4;
    guard  := J >= 0 && N2 > 1 && 0 > P2 && 0 > K && 0 > Q2 && 0 > L && M = 1;
    action := N' = N2, O' = O2, P' = K, Q' = O2, R' = K, J' = 1 + S, T' = R2, U' = V, W' = I, X' = L, Y' = S2, Z' = T2, A1' = U2, B1' = Q2, C1' = S, M' = 1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t2 := {
    from   := f2;
    to     := f4;
    guard  := J >= 0 && N2 > 1 && 0 > P2 && 0 > K && 0 > Q2 && L > 0 && M = 1;
    action := N' = N2, O' = O2, P' = K, Q' = O2, R' = K, J' = 1 + S, T' = R2, U' = V, W' = I, X' = L, Y' = S2, Z' = T2, A1' = U2, B1' = Q2, C1' = S, M' = 1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t3 := {
    from   := f2;
    to     := f4;
    guard  := J >= 0 && N2 > 1 && 0 > P2 && 0 > K && Q2 > 0 && 0 > L && M = 1;
    action := N' = N2, O' = O2, P' = K, Q' = O2, R' = K, J' = 1 + S, T' = R2, U' = V, W' = I, X' = L, Y' = S2, Z' = T2, A1' = U2, B1' = Q2, C1' = S, M' = 1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t4 := {
    from   := f2;
    to     := f4;
    guard  := J >= 0 && N2 > 1 && 0 > P2 && 0 > K && Q2 > 0 && L > 0 && M = 1;
    action := N' = N2, O' = O2, P' = K, Q' = O2, R' = K, J' = 1 + S, T' = R2, U' = V, W' = I, X' = L, Y' = S2, Z' = T2, A1' = U2, B1' = Q2, C1' = S, M' = 1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t5 := {
    from   := f2;
    to     := f4;
    guard  := J >= 0 && N2 > 1 && 0 > P2 && K > 0 && 0 > Q2 && 0 > L && M = 1;
    action := N' = N2, O' = O2, P' = K, Q' = O2, R' = K, J' = 1 + S, T' = R2, U' = V, W' = I, X' = L, Y' = S2, Z' = T2, A1' = U2, B1' = Q2, C1' = S, M' = 1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t6 := {
    from   := f2;
    to     := f4;
    guard  := J >= 0 && N2 > 1 && 0 > P2 && K > 0 && 0 > Q2 && L > 0 && M = 1;
    action := N' = N2, O' = O2, P' = K, Q' = O2, R' = K, J' = 1 + S, T' = R2, U' = V, W' = I, X' = L, Y' = S2, Z' = T2, A1' = U2, B1' = Q2, C1' = S, M' = 1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t7 := {
    from   := f2;
    to     := f4;
    guard  := J >= 0 && N2 > 1 && 0 > P2 && K > 0 && Q2 > 0 && 0 > L && M = 1;
    action := N' = N2, O' = O2, P' = K, Q' = O2, R' = K, J' = 1 + S, T' = R2, U' = V, W' = I, X' = L, Y' = S2, Z' = T2, A1' = U2, B1' = Q2, C1' = S, M' = 1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t8 := {
    from   := f2;
    to     := f4;
    guard  := J >= 0 && N2 > 1 && 0 > P2 && K > 0 && Q2 > 0 && L > 0 && M = 1;
    action := N' = N2, O' = O2, P' = K, Q' = O2, R' = K, J' = 1 + S, T' = R2, U' = V, W' = I, X' = L, Y' = S2, Z' = T2, A1' = U2, B1' = Q2, C1' = S, M' = 1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t9 := {
    from   := f2;
    to     := f4;
    guard  := J >= 0 && N2 > 1 && P2 > 0 && 0 > K && 0 > Q2 && 0 > L && M = 1;
    action := N' = N2, O' = O2, P' = K, Q' = O2, R' = K, J' = 1 + S, T' = R2, U' = V, W' = I, X' = L, Y' = S2, Z' = T2, A1' = U2, B1' = Q2, C1' = S, M' = 1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t10 := {
    from   := f2;
    to     := f4;
    guard  := J >= 0 && N2 > 1 && P2 > 0 && 0 > K && 0 > Q2 && L > 0 && M = 1;
    action := N' = N2, O' = O2, P' = K, Q' = O2, R' = K, J' = 1 + S, T' = R2, U' = V, W' = I, X' = L, Y' = S2, Z' = T2, A1' = U2, B1' = Q2, C1' = S, M' = 1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t11 := {
    from   := f2;
    to     := f4;
    guard  := J >= 0 && N2 > 1 && P2 > 0 && 0 > K && Q2 > 0 && 0 > L && M = 1;
    action := N' = N2, O' = O2, P' = K, Q' = O2, R' = K, J' = 1 + S, T' = R2, U' = V, W' = I, X' = L, Y' = S2, Z' = T2, A1' = U2, B1' = Q2, C1' = S, M' = 1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t12 := {
    from   := f2;
    to     := f4;
    guard  := J >= 0 && N2 > 1 && P2 > 0 && 0 > K && Q2 > 0 && L > 0 && M = 1;
    action := N' = N2, O' = O2, P' = K, Q' = O2, R' = K, J' = 1 + S, T' = R2, U' = V, W' = I, X' = L, Y' = S2, Z' = T2, A1' = U2, B1' = Q2, C1' = S, M' = 1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t13 := {
    from   := f2;
    to     := f4;
    guard  := J >= 0 && N2 > 1 && P2 > 0 && K > 0 && 0 > Q2 && 0 > L && M = 1;
    action := N' = N2, O' = O2, P' = K, Q' = O2, R' = K, J' = 1 + S, T' = R2, U' = V, W' = I, X' = L, Y' = S2, Z' = T2, A1' = U2, B1' = Q2, C1' = S, M' = 1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t14 := {
    from   := f2;
    to     := f4;
    guard  := J >= 0 && N2 > 1 && P2 > 0 && K > 0 && 0 > Q2 && L > 0 && M = 1;
    action := N' = N2, O' = O2, P' = K, Q' = O2, R' = K, J' = 1 + S, T' = R2, U' = V, W' = I, X' = L, Y' = S2, Z' = T2, A1' = U2, B1' = Q2, C1' = S, M' = 1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t15 := {
    from   := f2;
    to     := f4;
    guard  := J >= 0 && N2 > 1 && P2 > 0 && K > 0 && Q2 > 0 && 0 > L && M = 1;
    action := N' = N2, O' = O2, P' = K, Q' = O2, R' = K, J' = 1 + S, T' = R2, U' = V, W' = I, X' = L, Y' = S2, Z' = T2, A1' = U2, B1' = Q2, C1' = S, M' = 1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t16 := {
    from   := f2;
    to     := f4;
    guard  := J >= 0 && N2 > 1 && P2 > 0 && K > 0 && Q2 > 0 && L > 0 && M = 1;
    action := N' = N2, O' = O2, P' = K, Q' = O2, R' = K, J' = 1 + S, T' = R2, U' = V, W' = I, X' = L, Y' = S2, Z' = T2, A1' = U2, B1' = Q2, C1' = S, M' = 1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t17 := {
    from   := f3;
    to     := f4;
    guard  := C1 >= 0 && N2 > 1 && 0 > L && 0 > S2 && 0 > K;
    action := N' = N2, O' = O2, P' = K, Q' = O2, R' = K, D1' = R2, E1' = S2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t18 := {
    from   := f3;
    to     := f4;
    guard  := C1 >= 0 && N2 > 1 && 0 > L && 0 > S2 && K > 0;
    action := N' = N2, O' = O2, P' = K, Q' = O2, R' = K, D1' = R2, E1' = S2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t19 := {
    from   := f3;
    to     := f4;
    guard  := C1 >= 0 && N2 > 1 && 0 > L && S2 > 0 && 0 > K;
    action := N' = N2, O' = O2, P' = K, Q' = O2, R' = K, D1' = R2, E1' = S2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t20 := {
    from   := f3;
    to     := f4;
    guard  := C1 >= 0 && N2 > 1 && 0 > L && S2 > 0 && K > 0;
    action := N' = N2, O' = O2, P' = K, Q' = O2, R' = K, D1' = R2, E1' = S2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t21 := {
    from   := f3;
    to     := f4;
    guard  := C1 >= 0 && N2 > 1 && L > 0 && 0 > S2 && 0 > K;
    action := N' = N2, O' = O2, P' = K, Q' = O2, R' = K, D1' = R2, E1' = S2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t22 := {
    from   := f3;
    to     := f4;
    guard  := C1 >= 0 && N2 > 1 && L > 0 && 0 > S2 && K > 0;
    action := N' = N2, O' = O2, P' = K, Q' = O2, R' = K, D1' = R2, E1' = S2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t23 := {
    from   := f3;
    to     := f4;
    guard  := C1 >= 0 && N2 > 1 && L > 0 && S2 > 0 && 0 > K;
    action := N' = N2, O' = O2, P' = K, Q' = O2, R' = K, D1' = R2, E1' = S2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t24 := {
    from   := f3;
    to     := f4;
    guard  := C1 >= 0 && N2 > 1 && L > 0 && S2 > 0 && K > 0;
    action := N' = N2, O' = O2, P' = K, Q' = O2, R' = K, D1' = R2, E1' = S2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t25 := {
    from   := f4;
    to     := f4;
    guard  := T2 >= 0 && S >= 0 && N2 > 1 && 0 > U2 && 0 > K && 0 > L && 0 > S2;
    action := N' = N2, O' = O2, P' = K, Q' = O2, R' = K, S' = -1 + S, M' = M + 1, F1' = R2, G1' = S2, H1' = V, I1' = I, J1' = L, K1' = M + 1, L1' = -1 + S, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t26 := {
    from   := f4;
    to     := f4;
    guard  := T2 >= 0 && S >= 0 && N2 > 1 && 0 > U2 && 0 > K && 0 > L && S2 > 0;
    action := N' = N2, O' = O2, P' = K, Q' = O2, R' = K, S' = -1 + S, M' = M + 1, F1' = R2, G1' = S2, H1' = V, I1' = I, J1' = L, K1' = M + 1, L1' = -1 + S, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t27 := {
    from   := f4;
    to     := f4;
    guard  := T2 >= 0 && S >= 0 && N2 > 1 && 0 > U2 && 0 > K && L > 0 && 0 > S2;
    action := N' = N2, O' = O2, P' = K, Q' = O2, R' = K, S' = -1 + S, M' = M + 1, F1' = R2, G1' = S2, H1' = V, I1' = I, J1' = L, K1' = M + 1, L1' = -1 + S, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t28 := {
    from   := f4;
    to     := f4;
    guard  := T2 >= 0 && S >= 0 && N2 > 1 && 0 > U2 && 0 > K && L > 0 && S2 > 0;
    action := N' = N2, O' = O2, P' = K, Q' = O2, R' = K, S' = -1 + S, M' = M + 1, F1' = R2, G1' = S2, H1' = V, I1' = I, J1' = L, K1' = M + 1, L1' = -1 + S, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t29 := {
    from   := f4;
    to     := f4;
    guard  := T2 >= 0 && S >= 0 && N2 > 1 && 0 > U2 && K > 0 && 0 > L && 0 > S2;
    action := N' = N2, O' = O2, P' = K, Q' = O2, R' = K, S' = -1 + S, M' = M + 1, F1' = R2, G1' = S2, H1' = V, I1' = I, J1' = L, K1' = M + 1, L1' = -1 + S, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t30 := {
    from   := f4;
    to     := f4;
    guard  := T2 >= 0 && S >= 0 && N2 > 1 && 0 > U2 && K > 0 && 0 > L && S2 > 0;
    action := N' = N2, O' = O2, P' = K, Q' = O2, R' = K, S' = -1 + S, M' = M + 1, F1' = R2, G1' = S2, H1' = V, I1' = I, J1' = L, K1' = M + 1, L1' = -1 + S, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t31 := {
    from   := f4;
    to     := f4;
    guard  := T2 >= 0 && S >= 0 && N2 > 1 && 0 > U2 && K > 0 && L > 0 && 0 > S2;
    action := N' = N2, O' = O2, P' = K, Q' = O2, R' = K, S' = -1 + S, M' = M + 1, F1' = R2, G1' = S2, H1' = V, I1' = I, J1' = L, K1' = M + 1, L1' = -1 + S, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t32 := {
    from   := f4;
    to     := f4;
    guard  := T2 >= 0 && S >= 0 && N2 > 1 && 0 > U2 && K > 0 && L > 0 && S2 > 0;
    action := N' = N2, O' = O2, P' = K, Q' = O2, R' = K, S' = -1 + S, M' = M + 1, F1' = R2, G1' = S2, H1' = V, I1' = I, J1' = L, K1' = M + 1, L1' = -1 + S, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t33 := {
    from   := f4;
    to     := f4;
    guard  := T2 >= 0 && S >= 0 && N2 > 1 && U2 > 0 && 0 > K && 0 > L && 0 > S2;
    action := N' = N2, O' = O2, P' = K, Q' = O2, R' = K, S' = -1 + S, M' = M + 1, F1' = R2, G1' = S2, H1' = V, I1' = I, J1' = L, K1' = M + 1, L1' = -1 + S, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t34 := {
    from   := f4;
    to     := f4;
    guard  := T2 >= 0 && S >= 0 && N2 > 1 && U2 > 0 && 0 > K && 0 > L && S2 > 0;
    action := N' = N2, O' = O2, P' = K, Q' = O2, R' = K, S' = -1 + S, M' = M + 1, F1' = R2, G1' = S2, H1' = V, I1' = I, J1' = L, K1' = M + 1, L1' = -1 + S, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t35 := {
    from   := f4;
    to     := f4;
    guard  := T2 >= 0 && S >= 0 && N2 > 1 && U2 > 0 && 0 > K && L > 0 && 0 > S2;
    action := N' = N2, O' = O2, P' = K, Q' = O2, R' = K, S' = -1 + S, M' = M + 1, F1' = R2, G1' = S2, H1' = V, I1' = I, J1' = L, K1' = M + 1, L1' = -1 + S, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t36 := {
    from   := f4;
    to     := f4;
    guard  := T2 >= 0 && S >= 0 && N2 > 1 && U2 > 0 && 0 > K && L > 0 && S2 > 0;
    action := N' = N2, O' = O2, P' = K, Q' = O2, R' = K, S' = -1 + S, M' = M + 1, F1' = R2, G1' = S2, H1' = V, I1' = I, J1' = L, K1' = M + 1, L1' = -1 + S, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t37 := {
    from   := f4;
    to     := f4;
    guard  := T2 >= 0 && S >= 0 && N2 > 1 && U2 > 0 && K > 0 && 0 > L && 0 > S2;
    action := N' = N2, O' = O2, P' = K, Q' = O2, R' = K, S' = -1 + S, M' = M + 1, F1' = R2, G1' = S2, H1' = V, I1' = I, J1' = L, K1' = M + 1, L1' = -1 + S, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t38 := {
    from   := f4;
    to     := f4;
    guard  := T2 >= 0 && S >= 0 && N2 > 1 && U2 > 0 && K > 0 && 0 > L && S2 > 0;
    action := N' = N2, O' = O2, P' = K, Q' = O2, R' = K, S' = -1 + S, M' = M + 1, F1' = R2, G1' = S2, H1' = V, I1' = I, J1' = L, K1' = M + 1, L1' = -1 + S, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t39 := {
    from   := f4;
    to     := f4;
    guard  := T2 >= 0 && S >= 0 && N2 > 1 && U2 > 0 && K > 0 && L > 0 && 0 > S2;
    action := N' = N2, O' = O2, P' = K, Q' = O2, R' = K, S' = -1 + S, M' = M + 1, F1' = R2, G1' = S2, H1' = V, I1' = I, J1' = L, K1' = M + 1, L1' = -1 + S, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t40 := {
    from   := f4;
    to     := f4;
    guard  := T2 >= 0 && S >= 0 && N2 > 1 && U2 > 0 && K > 0 && L > 0 && S2 > 0;
    action := N' = N2, O' = O2, P' = K, Q' = O2, R' = K, S' = -1 + S, M' = M + 1, F1' = R2, G1' = S2, H1' = V, I1' = I, J1' = L, K1' = M + 1, L1' = -1 + S, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t41 := {
    from   := f13;
    to     := f14;
    guard  := R2 > M1 && N1 >= 0 && N2 > 1 && O2 > R2 && 0 > O2 && O1 = 0;
    action := N' = N2, P1' = O2, Q1' = 0, R1' = O2, O1' = 0, S1' = O2, T1' = M1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t42 := {
    from   := f13;
    to     := f14;
    guard  := R2 > M1 && N1 >= 0 && N2 > 1 && O2 > R2 && O2 > 0 && O1 = 0;
    action := N' = N2, P1' = O2, Q1' = 0, R1' = O2, O1' = 0, S1' = O2, T1' = M1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t43 := {
    from   := f13;
    to     := f14;
    guard  := R2 > M1 && N1 >= 0 && N2 > 1 && R2 > O2 && 0 > O2 && O1 = 0;
    action := N' = N2, P1' = O2, Q1' = 0, R1' = O2, O1' = 0, S1' = O2, T1' = M1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t44 := {
    from   := f13;
    to     := f14;
    guard  := R2 > M1 && N1 >= 0 && N2 > 1 && R2 > O2 && O2 > 0 && O1 = 0;
    action := N' = N2, P1' = O2, Q1' = 0, R1' = O2, O1' = 0, S1' = O2, T1' = M1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t45 := {
    from   := f13;
    to     := f14;
    guard  := M1 > R2 && N1 >= 0 && N2 > 1 && O2 > R2 && 0 > O2 && O1 = 0;
    action := N' = N2, P1' = O2, Q1' = 0, R1' = O2, O1' = 0, S1' = O2, T1' = M1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t46 := {
    from   := f13;
    to     := f14;
    guard  := M1 > R2 && N1 >= 0 && N2 > 1 && O2 > R2 && O2 > 0 && O1 = 0;
    action := N' = N2, P1' = O2, Q1' = 0, R1' = O2, O1' = 0, S1' = O2, T1' = M1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t47 := {
    from   := f13;
    to     := f14;
    guard  := M1 > R2 && N1 >= 0 && N2 > 1 && R2 > O2 && 0 > O2 && O1 = 0;
    action := N' = N2, P1' = O2, Q1' = 0, R1' = O2, O1' = 0, S1' = O2, T1' = M1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t48 := {
    from   := f13;
    to     := f14;
    guard  := M1 > R2 && N1 >= 0 && N2 > 1 && R2 > O2 && O2 > 0 && O1 = 0;
    action := N' = N2, P1' = O2, Q1' = 0, R1' = O2, O1' = 0, S1' = O2, T1' = M1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t49 := {
    from   := f13;
    to     := f1;
    guard  := N1 >= 0 && 0 > V2 && N2 > 1 && O1 = M1;
    action := N' = N2, U1' = O2, P1' = R2, Q1' = S2, R1' = T2, O1' = U2, M1' = Q2, S1' = P2, T1' = W2, V1' = V2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t50 := {
    from   := f13;
    to     := f1;
    guard  := N1 >= 0 && V2 > 0 && N2 > 1 && O1 = M1;
    action := N' = N2, U1' = O2, P1' = R2, Q1' = S2, R1' = T2, O1' = U2, M1' = Q2, S1' = P2, T1' = W2, V1' = V2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t51 := {
    from   := f14;
    to     := f14;
    guard  := S2 > M1 && W1 >= 0 && N2 > 1 && O2 > S2 && 0 > O2 && O1 = 0;
    action := N' = N2, P1' = O2, Q1' = 0, R1' = O2, O1' = 0, S1' = O2, V' = R2, T1' = M1, W1' = -1 + W1, X1' = I, Y1' = -1 + W1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t52 := {
    from   := f14;
    to     := f14;
    guard  := S2 > M1 && W1 >= 0 && N2 > 1 && O2 > S2 && O2 > 0 && O1 = 0;
    action := N' = N2, P1' = O2, Q1' = 0, R1' = O2, O1' = 0, S1' = O2, V' = R2, T1' = M1, W1' = -1 + W1, X1' = I, Y1' = -1 + W1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t53 := {
    from   := f14;
    to     := f14;
    guard  := S2 > M1 && W1 >= 0 && N2 > 1 && S2 > O2 && 0 > O2 && O1 = 0;
    action := N' = N2, P1' = O2, Q1' = 0, R1' = O2, O1' = 0, S1' = O2, V' = R2, T1' = M1, W1' = -1 + W1, X1' = I, Y1' = -1 + W1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t54 := {
    from   := f14;
    to     := f14;
    guard  := S2 > M1 && W1 >= 0 && N2 > 1 && S2 > O2 && O2 > 0 && O1 = 0;
    action := N' = N2, P1' = O2, Q1' = 0, R1' = O2, O1' = 0, S1' = O2, V' = R2, T1' = M1, W1' = -1 + W1, X1' = I, Y1' = -1 + W1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t55 := {
    from   := f14;
    to     := f14;
    guard  := M1 > S2 && W1 >= 0 && N2 > 1 && O2 > S2 && 0 > O2 && O1 = 0;
    action := N' = N2, P1' = O2, Q1' = 0, R1' = O2, O1' = 0, S1' = O2, V' = R2, T1' = M1, W1' = -1 + W1, X1' = I, Y1' = -1 + W1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t56 := {
    from   := f14;
    to     := f14;
    guard  := M1 > S2 && W1 >= 0 && N2 > 1 && O2 > S2 && O2 > 0 && O1 = 0;
    action := N' = N2, P1' = O2, Q1' = 0, R1' = O2, O1' = 0, S1' = O2, V' = R2, T1' = M1, W1' = -1 + W1, X1' = I, Y1' = -1 + W1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t57 := {
    from   := f14;
    to     := f14;
    guard  := M1 > S2 && W1 >= 0 && N2 > 1 && S2 > O2 && 0 > O2 && O1 = 0;
    action := N' = N2, P1' = O2, Q1' = 0, R1' = O2, O1' = 0, S1' = O2, V' = R2, T1' = M1, W1' = -1 + W1, X1' = I, Y1' = -1 + W1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t58 := {
    from   := f14;
    to     := f14;
    guard  := M1 > S2 && W1 >= 0 && N2 > 1 && S2 > O2 && O2 > 0 && O1 = 0;
    action := N' = N2, P1' = O2, Q1' = 0, R1' = O2, O1' = 0, S1' = O2, V' = R2, T1' = M1, W1' = -1 + W1, X1' = I, Y1' = -1 + W1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t59 := {
    from   := f14;
    to     := f1;
    guard  := N2 > 1 && W1 >= 0 && O1 = M1;
    action := N' = N2, U1' = O2, P1' = R2, Q1' = S2, R1' = T2, O1' = U2, M1' = Q2, S1' = P2, T1' = W2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t60 := {
    from   := f0;
    to     := f16;
    guard  := O2 > 1;
    action := Z1' = N2, N' = O2, A' = O2, C' = R2, B' = 2, A2' = R2, E' = R2, D' = S2, B2' = T2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t61 := {
    from   := f16;
    to     := f4;
    guard  := X2 > 1 && C2 >= X2 && N2 > 1 && C2 >= N2 && B >= A && B >= 0 && C2 >= 0 && 0 > L && M = 0 && K = L;
    action := N' = N2, A' = O2, C' = R2, B' = S2, D2' = T2, U1' = U2, A2' = Q2, E' = P2, D' = W2, O' = V2, P' = K, Q' = V2, C2' = S + 1, R' = K, J' = S, M' = 0, L' = K, E2' = V, F2' = I, G2' = Y2, H2' = Z2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t62 := {
    from   := f16;
    to     := f4;
    guard  := X2 > 1 && C2 >= X2 && N2 > 1 && C2 >= N2 && B >= A && B >= 0 && C2 >= 0 && L > 0 && M = 0 && K = L;
    action := N' = N2, A' = O2, C' = R2, B' = S2, D2' = T2, U1' = U2, A2' = Q2, E' = P2, D' = W2, O' = V2, P' = K, Q' = V2, C2' = S + 1, R' = K, J' = S, M' = 0, L' = K, E2' = V, F2' = I, G2' = Y2, H2' = Z2, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t63 := {
    from   := f2;
    to     := f14;
    guard  := Q2 > 1 && N2 > 1 && S1 > 0 && J >= 0 && 0 > S1 && K = 0 && I2 = 1;
    action := N' = N2, K' = O2, O' = R2, P' = S2, R' = T2, P1' = S1, Q1' = 0, R1' = S1, O1' = 0, M1' = S1, J2' = I, I2' = W1 + 1, T1' = S1, K2' = I, L2' = U2, N1' = W1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t64 := {
    from   := f2;
    to     := f14;
    guard  := Q2 > 1 && N2 > 1 && S1 > 0 && J >= 0 && K = 0 && I2 = 1;
    action := N' = N2, K' = O2, O' = R2, P' = S2, R' = T2, P1' = S1, Q1' = 0, R1' = S1, O1' = 0, M1' = S1, J2' = I, I2' = W1 + 1, T1' = S1, K2' = I, L2' = U2, N1' = W1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t65 := {
    from   := f2;
    to     := f14;
    guard  := Q2 > 1 && N2 > 1 && 0 > S1 && J >= 0 && K = 0 && I2 = 1;
    action := N' = N2, K' = O2, O' = R2, P' = S2, R' = T2, P1' = S1, Q1' = 0, R1' = S1, O1' = 0, M1' = S1, J2' = I, I2' = W1 + 1, T1' = S1, K2' = I, L2' = U2, N1' = W1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t66 := {
    from   := f2;
    to     := f14;
    guard  := Q2 > 1 && N2 > 1 && 0 > S1 && J >= 0 && S1 > 0 && K = 0 && I2 = 1;
    action := N' = N2, K' = O2, O' = R2, P' = S2, R' = T2, P1' = S1, Q1' = 0, R1' = S1, O1' = 0, M1' = S1, J2' = I, I2' = W1 + 1, T1' = S1, K2' = I, L2' = U2, N1' = W1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t67 := {
    from   := f3;
    to     := f14;
    guard  := Q2 > 1 && N2 > 1 && C1 >= 0 && S1 > 0 && 0 > S1 && 0 > L && K = 0 && I2 = 2;
    action := N' = N2, K' = O2, O' = R2, P' = S2, R' = T2, P1' = S1, Q1' = 0, R1' = S1, O1' = 0, M1' = S1, I2' = W1 + 1, M2' = I, T1' = S1, K2' = I, L2' = U2, N1' = W1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t68 := {
    from   := f3;
    to     := f14;
    guard  := Q2 > 1 && N2 > 1 && C1 >= 0 && S1 > 0 && 0 > S1 && L > 0 && K = 0 && I2 = 2;
    action := N' = N2, K' = O2, O' = R2, P' = S2, R' = T2, P1' = S1, Q1' = 0, R1' = S1, O1' = 0, M1' = S1, I2' = W1 + 1, M2' = I, T1' = S1, K2' = I, L2' = U2, N1' = W1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t69 := {
    from   := f3;
    to     := f14;
    guard  := Q2 > 1 && N2 > 1 && C1 >= 0 && S1 > 0 && 0 > L && K = 0 && I2 = 2;
    action := N' = N2, K' = O2, O' = R2, P' = S2, R' = T2, P1' = S1, Q1' = 0, R1' = S1, O1' = 0, M1' = S1, I2' = W1 + 1, M2' = I, T1' = S1, K2' = I, L2' = U2, N1' = W1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t70 := {
    from   := f3;
    to     := f14;
    guard  := Q2 > 1 && N2 > 1 && C1 >= 0 && S1 > 0 && L > 0 && K = 0 && I2 = 2;
    action := N' = N2, K' = O2, O' = R2, P' = S2, R' = T2, P1' = S1, Q1' = 0, R1' = S1, O1' = 0, M1' = S1, I2' = W1 + 1, M2' = I, T1' = S1, K2' = I, L2' = U2, N1' = W1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t71 := {
    from   := f3;
    to     := f14;
    guard  := Q2 > 1 && N2 > 1 && C1 >= 0 && 0 > S1 && 0 > L && K = 0 && I2 = 2;
    action := N' = N2, K' = O2, O' = R2, P' = S2, R' = T2, P1' = S1, Q1' = 0, R1' = S1, O1' = 0, M1' = S1, I2' = W1 + 1, M2' = I, T1' = S1, K2' = I, L2' = U2, N1' = W1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t72 := {
    from   := f3;
    to     := f14;
    guard  := Q2 > 1 && N2 > 1 && C1 >= 0 && 0 > S1 && L > 0 && K = 0 && I2 = 2;
    action := N' = N2, K' = O2, O' = R2, P' = S2, R' = T2, P1' = S1, Q1' = 0, R1' = S1, O1' = 0, M1' = S1, I2' = W1 + 1, M2' = I, T1' = S1, K2' = I, L2' = U2, N1' = W1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t73 := {
    from   := f3;
    to     := f14;
    guard  := Q2 > 1 && N2 > 1 && C1 >= 0 && 0 > S1 && S1 > 0 && 0 > L && K = 0 && I2 = 2;
    action := N' = N2, K' = O2, O' = R2, P' = S2, R' = T2, P1' = S1, Q1' = 0, R1' = S1, O1' = 0, M1' = S1, I2' = W1 + 1, M2' = I, T1' = S1, K2' = I, L2' = U2, N1' = W1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t74 := {
    from   := f3;
    to     := f14;
    guard  := Q2 > 1 && N2 > 1 && C1 >= 0 && 0 > S1 && S1 > 0 && L > 0 && K = 0 && I2 = 2;
    action := N' = N2, K' = O2, O' = R2, P' = S2, R' = T2, P1' = S1, Q1' = 0, R1' = S1, O1' = 0, M1' = S1, I2' = W1 + 1, M2' = I, T1' = S1, K2' = I, L2' = U2, N1' = W1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t75 := {
    from   := f4;
    to     := f14;
    guard  := Q2 > 1 && N2 > 1 && I2 > 0 && S >= 0 && S1 > 0 && I2 >= 0 && 0 > S1 && 0 > L && M + 1 = I2 && K = 0;
    action := N' = N2, K' = O2, O' = R2, P' = S2, R' = T2, P1' = S1, Q1' = 0, R1' = S1, O1' = 0, M1' = S1, I2' = W1 + 1, T1' = S1, K2' = I, L2' = U2, N1' = W1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t76 := {
    from   := f4;
    to     := f14;
    guard  := Q2 > 1 && N2 > 1 && I2 > 0 && S >= 0 && S1 > 0 && I2 >= 0 && 0 > S1 && L > 0 && M + 1 = I2 && K = 0;
    action := N' = N2, K' = O2, O' = R2, P' = S2, R' = T2, P1' = S1, Q1' = 0, R1' = S1, O1' = 0, M1' = S1, I2' = W1 + 1, T1' = S1, K2' = I, L2' = U2, N1' = W1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t77 := {
    from   := f4;
    to     := f14;
    guard  := Q2 > 1 && N2 > 1 && I2 > 0 && S >= 0 && S1 > 0 && I2 >= 0 && 0 > L && M + 1 = I2 && K = 0;
    action := N' = N2, K' = O2, O' = R2, P' = S2, R' = T2, P1' = S1, Q1' = 0, R1' = S1, O1' = 0, M1' = S1, I2' = W1 + 1, T1' = S1, K2' = I, L2' = U2, N1' = W1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t78 := {
    from   := f4;
    to     := f14;
    guard  := Q2 > 1 && N2 > 1 && I2 > 0 && S >= 0 && S1 > 0 && I2 >= 0 && L > 0 && M + 1 = I2 && K = 0;
    action := N' = N2, K' = O2, O' = R2, P' = S2, R' = T2, P1' = S1, Q1' = 0, R1' = S1, O1' = 0, M1' = S1, I2' = W1 + 1, T1' = S1, K2' = I, L2' = U2, N1' = W1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t79 := {
    from   := f4;
    to     := f14;
    guard  := Q2 > 1 && N2 > 1 && I2 > 0 && S >= 0 && 0 > S1 && I2 >= 0 && 0 > L && M + 1 = I2 && K = 0;
    action := N' = N2, K' = O2, O' = R2, P' = S2, R' = T2, P1' = S1, Q1' = 0, R1' = S1, O1' = 0, M1' = S1, I2' = W1 + 1, T1' = S1, K2' = I, L2' = U2, N1' = W1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t80 := {
    from   := f4;
    to     := f14;
    guard  := Q2 > 1 && N2 > 1 && I2 > 0 && S >= 0 && 0 > S1 && I2 >= 0 && L > 0 && M + 1 = I2 && K = 0;
    action := N' = N2, K' = O2, O' = R2, P' = S2, R' = T2, P1' = S1, Q1' = 0, R1' = S1, O1' = 0, M1' = S1, I2' = W1 + 1, T1' = S1, K2' = I, L2' = U2, N1' = W1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t81 := {
    from   := f4;
    to     := f14;
    guard  := Q2 > 1 && N2 > 1 && I2 > 0 && S >= 0 && 0 > S1 && I2 >= 0 && S1 > 0 && 0 > L && M + 1 = I2 && K = 0;
    action := N' = N2, K' = O2, O' = R2, P' = S2, R' = T2, P1' = S1, Q1' = 0, R1' = S1, O1' = 0, M1' = S1, I2' = W1 + 1, T1' = S1, K2' = I, L2' = U2, N1' = W1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t82 := {
    from   := f4;
    to     := f14;
    guard  := Q2 > 1 && N2 > 1 && I2 > 0 && S >= 0 && 0 > S1 && I2 >= 0 && S1 > 0 && L > 0 && M + 1 = I2 && K = 0;
    action := N' = N2, K' = O2, O' = R2, P' = S2, R' = T2, P1' = S1, Q1' = 0, R1' = S1, O1' = 0, M1' = S1, I2' = W1 + 1, T1' = S1, K2' = I, L2' = U2, N1' = W1, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
  transition t83 := {
    from   := f0;
    to     := f1;
    guard  := 0 >= A3 && 0 >= B3 && 0 >= O2 && 0 >= C3 && S1 = 0;
    action := Z1' = N2, N' = O2, A' = R2, C' = S2, B' = T2, K' = U2, D2' = Q2, U1' = P2, A2' = W2, E' = V2, D' = Y2, O' = Z2, P' = X2, R' = D3, P1' = E3, Q1' = F3, R1' = G3, O1' = H3, M1' = I3, S1' = J3, T1' = K3, N2' = ?, O2' = ?, P2' = ?, Q2' = ?, R2' = ?, S2' = ?, T2' = ?, U2' = ?, V2' = ?, W2' = ?, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?;
  };
}
strategy dumb {
  Region init := { state = f0 };
}