YES(?, 1003) Initial complexity problem: 1: T: (?, 1) f300(a, b, c, d, e) -> f300(a - 1, b, c, d, e) [ a >= 101 /\ 9 >= b ] (?, 1) f300(a, b, c, d, e) -> f2(a, b, 0, 0, 0) [ 100 >= a /\ 9 >= b ] (?, 1) f300(a, b, c, d, e) -> f2(a, b, 0, 0, 0) [ b >= 10 ] (1, 1) f1(a, b, c, d, e) -> f300(1000, b, c, d, e) start location: f1 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem: 2: T: (?, 1) f300(a, b, c, d, e) -> f300(a - 1, b, c, d, e) [ a >= 101 /\ 9 >= b ] (1, 1) f1(a, b, c, d, e) -> f300(1000, b, c, d, e) start location: f1 leaf cost: 2 A polynomial rank function with Pol(f300) = V_1 Pol(f1) = 1000 orients all transitions weakly and the transition f300(a, b, c, d, e) -> f300(a - 1, b, c, d, e) [ a >= 101 /\ 9 >= b ] strictly and produces the following problem: 3: T: (1000, 1) f300(a, b, c, d, e) -> f300(a - 1, b, c, d, e) [ a >= 101 /\ 9 >= b ] (1, 1) f1(a, b, c, d, e) -> f300(1000, b, c, d, e) start location: f1 leaf cost: 2 Complexity upper bound 1003 Time: 0.109 sec (SMT: 0.102 sec)