YES(?, 3289) Initial complexity problem: 1: T: (1, 1) f0(a, b, c, d, e, f, g, h, i) -> f17(0, j, k, 0, e, f, g, h, i) (?, 1) f17(a, b, c, d, e, f, g, h, i) -> f17(a, b, c, d + 1, e, f, g, h, i) [ 49 >= d ] (?, 1) f27(a, b, c, d, e, f, g, h, i) -> f27(a, b, c, d, e + 1, f, g, h, i) [ 49 >= e ] (?, 1) f37(a, b, c, d, e, f, g, h, i) -> f37(a, b, c, d, e, f + 1, g, h, i) [ 49 >= f ] (?, 1) f45(a, b, c, d, e, f, g, h, i) -> f45(a + 1, b, c, d, e, f, g, h, i) [ 49 >= a ] (?, 1) f55(a, b, c, d, e, f, g, h, i) -> f55(a, b, c, d, e, f, g + 1, h, i) [ 49 >= g ] (?, 1) f65(a, b, c, d, e, f, g, h, i) -> f65(a, b, c, d, e, f, g, h + 1, i) [ 49 >= h ] (?, 1) f75(a, b, c, d, e, f, g, h, i) -> f75(a, b, c, d, e, f, g, h, i + 1) [ 49 >= i ] (?, 1) f83(a, b, c, d, e, f, g, h, i) -> f83(a + 1, b, c, d, e, f, g, h, i) [ 49 >= a ] (?, 1) f83(a, b, c, d, e, f, g, h, i) -> f93(a, b, c, d, e, f, g, h, i) [ a >= 50 ] (?, 1) f75(a, b, c, d, e, f, g, h, i) -> f83(0, b, c, d, e, f, g, h, i) [ i >= 50 ] (?, 1) f65(a, b, c, d, e, f, g, h, i) -> f75(a, b, c, d, e, f, g, h, 0) [ h >= 50 ] (?, 1) f55(a, b, c, d, e, f, g, h, i) -> f65(a, b, c, d, e, f, g, 0, i) [ g >= 50 ] (?, 1) f45(a, b, c, d, e, f, g, h, i) -> f55(a, b, c, d, e, f, 0, h, i) [ a >= 50 ] (?, 1) f37(a, b, c, d, e, f, g, h, i) -> f45(0, b, c, d, e, f, g, h, i) [ f >= 50 ] (?, 1) f27(a, b, c, d, e, f, g, h, i) -> f37(a, b, c, d, e, 0, g, h, i) [ e >= 50 ] (?, 1) f17(a, b, c, d, e, f, g, h, i) -> f27(a, b, c, d, 0, f, g, h, i) [ d >= 50 ] start location: f0 leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, d, e, f, g, h, i]. We thus obtain the following problem: 2: T: (?, 1) f17(a, d, e, f, g, h, i) -> f27(a, d, 0, f, g, h, i) [ d >= 50 ] (?, 1) f27(a, d, e, f, g, h, i) -> f37(a, d, e, 0, g, h, i) [ e >= 50 ] (?, 1) f37(a, d, e, f, g, h, i) -> f45(0, d, e, f, g, h, i) [ f >= 50 ] (?, 1) f45(a, d, e, f, g, h, i) -> f55(a, d, e, f, 0, h, i) [ a >= 50 ] (?, 1) f55(a, d, e, f, g, h, i) -> f65(a, d, e, f, g, 0, i) [ g >= 50 ] (?, 1) f65(a, d, e, f, g, h, i) -> f75(a, d, e, f, g, h, 0) [ h >= 50 ] (?, 1) f75(a, d, e, f, g, h, i) -> f83(0, d, e, f, g, h, i) [ i >= 50 ] (?, 1) f83(a, d, e, f, g, h, i) -> f93(a, d, e, f, g, h, i) [ a >= 50 ] (?, 1) f83(a, d, e, f, g, h, i) -> f83(a + 1, d, e, f, g, h, i) [ 49 >= a ] (?, 1) f75(a, d, e, f, g, h, i) -> f75(a, d, e, f, g, h, i + 1) [ 49 >= i ] (?, 1) f65(a, d, e, f, g, h, i) -> f65(a, d, e, f, g, h + 1, i) [ 49 >= h ] (?, 1) f55(a, d, e, f, g, h, i) -> f55(a, d, e, f, g + 1, h, i) [ 49 >= g ] (?, 1) f45(a, d, e, f, g, h, i) -> f45(a + 1, d, e, f, g, h, i) [ 49 >= a ] (?, 1) f37(a, d, e, f, g, h, i) -> f37(a, d, e, f + 1, g, h, i) [ 49 >= f ] (?, 1) f27(a, d, e, f, g, h, i) -> f27(a, d, e + 1, f, g, h, i) [ 49 >= e ] (?, 1) f17(a, d, e, f, g, h, i) -> f17(a, d + 1, e, f, g, h, i) [ 49 >= d ] (1, 1) f0(a, d, e, f, g, h, i) -> f17(0, 0, e, f, g, h, i) start location: f0 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem: 3: T: (?, 1) f17(a, d, e, f, g, h, i) -> f27(a, d, 0, f, g, h, i) [ d >= 50 ] (?, 1) f27(a, d, e, f, g, h, i) -> f37(a, d, e, 0, g, h, i) [ e >= 50 ] (?, 1) f37(a, d, e, f, g, h, i) -> f45(0, d, e, f, g, h, i) [ f >= 50 ] (?, 1) f45(a, d, e, f, g, h, i) -> f55(a, d, e, f, 0, h, i) [ a >= 50 ] (?, 1) f55(a, d, e, f, g, h, i) -> f65(a, d, e, f, g, 0, i) [ g >= 50 ] (?, 1) f65(a, d, e, f, g, h, i) -> f75(a, d, e, f, g, h, 0) [ h >= 50 ] (?, 1) f75(a, d, e, f, g, h, i) -> f83(0, d, e, f, g, h, i) [ i >= 50 ] (?, 1) f83(a, d, e, f, g, h, i) -> f83(a + 1, d, e, f, g, h, i) [ 49 >= a ] (?, 1) f75(a, d, e, f, g, h, i) -> f75(a, d, e, f, g, h, i + 1) [ 49 >= i ] (?, 1) f65(a, d, e, f, g, h, i) -> f65(a, d, e, f, g, h + 1, i) [ 49 >= h ] (?, 1) f55(a, d, e, f, g, h, i) -> f55(a, d, e, f, g + 1, h, i) [ 49 >= g ] (?, 1) f45(a, d, e, f, g, h, i) -> f45(a + 1, d, e, f, g, h, i) [ 49 >= a ] (?, 1) f37(a, d, e, f, g, h, i) -> f37(a, d, e, f + 1, g, h, i) [ 49 >= f ] (?, 1) f27(a, d, e, f, g, h, i) -> f27(a, d, e + 1, f, g, h, i) [ 49 >= e ] (?, 1) f17(a, d, e, f, g, h, i) -> f17(a, d + 1, e, f, g, h, i) [ 49 >= d ] (1, 1) f0(a, d, e, f, g, h, i) -> f17(0, 0, e, f, g, h, i) start location: f0 leaf cost: 1 A polynomial rank function with Pol(f17) = 49 Pol(f27) = 48 Pol(f37) = 47 Pol(f45) = 46 Pol(f55) = 45 Pol(f65) = 44 Pol(f75) = 43 Pol(f83) = 42 Pol(f0) = 49 orients all transitions weakly and the transitions f75(a, d, e, f, g, h, i) -> f83(0, d, e, f, g, h, i) [ i >= 50 ] f65(a, d, e, f, g, h, i) -> f75(a, d, e, f, g, h, 0) [ h >= 50 ] f55(a, d, e, f, g, h, i) -> f65(a, d, e, f, g, 0, i) [ g >= 50 ] f45(a, d, e, f, g, h, i) -> f55(a, d, e, f, 0, h, i) [ a >= 50 ] f37(a, d, e, f, g, h, i) -> f45(0, d, e, f, g, h, i) [ f >= 50 ] f27(a, d, e, f, g, h, i) -> f37(a, d, e, 0, g, h, i) [ e >= 50 ] f17(a, d, e, f, g, h, i) -> f27(a, d, 0, f, g, h, i) [ d >= 50 ] strictly and produces the following problem: 4: T: (49, 1) f17(a, d, e, f, g, h, i) -> f27(a, d, 0, f, g, h, i) [ d >= 50 ] (49, 1) f27(a, d, e, f, g, h, i) -> f37(a, d, e, 0, g, h, i) [ e >= 50 ] (49, 1) f37(a, d, e, f, g, h, i) -> f45(0, d, e, f, g, h, i) [ f >= 50 ] (49, 1) f45(a, d, e, f, g, h, i) -> f55(a, d, e, f, 0, h, i) [ a >= 50 ] (49, 1) f55(a, d, e, f, g, h, i) -> f65(a, d, e, f, g, 0, i) [ g >= 50 ] (49, 1) f65(a, d, e, f, g, h, i) -> f75(a, d, e, f, g, h, 0) [ h >= 50 ] (49, 1) f75(a, d, e, f, g, h, i) -> f83(0, d, e, f, g, h, i) [ i >= 50 ] (?, 1) f83(a, d, e, f, g, h, i) -> f83(a + 1, d, e, f, g, h, i) [ 49 >= a ] (?, 1) f75(a, d, e, f, g, h, i) -> f75(a, d, e, f, g, h, i + 1) [ 49 >= i ] (?, 1) f65(a, d, e, f, g, h, i) -> f65(a, d, e, f, g, h + 1, i) [ 49 >= h ] (?, 1) f55(a, d, e, f, g, h, i) -> f55(a, d, e, f, g + 1, h, i) [ 49 >= g ] (?, 1) f45(a, d, e, f, g, h, i) -> f45(a + 1, d, e, f, g, h, i) [ 49 >= a ] (?, 1) f37(a, d, e, f, g, h, i) -> f37(a, d, e, f + 1, g, h, i) [ 49 >= f ] (?, 1) f27(a, d, e, f, g, h, i) -> f27(a, d, e + 1, f, g, h, i) [ 49 >= e ] (?, 1) f17(a, d, e, f, g, h, i) -> f17(a, d + 1, e, f, g, h, i) [ 49 >= d ] (1, 1) f0(a, d, e, f, g, h, i) -> f17(0, 0, e, f, g, h, i) start location: f0 leaf cost: 1 A polynomial rank function with Pol(f17) = -V_2 + 98 Pol(f27) = -V_2 - V_3 + 98 Pol(f37) = -V_2 - V_3 - V_4 + 98 Pol(f45) = -V_2 - V_3 - V_4 + 98 Pol(f55) = -V_2 - V_3 - V_4 - V_5 + 98 Pol(f65) = -V_2 - V_3 - V_4 - V_5 - V_6 + 98 Pol(f75) = -V_2 - V_3 - V_4 - V_5 - V_6 - V_7 + 98 Pol(f83) = -V_1 - V_2 - V_3 - V_4 - V_5 - V_6 - V_7 + 98 Pol(f0) = 98 orients all transitions weakly and the transition f17(a, d, e, f, g, h, i) -> f17(a, d + 1, e, f, g, h, i) [ 49 >= d ] strictly and produces the following problem: 5: T: (49, 1) f17(a, d, e, f, g, h, i) -> f27(a, d, 0, f, g, h, i) [ d >= 50 ] (49, 1) f27(a, d, e, f, g, h, i) -> f37(a, d, e, 0, g, h, i) [ e >= 50 ] (49, 1) f37(a, d, e, f, g, h, i) -> f45(0, d, e, f, g, h, i) [ f >= 50 ] (49, 1) f45(a, d, e, f, g, h, i) -> f55(a, d, e, f, 0, h, i) [ a >= 50 ] (49, 1) f55(a, d, e, f, g, h, i) -> f65(a, d, e, f, g, 0, i) [ g >= 50 ] (49, 1) f65(a, d, e, f, g, h, i) -> f75(a, d, e, f, g, h, 0) [ h >= 50 ] (49, 1) f75(a, d, e, f, g, h, i) -> f83(0, d, e, f, g, h, i) [ i >= 50 ] (?, 1) f83(a, d, e, f, g, h, i) -> f83(a + 1, d, e, f, g, h, i) [ 49 >= a ] (?, 1) f75(a, d, e, f, g, h, i) -> f75(a, d, e, f, g, h, i + 1) [ 49 >= i ] (?, 1) f65(a, d, e, f, g, h, i) -> f65(a, d, e, f, g, h + 1, i) [ 49 >= h ] (?, 1) f55(a, d, e, f, g, h, i) -> f55(a, d, e, f, g + 1, h, i) [ 49 >= g ] (?, 1) f45(a, d, e, f, g, h, i) -> f45(a + 1, d, e, f, g, h, i) [ 49 >= a ] (?, 1) f37(a, d, e, f, g, h, i) -> f37(a, d, e, f + 1, g, h, i) [ 49 >= f ] (?, 1) f27(a, d, e, f, g, h, i) -> f27(a, d, e + 1, f, g, h, i) [ 49 >= e ] (98, 1) f17(a, d, e, f, g, h, i) -> f17(a, d + 1, e, f, g, h, i) [ 49 >= d ] (1, 1) f0(a, d, e, f, g, h, i) -> f17(0, 0, e, f, g, h, i) start location: f0 leaf cost: 1 A polynomial rank function with Pol(f17) = 50 Pol(f27) = -V_3 + 50 Pol(f37) = -V_3 - V_4 - 49 Pol(f45) = -V_3 - V_4 - 49 Pol(f55) = -V_3 - V_4 - V_5 - 49 Pol(f65) = -V_3 - V_4 - V_5 - V_6 - 49 Pol(f75) = -V_3 - V_4 - V_5 - V_6 - V_7 - 49 Pol(f83) = -V_1 - V_3 - V_4 - V_5 - V_6 - V_7 - 49 Pol(f0) = 50 orients all transitions weakly and the transition f27(a, d, e, f, g, h, i) -> f27(a, d, e + 1, f, g, h, i) [ 49 >= e ] strictly and produces the following problem: 6: T: (49, 1) f17(a, d, e, f, g, h, i) -> f27(a, d, 0, f, g, h, i) [ d >= 50 ] (49, 1) f27(a, d, e, f, g, h, i) -> f37(a, d, e, 0, g, h, i) [ e >= 50 ] (49, 1) f37(a, d, e, f, g, h, i) -> f45(0, d, e, f, g, h, i) [ f >= 50 ] (49, 1) f45(a, d, e, f, g, h, i) -> f55(a, d, e, f, 0, h, i) [ a >= 50 ] (49, 1) f55(a, d, e, f, g, h, i) -> f65(a, d, e, f, g, 0, i) [ g >= 50 ] (49, 1) f65(a, d, e, f, g, h, i) -> f75(a, d, e, f, g, h, 0) [ h >= 50 ] (49, 1) f75(a, d, e, f, g, h, i) -> f83(0, d, e, f, g, h, i) [ i >= 50 ] (?, 1) f83(a, d, e, f, g, h, i) -> f83(a + 1, d, e, f, g, h, i) [ 49 >= a ] (?, 1) f75(a, d, e, f, g, h, i) -> f75(a, d, e, f, g, h, i + 1) [ 49 >= i ] (?, 1) f65(a, d, e, f, g, h, i) -> f65(a, d, e, f, g, h + 1, i) [ 49 >= h ] (?, 1) f55(a, d, e, f, g, h, i) -> f55(a, d, e, f, g + 1, h, i) [ 49 >= g ] (?, 1) f45(a, d, e, f, g, h, i) -> f45(a + 1, d, e, f, g, h, i) [ 49 >= a ] (?, 1) f37(a, d, e, f, g, h, i) -> f37(a, d, e, f + 1, g, h, i) [ 49 >= f ] (50, 1) f27(a, d, e, f, g, h, i) -> f27(a, d, e + 1, f, g, h, i) [ 49 >= e ] (98, 1) f17(a, d, e, f, g, h, i) -> f17(a, d + 1, e, f, g, h, i) [ 49 >= d ] (1, 1) f0(a, d, e, f, g, h, i) -> f17(0, 0, e, f, g, h, i) start location: f0 leaf cost: 1 A polynomial rank function with Pol(f17) = 50 Pol(f27) = 50 Pol(f37) = -V_4 + 50 Pol(f45) = -V_4 - 49 Pol(f55) = -V_4 - V_5 - 49 Pol(f65) = -V_4 - V_5 - V_6 - 49 Pol(f75) = -V_4 - V_5 - V_6 - V_7 - 49 Pol(f83) = -V_1 - V_4 - V_5 - V_6 - V_7 - 49 Pol(f0) = 50 orients all transitions weakly and the transition f37(a, d, e, f, g, h, i) -> f37(a, d, e, f + 1, g, h, i) [ 49 >= f ] strictly and produces the following problem: 7: T: (49, 1) f17(a, d, e, f, g, h, i) -> f27(a, d, 0, f, g, h, i) [ d >= 50 ] (49, 1) f27(a, d, e, f, g, h, i) -> f37(a, d, e, 0, g, h, i) [ e >= 50 ] (49, 1) f37(a, d, e, f, g, h, i) -> f45(0, d, e, f, g, h, i) [ f >= 50 ] (49, 1) f45(a, d, e, f, g, h, i) -> f55(a, d, e, f, 0, h, i) [ a >= 50 ] (49, 1) f55(a, d, e, f, g, h, i) -> f65(a, d, e, f, g, 0, i) [ g >= 50 ] (49, 1) f65(a, d, e, f, g, h, i) -> f75(a, d, e, f, g, h, 0) [ h >= 50 ] (49, 1) f75(a, d, e, f, g, h, i) -> f83(0, d, e, f, g, h, i) [ i >= 50 ] (?, 1) f83(a, d, e, f, g, h, i) -> f83(a + 1, d, e, f, g, h, i) [ 49 >= a ] (?, 1) f75(a, d, e, f, g, h, i) -> f75(a, d, e, f, g, h, i + 1) [ 49 >= i ] (?, 1) f65(a, d, e, f, g, h, i) -> f65(a, d, e, f, g, h + 1, i) [ 49 >= h ] (?, 1) f55(a, d, e, f, g, h, i) -> f55(a, d, e, f, g + 1, h, i) [ 49 >= g ] (?, 1) f45(a, d, e, f, g, h, i) -> f45(a + 1, d, e, f, g, h, i) [ 49 >= a ] (50, 1) f37(a, d, e, f, g, h, i) -> f37(a, d, e, f + 1, g, h, i) [ 49 >= f ] (50, 1) f27(a, d, e, f, g, h, i) -> f27(a, d, e + 1, f, g, h, i) [ 49 >= e ] (98, 1) f17(a, d, e, f, g, h, i) -> f17(a, d + 1, e, f, g, h, i) [ 49 >= d ] (1, 1) f0(a, d, e, f, g, h, i) -> f17(0, 0, e, f, g, h, i) start location: f0 leaf cost: 1 A polynomial rank function with Pol(f17) = 50 Pol(f27) = 50 Pol(f37) = 50 Pol(f45) = 50 Pol(f55) = -V_5 + 50 Pol(f65) = -V_5 - V_6 + 50 Pol(f75) = -V_5 - V_6 - V_7 + 50 Pol(f83) = -V_1 - V_5 - V_6 - V_7 + 50 Pol(f0) = 50 orients all transitions weakly and the transition f55(a, d, e, f, g, h, i) -> f55(a, d, e, f, g + 1, h, i) [ 49 >= g ] strictly and produces the following problem: 8: T: (49, 1) f17(a, d, e, f, g, h, i) -> f27(a, d, 0, f, g, h, i) [ d >= 50 ] (49, 1) f27(a, d, e, f, g, h, i) -> f37(a, d, e, 0, g, h, i) [ e >= 50 ] (49, 1) f37(a, d, e, f, g, h, i) -> f45(0, d, e, f, g, h, i) [ f >= 50 ] (49, 1) f45(a, d, e, f, g, h, i) -> f55(a, d, e, f, 0, h, i) [ a >= 50 ] (49, 1) f55(a, d, e, f, g, h, i) -> f65(a, d, e, f, g, 0, i) [ g >= 50 ] (49, 1) f65(a, d, e, f, g, h, i) -> f75(a, d, e, f, g, h, 0) [ h >= 50 ] (49, 1) f75(a, d, e, f, g, h, i) -> f83(0, d, e, f, g, h, i) [ i >= 50 ] (?, 1) f83(a, d, e, f, g, h, i) -> f83(a + 1, d, e, f, g, h, i) [ 49 >= a ] (?, 1) f75(a, d, e, f, g, h, i) -> f75(a, d, e, f, g, h, i + 1) [ 49 >= i ] (?, 1) f65(a, d, e, f, g, h, i) -> f65(a, d, e, f, g, h + 1, i) [ 49 >= h ] (50, 1) f55(a, d, e, f, g, h, i) -> f55(a, d, e, f, g + 1, h, i) [ 49 >= g ] (?, 1) f45(a, d, e, f, g, h, i) -> f45(a + 1, d, e, f, g, h, i) [ 49 >= a ] (50, 1) f37(a, d, e, f, g, h, i) -> f37(a, d, e, f + 1, g, h, i) [ 49 >= f ] (50, 1) f27(a, d, e, f, g, h, i) -> f27(a, d, e + 1, f, g, h, i) [ 49 >= e ] (98, 1) f17(a, d, e, f, g, h, i) -> f17(a, d + 1, e, f, g, h, i) [ 49 >= d ] (1, 1) f0(a, d, e, f, g, h, i) -> f17(0, 0, e, f, g, h, i) start location: f0 leaf cost: 1 A polynomial rank function with Pol(f17) = 98 Pol(f27) = 98 Pol(f37) = 98 Pol(f45) = 98 Pol(f55) = 50 Pol(f65) = -V_6 + 50 Pol(f75) = -V_6 - V_7 - 49 Pol(f83) = -V_1 - V_6 - V_7 - 49 Pol(f0) = 98 orients all transitions weakly and the transition f65(a, d, e, f, g, h, i) -> f65(a, d, e, f, g, h + 1, i) [ 49 >= h ] strictly and produces the following problem: 9: T: (49, 1) f17(a, d, e, f, g, h, i) -> f27(a, d, 0, f, g, h, i) [ d >= 50 ] (49, 1) f27(a, d, e, f, g, h, i) -> f37(a, d, e, 0, g, h, i) [ e >= 50 ] (49, 1) f37(a, d, e, f, g, h, i) -> f45(0, d, e, f, g, h, i) [ f >= 50 ] (49, 1) f45(a, d, e, f, g, h, i) -> f55(a, d, e, f, 0, h, i) [ a >= 50 ] (49, 1) f55(a, d, e, f, g, h, i) -> f65(a, d, e, f, g, 0, i) [ g >= 50 ] (49, 1) f65(a, d, e, f, g, h, i) -> f75(a, d, e, f, g, h, 0) [ h >= 50 ] (49, 1) f75(a, d, e, f, g, h, i) -> f83(0, d, e, f, g, h, i) [ i >= 50 ] (?, 1) f83(a, d, e, f, g, h, i) -> f83(a + 1, d, e, f, g, h, i) [ 49 >= a ] (?, 1) f75(a, d, e, f, g, h, i) -> f75(a, d, e, f, g, h, i + 1) [ 49 >= i ] (98, 1) f65(a, d, e, f, g, h, i) -> f65(a, d, e, f, g, h + 1, i) [ 49 >= h ] (50, 1) f55(a, d, e, f, g, h, i) -> f55(a, d, e, f, g + 1, h, i) [ 49 >= g ] (?, 1) f45(a, d, e, f, g, h, i) -> f45(a + 1, d, e, f, g, h, i) [ 49 >= a ] (50, 1) f37(a, d, e, f, g, h, i) -> f37(a, d, e, f + 1, g, h, i) [ 49 >= f ] (50, 1) f27(a, d, e, f, g, h, i) -> f27(a, d, e + 1, f, g, h, i) [ 49 >= e ] (98, 1) f17(a, d, e, f, g, h, i) -> f17(a, d + 1, e, f, g, h, i) [ 49 >= d ] (1, 1) f0(a, d, e, f, g, h, i) -> f17(0, 0, e, f, g, h, i) start location: f0 leaf cost: 1 A polynomial rank function with Pol(f17) = 98 Pol(f27) = 98 Pol(f37) = 98 Pol(f45) = 98 Pol(f55) = 98 Pol(f65) = 50 Pol(f75) = -V_7 + 50 Pol(f83) = -V_1 - V_7 - 49 Pol(f0) = 98 orients all transitions weakly and the transition f75(a, d, e, f, g, h, i) -> f75(a, d, e, f, g, h, i + 1) [ 49 >= i ] strictly and produces the following problem: 10: T: (49, 1) f17(a, d, e, f, g, h, i) -> f27(a, d, 0, f, g, h, i) [ d >= 50 ] (49, 1) f27(a, d, e, f, g, h, i) -> f37(a, d, e, 0, g, h, i) [ e >= 50 ] (49, 1) f37(a, d, e, f, g, h, i) -> f45(0, d, e, f, g, h, i) [ f >= 50 ] (49, 1) f45(a, d, e, f, g, h, i) -> f55(a, d, e, f, 0, h, i) [ a >= 50 ] (49, 1) f55(a, d, e, f, g, h, i) -> f65(a, d, e, f, g, 0, i) [ g >= 50 ] (49, 1) f65(a, d, e, f, g, h, i) -> f75(a, d, e, f, g, h, 0) [ h >= 50 ] (49, 1) f75(a, d, e, f, g, h, i) -> f83(0, d, e, f, g, h, i) [ i >= 50 ] (?, 1) f83(a, d, e, f, g, h, i) -> f83(a + 1, d, e, f, g, h, i) [ 49 >= a ] (98, 1) f75(a, d, e, f, g, h, i) -> f75(a, d, e, f, g, h, i + 1) [ 49 >= i ] (98, 1) f65(a, d, e, f, g, h, i) -> f65(a, d, e, f, g, h + 1, i) [ 49 >= h ] (50, 1) f55(a, d, e, f, g, h, i) -> f55(a, d, e, f, g + 1, h, i) [ 49 >= g ] (?, 1) f45(a, d, e, f, g, h, i) -> f45(a + 1, d, e, f, g, h, i) [ 49 >= a ] (50, 1) f37(a, d, e, f, g, h, i) -> f37(a, d, e, f + 1, g, h, i) [ 49 >= f ] (50, 1) f27(a, d, e, f, g, h, i) -> f27(a, d, e + 1, f, g, h, i) [ 49 >= e ] (98, 1) f17(a, d, e, f, g, h, i) -> f17(a, d + 1, e, f, g, h, i) [ 49 >= d ] (1, 1) f0(a, d, e, f, g, h, i) -> f17(0, 0, e, f, g, h, i) start location: f0 leaf cost: 1 A polynomial rank function with Pol(f17) = 50 Pol(f27) = 50 Pol(f37) = 50 Pol(f45) = 50 Pol(f55) = 50 Pol(f65) = 50 Pol(f75) = 50 Pol(f83) = -V_1 + 50 Pol(f0) = 50 orients all transitions weakly and the transition f83(a, d, e, f, g, h, i) -> f83(a + 1, d, e, f, g, h, i) [ 49 >= a ] strictly and produces the following problem: 11: T: (49, 1) f17(a, d, e, f, g, h, i) -> f27(a, d, 0, f, g, h, i) [ d >= 50 ] (49, 1) f27(a, d, e, f, g, h, i) -> f37(a, d, e, 0, g, h, i) [ e >= 50 ] (49, 1) f37(a, d, e, f, g, h, i) -> f45(0, d, e, f, g, h, i) [ f >= 50 ] (49, 1) f45(a, d, e, f, g, h, i) -> f55(a, d, e, f, 0, h, i) [ a >= 50 ] (49, 1) f55(a, d, e, f, g, h, i) -> f65(a, d, e, f, g, 0, i) [ g >= 50 ] (49, 1) f65(a, d, e, f, g, h, i) -> f75(a, d, e, f, g, h, 0) [ h >= 50 ] (49, 1) f75(a, d, e, f, g, h, i) -> f83(0, d, e, f, g, h, i) [ i >= 50 ] (50, 1) f83(a, d, e, f, g, h, i) -> f83(a + 1, d, e, f, g, h, i) [ 49 >= a ] (98, 1) f75(a, d, e, f, g, h, i) -> f75(a, d, e, f, g, h, i + 1) [ 49 >= i ] (98, 1) f65(a, d, e, f, g, h, i) -> f65(a, d, e, f, g, h + 1, i) [ 49 >= h ] (50, 1) f55(a, d, e, f, g, h, i) -> f55(a, d, e, f, g + 1, h, i) [ 49 >= g ] (?, 1) f45(a, d, e, f, g, h, i) -> f45(a + 1, d, e, f, g, h, i) [ 49 >= a ] (50, 1) f37(a, d, e, f, g, h, i) -> f37(a, d, e, f + 1, g, h, i) [ 49 >= f ] (50, 1) f27(a, d, e, f, g, h, i) -> f27(a, d, e + 1, f, g, h, i) [ 49 >= e ] (98, 1) f17(a, d, e, f, g, h, i) -> f17(a, d + 1, e, f, g, h, i) [ 49 >= d ] (1, 1) f0(a, d, e, f, g, h, i) -> f17(0, 0, e, f, g, h, i) start location: f0 leaf cost: 1 A polynomial rank function with Pol(f45) = -V_1 + 50 and size complexities S("f0(a, d, e, f, g, h, i) -> f17(0, 0, e, f, g, h, i)", 0-0) = 0 S("f0(a, d, e, f, g, h, i) -> f17(0, 0, e, f, g, h, i)", 0-1) = 0 S("f0(a, d, e, f, g, h, i) -> f17(0, 0, e, f, g, h, i)", 0-2) = e S("f0(a, d, e, f, g, h, i) -> f17(0, 0, e, f, g, h, i)", 0-3) = f S("f0(a, d, e, f, g, h, i) -> f17(0, 0, e, f, g, h, i)", 0-4) = g S("f0(a, d, e, f, g, h, i) -> f17(0, 0, e, f, g, h, i)", 0-5) = h S("f0(a, d, e, f, g, h, i) -> f17(0, 0, e, f, g, h, i)", 0-6) = i S("f17(a, d, e, f, g, h, i) -> f17(a, d + 1, e, f, g, h, i) [ 49 >= d ]", 0-0) = 0 S("f17(a, d, e, f, g, h, i) -> f17(a, d + 1, e, f, g, h, i) [ 49 >= d ]", 0-1) = 50 S("f17(a, d, e, f, g, h, i) -> f17(a, d + 1, e, f, g, h, i) [ 49 >= d ]", 0-2) = e S("f17(a, d, e, f, g, h, i) -> f17(a, d + 1, e, f, g, h, i) [ 49 >= d ]", 0-3) = f S("f17(a, d, e, f, g, h, i) -> f17(a, d + 1, e, f, g, h, i) [ 49 >= d ]", 0-4) = g S("f17(a, d, e, f, g, h, i) -> f17(a, d + 1, e, f, g, h, i) [ 49 >= d ]", 0-5) = h S("f17(a, d, e, f, g, h, i) -> f17(a, d + 1, e, f, g, h, i) [ 49 >= d ]", 0-6) = i S("f27(a, d, e, f, g, h, i) -> f27(a, d, e + 1, f, g, h, i) [ 49 >= e ]", 0-0) = 0 S("f27(a, d, e, f, g, h, i) -> f27(a, d, e + 1, f, g, h, i) [ 49 >= e ]", 0-1) = 50 S("f27(a, d, e, f, g, h, i) -> f27(a, d, e + 1, f, g, h, i) [ 49 >= e ]", 0-2) = 50 S("f27(a, d, e, f, g, h, i) -> f27(a, d, e + 1, f, g, h, i) [ 49 >= e ]", 0-3) = f S("f27(a, d, e, f, g, h, i) -> f27(a, d, e + 1, f, g, h, i) [ 49 >= e ]", 0-4) = g S("f27(a, d, e, f, g, h, i) -> f27(a, d, e + 1, f, g, h, i) [ 49 >= e ]", 0-5) = h S("f27(a, d, e, f, g, h, i) -> f27(a, d, e + 1, f, g, h, i) [ 49 >= e ]", 0-6) = i S("f37(a, d, e, f, g, h, i) -> f37(a, d, e, f + 1, g, h, i) [ 49 >= f ]", 0-0) = 0 S("f37(a, d, e, f, g, h, i) -> f37(a, d, e, f + 1, g, h, i) [ 49 >= f ]", 0-1) = 50 S("f37(a, d, e, f, g, h, i) -> f37(a, d, e, f + 1, g, h, i) [ 49 >= f ]", 0-2) = 50 S("f37(a, d, e, f, g, h, i) -> f37(a, d, e, f + 1, g, h, i) [ 49 >= f ]", 0-3) = 50 S("f37(a, d, e, f, g, h, i) -> f37(a, d, e, f + 1, g, h, i) [ 49 >= f ]", 0-4) = g S("f37(a, d, e, f, g, h, i) -> f37(a, d, e, f + 1, g, h, i) [ 49 >= f ]", 0-5) = h S("f37(a, d, e, f, g, h, i) -> f37(a, d, e, f + 1, g, h, i) [ 49 >= f ]", 0-6) = i S("f45(a, d, e, f, g, h, i) -> f45(a + 1, d, e, f, g, h, i) [ 49 >= a ]", 0-0) = 50 S("f45(a, d, e, f, g, h, i) -> f45(a + 1, d, e, f, g, h, i) [ 49 >= a ]", 0-1) = 50 S("f45(a, d, e, f, g, h, i) -> f45(a + 1, d, e, f, g, h, i) [ 49 >= a ]", 0-2) = 50 S("f45(a, d, e, f, g, h, i) -> f45(a + 1, d, e, f, g, h, i) [ 49 >= a ]", 0-3) = 50 S("f45(a, d, e, f, g, h, i) -> f45(a + 1, d, e, f, g, h, i) [ 49 >= a ]", 0-4) = g S("f45(a, d, e, f, g, h, i) -> f45(a + 1, d, e, f, g, h, i) [ 49 >= a ]", 0-5) = h S("f45(a, d, e, f, g, h, i) -> f45(a + 1, d, e, f, g, h, i) [ 49 >= a ]", 0-6) = i S("f55(a, d, e, f, g, h, i) -> f55(a, d, e, f, g + 1, h, i) [ 49 >= g ]", 0-0) = 50 S("f55(a, d, e, f, g, h, i) -> f55(a, d, e, f, g + 1, h, i) [ 49 >= g ]", 0-1) = 50 S("f55(a, d, e, f, g, h, i) -> f55(a, d, e, f, g + 1, h, i) [ 49 >= g ]", 0-2) = 50 S("f55(a, d, e, f, g, h, i) -> f55(a, d, e, f, g + 1, h, i) [ 49 >= g ]", 0-3) = 50 S("f55(a, d, e, f, g, h, i) -> f55(a, d, e, f, g + 1, h, i) [ 49 >= g ]", 0-4) = 50 S("f55(a, d, e, f, g, h, i) -> f55(a, d, e, f, g + 1, h, i) [ 49 >= g ]", 0-5) = h S("f55(a, d, e, f, g, h, i) -> f55(a, d, e, f, g + 1, h, i) [ 49 >= g ]", 0-6) = i S("f65(a, d, e, f, g, h, i) -> f65(a, d, e, f, g, h + 1, i) [ 49 >= h ]", 0-0) = 50 S("f65(a, d, e, f, g, h, i) -> f65(a, d, e, f, g, h + 1, i) [ 49 >= h ]", 0-1) = 50 S("f65(a, d, e, f, g, h, i) -> f65(a, d, e, f, g, h + 1, i) [ 49 >= h ]", 0-2) = 50 S("f65(a, d, e, f, g, h, i) -> f65(a, d, e, f, g, h + 1, i) [ 49 >= h ]", 0-3) = 50 S("f65(a, d, e, f, g, h, i) -> f65(a, d, e, f, g, h + 1, i) [ 49 >= h ]", 0-4) = 50 S("f65(a, d, e, f, g, h, i) -> f65(a, d, e, f, g, h + 1, i) [ 49 >= h ]", 0-5) = 50 S("f65(a, d, e, f, g, h, i) -> f65(a, d, e, f, g, h + 1, i) [ 49 >= h ]", 0-6) = i S("f75(a, d, e, f, g, h, i) -> f75(a, d, e, f, g, h, i + 1) [ 49 >= i ]", 0-0) = 50 S("f75(a, d, e, f, g, h, i) -> f75(a, d, e, f, g, h, i + 1) [ 49 >= i ]", 0-1) = 50 S("f75(a, d, e, f, g, h, i) -> f75(a, d, e, f, g, h, i + 1) [ 49 >= i ]", 0-2) = 50 S("f75(a, d, e, f, g, h, i) -> f75(a, d, e, f, g, h, i + 1) [ 49 >= i ]", 0-3) = 50 S("f75(a, d, e, f, g, h, i) -> f75(a, d, e, f, g, h, i + 1) [ 49 >= i ]", 0-4) = 50 S("f75(a, d, e, f, g, h, i) -> f75(a, d, e, f, g, h, i + 1) [ 49 >= i ]", 0-5) = 50 S("f75(a, d, e, f, g, h, i) -> f75(a, d, e, f, g, h, i + 1) [ 49 >= i ]", 0-6) = 50 S("f83(a, d, e, f, g, h, i) -> f83(a + 1, d, e, f, g, h, i) [ 49 >= a ]", 0-0) = 50 S("f83(a, d, e, f, g, h, i) -> f83(a + 1, d, e, f, g, h, i) [ 49 >= a ]", 0-1) = 50 S("f83(a, d, e, f, g, h, i) -> f83(a + 1, d, e, f, g, h, i) [ 49 >= a ]", 0-2) = 50 S("f83(a, d, e, f, g, h, i) -> f83(a + 1, d, e, f, g, h, i) [ 49 >= a ]", 0-3) = 50 S("f83(a, d, e, f, g, h, i) -> f83(a + 1, d, e, f, g, h, i) [ 49 >= a ]", 0-4) = 50 S("f83(a, d, e, f, g, h, i) -> f83(a + 1, d, e, f, g, h, i) [ 49 >= a ]", 0-5) = 50 S("f83(a, d, e, f, g, h, i) -> f83(a + 1, d, e, f, g, h, i) [ 49 >= a ]", 0-6) = 50 S("f75(a, d, e, f, g, h, i) -> f83(0, d, e, f, g, h, i) [ i >= 50 ]", 0-0) = 0 S("f75(a, d, e, f, g, h, i) -> f83(0, d, e, f, g, h, i) [ i >= 50 ]", 0-1) = 50 S("f75(a, d, e, f, g, h, i) -> f83(0, d, e, f, g, h, i) [ i >= 50 ]", 0-2) = 50 S("f75(a, d, e, f, g, h, i) -> f83(0, d, e, f, g, h, i) [ i >= 50 ]", 0-3) = 50 S("f75(a, d, e, f, g, h, i) -> f83(0, d, e, f, g, h, i) [ i >= 50 ]", 0-4) = 50 S("f75(a, d, e, f, g, h, i) -> f83(0, d, e, f, g, h, i) [ i >= 50 ]", 0-5) = 50 S("f75(a, d, e, f, g, h, i) -> f83(0, d, e, f, g, h, i) [ i >= 50 ]", 0-6) = 50 S("f65(a, d, e, f, g, h, i) -> f75(a, d, e, f, g, h, 0) [ h >= 50 ]", 0-0) = 50 S("f65(a, d, e, f, g, h, i) -> f75(a, d, e, f, g, h, 0) [ h >= 50 ]", 0-1) = 50 S("f65(a, d, e, f, g, h, i) -> f75(a, d, e, f, g, h, 0) [ h >= 50 ]", 0-2) = 50 S("f65(a, d, e, f, g, h, i) -> f75(a, d, e, f, g, h, 0) [ h >= 50 ]", 0-3) = 50 S("f65(a, d, e, f, g, h, i) -> f75(a, d, e, f, g, h, 0) [ h >= 50 ]", 0-4) = 50 S("f65(a, d, e, f, g, h, i) -> f75(a, d, e, f, g, h, 0) [ h >= 50 ]", 0-5) = 50 S("f65(a, d, e, f, g, h, i) -> f75(a, d, e, f, g, h, 0) [ h >= 50 ]", 0-6) = 0 S("f55(a, d, e, f, g, h, i) -> f65(a, d, e, f, g, 0, i) [ g >= 50 ]", 0-0) = 50 S("f55(a, d, e, f, g, h, i) -> f65(a, d, e, f, g, 0, i) [ g >= 50 ]", 0-1) = 50 S("f55(a, d, e, f, g, h, i) -> f65(a, d, e, f, g, 0, i) [ g >= 50 ]", 0-2) = 50 S("f55(a, d, e, f, g, h, i) -> f65(a, d, e, f, g, 0, i) [ g >= 50 ]", 0-3) = 50 S("f55(a, d, e, f, g, h, i) -> f65(a, d, e, f, g, 0, i) [ g >= 50 ]", 0-4) = 50 S("f55(a, d, e, f, g, h, i) -> f65(a, d, e, f, g, 0, i) [ g >= 50 ]", 0-5) = 0 S("f55(a, d, e, f, g, h, i) -> f65(a, d, e, f, g, 0, i) [ g >= 50 ]", 0-6) = i S("f45(a, d, e, f, g, h, i) -> f55(a, d, e, f, 0, h, i) [ a >= 50 ]", 0-0) = 50 S("f45(a, d, e, f, g, h, i) -> f55(a, d, e, f, 0, h, i) [ a >= 50 ]", 0-1) = 50 S("f45(a, d, e, f, g, h, i) -> f55(a, d, e, f, 0, h, i) [ a >= 50 ]", 0-2) = 50 S("f45(a, d, e, f, g, h, i) -> f55(a, d, e, f, 0, h, i) [ a >= 50 ]", 0-3) = 50 S("f45(a, d, e, f, g, h, i) -> f55(a, d, e, f, 0, h, i) [ a >= 50 ]", 0-4) = 0 S("f45(a, d, e, f, g, h, i) -> f55(a, d, e, f, 0, h, i) [ a >= 50 ]", 0-5) = h S("f45(a, d, e, f, g, h, i) -> f55(a, d, e, f, 0, h, i) [ a >= 50 ]", 0-6) = i S("f37(a, d, e, f, g, h, i) -> f45(0, d, e, f, g, h, i) [ f >= 50 ]", 0-0) = 0 S("f37(a, d, e, f, g, h, i) -> f45(0, d, e, f, g, h, i) [ f >= 50 ]", 0-1) = 50 S("f37(a, d, e, f, g, h, i) -> f45(0, d, e, f, g, h, i) [ f >= 50 ]", 0-2) = 50 S("f37(a, d, e, f, g, h, i) -> f45(0, d, e, f, g, h, i) [ f >= 50 ]", 0-3) = 50 S("f37(a, d, e, f, g, h, i) -> f45(0, d, e, f, g, h, i) [ f >= 50 ]", 0-4) = g S("f37(a, d, e, f, g, h, i) -> f45(0, d, e, f, g, h, i) [ f >= 50 ]", 0-5) = h S("f37(a, d, e, f, g, h, i) -> f45(0, d, e, f, g, h, i) [ f >= 50 ]", 0-6) = i S("f27(a, d, e, f, g, h, i) -> f37(a, d, e, 0, g, h, i) [ e >= 50 ]", 0-0) = 0 S("f27(a, d, e, f, g, h, i) -> f37(a, d, e, 0, g, h, i) [ e >= 50 ]", 0-1) = 50 S("f27(a, d, e, f, g, h, i) -> f37(a, d, e, 0, g, h, i) [ e >= 50 ]", 0-2) = 50 S("f27(a, d, e, f, g, h, i) -> f37(a, d, e, 0, g, h, i) [ e >= 50 ]", 0-3) = 0 S("f27(a, d, e, f, g, h, i) -> f37(a, d, e, 0, g, h, i) [ e >= 50 ]", 0-4) = g S("f27(a, d, e, f, g, h, i) -> f37(a, d, e, 0, g, h, i) [ e >= 50 ]", 0-5) = h S("f27(a, d, e, f, g, h, i) -> f37(a, d, e, 0, g, h, i) [ e >= 50 ]", 0-6) = i S("f17(a, d, e, f, g, h, i) -> f27(a, d, 0, f, g, h, i) [ d >= 50 ]", 0-0) = 0 S("f17(a, d, e, f, g, h, i) -> f27(a, d, 0, f, g, h, i) [ d >= 50 ]", 0-1) = 50 S("f17(a, d, e, f, g, h, i) -> f27(a, d, 0, f, g, h, i) [ d >= 50 ]", 0-2) = 0 S("f17(a, d, e, f, g, h, i) -> f27(a, d, 0, f, g, h, i) [ d >= 50 ]", 0-3) = f S("f17(a, d, e, f, g, h, i) -> f27(a, d, 0, f, g, h, i) [ d >= 50 ]", 0-4) = g S("f17(a, d, e, f, g, h, i) -> f27(a, d, 0, f, g, h, i) [ d >= 50 ]", 0-5) = h S("f17(a, d, e, f, g, h, i) -> f27(a, d, 0, f, g, h, i) [ d >= 50 ]", 0-6) = i orients the transition f45(a, d, e, f, g, h, i) -> f45(a + 1, d, e, f, g, h, i) [ 49 >= a ] weakly and the transition f45(a, d, e, f, g, h, i) -> f45(a + 1, d, e, f, g, h, i) [ 49 >= a ] strictly and produces the following problem: 12: T: (49, 1) f17(a, d, e, f, g, h, i) -> f27(a, d, 0, f, g, h, i) [ d >= 50 ] (49, 1) f27(a, d, e, f, g, h, i) -> f37(a, d, e, 0, g, h, i) [ e >= 50 ] (49, 1) f37(a, d, e, f, g, h, i) -> f45(0, d, e, f, g, h, i) [ f >= 50 ] (49, 1) f45(a, d, e, f, g, h, i) -> f55(a, d, e, f, 0, h, i) [ a >= 50 ] (49, 1) f55(a, d, e, f, g, h, i) -> f65(a, d, e, f, g, 0, i) [ g >= 50 ] (49, 1) f65(a, d, e, f, g, h, i) -> f75(a, d, e, f, g, h, 0) [ h >= 50 ] (49, 1) f75(a, d, e, f, g, h, i) -> f83(0, d, e, f, g, h, i) [ i >= 50 ] (50, 1) f83(a, d, e, f, g, h, i) -> f83(a + 1, d, e, f, g, h, i) [ 49 >= a ] (98, 1) f75(a, d, e, f, g, h, i) -> f75(a, d, e, f, g, h, i + 1) [ 49 >= i ] (98, 1) f65(a, d, e, f, g, h, i) -> f65(a, d, e, f, g, h + 1, i) [ 49 >= h ] (50, 1) f55(a, d, e, f, g, h, i) -> f55(a, d, e, f, g + 1, h, i) [ 49 >= g ] (2450, 1) f45(a, d, e, f, g, h, i) -> f45(a + 1, d, e, f, g, h, i) [ 49 >= a ] (50, 1) f37(a, d, e, f, g, h, i) -> f37(a, d, e, f + 1, g, h, i) [ 49 >= f ] (50, 1) f27(a, d, e, f, g, h, i) -> f27(a, d, e + 1, f, g, h, i) [ 49 >= e ] (98, 1) f17(a, d, e, f, g, h, i) -> f17(a, d + 1, e, f, g, h, i) [ 49 >= d ] (1, 1) f0(a, d, e, f, g, h, i) -> f17(0, 0, e, f, g, h, i) start location: f0 leaf cost: 1 Complexity upper bound 3289 Time: 1.011 sec (SMT: 0.882 sec)