YES
Termination proof succeeded
Initially, performed program simplifications using lexicographic rank functions:
 * Removed transitions 40, 41, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 63, 64 using the following rank functions:
    - Rank function 1:
      RF for loc. 22: 8*x0_0-8*x2_0
      RF for loc. 24: -1+8*x0_0-8*x2_0
      RF for loc. 26: 8*x0_0-8*x2_0
      RF for loc. 27: 8*x0_0-8*x2_0
      RF for loc. 28: -1+8*x0_0-8*x2_0
      RF for loc. 29: 8*x0_0-8*x2_0
      RF for loc. 36: 8*x0_0-8*x2_0
      Bound for (chained) transitions 40, 41, 51: 15
    - Rank function 2:
      RF for loc. 22: 1+3*x0_0-3*x3_0
      RF for loc. 24: -2+3*oldX0_post-3*oldX3_post
      RF for loc. 26: -1+3*x0_0-3*x3_0
      RF for loc. 27: -1+3*x0_0-3*x3_0
      RF for loc. 28: -1+3*x0_0-3*x3_0
      RF for loc. 29: -1+3*x0_0-3*x3_0
      RF for loc. 36: 3*x0_0-3*x3_0
      Bound for (chained) transitions 64: 0
    - Rank function 3:
      RF for loc. 22: 2
      RF for loc. 24: -1
      RF for loc. 26: 3
      RF for loc. 27: 4
      RF for loc. 28: 0
      RF for loc. 29: 5
      RF for loc. 36: 1
      Bound for (chained) transitions 52, 55: 4
      Bound for (chained) transitions 53: 3
      Bound for (chained) transitions 54: 4
      Bound for (chained) transitions 56: 0
      Bound for (chained) transitions 57: 0
      Bound for (chained) transitions 58: 5
      Bound for (chained) transitions 59: 5
      Bound for (chained) transitions 60: 2
      Bound for (chained) transitions 63: 1
 * Removed transitions 42, 43, 45, 47, 48 using the following rank functions:
    - Rank function 1:
      RF for loc. 30: 3*x0_0-3*x1_0
      RF for loc. 31: 2+3*x0_0-3*x1_0
      RF for loc. 32: 1+3*x0_0-3*x1_0
      Bound for (chained) transitions 47: 4
      Bound for (chained) transitions 48: 4
    - Rank function 2:
      RF for loc. 30: 0
      RF for loc. 31: -1
      RF for loc. 32: -2
      Bound for (chained) transitions 42: 0
      Bound for (chained) transitions 43: 0
    - Rank function 3:
      RF for loc. 31: 0
      RF for loc. 32: -1
      Bound for (chained) transitions 45: 0
Errors: