YES
Termination proof succeeded
Initially, performed program simplifications using lexicographic rank functions:
 * Removed transitions 27, 29, 30, 35, 37, 38, 43, 44, 45, 46, 47, 48, 50, 51 using the following rank functions:
    - Rank function 1:
      RF for loc. 20: 10*___const_5_0+1-10*i4_0
      RF for loc. 21: 10*___const_5_0-10*i4_0
      RF for loc. 22: 10*___const_5_0-10*i4_0
      RF for loc. 23: 10*___const_5_0-10*i4_0
      RF for loc. 24: 10*___const_5_0-10*i4_0
      RF for loc. 33: 10*___const_5_0+2-10*i4_0
      RF for loc. 37: 10*___const_5_0-10*i4_0
      RF for loc. 41: 10*___const_5_0-10*i4_0
      Bound for (chained) transitions 47: 1
    - Rank function 2:
      RF for loc. 20: 11*___const_5_0-11*j5_0
      RF for loc. 21: 11*___const_5_0+2-11*j5_0
      RF for loc. 22: 11*___const_5_0+1-11*j5_0
      RF for loc. 23: 11*___const_5_0-11*j5_0
      RF for loc. 24: 11*___const_5_0-11*j5_0
      RF for loc. 33: 11*___const_5_0+1-11*j5_0
      RF for loc. 37: 11*___const_5_0+1-11*j5_0
      RF for loc. 41: 11*___const_5_0-11*j5_0
      Bound for (chained) transitions 46: 1
    - Rank function 3:
      RF for loc. 20: 3*___const_5_0+-4-3*k6_0
      RF for loc. 21: 3*___const_5_0-3*k6_0
      RF for loc. 22: 3*___const_5_0+-2-3*k6_0
      RF for loc. 23: 3*___const_5_0-3*k6_0
      RF for loc. 24: 3*___const_5_0+2-3*k6_0
      RF for loc. 33: 3*___const_5_0+-3-3*k6_0
      RF for loc. 37: 3*___const_5_0+-1-3*k6_0
      RF for loc. 41: 3*___const_5_0+1-3*k6_0
      Bound for (chained) transitions 44: 0
    - Rank function 4:
      RF for loc. 20: -6
      RF for loc. 21: -2
      RF for loc. 22: -4
      RF for loc. 23: -1
      RF for loc. 24: 1
      RF for loc. 33: -5
      RF for loc. 37: -3
      RF for loc. 41: 0
      Bound for (chained) transitions 27, 45: -4
      Bound for (chained) transitions 29: -5
      Bound for (chained) transitions 30: -5
      Bound for (chained) transitions 35: -2
      Bound for (chained) transitions 37: -3
      Bound for (chained) transitions 38: -3
      Bound for (chained) transitions 43: -1
      Bound for (chained) transitions 48: 1
      Bound for (chained) transitions 50: 0
      Bound for (chained) transitions 51: 0
 * Removed transitions 11, 13, 14, 19, 21, 22, 56, 57, 59 using the following rank functions:
    - Rank function 1:
      RF for loc. 16: 2*___const_5_0-2*i4_0
      RF for loc. 17: 2*___const_5_0+-1-2*i4_0
      RF for loc. 18: 2*___const_5_0+-1-2*i4_0
      RF for loc. 25: 2*___const_5_0+1-2*i4_0
      RF for loc. 29: 2*___const_5_0+-1-2*i4_0
      Bound for (chained) transitions 59: 0
    - Rank function 2:
      RF for loc. 16: 2*___const_5_0+-2-2*j5_0
      RF for loc. 17: 2*___const_5_0+1-2*j5_0
      RF for loc. 18: 2*___const_5_0-2*j5_0
      RF for loc. 25: 2*___const_5_0+-1-2*j5_0
      RF for loc. 29: 2*___const_5_0+1-2*j5_0
      Bound for (chained) transitions 57: 0
    - Rank function 3:
      RF for loc. 16: -3
      RF for loc. 17: 1
      RF for loc. 18: -1
      RF for loc. 25: -2
      RF for loc. 29: 0
      Bound for (chained) transitions 11, 56: -1
      Bound for (chained) transitions 13: -2
      Bound for (chained) transitions 14: -2
      Bound for (chained) transitions 19: 1
      Bound for (chained) transitions 21: 0
      Bound for (chained) transitions 22: 0
Errors: