YES(?, 52) Initial complexity problem: 1: T: (1, 1) f0(a, b) -> f6(0, c) (?, 1) f6(a, b) -> f6(a + 1, b) [ 49 >= a ] (?, 1) f6(a, b) -> f14(a, b) [ a >= 50 ] 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(0, c) (?, 1) f6(a, b) -> f6(a + 1, b) [ 49 >= a ] start location: f0 leaf cost: 1 A polynomial rank function with Pol(f0) = 50 Pol(f6) = -V_1 + 50 orients all transitions weakly and the transition f6(a, b) -> f6(a + 1, b) [ 49 >= a ] strictly and produces the following problem: 3: T: (1, 1) f0(a, b) -> f6(0, c) (50, 1) f6(a, b) -> f6(a + 1, b) [ 49 >= a ] start location: f0 leaf cost: 1 Complexity upper bound 52 Time: 0.077 sec (SMT: 0.074 sec)