YES(?, 103) Initial complexity problem: 1: T: (?, 1) f300(a, b, c, d, e) -> f300(a + 1, b, c, d, e) [ 100 >= a /\ b >= 1 ] (?, 1) f300(a, b, c, d, e) -> f3(a, b, 0, 0, 0) [ a >= 101 ] (1, 1) f2(a, b, c, d, e) -> f300(1, b, c, d, e) [ b >= 1 ] (1, 1) f2(a, b, c, d, e) -> f3(0, b, 0, 0, 0) [ 0 >= b ] start location: f2 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) [ 100 >= a /\ b >= 1 ] (1, 1) f2(a, b, c, d, e) -> f300(1, b, c, d, e) [ b >= 1 ] start location: f2 leaf cost: 2 A polynomial rank function with Pol(f300) = -V_1 + 101 Pol(f2) = 100 orients all transitions weakly and the transition f300(a, b, c, d, e) -> f300(a + 1, b, c, d, e) [ 100 >= a /\ b >= 1 ] strictly and produces the following problem: 3: T: (100, 1) f300(a, b, c, d, e) -> f300(a + 1, b, c, d, e) [ 100 >= a /\ b >= 1 ] (1, 1) f2(a, b, c, d, e) -> f300(1, b, c, d, e) [ b >= 1 ] start location: f2 leaf cost: 2 Complexity upper bound 103 Time: 0.101 sec (SMT: 0.097 sec)