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, L3, M3, N3, O3, P3, Q3, R3, S3, T3, U3, V3, W3, X3, Y3, Z3, A4, B4, C4, D4, E4, F4, G4, H4, I4, J4, K4, L4, M4, N4, O4, P4, Q4, R4, S4, T4;
  states f29, f34, f30, f35, f31, f32, f1, f10, f13, f11, f27, f12, f14, f15, f16, f17, f26;
  transition t0 := {
    from   := f29;
    to     := f34;
    guard  := A >= 0 && B > 0 && B4 > 1 && C4 >= B4 && C = 1;
    action := D' = B4, E' = D4, F' = 0, G' = H, C' = 1, I' = E4, J' = 1 + H, K' = F4, L' = G4, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t1 := {
    from   := f29;
    to     := f29;
    guard  := A >= B4 && A >= 0 && B > 0 && B4 > 1;
    action := D' = B4, E' = M, B' = -1 + B, F' = D4, L' = E4, N' = B, O' = A, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t2 := {
    from   := f30;
    to     := f35;
    guard  := B > 0 && H >= 0 && B4 > 1 && E4 > 0 && G = H && C = 1;
    action := D' = B4, E' = D4, B' = -1 + E4, F' = F4, C' = 1, H' = G, L' = G4, P' = E4, Q' = C4, R' = -1 + E4, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t3 := {
    from   := f30;
    to     := f34;
    guard  := B > 0 && B4 > 1 && G >= 0 && H + 1 = G && C = 2;
    action := D' = B4, E' = D4, F' = 0, C' = 2, H' = -1 + G, L' = E4, S' = M, T' = F4, U' = G4, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t4 := {
    from   := f31;
    to     := f35;
    guard  := B > 0 && G >= 0 && B4 > 1 && H = G && C = 1;
    action := D' = B4, E' = D4, B' = -1 + B, F' = E4, C' = 1, H' = G, L' = F4, V' = G4, W' = B, X' = I, Y' = G, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t5 := {
    from   := f31;
    to     := f34;
    guard  := B > 0 && B4 > 1 && G >= 0;
    action := D' = B4, E' = D4, F' = 0, L' = E4, Z' = F4, A1' = G4, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t6 := {
    from   := f32;
    to     := f32;
    guard  := B > 0;
    action := D' = 1, E' = M, B' = -1 + B, F' = B4, L' = D4, B1' = B, C1' = D1, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t7 := {
    from   := f34;
    to     := f35;
    guard  := C >= 0 && B > 0 && H >= 0 && E4 > 0 && B4 > 1;
    action := D' = B4, E' = D4, B' = -1 + E4, F' = F4, L' = G4, E1' = E4, F1' = -1 + E4, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t8 := {
    from   := f34;
    to     := f34;
    guard  := C >= 0 && B > 0 && H >= 0 && B4 > 1;
    action := D' = B4, E' = D4, F' = 0, C' = 1 + C, H' = -1 + H, I' = E4, L' = F4, G1' = M, H1' = G4, I1' = 1 + C, J1' = -1 + H, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t9 := {
    from   := f35;
    to     := f35;
    guard  := C >= 0 && B > 0 && H >= 0 && B4 > 1;
    action := D' = B4, E' = D4, B' = -1 + B, F' = E4, L' = F4, K1' = G4, L1' = B, M1' = C, N1' = H, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t10 := {
    from   := f35;
    to     := f34;
    guard  := C >= 0 && B > 0 && H >= 0 && B4 > 1;
    action := D' = B4, E' = D4, F' = 0, C' = 1 + C, H' = -1 + H, I' = E4, L' = F4, K1' = G4, O1' = M, P1' = C4, Q1' = 1 + C, R1' = -1 + H, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t11 := {
    from   := f1;
    to     := f1;
    guard  := S1 > A && A >= 0;
    action := A' = 1 + A, T1' = U1, V1' = U1, U1' = B4, W1' = D4, X1' = A, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t12 := {
    from   := f1;
    to     := f29;
    guard  := A >= S1 && A >= 0 && D4 >= B4 && B4 > 1;
    action := D' = B4, M' = T1, E' = T1, A' = D4, S1' = E4, T1' = F4, Y1' = G4, V1' = C4, U1' = H4, Z1' = I4, A2' = J4, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t13 := {
    from   := f10;
    to     := f13;
    guard  := G4 >= 0 && H >= 0 && 0 >= D4 && B4 > 1 && B2 = 0 && C = 0;
    action := D' = B4, M' = C2, D2' = C2, E2' = 0, F2' = C2, B2' = 0, E' = C2, B' = D4, F' = E4, C' = 1 + G2, H2' = C2, I2' = G2, J2' = H, K2' = F4, L2' = -1 + F4, M2' = H, N2' = G2, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t14 := {
    from   := f10;
    to     := f13;
    guard  := C >= 0 && H >= 0 && 0 >= E4 && B4 > 1 && B2 = 0;
    action := D' = B4, M' = D4, D2' = C2, E2' = 0, F2' = C2, B2' = 0, E' = C2, B' = E4, F' = F4, C' = 1 + G2, H' = G4, H2' = C2, I2' = G2, J2' = H, K2' = G4, M2' = H, N2' = G2, O2' = -1 + C, P2' = G4, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t15 := {
    from   := f10;
    to     := f13;
    guard  := C4 >= 0 && H >= 0 && 0 >= D4 && B4 > 1 && B2 = 0 && C = 0;
    action := D' = B4, M' = C2, D2' = C2, E2' = 0, F2' = C2, B2' = 0, E' = C2, B' = D4, F' = E4, C' = 0, H' = F4, H2' = C2, I2' = G2, K2' = G4, L2' = -1 + G4, M2' = H, Q2' = -1 + F4, R2' = -1 + F4, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t16 := {
    from   := f10;
    to     := f13;
    guard  := C >= 0 && H >= 0 && 0 >= D4 && B4 > 1 && B2 = 0;
    action := D' = B4, M' = C2, D2' = C2, E2' = 0, F2' = C2, B2' = 0, E' = C2, B' = D4, F' = E4, H' = F4, H2' = C2, I2' = G2, K2' = F4, M2' = H, O2' = -1 + C, P2' = F4, Q2' = -1 + G4, R2' = -1 + G4, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t17 := {
    from   := f10;
    to     := f13;
    guard  := C4 >= 0 && H >= 0 && 0 >= D4 && B4 > 1 && B2 = 0 && C = 0;
    action := D' = B4, M' = C2, D2' = C2, E2' = 0, F2' = C2, B2' = 0, E' = C2, B' = D4, F' = E4, C' = F4, H2' = C2, I2' = -1 + F4, J2' = H, K2' = G4, L2' = -1 + G4, N2' = -1 + F4, Q2' = S2, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t18 := {
    from   := f10;
    to     := f13;
    guard  := C >= 0 && H >= 0 && 0 >= D4 && B4 > 1 && B2 = 0;
    action := D' = B4, M' = C2, D2' = C2, E2' = 0, F2' = C2, B2' = 0, E' = C2, B' = D4, F' = E4, C' = F4, H' = G4, H2' = C2, I2' = -1 + F4, J2' = H, K2' = G4, N2' = -1 + F4, O2' = -1 + C, P2' = G4, Q2' = S2, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t19 := {
    from   := f10;
    to     := f13;
    guard  := G4 >= 0 && H >= 0 && 0 >= D4 && B4 > 1 && B2 = 0 && C = 0;
    action := D' = B4, M' = C2, D2' = C2, E2' = 0, F2' = C2, B2' = 0, E' = C2, B' = D4, F' = E4, C' = 0, H' = 1 + S2, H2' = C2, K2' = F4, L2' = -1 + F4, Q2' = S2, R2' = S2, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t20 := {
    from   := f10;
    to     := f13;
    guard  := C >= 0 && H >= 0 && 0 >= D4 && B4 > 1 && B2 = 0;
    action := D' = B4, M' = C2, D2' = C2, E2' = 0, F2' = C2, B2' = 0, E' = C2, B' = D4, F' = E4, H' = F4, H2' = C2, K2' = F4, O2' = -1 + C, P2' = F4, Q2' = S2, R2' = S2, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t21 := {
    from   := f10;
    to     := f13;
    guard  := C4 >= 0 && H >= 0 && 0 >= D4 && B4 > 1 && B2 = 0 && C = 0;
    action := D' = B4, M' = C2, D2' = C2, E2' = 0, F2' = C2, B2' = 0, E' = C2, B' = D4, F' = E4, C' = F4, H2' = C2, I2' = -1 + F4, J2' = H, K2' = G4, L2' = -1 + G4, N2' = -1 + F4, T2' = U2, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t22 := {
    from   := f10;
    to     := f13;
    guard  := C >= 0 && H >= 0 && 0 >= D4 && B4 > 1 && B2 = 0;
    action := D' = B4, M' = C2, D2' = C2, E2' = 0, F2' = C2, B2' = 0, E' = C2, B' = D4, F' = E4, C' = F4, H' = G4, H2' = C2, I2' = -1 + F4, J2' = H, K2' = G4, N2' = -1 + F4, O2' = -1 + C, P2' = G4, T2' = U2, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t23 := {
    from   := f10;
    to     := f13;
    guard  := C4 >= 0 && H >= 0 && 0 >= D4 && B4 > 1 && B2 = 0 && C = 0;
    action := D' = B4, M' = C2, D2' = C2, E2' = 0, F2' = C2, B2' = 0, E' = C2, B' = D4, F' = E4, C' = 0, H' = F4, H2' = C2, K2' = G4, L2' = -1 + G4, Q2' = -1 + F4, R2' = -1 + F4, T2' = U2, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t24 := {
    from   := f10;
    to     := f13;
    guard  := C >= 0 && H >= 0 && 0 >= D4 && B4 > 1 && B2 = 0;
    action := D' = B4, M' = C2, D2' = C2, E2' = 0, F2' = C2, B2' = 0, E' = C2, B' = D4, F' = E4, H' = F4, H2' = C2, K2' = F4, O2' = -1 + C, P2' = F4, Q2' = -1 + G4, R2' = -1 + G4, T2' = U2, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t25 := {
    from   := f11;
    to     := f13;
    guard  := 0 >= E4 && B4 > 1 && B2 = 0 && N2 = 0;
    action := D' = B4, M' = C2, D2' = D4, E2' = 0, F2' = D4, B2' = 0, E' = D4, B' = E4, F' = F4, H2' = C2, I2' = G2, M2' = H, N2' = 1 + G2, V2' = G4, W2' = -1 + G4, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t26 := {
    from   := f11;
    to     := f13;
    guard  := 0 >= F4 && B4 > 1 && B2 = 0;
    action := D' = B4, M' = D4, D2' = E4, E2' = 0, F2' = E4, B2' = 0, E' = E4, B' = F4, F' = G4, H' = C4, H2' = C2, I2' = G2, M2' = H, N2' = 1 + G2, V2' = C4, X2' = -1 + N2, Y2' = C4, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t27 := {
    from   := f11;
    to     := f13;
    guard  := 0 >= E4 && B4 > 1 && B2 = 0;
    action := D' = B4, M' = D4, D2' = D4, E2' = 0, F2' = D4, B2' = 0, E' = D4, B' = E4, F' = F4, H2' = C2, I2' = G2, M2' = H, N2' = 1 + G2, Z2' = -1 + R2, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t28 := {
    from   := f11;
    to     := f13;
    guard  := 0 >= E4 && B4 > 1 && B2 = 0 && N2 = 0;
    action := D' = B4, M' = C2, D2' = D4, E2' = 0, F2' = D4, B2' = 0, E' = D4, B' = E4, F' = F4, H' = 1 + S2, H2' = C2, N2' = 0, Q2' = S2, V2' = G4, W2' = -1 + G4, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t29 := {
    from   := f11;
    to     := f13;
    guard  := 0 >= E4 && B4 > 1 && B2 = 0;
    action := D' = B4, M' = C2, D2' = D4, E2' = 0, F2' = D4, B2' = 0, E' = D4, B' = E4, F' = F4, H' = G4, H2' = C2, Q2' = S2, V2' = G4, X2' = -1 + N2, Y2' = G4, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t30 := {
    from   := f11;
    to     := f13;
    guard  := 0 >= D4 && B4 > 1 && B2 = 0;
    action := D' = B4, M' = C2, D2' = C2, E2' = 0, F2' = C2, B2' = 0, E' = C2, B' = D4, F' = E4, H' = 1 + S2, H2' = C2, Q2' = S2, Z2' = -1 + R2, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t31 := {
    from   := f11;
    to     := f13;
    guard  := 0 >= D4 && B4 > 1 && B2 = 0 && N2 = 0;
    action := D' = B4, M' = C2, D2' = C2, E2' = 0, F2' = C2, B2' = 0, E' = C2, B' = D4, F' = E4, H2' = C2, N2' = 0, R2' = 1 + U2, T2' = U2, V2' = F4, W2' = -1 + F4, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t32 := {
    from   := f11;
    to     := f13;
    guard  := 0 >= E4 && B4 > 1 && B2 = 0;
    action := D' = B4, M' = D4, D2' = D4, E2' = 0, F2' = D4, B2' = 0, E' = D4, B' = E4, F' = F4, H' = G4, H2' = C2, R2' = 1 + U2, T2' = U2, V2' = G4, X2' = -1 + N2, Y2' = G4, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t33 := {
    from   := f11;
    to     := f13;
    guard  := 0 >= E4 && B4 > 1 && B2 = 0;
    action := D' = B4, M' = D4, D2' = D4, E2' = 0, F2' = D4, B2' = 0, E' = D4, B' = E4, F' = F4, H2' = C2, R2' = 1 + U2, T2' = U2, Z2' = -1 + R2, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t34 := {
    from   := f11;
    to     := f27;
    guard  := B4 > 1 && 0 >= I4 && B2 = C2;
    action := D' = B4, M' = D4, D2' = E4, E2' = F4, F2' = G4, B2' = C4, C2' = H4, E' = D4, B' = I4, F' = J4, A2' = K4, H2' = L4, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t35 := {
    from   := f12;
    to     := f13;
    guard  := 0 >= E4 && B4 > 1 && B2 = 0 && I2 = 0;
    action := D' = B4, M' = C2, D2' = D4, E2' = 0, F2' = D4, B2' = 0, E' = D4, B' = E4, F' = F4, H2' = C2, I2' = 0, S2' = -1 + H, A3' = G4, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t36 := {
    from   := f12;
    to     := f13;
    guard  := 0 >= F4 && B4 > 1 && B2 = 0;
    action := D' = B4, M' = D4, D2' = E4, E2' = 0, F2' = E4, B2' = 0, E' = E4, B' = F4, F' = G4, H2' = C2, G2' = -1 + I2, A3' = C4, B3' = H, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t37 := {
    from   := f12;
    to     := f13;
    guard  := 0 >= E4 && B4 > 1 && B2 = 0;
    action := D' = B4, M' = D4, D2' = D4, E2' = 0, F2' = D4, B2' = 0, E' = D4, B' = E4, F' = F4, H2' = C2, Q2' = T2, U2' = -1 + T2, A3' = G4, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t38 := {
    from   := f12;
    to     := f13;
    guard  := 0 >= F4 && B4 > 1 && B2 = 0;
    action := D' = B4, M' = D4, D2' = E4, E2' = 0, F2' = E4, B2' = 0, E' = E4, B' = F4, F' = G4, H2' = C2, U2' = -1 + Q2, A3' = D4, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t39 := {
    from   := f12;
    to     := f27;
    guard  := B4 > 1 && 0 >= J4 && B2 = C2 && Q2 = 0;
    action := D' = B4, M' = D4, D2' = E4, E2' = F4, F2' = G4, B2' = C4, C2' = H4, E' = I4, B' = J4, F' = K4, A2' = L4, H2' = D4, Q2' = 0, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t40 := {
    from   := f12;
    to     := f27;
    guard  := B4 > 1 && 0 >= I4 && B2 = C2 && T2 = 0;
    action := D' = B4, M' = D4, D2' = E4, E2' = F4, F2' = G4, B2' = C4, C2' = H4, E' = D4, B' = I4, F' = J4, A2' = K4, H2' = L4, T2' = 0, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t41 := {
    from   := f13;
    to     := f13;
    guard  := B4 > 1 && 0 >= F4 && B2 = 0 && G2 = 0;
    action := D' = B4, M' = D4, D2' = E4, E2' = 0, F2' = E4, B2' = 0, E' = E4, B' = F4, F' = G4, H2' = C2, G2' = 0, S2' = -1 + H, C3' = C4, D3' = H4, E3' = I4, F3' = J4, G3' = -1 + H, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t42 := {
    from   := f13;
    to     := f13;
    guard  := 0 >= F4 && B4 > 1 && B2 = 0;
    action := D' = B4, M' = D4, D2' = E4, E2' = 0, F2' = E4, B2' = 0, E' = E4, B' = F4, F' = G4, H2' = C2, G2' = -1 + G2, C3' = C4, D3' = H4, H3' = I4, I3' = J4, J3' = H, K3' = -1 + G2, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t43 := {
    from   := f13;
    to     := f13;
    guard  := B4 > 1 && 0 >= E4 && B2 = 0;
    action := D' = B4, M' = D4, D2' = D4, E2' = 0, F2' = D4, B2' = 0, E' = D4, B' = E4, F' = F4, I' = G4, H2' = C2, U2' = -1 + L3, C3' = C4, D3' = H4, M3' = I4, N3' = -1 + L3, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t44 := {
    from   := f13;
    to     := f13;
    guard  := B4 > 1 && 0 >= F4 && B2 = 0;
    action := D' = B4, M' = D4, D2' = E4, E2' = 0, F2' = E4, B2' = 0, E' = E4, B' = F4, F' = G4, H2' = C2, U2' = -1 + S2, C3' = D4, D3' = C4, N3' = -1 + S2, O3' = H4, P3' = I4, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t45 := {
    from   := f13;
    to     := f13;
    guard  := B4 > 1 && 0 >= F4 && B2 = 0;
    action := D' = B4, M' = D4, D2' = E4, E2' = 0, F2' = E4, B2' = 0, E' = E4, B' = F4, F' = G4, H2' = C2, U2' = -1 + U2, C3' = C4, D3' = H4, N3' = -1 + U2, Q3' = I4, R3' = J4, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t46 := {
    from   := f13;
    to     := f27;
    guard  := B4 > 1 && B2 = C2;
    action := D' = B4, D2' = D4, E2' = E4, F2' = F4, B2' = G4, C2' = C4, A2' = H4, H2' = I4, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t47 := {
    from   := f14;
    to     := f15;
    guard  := S3 >= 0 && E4 > 0 && B4 > 1 && B2 = 0;
    action := D' = B4, M' = 0, D2' = D4, E2' = 0, F2' = D4, B2' = 0, E' = D4, B' = E4, F' = 0, H2' = C2, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t48 := {
    from   := f14;
    to     := f27;
    guard  := S3 >= 0 && I4 > 0 && B4 > 1 && B2 = C2;
    action := D' = B4, D2' = D4, E2' = E4, F2' = F4, B2' = G4, C2' = C4, E' = H4, B' = I4, A2' = J4, H2' = K4, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t49 := {
    from   := f15;
    to     := f15;
    guard  := T3 >= 0 && E4 > 0 && B4 > 1 && B2 = 0;
    action := D' = B4, M' = 0, D2' = D4, E2' = 0, F2' = D4, B2' = 0, E' = D4, B' = E4, F' = 0, I' = F4, H2' = C2, T3' = -1 + T3, U3' = -1 + T3, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t50 := {
    from   := f15;
    to     := f27;
    guard  := T3 >= 0 && I4 > 0 && B4 > 1 && B2 = C2;
    action := D' = B4, D2' = D4, E2' = E4, F2' = F4, B2' = G4, C2' = C4, E' = H4, B' = I4, A2' = J4, H2' = K4, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t51 := {
    from   := f16;
    to     := f17;
    guard  := V3 >= 0 && B4 > 1 && 0 >= E4 && B2 = 0;
    action := D' = B4, M' = D4, D2' = D4, E2' = 0, F2' = D4, B2' = 0, E' = D4, B' = E4, H2' = C2, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t52 := {
    from   := f16;
    to     := f27;
    guard  := V3 >= 0 && B4 > 1 && 0 >= I4 && B2 = C2;
    action := D' = B4, M' = D4, D2' = E4, E2' = F4, F2' = G4, B2' = C4, C2' = H4, B' = I4, A2' = J4, H2' = K4, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t53 := {
    from   := f17;
    to     := f17;
    guard  := W3 >= 0 && B4 > 1 && 0 >= E4 && B2 = 0;
    action := D' = B4, M' = D4, D2' = D4, E2' = 0, F2' = D4, B2' = 0, E' = D4, B' = E4, I' = F4, H2' = C2, W3' = -1 + W3, X3' = -1 + W3, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t54 := {
    from   := f17;
    to     := f27;
    guard  := W3 >= 0 && B4 > 1 && 0 >= I4 && B2 = C2;
    action := D' = B4, M' = D4, D2' = E4, E2' = F4, F2' = G4, B2' = C4, C2' = H4, B' = I4, A2' = J4, H2' = K4, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t55 := {
    from   := f29;
    to     := f17;
    guard  := A >= E4 && A >= 0 && 0 >= B && F4 >= B4 && 0 >= G4 && E4 > 1 && 0 >= D4 && B4 > 1;
    action := D' = B4, M' = E, D2' = E, E2' = 0, F2' = E, B2' = 0, C2' = E, B' = D4, H2' = E, Y3' = W3 + 1, V3' = W3, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t56 := {
    from   := f30;
    to     := f15;
    guard  := E4 > 0 && F4 > 1 && D4 > 0 && B4 > 1 && M = 0 && G = 0 && C = 1;
    action := D' = B4, M' = 0, D2' = E, E2' = 0, F2' = E, B2' = 0, C2' = E, B' = D4, F' = 0, G' = 0, C' = T3 + 1, H2' = E, S3' = T3, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t57 := {
    from   := f31;
    to     := f10;
    guard  := 0 >= B && H >= 0 && 0 >= E4 && B4 > 1 && C = 1 && G = H;
    action := D' = B4, M' = D4, D2' = E, E2' = 0, F2' = E, B2' = 0, C2' = E, B' = E4, F' = F4, C' = 1, H' = G, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t58 := {
    from   := f34;
    to     := f15;
    guard  := H >= 0 && C >= 0 && E4 > 0 && F4 > 1 && D4 > 0 && B4 > 1 && M = 0;
    action := D' = B4, M' = 0, D2' = E, E2' = 0, F2' = E, B2' = 0, C2' = E, B' = D4, F' = 0, C' = T3 + 1, H2' = E, S3' = T3, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t59 := {
    from   := f35;
    to     := f10;
    guard  := 0 >= B && H >= 0 && C >= 0 && B4 > 1 && 0 >= E4;
    action := D' = B4, M' = D4, D2' = E, E2' = 0, F2' = E, B2' = 0, C2' = E, B' = E4, F' = F4, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t60 := {
    from   := f26;
    to     := f1;
    guard  := B4 > 1;
    action := D' = B4, A' = 2, L' = D4, S1' = B4, T1' = E4, Y1' = E4, V1' = E4, U1' = F4, Z3' = G4, A4' = 2, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t61 := {
    from   := f26;
    to     := f32;
    guard  := true;
    action := D' = 1, M' = U1, E' = U1, A' = B4, L' = D4, S1' = E4, T1' = F4, Y1' = G4, V1' = C4, U1' = H4, Z1' = I4, A2' = J4, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t62 := {
    from   := f26;
    to     := f27;
    guard  := 0 >= M4 && 0 >= N4 && 0 >= B4 && 0 >= O4;
    action := D' = B4, M' = 0, D2' = D4, E2' = E4, F2' = F4, B2' = G4, C2' = C4, E' = 0, A' = H4, L' = I4, S1' = J4, T1' = K4, Y1' = L4, V1' = P4, U1' = Q4, Z1' = R4, A2' = S4, H2' = T4, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t63 := {
    from   := f32;
    to     := f27;
    guard  := 0 >= B && 0 >= K4 && 0 >= H4 && 0 >= L4 && E = 0;
    action := D' = 1, M' = B4, D2' = D4, E2' = E4, F2' = F4, B2' = G4, C2' = C4, E' = 0, B' = H4, A2' = I4, H2' = J4, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
  transition t64 := {
    from   := f32;
    to     := f27;
    guard  := B > 0 && L4 > 0 && H4 > 0 && P4 > 0 && M = 0;
    action := D' = 1, M' = 0, D2' = B4, E2' = D4, F2' = E4, B2' = F4, C2' = G4, E' = C4, B' = H4, F' = 0, L' = I4, A2' = J4, H2' = K4, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?;
  };
}
strategy dumb {
  Region init := { state = f26 };
}