YES Termination proof succeeded Initially, performed program simplifications using lexicographic rank functions: * Removed transitions 44, 46, 47, 52, 53, 54, 56, 57, 62, 63, 64, 65, 67, 68 using the following rank functions: - Rank function 1: RF for loc. 29: 1+4*nDim_0-3*ni_0 RF for loc. 30: 4*nDim_0-3*ni_0 RF for loc. 31: 4*nDim_0-3*ni_0 RF for loc. 32: 4*nDim_0-3*ni_0 RF for loc. 33: 4*nDim_0-3*ni_0 RF for loc. 42: 2+4*nDim_0-3*ni_0 RF for loc. 46: 4*nDim_0-3*ni_0 RF for loc. 50: 4*nDim_0-3*ni_0 Bound for (chained) transitions 64: 6 - Rank function 2: RF for loc. 29: 9+8*nDim_0-10*nj_0 RF for loc. 30: 10*nDim_0-10*nj_0 RF for loc. 31: 9+10*nDim_0-10*nj_0 RF for loc. 32: 10*nDim_0-10*nj_0 RF for loc. 33: 7+10*nDim_0-10*nj_0 RF for loc. 42: 10+8*nDim_0-10*nj_0 RF for loc. 46: 8+10*nDim_0-10*nj_0 RF for loc. 50: 10*nDim_0-10*nj_0 Bound for (chained) transitions 63: 17 - Rank function 3: RF for loc. 29: 1-3*nk_0 RF for loc. 30: 3*nDim_0-3*nk_0 RF for loc. 31: 5-3*nk_0 RF for loc. 32: 2+3*nDim_0-3*nk_0 RF for loc. 33: 3-3*nk_0 RF for loc. 42: 2-3*nk_0 RF for loc. 46: 4-3*nk_0 RF for loc. 50: 1+3*nDim_0-3*nk_0 Bound for (chained) transitions 53: 3 - Rank function 4: RF for loc. 29: -3 RF for loc. 30: 2 RF for loc. 31: 1 RF for loc. 32: 4 RF for loc. 33: -1 RF for loc. 42: -2 RF for loc. 46: 0 RF for loc. 50: 3 Bound for (chained) transitions 44, 62: -1 Bound for (chained) transitions 46: -2 Bound for (chained) transitions 47: -2 Bound for (chained) transitions 52: 2 Bound for (chained) transitions 54: 1 Bound for (chained) transitions 56: 0 Bound for (chained) transitions 57: 0 Bound for (chained) transitions 65: 4 Bound for (chained) transitions 67: 3 Bound for (chained) transitions 68: 3 * Removed transitions 28, 30, 31, 36, 38, 39, 73, 74, 76 using the following rank functions: - Rank function 1: RF for loc. 25: nDim_0-8*ni_0 RF for loc. 26: -nDim_0-8*ni_0 RF for loc. 27: -nDim_0-8*ni_0 RF for loc. 34: 2+nDim_0-8*ni_0 RF for loc. 38: -nDim_0-8*ni_0 Bound for (chained) transitions 76: -6 - Rank function 2: RF for loc. 25: -1-7*nj_0 RF for loc. 26: 2-7*nj_0 RF for loc. 27: -7*nj_0 RF for loc. 34: -7*nj_0 RF for loc. 38: 1-7*nj_0 Bound for (chained) transitions 74: -7 - Rank function 3: RF for loc. 25: -3 RF for loc. 26: 1 RF for loc. 27: -1 RF for loc. 34: -2 RF for loc. 38: 0 Bound for (chained) transitions 28, 73: -1 Bound for (chained) transitions 30: -2 Bound for (chained) transitions 31: -2 Bound for (chained) transitions 36: 1 Bound for (chained) transitions 38: 0 Bound for (chained) transitions 39: 0 Errors: