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;
  states f15, f13, f9, f10, f0, f17;
  transition t0 := {
    from   := f15;
    to     := f15;
    guard  := A > B && B >= 0;
    action := C' = D, B' = 1 + B, E' = D, D' = X1, F' = Y1, G' = B, 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' = ?;
  };
  transition t1 := {
    from   := f13;
    to     := f13;
    guard  := H >= 0 && I >= 0 && X1 > 1 && 0 > Z1 && 0 > A2 && 0 > B2;
    action := J' = X1, K' = Y1, L' = A2, M' = A2, N' = C2, O' = D2, P' = 0, Q' = E2, R' = F2, S' = G2, T' = H2, U' = I2, V' = J2, W' = 0, H' = 1 + H, I' = -1 + I, X' = K2, Y' = Z, A1' = B2, B1' = 1 + H, C1' = -1 + I, 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' = ?;
  };
  transition t2 := {
    from   := f13;
    to     := f13;
    guard  := H >= 0 && I >= 0 && X1 > 1 && 0 > Z1 && 0 > A2 && B2 > 0;
    action := J' = X1, K' = Y1, L' = A2, M' = A2, N' = C2, O' = D2, P' = 0, Q' = E2, R' = F2, S' = G2, T' = H2, U' = I2, V' = J2, W' = 0, H' = 1 + H, I' = -1 + I, X' = K2, Y' = Z, A1' = B2, B1' = 1 + H, C1' = -1 + I, 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' = ?;
  };
  transition t3 := {
    from   := f13;
    to     := f13;
    guard  := H >= 0 && I >= 0 && X1 > 1 && 0 > Z1 && A2 > 0 && 0 > B2;
    action := J' = X1, K' = Y1, L' = A2, M' = A2, N' = C2, O' = D2, P' = 0, Q' = E2, R' = F2, S' = G2, T' = H2, U' = I2, V' = J2, W' = 0, H' = 1 + H, I' = -1 + I, X' = K2, Y' = Z, A1' = B2, B1' = 1 + H, C1' = -1 + I, 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' = ?;
  };
  transition t4 := {
    from   := f13;
    to     := f13;
    guard  := H >= 0 && I >= 0 && X1 > 1 && 0 > Z1 && A2 > 0 && B2 > 0;
    action := J' = X1, K' = Y1, L' = A2, M' = A2, N' = C2, O' = D2, P' = 0, Q' = E2, R' = F2, S' = G2, T' = H2, U' = I2, V' = J2, W' = 0, H' = 1 + H, I' = -1 + I, X' = K2, Y' = Z, A1' = B2, B1' = 1 + H, C1' = -1 + I, 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' = ?;
  };
  transition t5 := {
    from   := f13;
    to     := f13;
    guard  := H >= 0 && I >= 0 && X1 > 1 && Z1 > 0 && 0 > A2 && 0 > B2;
    action := J' = X1, K' = Y1, L' = A2, M' = A2, N' = C2, O' = D2, P' = 0, Q' = E2, R' = F2, S' = G2, T' = H2, U' = I2, V' = J2, W' = 0, H' = 1 + H, I' = -1 + I, X' = K2, Y' = Z, A1' = B2, B1' = 1 + H, C1' = -1 + I, 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' = ?;
  };
  transition t6 := {
    from   := f13;
    to     := f13;
    guard  := H >= 0 && I >= 0 && X1 > 1 && Z1 > 0 && 0 > A2 && B2 > 0;
    action := J' = X1, K' = Y1, L' = A2, M' = A2, N' = C2, O' = D2, P' = 0, Q' = E2, R' = F2, S' = G2, T' = H2, U' = I2, V' = J2, W' = 0, H' = 1 + H, I' = -1 + I, X' = K2, Y' = Z, A1' = B2, B1' = 1 + H, C1' = -1 + I, 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' = ?;
  };
  transition t7 := {
    from   := f13;
    to     := f13;
    guard  := H >= 0 && I >= 0 && X1 > 1 && Z1 > 0 && A2 > 0 && 0 > B2;
    action := J' = X1, K' = Y1, L' = A2, M' = A2, N' = C2, O' = D2, P' = 0, Q' = E2, R' = F2, S' = G2, T' = H2, U' = I2, V' = J2, W' = 0, H' = 1 + H, I' = -1 + I, X' = K2, Y' = Z, A1' = B2, B1' = 1 + H, C1' = -1 + I, 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' = ?;
  };
  transition t8 := {
    from   := f13;
    to     := f13;
    guard  := H >= 0 && I >= 0 && X1 > 1 && Z1 > 0 && A2 > 0 && B2 > 0;
    action := J' = X1, K' = Y1, L' = A2, M' = A2, N' = C2, O' = D2, P' = 0, Q' = E2, R' = F2, S' = G2, T' = H2, U' = I2, V' = J2, W' = 0, H' = 1 + H, I' = -1 + I, X' = K2, Y' = Z, A1' = B2, B1' = 1 + H, C1' = -1 + I, 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' = ?;
  };
  transition t9 := {
    from   := f9;
    to     := f10;
    guard  := A2 > D1 && E1 >= 0 && X1 > 1 && Y1 > A2 && 0 > Y1 && F1 = 0;
    action := J' = X1, L' = Y1, G1' = Y1, H1' = 0, I1' = Y1, F1' = 0, J1' = D1, 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' = ?;
  };
  transition t10 := {
    from   := f9;
    to     := f10;
    guard  := A2 > D1 && E1 >= 0 && X1 > 1 && Y1 > A2 && Y1 > 0 && F1 = 0;
    action := J' = X1, L' = Y1, G1' = Y1, H1' = 0, I1' = Y1, F1' = 0, J1' = D1, 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' = ?;
  };
  transition t11 := {
    from   := f9;
    to     := f10;
    guard  := A2 > D1 && E1 >= 0 && X1 > 1 && A2 > Y1 && 0 > Y1 && F1 = 0;
    action := J' = X1, L' = Y1, G1' = Y1, H1' = 0, I1' = Y1, F1' = 0, J1' = D1, 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' = ?;
  };
  transition t12 := {
    from   := f9;
    to     := f10;
    guard  := A2 > D1 && E1 >= 0 && X1 > 1 && A2 > Y1 && Y1 > 0 && F1 = 0;
    action := J' = X1, L' = Y1, G1' = Y1, H1' = 0, I1' = Y1, F1' = 0, J1' = D1, 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' = ?;
  };
  transition t13 := {
    from   := f9;
    to     := f10;
    guard  := D1 > A2 && E1 >= 0 && X1 > 1 && Y1 > A2 && 0 > Y1 && F1 = 0;
    action := J' = X1, L' = Y1, G1' = Y1, H1' = 0, I1' = Y1, F1' = 0, J1' = D1, 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' = ?;
  };
  transition t14 := {
    from   := f9;
    to     := f10;
    guard  := D1 > A2 && E1 >= 0 && X1 > 1 && Y1 > A2 && Y1 > 0 && F1 = 0;
    action := J' = X1, L' = Y1, G1' = Y1, H1' = 0, I1' = Y1, F1' = 0, J1' = D1, 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' = ?;
  };
  transition t15 := {
    from   := f9;
    to     := f10;
    guard  := D1 > A2 && E1 >= 0 && X1 > 1 && A2 > Y1 && 0 > Y1 && F1 = 0;
    action := J' = X1, L' = Y1, G1' = Y1, H1' = 0, I1' = Y1, F1' = 0, J1' = D1, 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' = ?;
  };
  transition t16 := {
    from   := f9;
    to     := f10;
    guard  := D1 > A2 && E1 >= 0 && X1 > 1 && A2 > Y1 && Y1 > 0 && F1 = 0;
    action := J' = X1, L' = Y1, G1' = Y1, H1' = 0, I1' = Y1, F1' = 0, J1' = D1, 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' = ?;
  };
  transition t17 := {
    from   := f9;
    to     := f0;
    guard  := E1 >= 0 && 0 > A2 && X1 > 1 && F1 = D1;
    action := J' = X1, K' = Y1, L' = A2, G1' = C2, H1' = D2, I1' = E2, F1' = F2, D1' = G2, J1' = H2, 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' = ?;
  };
  transition t18 := {
    from   := f9;
    to     := f0;
    guard  := E1 >= 0 && A2 > 0 && X1 > 1 && F1 = D1;
    action := J' = X1, K' = Y1, L' = A2, G1' = C2, H1' = D2, I1' = E2, F1' = F2, D1' = G2, J1' = H2, 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' = ?;
  };
  transition t19 := {
    from   := f10;
    to     := f10;
    guard  := C2 > D1 && K1 >= 0 && X1 > 1 && Y1 > C2 && 0 > Y1 && F1 = 0;
    action := J' = X1, L' = Y1, G1' = Y1, H1' = 0, I1' = Y1, F1' = 0, X' = A2, J1' = D1, K1' = -1 + K1, L1' = -1 + K1, 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' = ?;
  };
  transition t20 := {
    from   := f10;
    to     := f10;
    guard  := C2 > D1 && K1 >= 0 && X1 > 1 && Y1 > C2 && Y1 > 0 && F1 = 0;
    action := J' = X1, L' = Y1, G1' = Y1, H1' = 0, I1' = Y1, F1' = 0, X' = A2, J1' = D1, K1' = -1 + K1, L1' = -1 + K1, 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' = ?;
  };
  transition t21 := {
    from   := f10;
    to     := f10;
    guard  := C2 > D1 && K1 >= 0 && X1 > 1 && C2 > Y1 && 0 > Y1 && F1 = 0;
    action := J' = X1, L' = Y1, G1' = Y1, H1' = 0, I1' = Y1, F1' = 0, X' = A2, J1' = D1, K1' = -1 + K1, L1' = -1 + K1, 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' = ?;
  };
  transition t22 := {
    from   := f10;
    to     := f10;
    guard  := C2 > D1 && K1 >= 0 && X1 > 1 && C2 > Y1 && Y1 > 0 && F1 = 0;
    action := J' = X1, L' = Y1, G1' = Y1, H1' = 0, I1' = Y1, F1' = 0, X' = A2, J1' = D1, K1' = -1 + K1, L1' = -1 + K1, 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' = ?;
  };
  transition t23 := {
    from   := f10;
    to     := f10;
    guard  := D1 > C2 && K1 >= 0 && X1 > 1 && Y1 > C2 && 0 > Y1 && F1 = 0;
    action := J' = X1, L' = Y1, G1' = Y1, H1' = 0, I1' = Y1, F1' = 0, X' = A2, J1' = D1, K1' = -1 + K1, L1' = -1 + K1, 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' = ?;
  };
  transition t24 := {
    from   := f10;
    to     := f10;
    guard  := D1 > C2 && K1 >= 0 && X1 > 1 && Y1 > C2 && Y1 > 0 && F1 = 0;
    action := J' = X1, L' = Y1, G1' = Y1, H1' = 0, I1' = Y1, F1' = 0, X' = A2, J1' = D1, K1' = -1 + K1, L1' = -1 + K1, 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' = ?;
  };
  transition t25 := {
    from   := f10;
    to     := f10;
    guard  := D1 > C2 && K1 >= 0 && X1 > 1 && C2 > Y1 && 0 > Y1 && F1 = 0;
    action := J' = X1, L' = Y1, G1' = Y1, H1' = 0, I1' = Y1, F1' = 0, X' = A2, J1' = D1, K1' = -1 + K1, L1' = -1 + K1, 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' = ?;
  };
  transition t26 := {
    from   := f10;
    to     := f10;
    guard  := D1 > C2 && K1 >= 0 && X1 > 1 && C2 > Y1 && Y1 > 0 && F1 = 0;
    action := J' = X1, L' = Y1, G1' = Y1, H1' = 0, I1' = Y1, F1' = 0, X' = A2, J1' = D1, K1' = -1 + K1, L1' = -1 + K1, 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' = ?;
  };
  transition t27 := {
    from   := f10;
    to     := f0;
    guard  := X1 > 1 && K1 >= 0 && F1 = D1;
    action := J' = X1, K' = Y1, G1' = A2, H1' = C2, I1' = D2, F1' = E2, D1' = F2, J1' = G2, 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' = ?;
  };
  transition t28 := {
    from   := f17;
    to     := f15;
    guard  := Y1 > 1;
    action := M1' = X1, J' = Y1, A' = Y1, C' = A2, B' = 2, N1' = A2, E' = A2, D' = C2, O1' = D2, 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' = ?;
  };
  transition t29 := {
    from   := f15;
    to     := f13;
    guard  := L2 > 1 && Z1 >= L2 && X1 > 1 && B >= A && B >= 0 && P1 >= 0 && 0 > M2 && 0 > C && 0 > I2;
    action := J' = X1, A' = Y1, C' = A2, B' = C2, Q1' = D2, K' = E2, N1' = F2, E' = G2, D' = H2, L' = I2, M' = I2, Z' = C, R1' = J2, N' = K2, O' = B2, P' = 0, S1' = Z1, Q' = N2, R' = O2, S' = P2, T' = Q2, U' = R2, V' = S2, W' = 0, T1' = T2, U1' = M2, 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' = ?;
  };
  transition t30 := {
    from   := f15;
    to     := f13;
    guard  := L2 > 1 && Z1 >= L2 && X1 > 1 && B >= A && B >= 0 && P1 >= 0 && 0 > M2 && 0 > C && I2 > 0;
    action := J' = X1, A' = Y1, C' = A2, B' = C2, Q1' = D2, K' = E2, N1' = F2, E' = G2, D' = H2, L' = I2, M' = I2, Z' = C, R1' = J2, N' = K2, O' = B2, P' = 0, S1' = Z1, Q' = N2, R' = O2, S' = P2, T' = Q2, U' = R2, V' = S2, W' = 0, T1' = T2, U1' = M2, 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' = ?;
  };
  transition t31 := {
    from   := f15;
    to     := f13;
    guard  := L2 > 1 && Z1 >= L2 && X1 > 1 && B >= A && B >= 0 && P1 >= 0 && 0 > M2 && C > 0 && 0 > I2;
    action := J' = X1, A' = Y1, C' = A2, B' = C2, Q1' = D2, K' = E2, N1' = F2, E' = G2, D' = H2, L' = I2, M' = I2, Z' = C, R1' = J2, N' = K2, O' = B2, P' = 0, S1' = Z1, Q' = N2, R' = O2, S' = P2, T' = Q2, U' = R2, V' = S2, W' = 0, T1' = T2, U1' = M2, 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' = ?;
  };
  transition t32 := {
    from   := f15;
    to     := f13;
    guard  := L2 > 1 && Z1 >= L2 && X1 > 1 && B >= A && B >= 0 && P1 >= 0 && 0 > M2 && C > 0 && I2 > 0;
    action := J' = X1, A' = Y1, C' = A2, B' = C2, Q1' = D2, K' = E2, N1' = F2, E' = G2, D' = H2, L' = I2, M' = I2, Z' = C, R1' = J2, N' = K2, O' = B2, P' = 0, S1' = Z1, Q' = N2, R' = O2, S' = P2, T' = Q2, U' = R2, V' = S2, W' = 0, T1' = T2, U1' = M2, 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' = ?;
  };
  transition t33 := {
    from   := f15;
    to     := f13;
    guard  := L2 > 1 && Z1 >= L2 && X1 > 1 && B >= A && B >= 0 && P1 >= 0 && M2 > 0 && 0 > C && 0 > I2;
    action := J' = X1, A' = Y1, C' = A2, B' = C2, Q1' = D2, K' = E2, N1' = F2, E' = G2, D' = H2, L' = I2, M' = I2, Z' = C, R1' = J2, N' = K2, O' = B2, P' = 0, S1' = Z1, Q' = N2, R' = O2, S' = P2, T' = Q2, U' = R2, V' = S2, W' = 0, T1' = T2, U1' = M2, 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' = ?;
  };
  transition t34 := {
    from   := f15;
    to     := f13;
    guard  := L2 > 1 && Z1 >= L2 && X1 > 1 && B >= A && B >= 0 && P1 >= 0 && M2 > 0 && 0 > C && I2 > 0;
    action := J' = X1, A' = Y1, C' = A2, B' = C2, Q1' = D2, K' = E2, N1' = F2, E' = G2, D' = H2, L' = I2, M' = I2, Z' = C, R1' = J2, N' = K2, O' = B2, P' = 0, S1' = Z1, Q' = N2, R' = O2, S' = P2, T' = Q2, U' = R2, V' = S2, W' = 0, T1' = T2, U1' = M2, 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' = ?;
  };
  transition t35 := {
    from   := f15;
    to     := f13;
    guard  := L2 > 1 && Z1 >= L2 && X1 > 1 && B >= A && B >= 0 && P1 >= 0 && M2 > 0 && C > 0 && 0 > I2;
    action := J' = X1, A' = Y1, C' = A2, B' = C2, Q1' = D2, K' = E2, N1' = F2, E' = G2, D' = H2, L' = I2, M' = I2, Z' = C, R1' = J2, N' = K2, O' = B2, P' = 0, S1' = Z1, Q' = N2, R' = O2, S' = P2, T' = Q2, U' = R2, V' = S2, W' = 0, T1' = T2, U1' = M2, 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' = ?;
  };
  transition t36 := {
    from   := f15;
    to     := f13;
    guard  := L2 > 1 && Z1 >= L2 && X1 > 1 && B >= A && B >= 0 && P1 >= 0 && M2 > 0 && C > 0 && I2 > 0;
    action := J' = X1, A' = Y1, C' = A2, B' = C2, Q1' = D2, K' = E2, N1' = F2, E' = G2, D' = H2, L' = I2, M' = I2, Z' = C, R1' = J2, N' = K2, O' = B2, P' = 0, S1' = Z1, Q' = N2, R' = O2, S' = P2, T' = Q2, U' = R2, V' = S2, W' = 0, T1' = T2, U1' = M2, 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' = ?;
  };
  transition t37 := {
    from   := f17;
    to     := f0;
    guard  := 0 >= U2 && 0 >= Y1 && 0 >= V2;
    action := M1' = X1, J' = Y1, A' = A2, C' = C2, B' = D2, Q1' = E2, K' = F2, N1' = G2, E' = H2, D' = I2, L' = 0, M' = J2, Z' = K2, R1' = B2, N' = Z1, O' = N2, P' = O2, Q' = P2, R' = Q2, S' = R2, T' = S2, U' = T2, V1' = M2, W1' = L2, V' = W2, W' = X2, G1' = Y2, H1' = Z2, I1' = A3, F1' = B3, D1' = C3, J1' = D3, 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' = ?;
  };
  transition t38 := {
    from   := f13;
    to     := f10;
    guard  := Q2 > 1 && X1 > 1 && I >= 0 && H >= 0 && L > 0 && 0 > L && Z = 0;
    action := J' = X1, K' = Y1, M' = A2, Z' = C2, R1' = D2, N' = E2, O' = F2, P' = G2, Q' = H2, R' = I2, S' = J2, T' = K2, U' = B2, V1' = Z1, W1' = N2, V' = O2, W' = P2, G1' = L, H1' = 0, I1' = L, F1' = 0, D1' = L, H' = K1 + 1, J1' = L, E1' = K1, 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' = ?;
  };
  transition t39 := {
    from   := f13;
    to     := f10;
    guard  := Q2 > 1 && X1 > 1 && I >= 0 && H >= 0 && L > 0 && Z = 0;
    action := J' = X1, K' = Y1, M' = A2, Z' = C2, R1' = D2, N' = E2, O' = F2, P' = G2, Q' = H2, R' = I2, S' = J2, T' = K2, U' = B2, V1' = Z1, W1' = N2, V' = O2, W' = P2, G1' = L, H1' = 0, I1' = L, F1' = 0, D1' = L, H' = K1 + 1, J1' = L, E1' = K1, 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' = ?;
  };
  transition t40 := {
    from   := f13;
    to     := f10;
    guard  := Q2 > 1 && X1 > 1 && I >= 0 && H >= 0 && 0 > L && Z = 0;
    action := J' = X1, K' = Y1, M' = A2, Z' = C2, R1' = D2, N' = E2, O' = F2, P' = G2, Q' = H2, R' = I2, S' = J2, T' = K2, U' = B2, V1' = Z1, W1' = N2, V' = O2, W' = P2, G1' = L, H1' = 0, I1' = L, F1' = 0, D1' = L, H' = K1 + 1, J1' = L, E1' = K1, 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' = ?;
  };
  transition t41 := {
    from   := f13;
    to     := f10;
    guard  := Q2 > 1 && X1 > 1 && I >= 0 && H >= 0 && 0 > L && L > 0 && Z = 0;
    action := J' = X1, K' = Y1, M' = A2, Z' = C2, R1' = D2, N' = E2, O' = F2, P' = G2, Q' = H2, R' = I2, S' = J2, T' = K2, U' = B2, V1' = Z1, W1' = N2, V' = O2, W' = P2, G1' = L, H1' = 0, I1' = L, F1' = 0, D1' = L, H' = K1 + 1, J1' = L, E1' = K1, 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' = ?;
  };
}
strategy dumb {
  Region init := { state = f17 };
}