YES Termination proof succeeded Initially, performed program simplifications using lexicographic rank functions: * Removed transitions 71, 74, 75 using the following rank functions: - Rank function 1: RF for loc. 16: 1-arg4-arg5+2*arg7 RF for loc. 33: -arg4-arg5+2*arg7 Bound for (chained) transitions 74: 2 Bound for (chained) transitions 75: 2 - Rank function 2: RF for loc. 16: 0 RF for loc. 33: -1 Bound for (chained) transitions 71: 0 * Removed transitions 61, 64, 65 using the following rank functions: - Rank function 1: RF for loc. 15: 1-2*arg4+2*arg6 RF for loc. 29: -2*arg4+2*arg6 Bound for (chained) transitions 64: 2 Bound for (chained) transitions 65: 2 - Rank function 2: RF for loc. 15: 1 RF for loc. 29: 0 Bound for (chained) transitions 61: 1 * Removed transitions 51, 54, 55 using the following rank functions: - Rank function 1: RF for loc. 14: 1-arg4-arg5+2*arg7 RF for loc. 25: -arg4-arg5+2*arg7 Bound for (chained) transitions 54: 2 Bound for (chained) transitions 55: 2 - Rank function 2: RF for loc. 14: 1 RF for loc. 25: 0 Bound for (chained) transitions 51: 1 * Removed transitions 19, 22, 23, 24, 25, 26, 27, 28, 46, 47, 48 using the following rank functions: - Rank function 1: RF for loc. 12: 3-6*arg3+6*arg4 RF for loc. 13: -5*arg3+5*arg4 RF for loc. 21: 1-6*arg3+6*arg4 Bound for (chained) transitions 22: 7 Bound for (chained) transitions 23: 7 Bound for (chained) transitions 24: 7 Bound for (chained) transitions 25: 7 Bound for (chained) transitions 26: 7 Bound for (chained) transitions 27: 7 Bound for (chained) transitions 28: 7 Bound for (chained) transitions 46: 5 Bound for (chained) transitions 47: 5 Bound for (chained) transitions 48: 5 - Rank function 2: RF for loc. 12: 0 RF for loc. 21: -1 Bound for (chained) transitions 19: 0 * Removed transitions 9, 12, 13 using the following rank functions: - Rank function 1: RF for loc. 11: 1-2*arg2+2*arg3 RF for loc. 17: -2*arg2+2*arg3 Bound for (chained) transitions 12: 2 Bound for (chained) transitions 13: 2 - Rank function 2: RF for loc. 11: 0 RF for loc. 17: -1 Bound for (chained) transitions 9: 0 Errors: