YES Termination proof succeeded Initially, performed program simplifications using lexicographic rank functions: * Removed transitions 70, 73, 74 using the following rank functions: - Rank function 1: RF for loc. 14: 1 RF for loc. 41: 0 Bound for (chained) transitions 70: 1 Bound for (chained) transitions 73: 0 Bound for (chained) transitions 74: 0 * Removed transitions 57, 60, 61, 69 using the following rank functions: - Rank function 1: RF for loc. 20: 1+2*arg6 RF for loc. 37: 2*arg5 Bound for (chained) transitions 60: 2 Bound for (chained) transitions 61: 2 - Rank function 2: RF for loc. 20: 1 RF for loc. 37: 0 Bound for (chained) transitions 57, 69: 1 * Removed transitions 47, 51, 52 using the following rank functions: - Rank function 1: RF for loc. 18: 1+arg1+arg8-2*arg9 RF for loc. 33: arg1+arg8-2*arg9 Bound for (chained) transitions 51: 9 Bound for (chained) transitions 52: 9 - Rank function 2: RF for loc. 18: 0 RF for loc. 33: -1 Bound for (chained) transitions 47: 0 * Removed transitions 37, 41, 42 using the following rank functions: - Rank function 1: RF for loc. 17: 1-2*arg11+2*arg9 RF for loc. 29: -2*arg11+2*arg9 Bound for (chained) transitions 41: 2 - Rank function 2: RF for loc. 17: 2*arg7 RF for loc. 29: -1+2*arg7 Bound for (chained) transitions 42: -1 - Rank function 3: RF for loc. 17: 1 RF for loc. 29: 0 Bound for (chained) transitions 37: 1 * Removed transitions 30, 33, 34 using the following rank functions: - Rank function 1: RF for loc. 16: 1+arg1+arg3-2*arg4 RF for loc. 25: arg1+arg3-2*arg4 Bound for (chained) transitions 33: 9 - Rank function 2: RF for loc. 16: 1+arg1+arg3-2*arg4 RF for loc. 25: arg1+arg3-2*arg4 Bound for (chained) transitions 34: 9 - Rank function 3: RF for loc. 16: 1 RF for loc. 25: 0 Bound for (chained) transitions 30: 1 * Removed transitions 23, 26, 27 using the following rank functions: - Rank function 1: RF for loc. 15: arg1+arg4-arg6 RF for loc. 21: arg1+arg4-arg6 Bound for (chained) transitions 27: 9 - Rank function 2: RF for loc. 15: 1+2*arg4-2*arg6 RF for loc. 21: 2*arg4-2*arg6 Bound for (chained) transitions 26: 2 - Rank function 3: RF for loc. 15: 1 RF for loc. 21: 0 Bound for (chained) transitions 23: 1 Errors: