YES Termination proof succeeded Initially, performed program simplifications using lexicographic rank functions: * Removed transitions 82, 113, 115, 116, 131, 133, 134, 143, 145, 146, 161, 163, 164, 171, 173, 174, 183, 185, 186, 231, 240, 241, 242, 243, 244, 245, 246, 247, 248, 249, 250, 251, 252, 253, 262, 263, 264, 265, 266, 267 using the following rank functions: - Rank function 1: RF for loc. 61: 14*n_0-14*ni_0 RF for loc. 62: 14*n_0-14*ni_0 RF for loc. 63: 14*n_0-14*ni_0 RF for loc. 64: 14*n_0-14*ni_0 RF for loc. 65: 14*n_0-14*ni_0 RF for loc. 66: 14*n_0-14*ni_0 RF for loc. 67: 14*n_0-14*ni_0 RF for loc. 68: 14*n_0-14*ni_0 RF for loc. 69: 14*n_0-14*ni_0 RF for loc. 70: 14*n_0-14*ni_0 RF for loc. 71: 14*n_0-14*ni_0 RF for loc. 72: 14*n_0-14*ni_0 RF for loc. 73: 14*n_0-14*ni_0 RF for loc. 74: 14*n_0-14*ni_0 RF for loc. 75: 14*n_0-14*ni_0 RF for loc. 76: 14*n_0-14*ni_0 RF for loc. 87: 12+14*n_0-14*ni_0 RF for loc. 119: 13+14*n_0-14*ni_0 RF for loc. 123: 14*n_0-14*ni_0 RF for loc. 127: 14*n_0-14*ni_0 RF for loc. 131: 14*n_0-14*ni_0 RF for loc. 135: 14*n_0-14*ni_0 RF for loc. 139: 14*n_0-14*ni_0 Bound for (chained) transitions 82: 26 - Rank function 2: RF for loc. 61: 2+13*n_0-13*nj_0 RF for loc. 62: 13*n_0-13*nj_0 RF for loc. 63: -10+13*n_0-13*nj_0 RF for loc. 64: -10+13*n_0-13*nj_0 RF for loc. 65: -10+13*n_0-13*nj_0 RF for loc. 66: -10+13*n_0-13*nj_0 RF for loc. 67: -10+13*n_0-13*nj_0 RF for loc. 68: -10+13*n_0-13*nj_0 RF for loc. 69: -10+13*n_0-13*nj_0 RF for loc. 70: -10+13*n_0-13*nj_0 RF for loc. 71: -10+13*n_0-13*nj_0 RF for loc. 72: -10+13*n_0-13*nj_0 RF for loc. 73: -10+13*n_0-13*nj_0 RF for loc. 74: -10+13*n_0-13*nj_0 RF for loc. 75: -10+13*n_0-13*nj_0 RF for loc. 76: -10+13*n_0-13*nj_0 RF for loc. 87: -2+13*n_0-13*nj_0 RF for loc. 119: -1+13*n_0-13*nj_0 RF for loc. 123: 1+13*n_0-13*nj_0 RF for loc. 127: -10+13*n_0-13*nj_0 RF for loc. 131: -10+13*n_0-13*nj_0 RF for loc. 135: -10+13*n_0-13*nj_0 RF for loc. 139: -10+13*n_0-13*nj_0 Bound for (chained) transitions 267: 13 - Rank function 3: RF for loc. 61: 9*n_0-9*nk1_0 RF for loc. 62: -2+9*n_0-9*nk1_0 RF for loc. 63: 2+9*n_0-9*nk1_0 RF for loc. 64: 9*n_0-9*nk1_0 RF for loc. 65: -6+9*n_0-9*nk1_0 RF for loc. 66: -6+9*n_0-9*nk1_0 RF for loc. 67: -6+9*n_0-9*nk1_0 RF for loc. 68: -6+9*n_0-9*nk1_0 RF for loc. 69: -6+9*n_0-9*nk1_0 RF for loc. 70: -6+9*n_0-9*nk1_0 RF for loc. 71: -6+9*n_0-9*nk1_0 RF for loc. 72: -6+9*n_0-9*nk1_0 RF for loc. 73: -6+9*n_0-9*nk1_0 RF for loc. 74: -6+9*n_0-9*nk1_0 RF for loc. 75: -6+9*n_0-9*nk1_0 RF for loc. 76: -6+9*n_0-9*nk1_0 RF for loc. 87: -4+9*n_0-9*nk1_0 RF for loc. 119: -3+9*n_0-9*nk1_0 RF for loc. 123: -1+9*n_0-9*nk1_0 RF for loc. 127: 1+9*n_0-9*nk1_0 RF for loc. 131: -6+9*n_0-9*nk1_0 RF for loc. 135: -6+9*n_0-9*nk1_0 RF for loc. 139: -6+9*n_0-9*nk1_0 Bound for (chained) transitions 265: 9 - Rank function 4: RF for loc. 61: -4 RF for loc. 62: -6 RF for loc. 63: -1 RF for loc. 64: -3 RF for loc. 65: 0 RF for loc. 66: 0 RF for loc. 67: 0 RF for loc. 68: 0 RF for loc. 69: 0 RF for loc. 70: 0 RF for loc. 71: 0 RF for loc. 72: 0 RF for loc. 73: 0 RF for loc. 74: 0 RF for loc. 75: 0 RF for loc. 76: 0 RF for loc. 87: -8 RF for loc. 119: -7 RF for loc. 123: -5 RF for loc. 127: -2 RF for loc. 131: 0 RF for loc. 135: 0 RF for loc. 139: 0 Bound for (chained) transitions 113, 266: -6 Bound for (chained) transitions 115: -7 Bound for (chained) transitions 116: -7 Bound for (chained) transitions 131: -4 Bound for (chained) transitions 133: -5 Bound for (chained) transitions 134: -5 Bound for (chained) transitions 143: -1 Bound for (chained) transitions 145: -2 Bound for (chained) transitions 146: -2 Bound for (chained) transitions 262: 0 Bound for (chained) transitions 264: -3 - Rank function 5: RF for loc. 65: 2+12*n_0-12*nl1_0 RF for loc. 66: 12*n_0-12*nl1_0 RF for loc. 67: -9+12*n_0-12*nl1_0 RF for loc. 68: -9+12*n_0-12*nl1_0 RF for loc. 69: -9+12*n_0-12*nl1_0 RF for loc. 70: -9+12*n_0-12*nl1_0 RF for loc. 71: -9+12*n_0-12*nl1_0 RF for loc. 72: -9+12*n_0-12*nl1_0 RF for loc. 73: -9+12*n_0-12*nl1_0 RF for loc. 74: -9+12*n_0-12*nl1_0 RF for loc. 75: -9+12*n_0-12*nl1_0 RF for loc. 76: -9+12*n_0-12*nl1_0 RF for loc. 131: 1+12*n_0-12*nl1_0 RF for loc. 135: -9+12*n_0-12*nl1_0 RF for loc. 139: -9+12*n_0-12*nl1_0 Bound for (chained) transitions 263: 12 - Rank function 6: RF for loc. 65: -1+12*n_0-12*nk2_0 RF for loc. 66: -3+12*n_0-12*nk2_0 RF for loc. 67: 2+12*n_0-12*nk2_0 RF for loc. 68: 12*n_0-12*nk2_0 RF for loc. 69: -9+12*n_0-12*nk2_0 RF for loc. 70: -9+12*n_0-12*nk2_0 RF for loc. 71: -9+12*n_0-12*nk2_0 RF for loc. 72: -9+12*n_0-12*nk2_0 RF for loc. 73: -9+12*n_0-12*nk2_0 RF for loc. 74: -9+12*n_0-12*nk2_0 RF for loc. 75: -9+12*n_0-12*nk2_0 RF for loc. 76: -9+12*n_0-12*nk2_0 RF for loc. 131: -2+12*n_0-12*nk2_0 RF for loc. 135: 1+12*n_0-12*nk2_0 RF for loc. 139: -9+12*n_0-12*nk2_0 Bound for (chained) transitions 253: 12 - Rank function 7: RF for loc. 65: -4 RF for loc. 66: -6 RF for loc. 67: -1 RF for loc. 68: -3 RF for loc. 69: 0 RF for loc. 70: 0 RF for loc. 71: 0 RF for loc. 72: 0 RF for loc. 73: 0 RF for loc. 74: 0 RF for loc. 75: 0 RF for loc. 76: 0 RF for loc. 131: -5 RF for loc. 135: -2 RF for loc. 139: 0 Bound for (chained) transitions 161: -4 Bound for (chained) transitions 163: -5 Bound for (chained) transitions 164: -5 Bound for (chained) transitions 171: -1 Bound for (chained) transitions 173: -2 Bound for (chained) transitions 174: -2 Bound for (chained) transitions 250: 0 Bound for (chained) transitions 252: -3 - Rank function 8: RF for loc. 69: 2+8*n_0-8*nl2_0 RF for loc. 70: 8*n_0-8*nl2_0 RF for loc. 71: -5+8*n_0-8*nl2_0 RF for loc. 72: -4+8*n_0-8*nl2_0 RF for loc. 73: -3+8*n_0-8*nl2_0 RF for loc. 74: -3+8*n_0-8*nl2_0 RF for loc. 75: -2+8*n_0-8*nl2_0 RF for loc. 76: -1+8*n_0-8*nl2_0 RF for loc. 139: 1+8*n_0-8*nl2_0 Bound for (chained) transitions 251: 8 - Rank function 9: RF for loc. 69: -5 RF for loc. 70: -7 RF for loc. 71: -4 RF for loc. 72: -3 RF for loc. 73: -2 RF for loc. 74: -1 RF for loc. 75: 0 RF for loc. 76: 1 RF for loc. 139: -6 Bound for (chained) transitions 183: -5 Bound for (chained) transitions 185: -6 Bound for (chained) transitions 186: -6 Bound for (chained) transitions 231: -4 Bound for (chained) transitions 240: -3 Bound for (chained) transitions 241: -2 Bound for (chained) transitions 242: -1 Bound for (chained) transitions 243: -1 Bound for (chained) transitions 244: -1 Bound for (chained) transitions 245: 0 Bound for (chained) transitions 246: 0 Bound for (chained) transitions 247: 0 Bound for (chained) transitions 248: 1 Bound for (chained) transitions 249: 1 * Removed transitions 83, 85, 86, 91, 92, 93, 94, 95, 96, 97, 98, 99, 100, 101, 102, 103, 105, 106, 112, 268, 270, 271 using the following rank functions: - Rank function 1: RF for loc. 77: -4+5*n2_0-5*nj_0 RF for loc. 78: -4+5*n2_0-5*nj_0 RF for loc. 79: -4+5*n2_0-5*nj_0 RF for loc. 80: -4+5*n2_0-5*nj_0 RF for loc. 81: -4+5*n2_0-5*nj_0 RF for loc. 82: -4+5*n2_0-5*nj_0 RF for loc. 83: -4+5*n2_0-5*nj_0 RF for loc. 84: -4+5*n2_0-5*nj_0 RF for loc. 86: -1+5*n2_0-5*nj_0 RF for loc. 111: -4+5*n2_0-5*nj_0 RF for loc. 115: -4+5*n2_0-5*nj_0 RF for loc. 171: 5*n2_0-5*nj_0 Bound for (chained) transitions 112: 4 - Rank function 2: RF for loc. 77: 0 RF for loc. 78: 0 RF for loc. 79: 0 RF for loc. 80: 0 RF for loc. 81: 0 RF for loc. 82: 0 RF for loc. 83: 0 RF for loc. 84: 0 RF for loc. 86: -2 RF for loc. 111: 0 RF for loc. 115: 0 RF for loc. 171: -1 Bound for (chained) transitions 101, 268: 0 Bound for (chained) transitions 270: -1 Bound for (chained) transitions 271: -1 - Rank function 3: RF for loc. 77: 9+10*n2_0-10*ni1_0 RF for loc. 78: 7+10*n2_0-10*ni1_0 RF for loc. 79: 10*n2_0-10*ni1_0 RF for loc. 80: 10*n2_0-10*ni1_0 RF for loc. 81: 10*n2_0-10*ni1_0 RF for loc. 82: 10*n2_0-10*ni1_0 RF for loc. 83: 10*n2_0-10*ni1_0 RF for loc. 84: 10*n2_0-10*ni1_0 RF for loc. 111: 8+10*n2_0-10*ni1_0 RF for loc. 115: 10*n2_0-10*ni1_0 Bound for (chained) transitions 102: 27 - Rank function 4: RF for loc. 77: -1+7*n2_0-7*ni2_0 RF for loc. 78: -3+7*n2_0-7*ni2_0 RF for loc. 79: -4+7*n2_0-7*ni2_0 RF for loc. 80: 2+7*n2_0-7*ni2_0 RF for loc. 81: -3+7*n2_0-7*ni2_0 RF for loc. 82: -2+7*n2_0-7*ni2_0 RF for loc. 83: -1+7*n2_0-7*ni2_0 RF for loc. 84: 7*n2_0-7*ni2_0 RF for loc. 111: -2+7*n2_0-7*ni2_0 RF for loc. 115: 1+7*n2_0-7*ni2_0 Bound for (chained) transitions 100: 7 - Rank function 5: RF for loc. 77: -2 RF for loc. 78: -4 RF for loc. 79: 2 RF for loc. 80: 1 RF for loc. 81: 3 RF for loc. 82: 4 RF for loc. 83: 5 RF for loc. 84: -1 RF for loc. 111: -3 RF for loc. 115: 0 Bound for (chained) transitions 83: -2 Bound for (chained) transitions 85: -3 Bound for (chained) transitions 86: -3 Bound for (chained) transitions 91: 2 Bound for (chained) transitions 92: 3 Bound for (chained) transitions 93: 4 Bound for (chained) transitions 94: 4 Bound for (chained) transitions 95: 4 Bound for (chained) transitions 96: 5 Bound for (chained) transitions 97: 5 Bound for (chained) transitions 98: 5 Bound for (chained) transitions 99: -1 Bound for (chained) transitions 103: 1 Bound for (chained) transitions 105: 0 Bound for (chained) transitions 106: 0 * Removed transitions 121, 122, 123, 124, 125, 126, 127, 128, 129, 130, 139, 140, 142, 223, 225, 226, 232, 234, 235, 254, 256, 257 using the following rank functions: - Rank function 1: RF for loc. 89: 4*n2_0-4*ni_0 RF for loc. 90: 4*n2_0-4*ni_0 RF for loc. 91: 4*n2_0-4*ni_0 RF for loc. 92: 4*n2_0-4*ni_0 RF for loc. 93: 4*n2_0-4*ni_0 RF for loc. 94: 4*n2_0-4*ni_0 RF for loc. 95: 4*n2_0-4*ni_0 RF for loc. 96: 4*n2_0-4*ni_0 RF for loc. 98: 1+4*n2_0-4*ni_0 RF for loc. 159: 2+4*n2_0-4*ni_0 RF for loc. 163: 4*n2_0-4*ni_0 RF for loc. 167: 4*n2_0-4*ni_0 Bound for (chained) transitions 142: 5 - Rank function 2: RF for loc. 89: 11*n2_0-11*nj1_0 RF for loc. 90: 11*n2_0-11*nj1_0 RF for loc. 91: 11*n2_0-11*nj1_0 RF for loc. 92: 11*n2_0-11*nj1_0 RF for loc. 93: 11*n2_0-11*nj1_0 RF for loc. 94: 11*n2_0-11*nj1_0 RF for loc. 95: 10+11*n2_0-11*nj1_0 RF for loc. 96: 8+11*n2_0-11*nj1_0 RF for loc. 98: 6+11*n2_0-11*nj1_0 RF for loc. 159: 7+11*n2_0-11*nj1_0 RF for loc. 163: 9+11*n2_0-11*nj1_0 RF for loc. 167: 11*n2_0-11*nj1_0 Bound for (chained) transitions 140: 30 - Rank function 3: RF for loc. 89: -3+6*n2_0-6*nj2_0 RF for loc. 90: 2+6*n2_0-6*nj2_0 RF for loc. 91: -3+6*n2_0-6*nj2_0 RF for loc. 92: -2+6*n2_0-6*nj2_0 RF for loc. 93: -1+6*n2_0-6*nj2_0 RF for loc. 94: 6*n2_0-6*nj2_0 RF for loc. 95: -1+6*n2_0-6*nj2_0 RF for loc. 96: -3+6*n2_0-6*nj2_0 RF for loc. 98: -5+6*n2_0-6*nj2_0 RF for loc. 159: -4+6*n2_0-6*nj2_0 RF for loc. 163: -2+6*n2_0-6*nj2_0 RF for loc. 167: 1+6*n2_0-6*nj2_0 Bound for (chained) transitions 130: 6 - Rank function 4: RF for loc. 89: 2 RF for loc. 90: 1 RF for loc. 91: 3 RF for loc. 92: 4 RF for loc. 93: 5 RF for loc. 94: -1 RF for loc. 95: -2 RF for loc. 96: -4 RF for loc. 98: -6 RF for loc. 159: -5 RF for loc. 163: -3 RF for loc. 167: 0 Bound for (chained) transitions 121: 2 Bound for (chained) transitions 122: 3 Bound for (chained) transitions 123: 4 Bound for (chained) transitions 124: 4 Bound for (chained) transitions 125: 4 Bound for (chained) transitions 126: 5 Bound for (chained) transitions 127: 5 Bound for (chained) transitions 128: 5 Bound for (chained) transitions 129: -1 Bound for (chained) transitions 139, 223: -4 Bound for (chained) transitions 225: -5 Bound for (chained) transitions 226: -5 Bound for (chained) transitions 232: -2 Bound for (chained) transitions 234: -3 Bound for (chained) transitions 235: -3 Bound for (chained) transitions 254: 1 Bound for (chained) transitions 256: 0 Bound for (chained) transitions 257: 0 * Removed transitions 151, 152, 153, 154, 155, 156, 157, 158, 159, 160, 170, 207, 209, 210, 215, 217, 218 using the following rank functions: - Rank function 1: RF for loc. 99: 8*n2_0-8*ni_0 RF for loc. 100: 8*n2_0-8*ni_0 RF for loc. 101: 8*n2_0-8*ni_0 RF for loc. 102: 8*n2_0-8*ni_0 RF for loc. 103: 8*n2_0-8*ni_0 RF for loc. 104: 8*n2_0-8*ni_0 RF for loc. 106: 6+8*n2_0-8*ni_0 RF for loc. 151: 7+8*n2_0-8*ni_0 RF for loc. 155: 8*n2_0-8*ni_0 Bound for (chained) transitions 170: 14 - Rank function 2: RF for loc. 99: -6+9*n2_0-9*nj_0 RF for loc. 100: 2+9*n2_0-9*nj_0 RF for loc. 101: -5+9*n2_0-9*nj_0 RF for loc. 102: -4+9*n2_0-9*nj_0 RF for loc. 103: -3+9*n2_0-9*nj_0 RF for loc. 104: 9*n2_0-9*nj_0 RF for loc. 106: -2+9*n2_0-9*nj_0 RF for loc. 151: -1+9*n2_0-9*nj_0 RF for loc. 155: 1+9*n2_0-9*nj_0 Bound for (chained) transitions 160: 9 - Rank function 3: RF for loc. 99: 2 RF for loc. 100: 1 RF for loc. 101: 3 RF for loc. 102: 4 RF for loc. 103: 5 RF for loc. 104: -1 RF for loc. 106: -3 RF for loc. 151: -2 RF for loc. 155: 0 Bound for (chained) transitions 151: 2 Bound for (chained) transitions 152: 3 Bound for (chained) transitions 153: 3 Bound for (chained) transitions 154: 4 Bound for (chained) transitions 155: 4 Bound for (chained) transitions 156: 5 Bound for (chained) transitions 157: 5 Bound for (chained) transitions 158: 5 Bound for (chained) transitions 159, 207: -1 Bound for (chained) transitions 209: -2 Bound for (chained) transitions 210: -2 Bound for (chained) transitions 215: 1 Bound for (chained) transitions 217: 0 Bound for (chained) transitions 218: 0 * Removed transitions 179, 180, 182, 191, 193, 194, 199, 201, 202 using the following rank functions: - Rank function 1: RF for loc. 107: 4*n2_0-4*ni_0 RF for loc. 109: 4*n2_0-4*ni_0 RF for loc. 110: 2+4*n2_0-4*ni_0 RF for loc. 143: 3+4*n2_0-4*ni_0 RF for loc. 147: 4*n2_0-4*ni_0 Bound for (chained) transitions 182: 6 - Rank function 2: RF for loc. 107: -1+3*n2_0-3*nj_0 RF for loc. 109: 1+3*n2_0-3*nj_0 RF for loc. 110: -3+3*n2_0-3*nj_0 RF for loc. 143: -2+3*n2_0-3*nj_0 RF for loc. 147: 3*n2_0-3*nj_0 Bound for (chained) transitions 180: 2 - Rank function 3: RF for loc. 107: -1 RF for loc. 109: 1 RF for loc. 110: -3 RF for loc. 143: -2 RF for loc. 147: 0 Bound for (chained) transitions 179, 191: -1 Bound for (chained) transitions 193: -2 Bound for (chained) transitions 194: -2 Bound for (chained) transitions 199: 1 Bound for (chained) transitions 201: 0 Bound for (chained) transitions 202: 0 Errors: