YES Termination proof succeeded Initially, performed program simplifications using lexicographic rank functions: * Removed transitions 51, 53, 54, 60, 61, 62, 67, 70, 100, 110, 111, 112, 113, 114, 115 using the following rank functions: - Rank function 1: RF for loc. 34: 21*N_0-21*i_0 RF for loc. 35: 21*N_0+-10-21*i_0 RF for loc. 36: 21*N_0+-10-21*i_0 RF for loc. 37: 21*N_0+-20-21*i_0 RF for loc. 38: 21*N_0+-19-21*i_0 RF for loc. 39: 21*N_0+-10-21*i_0 RF for loc. 40: 21*N_0+-10-21*i_0 RF for loc. 41: 21*N_0+-10-21*i_0 RF for loc. 42: 21*N_0+-10-21*i_0 RF for loc. 43: 21*N_0+-10-21*i_0 RF for loc. 44: 21*N_0+-10-21*i_0 RF for loc. 45: 21*N_0+-10-21*i_0 RF for loc. 46: 21*N_0+-10-21*i_0 RF for loc. 47: 21*N_0+-10-21*i_0 RF for loc. 48: 21*N_0+-10-21*i_0 RF for loc. 49: 21*N_0+-10-21*i_0 RF for loc. 50: 21*N_0+-10-21*i_0 RF for loc. 51: 21*N_0+-10-21*i_0 RF for loc. 52: 21*N_0+-10-21*i_0 RF for loc. 53: 21*N_0+-10-21*i_0 RF for loc. 54: 21*N_0+-10-21*i_0 RF for loc. 55: 21*N_0+-10-21*i_0 RF for loc. 56: 21*N_0+-10-21*i_0 RF for loc. 57: 21*N_0+-10-21*i_0 RF for loc. 58: 21*N_0+-9-21*i_0 RF for loc. 59: 21*N_0+-8-21*i_0 RF for loc. 60: 21*N_0+-7-21*i_0 RF for loc. 61: 21*N_0-21*i_0 RF for loc. 65: 21*N_0+-10-21*i_0 Bound for (chained) transitions 111: 34 Bound for (chained) transitions 115: 21 - Rank function 2: RF for loc. 34: -9 RF for loc. 35: 20*N_0+-5-20*next_0 RF for loc. 36: 20*N_0+-5-20*next_0 RF for loc. 37: 20*N_0+-7-20*next_0 RF for loc. 38: 20*N_0+-6-20*next_0 RF for loc. 39: 20*N_0+-5-20*next_0 RF for loc. 40: 20*N_0+-5-20*next_0 RF for loc. 41: 20*N_0+-5-20*next_0 RF for loc. 42: 20*N_0+-5-20*next_0 RF for loc. 43: 20*N_0+-5-20*next_0 RF for loc. 44: 20*N_0+-5-20*next_0 RF for loc. 45: 20*N_0+-5-20*next_0 RF for loc. 46: 20*N_0+-5-20*next_0 RF for loc. 47: 20*N_0+-5-20*next_0 RF for loc. 48: 20*N_0+-5-20*next_0 RF for loc. 49: 20*N_0+-5-20*next_0 RF for loc. 50: 20*N_0+-5-20*next_0 RF for loc. 51: 20*N_0+-5-20*next_0 RF for loc. 52: 20*N_0+-5-20*next_0 RF for loc. 53: 20*N_0+-5-20*next_0 RF for loc. 54: 20*N_0+-5-20*next_0 RF for loc. 55: 20*N_0+-5-20*next_0 RF for loc. 56: 20*N_0+-5-20*next_0 RF for loc. 57: 20*N_0+-5-20*next_0 RF for loc. 58: 20*N_0+-4-20*next_0 RF for loc. 59: 18*N_0+-1+2*i_0-20*next_0 RF for loc. 60: 18*N_0+2*i_0-20*next_0 RF for loc. 61: -8 RF for loc. 65: 20*N_0+-5-20*next_0 Bound for (chained) transitions 51, 60: -7 Bound for (chained) transitions 53: -8 - Rank function 3: RF for loc. 34: -1 RF for loc. 35: -3-23*next_0 RF for loc. 36: -3-23*next_0 RF for loc. 37: -2-3*c2_0-23*next_0 RF for loc. 38: -1-3*c2_0-23*next_0 RF for loc. 39: -3-23*next_0 RF for loc. 40: -3-23*next_0 RF for loc. 41: -3-23*next_0 RF for loc. 42: -3-23*next_0 RF for loc. 43: -3-23*next_0 RF for loc. 44: -3-23*next_0 RF for loc. 45: -3-23*next_0 RF for loc. 46: -3-23*next_0 RF for loc. 47: -3-23*next_0 RF for loc. 48: -3-23*next_0 RF for loc. 49: -3-23*next_0 RF for loc. 50: -3-23*next_0 RF for loc. 51: -3-23*next_0 RF for loc. 52: -3-23*next_0 RF for loc. 53: -3-23*next_0 RF for loc. 54: -3-23*next_0 RF for loc. 55: -3-23*next_0 RF for loc. 56: -3-23*next_0 RF for loc. 57: -3-23*next_0 RF for loc. 58: -2-23*next_0 RF for loc. 59: -1-23*next_0 RF for loc. 60: -23*next_0 RF for loc. 61: 0 RF for loc. 65: -3-23*next_0 Bound for (chained) transitions 54: 0 - Rank function 4: RF for loc. 35: 0 RF for loc. 36: 0 RF for loc. 37: -s_ab_post RF for loc. 38: 0 RF for loc. 39: 0 RF for loc. 40: 0 RF for loc. 41: 0 RF for loc. 42: 0 RF for loc. 43: 0 RF for loc. 44: 0 RF for loc. 45: 0 RF for loc. 46: 0 RF for loc. 47: 0 RF for loc. 48: 0 RF for loc. 49: 0 RF for loc. 50: 0 RF for loc. 51: 0 RF for loc. 52: 0 RF for loc. 53: 0 RF for loc. 54: 0 RF for loc. 55: 0 RF for loc. 56: 0 RF for loc. 57: 0 RF for loc. 58: 0 RF for loc. 59: 0 RF for loc. 60: 0 RF for loc. 65: 0 Bound for (chained) transitions 61: 0 - Rank function 5: RF for loc. 35: -1 RF for loc. 36: -1 RF for loc. 37: -3 RF for loc. 38: -2 RF for loc. 39: -1 RF for loc. 40: -1 RF for loc. 41: -1 RF for loc. 42: -1 RF for loc. 43: -1 RF for loc. 44: -1 RF for loc. 45: -1 RF for loc. 46: -1 RF for loc. 47: -1 RF for loc. 48: -1 RF for loc. 49: -1 RF for loc. 50: -1 RF for loc. 51: -1 RF for loc. 52: -1 RF for loc. 53: -1 RF for loc. 54: -1 RF for loc. 55: -1 RF for loc. 56: -1 RF for loc. 57: -1 RF for loc. 58: 0 RF for loc. 59: 0 RF for loc. 60: 0 RF for loc. 65: -1 Bound for (chained) transitions 62: -2 Bound for (chained) transitions 67: -1 Bound for (chained) transitions 110: 0 - Rank function 6: RF for loc. 35: -18*next_0+z_0 RF for loc. 36: -18*next_0+z_0 RF for loc. 39: -18*next_0+z_0 RF for loc. 40: -18*next_0+z_0 RF for loc. 41: -18*next_0+z_0 RF for loc. 42: -18*next_0+z_0 RF for loc. 43: -18*next_0+z_0 RF for loc. 44: -18*next_0+z_0 RF for loc. 45: -18*next_0+z_0 RF for loc. 46: -18*next_0+z_0 RF for loc. 47: -18*next_0+z_0 RF for loc. 48: -18*next_0+z_0 RF for loc. 49: -18*next_0+z_0 RF for loc. 50: -18*next_0+z_0 RF for loc. 51: -18*next_0+z_0 RF for loc. 52: -18*next_0+z_0 RF for loc. 53: -18*next_0+z_0 RF for loc. 54: -18*next_0+z_0 RF for loc. 55: -18*next_0+z_0 RF for loc. 56: -18*next_0+z_0 RF for loc. 57: -18*next_0+z_0 RF for loc. 58: -1 RF for loc. 59: 0 RF for loc. 60: 1 RF for loc. 65: -18*next_0+z_0 Bound for (chained) transitions 112: 0 Bound for (chained) transitions 113: 1 Bound for (chained) transitions 114: 1 - Rank function 7: RF for loc. 35: 7*z_0 RF for loc. 36: 7*z_0 RF for loc. 39: 7*z_0 RF for loc. 40: 7*z_0 RF for loc. 41: 7*z_0 RF for loc. 42: 7*z_0 RF for loc. 43: 7*z_0 RF for loc. 44: 7*z_0 RF for loc. 45: 7*z_0 RF for loc. 46: 7*z_0 RF for loc. 47: 7*z_0 RF for loc. 48: 7*z_0 RF for loc. 49: 7*z_0 RF for loc. 50: 7*z_0 RF for loc. 51: 7*z_0 RF for loc. 52: 7*z_0 RF for loc. 53: 7*z_0 RF for loc. 54: 7*z_0 RF for loc. 55: 7*z_0 RF for loc. 56: 7*z_0 RF for loc. 57: 7*z_0 RF for loc. 65: 7*z_0 Bound for (chained) transitions 70: 7 Bound for (chained) transitions 100: 7 Errors: