YES Termination proof succeeded Initially, performed program simplifications using lexicographic rank functions: * Removed transitions 27, 29, 30, 35, 37, 38, 43, 44, 45, 46, 47, 48, 50, 51 using the following rank functions: - Rank function 1: RF for loc. 20: 7-9*i4_0 RF for loc. 21: -9*i4_0 RF for loc. 22: -9*i4_0 RF for loc. 23: -9*i4_0 RF for loc. 24: -9*i4_0 RF for loc. 33: 8-9*i4_0 RF for loc. 37: -9*i4_0 RF for loc. 41: -9*i4_0 Bound for (chained) transitions 47: -38 - Rank function 2: RF for loc. 20: -9*j5_0 RF for loc. 21: 3-9*j5_0 RF for loc. 22: 1-9*j5_0 RF for loc. 23: -9*j5_0 RF for loc. 24: -9*j5_0 RF for loc. 33: -9*j5_0 RF for loc. 37: 2-9*j5_0 RF for loc. 41: -9*j5_0 Bound for (chained) transitions 46: -44 - Rank function 3: RF for loc. 20: -4-2*k6_0 RF for loc. 21: -2*k6_0 RF for loc. 22: -2-2*k6_0 RF for loc. 23: -2*k6_0 RF for loc. 24: 1-2*k6_0 RF for loc. 33: -3-2*k6_0 RF for loc. 37: -1-2*k6_0 RF for loc. 41: 1-2*k6_0 Bound for (chained) transitions 44: -10 - Rank function 4: RF for loc. 20: -6 RF for loc. 21: -2 RF for loc. 22: -4 RF for loc. 23: -1 RF for loc. 24: 1 RF for loc. 33: -5 RF for loc. 37: -3 RF for loc. 41: 0 Bound for (chained) transitions 27, 45: -4 Bound for (chained) transitions 29: -5 Bound for (chained) transitions 30: -5 Bound for (chained) transitions 35: -2 Bound for (chained) transitions 37: -3 Bound for (chained) transitions 38: -3 Bound for (chained) transitions 43: -1 Bound for (chained) transitions 48: 1 Bound for (chained) transitions 50: 0 Bound for (chained) transitions 51: 0 * Removed transitions 11, 13, 14, 19, 21, 22, 56, 57, 59 using the following rank functions: - Rank function 1: RF for loc. 16: -8*i4_0 RF for loc. 17: -5-8*i4_0 RF for loc. 18: -5-8*i4_0 RF for loc. 25: 1-8*i4_0 RF for loc. 29: -5-8*i4_0 Bound for (chained) transitions 59: -40 - Rank function 2: RF for loc. 16: -1-7*j5_0 RF for loc. 17: 2-6*j5_0 RF for loc. 18: -6*j5_0 RF for loc. 25: -7*j5_0 RF for loc. 29: 1-6*j5_0 Bound for (chained) transitions 57: -30 - Rank function 3: RF for loc. 16: -3 RF for loc. 17: 1 RF for loc. 18: -1 RF for loc. 25: -2 RF for loc. 29: 0 Bound for (chained) transitions 11, 56: -1 Bound for (chained) transitions 13: -2 Bound for (chained) transitions 14: -2 Bound for (chained) transitions 19: 1 Bound for (chained) transitions 21: 0 Bound for (chained) transitions 22: 0 Errors: