YES Termination proof succeeded Initially, performed program simplifications using lexicographic rank functions: * Removed transitions 53, 54, 55, 57, 58, 63, 64, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 92, 93, 94, 95, 96, 98, 99, 104, 105, 108, 110, 111, 116, 117, 118, 119, 128, 129, 130, 132, 133, 138, 139, 140, 142, 143, 148, 149, 151, 152, 167, 168, 169, 171, 172, 177, 178, 179, 181, 182, 187, 188, 189, 191, 192, 197, 198, 199, 201, 202 using the following rank functions: - Rank function 1: RF for loc. 45: 1-12*iq_0+12*n_0 RF for loc. 46: 1-12*iq_0+12*n_0 RF for loc. 47: -12*iq_0+12*n_0 RF for loc. 48: -1-12*iq_0+12*n_0 RF for loc. 49: -1-12*iq_0+12*n_0 RF for loc. 50: -1-12*iq_0+12*n_0 RF for loc. 51: -1-12*iq_0+12*n_0 RF for loc. 52: -12*iq_0+12*n_0 RF for loc. 57: 3-12*iq_0+12*n_0 RF for loc. 58: 2-12*iq_0+12*n_0 RF for loc. 59: 3-12*iq_0+12*n_0 RF for loc. 60: 3-12*iq_0+12*n_0 RF for loc. 61: 4-12*iq_0+12*n_0 RF for loc. 62: -2-12*iq_0+12*n_0 RF for loc. 63: 5-12*iq_0+12*n_0 RF for loc. 64: 6-12*iq_0+12*n_0 RF for loc. 65: 6-12*iq_0+12*n_0 RF for loc. 66: 9-12*iq_0+12*n_0 RF for loc. 67: 7-12*iq_0+12*n_0 RF for loc. 68: 8-12*iq_0+12*n_0 RF for loc. 69: 9-12*iq_0+12*n_0 RF for loc. 70: 9-12*iq_0+12*n_0 RF for loc. 71: 9-12*iq_0+12*n_0 RF for loc. 72: 9-12*iq_0+12*n_0 RF for loc. 73: 9-12*iq_0+12*n_0 RF for loc. 74: 9-12*iq_0+12*n_0 RF for loc. 77: 9-12*iq_0+12*n_0 RF for loc. 78: 9-12*iq_0+12*n_0 RF for loc. 79: 9-12*iq_0+12*n_0 RF for loc. 80: 9-12*iq_0+12*n_0 RF for loc. 81: 9-12*iq_0+12*n_0 RF for loc. 82: 9-12*iq_0+12*n_0 RF for loc. 83: 9-12*iq_0+12*n_0 RF for loc. 85: 1-12*iq_0+12*n_0 RF for loc. 93: 9-12*iq_0+12*n_0 RF for loc. 97: 9-12*iq_0+12*n_0 RF for loc. 105: 9-12*iq_0+12*n_0 RF for loc. 109: 9-12*iq_0+12*n_0 RF for loc. 113: 9-12*iq_0+12*n_0 RF for loc. 121: 9-12*iq_0+12*n_0 RF for loc. 125: -1-12*iq_0+12*n_0 RF for loc. 129: -1-12*iq_0+12*n_0 RF for loc. 133: -12*iq_0+12*n_0 Bound for (chained) transitions 129: 9 - Rank function 2: RF for loc. 45: -13*iq_0+13*n_0 RF for loc. 46: -13*iq_0+13*n_0 RF for loc. 47: -13*iq_0+13*n_0 RF for loc. 48: -2-13*iq_0+13*n_0 RF for loc. 49: -2-13*iq_0+13*n_0 RF for loc. 50: -1-13*iq_0+13*n_0 RF for loc. 51: -1-13*iq_0+13*n_0 RF for loc. 52: -13*iq_0+13*n_0 RF for loc. 57: 2-13*iq_0+13*n_0 RF for loc. 58: 1-13*iq_0+13*n_0 RF for loc. 59: 3-13*iq_0+13*n_0 RF for loc. 60: 4-13*iq_0+13*n_0 RF for loc. 61: 4-13*iq_0+13*n_0 RF for loc. 62: -3-13*iq_0+13*n_0 RF for loc. 63: 5-13*iq_0+13*n_0 RF for loc. 64: 7-13*iq_0+13*n_0 RF for loc. 65: 5-13*iq_0+13*n_0 RF for loc. 66: 9-13*iq_0+13*n_0 RF for loc. 67: 6-13*iq_0+13*n_0 RF for loc. 68: 7-13*iq_0+13*n_0 RF for loc. 69: 8-13*iq_0+13*n_0 RF for loc. 70: 9-13*iq_0+13*n_0 RF for loc. 71: 9-13*iq_0+13*n_0 RF for loc. 72: 9-13*iq_0+13*n_0 RF for loc. 73: 9-13*iq_0+13*n_0 RF for loc. 74: 9-13*iq_0+13*n_0 RF for loc. 77: 9-13*iq_0+13*n_0 RF for loc. 78: 9-13*iq_0+13*n_0 RF for loc. 79: 9-13*iq_0+13*n_0 RF for loc. 80: 9-13*iq_0+13*n_0 RF for loc. 81: 9-13*iq_0+13*n_0 RF for loc. 82: 9-13*iq_0+13*n_0 RF for loc. 83: 9-13*iq_0+13*n_0 RF for loc. 85: -13*iq_0+13*n_0 RF for loc. 93: 9-13*iq_0+13*n_0 RF for loc. 97: 9-13*iq_0+13*n_0 RF for loc. 105: 9-13*iq_0+13*n_0 RF for loc. 109: 9-13*iq_0+13*n_0 RF for loc. 113: 9-13*iq_0+13*n_0 RF for loc. 121: 9-13*iq_0+13*n_0 RF for loc. 125: -2-13*iq_0+13*n_0 RF for loc. 129: -1-13*iq_0+13*n_0 RF for loc. 133: -13*iq_0+13*n_0 Bound for (chained) transitions 95: 9 - Rank function 3: RF for loc. 45: 2-61*i_0 RF for loc. 46: 2-61*i_0 RF for loc. 47: 1-61*i_0 RF for loc. 48: -1-61*i_0 RF for loc. 49: -1-61*i_0 RF for loc. 50: -61*i_0 RF for loc. 51: -61*i_0 RF for loc. 52: 1-61*i_0 RF for loc. 57: 3-61*i_0 RF for loc. 58: 2-61*i_0 RF for loc. 59: 4-61*i_0 RF for loc. 60: 5-61*i_0 RF for loc. 61: 6-61*i_0 RF for loc. 62: -2-61*i_0 RF for loc. 63: 7-61*i_0 RF for loc. 64: 7-61*i_0 RF for loc. 65: 7-61*i_0 RF for loc. 66: -3-61*i_0 RF for loc. 67: 7-61*i_0 RF for loc. 68: 7-61*i_0 RF for loc. 69: 7-61*i_0 RF for loc. 70: -3-61*i_0 RF for loc. 71: -3-61*i_0 RF for loc. 72: -3-61*i_0 RF for loc. 73: -4-61*i_0 RF for loc. 74: -4-61*i_0 RF for loc. 77: -3-61*i_0 RF for loc. 78: -2-61*i_0 RF for loc. 79: -2-61*i_0 RF for loc. 80: -2-61*i_0 RF for loc. 81: -2-61*i_0 RF for loc. 82: -2-61*i_0 RF for loc. 83: -1-61*i_0 RF for loc. 85: 2-61*i_0 RF for loc. 93: -3-61*i_0 RF for loc. 97: -3-61*i_0 RF for loc. 105: -2-61*i_0 RF for loc. 109: -2-61*i_0 RF for loc. 113: -61*i_0 RF for loc. 121: -4-61*i_0 RF for loc. 125: -1-61*i_0 RF for loc. 129: -61*i_0 RF for loc. 133: 1-61*i_0 Bound for (chained) transitions 148: -3051 - Rank function 4: RF for loc. 45: 2-4*ip_0+4*n_0 RF for loc. 46: 2-4*ip_0+4*n_0 RF for loc. 47: 1-4*ip_0+4*n_0 RF for loc. 48: -4*ip_0+4*n_0 RF for loc. 49: -4*ip_0+4*n_0 RF for loc. 50: -4*ip_0+4*n_0 RF for loc. 51: -4*ip_0+4*n_0 RF for loc. 52: 1-4*ip_0+4*n_0 RF for loc. 57: 4-4*ip_0+4*n_0 RF for loc. 58: 3-4*ip_0+4*n_0 RF for loc. 59: 5-4*ip_0+4*n_0 RF for loc. 60: 6-4*ip_0+4*n_0 RF for loc. 61: 7-4*ip_0+4*n_0 RF for loc. 62: -1-4*ip_0+4*n_0 RF for loc. 63: 8-4*ip_0+4*n_0 RF for loc. 64: 9-4*ip_0+4*n_0 RF for loc. 65: 9-4*ip_0+4*n_0 RF for loc. 66: -2-4*ip_0+4*n_0 RF for loc. 67: 10-4*ip_0+4*n_0 RF for loc. 68: 11-4*ip_0+4*n_0 RF for loc. 69: 11-4*ip_0+4*n_0 RF for loc. 70: -4-4*ip_0+4*n_0 RF for loc. 71: -1-4*ip_0+4*n_0 RF for loc. 72: -2-4*ip_0+4*n_0 RF for loc. 73: -3-4*ip_0+4*n_0 RF for loc. 74: -7-4*ip_0+4*n_0 RF for loc. 77: -4*ip_0+4*n_0 RF for loc. 78: 1-4*ip_0+4*n_0 RF for loc. 79: -4*ip_0+4*n_0 RF for loc. 80: 3-4*ip_0+4*n_0 RF for loc. 81: 1-4*ip_0+4*n_0 RF for loc. 82: 2-4*ip_0+4*n_0 RF for loc. 83: -9-4*ip_0+4*n_0 RF for loc. 85: 2-4*ip_0+4*n_0 RF for loc. 93: -3-4*ip_0+4*n_0 RF for loc. 97: -1-4*ip_0+4*n_0 RF for loc. 105: 1-4*ip_0+4*n_0 RF for loc. 109: 2-4*ip_0+4*n_0 RF for loc. 113: -8-4*ip_0+4*n_0 RF for loc. 121: -4-4*ip_0+4*n_0 RF for loc. 125: -4*ip_0+4*n_0 RF for loc. 129: -4*ip_0+4*n_0 RF for loc. 133: 1-4*ip_0+4*n_0 Bound for (chained) transitions 139: 6 - Rank function 5: RF for loc. 45: 3+2*iq_0-2*j_0 RF for loc. 46: 4+2*iq_0-2*j_0 RF for loc. 47: 2+2*iq_0-2*j_0 RF for loc. 48: -2+2*iq_0-2*j_0 RF for loc. 49: -2+2*iq_0-2*j_0 RF for loc. 50: -1+2*iq_0-2*j_0 RF for loc. 51: 2*iq_0-2*j_0 RF for loc. 52: 1+2*iq_0-2*j_0 RF for loc. 57: 6+2*iq_0-2*j_0 RF for loc. 58: 5+2*iq_0-2*j_0 RF for loc. 59: 7+2*iq_0-2*j_0 RF for loc. 60: 8+2*iq_0-2*j_0 RF for loc. 61: 9+2*iq_0-2*j_0 RF for loc. 62: -3+2*iq_0-2*j_0 RF for loc. 63: 10+2*iq_0-2*j_0 RF for loc. 64: 11+2*iq_0-2*j_0 RF for loc. 65: 11+2*iq_0-2*j_0 RF for loc. 66: -6+2*iq_0-2*j_0 RF for loc. 67: 12+2*iq_0-2*j_0 RF for loc. 68: 13+2*iq_0-2*j_0 RF for loc. 69: 14+2*iq_0-2*j_0 RF for loc. 70: -6+2*iq_0-2*j_0 RF for loc. 71: -6+2*iq_0-2*j_0 RF for loc. 72: -6+2*iq_0-2*j_0 RF for loc. 73: -6-3*ip_0+2*iq_0-2*j_0+3*n_0 RF for loc. 74: -8-3*ip_0+2*iq_0-2*j_0+3*n_0 RF for loc. 77: -5+2*iq_0-2*j_0 RF for loc. 78: -4+2*iq_0-2*j_0 RF for loc. 79: 2*iq_0-2*j_0 RF for loc. 80: -1+2*iq_0-2*j_0 RF for loc. 81: 2+2*iq_0-2*j_0 RF for loc. 82: -3+2*iq_0-2*j_0 RF for loc. 83: -10-3*ip_0+2*iq_0-2*j_0+3*n_0 RF for loc. 85: 4+2*iq_0-2*j_0 RF for loc. 93: -6+2*iq_0-2*j_0 RF for loc. 97: -6+2*iq_0-2*j_0 RF for loc. 105: 1+2*iq_0-2*j_0 RF for loc. 109: -2+2*iq_0-2*j_0 RF for loc. 113: -9-3*ip_0+2*iq_0-2*j_0+3*n_0 RF for loc. 121: -7-3*ip_0+2*iq_0-2*j_0+3*n_0 RF for loc. 125: -2+2*iq_0-2*j_0 RF for loc. 129: 2*iq_0-2*j_0 RF for loc. 133: 2+2*iq_0-2*j_0 Bound for (chained) transitions 197: 3 - Rank function 6: RF for loc. 45: 1-5*ip_0+5*n_0 RF for loc. 46: 1-5*ip_0+5*n_0 RF for loc. 47: -5*ip_0+5*n_0 RF for loc. 48: -3-5*ip_0+5*n_0 RF for loc. 49: -3-5*ip_0+5*n_0 RF for loc. 50: -2-5*ip_0+5*n_0 RF for loc. 51: -2-5*ip_0+5*n_0 RF for loc. 52: -1-5*ip_0+5*n_0 RF for loc. 57: 3-5*ip_0+5*n_0 RF for loc. 58: 2-5*ip_0+5*n_0 RF for loc. 59: 4-5*ip_0+5*n_0 RF for loc. 60: 5-5*ip_0+5*n_0 RF for loc. 61: 6-5*ip_0+5*n_0 RF for loc. 62: -4-5*ip_0+5*n_0 RF for loc. 63: 7-5*ip_0+5*n_0 RF for loc. 64: 8-5*ip_0+5*n_0 RF for loc. 65: 8-5*ip_0+5*n_0 RF for loc. 66: -4-5*ip_0+5*n_0 RF for loc. 67: 9-5*ip_0+5*n_0 RF for loc. 68: 10-5*ip_0+5*n_0 RF for loc. 69: 11-5*ip_0+5*n_0 RF for loc. 70: -5-5*ip_0+5*n_0 RF for loc. 71: -3-5*ip_0+5*n_0 RF for loc. 72: -4-5*ip_0+5*n_0 RF for loc. 73: -5-5*ip_0+5*n_0 RF for loc. 74: -10-5*ip_0+5*n_0 RF for loc. 77: -2-5*ip_0+5*n_0 RF for loc. 78: -1-5*ip_0+5*n_0 RF for loc. 79: 0 RF for loc. 80: 0 RF for loc. 81: 0 RF for loc. 82: -1 RF for loc. 83: -12-5*ip_0+5*n_0 RF for loc. 85: 1-5*ip_0+5*n_0 RF for loc. 93: -5-5*ip_0+5*n_0 RF for loc. 97: -4-5*ip_0+5*n_0 RF for loc. 105: 0 RF for loc. 109: 0 RF for loc. 113: -11-5*ip_0+5*n_0 RF for loc. 121: -6-5*ip_0+5*n_0 RF for loc. 125: -3-5*ip_0+5*n_0 RF for loc. 129: -2-5*ip_0+5*n_0 RF for loc. 133: -5*ip_0+5*n_0 Bound for (chained) transitions 142: 0 - Rank function 7: RF for loc. 45: 2-13*j_0+13*n_0 RF for loc. 46: 3-13*j_0+13*n_0 RF for loc. 47: 1-13*j_0+13*n_0 RF for loc. 48: -17-13*j_0+13*n_0 RF for loc. 49: -16-13*j_0+13*n_0 RF for loc. 50: -15-13*j_0+13*n_0 RF for loc. 51: -2-13*j_0+13*n_0 RF for loc. 52: -1-13*j_0+13*n_0 RF for loc. 57: 4-13*j_0+13*n_0 RF for loc. 58: 3-13*j_0+13*n_0 RF for loc. 59: 5-13*j_0+13*n_0 RF for loc. 60: 6-13*j_0+13*n_0 RF for loc. 61: 7-13*j_0+13*n_0 RF for loc. 62: -18-13*j_0+13*n_0 RF for loc. 63: 8-13*j_0+13*n_0 RF for loc. 64: 9-13*j_0+13*n_0 RF for loc. 65: 9-13*j_0+13*n_0 RF for loc. 66: -19-13*j_0+13*n_0 RF for loc. 67: 10-13*j_0+13*n_0 RF for loc. 68: 11-13*j_0+13*n_0 RF for loc. 69: 12-13*j_0+13*n_0 RF for loc. 70: -19-13*j_0+13*n_0 RF for loc. 71: -19-13*j_0+13*n_0 RF for loc. 72: -19-13*j_0+13*n_0 RF for loc. 73: -20-54*ip_0-13*j_0+67*n_0 RF for loc. 74: -73-54*ip_0-13*j_0+67*n_0 RF for loc. 77: -18-13*j_0+13*n_0 RF for loc. 78: -17-13*j_0+13*n_0 RF for loc. 79: 6+20*ip_0-13*j_0-7*n_0 RF for loc. 80: -16+20*ip_0-13*j_0-7*n_0 RF for loc. 81: 8+20*ip_0-13*j_0-7*n_0 RF for loc. 82: -16+20*ip_0-13*j_0-7*n_0 RF for loc. 83: -75-54*ip_0-13*j_0+67*n_0 RF for loc. 85: 3-13*j_0+13*n_0 RF for loc. 93: -19-13*j_0+13*n_0 RF for loc. 97: -19-13*j_0+13*n_0 RF for loc. 105: 7+20*ip_0-13*j_0-7*n_0 RF for loc. 109: -16+20*ip_0-13*j_0-7*n_0 RF for loc. 113: -74-54*ip_0-13*j_0+67*n_0 RF for loc. 121: -73-54*ip_0-13*j_0+67*n_0 RF for loc. 125: -16-13*j_0+13*n_0 RF for loc. 129: -14-13*j_0+13*n_0 RF for loc. 133: -13*j_0+13*n_0 Bound for (chained) transitions 177: -17 - Rank function 8: RF for loc. 45: 2-13*j_0+13*n_0 RF for loc. 46: 3-13*j_0+13*n_0 RF for loc. 47: 1-13*j_0+13*n_0 RF for loc. 48: -7-13*j_0+13*n_0 RF for loc. 49: -5-13*j_0+13*n_0 RF for loc. 50: -4-13*j_0+13*n_0 RF for loc. 51: -2-13*j_0+13*n_0 RF for loc. 52: -1-13*j_0+13*n_0 RF for loc. 57: 5-13*j_0+13*n_0 RF for loc. 58: 4-13*j_0+13*n_0 RF for loc. 59: 6-13*j_0+13*n_0 RF for loc. 60: 6-13*j_0+13*n_0 RF for loc. 61: 7-13*j_0+13*n_0 RF for loc. 62: -8-13*j_0+13*n_0 RF for loc. 63: 8-13*j_0+13*n_0 RF for loc. 64: 9-13*j_0+13*n_0 RF for loc. 65: 9-13*j_0+13*n_0 RF for loc. 66: -9-13*j_0+13*n_0 RF for loc. 67: 10-13*j_0+13*n_0 RF for loc. 68: 11-13*j_0+13*n_0 RF for loc. 69: 12-13*j_0+13*n_0 RF for loc. 70: -9-13*j_0+13*n_0 RF for loc. 71: -9-13*j_0+13*n_0 RF for loc. 72: -9-13*j_0+13*n_0 RF for loc. 73: -10-3*ip_0-13*j_0+16*n_0 RF for loc. 74: -12-3*ip_0-13*j_0+16*n_0 RF for loc. 77: -8-13*j_0+13*n_0 RF for loc. 78: -7-13*j_0+13*n_0 RF for loc. 79: 21+23*ip_0-13*j_0-10*n_0 RF for loc. 80: -4+23*ip_0-13*j_0-10*n_0 RF for loc. 81: 23+23*ip_0-13*j_0-10*n_0 RF for loc. 82: -6+23*ip_0-13*j_0-10*n_0 RF for loc. 83: 31-48*ip_0-13*j_0+61*n_0 RF for loc. 85: 3-13*j_0+13*n_0 RF for loc. 93: -9-13*j_0+13*n_0 RF for loc. 97: -9-13*j_0+13*n_0 RF for loc. 105: 22+23*ip_0-13*j_0-10*n_0 RF for loc. 109: -5+23*ip_0-13*j_0-10*n_0 RF for loc. 113: 32-48*ip_0-13*j_0+61*n_0 RF for loc. 121: -11-3*ip_0-13*j_0+16*n_0 RF for loc. 125: -6-13*j_0+13*n_0 RF for loc. 129: -3-13*j_0+13*n_0 RF for loc. 133: -13*j_0+13*n_0 Bound for (chained) transitions 187: -4 - Rank function 9: RF for loc. 45: 2-4*ip_0+4*n_0 RF for loc. 46: 2-4*ip_0+4*n_0 RF for loc. 47: 1-4*ip_0+4*n_0 RF for loc. 48: -7-4*ip_0+4*n_0 RF for loc. 49: -5-4*ip_0+4*n_0 RF for loc. 50: -4-4*ip_0+4*n_0 RF for loc. 51: -2-4*ip_0+4*n_0 RF for loc. 52: -1-4*ip_0+4*n_0 RF for loc. 57: 4-4*ip_0+4*n_0 RF for loc. 58: 3-4*ip_0+4*n_0 RF for loc. 59: 5-4*ip_0+4*n_0 RF for loc. 60: 5-4*ip_0+4*n_0 RF for loc. 61: 6-4*ip_0+4*n_0 RF for loc. 62: -8-4*ip_0+4*n_0 RF for loc. 63: 7-4*ip_0+4*n_0 RF for loc. 64: 8-4*ip_0+4*n_0 RF for loc. 65: 8-4*ip_0+4*n_0 RF for loc. 66: -9-4*ip_0+4*n_0 RF for loc. 67: 9-4*ip_0+4*n_0 RF for loc. 68: 10-4*ip_0+4*n_0 RF for loc. 69: 11-4*ip_0+4*n_0 RF for loc. 70: -11-4*ip_0+4*n_0 RF for loc. 71: -8-4*ip_0+4*n_0 RF for loc. 72: -8-4*ip_0+4*n_0 RF for loc. 73: -8-7*ip_0+7*n_0 RF for loc. 74: -10-7*ip_0+7*n_0 RF for loc. 77: -3-4*ip_0+4*n_0 RF for loc. 78: -2-4*ip_0+4*n_0 RF for loc. 79: 2 RF for loc. 80: 1 RF for loc. 81: 4 RF for loc. 82: -1 RF for loc. 83: -12-7*ip_0+7*n_0 RF for loc. 85: 2-4*ip_0+4*n_0 RF for loc. 93: -10-4*ip_0+4*n_0 RF for loc. 97: -8-4*ip_0+4*n_0 RF for loc. 105: 3 RF for loc. 109: 0 RF for loc. 113: -11-7*ip_0+7*n_0 RF for loc. 121: -9-7*ip_0+7*n_0 RF for loc. 125: -6-4*ip_0+4*n_0 RF for loc. 129: -3-4*ip_0+4*n_0 RF for loc. 133: -4*ip_0+4*n_0 Bound for (chained) transitions 105: -4 Bound for (chained) transitions 128: 2 Bound for (chained) transitions 130: 4 Bound for (chained) transitions 132: 3 Bound for (chained) transitions 133: 3 Bound for (chained) transitions 138: -1 Bound for (chained) transitions 140: 1 Bound for (chained) transitions 143: 0 Bound for (chained) transitions 168: -10 - Rank function 10: RF for loc. 45: 2+52*ip_0-52*j_0 RF for loc. 46: 3+52*ip_0-52*j_0 RF for loc. 47: 1+52*ip_0-52*j_0 RF for loc. 48: -7+52*ip_0-52*j_0 RF for loc. 49: -5+52*ip_0-52*j_0 RF for loc. 50: -4+52*ip_0-52*j_0 RF for loc. 51: -2+52*ip_0-52*j_0 RF for loc. 52: -1+52*ip_0-52*j_0 RF for loc. 57: 5+52*ip_0-52*j_0 RF for loc. 58: 4+52*ip_0-52*j_0 RF for loc. 59: 6+52*ip_0-52*j_0 RF for loc. 60: 7+52*ip_0-52*j_0 RF for loc. 61: 8+52*ip_0-52*j_0 RF for loc. 62: -8+52*ip_0-52*j_0 RF for loc. 63: 9+52*ip_0-52*j_0 RF for loc. 64: 10+52*ip_0-52*j_0 RF for loc. 65: 10+52*ip_0-52*j_0 RF for loc. 66: -9+52*ip_0-52*j_0 RF for loc. 67: 10+52*ip_0-52*j_0 RF for loc. 68: 11+52*ip_0-52*j_0 RF for loc. 69: 12+52*ip_0-52*j_0 RF for loc. 70: -11+52*ip_0-52*j_0 RF for loc. 71: -64+50*ip_0+2*ip_post-52*j_0 RF for loc. 72: -66+50*ip_0+2*ip_post-52*j_0 RF for loc. 73: -67+46*ip_0+2*ip_post-52*j_0+4*n_0 RF for loc. 74: -69+46*ip_0+2*ip_post-52*j_0+4*n_0 RF for loc. 77: 50*ip_0+2*ip_post-52*j_0 RF for loc. 78: 1+50*ip_0+2*ip_post-52*j_0 RF for loc. 83: -71+46*ip_0+2*ip_post-52*j_0+4*n_0 RF for loc. 85: 3+52*ip_0-52*j_0 RF for loc. 93: -10+52*ip_0-52*j_0 RF for loc. 97: -65+50*ip_0+2*ip_post-52*j_0 RF for loc. 113: -70+46*ip_0+2*ip_post-52*j_0+4*n_0 RF for loc. 121: -68+46*ip_0+2*ip_post-52*j_0+4*n_0 RF for loc. 125: -6+52*ip_0-52*j_0 RF for loc. 129: -3+52*ip_0-52*j_0 RF for loc. 133: 52*ip_0-52*j_0 Bound for (chained) transitions 53: 54 - Rank function 11: RF for loc. 45: 2 RF for loc. 46: 4 RF for loc. 47: 1 RF for loc. 48: -7 RF for loc. 49: -5 RF for loc. 50: -4 RF for loc. 51: -2 RF for loc. 52: -1 RF for loc. 57: 6 RF for loc. 58: 5 RF for loc. 59: 7 RF for loc. 60: 8 RF for loc. 61: 9 RF for loc. 62: -8 RF for loc. 63: 10 RF for loc. 64: 11 RF for loc. 65: 11 RF for loc. 66: -9 RF for loc. 67: 12 RF for loc. 68: 13 RF for loc. 69: 14 RF for loc. 70: -11 RF for loc. 71: -12 RF for loc. 72: -14 RF for loc. 73: -15 RF for loc. 74: -17 RF for loc. 77: 0 RF for loc. 78: 1 RF for loc. 83: -19 RF for loc. 85: 3 RF for loc. 93: -10 RF for loc. 97: -13 RF for loc. 113: -18 RF for loc. 121: -16 RF for loc. 125: -6 RF for loc. 129: -3 RF for loc. 133: 0 Bound for (chained) transitions 54: 2 Bound for (chained) transitions 55: 4 Bound for (chained) transitions 57: 3 Bound for (chained) transitions 58: 3 Bound for (chained) transitions 63: 6 Bound for (chained) transitions 64: 6 Bound for (chained) transitions 67: 7 Bound for (chained) transitions 68: 5 Bound for (chained) transitions 69: 8 Bound for (chained) transitions 70: 8 Bound for (chained) transitions 71: 8 Bound for (chained) transitions 72: 9 Bound for (chained) transitions 73: 9 Bound for (chained) transitions 74: 10 Bound for (chained) transitions 75: 11 Bound for (chained) transitions 76: 11 Bound for (chained) transitions 77: -8 Bound for (chained) transitions 78: 12 Bound for (chained) transitions 79: 12 Bound for (chained) transitions 80: 12 Bound for (chained) transitions 81: 13 Bound for (chained) transitions 82: 13 Bound for (chained) transitions 83: 13 Bound for (chained) transitions 92: 14 Bound for (chained) transitions 93: 14 Bound for (chained) transitions 94: -11 Bound for (chained) transitions 96: -9 Bound for (chained) transitions 98: -10 Bound for (chained) transitions 99: -10 Bound for (chained) transitions 104: -14 Bound for (chained) transitions 108: -12 Bound for (chained) transitions 110: -13 Bound for (chained) transitions 111: -13 Bound for (chained) transitions 116: 0 Bound for (chained) transitions 117: 0 Bound for (chained) transitions 118: 1 Bound for (chained) transitions 119: 1 Bound for (chained) transitions 149, 167: -17 Bound for (chained) transitions 151: -18 Bound for (chained) transitions 152: -18 Bound for (chained) transitions 169: -15 Bound for (chained) transitions 171: -16 Bound for (chained) transitions 172: -16 Bound for (chained) transitions 178: -7 Bound for (chained) transitions 179: -5 Bound for (chained) transitions 181: -6 Bound for (chained) transitions 182: -6 Bound for (chained) transitions 188: -4 Bound for (chained) transitions 189: -2 Bound for (chained) transitions 191: -3 Bound for (chained) transitions 192: -3 Bound for (chained) transitions 198: -1 Bound for (chained) transitions 199: 1 Bound for (chained) transitions 201: 0 Bound for (chained) transitions 202: 0 * 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: -1 RF for loc. 117: 0 Bound for (chained) transitions 161: 0 Bound for (chained) transitions 162: 0 * 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: