YES Termination proof succeeded Initially, performed program simplifications using lexicographic rank functions: * Removed transitions 54, 57, 58, 66, 68, 69, 70 using the following rank functions: - Rank function 1: RF for loc. 16: 2-3*arg4+3*arg8 RF for loc. 17: 3*arg10-3*arg3 RF for loc. 30: 1-3*arg4+3*arg8 RF for loc. 34: 3*arg10-3*arg3 Bound for (chained) transitions 57: 4 Bound for (chained) transitions 58: 4 - Rank function 2: RF for loc. 16: 0 RF for loc. 17: 2+2*arg4+arg5 RF for loc. 30: -1 RF for loc. 34: 2*arg4+arg5 Bound for (chained) transitions 54: 0 Bound for (chained) transitions 68: 4 Bound for (chained) transitions 69: 5 Bound for (chained) transitions 70: 1 - Rank function 3: RF for loc. 17: 0 RF for loc. 34: -1 Bound for (chained) transitions 66: 0 * Removed transitions 25, 30, 31, 32, 33, 34, 35, 53 using the following rank functions: - Rank function 1: RF for loc. 14: 2*arg4 RF for loc. 15: -2+2*arg3 RF for loc. 26: -1+2*arg4 Bound for (chained) transitions 30: -1 Bound for (chained) transitions 32: -1 Bound for (chained) transitions 33: -1 Bound for (chained) transitions 34: -1 Bound for (chained) transitions 35: -1 Bound for (chained) transitions 53: 4 - Rank function 2: RF for loc. 14: 1 RF for loc. 15: -arg3P RF for loc. 26: 0 Bound for (chained) transitions 25: 1 Bound for (chained) transitions 31: 0 * Removed transitions 15, 18, 19 using the following rank functions: - Rank function 1: RF for loc. 13: 2+arg2+arg3-arg4 RF for loc. 22: arg2+arg3-arg4 Bound for (chained) transitions 18: 3 Bound for (chained) transitions 19: 3 - Rank function 2: RF for loc. 13: 1 RF for loc. 22: 0 Bound for (chained) transitions 15: 1 * Removed transitions 7, 9, 10 using the following rank functions: - Rank function 1: RF for loc. 12: 1-2*arg3+2*arg6 RF for loc. 18: -2*arg3+2*arg6 Bound for (chained) transitions 9: 2 Bound for (chained) transitions 10: 2 - Rank function 2: RF for loc. 12: 0 RF for loc. 18: -1 Bound for (chained) transitions 7: 0 Errors: