YES Termination proof succeeded Initially, performed program simplifications using lexicographic rank functions: * Removed transitions 329, 331, 332, 335, 336, 337, 338, 339, 340, 341, 342, 343, 344 using the following rank functions: - Rank function 1: RF for loc. 273: -3+7*a_1162_0 RF for loc. 274: -4+7*a_1162_0 RF for loc. 275: 2+7*a_1236_0 RF for loc. 276: 1+7*a_1236_0 RF for loc. 277: 7*a_1236_0 RF for loc. 278: -1+7*a_1236_0 RF for loc. 296: -2+7*a_1162_0 Bound for (chained) transitions 331: -2 - Rank function 2: RF for loc. 273: -3+7*a_1162_0 RF for loc. 274: -4+7*a_1162_0 RF for loc. 275: 2+7*a_1236_0 RF for loc. 276: 1+7*a_1236_0 RF for loc. 277: 7*a_1236_0 RF for loc. 278: -1+7*a_1236_0 RF for loc. 296: -2+7*a_1162_0 Bound for (chained) transitions 332: -2 - Rank function 3: RF for loc. 273: 4 RF for loc. 274: 3 RF for loc. 275: 2 RF for loc. 276: 1 RF for loc. 277: 0 RF for loc. 278: -1 RF for loc. 296: -2 Bound for (chained) transitions 329, 344: -1 Bound for (chained) transitions 335: 4 Bound for (chained) transitions 336: 4 Bound for (chained) transitions 337: 3 Bound for (chained) transitions 338: 2 Bound for (chained) transitions 339: 2 Bound for (chained) transitions 340: 1 Bound for (chained) transitions 341: 1 Bound for (chained) transitions 342: 0 Bound for (chained) transitions 343: 0 * Removed transitions 346, 348, 349, 352, 353, 354, 355, 356, 357, 358, 359, 360, 361 using the following rank functions: - Rank function 1: RF for loc. 220: -3+7*a_924_0 RF for loc. 221: -4+7*a_924_0 RF for loc. 222: 2+7*a_947_0 RF for loc. 223: 1+7*a_947_0 RF for loc. 224: 7*a_947_0 RF for loc. 225: -1+7*a_947_0 RF for loc. 300: -2+7*a_924_0 Bound for (chained) transitions 348: -2 - Rank function 2: RF for loc. 220: -3+7*a_924_0 RF for loc. 221: -4+7*a_924_0 RF for loc. 222: 2+7*a_947_0 RF for loc. 223: 1+7*a_947_0 RF for loc. 224: 7*a_947_0 RF for loc. 225: -1+7*a_947_0 RF for loc. 300: -2+7*a_924_0 Bound for (chained) transitions 349: -2 - Rank function 3: RF for loc. 220: 4 RF for loc. 221: 3 RF for loc. 222: 2 RF for loc. 223: 1 RF for loc. 224: 0 RF for loc. 225: -1 RF for loc. 300: -2 Bound for (chained) transitions 346, 361: -1 Bound for (chained) transitions 352: 4 Bound for (chained) transitions 353: 4 Bound for (chained) transitions 354: 3 Bound for (chained) transitions 355: 2 Bound for (chained) transitions 356: 2 Bound for (chained) transitions 357: 1 Bound for (chained) transitions 358: 1 Bound for (chained) transitions 359: 0 Bound for (chained) transitions 360: 0 * Removed transitions 223, 227, 228, 233, 234, 235, 236, 237, 238, 239, 240, 241, 242, 243, 244, 245, 246, 247, 248, 249, 250, 251, 252, 253, 254, 255, 256, 257, 259, 262, 263, 268, 269, 270, 271, 272, 273, 274, 275, 276, 277, 278, 279, 280, 281, 282, 283, 284, 285, 286, 287, 288 using the following rank functions: - Rank function 1: RF for loc. 226: -1+16*a_176_0 RF for loc. 227: -2+16*a_176_0 RF for loc. 228: -1+16*a_176_0 RF for loc. 229: -3+16*a_176_0 RF for loc. 230: 12+16*a_263_0 RF for loc. 231: 12+16*a_263_0 RF for loc. 232: 11+16*a_263_0 RF for loc. 233: 10+16*a_263_0 RF for loc. 234: -1+16*a_176_0 RF for loc. 235: -1+16*a_176_0 RF for loc. 236: -1+16*a_176_0 RF for loc. 237: -1+16*a_239_0 RF for loc. 238: -1+16*a_239_0 RF for loc. 239: -1+16*a_239_0 RF for loc. 240: -1+16*a_239_0 RF for loc. 241: -1+16*a_239_0 RF for loc. 242: 9+16*a_176_0 RF for loc. 243: -2+16*a_176_0 RF for loc. 244: 7+16*a_176_0 RF for loc. 245: -3+16*a_176_0 RF for loc. 246: 12+16*a_862_0 RF for loc. 247: 11+16*a_862_0 RF for loc. 248: 10+16*a_862_0 RF for loc. 249: 6+16*a_176_0 RF for loc. 250: 5+16*a_176_0 RF for loc. 251: 4+16*a_176_0 RF for loc. 252: 3+16*a_176_0 RF for loc. 253: 2+16*a_176_0 RF for loc. 254: 1+16*a_176_0 RF for loc. 255: 16*a_176_0 RF for loc. 280: -1+16*a_176_0 RF for loc. 284: 8+16*a_176_0 Bound for (chained) transitions 262: 8 - Rank function 2: RF for loc. 226: -1+a_176_0-a_862_0-15*len_161_0+15*len_861_0 RF for loc. 227: -2+a_176_0-a_862_0-15*len_161_0+15*len_861_0 RF for loc. 228: -1+a_176_0-a_862_0-15*len_161_0+15*len_861_0 RF for loc. 229: -3+a_176_0-a_862_0-15*len_161_0+15*len_861_0 RF for loc. 230: 12+a_263_0-a_862_0-15*len_262_0+15*len_861_0 RF for loc. 231: 11+a_263_0-a_862_0-15*len_262_0+15*len_861_0 RF for loc. 232: 10+a_263_0-a_862_0-15*len_262_0+15*len_861_0 RF for loc. 233: 9+a_263_0-a_862_0-15*len_262_0+15*len_861_0 RF for loc. 234: -1+a_176_0-a_862_0-15*len_161_0+15*len_861_0 RF for loc. 235: -1+a_176_0-a_862_0-15*len_161_0+15*len_861_0 RF for loc. 236: -1+a_176_0-a_862_0-15*len_161_0+15*len_861_0 RF for loc. 237: -1+a_239_0-a_862_0-15*len_238_0+15*len_861_0 RF for loc. 238: -1+a_239_0-a_862_0-15*len_238_0+15*len_861_0 RF for loc. 239: -1+a_239_0-a_862_0-15*len_238_0+15*len_861_0 RF for loc. 240: -1+a_239_0-a_862_0-15*len_238_0+15*len_861_0 RF for loc. 241: -1+a_239_0-a_862_0-15*len_238_0+15*len_861_0 RF for loc. 242: 8+a_176_0-a_862_0-15*len_161_0+15*len_861_0 RF for loc. 243: 13 RF for loc. 244: 6+a_176_0-a_862_0-15*len_161_0+15*len_861_0 RF for loc. 245: 12 RF for loc. 246: 11 RF for loc. 247: 10 RF for loc. 248: 9 RF for loc. 249: 5+a_176_0-a_862_0-15*len_161_0+15*len_861_0 RF for loc. 250: 4+a_176_0-a_862_0-15*len_161_0+15*len_861_0 RF for loc. 251: 3+a_176_0-a_862_0-15*len_161_0+15*len_861_0 RF for loc. 252: 2+a_176_0-a_862_0-15*len_161_0+15*len_861_0 RF for loc. 253: 2+a_176_0-a_862_0-15*len_161_0+15*len_861_0 RF for loc. 254: 1+a_176_0-a_862_0-15*len_161_0+15*len_861_0 RF for loc. 255: a_176_0-a_862_0-15*len_161_0+15*len_861_0 RF for loc. 280: -1+a_176_0-a_862_0-15*len_161_0+15*len_861_0 RF for loc. 284: 7+a_176_0-a_862_0-15*len_161_0+15*len_861_0 Bound for (chained) transitions 268: 13 Bound for (chained) transitions 269: 13 Bound for (chained) transitions 270: 12 Bound for (chained) transitions 271: 11 Bound for (chained) transitions 272: 11 Bound for (chained) transitions 273: 10 Bound for (chained) transitions 274: 10 - Rank function 3: RF for loc. 226: -1+17*i_27_0 RF for loc. 227: -3+17*i_27_0 RF for loc. 228: -3+17*i_27_0 RF for loc. 229: -4+17*i_27_0 RF for loc. 230: -5+17*i_27_0 RF for loc. 231: -6+17*i_27_0 RF for loc. 232: -6+17*i_27_0 RF for loc. 233: -7+17*i_27_0 RF for loc. 234: -4+17*i_27_0 RF for loc. 235: -5+17*i_27_0 RF for loc. 236: -5+17*i_27_0 RF for loc. 237: 3+17*i_27_0 RF for loc. 238: 2+17*i_27_0 RF for loc. 239: 2+17*i_27_0 RF for loc. 240: 1+17*i_27_0 RF for loc. 241: 17*i_27_0 RF for loc. 242: -8+17*i_27_0 RF for loc. 244: -10+17*i_27_0 RF for loc. 248: 17*i_27_0 RF for loc. 249: -11+17*i_27_0 RF for loc. 250: -12+17*i_27_0 RF for loc. 251: -13+17*i_27_0 RF for loc. 252: 3+17*i_27_0 RF for loc. 253: 2+17*i_27_0 RF for loc. 254: 1+17*i_27_0 RF for loc. 255: 17*i_27_0 RF for loc. 280: -2+17*i_27_0 RF for loc. 284: -9+17*i_27_0 Bound for (chained) transitions 275: 17 - Rank function 4: RF for loc. 226: -1+18*i_27_0 RF for loc. 227: -3+18*i_27_0 RF for loc. 228: -3+18*i_27_0 RF for loc. 229: -4+18*i_27_0 RF for loc. 230: -5+18*i_27_0 RF for loc. 231: -6+18*i_27_0 RF for loc. 232: -7+18*i_27_0 RF for loc. 233: -8+18*i_27_0 RF for loc. 234: -4+18*i_27_0 RF for loc. 235: -5+18*i_27_0 RF for loc. 236: -6+18*i_27_0 RF for loc. 237: 11+18*i_27_0 RF for loc. 238: 10+18*i_27_0 RF for loc. 239: 10+18*i_27_0 RF for loc. 240: 7+18*i_27_0 RF for loc. 241: -1+18*i_27_0 RF for loc. 242: -9+18*i_27_0 RF for loc. 244: -11+18*i_27_0 RF for loc. 249: -12+18*i_27_0 RF for loc. 250: -13+18*i_27_0 RF for loc. 251: -14+18*i_27_0 RF for loc. 252: 3+18*i_27_0 RF for loc. 253: 2+18*i_27_0 RF for loc. 254: 1+18*i_27_0 RF for loc. 255: 18*i_27_0 RF for loc. 280: -2+18*i_27_0 RF for loc. 284: -10+18*i_27_0 Bound for (chained) transitions 235: 14 - Rank function 5: RF for loc. 226: -1-11*i_197_0+11*i_27_0 RF for loc. 227: -3-11*i_197_0+11*i_27_0 RF for loc. 228: -3-11*i_197_0+11*i_27_0 RF for loc. 229: -4-11*i_197_0+11*i_27_0 RF for loc. 230: 2 RF for loc. 231: 1 RF for loc. 232: 0 RF for loc. 233: -1 RF for loc. 234: -4-11*i_197_0+11*i_27_0 RF for loc. 235: -5-11*i_197_0+11*i_27_0 RF for loc. 236: -6-11*i_197_0+11*i_27_0 RF for loc. 237: 4-11*i_197_0+11*i_27_0 RF for loc. 238: 3-11*i_197_0+11*i_27_0 RF for loc. 239: 2-11*i_197_0+11*i_27_0 RF for loc. 240: 1-11*i_197_0+11*i_27_0 RF for loc. 241: -11*i_197_0+11*i_27_0 RF for loc. 242: -2 RF for loc. 244: -4 RF for loc. 249: -5 RF for loc. 250: -6 RF for loc. 251: -7 RF for loc. 252: 3-11*i_197_0+11*i_27_0 RF for loc. 253: 2-11*i_197_0+11*i_27_0 RF for loc. 254: 1-11*i_197_0+11*i_27_0 RF for loc. 255: -11*i_197_0+11*i_27_0 RF for loc. 280: -2-11*i_197_0+11*i_27_0 RF for loc. 284: -3 Bound for (chained) transitions 236: 2 Bound for (chained) transitions 237: 2 Bound for (chained) transitions 238: 1 Bound for (chained) transitions 239: 1 Bound for (chained) transitions 240: 0 Bound for (chained) transitions 259: -2 Bound for (chained) transitions 263: -3 Bound for (chained) transitions 276: -4 Bound for (chained) transitions 277: -4 Bound for (chained) transitions 278: -5 Bound for (chained) transitions 279: -6 Bound for (chained) transitions 280: -6 Bound for (chained) transitions 281: -7 - Rank function 6: RF for loc. 226: -8+17*i_27_0 RF for loc. 227: -10+17*i_27_0 RF for loc. 228: -10+17*i_27_0 RF for loc. 229: -11+17*i_27_0 RF for loc. 232: 1 RF for loc. 233: 0 RF for loc. 234: -11+17*i_27_0 RF for loc. 235: -12+17*i_27_0 RF for loc. 236: -13+17*i_27_0 RF for loc. 237: 3+17*i_27_0 RF for loc. 238: 2+17*i_27_0 RF for loc. 239: 1+17*i_27_0 RF for loc. 240: 17*i_27_0 RF for loc. 241: 17*i_27_0 RF for loc. 242: -i_27_0 RF for loc. 252: 3+17*i_27_0 RF for loc. 253: 2+17*i_27_0 RF for loc. 254: 1+17*i_27_0 RF for loc. 255: 17*i_27_0 RF for loc. 280: -9+17*i_27_0 Bound for (chained) transitions 241: 1 Bound for (chained) transitions 245: 6 - Rank function 7: RF for loc. 226: 0 RF for loc. 227: -2 RF for loc. 228: -2 RF for loc. 229: -3 RF for loc. 233: result_dot_nondet_sdv_special_RETURN_VALUE_13_0 RF for loc. 234: -3 RF for loc. 235: 7 RF for loc. 236: 6 RF for loc. 237: 5 RF for loc. 238: 4 RF for loc. 239: 3 RF for loc. 240: 2 RF for loc. 241: 1 RF for loc. 242: 0 RF for loc. 252: 4 RF for loc. 253: 3 RF for loc. 254: 2 RF for loc. 255: 1 RF for loc. 280: -1 Bound for (chained) transitions 223: 0 Bound for (chained) transitions 227: -1 Bound for (chained) transitions 228: -1 Bound for (chained) transitions 233: -2 Bound for (chained) transitions 234: -2 Bound for (chained) transitions 242: 2 Bound for (chained) transitions 243: -2 Bound for (chained) transitions 244: -2 Bound for (chained) transitions 246: 7 Bound for (chained) transitions 247: 7 Bound for (chained) transitions 248: 6 Bound for (chained) transitions 249: 5 Bound for (chained) transitions 250: 5 Bound for (chained) transitions 251: 4 Bound for (chained) transitions 252: 4 Bound for (chained) transitions 253: 3 Bound for (chained) transitions 254: 3 Bound for (chained) transitions 255: 2 Bound for (chained) transitions 256: 2 Bound for (chained) transitions 257: 1 Bound for (chained) transitions 282: 4 Bound for (chained) transitions 283: 4 Bound for (chained) transitions 284: 3 Bound for (chained) transitions 285: 3 Bound for (chained) transitions 286: 2 Bound for (chained) transitions 287: 2 Bound for (chained) transitions 288: 1 * Removed transitions 309, 313, 314, 317, 318, 319, 320, 321, 322, 323, 324, 325, 326, 327 using the following rank functions: - Rank function 1: RF for loc. 265: -3+8*i_27_0 RF for loc. 266: -4+8*i_27_0 RF for loc. 267: -5+8*i_27_0 RF for loc. 268: -6+8*i_27_0 RF for loc. 269: 1+8*i_27_0 RF for loc. 270: 8*i_27_0 RF for loc. 271: -1+8*i_27_0 RF for loc. 292: -2+8*i_27_0 Bound for (chained) transitions 319: 4 - Rank function 2: RF for loc. 265: -3 RF for loc. 266: -4 RF for loc. 267: 3 RF for loc. 268: 2 RF for loc. 269: 1 RF for loc. 270: 0 RF for loc. 271: -1 RF for loc. 292: -2 Bound for (chained) transitions 309, 327: -1 Bound for (chained) transitions 313: -2 Bound for (chained) transitions 314: -2 Bound for (chained) transitions 317: -3 Bound for (chained) transitions 318: -3 Bound for (chained) transitions 320: 3 Bound for (chained) transitions 321: 3 Bound for (chained) transitions 322: 2 Bound for (chained) transitions 323: 1 Bound for (chained) transitions 324: 1 Bound for (chained) transitions 325: 0 Bound for (chained) transitions 326: 0 * Removed transitions 362, 365, 366 using the following rank functions: - Rank function 1: RF for loc. 279: 1-2*i_30_0+2*length_29_0 RF for loc. 304: -2*i_30_0+2*length_29_0 Bound for (chained) transitions 365: 2 - Rank function 2: RF for loc. 279: 1-2*i_30_0+2*length_29_0 RF for loc. 304: -2*i_30_0+2*length_29_0 Bound for (chained) transitions 366: 2 - Rank function 3: RF for loc. 279: 0 RF for loc. 304: -1 Bound for (chained) transitions 362: 0 * Removed transitions 289, 294, 295, 298, 299, 300, 301, 302, 303, 304, 305, 306, 307, 308 using the following rank functions: - Rank function 1: RF for loc. 257: -2+7*i_27_0 RF for loc. 258: -3+7*i_27_0 RF for loc. 259: -4+7*i_27_0 RF for loc. 260: -5+7*i_27_0 RF for loc. 261: 1+7*i_27_0 RF for loc. 262: 7*i_27_0 RF for loc. 263: -1+7*i_27_0 RF for loc. 288: -1+7*i_27_0 Bound for (chained) transitions 300: 4 - Rank function 2: RF for loc. 257: -3 RF for loc. 258: -4 RF for loc. 259: 3 RF for loc. 260: 2 RF for loc. 261: 1 RF for loc. 262: 0 RF for loc. 263: -1 RF for loc. 288: -2 Bound for (chained) transitions 289, 308: -1 Bound for (chained) transitions 295: -2 Bound for (chained) transitions 298: -3 Bound for (chained) transitions 299: -3 Bound for (chained) transitions 301: 3 Bound for (chained) transitions 302: 3 Bound for (chained) transitions 303: 2 Bound for (chained) transitions 304: 1 Bound for (chained) transitions 305: 1 Bound for (chained) transitions 306: 0 Bound for (chained) transitions 307: 0 - Rank function 3: RF for loc. 257: -1 RF for loc. 288: 0 Bound for (chained) transitions 294: 0 Errors: