YES(?, 30*b + 12*b*d + 8*d + 24) Initial complexity problem: 1: T: (1, 1) evalfstart(a, b, c, d) -> evalfentryin(a, b, c, d) (?, 1) evalfentryin(a, b, c, d) -> evalfbb4in(1, b, c, d) (?, 1) evalfbb4in(a, b, c, d) -> evalfbb2in(a, b, 1, d) [ b >= a ] (?, 1) evalfbb4in(a, b, c, d) -> evalfreturnin(a, b, c, d) [ a >= b + 1 ] (?, 1) evalfbb2in(a, b, c, d) -> evalfbb1in(a, b, c, d) [ d >= c ] (?, 1) evalfbb2in(a, b, c, d) -> evalfbb3in(a, b, c, d) [ c >= d + 1 ] (?, 1) evalfbb1in(a, b, c, d) -> evalfbb2in(a, b, c + 1, d) (?, 1) evalfbb3in(a, b, c, d) -> evalfbb4in(a + 1, b, c, d) (?, 1) evalfreturnin(a, b, c, d) -> evalfstop(a, b, c, d) start location: evalfstart leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem: 2: T: (1, 1) evalfstart(a, b, c, d) -> evalfentryin(a, b, c, d) (?, 1) evalfentryin(a, b, c, d) -> evalfbb4in(1, b, c, d) (?, 1) evalfbb4in(a, b, c, d) -> evalfbb2in(a, b, 1, d) [ b >= a ] (?, 1) evalfbb2in(a, b, c, d) -> evalfbb1in(a, b, c, d) [ d >= c ] (?, 1) evalfbb2in(a, b, c, d) -> evalfbb3in(a, b, c, d) [ c >= d + 1 ] (?, 1) evalfbb1in(a, b, c, d) -> evalfbb2in(a, b, c + 1, d) (?, 1) evalfbb3in(a, b, c, d) -> evalfbb4in(a + 1, b, c, d) start location: evalfstart leaf cost: 2 Repeatedly propagating knowledge in problem 2 produces the following problem: 3: T: (1, 1) evalfstart(a, b, c, d) -> evalfentryin(a, b, c, d) (1, 1) evalfentryin(a, b, c, d) -> evalfbb4in(1, b, c, d) (?, 1) evalfbb4in(a, b, c, d) -> evalfbb2in(a, b, 1, d) [ b >= a ] (?, 1) evalfbb2in(a, b, c, d) -> evalfbb1in(a, b, c, d) [ d >= c ] (?, 1) evalfbb2in(a, b, c, d) -> evalfbb3in(a, b, c, d) [ c >= d + 1 ] (?, 1) evalfbb1in(a, b, c, d) -> evalfbb2in(a, b, c + 1, d) (?, 1) evalfbb3in(a, b, c, d) -> evalfbb4in(a + 1, b, c, d) start location: evalfstart leaf cost: 2 A polynomial rank function with Pol(evalfstart) = 3*V_2 - 2 Pol(evalfentryin) = 3*V_2 - 2 Pol(evalfbb4in) = -3*V_1 + 3*V_2 + 1 Pol(evalfbb2in) = -3*V_1 + 3*V_2 Pol(evalfbb1in) = -3*V_1 + 3*V_2 Pol(evalfbb3in) = -3*V_1 + 3*V_2 - 1 orients all transitions weakly and the transition evalfbb4in(a, b, c, d) -> evalfbb2in(a, b, 1, d) [ b >= a ] strictly and produces the following problem: 4: T: (1, 1) evalfstart(a, b, c, d) -> evalfentryin(a, b, c, d) (1, 1) evalfentryin(a, b, c, d) -> evalfbb4in(1, b, c, d) (3*b + 2, 1) evalfbb4in(a, b, c, d) -> evalfbb2in(a, b, 1, d) [ b >= a ] (?, 1) evalfbb2in(a, b, c, d) -> evalfbb1in(a, b, c, d) [ d >= c ] (?, 1) evalfbb2in(a, b, c, d) -> evalfbb3in(a, b, c, d) [ c >= d + 1 ] (?, 1) evalfbb1in(a, b, c, d) -> evalfbb2in(a, b, c + 1, d) (?, 1) evalfbb3in(a, b, c, d) -> evalfbb4in(a + 1, b, c, d) start location: evalfstart leaf cost: 2 A polynomial rank function with Pol(evalfbb3in) = 1 Pol(evalfbb4in) = 0 Pol(evalfbb2in) = 2 Pol(evalfbb1in) = 2 and size complexities S("evalfbb3in(a, b, c, d) -> evalfbb4in(a + 1, b, c, d)", 0-0) = ? S("evalfbb3in(a, b, c, d) -> evalfbb4in(a + 1, b, c, d)", 0-1) = b S("evalfbb3in(a, b, c, d) -> evalfbb4in(a + 1, b, c, d)", 0-2) = ? S("evalfbb3in(a, b, c, d) -> evalfbb4in(a + 1, b, c, d)", 0-3) = d S("evalfbb1in(a, b, c, d) -> evalfbb2in(a, b, c + 1, d)", 0-0) = ? S("evalfbb1in(a, b, c, d) -> evalfbb2in(a, b, c + 1, d)", 0-1) = b S("evalfbb1in(a, b, c, d) -> evalfbb2in(a, b, c + 1, d)", 0-2) = ? S("evalfbb1in(a, b, c, d) -> evalfbb2in(a, b, c + 1, d)", 0-3) = d S("evalfbb2in(a, b, c, d) -> evalfbb3in(a, b, c, d) [ c >= d + 1 ]", 0-0) = ? S("evalfbb2in(a, b, c, d) -> evalfbb3in(a, b, c, d) [ c >= d + 1 ]", 0-1) = b S("evalfbb2in(a, b, c, d) -> evalfbb3in(a, b, c, d) [ c >= d + 1 ]", 0-2) = ? S("evalfbb2in(a, b, c, d) -> evalfbb3in(a, b, c, d) [ c >= d + 1 ]", 0-3) = d S("evalfbb2in(a, b, c, d) -> evalfbb1in(a, b, c, d) [ d >= c ]", 0-0) = ? S("evalfbb2in(a, b, c, d) -> evalfbb1in(a, b, c, d) [ d >= c ]", 0-1) = b S("evalfbb2in(a, b, c, d) -> evalfbb1in(a, b, c, d) [ d >= c ]", 0-2) = ? S("evalfbb2in(a, b, c, d) -> evalfbb1in(a, b, c, d) [ d >= c ]", 0-3) = d S("evalfbb4in(a, b, c, d) -> evalfbb2in(a, b, 1, d) [ b >= a ]", 0-0) = ? S("evalfbb4in(a, b, c, d) -> evalfbb2in(a, b, 1, d) [ b >= a ]", 0-1) = b S("evalfbb4in(a, b, c, d) -> evalfbb2in(a, b, 1, d) [ b >= a ]", 0-2) = 1 S("evalfbb4in(a, b, c, d) -> evalfbb2in(a, b, 1, d) [ b >= a ]", 0-3) = d S("evalfentryin(a, b, c, d) -> evalfbb4in(1, b, c, d)", 0-0) = 1 S("evalfentryin(a, b, c, d) -> evalfbb4in(1, b, c, d)", 0-1) = b S("evalfentryin(a, b, c, d) -> evalfbb4in(1, b, c, d)", 0-2) = c S("evalfentryin(a, b, c, d) -> evalfbb4in(1, b, c, d)", 0-3) = d S("evalfstart(a, b, c, d) -> evalfentryin(a, b, c, d)", 0-0) = a S("evalfstart(a, b, c, d) -> evalfentryin(a, b, c, d)", 0-1) = b S("evalfstart(a, b, c, d) -> evalfentryin(a, b, c, d)", 0-2) = c S("evalfstart(a, b, c, d) -> evalfentryin(a, b, c, d)", 0-3) = d orients the transitions evalfbb3in(a, b, c, d) -> evalfbb4in(a + 1, b, c, d) evalfbb2in(a, b, c, d) -> evalfbb3in(a, b, c, d) [ c >= d + 1 ] evalfbb2in(a, b, c, d) -> evalfbb1in(a, b, c, d) [ d >= c ] evalfbb1in(a, b, c, d) -> evalfbb2in(a, b, c + 1, d) weakly and the transition evalfbb3in(a, b, c, d) -> evalfbb4in(a + 1, b, c, d) strictly and produces the following problem: 5: T: (1, 1) evalfstart(a, b, c, d) -> evalfentryin(a, b, c, d) (1, 1) evalfentryin(a, b, c, d) -> evalfbb4in(1, b, c, d) (3*b + 2, 1) evalfbb4in(a, b, c, d) -> evalfbb2in(a, b, 1, d) [ b >= a ] (?, 1) evalfbb2in(a, b, c, d) -> evalfbb1in(a, b, c, d) [ d >= c ] (?, 1) evalfbb2in(a, b, c, d) -> evalfbb3in(a, b, c, d) [ c >= d + 1 ] (?, 1) evalfbb1in(a, b, c, d) -> evalfbb2in(a, b, c + 1, d) (6*b + 4, 1) evalfbb3in(a, b, c, d) -> evalfbb4in(a + 1, b, c, d) start location: evalfstart leaf cost: 2 A polynomial rank function with Pol(evalfbb2in) = 1 Pol(evalfbb3in) = 0 Pol(evalfbb1in) = 1 and size complexities S("evalfbb3in(a, b, c, d) -> evalfbb4in(a + 1, b, c, d)", 0-0) = 6*b + 180 S("evalfbb3in(a, b, c, d) -> evalfbb4in(a + 1, b, c, d)", 0-1) = b S("evalfbb3in(a, b, c, d) -> evalfbb4in(a + 1, b, c, d)", 0-2) = ? S("evalfbb3in(a, b, c, d) -> evalfbb4in(a + 1, b, c, d)", 0-3) = d S("evalfbb1in(a, b, c, d) -> evalfbb2in(a, b, c + 1, d)", 0-0) = 6*b + 180 S("evalfbb1in(a, b, c, d) -> evalfbb2in(a, b, c + 1, d)", 0-1) = b S("evalfbb1in(a, b, c, d) -> evalfbb2in(a, b, c + 1, d)", 0-2) = ? S("evalfbb1in(a, b, c, d) -> evalfbb2in(a, b, c + 1, d)", 0-3) = d S("evalfbb2in(a, b, c, d) -> evalfbb3in(a, b, c, d) [ c >= d + 1 ]", 0-0) = 6*b + 180 S("evalfbb2in(a, b, c, d) -> evalfbb3in(a, b, c, d) [ c >= d + 1 ]", 0-1) = b S("evalfbb2in(a, b, c, d) -> evalfbb3in(a, b, c, d) [ c >= d + 1 ]", 0-2) = ? S("evalfbb2in(a, b, c, d) -> evalfbb3in(a, b, c, d) [ c >= d + 1 ]", 0-3) = d S("evalfbb2in(a, b, c, d) -> evalfbb1in(a, b, c, d) [ d >= c ]", 0-0) = 6*b + 180 S("evalfbb2in(a, b, c, d) -> evalfbb1in(a, b, c, d) [ d >= c ]", 0-1) = b S("evalfbb2in(a, b, c, d) -> evalfbb1in(a, b, c, d) [ d >= c ]", 0-2) = ? S("evalfbb2in(a, b, c, d) -> evalfbb1in(a, b, c, d) [ d >= c ]", 0-3) = d S("evalfbb4in(a, b, c, d) -> evalfbb2in(a, b, 1, d) [ b >= a ]", 0-0) = 6*b + 180 S("evalfbb4in(a, b, c, d) -> evalfbb2in(a, b, 1, d) [ b >= a ]", 0-1) = b S("evalfbb4in(a, b, c, d) -> evalfbb2in(a, b, 1, d) [ b >= a ]", 0-2) = 1 S("evalfbb4in(a, b, c, d) -> evalfbb2in(a, b, 1, d) [ b >= a ]", 0-3) = d S("evalfentryin(a, b, c, d) -> evalfbb4in(1, b, c, d)", 0-0) = 1 S("evalfentryin(a, b, c, d) -> evalfbb4in(1, b, c, d)", 0-1) = b S("evalfentryin(a, b, c, d) -> evalfbb4in(1, b, c, d)", 0-2) = c S("evalfentryin(a, b, c, d) -> evalfbb4in(1, b, c, d)", 0-3) = d S("evalfstart(a, b, c, d) -> evalfentryin(a, b, c, d)", 0-0) = a S("evalfstart(a, b, c, d) -> evalfentryin(a, b, c, d)", 0-1) = b S("evalfstart(a, b, c, d) -> evalfentryin(a, b, c, d)", 0-2) = c S("evalfstart(a, b, c, d) -> evalfentryin(a, b, c, d)", 0-3) = d orients the transitions evalfbb2in(a, b, c, d) -> evalfbb3in(a, b, c, d) [ c >= d + 1 ] evalfbb2in(a, b, c, d) -> evalfbb1in(a, b, c, d) [ d >= c ] evalfbb1in(a, b, c, d) -> evalfbb2in(a, b, c + 1, d) weakly and the transition evalfbb2in(a, b, c, d) -> evalfbb3in(a, b, c, d) [ c >= d + 1 ] strictly and produces the following problem: 6: T: (1, 1) evalfstart(a, b, c, d) -> evalfentryin(a, b, c, d) (1, 1) evalfentryin(a, b, c, d) -> evalfbb4in(1, b, c, d) (3*b + 2, 1) evalfbb4in(a, b, c, d) -> evalfbb2in(a, b, 1, d) [ b >= a ] (?, 1) evalfbb2in(a, b, c, d) -> evalfbb1in(a, b, c, d) [ d >= c ] (3*b + 2, 1) evalfbb2in(a, b, c, d) -> evalfbb3in(a, b, c, d) [ c >= d + 1 ] (?, 1) evalfbb1in(a, b, c, d) -> evalfbb2in(a, b, c + 1, d) (6*b + 4, 1) evalfbb3in(a, b, c, d) -> evalfbb4in(a + 1, b, c, d) start location: evalfstart leaf cost: 2 A polynomial rank function with Pol(evalfbb2in) = -2*V_3 + 2*V_4 + 1 Pol(evalfbb1in) = -2*V_3 + 2*V_4 and size complexities S("evalfbb3in(a, b, c, d) -> evalfbb4in(a + 1, b, c, d)", 0-0) = 6*b + 180 S("evalfbb3in(a, b, c, d) -> evalfbb4in(a + 1, b, c, d)", 0-1) = b S("evalfbb3in(a, b, c, d) -> evalfbb4in(a + 1, b, c, d)", 0-2) = ? S("evalfbb3in(a, b, c, d) -> evalfbb4in(a + 1, b, c, d)", 0-3) = d S("evalfbb1in(a, b, c, d) -> evalfbb2in(a, b, c + 1, d)", 0-0) = 6*b + 180 S("evalfbb1in(a, b, c, d) -> evalfbb2in(a, b, c + 1, d)", 0-1) = b S("evalfbb1in(a, b, c, d) -> evalfbb2in(a, b, c + 1, d)", 0-2) = ? S("evalfbb1in(a, b, c, d) -> evalfbb2in(a, b, c + 1, d)", 0-3) = d S("evalfbb2in(a, b, c, d) -> evalfbb3in(a, b, c, d) [ c >= d + 1 ]", 0-0) = 6*b + 180 S("evalfbb2in(a, b, c, d) -> evalfbb3in(a, b, c, d) [ c >= d + 1 ]", 0-1) = b S("evalfbb2in(a, b, c, d) -> evalfbb3in(a, b, c, d) [ c >= d + 1 ]", 0-2) = ? S("evalfbb2in(a, b, c, d) -> evalfbb3in(a, b, c, d) [ c >= d + 1 ]", 0-3) = d S("evalfbb2in(a, b, c, d) -> evalfbb1in(a, b, c, d) [ d >= c ]", 0-0) = 6*b + 180 S("evalfbb2in(a, b, c, d) -> evalfbb1in(a, b, c, d) [ d >= c ]", 0-1) = b S("evalfbb2in(a, b, c, d) -> evalfbb1in(a, b, c, d) [ d >= c ]", 0-2) = ? S("evalfbb2in(a, b, c, d) -> evalfbb1in(a, b, c, d) [ d >= c ]", 0-3) = d S("evalfbb4in(a, b, c, d) -> evalfbb2in(a, b, 1, d) [ b >= a ]", 0-0) = 6*b + 180 S("evalfbb4in(a, b, c, d) -> evalfbb2in(a, b, 1, d) [ b >= a ]", 0-1) = b S("evalfbb4in(a, b, c, d) -> evalfbb2in(a, b, 1, d) [ b >= a ]", 0-2) = 1 S("evalfbb4in(a, b, c, d) -> evalfbb2in(a, b, 1, d) [ b >= a ]", 0-3) = d S("evalfentryin(a, b, c, d) -> evalfbb4in(1, b, c, d)", 0-0) = 1 S("evalfentryin(a, b, c, d) -> evalfbb4in(1, b, c, d)", 0-1) = b S("evalfentryin(a, b, c, d) -> evalfbb4in(1, b, c, d)", 0-2) = c S("evalfentryin(a, b, c, d) -> evalfbb4in(1, b, c, d)", 0-3) = d S("evalfstart(a, b, c, d) -> evalfentryin(a, b, c, d)", 0-0) = a S("evalfstart(a, b, c, d) -> evalfentryin(a, b, c, d)", 0-1) = b S("evalfstart(a, b, c, d) -> evalfentryin(a, b, c, d)", 0-2) = c S("evalfstart(a, b, c, d) -> evalfentryin(a, b, c, d)", 0-3) = d orients the transitions evalfbb2in(a, b, c, d) -> evalfbb1in(a, b, c, d) [ d >= c ] evalfbb1in(a, b, c, d) -> evalfbb2in(a, b, c + 1, d) weakly and the transition evalfbb2in(a, b, c, d) -> evalfbb1in(a, b, c, d) [ d >= c ] strictly and produces the following problem: 7: T: (1, 1) evalfstart(a, b, c, d) -> evalfentryin(a, b, c, d) (1, 1) evalfentryin(a, b, c, d) -> evalfbb4in(1, b, c, d) (3*b + 2, 1) evalfbb4in(a, b, c, d) -> evalfbb2in(a, b, 1, d) [ b >= a ] (6*b*d + 4*d + 9*b + 6, 1) evalfbb2in(a, b, c, d) -> evalfbb1in(a, b, c, d) [ d >= c ] (3*b + 2, 1) evalfbb2in(a, b, c, d) -> evalfbb3in(a, b, c, d) [ c >= d + 1 ] (?, 1) evalfbb1in(a, b, c, d) -> evalfbb2in(a, b, c + 1, d) (6*b + 4, 1) evalfbb3in(a, b, c, d) -> evalfbb4in(a + 1, b, c, d) start location: evalfstart leaf cost: 2 Repeatedly propagating knowledge in problem 7 produces the following problem: 8: T: (1, 1) evalfstart(a, b, c, d) -> evalfentryin(a, b, c, d) (1, 1) evalfentryin(a, b, c, d) -> evalfbb4in(1, b, c, d) (3*b + 2, 1) evalfbb4in(a, b, c, d) -> evalfbb2in(a, b, 1, d) [ b >= a ] (6*b*d + 4*d + 9*b + 6, 1) evalfbb2in(a, b, c, d) -> evalfbb1in(a, b, c, d) [ d >= c ] (3*b + 2, 1) evalfbb2in(a, b, c, d) -> evalfbb3in(a, b, c, d) [ c >= d + 1 ] (6*b*d + 4*d + 9*b + 6, 1) evalfbb1in(a, b, c, d) -> evalfbb2in(a, b, c + 1, d) (6*b + 4, 1) evalfbb3in(a, b, c, d) -> evalfbb4in(a + 1, b, c, d) start location: evalfstart leaf cost: 2 Complexity upper bound 30*b + 12*b*d + 8*d + 24 Time: 0.216 sec (SMT: 0.202 sec)