YES Termination proof succeeded Initially, performed program simplifications using lexicographic rank functions: * Removed transitions 239, 241, 242, 247, 248, 250, 251 using the following rank functions: - Rank function 1: RF for loc. 66: -3*arg2 RF for loc. 106: 1-3*arg2 RF for loc. 110: -3*arg2 Bound for (chained) transitions 241: -17 - Rank function 2: RF for loc. 66: -3*arg2 RF for loc. 106: 1-3*arg2 RF for loc. 110: -3*arg2 Bound for (chained) transitions 242: -17 - Rank function 3: RF for loc. 66: 0 RF for loc. 106: -arg1P RF for loc. 110: 0 Bound for (chained) transitions 239, 247: 0 - Rank function 4: RF for loc. 66: 1-arg3-arg4 RF for loc. 110: -arg3-arg4 Bound for (chained) transitions 250: -12 Bound for (chained) transitions 251: -12 - Rank function 5: RF for loc. 66: 0 RF for loc. 110: -1 Bound for (chained) transitions 248: 0 * Removed transitions 348, 355, 356, 357, 358, 359, 367 using the following rank functions: - Rank function 1: RF for loc. 77: -1+2*arg2 RF for loc. 78: arg3+2*arg6 RF for loc. 142: -2+2*arg2 Bound for (chained) transitions 355: 4 Bound for (chained) transitions 356: 4 Bound for (chained) transitions 357: 4 Bound for (chained) transitions 358: 4 Bound for (chained) transitions 359: 4 Bound for (chained) transitions 367: 0 - Rank function 2: RF for loc. 77: 0 RF for loc. 142: -1 Bound for (chained) transitions 348: 0 * Removed transitions 340, 342, 343 using the following rank functions: - Rank function 1: RF for loc. 76: 1+arg1+arg2 RF for loc. 138: arg1+arg2 Bound for (chained) transitions 342: 2 Bound for (chained) transitions 343: 2 - Rank function 2: RF for loc. 76: 1 RF for loc. 138: 0 Bound for (chained) transitions 340: 1 * Removed transitions 310, 312, 313 using the following rank functions: - Rank function 1: RF for loc. 75: 1+2*arg1 RF for loc. 126: 2*arg1 Bound for (chained) transitions 312: 2 Bound for (chained) transitions 313: 2 - Rank function 2: RF for loc. 75: 1 RF for loc. 126: 0 Bound for (chained) transitions 310: 1 * Removed transitions 284, 288, 289, 294, 295, 296, 297, 298, 300, 301, 303, 305, 306, 307, 308, 309 using the following rank functions: - Rank function 1: RF for loc. 70: 5-6*arg3+6*arg4 RF for loc. 71: 3+6*arg1-6*arg2 RF for loc. 72: 2+6*arg1-6*arg2 RF for loc. 73: 1+6*arg1-6*arg2 RF for loc. 74: 6*arg2-6*arg3 RF for loc. 122: 4-6*arg3+6*arg4 Bound for (chained) transitions 288: 10 Bound for (chained) transitions 289: 10 Bound for (chained) transitions 294: 9 Bound for (chained) transitions 295: 9 Bound for (chained) transitions 296: 9 Bound for (chained) transitions 297: 9 Bound for (chained) transitions 298: 9 Bound for (chained) transitions 300: 8 Bound for (chained) transitions 301: 8 Bound for (chained) transitions 305: 7 Bound for (chained) transitions 306: 7 Bound for (chained) transitions 307: 7 - Rank function 2: RF for loc. 70: 0 RF for loc. 72: arg1 RF for loc. 73: arg6 RF for loc. 74: arg1 RF for loc. 122: -1 Bound for (chained) transitions 303: 1 Bound for (chained) transitions 308: 3 Bound for (chained) transitions 309: 5 - Rank function 3: RF for loc. 70: 1 RF for loc. 122: 0 Bound for (chained) transitions 284: 1 * Removed transitions 318, 321, 322, 330, 331 using the following rank functions: - Rank function 1: RF for loc. 89: -1+2*arg2 RF for loc. 90: 2*arg6 RF for loc. 130: -2+2*arg2 Bound for (chained) transitions 321: 4 Bound for (chained) transitions 322: 4 Bound for (chained) transitions 330: 0 - Rank function 2: RF for loc. 89: 0 RF for loc. 90: 1 RF for loc. 130: -1 Bound for (chained) transitions 331: 1 - Rank function 3: RF for loc. 89: 0 RF for loc. 130: -1 Bound for (chained) transitions 318: 0 * Removed transitions 270, 274, 275 using the following rank functions: - Rank function 1: RF for loc. 88: 1-2*arg3+2*arg4 RF for loc. 118: -2*arg3+2*arg4 Bound for (chained) transitions 274: 2 Bound for (chained) transitions 275: 2 - Rank function 2: RF for loc. 88: 0 RF for loc. 118: -1 Bound for (chained) transitions 270: 0 * Removed transitions 254, 258, 259, 268, 269 using the following rank functions: - Rank function 1: RF for loc. 68: -1+2*arg3 RF for loc. 69: 2*arg10 RF for loc. 114: -2+2*arg3 Bound for (chained) transitions 258: 4 Bound for (chained) transitions 259: 4 Bound for (chained) transitions 268: 0 Bound for (chained) transitions 269: 0 - Rank function 2: RF for loc. 68: 1 RF for loc. 114: 0 Bound for (chained) transitions 254: 1 * Removed transitions 332, 334, 335 using the following rank functions: - Rank function 1: RF for loc. 67: 1+2*arg1 RF for loc. 134: 2*arg1 Bound for (chained) transitions 334: 2 Bound for (chained) transitions 335: 2 - Rank function 2: RF for loc. 67: 1 RF for loc. 134: 0 Bound for (chained) transitions 332: 1 * Removed transitions 613, 616, 617, 618, 624, 625, 626, 627, 629, 630, 631 using the following rank functions: - Rank function 1: RF for loc. 83: 3-4*arg4+4*arg5 RF for loc. 84: 1-4*arg3+4*arg6 RF for loc. 85: -4*arg4+4*arg7 RF for loc. 178: 2-4*arg4+4*arg5 RF for loc. 182: -4*arg4+4*arg7 Bound for (chained) transitions 616: 6 Bound for (chained) transitions 617: 6 - Rank function 2: RF for loc. 83: 3-4*arg4+4*arg5 RF for loc. 84: 1-4*arg3+4*arg6 RF for loc. 85: -4*arg4+4*arg7 RF for loc. 178: 2-4*arg4+4*arg5 RF for loc. 182: -4*arg4+4*arg7 Bound for (chained) transitions 618: 6 - Rank function 3: RF for loc. 83: -1 RF for loc. 84: 1 RF for loc. 85: 0 RF for loc. 178: -2 RF for loc. 182: 0 Bound for (chained) transitions 613: -1 Bound for (chained) transitions 624: 1 Bound for (chained) transitions 625: 1 Bound for (chained) transitions 626: 1 Bound for (chained) transitions 629: 0 - Rank function 4: RF for loc. 85: 1+arg10+arg11-2*arg6 RF for loc. 182: arg10+arg11-2*arg6 Bound for (chained) transitions 630: 2 Bound for (chained) transitions 631: 2 - Rank function 5: RF for loc. 85: 0 RF for loc. 182: -1 Bound for (chained) transitions 627: 0 * Removed transitions 604, 606, 607 using the following rank functions: - Rank function 1: RF for loc. 93: 2+arg1+2*arg2 RF for loc. 174: arg1+2*arg2 Bound for (chained) transitions 606: 5 Bound for (chained) transitions 607: 5 - Rank function 2: RF for loc. 93: 1 RF for loc. 174: 0 Bound for (chained) transitions 604: 1 * Removed transitions 368, 372, 373 using the following rank functions: - Rank function 1: RF for loc. 87: 1+arg4+arg5 RF for loc. 146: arg4+arg5 Bound for (chained) transitions 372: 4 Bound for (chained) transitions 373: 4 - Rank function 2: RF for loc. 87: 0 RF for loc. 146: -1 Bound for (chained) transitions 368: 0 * Removed transitions 583, 600, 601 using the following rank functions: - Rank function 1: RF for loc. 97: 2+4*arg7 RF for loc. 170: 4*arg7 Bound for (chained) transitions 600: 4 Bound for (chained) transitions 601: 4 - Rank function 2: RF for loc. 97: 0 RF for loc. 170: -1 Bound for (chained) transitions 583: 0 * Removed transitions 513, 546, 547 using the following rank functions: - Rank function 1: RF for loc. 94: 1+arg5+arg6 RF for loc. 166: arg5+arg6 Bound for (chained) transitions 546: 4 Bound for (chained) transitions 547: 4 - Rank function 2: RF for loc. 94: 0 RF for loc. 166: -1 Bound for (chained) transitions 513: 0 * Removed transitions 492, 509, 510 using the following rank functions: - Rank function 1: RF for loc. 96: 2+arg6+arg7 RF for loc. 162: arg6+arg7 Bound for (chained) transitions 509: 4 Bound for (chained) transitions 510: 4 - Rank function 2: RF for loc. 96: 0 RF for loc. 162: -1 Bound for (chained) transitions 492: 0 * Removed transitions 422, 455, 456 using the following rank functions: - Rank function 1: RF for loc. 95: 2+arg5+arg6 RF for loc. 158: arg5+arg6 Bound for (chained) transitions 455: 4 Bound for (chained) transitions 456: 4 - Rank function 2: RF for loc. 95: 1 RF for loc. 158: 0 Bound for (chained) transitions 422: 1 * Removed transitions 412, 418, 419 using the following rank functions: - Rank function 1: RF for loc. 86: 1+arg2+arg4 RF for loc. 154: arg2+arg4 Bound for (chained) transitions 418: 6 Bound for (chained) transitions 419: 6 - Rank function 2: RF for loc. 86: 0 RF for loc. 154: -1 Bound for (chained) transitions 412: 0 * Removed transitions 211, 218, 219, 225, 226, 227, 228, 229, 230, 231, 232, 238 using the following rank functions: - Rank function 1: RF for loc. 79: 4+5*arg5 RF for loc. 80: 2+5*arg4 RF for loc. 81: 1+5*arg2 RF for loc. 82: 5*arg4 RF for loc. 102: 3+5*arg5 Bound for (chained) transitions 218: 3 Bound for (chained) transitions 219: 3 - Rank function 2: RF for loc. 79: -arg1 RF for loc. 80: 1+arg3 RF for loc. 81: arg5 RF for loc. 82: 0 RF for loc. 102: -1-arg1 Bound for (chained) transitions 225: 4 Bound for (chained) transitions 226: 3 Bound for (chained) transitions 228: 3 Bound for (chained) transitions 229: 3 Bound for (chained) transitions 230: 3 Bound for (chained) transitions 231: 3 Bound for (chained) transitions 232: 3 Bound for (chained) transitions 238: 0 - Rank function 3: RF for loc. 79: 0 RF for loc. 81: arg3 RF for loc. 82: 0 RF for loc. 102: 0 Bound for (chained) transitions 227: 3 - Rank function 4: RF for loc. 79: 0 RF for loc. 102: -1 Bound for (chained) transitions 211: 0 * Removed transitions 201, 206, 207 using the following rank functions: - Rank function 1: RF for loc. 64: 1-2*arg3 RF for loc. 98: -2*arg3 Bound for (chained) transitions 206: -6 Bound for (chained) transitions 207: -6 - Rank function 2: RF for loc. 64: 1 RF for loc. 98: 0 Bound for (chained) transitions 201: 1 Used the following cutpoint-specific lexicographic rank functions: * For cutpoint 91, used the following rank functions/bounds (in descending priority order): - RF arg5, bound 3 Errors: