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;
  states f12, f16, f13, f1, f7, f8, f10, f9;
  transition t0 := {
    from   := f12;
    to     := f16;
    guard  := A >= 0 && L1 > 1 && 0 > B && M1 >= L1 && 0 > N1 && C = 1;
    action := D' = L1, E' = N1, F' = O1, G' = 1 + H, I' = P1, J' = H, C' = 1, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t1 := {
    from   := f12;
    to     := f16;
    guard  := A >= 0 && L1 > 1 && 0 > B && M1 >= L1 && N1 > 0 && C = 1;
    action := D' = L1, E' = N1, F' = O1, G' = 1 + H, I' = P1, J' = H, C' = 1, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t2 := {
    from   := f12;
    to     := f16;
    guard  := A >= 0 && L1 > 1 && B > 0 && M1 >= L1 && 0 > N1 && C = 1;
    action := D' = L1, E' = N1, F' = O1, G' = 1 + H, I' = P1, J' = H, C' = 1, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t3 := {
    from   := f12;
    to     := f16;
    guard  := A >= 0 && L1 > 1 && B > 0 && M1 >= L1 && N1 > 0 && C = 1;
    action := D' = L1, E' = N1, F' = O1, G' = 1 + H, I' = P1, J' = H, C' = 1, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t4 := {
    from   := f13;
    to     := f16;
    guard  := J >= 0 && L1 > 1 && 0 > B && 0 > N1 && 0 > P1;
    action := D' = L1, E' = N1, K' = O1, L' = P1, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t5 := {
    from   := f13;
    to     := f16;
    guard  := J >= 0 && L1 > 1 && 0 > B && 0 > N1 && P1 > 0;
    action := D' = L1, E' = N1, K' = O1, L' = P1, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t6 := {
    from   := f13;
    to     := f16;
    guard  := J >= 0 && L1 > 1 && 0 > B && N1 > 0 && 0 > P1;
    action := D' = L1, E' = N1, K' = O1, L' = P1, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t7 := {
    from   := f13;
    to     := f16;
    guard  := J >= 0 && L1 > 1 && 0 > B && N1 > 0 && P1 > 0;
    action := D' = L1, E' = N1, K' = O1, L' = P1, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t8 := {
    from   := f13;
    to     := f16;
    guard  := J >= 0 && L1 > 1 && B > 0 && 0 > N1 && 0 > P1;
    action := D' = L1, E' = N1, K' = O1, L' = P1, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t9 := {
    from   := f13;
    to     := f16;
    guard  := J >= 0 && L1 > 1 && B > 0 && 0 > N1 && P1 > 0;
    action := D' = L1, E' = N1, K' = O1, L' = P1, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t10 := {
    from   := f13;
    to     := f16;
    guard  := J >= 0 && L1 > 1 && B > 0 && N1 > 0 && 0 > P1;
    action := D' = L1, E' = N1, K' = O1, L' = P1, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t11 := {
    from   := f13;
    to     := f16;
    guard  := J >= 0 && L1 > 1 && B > 0 && N1 > 0 && P1 > 0;
    action := D' = L1, E' = N1, K' = O1, L' = P1, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t12 := {
    from   := f16;
    to     := f16;
    guard  := C >= 0 && H >= 0 && L1 > 1 && 0 > M1 && 0 > N1 && 0 > P1;
    action := D' = L1, E' = N1, F' = O1, H' = -1 + H, C' = 1 + C, M' = B, N' = P1, O' = 1 + C, P' = -1 + H, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t13 := {
    from   := f16;
    to     := f16;
    guard  := C >= 0 && H >= 0 && L1 > 1 && 0 > M1 && 0 > N1 && P1 > 0;
    action := D' = L1, E' = N1, F' = O1, H' = -1 + H, C' = 1 + C, M' = B, N' = P1, O' = 1 + C, P' = -1 + H, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t14 := {
    from   := f16;
    to     := f16;
    guard  := C >= 0 && H >= 0 && L1 > 1 && 0 > M1 && N1 > 0 && 0 > P1;
    action := D' = L1, E' = N1, F' = O1, H' = -1 + H, C' = 1 + C, M' = B, N' = P1, O' = 1 + C, P' = -1 + H, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t15 := {
    from   := f16;
    to     := f16;
    guard  := C >= 0 && H >= 0 && L1 > 1 && 0 > M1 && N1 > 0 && P1 > 0;
    action := D' = L1, E' = N1, F' = O1, H' = -1 + H, C' = 1 + C, M' = B, N' = P1, O' = 1 + C, P' = -1 + H, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t16 := {
    from   := f16;
    to     := f16;
    guard  := C >= 0 && H >= 0 && L1 > 1 && M1 > 0 && 0 > N1 && 0 > P1;
    action := D' = L1, E' = N1, F' = O1, H' = -1 + H, C' = 1 + C, M' = B, N' = P1, O' = 1 + C, P' = -1 + H, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t17 := {
    from   := f16;
    to     := f16;
    guard  := C >= 0 && H >= 0 && L1 > 1 && M1 > 0 && 0 > N1 && P1 > 0;
    action := D' = L1, E' = N1, F' = O1, H' = -1 + H, C' = 1 + C, M' = B, N' = P1, O' = 1 + C, P' = -1 + H, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t18 := {
    from   := f16;
    to     := f16;
    guard  := C >= 0 && H >= 0 && L1 > 1 && M1 > 0 && N1 > 0 && 0 > P1;
    action := D' = L1, E' = N1, F' = O1, H' = -1 + H, C' = 1 + C, M' = B, N' = P1, O' = 1 + C, P' = -1 + H, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t19 := {
    from   := f16;
    to     := f16;
    guard  := C >= 0 && H >= 0 && L1 > 1 && M1 > 0 && N1 > 0 && P1 > 0;
    action := D' = L1, E' = N1, F' = O1, H' = -1 + H, C' = 1 + C, M' = B, N' = P1, O' = 1 + C, P' = -1 + H, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t20 := {
    from   := f1;
    to     := f1;
    guard  := Q > A && A >= 0;
    action := A' = 1 + A, R' = S, T' = S, S' = L1, U' = N1, V' = A, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t21 := {
    from   := f1;
    to     := f16;
    guard  := A >= Q && A >= 0 && L1 > 1 && 0 > R && Q1 >= L1 && H >= L1 && C = 0;
    action := D' = L1, B' = R, E' = R, A' = H, C' = 0, Q' = N1, R' = O1, W' = P1, T' = M1, S' = R1, X' = S1, Y' = T1, Z' = Q1, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t22 := {
    from   := f1;
    to     := f16;
    guard  := A >= Q && A >= 0 && L1 > 1 && R > 0 && Q1 >= L1 && H >= L1 && C = 0;
    action := D' = L1, B' = R, E' = R, A' = H, C' = 0, Q' = N1, R' = O1, W' = P1, T' = M1, S' = R1, X' = S1, Y' = T1, Z' = Q1, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t23 := {
    from   := f7;
    to     := f8;
    guard  := O1 > A1 && B1 >= 0 && L1 > 1 && N1 > O1 && 0 > N1 && C1 = 0;
    action := D' = L1, D1' = N1, E1' = 0, F1' = N1, C1' = 0, B' = 0, E' = N1, G1' = A1, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t24 := {
    from   := f7;
    to     := f8;
    guard  := O1 > A1 && B1 >= 0 && L1 > 1 && N1 > O1 && N1 > 0 && C1 = 0;
    action := D' = L1, D1' = N1, E1' = 0, F1' = N1, C1' = 0, B' = 0, E' = N1, G1' = A1, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t25 := {
    from   := f7;
    to     := f8;
    guard  := O1 > A1 && B1 >= 0 && L1 > 1 && O1 > N1 && 0 > N1 && C1 = 0;
    action := D' = L1, D1' = N1, E1' = 0, F1' = N1, C1' = 0, B' = 0, E' = N1, G1' = A1, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t26 := {
    from   := f7;
    to     := f8;
    guard  := O1 > A1 && B1 >= 0 && L1 > 1 && O1 > N1 && N1 > 0 && C1 = 0;
    action := D' = L1, D1' = N1, E1' = 0, F1' = N1, C1' = 0, B' = 0, E' = N1, G1' = A1, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t27 := {
    from   := f7;
    to     := f8;
    guard  := A1 > O1 && B1 >= 0 && L1 > 1 && N1 > O1 && 0 > N1 && C1 = 0;
    action := D' = L1, D1' = N1, E1' = 0, F1' = N1, C1' = 0, B' = 0, E' = N1, G1' = A1, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t28 := {
    from   := f7;
    to     := f8;
    guard  := A1 > O1 && B1 >= 0 && L1 > 1 && N1 > O1 && N1 > 0 && C1 = 0;
    action := D' = L1, D1' = N1, E1' = 0, F1' = N1, C1' = 0, B' = 0, E' = N1, G1' = A1, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t29 := {
    from   := f7;
    to     := f8;
    guard  := A1 > O1 && B1 >= 0 && L1 > 1 && O1 > N1 && 0 > N1 && C1 = 0;
    action := D' = L1, D1' = N1, E1' = 0, F1' = N1, C1' = 0, B' = 0, E' = N1, G1' = A1, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t30 := {
    from   := f7;
    to     := f8;
    guard  := A1 > O1 && B1 >= 0 && L1 > 1 && O1 > N1 && N1 > 0 && C1 = 0;
    action := D' = L1, D1' = N1, E1' = 0, F1' = N1, C1' = 0, B' = 0, E' = N1, G1' = A1, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t31 := {
    from   := f7;
    to     := f10;
    guard  := B1 >= 0 && 0 > S1 && L1 > 1 && C1 = A1;
    action := D' = L1, D1' = N1, E1' = O1, F1' = P1, C1' = M1, A1' = R1, E' = S1, Y' = T1, G1' = Q1, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t32 := {
    from   := f7;
    to     := f10;
    guard  := B1 >= 0 && S1 > 0 && L1 > 1 && C1 = A1;
    action := D' = L1, D1' = N1, E1' = O1, F1' = P1, C1' = M1, A1' = R1, E' = S1, Y' = T1, G1' = Q1, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t33 := {
    from   := f8;
    to     := f8;
    guard  := P1 > A1 && H1 >= 0 && L1 > 1 && N1 > P1 && 0 > N1 && C1 = 0;
    action := D' = L1, D1' = N1, E1' = 0, F1' = N1, C1' = 0, B' = 0, E' = N1, F' = O1, G1' = A1, H1' = -1 + H1, I1' = -1 + H1, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t34 := {
    from   := f8;
    to     := f8;
    guard  := P1 > A1 && H1 >= 0 && L1 > 1 && N1 > P1 && N1 > 0 && C1 = 0;
    action := D' = L1, D1' = N1, E1' = 0, F1' = N1, C1' = 0, B' = 0, E' = N1, F' = O1, G1' = A1, H1' = -1 + H1, I1' = -1 + H1, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t35 := {
    from   := f8;
    to     := f8;
    guard  := P1 > A1 && H1 >= 0 && L1 > 1 && P1 > N1 && 0 > N1 && C1 = 0;
    action := D' = L1, D1' = N1, E1' = 0, F1' = N1, C1' = 0, B' = 0, E' = N1, F' = O1, G1' = A1, H1' = -1 + H1, I1' = -1 + H1, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t36 := {
    from   := f8;
    to     := f8;
    guard  := P1 > A1 && H1 >= 0 && L1 > 1 && P1 > N1 && N1 > 0 && C1 = 0;
    action := D' = L1, D1' = N1, E1' = 0, F1' = N1, C1' = 0, B' = 0, E' = N1, F' = O1, G1' = A1, H1' = -1 + H1, I1' = -1 + H1, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t37 := {
    from   := f8;
    to     := f8;
    guard  := A1 > P1 && H1 >= 0 && L1 > 1 && N1 > P1 && 0 > N1 && C1 = 0;
    action := D' = L1, D1' = N1, E1' = 0, F1' = N1, C1' = 0, B' = 0, E' = N1, F' = O1, G1' = A1, H1' = -1 + H1, I1' = -1 + H1, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t38 := {
    from   := f8;
    to     := f8;
    guard  := A1 > P1 && H1 >= 0 && L1 > 1 && N1 > P1 && N1 > 0 && C1 = 0;
    action := D' = L1, D1' = N1, E1' = 0, F1' = N1, C1' = 0, B' = 0, E' = N1, F' = O1, G1' = A1, H1' = -1 + H1, I1' = -1 + H1, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t39 := {
    from   := f8;
    to     := f8;
    guard  := A1 > P1 && H1 >= 0 && L1 > 1 && P1 > N1 && 0 > N1 && C1 = 0;
    action := D' = L1, D1' = N1, E1' = 0, F1' = N1, C1' = 0, B' = 0, E' = N1, F' = O1, G1' = A1, H1' = -1 + H1, I1' = -1 + H1, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t40 := {
    from   := f8;
    to     := f8;
    guard  := A1 > P1 && H1 >= 0 && L1 > 1 && P1 > N1 && N1 > 0 && C1 = 0;
    action := D' = L1, D1' = N1, E1' = 0, F1' = N1, C1' = 0, B' = 0, E' = N1, F' = O1, G1' = A1, H1' = -1 + H1, I1' = -1 + H1, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t41 := {
    from   := f8;
    to     := f10;
    guard  := L1 > 1 && H1 >= 0 && C1 = A1;
    action := D' = L1, D1' = N1, E1' = O1, F1' = P1, C1' = M1, A1' = R1, Y' = S1, G1' = T1, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t42 := {
    from   := f13;
    to     := f8;
    guard  := N1 > 1 && E > 0 && L1 > 1 && 0 > E && B = 0 && J = 0 && C = 1;
    action := D' = L1, D1' = E, E1' = 0, F1' = E, C1' = 0, A1' = E, B' = 0, J' = 0, C' = H1 + 1, G1' = E, B1' = H1, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t43 := {
    from   := f13;
    to     := f8;
    guard  := N1 > 1 && E > 0 && L1 > 1 && B = 0 && J = 0 && C = 1;
    action := D' = L1, D1' = E, E1' = 0, F1' = E, C1' = 0, A1' = E, B' = 0, J' = 0, C' = H1 + 1, G1' = E, B1' = H1, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t44 := {
    from   := f13;
    to     := f8;
    guard  := N1 > 1 && 0 > E && L1 > 1 && B = 0 && J = 0 && C = 1;
    action := D' = L1, D1' = E, E1' = 0, F1' = E, C1' = 0, A1' = E, B' = 0, J' = 0, C' = H1 + 1, G1' = E, B1' = H1, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t45 := {
    from   := f13;
    to     := f8;
    guard  := N1 > 1 && 0 > E && L1 > 1 && E > 0 && B = 0 && J = 0 && C = 1;
    action := D' = L1, D1' = E, E1' = 0, F1' = E, C1' = 0, A1' = E, B' = 0, J' = 0, C' = H1 + 1, G1' = E, B1' = H1, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t46 := {
    from   := f16;
    to     := f8;
    guard  := N1 > 1 && E > 0 && L1 > 1 && C >= 0 && H >= 0 && 0 > E && B = 0;
    action := D' = L1, D1' = E, E1' = 0, F1' = E, C1' = 0, A1' = E, B' = 0, C' = H1 + 1, G1' = E, B1' = H1, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t47 := {
    from   := f16;
    to     := f8;
    guard  := N1 > 1 && E > 0 && L1 > 1 && C >= 0 && H >= 0 && B = 0;
    action := D' = L1, D1' = E, E1' = 0, F1' = E, C1' = 0, A1' = E, B' = 0, C' = H1 + 1, G1' = E, B1' = H1, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t48 := {
    from   := f16;
    to     := f8;
    guard  := N1 > 1 && 0 > E && L1 > 1 && C >= 0 && H >= 0 && B = 0;
    action := D' = L1, D1' = E, E1' = 0, F1' = E, C1' = 0, A1' = E, B' = 0, C' = H1 + 1, G1' = E, B1' = H1, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t49 := {
    from   := f16;
    to     := f8;
    guard  := N1 > 1 && 0 > E && L1 > 1 && C >= 0 && H >= 0 && E > 0 && B = 0;
    action := D' = L1, D1' = E, E1' = 0, F1' = E, C1' = 0, A1' = E, B' = 0, C' = H1 + 1, G1' = E, B1' = H1, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t50 := {
    from   := f9;
    to     := f1;
    guard  := L1 > 1;
    action := D' = L1, A' = 2, J1' = N1, Q' = L1, R' = O1, W' = O1, T' = O1, S' = P1, K1' = M1, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
  transition t51 := {
    from   := f9;
    to     := f10;
    guard  := 0 >= U1 && 0 >= V1 && 0 >= L1 && 0 >= W1;
    action := D' = L1, D1' = N1, E1' = O1, F1' = P1, C1' = M1, A1' = R1, B' = 0, E' = 0, A' = S1, J1' = T1, Q' = Q1, R' = X1, W' = Y1, T' = Z1, S' = A2, X' = B2, Y' = C2, G1' = D2, L1' = ?, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?;
  };
}
strategy dumb {
  Region init := { state = f9 };
}