YES(?, 12) Initial complexity problem: 1: T: (1, 1) f0(a, b) -> f6(c, 0) (?, 1) f6(a, b) -> f6(a, b + 1) [ 9 >= b ] (?, 1) f6(a, b) -> f15(a, b) [ b >= 10 ] start location: f0 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem: 2: T: (1, 1) f0(a, b) -> f6(c, 0) (?, 1) f6(a, b) -> f6(a, b + 1) [ 9 >= b ] start location: f0 leaf cost: 1 A polynomial rank function with Pol(f0) = 10 Pol(f6) = -V_2 + 10 orients all transitions weakly and the transition f6(a, b) -> f6(a, b + 1) [ 9 >= b ] strictly and produces the following problem: 3: T: (1, 1) f0(a, b) -> f6(c, 0) (10, 1) f6(a, b) -> f6(a, b + 1) [ 9 >= b ] start location: f0 leaf cost: 1 Complexity upper bound 12 Time: 0.070 sec (SMT: 0.068 sec)