YES(?, 66) 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) [ 31 >= 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) [ 31 >= c ] (?, 1) f5(a, b, c, d, e, f, g, h, i, j) -> f28(a, b, c, d, b, b, k, l, l, l) [ c >= 32 ] 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) -> f28(c) [ c >= 32 ] (?, 1) f5(c) -> f5(c + 1) [ 31 >= c ] (?, 1) f5(c) -> f5(c + 1) [ 31 >= 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) [ 31 >= c ] (?, 1) f5(c) -> f5(c + 1) [ 31 >= c ] (1, 1) f0(c) -> f5(0) start location: f0 leaf cost: 1 A polynomial rank function with Pol(f5) = -V_1 + 32 Pol(f0) = 32 orients all transitions weakly and the transition f5(c) -> f5(c + 1) [ 31 >= c ] strictly and produces the following problem: 4: T: (32, 1) f5(c) -> f5(c + 1) [ 31 >= c ] (32, 1) f5(c) -> f5(c + 1) [ 31 >= c ] (1, 1) f0(c) -> f5(0) start location: f0 leaf cost: 1 Complexity upper bound 66 Time: 0.121 sec (SMT: 0.117 sec)