YES Termination proof succeeded Initially, performed program simplifications using lexicographic rank functions: * Removed transitions 22, 24, 25 using the following rank functions: - Rank function 1: RF for loc. 12: 1-arg2+arg3-arg4+arg5 RF for loc. 17: -arg2+arg3-arg4+arg5 Bound for (chained) transitions 24: 2 Bound for (chained) transitions 25: 2 - Rank function 2: RF for loc. 12: 0 RF for loc. 17: -1 Bound for (chained) transitions 22: 0 * Removed transitions 30, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94, 95, 96, 97, 98, 99, 100, 101 using the following rank functions: - Rank function 1: RF for loc. 13: 2-4*arg4+3*arg5+arg6 RF for loc. 14: -4*arg4+3*arg5+arg6 RF for loc. 15: -1+3*arg3-4*arg4+arg7 RF for loc. 16: -1+3*arg3-4*arg4+arg7 RF for loc. 21: 1-4*arg4+3*arg5+arg6 Bound for (chained) transitions 33: 2 Bound for (chained) transitions 34: 2 Bound for (chained) transitions 35: 2 Bound for (chained) transitions 36: 2 Bound for (chained) transitions 37: 2 Bound for (chained) transitions 38: 2 Bound for (chained) transitions 39: 2 Bound for (chained) transitions 40: 2 Bound for (chained) transitions 41: 2 Bound for (chained) transitions 42: 2 Bound for (chained) transitions 43: 2 Bound for (chained) transitions 44: 2 Bound for (chained) transitions 45: 2 Bound for (chained) transitions 46: 2 Bound for (chained) transitions 47: 2 Bound for (chained) transitions 48: 2 Bound for (chained) transitions 84: 1 Bound for (chained) transitions 85: 1 Bound for (chained) transitions 86: 1 Bound for (chained) transitions 87: 1 Bound for (chained) transitions 88: 1 Bound for (chained) transitions 89: 1 Bound for (chained) transitions 90: 1 Bound for (chained) transitions 91: 1 Bound for (chained) transitions 92: 1 Bound for (chained) transitions 93: 1 Bound for (chained) transitions 94: 1 Bound for (chained) transitions 95: 1 Bound for (chained) transitions 96: 1 Bound for (chained) transitions 97: 1 Bound for (chained) transitions 98: 1 Bound for (chained) transitions 99: 1 - Rank function 2: RF for loc. 13: 0 RF for loc. 15: arg1P RF for loc. 16: 1 RF for loc. 21: -1 Bound for (chained) transitions 30: 0 Bound for (chained) transitions 100: 1 Bound for (chained) transitions 101: 1 Errors: