YES Termination proof succeeded Initially, performed program simplifications using lexicographic rank functions: * Removed transitions 33, 35, 36, 41, 43, 44, 49, 50, 51, 53, 54, 59, 60, 61, 62, 63, 65, 66, 71, 72, 73, 74, 75, 77, 78, 83, 84, 85, 86, 87, 88, 89, 91, 92, 97, 98, 99, 100, 101, 102, 103, 104, 106, 107, 112, 113, 114, 115, 116 using the following rank functions: - Rank function 1: RF for loc. 31: -3*i_0+3*n_0 RF for loc. 32: -3*i_0+3*n_0 RF for loc. 33: -3*i_0+3*n_0 RF for loc. 34: -3*i_0+3*n_0 RF for loc. 35: -3*i_0+3*n_0 RF for loc. 36: -3*i_0+3*n_0 RF for loc. 37: -3*i_0+3*n_0 RF for loc. 38: -3*i_0+3*n_0 RF for loc. 39: -3*i_0+3*n_0 RF for loc. 40: -3*i_0+3*n_0 RF for loc. 41: -3*i_0+3*n_0 RF for loc. 42: -3*i_0+3*n_0 RF for loc. 43: -3*i_0+3*n_0 RF for loc. 44: -3*i_0+3*n_0 RF for loc. 45: -3*i_0+3*n_0 RF for loc. 46: -3*i_0+3*n_0 RF for loc. 47: -1-3*i_0+3*n_0 RF for loc. 48: -2-3*i_0+3*n_0 RF for loc. 49: -3*i_0+3*n_0 RF for loc. 50: -3*i_0+3*n_0 RF for loc. 51: -3-3*i_0+3*n_0 RF for loc. 52: -3*i_0+3*n_0 RF for loc. 53: -3*i_0+3*n_0 RF for loc. 57: -3*i_0+3*n_0 RF for loc. 61: -3*i_0+3*n_0 RF for loc. 65: -3*i_0+3*n_0 RF for loc. 69: -3*i_0+3*n_0 RF for loc. 73: -3*i_0+3*n_0 RF for loc. 77: -3*i_0+3*n_0 Bound for (chained) transitions 50: 0 Bound for (chained) transitions 60: 0 - Rank function 2: RF for loc. 31: -5*i_0+5*n_0 RF for loc. 32: -5*i_0+5*n_0 RF for loc. 33: -5*i_0+5*n_0 RF for loc. 34: -5*i_0+5*n_0 RF for loc. 35: -5*i_0+5*n_0 RF for loc. 36: -5*i_0+5*n_0 RF for loc. 37: -5*i_0+5*n_0 RF for loc. 38: -5*i_0+5*n_0 RF for loc. 39: -5*i_0+5*n_0 RF for loc. 40: -5*i_0+5*n_0 RF for loc. 41: -5*i_0+5*n_0 RF for loc. 42: -5*i_0+5*n_0 RF for loc. 43: -5*i_0+5*n_0 RF for loc. 44: -5*i_0+5*n_0 RF for loc. 45: -5*i_0+5*n_0 RF for loc. 46: -5*i_0+5*n_0 RF for loc. 47: -1-5*i_0+5*n_0 RF for loc. 48: -4-5*i_0+5*n_0 RF for loc. 49: -5*i_0+5*n_0 RF for loc. 50: -5*i_0+5*n_0 RF for loc. 51: -1-5*i_0+5*n_0 RF for loc. 52: -5*i_0+5*n_0 RF for loc. 53: -5*i_0+5*n_0 RF for loc. 57: -5*i_0+5*n_0 RF for loc. 61: -5*i_0+5*n_0 RF for loc. 65: -5*i_0+5*n_0 RF for loc. 69: -5*i_0+5*n_0 RF for loc. 73: -5*i_0+5*n_0 RF for loc. 77: -5*i_0+5*n_0 Bound for (chained) transitions 97: 0 - Rank function 3: RF for loc. 31: -4*i_0+4*n_0 RF for loc. 32: -4*i_0+4*n_0 RF for loc. 33: -4*i_0+4*n_0 RF for loc. 34: -4*i_0+4*n_0 RF for loc. 35: -4*i_0+4*n_0 RF for loc. 36: -4*i_0+4*n_0 RF for loc. 37: -4*i_0+4*n_0 RF for loc. 38: -4*i_0+4*n_0 RF for loc. 39: -4*i_0+4*n_0 RF for loc. 40: -4*i_0+4*n_0 RF for loc. 41: -4*i_0+4*n_0 RF for loc. 42: -4*i_0+4*n_0 RF for loc. 43: -4*i_0+4*n_0 RF for loc. 44: -4*i_0+4*n_0 RF for loc. 45: -4*i_0+4*n_0 RF for loc. 46: -4*i_0+4*n_0 RF for loc. 47: -2-4*i_0+4*n_0 RF for loc. 48: -3-4*i_0+4*n_0 RF for loc. 49: -1-4*i_0+4*n_0 RF for loc. 50: -4*i_0+4*n_0 RF for loc. 51: -1-4*i_0+4*n_0 RF for loc. 52: -1-4*i_0+4*n_0 RF for loc. 53: -4*i_0+4*n_0 RF for loc. 57: -4*i_0+4*n_0 RF for loc. 61: -4*i_0+4*n_0 RF for loc. 65: -4*i_0+4*n_0 RF for loc. 69: -4*i_0+4*n_0 RF for loc. 73: -4*i_0+4*n_0 RF for loc. 77: -4*i_0+4*n_0 Bound for (chained) transitions 87: 0 - Rank function 4: RF for loc. 31: 2-3*i_0+4*n_0 RF for loc. 32: 2-3*i_0+4*n_0 RF for loc. 33: 2-3*i_0+4*n_0 RF for loc. 34: 2-3*i_0+4*n_0 RF for loc. 35: 2-3*i_0+4*n_0 RF for loc. 36: 2-3*i_0+4*n_0 RF for loc. 37: 2-3*i_0+4*n_0 RF for loc. 38: 2-3*i_0+4*n_0 RF for loc. 39: 2-3*i_0+4*n_0 RF for loc. 40: 2-3*i_0+4*n_0 RF for loc. 41: 2-3*i_0+4*n_0 RF for loc. 42: 2-3*i_0+4*n_0 RF for loc. 43: 2-3*i_0+4*n_0 RF for loc. 44: 2-3*i_0+4*n_0 RF for loc. 45: 2-3*i_0+4*n_0 RF for loc. 46: 2-3*i_0+4*n_0 RF for loc. 47: 1-3*i_0+4*n_0 RF for loc. 48: -3*i_0+4*n_0 RF for loc. 49: 2-3*i_0+4*n_0 RF for loc. 50: 2-3*i_0+4*n_0 RF for loc. 51: -3*i_0+4*n_0 RF for loc. 52: 1-3*i_0+4*n_0 RF for loc. 53: 2-3*i_0+4*n_0 RF for loc. 57: 2-3*i_0+4*n_0 RF for loc. 61: 2-3*i_0+4*n_0 RF for loc. 65: 2-3*i_0+4*n_0 RF for loc. 69: 2-3*i_0+4*n_0 RF for loc. 73: 2-3*i_0+4*n_0 RF for loc. 77: 2-3*i_0+4*n_0 Bound for (chained) transitions 114: 4 - Rank function 5: RF for loc. 31: 0 RF for loc. 32: 0 RF for loc. 33: 0 RF for loc. 34: 0 RF for loc. 35: 0 RF for loc. 36: 0 RF for loc. 37: 0 RF for loc. 38: 0 RF for loc. 39: 0 RF for loc. 40: 0 RF for loc. 41: 0 RF for loc. 42: 0 RF for loc. 43: 0 RF for loc. 44: 0 RF for loc. 45: 0 RF for loc. 46: 0 RF for loc. 47: 0 RF for loc. 48: 0 RF for loc. 49: 0 RF for loc. 50: 0 RF for loc. 51: 0 RF for loc. 52: 1 RF for loc. 53: 0 RF for loc. 57: 0 RF for loc. 61: 0 RF for loc. 65: 0 RF for loc. 69: 0 RF for loc. 73: 0 RF for loc. 77: 0 Bound for (chained) transitions 113: 1 - Rank function 6: RF for loc. 31: 0 RF for loc. 32: 0 RF for loc. 33: 0 RF for loc. 34: 0 RF for loc. 35: 0 RF for loc. 36: 0 RF for loc. 37: 0 RF for loc. 38: 0 RF for loc. 39: 0 RF for loc. 40: 0 RF for loc. 41: 0 RF for loc. 42: 0 RF for loc. 43: 0 RF for loc. 44: 0 RF for loc. 45: 0 RF for loc. 46: 0 RF for loc. 47: 1 RF for loc. 48: 1 RF for loc. 49: 1 RF for loc. 50: 0 RF for loc. 51: 0 RF for loc. 52: 0 RF for loc. 53: 0 RF for loc. 57: 0 RF for loc. 61: 0 RF for loc. 65: 0 RF for loc. 69: 0 RF for loc. 73: 0 RF for loc. 77: 0 Bound for (chained) transitions 83: 1 - Rank function 7: RF for loc. 31: -9*j_0-18*k_0+18*n_0 RF for loc. 32: -1-9*j_0-18*k_0+18*n_0 RF for loc. 33: -3-9*j_0-18*k_0+18*n_0 RF for loc. 34: -21-9*j_0-18*k_0+18*n_0 RF for loc. 35: -13-9*j_0-18*k_0+18*n_0 RF for loc. 36: -19-9*j_0-18*k_0+18*n_0 RF for loc. 37: -5-9*j_0-18*k_0+18*n_0 RF for loc. 38: -7-9*j_0-18*k_0+18*n_0 RF for loc. 39: -18-9*j_0-18*k_0+18*n_0 RF for loc. 40: -16-9*j_0-18*k_0+18*n_0 RF for loc. 41: -15-9*j_0-18*k_0+18*n_0 RF for loc. 42: -16-9*j_0-18*k_0+18*n_0 RF for loc. 43: -8-9*j_0-18*k_0+18*n_0 RF for loc. 44: -10-9*j_0-18*k_0+18*n_0 RF for loc. 45: -12-9*j_0-18*k_0+18*n_0 RF for loc. 46: -11-9*j_0-18*k_0+18*n_0 RF for loc. 47: -1 RF for loc. 48: -1 RF for loc. 49: 0 RF for loc. 50: -4-9*j_0-18*k_0+18*n_0 RF for loc. 51: -9*j_0-18*k_0+18*n_0 RF for loc. 52: 1-9*j_0-18*k_0+18*n_0 RF for loc. 53: 1-9*j_0-18*k_0+18*n_0 RF for loc. 57: -2-9*j_0-18*k_0+18*n_0 RF for loc. 61: -6-9*j_0-18*k_0+18*n_0 RF for loc. 65: -9-9*j_0-18*k_0+18*n_0 RF for loc. 69: -14-9*j_0-18*k_0+18*n_0 RF for loc. 73: -17-9*j_0-18*k_0+18*n_0 RF for loc. 77: -20-9*j_0-18*k_0+18*n_0 Bound for (chained) transitions 84: 0 - Rank function 8: RF for loc. 31: -9*j_0-17*k_0+17*n_0 RF for loc. 32: -1-9*j_0-17*k_0+17*n_0 RF for loc. 33: -3-9*j_0-17*k_0+17*n_0 RF for loc. 34: -20-9*j_0-17*k_0+17*n_0 RF for loc. 35: -12-9*j_0-17*k_0+17*n_0 RF for loc. 36: -18-9*j_0-17*k_0+17*n_0 RF for loc. 37: -4-9*j_0-17*k_0+17*n_0 RF for loc. 38: -6-9*j_0-17*k_0+17*n_0 RF for loc. 39: -17-9*j_0-17*k_0+17*n_0 RF for loc. 40: -15-9*j_0-17*k_0+17*n_0 RF for loc. 41: -14-9*j_0-17*k_0+17*n_0 RF for loc. 42: -15-9*j_0-17*k_0+17*n_0 RF for loc. 43: -7-9*j_0-17*k_0+17*n_0 RF for loc. 44: -9-9*j_0-17*k_0+17*n_0 RF for loc. 45: -11-9*j_0-17*k_0+17*n_0 RF for loc. 46: -10-9*j_0-17*k_0+17*n_0 RF for loc. 47: -1 RF for loc. 48: -2 RF for loc. 49: 0 RF for loc. 50: -3-9*j_0-17*k_0+17*n_0 RF for loc. 51: -9*j_0-17*k_0+17*n_0 RF for loc. 52: 1-9*j_0-17*k_0+17*n_0 RF for loc. 53: 1-9*j_0-17*k_0+17*n_0 RF for loc. 57: -2-9*j_0-17*k_0+17*n_0 RF for loc. 61: -5-9*j_0-17*k_0+17*n_0 RF for loc. 65: -8-9*j_0-17*k_0+17*n_0 RF for loc. 69: -13-9*j_0-17*k_0+17*n_0 RF for loc. 73: -16-9*j_0-17*k_0+17*n_0 RF for loc. 77: -19-9*j_0-17*k_0+17*n_0 Bound for (chained) transitions 86: 0 - Rank function 9: RF for loc. 31: -8*j_0-16*k_0+16*n_0 RF for loc. 32: -1-8*j_0-16*k_0+16*n_0 RF for loc. 33: -3-8*j_0-16*k_0+16*n_0 RF for loc. 34: -19-8*j_0-16*k_0+16*n_0 RF for loc. 35: -12-8*j_0-16*k_0+16*n_0 RF for loc. 36: -17-8*j_0-16*k_0+16*n_0 RF for loc. 37: -4-8*j_0-16*k_0+16*n_0 RF for loc. 38: -6-8*j_0-16*k_0+16*n_0 RF for loc. 39: -16-8*j_0-16*k_0+16*n_0 RF for loc. 40: -14-8*j_0-16*k_0+16*n_0 RF for loc. 41: -13-8*j_0-16*k_0+16*n_0 RF for loc. 42: -14-8*j_0-16*k_0+16*n_0 RF for loc. 43: -7-8*j_0-16*k_0+16*n_0 RF for loc. 44: -9-8*j_0-16*k_0+16*n_0 RF for loc. 45: -11-8*j_0-16*k_0+16*n_0 RF for loc. 46: -10-8*j_0-16*k_0+16*n_0 RF for loc. 47: 1 RF for loc. 48: 0 RF for loc. 49: 2 RF for loc. 50: -3-8*j_0-16*k_0+16*n_0 RF for loc. 51: -8*j_0-16*k_0+16*n_0 RF for loc. 52: 1-8*j_0-16*k_0+16*n_0 RF for loc. 53: 1-8*j_0-16*k_0+16*n_0 RF for loc. 57: -2-8*j_0-16*k_0+16*n_0 RF for loc. 61: -5-8*j_0-16*k_0+16*n_0 RF for loc. 65: -8-8*j_0-16*k_0+16*n_0 RF for loc. 69: -13-8*j_0-16*k_0+16*n_0 RF for loc. 73: -15-8*j_0-16*k_0+16*n_0 RF for loc. 77: -18-8*j_0-16*k_0+16*n_0 Bound for (chained) transitions 74: 1 Bound for (chained) transitions 85: 2 - Rank function 10: RF for loc. 31: -5*j_0+5*n_0 RF for loc. 32: -5*j_0+5*n_0 RF for loc. 33: -5*j_0+5*n_0 RF for loc. 34: -4-5*j_0+5*n_0 RF for loc. 35: -5*j_0+5*n_0 RF for loc. 36: -3-5*j_0+5*n_0 RF for loc. 37: -5*j_0+5*n_0 RF for loc. 38: -5*j_0+5*n_0 RF for loc. 39: -2-5*j_0+5*n_0 RF for loc. 40: -1-5*j_0+5*n_0 RF for loc. 41: -5*j_0+5*n_0 RF for loc. 42: -5*j_0+5*n_0 RF for loc. 43: -5*j_0+5*n_0 RF for loc. 44: -5*j_0+5*n_0 RF for loc. 45: -5*j_0+5*n_0 RF for loc. 46: -5*j_0+5*n_0 RF for loc. 50: -5*j_0+5*n_0 RF for loc. 51: 1-5*j_0+5*n_0 RF for loc. 52: 1-5*j_0+5*n_0 RF for loc. 53: -5*j_0+5*n_0 RF for loc. 57: -5*j_0+5*n_0 RF for loc. 61: -5*j_0+5*n_0 RF for loc. 65: -5*j_0+5*n_0 RF for loc. 69: -5*j_0+5*n_0 RF for loc. 73: -1-5*j_0+5*n_0 RF for loc. 77: -3-5*j_0+5*n_0 Bound for (chained) transitions 62: 0 - Rank function 11: RF for loc. 31: -11*k_0+11*n_0 RF for loc. 32: -1-11*k_0+11*n_0 RF for loc. 33: -3-11*k_0+11*n_0 RF for loc. 34: -8-11*k_0+11*n_0 RF for loc. 35: -8-11*k_0+11*n_0 RF for loc. 36: -11*k_0+11*n_0 RF for loc. 37: -3-11*k_0+11*n_0 RF for loc. 38: -4-11*k_0+11*n_0 RF for loc. 39: -11*k_0+12*n_0 RF for loc. 40: 2-11*k_0+12*n_0 RF for loc. 41: -9-11*k_0+11*n_0 RF for loc. 42: -9-11*k_0+11*n_0 RF for loc. 43: -4-11*k_0+11*n_0 RF for loc. 44: -6-11*k_0+11*n_0 RF for loc. 45: -7-11*k_0+11*n_0 RF for loc. 46: -7-11*k_0+11*n_0 RF for loc. 50: -3-11*k_0+11*n_0 RF for loc. 51: -11*k_0+11*n_0 RF for loc. 52: 1-11*k_0+11*n_0 RF for loc. 53: 1-11*k_0+11*n_0 RF for loc. 57: -2-11*k_0+11*n_0 RF for loc. 61: -3-11*k_0+11*n_0 RF for loc. 65: -5-11*k_0+11*n_0 RF for loc. 69: -9-11*k_0+11*n_0 RF for loc. 73: 1-11*k_0+12*n_0 RF for loc. 77: -1-11*k_0+11*n_0 Bound for (chained) transitions 116: 11 - Rank function 12: RF for loc. 31: -14 RF for loc. 32: 3 RF for loc. 33: 1 RF for loc. 34: -1 RF for loc. 35: -9 RF for loc. 36: 1 RF for loc. 37: -1 RF for loc. 38: -3 RF for loc. 39: 2 RF for loc. 40: 4 RF for loc. 41: -11 RF for loc. 42: -12 RF for loc. 43: -4 RF for loc. 44: -6 RF for loc. 45: -8 RF for loc. 46: -7 RF for loc. 50: 0 RF for loc. 51: 4 RF for loc. 52: 5 RF for loc. 53: -13 RF for loc. 57: 2 RF for loc. 61: -2 RF for loc. 65: -5 RF for loc. 69: -10 RF for loc. 73: 3 RF for loc. 77: 0 Bound for (chained) transitions 33, 99: -12 Bound for (chained) transitions 35: -13 Bound for (chained) transitions 36: -13 Bound for (chained) transitions 41: 3 Bound for (chained) transitions 43: 2 Bound for (chained) transitions 44: 2 Bound for (chained) transitions 49: -1 Bound for (chained) transitions 51: -1 Bound for (chained) transitions 53: -2 Bound for (chained) transitions 54: -2 Bound for (chained) transitions 59: 2 Bound for (chained) transitions 61: -11 Bound for (chained) transitions 63: -4 Bound for (chained) transitions 65: -5 Bound for (chained) transitions 66: -5 Bound for (chained) transitions 71: -8 Bound for (chained) transitions 72: -7 Bound for (chained) transitions 73: -7 Bound for (chained) transitions 75: -9 Bound for (chained) transitions 77: -10 Bound for (chained) transitions 78: -10 Bound for (chained) transitions 88: -6 Bound for (chained) transitions 89: 4 Bound for (chained) transitions 91: 3 Bound for (chained) transitions 92: 3 Bound for (chained) transitions 98: -3 Bound for (chained) transitions 100: 0 Bound for (chained) transitions 101: 0 Bound for (chained) transitions 102: 0 Bound for (chained) transitions 103: 4 Bound for (chained) transitions 104: 1 Bound for (chained) transitions 106: 0 Bound for (chained) transitions 107: 0 Bound for (chained) transitions 112: 5 Bound for (chained) transitions 115: 1 Errors: