YES(?, 11) Initial complexity problem: 1: T: (1, 1) f0(a, b, c, d) -> f8(0, b, c, d) (?, 1) f8(a, b, c, d) -> f8(a + 1, b, c, d) [ 3 >= a ] (?, 1) f8(a, b, c, d) -> f8(a + 1, a, a + 1, e) [ 3 >= a ] (?, 1) f8(a, b, c, d) -> f23(a, b, c, d) [ a >= 4 /\ 0 >= e + 1 ] (?, 1) f8(a, b, c, d) -> f23(a, b, c, d) [ a >= 4 ] start location: f0 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem: 2: T: (1, 1) f0(a, b, c, d) -> f8(0, b, c, d) (?, 1) f8(a, b, c, d) -> f8(a + 1, b, c, d) [ 3 >= a ] (?, 1) f8(a, b, c, d) -> f8(a + 1, a, a + 1, e) [ 3 >= a ] start location: f0 leaf cost: 2 A polynomial rank function with Pol(f0) = 4 Pol(f8) = -V_1 + 4 orients all transitions weakly and the transitions f8(a, b, c, d) -> f8(a + 1, b, c, d) [ 3 >= a ] f8(a, b, c, d) -> f8(a + 1, a, a + 1, e) [ 3 >= a ] strictly and produces the following problem: 3: T: (1, 1) f0(a, b, c, d) -> f8(0, b, c, d) (4, 1) f8(a, b, c, d) -> f8(a + 1, b, c, d) [ 3 >= a ] (4, 1) f8(a, b, c, d) -> f8(a + 1, a, a + 1, e) [ 3 >= a ] start location: f0 leaf cost: 2 Complexity upper bound 11 Time: 0.215 sec (SMT: 0.204 sec)