YES Termination proof succeeded Initially, performed program simplifications using lexicographic rank functions: * Removed transitions 117 using the following rank functions: - Rank function 1: RF for loc. 45: -66*i_0 RF for loc. 46: -66*i_0 RF for loc. 47: -66*i_0 RF for loc. 48: -66*i_0 RF for loc. 49: -66*i_0 RF for loc. 50: -66*i_0 RF for loc. 51: -66*i_0 RF for loc. 52: -66*i_0 RF for loc. 57: -66*i_0 RF for loc. 58: -66*i_0 RF for loc. 59: -66*i_0 RF for loc. 60: -66*i_0 RF for loc. 61: -66*i_0 RF for loc. 62: -66*i_0 RF for loc. 63: -66*i_0 RF for loc. 64: -66*i_0 RF for loc. 65: -66*i_0 RF for loc. 66: -66*i_0 RF for loc. 67: -66*i_0 RF for loc. 68: -66*i_0 RF for loc. 69: -66*i_0 RF for loc. 70: -66*i_0 RF for loc. 71: -66*i_0 RF for loc. 72: -66*i_0 RF for loc. 73: -1-66*i_0 RF for loc. 74: -1-66*i_0 RF for loc. 77: 9-66*i_0 RF for loc. 78: 10-66*i_0 RF for loc. 79: 11-66*i_0 RF for loc. 80: 11-66*i_0 RF for loc. 81: 11-66*i_0 RF for loc. 82: 11-66*i_0 RF for loc. 83: 11-66*i_0 RF for loc. 85: -66*i_0 RF for loc. 93: -66*i_0 RF for loc. 97: -66*i_0 RF for loc. 105: 11-66*i_0 RF for loc. 109: 11-66*i_0 RF for loc. 113: 12-66*i_0 RF for loc. 121: -1-66*i_0 RF for loc. 125: -66*i_0 RF for loc. 129: -66*i_0 RF for loc. 133: -66*i_0 Bound for (chained) transitions 117: -189 * Removed transitions 157, 159, 161, 162 using the following rank functions: - Rank function 1: RF for loc. 76: -1-2*ip_0+2*n_0 RF for loc. 117: -2*ip_0+2*n_0 Bound for (chained) transitions 157, 159: -1 - Rank function 2: RF for loc. 76: 0 RF for loc. 117: 1 Bound for (chained) transitions 161: 1 Bound for (chained) transitions 162: 1 * Removed transitions 65, 66, 84, 86, 87, 107, 120, 122, 123 using the following rank functions: - Rank function 1: RF for loc. 53: -2-5*ip_0+5*n_0 RF for loc. 55: -2-5*ip_0+5*n_0 RF for loc. 56: -1-5*ip_0+5*n_0 RF for loc. 89: -2-5*ip_0+5*n_0 RF for loc. 101: -5*ip_0+5*n_0 Bound for (chained) transitions 107: -1 - Rank function 2: RF for loc. 53: -1-3*iq_0+3*n_0 RF for loc. 55: 1-3*iq_0+3*n_0 RF for loc. 56: -2-4*iq_0+4*n_0 RF for loc. 89: -3*iq_0+3*n_0 RF for loc. 101: -1-4*iq_0+4*n_0 Bound for (chained) transitions 66: -1 - Rank function 3: RF for loc. 53: -1 RF for loc. 55: 1 RF for loc. 56: -3 RF for loc. 89: 0 RF for loc. 101: -2 Bound for (chained) transitions 65, 120: -1 Bound for (chained) transitions 84: 1 Bound for (chained) transitions 86: 0 Bound for (chained) transitions 87: 0 Bound for (chained) transitions 122: -2 Bound for (chained) transitions 123: -2 Errors: