YES Termination proof succeeded Initially, performed program simplifications using lexicographic rank functions: * Removed transitions 217, 220, 221, 222 using the following rank functions: - Rank function 1: RF for loc. 16: 1+arg2 RF for loc. 26: arg2 Bound for (chained) transitions 220: 2 Bound for (chained) transitions 221: 3 Bound for (chained) transitions 222: 3 - Rank function 2: RF for loc. 16: 0 RF for loc. 26: -1 Bound for (chained) transitions 217: 0 * Removed transitions 205, 208, 209 using the following rank functions: - Rank function 1: RF for loc. 15: 1+arg2 RF for loc. 22: arg2 Bound for (chained) transitions 208: 2 Bound for (chained) transitions 209: 3 - Rank function 2: RF for loc. 15: 0 RF for loc. 22: -1 Bound for (chained) transitions 205: 0 * Removed transitions 49, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 172, 173, 174, 175, 176, 177, 178, 179, 180, 181, 182, 183, 184, 185, 186, 187, 188, 189, 190, 191, 192, 193, 194, 195, 196, 197, 198, 199, 200, 201, 202, 203, 204 using the following rank functions: - Rank function 1: RF for loc. 13: -3*arg2+3*arg3 RF for loc. 14: -2+3*arg1-3*arg2 RF for loc. 18: -1-3*arg2+3*arg3 Bound for (chained) transitions 56: 2 Bound for (chained) transitions 57: 2 Bound for (chained) transitions 58: 2 Bound for (chained) transitions 59: 2 Bound for (chained) transitions 60: 2 Bound for (chained) transitions 61: 2 Bound for (chained) transitions 62: 2 Bound for (chained) transitions 63: 2 Bound for (chained) transitions 64: 2 Bound for (chained) transitions 65: 2 Bound for (chained) transitions 66: 2 Bound for (chained) transitions 67: 2 Bound for (chained) transitions 68: 2 Bound for (chained) transitions 69: 2 Bound for (chained) transitions 70: 2 Bound for (chained) transitions 71: 2 Bound for (chained) transitions 72: 2 Bound for (chained) transitions 73: 2 Bound for (chained) transitions 74: 2 Bound for (chained) transitions 75: 2 Bound for (chained) transitions 76: 2 Bound for (chained) transitions 77: 2 Bound for (chained) transitions 78: 2 Bound for (chained) transitions 79: 2 Bound for (chained) transitions 80: 2 Bound for (chained) transitions 81: 2 Bound for (chained) transitions 82: 2 Bound for (chained) transitions 83: 2 Bound for (chained) transitions 84: 2 Bound for (chained) transitions 85: 2 Bound for (chained) transitions 86: 2 Bound for (chained) transitions 87: 2 Bound for (chained) transitions 88: 2 Bound for (chained) transitions 89: 2 Bound for (chained) transitions 90: 2 Bound for (chained) transitions 172: 1 Bound for (chained) transitions 173: 1 Bound for (chained) transitions 174: 1 Bound for (chained) transitions 175: 1 Bound for (chained) transitions 176: 1 Bound for (chained) transitions 177: 1 Bound for (chained) transitions 178: 1 Bound for (chained) transitions 179: 1 Bound for (chained) transitions 180: 1 Bound for (chained) transitions 181: 1 Bound for (chained) transitions 182: 1 Bound for (chained) transitions 183: 1 Bound for (chained) transitions 184: 1 Bound for (chained) transitions 185: 1 Bound for (chained) transitions 186: 1 Bound for (chained) transitions 187: 1 Bound for (chained) transitions 188: 1 Bound for (chained) transitions 189: 1 Bound for (chained) transitions 190: 1 Bound for (chained) transitions 191: 1 Bound for (chained) transitions 192: 1 Bound for (chained) transitions 193: 1 Bound for (chained) transitions 194: 1 Bound for (chained) transitions 195: 1 Bound for (chained) transitions 196: 1 Bound for (chained) transitions 197: 1 Bound for (chained) transitions 198: 1 Bound for (chained) transitions 199: 1 Bound for (chained) transitions 200: 1 Bound for (chained) transitions 201: 1 Bound for (chained) transitions 202: 1 Bound for (chained) transitions 203: 1 Bound for (chained) transitions 204: 1 - Rank function 2: RF for loc. 13: 0 RF for loc. 18: -1 Bound for (chained) transitions 49: 0 * Removed transitions 232, 234, 235 using the following rank functions: - Rank function 1: RF for loc. 17: 3+6*arg2 RF for loc. 30: 6*arg2 Bound for (chained) transitions 234: 6 Bound for (chained) transitions 235: 6 - Rank function 2: RF for loc. 17: 0 RF for loc. 30: -1 Bound for (chained) transitions 232: 0 Errors: