YES Termination proof succeeded Initially, performed program simplifications using lexicographic rank functions: * Removed transitions 83, 86, 87, 95, 97, 98, 99 using the following rank functions: - Rank function 1: RF for loc. 21: 2-3*arg4+3*arg8 RF for loc. 22: 3*arg10-3*arg3 RF for loc. 43: 1-3*arg4+3*arg8 RF for loc. 47: 3*arg10-3*arg3 Bound for (chained) transitions 86: 4 Bound for (chained) transitions 87: 4 - Rank function 2: RF for loc. 21: 3 RF for loc. 22: 1+2*arg4+3*arg6 RF for loc. 43: 2 RF for loc. 47: 2*arg4+3*arg6 Bound for (chained) transitions 83: 3 Bound for (chained) transitions 97: 4 Bound for (chained) transitions 98: 5 Bound for (chained) transitions 99: 5 - Rank function 3: RF for loc. 22: 1 RF for loc. 47: 0 Bound for (chained) transitions 95: 1 * Removed transitions 54, 59, 60, 61, 62, 63, 64, 82 using the following rank functions: - Rank function 1: RF for loc. 19: 2*arg4 RF for loc. 20: 1+2*arg8 RF for loc. 39: -1+2*arg4 Bound for (chained) transitions 59: -1 Bound for (chained) transitions 61: -1 Bound for (chained) transitions 62: -1 Bound for (chained) transitions 63: -1 Bound for (chained) transitions 64: -1 Bound for (chained) transitions 82: 1 - Rank function 2: RF for loc. 19: 1 RF for loc. 20: -1 RF for loc. 39: 0 Bound for (chained) transitions 54: 1 Bound for (chained) transitions 60: 0 * Removed transitions 44, 47, 48 using the following rank functions: - Rank function 1: RF for loc. 15: 1+arg3-arg4 RF for loc. 35: arg3-arg4 Bound for (chained) transitions 47: 2 Bound for (chained) transitions 48: 2 - Rank function 2: RF for loc. 15: 0 RF for loc. 35: -1 Bound for (chained) transitions 44: 0 * Removed transitions 24, 27, 28, 36, 37, 39, 40, 41 using the following rank functions: - Rank function 1: RF for loc. 17: -2*arg3+3*arg5 RF for loc. 18: -2*arg3+3*arg6 RF for loc. 27: -2*arg3+3*arg5 RF for loc. 31: -1-2*arg3+3*arg6 Bound for (chained) transitions 40: 1 Bound for (chained) transitions 41: 1 - Rank function 2: RF for loc. 17: -4*arg3+4*arg5 RF for loc. 18: -4*arg3+4*arg6 RF for loc. 27: -4*arg3+4*arg5 RF for loc. 31: -1-4*arg3+4*arg6 Bound for (chained) transitions 39: 4 - Rank function 3: RF for loc. 17: 0 RF for loc. 18: 0 RF for loc. 27: 0 RF for loc. 31: -1 Bound for (chained) transitions 37: 0 - Rank function 4: RF for loc. 17: 2*arg2 RF for loc. 18: 2*arg2 RF for loc. 27: -1+2*arg2 Bound for (chained) transitions 28: -1 Bound for (chained) transitions 36: 2 - Rank function 5: RF for loc. 17: 1 RF for loc. 18: -arg2P RF for loc. 27: 0 Bound for (chained) transitions 24: 1 - Rank function 6: RF for loc. 18: -arg2P RF for loc. 27: 0 Bound for (chained) transitions 27: 0 * Removed transitions 12, 16, 17 using the following rank functions: - Rank function 1: RF for loc. 16: 1-2*arg3+2*arg6 RF for loc. 23: -2*arg3+2*arg6 Bound for (chained) transitions 16: 2 - Rank function 2: RF for loc. 16: 1-2*arg3+2*arg6 RF for loc. 23: -2*arg3+2*arg6 Bound for (chained) transitions 17: 2 - Rank function 3: RF for loc. 16: 0 RF for loc. 23: -1 Bound for (chained) transitions 12: 0 Errors: