YES Termination proof succeeded Initially, performed program simplifications using lexicographic rank functions: * Removed transitions 53, 54, 55, 57, 58, 63, 64, 65, 66, 67, 69, 70, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 86, 87, 92, 93, 94, 95, 96, 97, 98, 99, 100, 102, 103, 108, 109, 110, 111, 112, 113, 114, 116, 117, 122, 123, 124, 125, 126, 128, 129, 134, 135, 136, 137, 139, 140, 147, 149, 150, 167, 168, 177, 178, 187, 188, 189, 191, 192, 197, 198, 199, 201, 202 using the following rank functions: - Rank function 1: RF for loc. 45: 4*___const_50_0-4*i_0 RF for loc. 46: 4*___const_50_0-4*i_0 RF for loc. 47: 4*___const_50_0-4*i_0 RF for loc. 48: 4*___const_50_0-4*i_0 RF for loc. 49: 4*___const_50_0-4*i_0 RF for loc. 50: 4*___const_50_0-4*i_0 RF for loc. 51: 4*___const_50_0-4*i_0 RF for loc. 52: 4*___const_50_0-4*i_0 RF for loc. 53: 4*___const_50_0+1-4*i_0 RF for loc. 54: 4*___const_50_0+1-4*i_0 RF for loc. 55: 4*___const_50_0-4*i_0 RF for loc. 56: 4*___const_50_0-4*i_0 RF for loc. 57: 4*___const_50_0-4*i_0 RF for loc. 58: 4*___const_50_0-4*i_0 RF for loc. 59: 4*___const_50_0-4*i_0 RF for loc. 60: 4*___const_50_0-4*i_0 RF for loc. 61: 4*___const_50_0-4*i_0 RF for loc. 62: 4*___const_50_0-4*i_0 RF for loc. 63: 4*___const_50_0-4*i_0 RF for loc. 64: 4*___const_50_0-4*i_0 RF for loc. 65: 4*___const_50_0-4*i_0 RF for loc. 66: 4*___const_50_0-4*i_0 RF for loc. 67: 4*___const_50_0-4*i_0 RF for loc. 68: 4*___const_50_0-4*i_0 RF for loc. 69: 4*___const_50_0-4*i_0 RF for loc. 70: 4*___const_50_0-4*i_0 RF for loc. 71: 4*___const_50_0+-1-4*i_0 RF for loc. 72: 4*___const_50_0+-1-4*i_0 RF for loc. 73: 4*___const_50_0-4*i_0 RF for loc. 74: 4*___const_50_0+1-4*i_0 RF for loc. 75: 4*___const_50_0+1-4*i_0 RF for loc. 76: 4*___const_50_0+1-4*i_0 RF for loc. 79: 4*___const_50_0+2-4*i_0 RF for loc. 85: 4*___const_50_0+1-4*i_0 RF for loc. 89: 4*___const_50_0-4*i_0 RF for loc. 93: 4*___const_50_0-4*i_0 RF for loc. 97: 4*___const_50_0-4*i_0 RF for loc. 101: 4*___const_50_0-4*i_0 RF for loc. 105: 4*___const_50_0-4*i_0 RF for loc. 109: 4*___const_50_0-4*i_0 RF for loc. 113: 4*___const_50_0+-1-4*i_0 RF for loc. 129: 4*___const_50_0+3-4*i_0 RF for loc. 133: 4*___const_50_0+1-4*i_0 Bound for (chained) transitions 136: 2 - Rank function 2: RF for loc. 45: 2-39*ip_0-11*iq_0+50*n_0 RF for loc. 46: 2-39*ip_0-11*iq_0+50*n_0 RF for loc. 47: 1-39*ip_0-11*iq_0+50*n_0 RF for loc. 48: 1-39*ip_0-11*iq_0+50*n_0 RF for loc. 49: -39*ip_0-11*iq_0+50*n_0 RF for loc. 50: -39*ip_0-11*iq_0+50*n_0 RF for loc. 51: -1-39*ip_0-11*iq_0+50*n_0 RF for loc. 52: -1-39*ip_0-11*iq_0+50*n_0 RF for loc. 53: 30-11*iq_0+11*n_0 RF for loc. 54: 30-11*iq_0+11*n_0 RF for loc. 55: 3-39*ip_0-11*iq_0+50*n_0 RF for loc. 56: 2-39*ip_0-11*iq_0+50*n_0 RF for loc. 57: 4-39*ip_0-11*iq_0+50*n_0 RF for loc. 58: 27-39*ip_0-11*iq_0+50*n_0 RF for loc. 59: 25-39*ip_0-11*iq_0+50*n_0 RF for loc. 60: 5-39*ip_0-11*iq_0+50*n_0 RF for loc. 61: 5-39*ip_0-11*iq_0+50*n_0 RF for loc. 62: -2-39*ip_0-11*iq_0+50*n_0 RF for loc. 63: 6-39*ip_0-11*iq_0+50*n_0 RF for loc. 64: 6-39*ip_0-11*iq_0+50*n_0 RF for loc. 65: 6-39*ip_0-11*iq_0+50*n_0 RF for loc. 66: 8-39*ip_0-11*iq_0+50*n_0 RF for loc. 67: 7-39*ip_0-11*iq_0+50*n_0 RF for loc. 68: 6-39*ip_0-11*iq_0+50*n_0 RF for loc. 69: 6-39*ip_0-11*iq_0+50*n_0 RF for loc. 70: 6-39*ip_0-11*iq_0+50*n_0 RF for loc. 71: 24-39*ip_0-11*iq_0+50*n_0 RF for loc. 72: 23-39*ip_0-11*iq_0+50*n_0 RF for loc. 73: 28-39*ip_0-11*iq_0+50*n_0 RF for loc. 74: 29-39*ip_0-11*iq_0+50*n_0 RF for loc. 75: 30-11*iq_0+11*n_0 RF for loc. 76: 30-11*iq_0+11*n_0 RF for loc. 79: 21-39*ip_0-11*iq_0+50*n_0 RF for loc. 85: 30-11*iq_0+11*n_0 RF for loc. 89: 26-39*ip_0-11*iq_0+50*n_0 RF for loc. 93: 7-39*ip_0-11*iq_0+50*n_0 RF for loc. 97: 2-39*ip_0-11*iq_0+50*n_0 RF for loc. 101: 1-39*ip_0-11*iq_0+50*n_0 RF for loc. 105: -39*ip_0-11*iq_0+50*n_0 RF for loc. 109: -1-39*ip_0-11*iq_0+50*n_0 RF for loc. 113: 23-39*ip_0-11*iq_0+50*n_0 RF for loc. 129: 22-39*ip_0-11*iq_0+50*n_0 RF for loc. 133: 30-11*iq_0+11*n_0 Bound for (chained) transitions 125: 30 - Rank function 3: RF for loc. 45: -52*ip_0+52*n_0 RF for loc. 46: -52*ip_0+52*n_0 RF for loc. 47: -52*ip_0+52*n_0 RF for loc. 48: -52*ip_0+52*n_0 RF for loc. 49: -52*ip_0+52*n_0 RF for loc. 50: -52*ip_0+52*n_0 RF for loc. 51: -52*ip_0+52*n_0 RF for loc. 52: -52*ip_0+52*n_0 RF for loc. 53: 10-39*ip_0+39*n_0 RF for loc. 54: 9-39*ip_0+39*n_0 RF for loc. 55: -52*ip_0+52*n_0 RF for loc. 56: -52*ip_0+52*n_0 RF for loc. 57: -52*ip_0+52*n_0 RF for loc. 58: 27-52*ip_0+52*n_0 RF for loc. 59: 1-52*ip_0+52*n_0 RF for loc. 60: -52*ip_0+52*n_0 RF for loc. 61: -52*ip_0+52*n_0 RF for loc. 62: -52*ip_0+52*n_0 RF for loc. 63: -52*ip_0+52*n_0 RF for loc. 64: -52*ip_0+52*n_0 RF for loc. 65: -52*ip_0+52*n_0 RF for loc. 66: -52*ip_0+52*n_0 RF for loc. 67: -52*ip_0+52*n_0 RF for loc. 68: -52*ip_0+52*n_0 RF for loc. 69: -52*ip_0+52*n_0 RF for loc. 70: -52*ip_0+52*n_0 RF for loc. 71: -52*ip_0+52*n_0 RF for loc. 72: -2-52*ip_0+52*n_0 RF for loc. 73: 28-52*ip_0+52*n_0 RF for loc. 74: 29-52*ip_0+52*n_0 RF for loc. 75: 32-39*ip_0+39*n_0 RF for loc. 76: 30-39*ip_0+39*n_0 RF for loc. 79: -4-52*ip_0+52*n_0 RF for loc. 85: 9-39*ip_0+39*n_0 RF for loc. 89: 26-52*ip_0+52*n_0 RF for loc. 93: -52*ip_0+52*n_0 RF for loc. 97: -52*ip_0+52*n_0 RF for loc. 101: -52*ip_0+52*n_0 RF for loc. 105: -52*ip_0+52*n_0 RF for loc. 109: -52*ip_0+52*n_0 RF for loc. 113: -1-52*ip_0+52*n_0 RF for loc. 129: -3-52*ip_0+52*n_0 RF for loc. 133: 31-39*ip_0+39*n_0 Bound for (chained) transitions 111: 53 Bound for (chained) transitions 135: 69 Bound for (chained) transitions 168: -2 - Rank function 4: RF for loc. 45: 1-34*iq_0+34*n_0 RF for loc. 46: 1-34*iq_0+34*n_0 RF for loc. 47: -34*iq_0+34*n_0 RF for loc. 48: -34*iq_0+34*n_0 RF for loc. 49: -1-34*iq_0+34*n_0 RF for loc. 50: -1-34*iq_0+34*n_0 RF for loc. 51: -10-34*iq_0+34*n_0 RF for loc. 52: -10-34*iq_0+34*n_0 RF for loc. 53: -32 RF for loc. 54: -33 RF for loc. 55: 3-34*iq_0+34*n_0 RF for loc. 56: 2-34*iq_0+34*n_0 RF for loc. 57: 3-34*iq_0+34*n_0 RF for loc. 58: -4-34*iq_0+34*n_0 RF for loc. 59: -6-34*iq_0+34*n_0 RF for loc. 60: 3-34*iq_0+34*n_0 RF for loc. 61: 4-34*iq_0+34*n_0 RF for loc. 62: -20-34*iq_0+34*n_0 RF for loc. 63: 5-34*iq_0+34*n_0 RF for loc. 64: 6-34*iq_0+34*n_0 RF for loc. 65: 6-34*iq_0+34*n_0 RF for loc. 66: 11-34*iq_0+34*n_0 RF for loc. 67: 9-34*iq_0+34*n_0 RF for loc. 68: 7-34*iq_0+34*n_0 RF for loc. 69: 8-34*iq_0+34*n_0 RF for loc. 70: 9-34*iq_0+34*n_0 RF for loc. 71: -7-34*iq_0+34*n_0 RF for loc. 72: -9-34*iq_0+34*n_0 RF for loc. 73: -3-34*iq_0+34*n_0 RF for loc. 74: -2-34*iq_0+34*n_0 RF for loc. 75: 1-34*iq_0+34*n_0 RF for loc. 76: -1-34*iq_0+34*n_0 RF for loc. 79: -10-34*iq_0+34*n_0 RF for loc. 85: -32 RF for loc. 89: -5-34*iq_0+34*n_0 RF for loc. 93: 10-34*iq_0+34*n_0 RF for loc. 97: 1-34*iq_0+34*n_0 RF for loc. 101: -34*iq_0+34*n_0 RF for loc. 105: -1-34*iq_0+34*n_0 RF for loc. 109: -10-34*iq_0+34*n_0 RF for loc. 113: -8-34*iq_0+34*n_0 RF for loc. 129: -10-34*iq_0+34*n_0 RF for loc. 133: -34*iq_0+34*n_0 Bound for (chained) transitions 57: -32 - Rank function 5: RF for loc. 45: 1-59*iq_0+59*n_0 RF for loc. 46: 1-59*iq_0+59*n_0 RF for loc. 47: -59*iq_0+59*n_0 RF for loc. 48: -59*iq_0+59*n_0 RF for loc. 49: -1-59*iq_0+59*n_0 RF for loc. 50: -1-59*iq_0+59*n_0 RF for loc. 51: -44-59*iq_0+59*n_0 RF for loc. 52: -44-59*iq_0+59*n_0 RF for loc. 53: -41 RF for loc. 54: -41 RF for loc. 55: 3-59*iq_0+59*n_0 RF for loc. 56: 2-59*iq_0+59*n_0 RF for loc. 57: 4-59*iq_0+59*n_0 RF for loc. 58: 9-59*iq_0+59*n_0 RF for loc. 59: 8-59*iq_0+59*n_0 RF for loc. 60: 5-59*iq_0+59*n_0 RF for loc. 61: 6-59*iq_0+59*n_0 RF for loc. 62: -45-59*iq_0+59*n_0 RF for loc. 63: 7-59*iq_0+59*n_0 RF for loc. 64: 8-59*iq_0+59*n_0 RF for loc. 65: 8-59*iq_0+59*n_0 RF for loc. 66: 13-59*iq_0+59*n_0 RF for loc. 67: 11-59*iq_0+59*n_0 RF for loc. 68: 9-59*iq_0+59*n_0 RF for loc. 69: 10-59*iq_0+59*n_0 RF for loc. 70: 11-59*iq_0+59*n_0 RF for loc. 71: 7-59*iq_0+59*n_0 RF for loc. 72: 6-59*iq_0+59*n_0 RF for loc. 73: 10-59*iq_0+59*n_0 RF for loc. 74: 11-59*iq_0+59*n_0 RF for loc. 75: 17-59*iq_0+59*n_0 RF for loc. 76: 12-59*iq_0+59*n_0 RF for loc. 79: 5-59*iq_0+59*n_0 RF for loc. 85: -41 RF for loc. 89: 9-59*iq_0+59*n_0 RF for loc. 93: 12-59*iq_0+59*n_0 RF for loc. 97: 1-59*iq_0+59*n_0 RF for loc. 101: -59*iq_0+59*n_0 RF for loc. 105: -1-59*iq_0+59*n_0 RF for loc. 109: -44-59*iq_0+59*n_0 RF for loc. 113: 6-59*iq_0+59*n_0 RF for loc. 129: 5-59*iq_0+59*n_0 RF for loc. 133: 16-59*iq_0+59*n_0 Bound for (chained) transitions 124: -41 - Rank function 6: RF for loc. 45: 3+ip_0-48*iq_0-3*j_0 RF for loc. 46: 5+ip_0-48*iq_0-3*j_0 RF for loc. 47: 2+ip_0-48*iq_0-3*j_0 RF for loc. 48: ip_0-48*iq_0-3*j_0 RF for loc. 49: -1+ip_0-48*iq_0-3*j_0 RF for loc. 50: -3+ip_0-48*iq_0-3*j_0 RF for loc. 51: -17+ip_0-48*iq_0-3*j_0 RF for loc. 52: -20+ip_0-48*iq_0-3*j_0 RF for loc. 53: 1 RF for loc. 54: -1 RF for loc. 55: 6+ip_0-48*iq_0-3*j_0 RF for loc. 56: 6+ip_0-48*iq_0-3*j_0 RF for loc. 57: 7+ip_0-48*iq_0-3*j_0 RF for loc. 58: -4+ip_post-48*iq_0-3*j_0 RF for loc. 59: -6+ip_post-48*iq_0-3*j_0 RF for loc. 60: 8+ip_0-48*iq_0-3*j_0 RF for loc. 61: 8+ip_0-48*iq_0-3*j_0 RF for loc. 62: -22+ip_0-48*iq_0-3*j_0 RF for loc. 63: 9+ip_0-48*iq_0-3*j_0 RF for loc. 64: 10+ip_0-48*iq_0-3*j_0 RF for loc. 65: 9+ip_0-48*iq_0-3*j_0 RF for loc. 66: 25+ip_0-48*iq_0-3*j_0 RF for loc. 67: 23+ip_0-48*iq_0-3*j_0 RF for loc. 68: 21+ip_0-48*iq_0-3*j_0 RF for loc. 69: 21+ip_0-48*iq_0-3*j_0 RF for loc. 70: 22+ip_0-48*iq_0-3*j_0 RF for loc. 71: -7+ip_post-48*iq_0-3*j_0 RF for loc. 72: -9+ip_post-48*iq_0-3*j_0 RF for loc. 73: -3+ip_post-48*iq_0-3*j_0 RF for loc. 74: -2+ip_post-48*iq_0-3*j_0 RF for loc. 75: 1+ip_post-48*iq_0-3*j_0 RF for loc. 76: -1+ip_post-48*iq_0-3*j_0 RF for loc. 79: -11+ip_post-48*iq_0-3*j_0 RF for loc. 85: 0 RF for loc. 89: -5+ip_post-48*iq_0-3*j_0 RF for loc. 93: 24+ip_0-48*iq_0-3*j_0 RF for loc. 97: 4+ip_0-48*iq_0-3*j_0 RF for loc. 101: 1+ip_0-48*iq_0-3*j_0 RF for loc. 105: -2+ip_0-48*iq_0-3*j_0 RF for loc. 109: -19+ip_0-48*iq_0-3*j_0 RF for loc. 113: -8+ip_post-48*iq_0-3*j_0 RF for loc. 129: -10+ip_post-48*iq_0-3*j_0 RF for loc. 133: ip_post-48*iq_0-3*j_0 Bound for (chained) transitions 55: 1 - Rank function 7: RF for loc. 45: 3-50*iq_0-3*j_0 RF for loc. 46: 5-50*iq_0-3*j_0 RF for loc. 47: 2-50*iq_0-3*j_0 RF for loc. 48: -50*iq_0-3*j_0 RF for loc. 49: -1-50*iq_0-3*j_0 RF for loc. 50: -3-50*iq_0-3*j_0 RF for loc. 51: -13-50*iq_0-3*j_0 RF for loc. 52: -15-50*iq_0-3*j_0 RF for loc. 54: -1 RF for loc. 55: 7-50*iq_0-3*j_0 RF for loc. 56: 6-50*iq_0-3*j_0 RF for loc. 57: 8-50*iq_0-3*j_0 RF for loc. 58: -4-50*iq_0-3*j_0 RF for loc. 59: -6-50*iq_0-3*j_0 RF for loc. 60: 9-50*iq_0-3*j_0 RF for loc. 61: 10-50*iq_0-3*j_0 RF for loc. 62: -17-50*iq_0-3*j_0 RF for loc. 63: 11-50*iq_0-3*j_0 RF for loc. 64: 12-50*iq_0-3*j_0 RF for loc. 65: 12-50*iq_0-3*j_0 RF for loc. 66: 32-50*iq_0-3*j_0 RF for loc. 67: 31-50*iq_0-3*j_0 RF for loc. 68: 28-50*iq_0-3*j_0 RF for loc. 69: 29-50*iq_0-3*j_0 RF for loc. 70: 30-50*iq_0-3*j_0 RF for loc. 71: -7-50*iq_0-3*j_0 RF for loc. 72: -9-50*iq_0-3*j_0 RF for loc. 73: -3-50*iq_0-3*j_0 RF for loc. 74: -2-50*iq_0-3*j_0 RF for loc. 75: 1-50*iq_0-3*j_0 RF for loc. 76: -1-50*iq_0-3*j_0 RF for loc. 79: -10-50*iq_0-3*j_0 RF for loc. 85: 0 RF for loc. 89: -5-50*iq_0-3*j_0 RF for loc. 93: 31-50*iq_0-3*j_0 RF for loc. 97: 4-50*iq_0-3*j_0 RF for loc. 101: 1-50*iq_0-3*j_0 RF for loc. 105: -2-50*iq_0-3*j_0 RF for loc. 109: -14-50*iq_0-3*j_0 RF for loc. 113: -8-50*iq_0-3*j_0 RF for loc. 129: -10-50*iq_0-3*j_0 RF for loc. 133: -50*iq_0-3*j_0 Bound for (chained) transitions 58: 0 - Rank function 8: RF for loc. 45: 1-50*iq_0+50*n_0 RF for loc. 46: 1-50*iq_0+50*n_0 RF for loc. 47: -50*iq_0+50*n_0 RF for loc. 48: -50*iq_0+50*n_0 RF for loc. 49: -1-50*iq_0+50*n_0 RF for loc. 50: -1-50*iq_0+50*n_0 RF for loc. 51: -15-50*iq_0+50*n_0 RF for loc. 52: -15-50*iq_0+50*n_0 RF for loc. 55: 3-50*iq_0+50*n_0 RF for loc. 56: 2-50*iq_0+50*n_0 RF for loc. 57: 4-50*iq_0+50*n_0 RF for loc. 58: -4-50*iq_0+50*n_0 RF for loc. 59: -6-50*iq_0+50*n_0 RF for loc. 60: 5-50*iq_0+50*n_0 RF for loc. 61: 6-50*iq_0+50*n_0 RF for loc. 62: -16-50*iq_0+50*n_0 RF for loc. 63: 6-50*iq_0+50*n_0 RF for loc. 64: 7-50*iq_0+50*n_0 RF for loc. 65: 29-50*iq_0+50*n_0 RF for loc. 66: 33-50*iq_0+50*n_0 RF for loc. 67: 32-50*iq_0+50*n_0 RF for loc. 68: 29-50*iq_0+50*n_0 RF for loc. 69: 30-50*iq_0+50*n_0 RF for loc. 70: 31-50*iq_0+50*n_0 RF for loc. 71: -7-50*iq_0+50*n_0 RF for loc. 72: -9-50*iq_0+50*n_0 RF for loc. 73: -3-50*iq_0+50*n_0 RF for loc. 74: -2-50*iq_0+50*n_0 RF for loc. 75: 1-50*iq_0+50*n_0 RF for loc. 76: -1-50*iq_0+50*n_0 RF for loc. 79: -11-50*iq_0+50*n_0 RF for loc. 89: -5-50*iq_0+50*n_0 RF for loc. 93: 33-50*iq_0+50*n_0 RF for loc. 97: 1-50*iq_0+50*n_0 RF for loc. 101: -50*iq_0+50*n_0 RF for loc. 105: -1-50*iq_0+50*n_0 RF for loc. 109: -15-50*iq_0+50*n_0 RF for loc. 113: -8-50*iq_0+50*n_0 RF for loc. 129: -10-50*iq_0+50*n_0 RF for loc. 133: -50*iq_0+50*n_0 Bound for (chained) transitions 109: 32 - Rank function 9: RF for loc. 45: 1 RF for loc. 46: 1 RF for loc. 47: 0 RF for loc. 48: 0 RF for loc. 49: -1 RF for loc. 50: -1 RF for loc. 51: -2 RF for loc. 52: -2 RF for loc. 55: 3 RF for loc. 56: 2 RF for loc. 57: 4 RF for loc. 58: -7 RF for loc. 59: -9 RF for loc. 60: 5 RF for loc. 61: 6 RF for loc. 62: -3 RF for loc. 63: 7 RF for loc. 64: 8 RF for loc. 65: 8 RF for loc. 66: -4 RF for loc. 67: -6 RF for loc. 68: 9 RF for loc. 69: 10 RF for loc. 70: 11 RF for loc. 71: -10 RF for loc. 72: -12 RF for loc. 73: -6 RF for loc. 74: -5 RF for loc. 75: -2 RF for loc. 76: -4 RF for loc. 79: -14 RF for loc. 89: -8 RF for loc. 93: -5 RF for loc. 97: 1 RF for loc. 101: 0 RF for loc. 105: -1 RF for loc. 109: -2 RF for loc. 113: -11 RF for loc. 129: -13 RF for loc. 133: -3 Bound for (chained) transitions 54: 1 Bound for (chained) transitions 63: 3 Bound for (chained) transitions 64: 3 Bound for (chained) transitions 65: 4 Bound for (chained) transitions 66: 2 Bound for (chained) transitions 67: -7 Bound for (chained) transitions 69: -8 Bound for (chained) transitions 70: -8 Bound for (chained) transitions 75: 5 Bound for (chained) transitions 76: 5 Bound for (chained) transitions 77: 5 Bound for (chained) transitions 78: 6 Bound for (chained) transitions 79: 6 Bound for (chained) transitions 80: 7 Bound for (chained) transitions 81: 8 Bound for (chained) transitions 82: 8 Bound for (chained) transitions 83: -3 Bound for (chained) transitions 84: -4 Bound for (chained) transitions 86: -5 Bound for (chained) transitions 87: -5 Bound for (chained) transitions 92: 9 Bound for (chained) transitions 93: 9 Bound for (chained) transitions 94: 9 Bound for (chained) transitions 95: 10 Bound for (chained) transitions 96: 10 Bound for (chained) transitions 97: 10 Bound for (chained) transitions 98: 11 Bound for (chained) transitions 99: 11 Bound for (chained) transitions 108: -6 Bound for (chained) transitions 110: -9 Bound for (chained) transitions 112: -6 Bound for (chained) transitions 113: -6 Bound for (chained) transitions 122: -5 Bound for (chained) transitions 123: -5 Bound for (chained) transitions 134: -4 Bound for (chained) transitions 147: -10 Bound for (chained) transitions 149: -11 Bound for (chained) transitions 150: -11 Bound for (chained) transitions 167, 189: -12 Bound for (chained) transitions 178: -2 Bound for (chained) transitions 188: -1 Bound for (chained) transitions 191: -13 Bound for (chained) transitions 192: -13 Bound for (chained) transitions 198: 0 Bound for (chained) transitions 199: -2 Bound for (chained) transitions 201: -3 Bound for (chained) transitions 202: -3 - Rank function 10: RF for loc. 45: -1-3*j_0 RF for loc. 46: 1-3*j_0 RF for loc. 47: 0 RF for loc. 48: 0 RF for loc. 49: -j_0+n_0 RF for loc. 50: -j_0+n_0 RF for loc. 51: 2-3*j_0+3*n_0 RF for loc. 52: -3*j_0+3*n_0 RF for loc. 97: -3*j_0 RF for loc. 101: 0 RF for loc. 105: -j_0+n_0 RF for loc. 109: 1-3*j_0+3*n_0 Bound for (chained) transitions 177: 0 Bound for (chained) transitions 187: 0 - Rank function 11: RF for loc. 45: -1-3*j_0 RF for loc. 46: 1-3*j_0 RF for loc. 47: 2+3*iq_0-3*j_0 RF for loc. 48: 3*iq_0-3*j_0 RF for loc. 49: 1 RF for loc. 50: -1 RF for loc. 51: 1 RF for loc. 52: -1 RF for loc. 97: -3*j_0 RF for loc. 101: 1+3*iq_0-3*j_0 RF for loc. 105: 0 RF for loc. 109: 0 Bound for (chained) transitions 126: 1 Bound for (chained) transitions 128: 0 Bound for (chained) transitions 129: 0 Bound for (chained) transitions 137: 1 Bound for (chained) transitions 139: 0 Bound for (chained) transitions 140: 0 Bound for (chained) transitions 197: 3 - Rank function 12: RF for loc. 45: -1+3*ip_0-3*j_0 RF for loc. 46: 1+3*ip_0-3*j_0 RF for loc. 47: 1 RF for loc. 48: -1 RF for loc. 97: 3*ip_0-3*j_0 RF for loc. 101: 0 Bound for (chained) transitions 53: 2 Bound for (chained) transitions 114: 1 Bound for (chained) transitions 116: 0 Bound for (chained) transitions 117: 0 - Rank function 13: RF for loc. 45: -1 RF for loc. 46: 1 RF for loc. 97: 0 Bound for (chained) transitions 100: 1 Bound for (chained) transitions 103: 0 - Rank function 14: RF for loc. 45: -1 RF for loc. 97: 0 Bound for (chained) transitions 102: 0 * Removed transitions 145, 179, 181, 182 using the following rank functions: - Rank function 1: RF for loc. 77: -1-2*ip_0+2*n_0 RF for loc. 125: -2*ip_0+2*n_0 Bound for (chained) transitions 145, 179: -1 - Rank function 2: RF for loc. 77: 0 RF for loc. 125: 1 Bound for (chained) transitions 181: 1 Bound for (chained) transitions 182: 1 * Removed transitions 155, 156, 158, 159, 161, 162, 169, 171, 172 using the following rank functions: - Rank function 1: RF for loc. 81: -iq_0+n_0 RF for loc. 83: -iq_0+n_0 RF for loc. 84: -iq_0+n_0 RF for loc. 117: -iq_0+n_0 RF for loc. 121: -iq_0+n_0 Bound for (chained) transitions 156: 0 - Rank function 2: RF for loc. 81: -1-6*ip_0+6*n_0 RF for loc. 83: 1-6*ip_0+6*n_0 RF for loc. 84: 2-6*ip_0+6*n_0 RF for loc. 117: 3-6*ip_0+6*n_0 RF for loc. 121: -6*ip_0+6*n_0 Bound for (chained) transitions 158: 2 - Rank function 3: RF for loc. 81: -1 RF for loc. 83: 1 RF for loc. 84: -3 RF for loc. 117: -2 RF for loc. 121: 0 Bound for (chained) transitions 155, 159: -1 Bound for (chained) transitions 161: -2 Bound for (chained) transitions 162: -2 Bound for (chained) transitions 169: 1 Bound for (chained) transitions 171: 0 Bound for (chained) transitions 172: 0 Errors: