YES(?, 34) Initial complexity problem: 1: T: (1, 1) f0(a, b, c, d, e, f, g, h, i, j) -> f5(k, 0, 0, d, e, f, g, h, i, j) (?, 1) f5(a, b, c, d, e, f, g, h, i, j) -> f5(a, b + 1, c + 1, 1, e, f, g, h, i, j) [ 15 >= c ] (?, 1) f5(a, b, c, d, e, f, g, h, i, j) -> f5(a, b, c + 1, 0, e, f, g, h, i, j) [ 15 >= c ] (?, 1) f5(a, b, c, d, e, f, g, h, i, j) -> f27(a, b, c, d, b, b, k, l, l, l) [ c >= 16 ] start location: f0 leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [c]. We thus obtain the following problem: 2: T: (?, 1) f5(c) -> f27(c) [ c >= 16 ] (?, 1) f5(c) -> f5(c + 1) [ 15 >= c ] (?, 1) f5(c) -> f5(c + 1) [ 15 >= c ] (1, 1) f0(c) -> f5(0) start location: f0 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem: 3: T: (?, 1) f5(c) -> f5(c + 1) [ 15 >= c ] (?, 1) f5(c) -> f5(c + 1) [ 15 >= c ] (1, 1) f0(c) -> f5(0) start location: f0 leaf cost: 1 A polynomial rank function with Pol(f5) = -V_1 + 16 Pol(f0) = 16 orients all transitions weakly and the transition f5(c) -> f5(c + 1) [ 15 >= c ] strictly and produces the following problem: 4: T: (16, 1) f5(c) -> f5(c + 1) [ 15 >= c ] (16, 1) f5(c) -> f5(c + 1) [ 15 >= c ] (1, 1) f0(c) -> f5(0) start location: f0 leaf cost: 1 Complexity upper bound 34 Time: 0.127 sec (SMT: 0.122 sec)