YES(?, 39) Initial complexity problem: 1: T: (1, 1) f0(a, b, c) -> f5(a, 0, c) [ a >= 128 ] (1, 1) f0(a, b, c) -> f7(a, 0, d) [ 127 >= a ] (?, 1) f7(a, b, c) -> f7(a, b + 1, c + 1) [ 35 >= b ] (?, 1) f7(a, b, c) -> f5(a, b, c) [ b >= 36 ] 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, c) -> f7(a, 0, d) [ 127 >= a ] (?, 1) f7(a, b, c) -> f7(a, b + 1, c + 1) [ 35 >= b ] start location: f0 leaf cost: 2 A polynomial rank function with Pol(f0) = 36 Pol(f7) = -V_2 + 36 orients all transitions weakly and the transition f7(a, b, c) -> f7(a, b + 1, c + 1) [ 35 >= b ] strictly and produces the following problem: 3: T: (1, 1) f0(a, b, c) -> f7(a, 0, d) [ 127 >= a ] (36, 1) f7(a, b, c) -> f7(a, b + 1, c + 1) [ 35 >= b ] start location: f0 leaf cost: 2 Complexity upper bound 39 Time: 0.100 sec (SMT: 0.095 sec)