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