YES(?, 830) Initial complexity problem: 1: T: (1, 1) evaleasy1start(a, b) -> evaleasy1entryin(a, b) (?, 1) evaleasy1entryin(a, b) -> evaleasy1bb3in(0, b) (?, 1) evaleasy1bb3in(a, b) -> evaleasy1bbin(a, b) [ 39 >= a ] (?, 1) evaleasy1bb3in(a, b) -> evaleasy1returnin(a, b) [ a >= 40 ] (?, 1) evaleasy1bbin(a, b) -> evaleasy1bb1in(a, b) [ b = 0 ] (?, 1) evaleasy1bbin(a, b) -> evaleasy1bb2in(a, b) [ 0 >= b + 1 ] (?, 1) evaleasy1bbin(a, b) -> evaleasy1bb2in(a, b) [ b >= 1 ] (?, 1) evaleasy1bb1in(a, b) -> evaleasy1bb3in(a + 1, b) (?, 1) evaleasy1bb2in(a, b) -> evaleasy1bb3in(a + 2, b) (?, 1) evaleasy1returnin(a, b) -> evaleasy1stop(a, b) start location: evaleasy1start leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem: 2: T: (1, 1) evaleasy1start(a, b) -> evaleasy1entryin(a, b) (?, 1) evaleasy1entryin(a, b) -> evaleasy1bb3in(0, b) (?, 1) evaleasy1bb3in(a, b) -> evaleasy1bbin(a, b) [ 39 >= a ] (?, 1) evaleasy1bbin(a, b) -> evaleasy1bb1in(a, b) [ b = 0 ] (?, 1) evaleasy1bbin(a, b) -> evaleasy1bb2in(a, b) [ 0 >= b + 1 ] (?, 1) evaleasy1bbin(a, b) -> evaleasy1bb2in(a, b) [ b >= 1 ] (?, 1) evaleasy1bb1in(a, b) -> evaleasy1bb3in(a + 1, b) (?, 1) evaleasy1bb2in(a, b) -> evaleasy1bb3in(a + 2, b) start location: evaleasy1start leaf cost: 2 Repeatedly propagating knowledge in problem 2 produces the following problem: 3: T: (1, 1) evaleasy1start(a, b) -> evaleasy1entryin(a, b) (1, 1) evaleasy1entryin(a, b) -> evaleasy1bb3in(0, b) (?, 1) evaleasy1bb3in(a, b) -> evaleasy1bbin(a, b) [ 39 >= a ] (?, 1) evaleasy1bbin(a, b) -> evaleasy1bb1in(a, b) [ b = 0 ] (?, 1) evaleasy1bbin(a, b) -> evaleasy1bb2in(a, b) [ 0 >= b + 1 ] (?, 1) evaleasy1bbin(a, b) -> evaleasy1bb2in(a, b) [ b >= 1 ] (?, 1) evaleasy1bb1in(a, b) -> evaleasy1bb3in(a + 1, b) (?, 1) evaleasy1bb2in(a, b) -> evaleasy1bb3in(a + 2, b) start location: evaleasy1start leaf cost: 2 A polynomial rank function with Pol(evaleasy1start) = 118 Pol(evaleasy1entryin) = 118 Pol(evaleasy1bb3in) = -3*V_1 + 118 Pol(evaleasy1bbin) = -3*V_1 + 117 Pol(evaleasy1bb1in) = -3*V_1 + 116 Pol(evaleasy1bb2in) = -3*V_1 + 116 orients all transitions weakly and the transition evaleasy1bb3in(a, b) -> evaleasy1bbin(a, b) [ 39 >= a ] strictly and produces the following problem: 4: T: (1, 1) evaleasy1start(a, b) -> evaleasy1entryin(a, b) (1, 1) evaleasy1entryin(a, b) -> evaleasy1bb3in(0, b) (118, 1) evaleasy1bb3in(a, b) -> evaleasy1bbin(a, b) [ 39 >= a ] (?, 1) evaleasy1bbin(a, b) -> evaleasy1bb1in(a, b) [ b = 0 ] (?, 1) evaleasy1bbin(a, b) -> evaleasy1bb2in(a, b) [ 0 >= b + 1 ] (?, 1) evaleasy1bbin(a, b) -> evaleasy1bb2in(a, b) [ b >= 1 ] (?, 1) evaleasy1bb1in(a, b) -> evaleasy1bb3in(a + 1, b) (?, 1) evaleasy1bb2in(a, b) -> evaleasy1bb3in(a + 2, b) start location: evaleasy1start leaf cost: 2 Repeatedly propagating knowledge in problem 4 produces the following problem: 5: T: (1, 1) evaleasy1start(a, b) -> evaleasy1entryin(a, b) (1, 1) evaleasy1entryin(a, b) -> evaleasy1bb3in(0, b) (118, 1) evaleasy1bb3in(a, b) -> evaleasy1bbin(a, b) [ 39 >= a ] (118, 1) evaleasy1bbin(a, b) -> evaleasy1bb1in(a, b) [ b = 0 ] (118, 1) evaleasy1bbin(a, b) -> evaleasy1bb2in(a, b) [ 0 >= b + 1 ] (118, 1) evaleasy1bbin(a, b) -> evaleasy1bb2in(a, b) [ b >= 1 ] (118, 1) evaleasy1bb1in(a, b) -> evaleasy1bb3in(a + 1, b) (236, 1) evaleasy1bb2in(a, b) -> evaleasy1bb3in(a + 2, b) start location: evaleasy1start leaf cost: 2 Complexity upper bound 830 Time: 0.190 sec (SMT: 0.181 sec)