YES Termination proof succeeded Initially, performed program simplifications using lexicographic rank functions: * Removed transitions 203, 204, 206, 207 using the following rank functions: - Rank function 1: RF for loc. 90: -1-2*j_0+2*m_0 RF for loc. 144: -2*j_0+2*m_0 Bound for (chained) transitions 203, 204: -1 - Rank function 2: RF for loc. 90: 0 RF for loc. 144: 1 Bound for (chained) transitions 207: 1 - Rank function 3: RF for loc. 90: 0 RF for loc. 144: 1 Bound for (chained) transitions 206: 1 * Removed transitions 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 79, 80, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94, 95, 96, 97, 99, 100, 105, 106, 107, 109, 110, 115, 116, 117, 118, 120, 121, 126, 127, 128, 130, 131, 136, 137, 138, 140, 141, 146, 147, 148, 149, 150, 151, 153, 154, 160, 161, 163, 164, 212, 213, 214, 215, 216, 217, 218, 219, 220, 221, 222, 223 using the following rank functions: - Rank function 1: RF for loc. 53: 3-45*j_0+45*m4_0 RF for loc. 54: 1-45*j_0+45*m4_0 RF for loc. 55: 2-45*j_0+45*m4_0 RF for loc. 56: 4-45*j_0+45*m4_0 RF for loc. 57: 3-45*j_0+45*m4_0 RF for loc. 58: 41-45*j_0+45*m4_0 RF for loc. 59: 41-45*j_0+45*m4_0 RF for loc. 61: 41-45*j_0+45*m4_0 RF for loc. 62: 41-45*j_0+45*m4_0 RF for loc. 63: 41-45*j_0+45*m4_0 RF for loc. 64: 41-45*j_0+45*m4_0 RF for loc. 65: 41-45*j_0+45*m4_0 RF for loc. 66: 41-45*j_0+45*m4_0 RF for loc. 67: 41-45*j_0+45*m4_0 RF for loc. 68: 41-45*j_0+45*m4_0 RF for loc. 69: 41-45*j_0+45*m4_0 RF for loc. 70: 41-45*j_0+45*m4_0 RF for loc. 71: 41-45*j_0+45*m4_0 RF for loc. 72: 41-45*j_0+45*m4_0 RF for loc. 73: 41-45*j_0+45*m4_0 RF for loc. 74: 41-45*j_0+45*m4_0 RF for loc. 75: 41-45*j_0+45*m4_0 RF for loc. 76: 41-45*j_0+45*m4_0 RF for loc. 77: 41-45*j_0+45*m4_0 RF for loc. 78: 41-45*j_0+45*m4_0 RF for loc. 79: 41-45*j_0+45*m4_0 RF for loc. 80: 41-45*j_0+45*m4_0 RF for loc. 81: 41-45*j_0+45*m4_0 RF for loc. 82: 41-45*j_0+45*m4_0 RF for loc. 83: -4-45*j_0+45*m4_0 RF for loc. 84: -4-45*j_0+45*m4_0 RF for loc. 85: -3-45*j_0+45*m4_0 RF for loc. 86: -1-45*j_0+45*m4_0 RF for loc. 87: -2-45*j_0+45*m4_0 RF for loc. 88: -45*j_0+45*m4_0 RF for loc. 100: 41-45*j_0+45*m4_0 RF for loc. 104: 41-45*j_0+45*m4_0 RF for loc. 108: 41-45*j_0+45*m4_0 RF for loc. 112: 41-45*j_0+45*m4_0 RF for loc. 116: 41-45*j_0+45*m4_0 RF for loc. 120: 41-45*j_0+45*m4_0 RF for loc. 124: 41-45*j_0+45*m4_0 RF for loc. 128: 41-45*j_0+45*m4_0 Bound for (chained) transitions 105: 41 - Rank function 2: RF for loc. 53: 2-8*j_0+8*m_0 RF for loc. 54: 1-8*j_0+8*m_0 RF for loc. 55: 1-8*j_0+8*m_0 RF for loc. 56: 4-8*j_0+8*m_0 RF for loc. 57: 3-8*j_0+8*m_0 RF for loc. 58: 5-8*j_0+8*m_0 RF for loc. 59: 5-8*j_0+8*m_0 RF for loc. 61: 5-8*j_0+8*m_0 RF for loc. 62: 5-8*j_0+8*m_0 RF for loc. 63: 5-8*j_0+8*m_0 RF for loc. 64: 5-8*j_0+8*m_0 RF for loc. 65: 5-8*j_0+8*m_0 RF for loc. 66: 5-8*j_0+8*m_0 RF for loc. 67: 5-8*j_0+8*m_0 RF for loc. 68: 5-8*j_0+8*m_0 RF for loc. 69: 5-8*j_0+8*m_0 RF for loc. 70: 5-8*j_0+8*m_0 RF for loc. 71: 5-8*j_0+8*m_0 RF for loc. 72: 5-8*j_0+8*m_0 RF for loc. 73: 5-8*j_0+8*m_0 RF for loc. 74: 5-8*j_0+8*m_0 RF for loc. 75: 5-8*j_0+8*m_0 RF for loc. 76: 5-8*j_0+8*m_0 RF for loc. 77: 5-8*j_0+8*m_0 RF for loc. 78: 5-8*j_0+8*m_0 RF for loc. 79: 5-8*j_0+8*m_0 RF for loc. 80: 5-8*j_0+8*m_0 RF for loc. 81: 5-8*j_0+8*m_0 RF for loc. 82: 5-8*j_0+8*m_0 RF for loc. 83: -3-8*j_0+8*m_0 RF for loc. 84: -3-8*j_0+8*m_0 RF for loc. 85: -2-8*j_0+8*m_0 RF for loc. 86: -1-8*j_0+8*m_0 RF for loc. 87: -2-8*j_0+8*m_0 RF for loc. 88: -8*j_0+8*m_0 RF for loc. 100: 5-8*j_0+8*m_0 RF for loc. 104: 5-8*j_0+8*m_0 RF for loc. 108: 5-8*j_0+8*m_0 RF for loc. 112: 5-8*j_0+8*m_0 RF for loc. 116: 5-8*j_0+8*m_0 RF for loc. 120: 5-8*j_0+8*m_0 RF for loc. 124: 5-8*j_0+8*m_0 RF for loc. 128: 5-8*j_0+8*m_0 Bound for (chained) transitions 116: 5 - Rank function 3: RF for loc. 53: 2-40*j_0+40*m_0 RF for loc. 54: 1-40*j_0+40*m_0 RF for loc. 55: 1-40*j_0+40*m_0 RF for loc. 56: 4-40*j_0+40*m_0 RF for loc. 57: 3-40*j_0+40*m_0 RF for loc. 58: 35-40*j_0+40*m_0 RF for loc. 59: 35-40*j_0+40*m_0 RF for loc. 61: 35-40*j_0+40*m_0 RF for loc. 62: 35-40*j_0+40*m_0 RF for loc. 63: 35-40*j_0+40*m_0 RF for loc. 64: 35-40*j_0+40*m_0 RF for loc. 65: 35-40*j_0+40*m_0 RF for loc. 66: 35-40*j_0+40*m_0 RF for loc. 67: 35-40*j_0+40*m_0 RF for loc. 68: 35-40*j_0+40*m_0 RF for loc. 69: 35-40*j_0+40*m_0 RF for loc. 70: 35-40*j_0+40*m_0 RF for loc. 71: 35-40*j_0+40*m_0 RF for loc. 72: 35-40*j_0+40*m_0 RF for loc. 73: 35-40*j_0+40*m_0 RF for loc. 74: 35-40*j_0+40*m_0 RF for loc. 75: 35-40*j_0+40*m_0 RF for loc. 76: 35-40*j_0+40*m_0 RF for loc. 77: 35-40*j_0+40*m_0 RF for loc. 78: 35-40*j_0+40*m_0 RF for loc. 79: 35-40*j_0+40*m_0 RF for loc. 80: 35-40*j_0+40*m_0 RF for loc. 81: 35-40*j_0+40*m_0 RF for loc. 82: 35-40*j_0+40*m_0 RF for loc. 83: -3-40*j_0+40*m_0 RF for loc. 84: -4-40*j_0+40*m_0 RF for loc. 85: -2-40*j_0+40*m_0 RF for loc. 86: -40*j_0+40*m_0 RF for loc. 87: -1-40*j_0+40*m_0 RF for loc. 88: -40*j_0+40*m_0 RF for loc. 100: 35-40*j_0+40*m_0 RF for loc. 104: 35-40*j_0+40*m_0 RF for loc. 108: 35-40*j_0+40*m_0 RF for loc. 112: 35-40*j_0+40*m_0 RF for loc. 116: 35-40*j_0+40*m_0 RF for loc. 120: 35-40*j_0+40*m_0 RF for loc. 124: 35-40*j_0+40*m_0 RF for loc. 128: 35-40*j_0+40*m_0 Bound for (chained) transitions 127: 35 - Rank function 4: RF for loc. 53: 3-9*j_0+9*m_0 RF for loc. 54: 1-9*j_0+9*m_0 RF for loc. 55: 2-9*j_0+9*m_0 RF for loc. 56: 4-9*j_0+9*m_0 RF for loc. 57: 3-9*j_0+9*m_0 RF for loc. 58: 5-9*j_0+9*m_0 RF for loc. 59: 5-9*j_0+9*m_0 RF for loc. 61: 5-9*j_0+9*m_0 RF for loc. 62: 5-9*j_0+9*m_0 RF for loc. 63: 5-9*j_0+9*m_0 RF for loc. 64: 5-9*j_0+9*m_0 RF for loc. 65: 5-9*j_0+9*m_0 RF for loc. 66: 5-9*j_0+9*m_0 RF for loc. 67: 5-9*j_0+9*m_0 RF for loc. 68: 5-9*j_0+9*m_0 RF for loc. 69: 5-9*j_0+9*m_0 RF for loc. 70: 5-9*j_0+9*m_0 RF for loc. 71: 5-9*j_0+9*m_0 RF for loc. 72: 5-9*j_0+9*m_0 RF for loc. 73: 5-9*j_0+9*m_0 RF for loc. 74: 5-9*j_0+9*m_0 RF for loc. 75: 5-9*j_0+9*m_0 RF for loc. 76: 5-9*j_0+9*m_0 RF for loc. 77: 5-9*j_0+9*m_0 RF for loc. 78: 5-9*j_0+9*m_0 RF for loc. 79: 5-9*j_0+9*m_0 RF for loc. 80: 5-9*j_0+9*m_0 RF for loc. 81: 5-9*j_0+9*m_0 RF for loc. 82: 5-9*j_0+9*m_0 RF for loc. 83: -2-9*j_0+9*m_0 RF for loc. 84: -3-9*j_0+9*m_0 RF for loc. 85: -2-9*j_0+9*m_0 RF for loc. 86: -1-9*j_0+9*m_0 RF for loc. 87: -2-9*j_0+9*m_0 RF for loc. 88: -9*j_0+9*m_0 RF for loc. 100: 5-9*j_0+9*m_0 RF for loc. 104: 5-9*j_0+9*m_0 RF for loc. 108: 5-9*j_0+9*m_0 RF for loc. 112: 5-9*j_0+9*m_0 RF for loc. 116: 5-9*j_0+9*m_0 RF for loc. 120: 5-9*j_0+9*m_0 RF for loc. 124: 5-9*j_0+9*m_0 RF for loc. 128: 5-9*j_0+9*m_0 Bound for (chained) transitions 136: 5 - Rank function 5: RF for loc. 53: 3-57*j_0+57*m_0 RF for loc. 54: 1-57*j_0+57*m_0 RF for loc. 55: 2-57*j_0+57*m_0 RF for loc. 56: 5-57*j_0+57*m_0 RF for loc. 57: 4-57*j_0+57*m_0 RF for loc. 58: 6-57*j_0+57*m_0 RF for loc. 59: 7-57*j_0+57*m_0 RF for loc. 61: 7-57*j_0+57*m_0 RF for loc. 62: 7-57*j_0+57*m_0 RF for loc. 63: 7-57*j_0+57*m_0 RF for loc. 64: 7-57*j_0+57*m_0 RF for loc. 65: 7-57*j_0+57*m_0 RF for loc. 66: 7-57*j_0+57*m_0 RF for loc. 67: 7-57*j_0+57*m_0 RF for loc. 68: 7-57*j_0+57*m_0 RF for loc. 69: 7-57*j_0+57*m_0 RF for loc. 70: 7-57*j_0+57*m_0 RF for loc. 71: 7-57*j_0+57*m_0 RF for loc. 72: 7-57*j_0+57*m_0 RF for loc. 73: 7-57*j_0+57*m_0 RF for loc. 74: 7-57*j_0+57*m_0 RF for loc. 75: 7-57*j_0+57*m_0 RF for loc. 76: 7-57*j_0+57*m_0 RF for loc. 77: 7-57*j_0+57*m_0 RF for loc. 78: 7-57*j_0+57*m_0 RF for loc. 79: 7-57*j_0+57*m_0 RF for loc. 80: 7-57*j_0+57*m_0 RF for loc. 81: 7-57*j_0+57*m_0 RF for loc. 82: 7-57*j_0+57*m_0 RF for loc. 83: -48-57*j_0+57*m_0 RF for loc. 84: -49-57*j_0+57*m_0 RF for loc. 85: -47-57*j_0+57*m_0 RF for loc. 86: -1-57*j_0+57*m_0 RF for loc. 87: -46-57*j_0+57*m_0 RF for loc. 88: -57*j_0+57*m_0 RF for loc. 100: 7-57*j_0+57*m_0 RF for loc. 104: 7-57*j_0+57*m_0 RF for loc. 108: 7-57*j_0+57*m_0 RF for loc. 112: 7-57*j_0+57*m_0 RF for loc. 116: 7-57*j_0+57*m_0 RF for loc. 120: 7-57*j_0+57*m_0 RF for loc. 124: 7-57*j_0+57*m_0 RF for loc. 128: 7-57*j_0+57*m_0 Bound for (chained) transitions 76: 7 - Rank function 6: RF for loc. 53: 0 RF for loc. 54: 0 RF for loc. 55: 0 RF for loc. 56: 0 RF for loc. 57: 0 RF for loc. 58: 0 RF for loc. 59: -1 RF for loc. 61: -1 RF for loc. 62: -1 RF for loc. 63: -1 RF for loc. 64: -1 RF for loc. 65: -1 RF for loc. 66: -1 RF for loc. 67: -1 RF for loc. 68: -1 RF for loc. 69: -1 RF for loc. 70: -1 RF for loc. 71: -1 RF for loc. 72: -1 RF for loc. 73: -1 RF for loc. 74: -1 RF for loc. 75: -1 RF for loc. 76: -1 RF for loc. 77: -1 RF for loc. 78: -1 RF for loc. 79: -1 RF for loc. 80: -1 RF for loc. 81: -1 RF for loc. 82: -1 RF for loc. 83: -1 RF for loc. 84: -1 RF for loc. 85: -1 RF for loc. 86: 0 RF for loc. 87: 0 RF for loc. 88: 0 RF for loc. 100: -1 RF for loc. 104: -1 RF for loc. 108: -1 RF for loc. 112: -1 RF for loc. 116: -1 RF for loc. 120: -1 RF for loc. 124: -1 RF for loc. 128: -1 Bound for (chained) transitions 218: 0 - Rank function 7: RF for loc. 53: 3 RF for loc. 54: 1 RF for loc. 55: 2 RF for loc. 56: 5 RF for loc. 57: 4 RF for loc. 58: 6 RF for loc. 59: -2-3*j_0-11*joff_0+14*k_0-16*kk_0 RF for loc. 61: -3*j_0-11*joff_0+14*k_0-16*kk_0 RF for loc. 62: 2-3*j_0-11*joff_0+14*k_0-16*kk_0 RF for loc. 63: 1-3*j_0-11*joff_0+14*k_0-16*kk_0 RF for loc. 64: 3-3*j_0-11*joff_0+14*k_0-16*kk_0 RF for loc. 65: 5-3*j_0-11*joff_0+14*k_0-16*kk_0 RF for loc. 66: 4-3*j_0-11*joff_0+14*k_0-16*kk_0 RF for loc. 67: 6-3*j_0-11*joff_0+14*k_0-16*kk_0 RF for loc. 68: 7-3*j_0-11*joff_0+14*k_0-16*kk_0 RF for loc. 69: 9-3*j_0-11*joff_0+14*k_0-16*kk_0 RF for loc. 70: 7-3*j_0-11*joff_0+14*k_0-16*kk_0 RF for loc. 71: 8-3*j_0-11*joff_0+14*k_0-16*kk_0 RF for loc. 72: 1-3*j_0-11*joff_0+14*k_0-16*kk_0 RF for loc. 73: 11-3*j_0-11*joff_0+14*k_0-16*kk_0 RF for loc. 74: 2-3*j_0-11*joff_0+14*k_0-16*kk_0 RF for loc. 75: 4-3*j_0-11*joff_0+14*k_0-16*kk_0 RF for loc. 76: 5-3*j_0-11*joff_0+14*k_0-16*kk_0 RF for loc. 77: 6-3*j_0-11*joff_0+14*k_0-16*kk_0 RF for loc. 78: 7-3*j_0-11*joff_0+14*k_0-16*kk_0 RF for loc. 79: 8-3*j_0-11*joff_0+14*k_0-16*kk_0 RF for loc. 80: 9-3*j_0-11*joff_0+14*k_0-16*kk_0 RF for loc. 81: 10-3*j_0-11*joff_0+14*k_0-16*kk_0 RF for loc. 82: 12-3*j_0-11*joff_0+14*k_0-16*kk_0 RF for loc. 83: -1-3*j_0-11*joff_0+14*k_0-16*kk_0 RF for loc. 84: -2-3*j_0-11*joff_0+14*k_0-16*kk_0 RF for loc. 85: -3*j_0-11*joff_0+14*k_0-16*kk_0 RF for loc. 86: -1 RF for loc. 87: -2 RF for loc. 88: 0 RF for loc. 100: -1-3*j_0-11*joff_0+14*k_0-16*kk_0 RF for loc. 104: 8-3*j_0-11*joff_0+14*k_0-16*kk_0 RF for loc. 108: 7-3*j_0-11*joff_0+14*k_0-16*kk_0 RF for loc. 112: 3-3*j_0-11*joff_0+14*k_0-16*kk_0 RF for loc. 116: 5-3*j_0-11*joff_0+14*k_0-16*kk_0 RF for loc. 120: 7-3*j_0-11*joff_0+14*k_0-16*kk_0 RF for loc. 124: 10-3*j_0-11*joff_0+14*k_0-16*kk_0 RF for loc. 128: 13-3*j_0-11*joff_0+14*k_0-16*kk_0 Bound for (chained) transitions 68: 3 Bound for (chained) transitions 69: 3 Bound for (chained) transitions 70: 5 Bound for (chained) transitions 71: 4 Bound for (chained) transitions 217: -1 Bound for (chained) transitions 219: 0 Bound for (chained) transitions 220: 0 Bound for (chained) transitions 221: 0 Bound for (chained) transitions 222: 2 Bound for (chained) transitions 223: 1 - Rank function 8: RF for loc. 53: 0 RF for loc. 54: -1 RF for loc. 56: 0 RF for loc. 57: 0 RF for loc. 58: 1 RF for loc. 59: -3-2*j_0-15*joff_0+5*k_0-16*kk_0 RF for loc. 61: -1-2*j_0-15*joff_0+5*k_0-16*kk_0 RF for loc. 62: 1-2*j_0-15*joff_0+5*k_0-16*kk_0 RF for loc. 63: -2*j_0-15*joff_0+5*k_0-16*kk_0 RF for loc. 64: 2-2*j_0-15*joff_0+5*k_0-16*kk_0 RF for loc. 65: 4-2*j_0-15*joff_0+5*k_0-16*kk_0 RF for loc. 66: 3-2*j_0-15*joff_0+5*k_0-16*kk_0 RF for loc. 67: 5-2*j_0-15*joff_0+5*k_0-16*kk_0 RF for loc. 68: 6-2*j_0-15*joff_0+5*k_0-16*kk_0 RF for loc. 69: 7-2*j_0-15*joff_0+5*k_0-16*kk_0 RF for loc. 70: -4-2*j_0-15*joff_0+5*k_0-16*kk_0 RF for loc. 71: 7-2*j_0-15*joff_0+5*k_0-16*kk_0 RF for loc. 72: -4-2*j_0-15*joff_0+5*k_0-16*kk_0 RF for loc. 73: 10-2*j_0-15*joff_0+5*k_0-16*kk_0 RF for loc. 74: -3-2*j_0-15*joff_0+5*k_0-16*kk_0 RF for loc. 75: -1-2*j_0-15*joff_0+5*k_0-16*kk_0 RF for loc. 76: -2*j_0-15*joff_0+5*k_0-16*kk_0 RF for loc. 77: 4-2*j_0-15*joff_0+5*k_0-16*kk_0 RF for loc. 78: 4-2*j_0-15*joff_0+5*k_0-16*kk_0 RF for loc. 79: 6-2*j_0-15*joff_0+5*k_0-16*kk_0 RF for loc. 80: 7-2*j_0-15*joff_0+5*k_0-16*kk_0 RF for loc. 81: 8-2*j_0-15*joff_0+5*k_0-16*kk_0 RF for loc. 82: 11-2*j_0-15*joff_0+5*k_0-16*kk_0 RF for loc. 83: -1-2*j_0-15*joff_0+5*k_0-16*kk_0 RF for loc. 84: -2-2*j_0-15*joff_0+5*k_0-16*kk_0 RF for loc. 85: -2*j_0-15*joff_0+5*k_0-16*kk_0 RF for loc. 100: -2-2*j_0-15*joff_0+5*k_0-16*kk_0 RF for loc. 104: 6-2*j_0-15*joff_0+5*k_0-16*kk_0 RF for loc. 108: 6-2*j_0-15*joff_0+5*k_0-16*kk_0 RF for loc. 112: -2-2*j_0-15*joff_0+5*k_0-16*kk_0 RF for loc. 116: 3-2*j_0-15*joff_0+5*k_0-16*kk_0 RF for loc. 120: 5-2*j_0-15*joff_0+5*k_0-16*kk_0 RF for loc. 124: 9-2*j_0-15*joff_0+5*k_0-16*kk_0 RF for loc. 128: 12-2*j_0-15*joff_0+5*k_0-16*kk_0 Bound for (chained) transitions 67: 0 - Rank function 9: RF for loc. 56: -1 RF for loc. 57: -1 RF for loc. 58: 0 RF for loc. 59: -3-2*j_0-12*joff_0+2*k_0-15*kk_0 RF for loc. 61: -1-2*j_0-12*joff_0+2*k_0-15*kk_0 RF for loc. 62: 1-2*j_0-12*joff_0+2*k_0-15*kk_0 RF for loc. 63: -2*j_0-12*joff_0+2*k_0-15*kk_0 RF for loc. 64: 2-2*j_0-12*joff_0+2*k_0-15*kk_0 RF for loc. 65: 4-2*j_0-12*joff_0+2*k_0-15*kk_0 RF for loc. 66: 3-2*j_0-12*joff_0+2*k_0-15*kk_0 RF for loc. 67: 5-2*j_0-12*joff_0+2*k_0-15*kk_0 RF for loc. 68: 6-2*j_0-12*joff_0+2*k_0-15*kk_0 RF for loc. 69: 7-2*j_0-12*joff_0+2*k_0-15*kk_0 RF for loc. 70: 4-2*j_0-12*joff_0+2*k_0-15*kk_0 RF for loc. 71: 6-2*j_0-12*joff_0+2*k_0-15*kk_0 RF for loc. 72: -2-2*j_0-12*joff_0+2*k_0-15*kk_0 RF for loc. 73: 9-2*j_0-12*joff_0+2*k_0-15*kk_0 RF for loc. 74: -1-2*j_0-12*joff_0+2*k_0-15*kk_0 RF for loc. 75: 1-2*j_0-12*joff_0+2*k_0-15*kk_0 RF for loc. 76: 2-2*j_0-12*joff_0+2*k_0-15*kk_0 RF for loc. 77: 4-2*j_0-12*joff_0+2*k_0-15*kk_0 RF for loc. 78: 5-2*j_0-12*joff_0+2*k_0-15*kk_0 RF for loc. 79: 6-2*j_0-12*joff_0+2*k_0-15*kk_0 RF for loc. 80: 7-2*j_0-12*joff_0+2*k_0-15*kk_0 RF for loc. 81: 8-2*j_0-12*joff_0+2*k_0-15*kk_0 RF for loc. 82: 10-2*j_0-12*joff_0+2*k_0-15*kk_0 RF for loc. 83: -1-2*j_0-12*joff_0+2*k_0-15*kk_0 RF for loc. 84: -2-2*j_0-12*joff_0+2*k_0-15*kk_0 RF for loc. 85: -2*j_0-12*joff_0+2*k_0-15*kk_0 RF for loc. 100: -2-2*j_0-12*joff_0+2*k_0-15*kk_0 RF for loc. 104: 6-2*j_0-12*joff_0+2*k_0-15*kk_0 RF for loc. 108: 5-2*j_0-12*joff_0+2*k_0-15*kk_0 RF for loc. 112: -2*j_0-12*joff_0+2*k_0-15*kk_0 RF for loc. 116: 3-2*j_0-12*joff_0+2*k_0-15*kk_0 RF for loc. 120: 6-2*j_0-12*joff_0+2*k_0-15*kk_0 RF for loc. 124: 8-2*j_0-12*joff_0+2*k_0-15*kk_0 RF for loc. 128: 11-2*j_0-12*joff_0+2*k_0-15*kk_0 Bound for (chained) transitions 73: 0 - Rank function 10: RF for loc. 56: 0 RF for loc. 57: 0 RF for loc. 58: 1 RF for loc. 59: -2-2*j_0-12*joff_0+2*k_0-14*kk_0 RF for loc. 61: -1-2*j_0-12*joff_0+2*k_0-14*kk_0 RF for loc. 62: 1-2*j_0-12*joff_0+2*k_0-14*kk_0 RF for loc. 63: -2*j_0-12*joff_0+2*k_0-14*kk_0 RF for loc. 64: 2-2*j_0-12*joff_0+2*k_0-14*kk_0 RF for loc. 65: 4-2*j_0-12*joff_0+2*k_0-14*kk_0 RF for loc. 66: 3-2*j_0-12*joff_0+2*k_0-14*kk_0 RF for loc. 67: 5-2*j_0-12*joff_0+2*k_0-14*kk_0 RF for loc. 68: 6-2*j_0-12*joff_0+2*k_0-14*kk_0 RF for loc. 69: 7-2*j_0-12*joff_0+2*k_0-14*kk_0 RF for loc. 70: 4-2*j_0-12*joff_0+2*k_0-14*kk_0 RF for loc. 71: 6-2*j_0-12*joff_0+2*k_0-14*kk_0 RF for loc. 72: -2-2*j_0-12*joff_0+2*k_0-14*kk_0 RF for loc. 73: 9-2*j_0-12*joff_0+2*k_0-14*kk_0 RF for loc. 74: -1-2*j_0-12*joff_0+2*k_0-14*kk_0 RF for loc. 75: -2*j_0-12*joff_0+2*k_0-14*kk_0 RF for loc. 76: 1-2*j_0-12*joff_0+2*k_0-14*kk_0 RF for loc. 77: 3-2*j_0-12*joff_0+2*k_0-14*kk_0 RF for loc. 78: 4-2*j_0-12*joff_0+2*k_0-14*kk_0 RF for loc. 79: 6-2*j_0-12*joff_0+2*k_0-14*kk_0 RF for loc. 80: 7-2*j_0-12*joff_0+2*k_0-14*kk_0 RF for loc. 81: 8-2*j_0-12*joff_0+2*k_0-14*kk_0 RF for loc. 82: 10-2*j_0-12*joff_0+2*k_0-14*kk_0 RF for loc. 83: -1-2*j_0-12*joff_0+2*k_0-14*kk_0 RF for loc. 84: -2-2*j_0-12*joff_0+2*k_0-14*kk_0 RF for loc. 85: -2*j_0-12*joff_0+2*k_0-14*kk_0 RF for loc. 100: -2-2*j_0-12*joff_0+2*k_0-14*kk_0 RF for loc. 104: 6-2*j_0-12*joff_0+2*k_0-14*kk_0 RF for loc. 108: 5-2*j_0-12*joff_0+2*k_0-14*kk_0 RF for loc. 112: -1-2*j_0-12*joff_0+2*k_0-14*kk_0 RF for loc. 116: 2-2*j_0-12*joff_0+2*k_0-14*kk_0 RF for loc. 120: 5-2*j_0-12*joff_0+2*k_0-14*kk_0 RF for loc. 124: 8-2*j_0-12*joff_0+2*k_0-14*kk_0 RF for loc. 128: 11-2*j_0-12*joff_0+2*k_0-14*kk_0 Bound for (chained) transitions 72: 1 - Rank function 11: RF for loc. 56: -1 RF for loc. 58: 0 RF for loc. 59: -2-2*j_0-13*joff_0+5*k_0-14*kk_0 RF for loc. 61: -1-2*j_0-13*joff_0+5*k_0-14*kk_0 RF for loc. 62: 1-2*j_0-13*joff_0+5*k_0-14*kk_0 RF for loc. 63: -2*j_0-13*joff_0+5*k_0-14*kk_0 RF for loc. 64: 2-2*j_0-13*joff_0+5*k_0-14*kk_0 RF for loc. 65: 4-2*j_0-13*joff_0+5*k_0-14*kk_0 RF for loc. 66: 3-2*j_0-13*joff_0+5*k_0-14*kk_0 RF for loc. 67: 4-2*j_0-13*joff_0+5*k_0-14*kk_0 RF for loc. 68: 5-2*j_0-13*joff_0+5*k_0-14*kk_0 RF for loc. 69: 6-2*j_0-13*joff_0+5*k_0-14*kk_0 RF for loc. 70: 4-2*j_0-13*joff_0+5*k_0-14*kk_0 RF for loc. 71: 5-2*j_0-13*joff_0+5*k_0-14*kk_0 RF for loc. 72: -3-2*j_0-13*joff_0+5*k_0-14*kk_0 RF for loc. 73: 9-2*j_0-13*joff_0+5*k_0-14*kk_0 RF for loc. 74: -3-2*j_0-13*joff_0+5*k_0-14*kk_0 RF for loc. 75: -1-2*j_0-13*joff_0+5*k_0-14*kk_0 RF for loc. 76: -2*j_0-13*joff_0+5*k_0-14*kk_0 RF for loc. 77: 2-2*j_0-13*joff_0+5*k_0-14*kk_0 RF for loc. 78: 3-2*j_0-13*joff_0+5*k_0-14*kk_0 RF for loc. 79: 5-2*j_0-13*joff_0+5*k_0-14*kk_0 RF for loc. 80: 6-2*j_0-13*joff_0+5*k_0-14*kk_0 RF for loc. 81: 7-2*j_0-13*joff_0+5*k_0-14*kk_0 RF for loc. 82: 10-2*j_0-13*joff_0+5*k_0-14*kk_0 RF for loc. 83: -1-2*j_0-13*joff_0+5*k_0-14*kk_0 RF for loc. 84: -2-2*j_0-13*joff_0+5*k_0-14*kk_0 RF for loc. 85: -2*j_0-13*joff_0+5*k_0-14*kk_0 RF for loc. 100: -2-2*j_0-13*joff_0+5*k_0-14*kk_0 RF for loc. 104: 5-2*j_0-13*joff_0+5*k_0-14*kk_0 RF for loc. 108: 4-2*j_0-13*joff_0+5*k_0-14*kk_0 RF for loc. 112: -2-2*j_0-13*joff_0+5*k_0-14*kk_0 RF for loc. 116: 1-2*j_0-13*joff_0+5*k_0-14*kk_0 RF for loc. 120: 4-2*j_0-13*joff_0+5*k_0-14*kk_0 RF for loc. 124: 8-2*j_0-13*joff_0+5*k_0-14*kk_0 RF for loc. 128: 11-2*j_0-13*joff_0+5*k_0-14*kk_0 Bound for (chained) transitions 74: 0 - Rank function 12: RF for loc. 59: -1 RF for loc. 61: -1 RF for loc. 62: -1 RF for loc. 63: -1 RF for loc. 64: -1 RF for loc. 65: -1 RF for loc. 66: -1 RF for loc. 67: -1 RF for loc. 68: -1 RF for loc. 69: -1 RF for loc. 70: -1 RF for loc. 71: -1 RF for loc. 72: -1 RF for loc. 73: -1 RF for loc. 74: -1 RF for loc. 75: -1 RF for loc. 76: -1 RF for loc. 77: -1 RF for loc. 78: -1 RF for loc. 79: -1 RF for loc. 80: -1 RF for loc. 81: -1 RF for loc. 82: -1 RF for loc. 83: 0 RF for loc. 84: -1 RF for loc. 85: 0 RF for loc. 100: -1 RF for loc. 104: -1 RF for loc. 108: -1 RF for loc. 112: -1 RF for loc. 116: -1 RF for loc. 120: -1 RF for loc. 124: -1 RF for loc. 128: -1 Bound for (chained) transitions 212: 0 - Rank function 13: RF for loc. 59: -2-44*joff_0 RF for loc. 61: -2-44*joff_0 RF for loc. 62: -2-44*joff_0 RF for loc. 63: -2-44*joff_0 RF for loc. 64: -2-44*joff_0 RF for loc. 65: -2-44*joff_0 RF for loc. 66: -2-44*joff_0 RF for loc. 67: -2-44*joff_0 RF for loc. 68: -2-44*joff_0 RF for loc. 69: -2-44*joff_0 RF for loc. 70: -14-44*joff_0 RF for loc. 71: -13-44*joff_0 RF for loc. 72: -42-44*joff_0 RF for loc. 73: -2-44*joff_0 RF for loc. 74: -41-44*joff_0 RF for loc. 75: -39-44*joff_0 RF for loc. 76: -38-44*joff_0 RF for loc. 77: -36-44*joff_0 RF for loc. 78: -35-44*joff_0 RF for loc. 79: -33-44*joff_0 RF for loc. 80: -3-44*joff_0 RF for loc. 81: -2-44*joff_0 RF for loc. 82: -2-44*joff_0 RF for loc. 83: -1-44*joff_0 RF for loc. 84: -1-44*joff_0 RF for loc. 85: -44*joff_0 RF for loc. 100: -2-44*joff_0 RF for loc. 104: -2-44*joff_0 RF for loc. 108: -13-44*joff_0 RF for loc. 112: -40-44*joff_0 RF for loc. 116: -37-44*joff_0 RF for loc. 120: -34-44*joff_0 RF for loc. 124: -2-44*joff_0 RF for loc. 128: -2-44*joff_0 Bound for (chained) transitions 150: -2 - Rank function 14: RF for loc. 59: -4+13*k_0-13*kk_0 RF for loc. 61: -2+13*k_0-13*kk_0 RF for loc. 62: 13*k_0-13*kk_0 RF for loc. 63: -1+13*k_0-13*kk_0 RF for loc. 64: 13*k_0-13*kk_0 RF for loc. 65: 2+13*k_0-13*kk_0 RF for loc. 66: 1+13*k_0-13*kk_0 RF for loc. 67: 2+13*k_0-13*kk_0 RF for loc. 68: 3+13*k_0-13*kk_0 RF for loc. 69: 3+13*k_0-13*kk_0 RF for loc. 70: 8+13*k_0-13*kk_0 RF for loc. 71: 10+13*k_0-13*kk_0 RF for loc. 72: 7+13*k_0-13*kk_0 RF for loc. 73: 6+13*k_0-13*kk_0 RF for loc. 74: 7+13*k_0-13*kk_0 RF for loc. 75: 9+13*k_0-13*kk_0 RF for loc. 76: 10+13*k_0-13*kk_0 RF for loc. 77: 12+13*k_0-13*kk_0 RF for loc. 78: 13+13*k_0-13*kk_0 RF for loc. 79: 15+13*k_0-13*kk_0 RF for loc. 80: 16+13*k_0-13*kk_0 RF for loc. 81: 4+13*k_0-13*kk_0 RF for loc. 82: 7+13*k_0-13*kk_0 RF for loc. 83: -1+13*k_0-13*kk_0 RF for loc. 84: -1+13*k_0-13*kk_0 RF for loc. 85: 13*k_0-13*kk_0 RF for loc. 100: -3+13*k_0-13*kk_0 RF for loc. 104: 3+13*k_0-13*kk_0 RF for loc. 108: 9+13*k_0-13*kk_0 RF for loc. 112: 8+13*k_0-13*kk_0 RF for loc. 116: 11+13*k_0-13*kk_0 RF for loc. 120: 14+13*k_0-13*kk_0 RF for loc. 124: 5+13*k_0-13*kk_0 RF for loc. 128: 8+13*k_0-13*kk_0 Bound for (chained) transitions 160: 7 - Rank function 15: RF for loc. 59: -51-41*j_0+41*mm_0 RF for loc. 61: -49-41*j_0+41*mm_0 RF for loc. 62: -47-41*j_0+41*mm_0 RF for loc. 63: -48-41*j_0+41*mm_0 RF for loc. 64: -46-41*j_0+41*mm_0 RF for loc. 65: -44-41*j_0+41*mm_0 RF for loc. 66: -45-41*j_0+41*mm_0 RF for loc. 67: -43-41*j_0+41*mm_0 RF for loc. 68: -42-41*j_0+41*mm_0 RF for loc. 69: -2-41*j_0+41*mm_0 RF for loc. 70: 3-41*j_0+41*mm_0 RF for loc. 71: 5-41*j_0+41*mm_0 RF for loc. 72: 2-41*j_0+41*mm_0 RF for loc. 73: 1-41*j_0+41*mm_0 RF for loc. 74: 3-41*j_0+41*mm_0 RF for loc. 75: 5-41*j_0+41*mm_0 RF for loc. 76: 6-41*j_0+41*mm_0 RF for loc. 77: 8-41*j_0+41*mm_0 RF for loc. 78: 9-41*j_0+41*mm_0 RF for loc. 79: 11-41*j_0+41*mm_0 RF for loc. 80: 12-41*j_0+41*mm_0 RF for loc. 81: -1-41*j_0+41*mm_0 RF for loc. 82: -52-41*j_0+41*mm_0 RF for loc. 83: -1-41*j_0+41*mm_0 RF for loc. 84: -1-41*j_0+41*mm_0 RF for loc. 85: -41*j_0+41*mm_0 RF for loc. 100: -50-41*j_0+41*mm_0 RF for loc. 104: -3-41*j_0+41*mm_0 RF for loc. 108: 4-41*j_0+41*mm_0 RF for loc. 112: 4-41*j_0+41*mm_0 RF for loc. 116: 7-41*j_0+41*mm_0 RF for loc. 120: 10-41*j_0+41*mm_0 RF for loc. 124: -41*j_0+41*mm_0 RF for loc. 128: -52-41*j_0+41*mm_0 Bound for (chained) transitions 96: -42 - Rank function 16: RF for loc. 59: -13 RF for loc. 61: -11 RF for loc. 62: -9 RF for loc. 63: -10 RF for loc. 64: -8 RF for loc. 65: -6 RF for loc. 66: -7 RF for loc. 67: -5 RF for loc. 68: -4 RF for loc. 69: -2 RF for loc. 70: 3 RF for loc. 71: 5 RF for loc. 72: 2 RF for loc. 73: 1 RF for loc. 74: 3 RF for loc. 75: 5 RF for loc. 76: 6 RF for loc. 77: 8 RF for loc. 78: 9 RF for loc. 79: 11 RF for loc. 80: 12 RF for loc. 81: -1 RF for loc. 82: -15 RF for loc. 83: -1 RF for loc. 84: -1 RF for loc. 85: 0 RF for loc. 100: -12 RF for loc. 104: -3 RF for loc. 108: 4 RF for loc. 112: 4 RF for loc. 116: 7 RF for loc. 120: 10 RF for loc. 124: 0 RF for loc. 128: -14 Bound for (chained) transitions 75, 161: -13 Bound for (chained) transitions 77: -11 Bound for (chained) transitions 79: -12 Bound for (chained) transitions 80: -12 Bound for (chained) transitions 85: -9 Bound for (chained) transitions 86: -10 Bound for (chained) transitions 87: -8 Bound for (chained) transitions 88: -8 Bound for (chained) transitions 89: -8 Bound for (chained) transitions 90: -6 Bound for (chained) transitions 91: -7 Bound for (chained) transitions 92: -5 Bound for (chained) transitions 93: -5 Bound for (chained) transitions 94: -5 Bound for (chained) transitions 95: -4 Bound for (chained) transitions 97: -2 Bound for (chained) transitions 99: -3 Bound for (chained) transitions 100: -3 Bound for (chained) transitions 106: 3 Bound for (chained) transitions 107: 5 Bound for (chained) transitions 109: 4 Bound for (chained) transitions 110: 4 Bound for (chained) transitions 115: 2 Bound for (chained) transitions 117: 3 Bound for (chained) transitions 118: 5 Bound for (chained) transitions 120: 4 Bound for (chained) transitions 121: 4 Bound for (chained) transitions 126: 6 Bound for (chained) transitions 128: 8 Bound for (chained) transitions 130: 7 Bound for (chained) transitions 131: 7 Bound for (chained) transitions 137: 9 Bound for (chained) transitions 138: 11 Bound for (chained) transitions 140: 10 Bound for (chained) transitions 141: 10 Bound for (chained) transitions 146: 12 Bound for (chained) transitions 147: 12 Bound for (chained) transitions 148: 12 Bound for (chained) transitions 149: -1 Bound for (chained) transitions 151: 1 Bound for (chained) transitions 153: 0 Bound for (chained) transitions 154: 0 Bound for (chained) transitions 163: -14 Bound for (chained) transitions 164: -14 Bound for (chained) transitions 213: -1 Bound for (chained) transitions 214: 0 Bound for (chained) transitions 215: 0 Bound for (chained) transitions 216: 0 * Removed transitions 169, 171, 173, 174 using the following rank functions: - Rank function 1: RF for loc. 91: -1-2*j_0+2*m_0 RF for loc. 132: -2*j_0+2*m_0 Bound for (chained) transitions 169, 171: -1 - Rank function 2: RF for loc. 91: -1 RF for loc. 132: 0 Bound for (chained) transitions 174: 0 - Rank function 3: RF for loc. 91: -1 RF for loc. 132: 0 Bound for (chained) transitions 173: 0 * Removed transitions 179, 180, 182, 183 using the following rank functions: - Rank function 1: RF for loc. 93: -1-2*j_0+2*m_0 RF for loc. 136: -2*j_0+2*m_0 Bound for (chained) transitions 179, 180: -1 - Rank function 2: RF for loc. 93: 0 RF for loc. 136: 1 Bound for (chained) transitions 183: 1 - Rank function 3: RF for loc. 93: -1 RF for loc. 136: 0 Bound for (chained) transitions 182: 0 * Removed transitions 188, 189, 190, 191, 192, 193, 195, 197, 198 using the following rank functions: - Rank function 1: RF for loc. 95: -3-5*j_0+5*mm_0 RF for loc. 96: -4-5*j_0+5*mm_0 RF for loc. 98: -2-5*j_0+5*mm_0 RF for loc. 99: -1-5*j_0+5*mm_0 RF for loc. 140: -5*j_0+5*mm_0 Bound for (chained) transitions 193: -1 - Rank function 2: RF for loc. 95: -1 RF for loc. 96: -2 RF for loc. 98: 0 RF for loc. 99: -4 RF for loc. 140: -3 Bound for (chained) transitions 188: -1 Bound for (chained) transitions 189, 195: -2 Bound for (chained) transitions 190: 0 Bound for (chained) transitions 191: 0 Bound for (chained) transitions 192: 0 Bound for (chained) transitions 197: -3 Bound for (chained) transitions 198: -3 Errors: