YES Termination proof succeeded Initially, performed program simplifications using lexicographic rank functions: * Removed transitions 30, 31, 33, 34, 39, 41, 42, 47, 48, 49, 51, 52, 57, 58, 59, 60, 61, 62, 63, 64, 65, 67, 68, 73, 74, 75, 76, 77, 78, 80, 81, 86, 87, 88, 89, 90, 91, 92, 93, 95, 96, 101, 102, 103, 104, 105, 106, 108, 109 using the following rank functions: - Rank function 1: RF for loc. 27: -2-10*m_0+10*n_0 RF for loc. 28: -2-10*m_0+10*n_0 RF for loc. 29: -4-10*m_0+10*n_0 RF for loc. 30: -4-10*m_0+10*n_0 RF for loc. 31: -9-10*m_0+10*n_0 RF for loc. 32: -8-10*m_0+10*n_0 RF for loc. 33: -8-10*m_0+10*n_0 RF for loc. 34: -7-10*m_0+10*n_0 RF for loc. 35: -7-10*m_0+10*n_0 RF for loc. 36: -8-10*m_0+10*n_0 RF for loc. 37: -8-10*m_0+10*n_0 RF for loc. 38: -8-10*m_0+10*n_0 RF for loc. 39: -8-10*m_0+10*n_0 RF for loc. 40: -8-10*m_0+10*n_0 RF for loc. 41: -8-10*m_0+10*n_0 RF for loc. 42: -8-10*m_0+10*n_0 RF for loc. 43: -8-10*m_0+10*n_0 RF for loc. 44: -3-10*m_0+10*n_0 RF for loc. 45: -2-10*m_0+10*n_0 RF for loc. 46: -2-10*m_0+10*n_0 RF for loc. 47: -1-10*m_0+10*n_0 RF for loc. 49: -2-10*m_0+10*n_0 RF for loc. 53: -4-10*m_0+10*n_0 RF for loc. 57: -7-10*m_0+10*n_0 RF for loc. 61: -8-10*m_0+10*n_0 RF for loc. 65: -8-10*m_0+10*n_0 RF for loc. 69: -8-10*m_0+10*n_0 RF for loc. 73: -10*m_0+10*n_0 Bound for (chained) transitions 30: 9 - Rank function 2: RF for loc. 27: 0 RF for loc. 28: 0 RF for loc. 29: -2 RF for loc. 30: -2 RF for loc. 31: -6 RF for loc. 32: -5 RF for loc. 33: -5 RF for loc. 34: -3 RF for loc. 35: -3 RF for loc. 36: -5 RF for loc. 37: -5 RF for loc. 38: -5 RF for loc. 39: -5 RF for loc. 40: -5 RF for loc. 41: -5 RF for loc. 42: -5 RF for loc. 43: -4 RF for loc. 44: -1 RF for loc. 45: 0 RF for loc. 46: 0 RF for loc. 47: -8 RF for loc. 49: 0 RF for loc. 53: -2 RF for loc. 57: -3 RF for loc. 61: -5 RF for loc. 65: -5 RF for loc. 69: -5 RF for loc. 73: -7 Bound for (chained) transitions 75: -4 Bound for (chained) transitions 77: -4 Bound for (chained) transitions 89: -2 Bound for (chained) transitions 90: -1 Bound for (chained) transitions 92: -1 Bound for (chained) transitions 105: 0 Bound for (chained) transitions 108: -7 - Rank function 3: RF for loc. 27: 2-5*j_0+5*n_0 RF for loc. 28: -5*j_0+5*n_0 RF for loc. 29: 2-3*j_0+3*n_0 RF for loc. 30: -3*j_0+3*n_0 RF for loc. 31: 2-9*i_0-2*j_0 RF for loc. 32: -3-9*i_0-2*j_0 RF for loc. 33: 5-9*i_0-2*j_0 RF for loc. 34: 9-9*i_0-2*j_0 RF for loc. 35: 7-9*i_0-2*j_0 RF for loc. 36: -2-9*i_0-2*j_0 RF for loc. 37: -1-9*i_0-2*j_0 RF for loc. 38: -9*i_0-2*j_0 RF for loc. 39: 1-9*i_0-2*j_0 RF for loc. 40: 1-9*i_0-2*j_0 RF for loc. 41: 2-9*i_0-2*j_0 RF for loc. 42: 3-9*i_0-2*j_0 RF for loc. 43: 6-9*i_0-2*j_0 RF for loc. 44: 3-3*j_0+3*n_0 RF for loc. 45: -2-5*j_0+5*n_0 RF for loc. 46: -1-5*j_0+5*n_0 RF for loc. 47: -9*i_0-2*j_0 RF for loc. 49: 1-5*j_0+5*n_0 RF for loc. 53: 1-3*j_0+3*n_0 RF for loc. 57: 8-9*i_0-2*j_0 RF for loc. 61: 4-9*i_0-2*j_0 RF for loc. 65: -9*i_0-2*j_0 RF for loc. 69: -1-9*i_0-2*j_0 RF for loc. 73: 1-9*i_0-2*j_0 Bound for (chained) transitions 88: 0 Bound for (chained) transitions 104: 0 - Rank function 4: RF for loc. 27: -2 RF for loc. 28: -4 RF for loc. 29: 1 RF for loc. 30: -1 RF for loc. 31: 2-11*i_0-2*j_0 RF for loc. 32: -5-11*i_0-2*j_0 RF for loc. 33: 5-11*i_0-2*j_0 RF for loc. 34: 8-11*i_0-2*j_0 RF for loc. 35: 7-11*i_0-2*j_0 RF for loc. 36: -4-11*i_0-2*j_0 RF for loc. 37: -2-11*i_0-2*j_0 RF for loc. 38: -1-11*i_0-2*j_0 RF for loc. 39: -11*i_0-2*j_0 RF for loc. 40: 1-11*i_0-2*j_0 RF for loc. 41: 2-11*i_0-2*j_0 RF for loc. 42: 3-11*i_0-2*j_0 RF for loc. 43: 6-11*i_0-2*j_0 RF for loc. 44: 1 RF for loc. 45: -1 RF for loc. 46: 0 RF for loc. 47: -11*i_0-2*j_0 RF for loc. 49: -3 RF for loc. 53: 0 RF for loc. 57: 8-11*i_0-2*j_0 RF for loc. 61: 4-11*i_0-2*j_0 RF for loc. 65: -1-11*i_0-2*j_0 RF for loc. 69: -3-11*i_0-2*j_0 RF for loc. 73: 1-11*i_0-2*j_0 Bound for (chained) transitions 31: -2 Bound for (chained) transitions 33: -3 Bound for (chained) transitions 34: -3 Bound for (chained) transitions 39: 1 Bound for (chained) transitions 41: 0 Bound for (chained) transitions 101: -1 Bound for (chained) transitions 102: 0 Bound for (chained) transitions 103: 0 - Rank function 5: RF for loc. 29: -1 RF for loc. 30: 0 RF for loc. 31: 2-11*i_0-3*j_0 RF for loc. 32: -5-11*i_0-3*j_0 RF for loc. 33: 5-11*i_0-3*j_0 RF for loc. 34: 9-11*i_0-3*j_0 RF for loc. 35: 7-11*i_0-3*j_0 RF for loc. 36: -4-11*i_0-3*j_0 RF for loc. 37: -3-11*i_0-3*j_0 RF for loc. 38: -2-11*i_0-3*j_0 RF for loc. 39: -11*i_0-3*j_0 RF for loc. 40: 1-11*i_0-3*j_0 RF for loc. 41: 2-11*i_0-3*j_0 RF for loc. 42: 3-11*i_0-3*j_0 RF for loc. 43: 6-11*i_0-3*j_0 RF for loc. 44: 0 RF for loc. 47: -11*i_0-3*j_0 RF for loc. 53: 1 RF for loc. 57: 8-11*i_0-3*j_0 RF for loc. 61: 4-11*i_0-3*j_0 RF for loc. 65: -1-11*i_0-3*j_0 RF for loc. 69: -3-11*i_0-3*j_0 RF for loc. 73: 1-11*i_0-3*j_0 Bound for (chained) transitions 91: 0 - Rank function 6: RF for loc. 30: 0 RF for loc. 31: -20*i_0-3*j_0-19*x_0 RF for loc. 32: -1-20*i_0-3*j_0-19*x_0 RF for loc. 33: 18-20*i_0-3*j_0-19*x_0 RF for loc. 34: 3-20*i_0-3*j_0 RF for loc. 35: 1-20*i_0-3*j_0 RF for loc. 36: -20*i_0-3*j_0-19*x_0 RF for loc. 37: 1-20*i_0-3*j_0-19*x_0 RF for loc. 38: 1-20*i_0-3*j_0-19*x_0 RF for loc. 39: 2-20*i_0-3*j_0-19*x_0 RF for loc. 40: 3-20*i_0-3*j_0-19*x_0 RF for loc. 41: 15-20*i_0-3*j_0-19*x_0 RF for loc. 42: 16-20*i_0-3*j_0-19*x_0 RF for loc. 43: -20*i_0-3*j_0 RF for loc. 47: -2-20*i_0-3*j_0-19*x_0 RF for loc. 53: 1 RF for loc. 57: 2-20*i_0-3*j_0 RF for loc. 61: 17-20*i_0-3*j_0-19*x_0 RF for loc. 65: 1-20*i_0-3*j_0-19*x_0 RF for loc. 69: 1-20*i_0-3*j_0-19*x_0 RF for loc. 73: -1-20*i_0-3*j_0-19*x_0 Bound for (chained) transitions 42: 1 - Rank function 7: RF for loc. 31: 2-19*i_0+19*n_0 RF for loc. 32: -11-19*i_0+19*n_0 RF for loc. 33: 4-19*i_0+19*n_0 RF for loc. 34: 6-19*i_0+19*n_0 RF for loc. 35: 6-19*i_0+19*n_0 RF for loc. 36: -10-19*i_0+19*n_0 RF for loc. 37: -10-19*i_0+19*n_0 RF for loc. 38: -9-19*i_0+19*n_0 RF for loc. 39: -9-19*i_0+19*n_0 RF for loc. 40: -8-19*i_0+19*n_0 RF for loc. 41: 2-19*i_0+19*n_0 RF for loc. 42: 3-19*i_0+19*n_0 RF for loc. 43: 5-19*i_0+19*n_0 RF for loc. 47: -19*i_0+19*n_0 RF for loc. 57: 6-19*i_0+19*n_0 RF for loc. 61: 3-19*i_0+19*n_0 RF for loc. 65: -9-19*i_0+19*n_0 RF for loc. 69: -10-19*i_0+19*n_0 RF for loc. 73: 1-19*i_0+19*n_0 Bound for (chained) transitions 73: 3 - Rank function 8: RF for loc. 31: 2-9*j_0+9*n_0 RF for loc. 32: 6-9*j_0+9*n_0 RF for loc. 33: 5-9*j_0+9*n_0 RF for loc. 34: 8-9*j_0+9*n_0 RF for loc. 35: 7-9*j_0+9*n_0 RF for loc. 36: 7-9*j_0+9*n_0 RF for loc. 37: 9-9*j_0+9*n_0 RF for loc. 38: 10-9*j_0+9*n_0 RF for loc. 39: 12-9*j_0+9*n_0 RF for loc. 40: 13-9*j_0+9*n_0 RF for loc. 41: 14-9*j_0+9*n_0 RF for loc. 42: 3-9*j_0+9*n_0 RF for loc. 43: 6-9*j_0+9*n_0 RF for loc. 47: -9*j_0+9*n_0 RF for loc. 57: 7-9*j_0+9*n_0 RF for loc. 61: 4-9*j_0+9*n_0 RF for loc. 65: 11-9*j_0+9*n_0 RF for loc. 69: 8-9*j_0+9*n_0 RF for loc. 73: 1-9*j_0+9*n_0 Bound for (chained) transitions 57: 7 Bound for (chained) transitions 59: 10 Bound for (chained) transitions 86: 7 - Rank function 9: RF for loc. 31: -6 RF for loc. 32: -2 RF for loc. 33: -3 RF for loc. 34: 1 RF for loc. 35: -1 RF for loc. 36: -1 RF for loc. 37: 1 RF for loc. 38: 2 RF for loc. 39: 4 RF for loc. 40: 5 RF for loc. 41: 6 RF for loc. 42: -5 RF for loc. 43: -2 RF for loc. 47: -8 RF for loc. 57: 0 RF for loc. 61: -4 RF for loc. 65: 3 RF for loc. 69: 0 RF for loc. 73: -7 Bound for (chained) transitions 47, 106: -6 Bound for (chained) transitions 48: -2 Bound for (chained) transitions 49: 1 Bound for (chained) transitions 51: 0 Bound for (chained) transitions 52: 0 Bound for (chained) transitions 58: -1 Bound for (chained) transitions 60: 2 Bound for (chained) transitions 61: 5 Bound for (chained) transitions 62: 6 Bound for (chained) transitions 63: 6 Bound for (chained) transitions 64: 6 Bound for (chained) transitions 65: -3 Bound for (chained) transitions 67: -4 Bound for (chained) transitions 68: -4 Bound for (chained) transitions 74: -5 Bound for (chained) transitions 76: -2 Bound for (chained) transitions 78: 4 Bound for (chained) transitions 80: 3 Bound for (chained) transitions 81: 3 Bound for (chained) transitions 87: -1 Bound for (chained) transitions 93: 1 Bound for (chained) transitions 95: 0 Bound for (chained) transitions 96: 0 Bound for (chained) transitions 109: -7 Errors: