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