YES
Termination proof succeeded
Initially, performed program simplifications using lexicographic rank functions:
* Removed transitions 237, 240, 241 using the following rank functions:
- Rank function 1:
RF for loc. 26: 1+2*arg2
RF for loc. 75: 2*arg2
Bound for (chained) transitions 240: 2
Bound for (chained) transitions 241: 2
- Rank function 2:
RF for loc. 26: 1
RF for loc. 75: 0
Bound for (chained) transitions 237: 1
* Removed transitions 136, 141, 142, 143, 144, 145, 146, 147, 148, 161, 162 using the following rank functions:
- Rank function 1:
RF for loc. 32: 3*arg6
RF for loc. 33: 1+3*arg7
RF for loc. 34: 1+3*arg4
RF for loc. 55: -1+3*arg6
Bound for (chained) transitions 141: 2
Bound for (chained) transitions 142: 2
Bound for (chained) transitions 143: 2
Bound for (chained) transitions 144: 2
Bound for (chained) transitions 145: 2
Bound for (chained) transitions 146: 2
Bound for (chained) transitions 148: 2
- Rank function 2:
RF for loc. 32: 0
RF for loc. 33: -arg10+arg2
RF for loc. 34: arg2
RF for loc. 55: 0
Bound for (chained) transitions 162: 10
- Rank function 3:
RF for loc. 32: 0
RF for loc. 33: arg2
RF for loc. 55: 0
Bound for (chained) transitions 161: 8
- Rank function 4:
RF for loc. 32: 2*arg6
RF for loc. 55: -1+2*arg6
Bound for (chained) transitions 147: 1
- Rank function 5:
RF for loc. 32: 0
RF for loc. 55: -1
Bound for (chained) transitions 136: 0
* Removed transitions 113, 118, 119, 120, 121, 122, 123, 124, 125, 159, 160 using the following rank functions:
- Rank function 1:
RF for loc. 29: 3*arg6
RF for loc. 30: 1+3*arg7
RF for loc. 31: 1+3*arg4
RF for loc. 51: -1+3*arg6
Bound for (chained) transitions 118: 2
Bound for (chained) transitions 119: 2
Bound for (chained) transitions 120: 2
Bound for (chained) transitions 121: 2
Bound for (chained) transitions 122: 2
Bound for (chained) transitions 123: 2
Bound for (chained) transitions 124: 2
Bound for (chained) transitions 125: 2
- Rank function 2:
RF for loc. 29: -arg2
RF for loc. 30: 0
RF for loc. 31: 0
RF for loc. 51: -1-arg2
Bound for (chained) transitions 159: 0
Bound for (chained) transitions 160: 0
- Rank function 3:
RF for loc. 29: 1
RF for loc. 51: 0
Bound for (chained) transitions 113: 1
* Removed transitions 212, 215, 216, 217, 218, 219, 220, 221, 222, 235, 236 using the following rank functions:
- Rank function 1:
RF for loc. 40: 3*arg7
RF for loc. 41: 1+3*arg7
RF for loc. 42: 1+3*arg4
RF for loc. 71: -1+3*arg7
Bound for (chained) transitions 215: 2
Bound for (chained) transitions 216: 2
Bound for (chained) transitions 217: 2
Bound for (chained) transitions 218: 2
Bound for (chained) transitions 219: 2
Bound for (chained) transitions 221: 2
Bound for (chained) transitions 222: 2
- Rank function 2:
RF for loc. 40: 1+2*arg6-2*arg9
RF for loc. 41: 2*arg5-2*arg6
RF for loc. 42: 0
RF for loc. 71: 2*arg6-2*arg9
Bound for (chained) transitions 220: 2
Bound for (chained) transitions 236: 0
- Rank function 3:
RF for loc. 40: 0
RF for loc. 41: arg1
RF for loc. 71: -1
Bound for (chained) transitions 212: 0
Bound for (chained) transitions 235: 1
* Removed transitions 189, 192, 193, 194, 195, 196, 197, 198, 199, 233, 234 using the following rank functions:
- Rank function 1:
RF for loc. 37: 3*arg7
RF for loc. 38: 1+3*arg7
RF for loc. 39: 1+3*arg4
RF for loc. 67: -1+3*arg7
Bound for (chained) transitions 192: 2
Bound for (chained) transitions 193: 2
Bound for (chained) transitions 194: 2
Bound for (chained) transitions 195: 2
Bound for (chained) transitions 196: 2
Bound for (chained) transitions 197: 2
Bound for (chained) transitions 198: 2
Bound for (chained) transitions 199: 2
- Rank function 2:
RF for loc. 37: -1
RF for loc. 38: 0
RF for loc. 39: 0
RF for loc. 67: -2
Bound for (chained) transitions 233: 0
Bound for (chained) transitions 234: 0
- Rank function 3:
RF for loc. 37: 0
RF for loc. 67: -1
Bound for (chained) transitions 189: 0
* Removed transitions 175, 178, 179 using the following rank functions:
- Rank function 1:
RF for loc. 36: 2*arg5
RF for loc. 63: -1+2*arg5
Bound for (chained) transitions 178: 1
Bound for (chained) transitions 179: 1
- Rank function 2:
RF for loc. 36: 0
RF for loc. 63: -1
Bound for (chained) transitions 175: 0
* Removed transitions 163, 166, 167 using the following rank functions:
- Rank function 1:
RF for loc. 35: 1+2*arg5
RF for loc. 59: 2*arg5
Bound for (chained) transitions 166: 2
Bound for (chained) transitions 167: 2
- Rank function 2:
RF for loc. 35: 0
RF for loc. 59: -1
Bound for (chained) transitions 163: 0
* Removed transitions 98, 101, 102, 103, 104, 105 using the following rank functions:
- Rank function 1:
RF for loc. 28: 1-2*arg4+2*arg5
RF for loc. 47: -2*arg4+2*arg5
Bound for (chained) transitions 101: 0
Bound for (chained) transitions 102: 0
Bound for (chained) transitions 103: 0
Bound for (chained) transitions 104: 0
Bound for (chained) transitions 105: 0
- Rank function 2:
RF for loc. 28: 1
RF for loc. 47: 0
Bound for (chained) transitions 98: 1
* Removed transitions 79, 84, 85, 86, 87, 88 using the following rank functions:
- Rank function 1:
RF for loc. 27: 1+2*arg4-2*arg5
RF for loc. 43: 2*arg4-2*arg5
Bound for (chained) transitions 84: 2
Bound for (chained) transitions 85: 2
Bound for (chained) transitions 86: 2
Bound for (chained) transitions 87: 2
Bound for (chained) transitions 88: 2
- Rank function 2:
RF for loc. 27: 0
RF for loc. 43: -1
Bound for (chained) transitions 79: 0
Errors: