YES(?, b + 3) Initial complexity problem: 1: T: (?, 1) f2(a, b, c, d, e, f) -> f2(a - 1, b - 1, a, b, a - 2, f) [ a >= 1 /\ b >= 1 ] (1, 1) f3(a, b, c, d, e, f) -> f2(a, b, c, d, e, f) (?, 1) f2(a, b, c, d, e, f) -> f4(a, g, c, d, e, h) [ 0 >= b /\ 0 >= g ] (?, 1) f2(a, b, c, d, e, f) -> f4(a, b, c, d, e, h) [ b >= 1 /\ 0 >= a ] start location: f3 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem: 2: T: (?, 1) f2(a, b, c, d, e, f) -> f2(a - 1, b - 1, a, b, a - 2, f) [ a >= 1 /\ b >= 1 ] (1, 1) f3(a, b, c, d, e, f) -> f2(a, b, c, d, e, f) start location: f3 leaf cost: 2 A polynomial rank function with Pol(f2) = V_2 Pol(f3) = V_2 orients all transitions weakly and the transition f2(a, b, c, d, e, f) -> f2(a - 1, b - 1, a, b, a - 2, f) [ a >= 1 /\ b >= 1 ] strictly and produces the following problem: 3: T: (b, 1) f2(a, b, c, d, e, f) -> f2(a - 1, b - 1, a, b, a - 2, f) [ a >= 1 /\ b >= 1 ] (1, 1) f3(a, b, c, d, e, f) -> f2(a, b, c, d, e, f) start location: f3 leaf cost: 2 Complexity upper bound b + 3 Time: 0.189 sec (SMT: 0.180 sec)