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