YES Termination proof succeeded Initially, performed program simplifications using lexicographic rank functions: * Removed transitions 179, 182, 183 using the following rank functions: - Rank function 1: RF for loc. 22: 1+2*arg2 RF for loc. 58: 2*arg2 Bound for (chained) transitions 182: 2 Bound for (chained) transitions 183: 2 - Rank function 2: RF for loc. 22: 1 RF for loc. 58: 0 Bound for (chained) transitions 179: 1 * Removed transitions 191, 194, 195 using the following rank functions: - Rank function 1: RF for loc. 23: 1+2*arg2 RF for loc. 62: 2*arg2 Bound for (chained) transitions 194: 2 Bound for (chained) transitions 195: 2 - Rank function 2: RF for loc. 23: 1 RF for loc. 62: 0 Bound for (chained) transitions 191: 1 * Removed transitions 77, 80, 81, 82, 83, 95, 97, 98, 100, 101, 106, 108, 109, 111, 112, 119, 122, 123, 124, 125, 126, 127, 128, 129, 130, 131, 146, 149, 150, 151, 152, 153, 154, 155, 156, 157, 158, 171, 172, 173, 174, 175, 176, 177, 178 using the following rank functions: - Rank function 1: RF for loc. 25: 19*arg12-19*arg13 RF for loc. 26: 1+19*arg13-19*arg14 RF for loc. 27: 2+19*arg13-19*arg14 RF for loc. 28: 2+19*arg14-19*arg15 RF for loc. 29: 17+19*arg14-19*arg15 RF for loc. 30: 2+19*arg13-19*arg14-arg5 RF for loc. 31: 2+19*arg10-19*arg11-arg5 RF for loc. 32: 17+19*arg13-19*arg14-arg5 RF for loc. 33: 17+19*arg10-19*arg11-16*arg5 RF for loc. 38: -1+19*arg12-19*arg13 RF for loc. 42: 1+19*arg13-19*arg14 RF for loc. 46: 2+19*arg13-19*arg14 RF for loc. 50: 2+19*arg14-19*arg15 RF for loc. 54: 17+19*arg14-19*arg15 Bound for (chained) transitions 80: 18 Bound for (chained) transitions 81: 18 Bound for (chained) transitions 123: 2 Bound for (chained) transitions 125: 2 Bound for (chained) transitions 150: 17 Bound for (chained) transitions 152: 17 - Rank function 2: RF for loc. 25: 0 RF for loc. 26: -1+2*arg8 RF for loc. 27: 2*arg8 RF for loc. 28: -2 RF for loc. 29: -2 RF for loc. 30: -2+3*arg5 RF for loc. 31: -2+3*arg5 RF for loc. 32: -2+3*arg5 RF for loc. 33: -2+3*arg5 RF for loc. 38: -1 RF for loc. 42: -2+2*arg8 RF for loc. 46: -1+2*arg8 RF for loc. 50: -2 RF for loc. 54: -2 Bound for (chained) transitions 77: 0 Bound for (chained) transitions 82: -1 Bound for (chained) transitions 83: -1 Bound for (chained) transitions 97: 1 Bound for (chained) transitions 98: 1 Bound for (chained) transitions 100: 0 Bound for (chained) transitions 101: 0 Bound for (chained) transitions 108: 2 Bound for (chained) transitions 109: 2 Bound for (chained) transitions 111: 1 Bound for (chained) transitions 112: 1 Bound for (chained) transitions 172: 1 Bound for (chained) transitions 174: 1 Bound for (chained) transitions 176: 1 Bound for (chained) transitions 178: 1 - Rank function 3: RF for loc. 26: 0 RF for loc. 27: 1 RF for loc. 28: 1+3*arg9 RF for loc. 29: 1+3*arg9 RF for loc. 30: 2+3*arg9 RF for loc. 31: 2+3*arg6 RF for loc. 32: 2+3*arg9 RF for loc. 33: 2+3*arg6 RF for loc. 42: -1 RF for loc. 46: 0 RF for loc. 50: 3*arg9 RF for loc. 54: 3*arg9 Bound for (chained) transitions 122: 3 Bound for (chained) transitions 124: 3 Bound for (chained) transitions 126: 3 Bound for (chained) transitions 128: 3 Bound for (chained) transitions 129: 3 Bound for (chained) transitions 149: 3 Bound for (chained) transitions 151: 3 Bound for (chained) transitions 153: 3 Bound for (chained) transitions 158: 3 - Rank function 4: RF for loc. 26: 0 RF for loc. 27: 1 RF for loc. 28: 4*arg9 RF for loc. 29: 0 RF for loc. 30: arg3+4*arg9 RF for loc. 31: arg1+4*arg6 RF for loc. 32: arg3 RF for loc. 33: arg1 RF for loc. 42: -1 RF for loc. 46: 0 RF for loc. 50: -1+4*arg9 RF for loc. 54: 0 Bound for (chained) transitions 127: 3 Bound for (chained) transitions 130: 3 Bound for (chained) transitions 131: 3 Bound for (chained) transitions 175: 8 Bound for (chained) transitions 177: 1 - Rank function 5: RF for loc. 26: 0 RF for loc. 27: 0 RF for loc. 28: 0 RF for loc. 29: 1+2*arg9 RF for loc. 30: arg3 RF for loc. 31: arg1 RF for loc. 42: -1 RF for loc. 46: -1 RF for loc. 50: -1 RF for loc. 54: 2*arg9 Bound for (chained) transitions 106: 0 Bound for (chained) transitions 119: 0 Bound for (chained) transitions 154: 2 Bound for (chained) transitions 155: 2 Bound for (chained) transitions 156: 2 Bound for (chained) transitions 157: 2 Bound for (chained) transitions 171: 8 Bound for (chained) transitions 173: 1 - Rank function 6: RF for loc. 26: 0 RF for loc. 29: 0 RF for loc. 42: -1 RF for loc. 54: -1 Bound for (chained) transitions 146: 0 - Rank function 7: RF for loc. 26: 1 RF for loc. 42: 0 Bound for (chained) transitions 95: 1 * Removed transitions 61, 65, 66, 67, 68, 69 using the following rank functions: - Rank function 1: RF for loc. 24: 1+arg19+arg25 RF for loc. 34: arg19+arg25 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 - Rank function 2: RF for loc. 24: 0 RF for loc. 34: -1 Bound for (chained) transitions 61: 0 Errors: