YES(?, a + 2) Initial complexity problem: 1: T: (?, 1) f2(a, b) -> f2(a - 1, b) [ a >= 2 ] (?, 1) f2(a, b) -> f1(a - 1, c) [ 1 >= a ] (1, 1) f300(a, b) -> f2(a, b) start location: f300 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem: 2: T: (?, 1) f2(a, b) -> f2(a - 1, b) [ a >= 2 ] (1, 1) f300(a, b) -> f2(a, b) start location: f300 leaf cost: 1 A polynomial rank function with Pol(f2) = V_1 Pol(f300) = V_1 orients all transitions weakly and the transition f2(a, b) -> f2(a - 1, b) [ a >= 2 ] strictly and produces the following problem: 3: T: (a, 1) f2(a, b) -> f2(a - 1, b) [ a >= 2 ] (1, 1) f300(a, b) -> f2(a, b) start location: f300 leaf cost: 1 Complexity upper bound a + 2 Time: 0.079 sec (SMT: 0.076 sec)