YES(?, 85) Initial complexity problem: 1: T: (?, 1) f18(a, b, c, d, e, f) -> f18(a, b + 1, c, d, e, f) [ a >= b + 1 ] (?, 1) f24(a, b, c, d, e, f) -> f24(a, b + 1, c, d, e, f) [ a >= b + 1 ] (?, 1) f31(a, b, c, d, e, f) -> f31(a, b + 1, c, d, e, f) [ a >= b + 1 ] (?, 1) f31(a, b, c, d, e, f) -> f39(a, b, c, d, e, f) [ b >= a ] (?, 1) f24(a, b, c, d, e, f) -> f31(a, 0, c, d, e, f) [ b >= a ] (?, 1) f18(a, b, c, d, e, f) -> f24(a, 0, c, d, e, f) [ b >= a ] (1, 1) f0(a, b, c, d, e, f) -> f18(10, 0, 10, g, 10, h) start location: f0 leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b]. We thus obtain the following problem: 2: T: (1, 1) f0(a, b) -> f18(10, 0) (?, 1) f18(a, b) -> f24(a, 0) [ b >= a ] (?, 1) f24(a, b) -> f31(a, 0) [ b >= a ] (?, 1) f31(a, b) -> f39(a, b) [ b >= a ] (?, 1) f31(a, b) -> f31(a, b + 1) [ a >= b + 1 ] (?, 1) f24(a, b) -> f24(a, b + 1) [ a >= b + 1 ] (?, 1) f18(a, b) -> f18(a, b + 1) [ a >= b + 1 ] start location: f0 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem: 3: T: (1, 1) f0(a, b) -> f18(10, 0) (?, 1) f18(a, b) -> f24(a, 0) [ b >= a ] (?, 1) f24(a, b) -> f31(a, 0) [ b >= a ] (?, 1) f31(a, b) -> f31(a, b + 1) [ a >= b + 1 ] (?, 1) f24(a, b) -> f24(a, b + 1) [ a >= b + 1 ] (?, 1) f18(a, b) -> f18(a, b + 1) [ a >= b + 1 ] start location: f0 leaf cost: 1 A polynomial rank function with Pol(f0) = 2 Pol(f18) = 2 Pol(f24) = 1 Pol(f31) = -1 orients all transitions weakly and the transitions f24(a, b) -> f31(a, 0) [ b >= a ] f18(a, b) -> f24(a, 0) [ b >= a ] strictly and produces the following problem: 4: T: (1, 1) f0(a, b) -> f18(10, 0) (2, 1) f18(a, b) -> f24(a, 0) [ b >= a ] (2, 1) f24(a, b) -> f31(a, 0) [ b >= a ] (?, 1) f31(a, b) -> f31(a, b + 1) [ a >= b + 1 ] (?, 1) f24(a, b) -> f24(a, b + 1) [ a >= b + 1 ] (?, 1) f18(a, b) -> f18(a, b + 1) [ a >= b + 1 ] start location: f0 leaf cost: 1 A polynomial rank function with Pol(f0) = 19 Pol(f18) = 2*V_1 - 1 Pol(f24) = 2*V_1 - 1 Pol(f31) = 2*V_1 - 2*V_2 - 1 orients all transitions weakly and the transition f31(a, b) -> f31(a, b + 1) [ a >= b + 1 ] strictly and produces the following problem: 5: T: (1, 1) f0(a, b) -> f18(10, 0) (2, 1) f18(a, b) -> f24(a, 0) [ b >= a ] (2, 1) f24(a, b) -> f31(a, 0) [ b >= a ] (19, 1) f31(a, b) -> f31(a, b + 1) [ a >= b + 1 ] (?, 1) f24(a, b) -> f24(a, b + 1) [ a >= b + 1 ] (?, 1) f18(a, b) -> f18(a, b + 1) [ a >= b + 1 ] start location: f0 leaf cost: 1 A polynomial rank function with Pol(f24) = V_1 - V_2 Pol(f18) = V_1 - V_2 and size complexities S("f18(a, b) -> f18(a, b + 1) [ a >= b + 1 ]", 0-0) = 10 S("f18(a, b) -> f18(a, b + 1) [ a >= b + 1 ]", 0-1) = ? S("f24(a, b) -> f24(a, b + 1) [ a >= b + 1 ]", 0-0) = 10 S("f24(a, b) -> f24(a, b + 1) [ a >= b + 1 ]", 0-1) = ? S("f31(a, b) -> f31(a, b + 1) [ a >= b + 1 ]", 0-0) = 10 S("f31(a, b) -> f31(a, b + 1) [ a >= b + 1 ]", 0-1) = 19 S("f24(a, b) -> f31(a, 0) [ b >= a ]", 0-0) = 10 S("f24(a, b) -> f31(a, 0) [ b >= a ]", 0-1) = 0 S("f18(a, b) -> f24(a, 0) [ b >= a ]", 0-0) = 10 S("f18(a, b) -> f24(a, 0) [ b >= a ]", 0-1) = 0 S("f0(a, b) -> f18(10, 0)", 0-0) = 10 S("f0(a, b) -> f18(10, 0)", 0-1) = 0 orients the transitions f24(a, b) -> f24(a, b + 1) [ a >= b + 1 ] f18(a, b) -> f18(a, b + 1) [ a >= b + 1 ] weakly and the transitions f24(a, b) -> f24(a, b + 1) [ a >= b + 1 ] f18(a, b) -> f18(a, b + 1) [ a >= b + 1 ] strictly and produces the following problem: 6: T: (1, 1) f0(a, b) -> f18(10, 0) (2, 1) f18(a, b) -> f24(a, 0) [ b >= a ] (2, 1) f24(a, b) -> f31(a, 0) [ b >= a ] (19, 1) f31(a, b) -> f31(a, b + 1) [ a >= b + 1 ] (30, 1) f24(a, b) -> f24(a, b + 1) [ a >= b + 1 ] (30, 1) f18(a, b) -> f18(a, b + 1) [ a >= b + 1 ] start location: f0 leaf cost: 1 Complexity upper bound 85 Time: 0.174 sec (SMT: 0.164 sec)