YES(?, 7871239044*a + 11971777242*a*b + 1956402522*b + 19048810500*a^2*b + 12342906160*a^2 + 7748780184*a^2*b^2 + 4684436784*a*b^2 + 754235928*b^2 + 2245017312*a^3*b + 1128961152*a^3 + 1470368160*a^3*b^2 + 58765824*a^4*b^2 + 65138688*a^4*b + 23141376*a^4*b^3 + 322206336*a^3*b^3 + 306778752*a^2*b^3 + 100545408*a*b^3 + 26615808*a^4 + 3359232*a^4*b^4 + 4478976*a^3*b^4 + 2239488*a^2*b^4 + 497664*a*b^4 + 41472*b^4 + 11076480*b^3 + 1293797120) Initial complexity problem: 1: T: (1, 1) evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e) (?, 1) evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e) (?, 1) evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ] (?, 1) evalfbb10in(a, b, c, d, e) -> evalfreturnin(a, b, c, d, e) [ 0 >= b ] (?, 1) evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ] (?, 1) evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ] (?, 1) evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ] (?, 1) evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ] (?, 1) evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ] (?, 1) evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ] (?, 1) evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1) (?, 1) evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e) (?, 1) evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e) (?, 1) evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e) (?, 1) evalfreturnin(a, b, c, d, e) -> evalfstop(a, b, c, d, e) 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, e) -> evalfentryin(a, b, c, d, e) (?, 1) evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e) (?, 1) evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ] (?, 1) evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ] (?, 1) evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ] (?, 1) evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ] (?, 1) evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ] (?, 1) evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ] (?, 1) evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ] (?, 1) evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1) (?, 1) evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e) (?, 1) evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e) (?, 1) evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e) 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, e) -> evalfentryin(a, b, c, d, e) (1, 1) evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e) (?, 1) evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ] (?, 1) evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ] (?, 1) evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ] (?, 1) evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ] (?, 1) evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ] (?, 1) evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ] (?, 1) evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ] (?, 1) evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1) (?, 1) evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e) (?, 1) evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e) (?, 1) evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e) start location: evalfstart leaf cost: 2 A polynomial rank function with Pol(evalfstart) = 3*V_1 + 1 Pol(evalfentryin) = 3*V_1 + 1 Pol(evalfbb10in) = 3*V_2 + 1 Pol(evalfbb8in) = 3*V_2 Pol(evalfbb6in) = 3*V_2 Pol(evalfbb9in) = 3*V_2 - 1 Pol(evalfbb4in) = 3*V_2 Pol(evalfbb7in) = 3*V_2 Pol(evalfbb3in) = 3*V_2 Pol(evalfbb5in) = 3*V_2 orients all transitions weakly and the transition evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ] strictly and produces the following problem: 4: T: (1, 1) evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e) (1, 1) evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e) (3*a + 1, 1) evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ] (?, 1) evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ] (?, 1) evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ] (?, 1) evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ] (?, 1) evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ] (?, 1) evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ] (?, 1) evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ] (?, 1) evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1) (?, 1) evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e) (?, 1) evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e) (?, 1) evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e) start location: evalfstart leaf cost: 2 A polynomial rank function with Pol(evalfbb9in) = 1 Pol(evalfbb10in) = 0 Pol(evalfbb8in) = 2 Pol(evalfbb6in) = 2 Pol(evalfbb7in) = 2 Pol(evalfbb4in) = 2 Pol(evalfbb5in) = 2 Pol(evalfbb3in) = 2 and size complexities S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-0) = b S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-1) = ? S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-2) = ? S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-3) = ? S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-4) = ? S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-0) = b S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-1) = ? S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-2) = ? S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-3) = ? S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-4) = ? S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-0) = b S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-1) = ? S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-2) = ? S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-3) = ? S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-4) = ? S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-0) = b S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-1) = ? S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-2) = ? S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-3) = ? S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-4) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-0) = b S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-1) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-2) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-3) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-4) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-0) = b S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-1) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-2) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-3) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-4) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-0) = b S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-1) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-2) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-3) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-4) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-0) = b S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-1) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-2) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-3) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-4) = 1 S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-0) = b S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-1) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-2) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-3) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-4) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-0) = b S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-1) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-2) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-3) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-4) = ? S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-0) = b S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-1) = ? S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-2) = 1 S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-3) = ? S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-4) = ? S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-0) = b S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-1) = a S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-2) = c S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-3) = d S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-4) = e S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-0) = a S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-1) = b S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-2) = c S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-3) = d S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-4) = e orients the transitions evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e) evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ] evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ] evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e) evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ] evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ] evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e) evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ] evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ] evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1) weakly and the transition evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e) strictly and produces the following problem: 5: T: (1, 1) evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e) (1, 1) evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e) (3*a + 1, 1) evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ] (?, 1) evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ] (?, 1) evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ] (?, 1) evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ] (?, 1) evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ] (?, 1) evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ] (?, 1) evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ] (?, 1) evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1) (?, 1) evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e) (?, 1) evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e) (6*a + 2, 1) evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e) start location: evalfstart leaf cost: 2 A polynomial rank function with Pol(evalfbb8in) = 1 Pol(evalfbb9in) = 0 Pol(evalfbb6in) = 1 Pol(evalfbb7in) = 1 Pol(evalfbb4in) = 1 Pol(evalfbb5in) = 1 Pol(evalfbb3in) = 1 and size complexities S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-0) = b S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-1) = 7*a + 98 S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-2) = ? S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-3) = ? S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-4) = ? S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-0) = b S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-1) = 7*a + 98 S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-2) = ? S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-3) = ? S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-4) = ? S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-0) = b S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-1) = 7*a + 98 S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-2) = ? S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-3) = ? S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-4) = ? S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-0) = b S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-1) = 7*a + 98 S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-2) = ? S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-3) = ? S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-4) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-0) = b S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-1) = 7*a + 98 S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-2) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-3) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-4) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-0) = b S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-1) = 7*a + 98 S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-2) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-3) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-4) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-0) = b S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-1) = 7*a + 98 S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-2) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-3) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-4) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-0) = b S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-1) = 7*a + 98 S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-2) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-3) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-4) = 1 S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-0) = b S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-1) = 7*a + 98 S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-2) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-3) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-4) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-0) = b S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-1) = 7*a + 98 S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-2) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-3) = 7*a + 686 S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-4) = ? S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-0) = b S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-1) = 7*a + 98 S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-2) = 1 S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-3) = ? S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-4) = ? S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-0) = b S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-1) = a S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-2) = c S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-3) = d S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-4) = e S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-0) = a S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-1) = b S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-2) = c S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-3) = d S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-4) = e orients the transitions evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ] evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ] evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e) evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ] evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ] evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e) evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ] evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ] evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1) weakly and the transition evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ] strictly and produces the following problem: 6: T: (1, 1) evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e) (1, 1) evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e) (3*a + 1, 1) evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ] (?, 1) evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ] (3*a + 1, 1) evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ] (?, 1) evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ] (?, 1) evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ] (?, 1) evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ] (?, 1) evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ] (?, 1) evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1) (?, 1) evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e) (?, 1) evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e) (6*a + 2, 1) evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e) start location: evalfstart leaf cost: 2 A polynomial rank function with Pol(evalfbb8in) = 3*V_1 - 3*V_3 + 1 Pol(evalfbb6in) = 3*V_1 - 3*V_3 Pol(evalfbb7in) = 3*V_1 - 3*V_3 - 1 Pol(evalfbb4in) = 3*V_1 - 3*V_3 Pol(evalfbb5in) = 3*V_1 - 3*V_3 Pol(evalfbb3in) = 3*V_1 - 3*V_3 and size complexities S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-0) = b S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-1) = 7*a + 98 S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-2) = ? S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-3) = ? S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-4) = ? S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-0) = b S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-1) = 7*a + 98 S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-2) = ? S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-3) = ? S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-4) = ? S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-0) = b S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-1) = 7*a + 98 S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-2) = ? S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-3) = ? S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-4) = ? S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-0) = b S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-1) = 7*a + 98 S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-2) = ? S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-3) = ? S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-4) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-0) = b S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-1) = 7*a + 98 S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-2) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-3) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-4) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-0) = b S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-1) = 7*a + 98 S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-2) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-3) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-4) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-0) = b S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-1) = 7*a + 98 S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-2) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-3) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-4) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-0) = b S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-1) = 7*a + 98 S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-2) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-3) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-4) = 1 S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-0) = b S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-1) = 7*a + 98 S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-2) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-3) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-4) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-0) = b S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-1) = 7*a + 98 S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-2) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-3) = 7*a + 686 S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-4) = ? S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-0) = b S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-1) = 7*a + 98 S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-2) = 1 S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-3) = ? S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-4) = ? S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-0) = b S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-1) = a S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-2) = c S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-3) = d S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-4) = e S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-0) = a S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-1) = b S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-2) = c S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-3) = d S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-4) = e orients the transitions evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ] evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e) evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ] evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ] evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e) evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ] evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ] evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1) weakly and the transition evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ] strictly and produces the following problem: 7: T: (1, 1) evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e) (1, 1) evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e) (3*a + 1, 1) evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ] (9*a*b + 3*b + 12*a + 4, 1) evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ] (3*a + 1, 1) evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ] (?, 1) evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ] (?, 1) evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ] (?, 1) evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ] (?, 1) evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ] (?, 1) evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1) (?, 1) evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e) (?, 1) evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e) (6*a + 2, 1) evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e) start location: evalfstart leaf cost: 2 A polynomial rank function with Pol(evalfbb7in) = 1 Pol(evalfbb8in) = 0 Pol(evalfbb6in) = 2 Pol(evalfbb4in) = 2 Pol(evalfbb5in) = 2 Pol(evalfbb3in) = 2 and size complexities S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-0) = b S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-1) = 7*a + 98 S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-2) = ? S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-3) = ? S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-4) = ? S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-0) = b S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-1) = 7*a + 98 S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-2) = ? S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-3) = ? S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-4) = ? S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-0) = b S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-1) = 7*a + 98 S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-2) = ? S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-3) = ? S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-4) = ? S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-0) = b S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-1) = 7*a + 98 S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-2) = ? S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-3) = ? S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-4) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-0) = b S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-1) = 7*a + 98 S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-2) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-3) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-4) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-0) = b S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-1) = 7*a + 98 S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-2) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-3) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-4) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-0) = b S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-1) = 7*a + 98 S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-2) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-3) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-4) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-0) = b S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-1) = 7*a + 98 S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-2) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-3) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-4) = 1 S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-0) = b S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-1) = 7*a + 98 S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-2) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-3) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-4) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-0) = b S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-1) = 7*a + 98 S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-2) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-3) = 7*a + 686 S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-4) = ? S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-0) = b S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-1) = 7*a + 98 S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-2) = 1 S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-3) = ? S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-4) = ? S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-0) = b S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-1) = a S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-2) = c S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-3) = d S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-4) = e S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-0) = a S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-1) = b S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-2) = c S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-3) = d S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-4) = e orients the transitions evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e) evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ] evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ] evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e) evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ] evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ] evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1) weakly and the transition evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e) strictly and produces the following problem: 8: T: (1, 1) evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e) (1, 1) evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e) (3*a + 1, 1) evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ] (9*a*b + 3*b + 12*a + 4, 1) evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ] (3*a + 1, 1) evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ] (?, 1) evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ] (?, 1) evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ] (?, 1) evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ] (?, 1) evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ] (?, 1) evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1) (?, 1) evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e) (18*a*b + 6*b + 24*a + 8, 1) evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e) (6*a + 2, 1) evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e) start location: evalfstart leaf cost: 2 A polynomial rank function with Pol(evalfbb6in) = 1 Pol(evalfbb7in) = 0 Pol(evalfbb4in) = 1 Pol(evalfbb5in) = 1 Pol(evalfbb3in) = 1 and size complexities S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-0) = b S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-1) = 7*a + 98 S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-3) = ? S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-4) = ? S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-0) = b S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-1) = 7*a + 98 S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-3) = ? S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-4) = ? S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-0) = b S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-1) = 7*a + 98 S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-3) = ? S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-4) = ? S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-0) = b S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-1) = 7*a + 98 S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-3) = ? S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-4) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-0) = b S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-1) = 7*a + 98 S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-3) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-4) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-0) = b S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-1) = 7*a + 98 S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-3) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-4) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-0) = b S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-1) = 7*a + 98 S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-3) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-4) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-0) = b S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-1) = 7*a + 98 S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-3) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-4) = 1 S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-0) = b S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-1) = 7*a + 98 S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-3) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-4) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-0) = b S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-1) = 7*a + 98 S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-3) = 7*a + 686 S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-4) = ? S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-0) = b S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-1) = 7*a + 98 S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-2) = 1 S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-3) = ? S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-4) = ? S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-0) = b S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-1) = a S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-2) = c S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-3) = d S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-4) = e S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-0) = a S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-1) = b S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-2) = c S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-3) = d S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-4) = e orients the transitions evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ] evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ] evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e) evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ] evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ] evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1) weakly and the transition evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ] strictly and produces the following problem: 9: T: (1, 1) evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e) (1, 1) evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e) (3*a + 1, 1) evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ] (9*a*b + 3*b + 12*a + 4, 1) evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ] (3*a + 1, 1) evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ] (?, 1) evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ] (9*a*b + 3*b + 12*a + 4, 1) evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ] (?, 1) evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ] (?, 1) evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ] (?, 1) evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1) (?, 1) evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e) (18*a*b + 6*b + 24*a + 8, 1) evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e) (6*a + 2, 1) evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e) start location: evalfstart leaf cost: 2 A polynomial rank function with Pol(evalfbb6in) = 4*V_2 + 4*V_3 - 4*V_4 + 1 Pol(evalfbb4in) = 4*V_2 + 4*V_3 - 4*V_4 - 1 Pol(evalfbb5in) = 4*V_2 + 4*V_3 - 4*V_4 - 2 Pol(evalfbb3in) = 4*V_2 + 4*V_3 - 4*V_4 - 1 and size complexities S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-0) = b S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-1) = 7*a + 98 S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-3) = ? S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-4) = ? S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-0) = b S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-1) = 7*a + 98 S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-3) = ? S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-4) = ? S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-0) = b S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-1) = 7*a + 98 S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-3) = ? S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-4) = ? S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-0) = b S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-1) = 7*a + 98 S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-3) = ? S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-4) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-0) = b S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-1) = 7*a + 98 S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-3) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-4) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-0) = b S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-1) = 7*a + 98 S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-3) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-4) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-0) = b S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-1) = 7*a + 98 S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-3) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-4) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-0) = b S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-1) = 7*a + 98 S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-3) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-4) = 1 S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-0) = b S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-1) = 7*a + 98 S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-3) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-4) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-0) = b S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-1) = 7*a + 98 S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-3) = 7*a + 686 S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-4) = ? S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-0) = b S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-1) = 7*a + 98 S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-2) = 1 S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-3) = ? S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-4) = ? S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-0) = b S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-1) = a S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-2) = c S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-3) = d S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-4) = e S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-0) = a S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-1) = b S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-2) = c S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-3) = d S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-4) = e orients the transitions evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ] evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e) evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ] evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ] evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1) weakly and the transition evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ] strictly and produces the following problem: 10: T: (1, 1) evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e) (1, 1) evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e) (3*a + 1, 1) evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ] (9*a*b + 3*b + 12*a + 4, 1) evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ] (3*a + 1, 1) evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ] (2232*a^2*b + 29589*a*b + 1824*a^2 + 648*a^2*b^2 + 432*a*b^2 + 72*b^2 + 38684*a + 9615*b + 12692, 1) evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ] (9*a*b + 3*b + 12*a + 4, 1) evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ] (?, 1) evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ] (?, 1) evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ] (?, 1) evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1) (?, 1) evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e) (18*a*b + 6*b + 24*a + 8, 1) evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e) (6*a + 2, 1) evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e) start location: evalfstart leaf cost: 2 A polynomial rank function with Pol(evalfbb5in) = 1 Pol(evalfbb6in) = 0 Pol(evalfbb4in) = 2 Pol(evalfbb3in) = 2 and size complexities S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-0) = b S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-1) = 7*a + 98 S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-3) = ? S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-4) = ? S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-0) = b S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-1) = 7*a + 98 S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-3) = ? S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-4) = ? S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-0) = b S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-1) = 7*a + 98 S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-3) = ? S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-4) = ? S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-0) = b S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-1) = 7*a + 98 S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-3) = ? S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-4) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-0) = b S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-1) = 7*a + 98 S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-3) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-4) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-0) = b S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-1) = 7*a + 98 S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-3) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-4) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-0) = b S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-1) = 7*a + 98 S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-3) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-4) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-0) = b S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-1) = 7*a + 98 S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-3) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-4) = 1 S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-0) = b S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-1) = 7*a + 98 S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-3) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-4) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-0) = b S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-1) = 7*a + 98 S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-3) = 7*a + 686 S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-4) = ? S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-0) = b S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-1) = 7*a + 98 S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-2) = 1 S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-3) = ? S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-4) = ? S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-0) = b S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-1) = a S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-2) = c S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-3) = d S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-4) = e S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-0) = a S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-1) = b S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-2) = c S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-3) = d S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-4) = e orients the transitions evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e) evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ] evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ] evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1) weakly and the transition evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e) strictly and produces the following problem: 11: T: (1, 1) evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e) (1, 1) evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e) (3*a + 1, 1) evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ] (9*a*b + 3*b + 12*a + 4, 1) evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ] (3*a + 1, 1) evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ] (2232*a^2*b + 29589*a*b + 1824*a^2 + 648*a^2*b^2 + 432*a*b^2 + 72*b^2 + 38684*a + 9615*b + 12692, 1) evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ] (9*a*b + 3*b + 12*a + 4, 1) evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ] (?, 1) evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ] (?, 1) evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ] (?, 1) evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1) (4464*a^2*b + 59178*a*b + 3648*a^2 + 1296*a^2*b^2 + 864*a*b^2 + 144*b^2 + 77368*a + 19230*b + 25384, 1) evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e) (18*a*b + 6*b + 24*a + 8, 1) evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e) (6*a + 2, 1) evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e) start location: evalfstart leaf cost: 2 A polynomial rank function with Pol(evalfbb4in) = 1 Pol(evalfbb5in) = 0 Pol(evalfbb3in) = 1 and size complexities S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-0) = b S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-1) = 7*a + 98 S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-3) = d + 77369*a + 4464*a^2*b + 59178*a*b + 3648*a^2 + 1296*a^2*b^2 + 864*a*b^2 + 144*b^2 + 19230*b + 25482 S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-4) = ? S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-0) = b S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-1) = 7*a + 98 S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-3) = 77369*a + 4464*a^2*b + 59178*a*b + 3648*a^2 + 1296*a^2*b^2 + 864*a*b^2 + 144*b^2 + 19230*b + 25482 S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-4) = ? S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-0) = b S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-1) = 7*a + 98 S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-3) = 77369*a + 4464*a^2*b + 59178*a*b + 3648*a^2 + 1296*a^2*b^2 + 864*a*b^2 + 144*b^2 + 19230*b + 25482 S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-4) = ? S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-0) = b S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-1) = 7*a + 98 S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-3) = 77369*a + 4464*a^2*b + 59178*a*b + 3648*a^2 + 1296*a^2*b^2 + 864*a*b^2 + 144*b^2 + 19230*b + 25482 S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-4) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-0) = b S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-1) = 7*a + 98 S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-3) = 77369*a + 4464*a^2*b + 59178*a*b + 3648*a^2 + 1296*a^2*b^2 + 864*a*b^2 + 144*b^2 + 19230*b + 25482 S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-4) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-0) = b S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-1) = 7*a + 98 S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-3) = 77369*a + 4464*a^2*b + 59178*a*b + 3648*a^2 + 1296*a^2*b^2 + 864*a*b^2 + 144*b^2 + 19230*b + 25482 S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-4) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-0) = b S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-1) = 7*a + 98 S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-3) = 77369*a + 4464*a^2*b + 59178*a*b + 3648*a^2 + 1296*a^2*b^2 + 864*a*b^2 + 144*b^2 + 19230*b + 25482 S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-4) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-0) = b S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-1) = 7*a + 98 S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-3) = 77369*a + 4464*a^2*b + 59178*a*b + 3648*a^2 + 1296*a^2*b^2 + 864*a*b^2 + 144*b^2 + 19230*b + 25482 S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-4) = 1 S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-0) = b S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-1) = 7*a + 98 S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-3) = d + 77369*a + 4464*a^2*b + 59178*a*b + 3648*a^2 + 1296*a^2*b^2 + 864*a*b^2 + 144*b^2 + 19230*b + 25482 S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-4) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-0) = b S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-1) = 7*a + 98 S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-3) = 7*a + 686 S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-4) = ? S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-0) = b S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-1) = 7*a + 98 S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-2) = 1 S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-3) = d + 77369*a + 4464*a^2*b + 59178*a*b + 3648*a^2 + 1296*a^2*b^2 + 864*a*b^2 + 144*b^2 + 19230*b + 25482 S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-4) = ? S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-0) = b S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-1) = a S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-2) = c S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-3) = d S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-4) = e S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-0) = a S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-1) = b S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-2) = c S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-3) = d S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-4) = e orients the transitions evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ] evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ] evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1) weakly and the transition evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ] strictly and produces the following problem: 12: T: (1, 1) evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e) (1, 1) evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e) (3*a + 1, 1) evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ] (9*a*b + 3*b + 12*a + 4, 1) evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ] (3*a + 1, 1) evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ] (2232*a^2*b + 29589*a*b + 1824*a^2 + 648*a^2*b^2 + 432*a*b^2 + 72*b^2 + 38684*a + 9615*b + 12692, 1) evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ] (9*a*b + 3*b + 12*a + 4, 1) evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ] (?, 1) evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ] (2232*a^2*b + 29589*a*b + 1824*a^2 + 648*a^2*b^2 + 432*a*b^2 + 72*b^2 + 38684*a + 9615*b + 12692, 1) evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ] (?, 1) evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1) (4464*a^2*b + 59178*a*b + 3648*a^2 + 1296*a^2*b^2 + 864*a*b^2 + 144*b^2 + 77368*a + 19230*b + 25384, 1) evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e) (18*a*b + 6*b + 24*a + 8, 1) evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e) (6*a + 2, 1) evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e) start location: evalfstart leaf cost: 2 A polynomial rank function with Pol(evalfbb4in) = 2*V_4 - 2*V_5 + 1 Pol(evalfbb3in) = 2*V_4 - 2*V_5 and size complexities S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-0) = b S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-1) = 7*a + 98 S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-3) = d + 77369*a + 4464*a^2*b + 59178*a*b + 3648*a^2 + 1296*a^2*b^2 + 864*a*b^2 + 144*b^2 + 19230*b + 25482 S("evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e)", 0-4) = ? S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-0) = b S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-1) = 7*a + 98 S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-3) = 77369*a + 4464*a^2*b + 59178*a*b + 3648*a^2 + 1296*a^2*b^2 + 864*a*b^2 + 144*b^2 + 19230*b + 25482 S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-4) = ? S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-0) = b S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-1) = 7*a + 98 S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-3) = 77369*a + 4464*a^2*b + 59178*a*b + 3648*a^2 + 1296*a^2*b^2 + 864*a*b^2 + 144*b^2 + 19230*b + 25482 S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-4) = ? S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-0) = b S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-1) = 7*a + 98 S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-3) = 77369*a + 4464*a^2*b + 59178*a*b + 3648*a^2 + 1296*a^2*b^2 + 864*a*b^2 + 144*b^2 + 19230*b + 25482 S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-4) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-0) = b S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-1) = 7*a + 98 S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-3) = 77369*a + 4464*a^2*b + 59178*a*b + 3648*a^2 + 1296*a^2*b^2 + 864*a*b^2 + 144*b^2 + 19230*b + 25482 S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-4) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-0) = b S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-1) = 7*a + 98 S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-3) = 77369*a + 4464*a^2*b + 59178*a*b + 3648*a^2 + 1296*a^2*b^2 + 864*a*b^2 + 144*b^2 + 19230*b + 25482 S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-4) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-0) = b S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-1) = 7*a + 98 S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-3) = 77369*a + 4464*a^2*b + 59178*a*b + 3648*a^2 + 1296*a^2*b^2 + 864*a*b^2 + 144*b^2 + 19230*b + 25482 S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ]", 0-4) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-0) = b S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-1) = 7*a + 98 S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-3) = 77369*a + 4464*a^2*b + 59178*a*b + 3648*a^2 + 1296*a^2*b^2 + 864*a*b^2 + 144*b^2 + 19230*b + 25482 S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ]", 0-4) = 1 S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-0) = b S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-1) = 7*a + 98 S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-3) = d + 77369*a + 4464*a^2*b + 59178*a*b + 3648*a^2 + 1296*a^2*b^2 + 864*a*b^2 + 144*b^2 + 19230*b + 25482 S("evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ]", 0-4) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-0) = b S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-1) = 7*a + 98 S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-2) = 18*a*b + 6*b + 24*a + 9 S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-3) = 7*a + 686 S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ]", 0-4) = ? S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-0) = b S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-1) = 7*a + 98 S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-2) = 1 S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-3) = d + 77369*a + 4464*a^2*b + 59178*a*b + 3648*a^2 + 1296*a^2*b^2 + 864*a*b^2 + 144*b^2 + 19230*b + 25482 S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ]", 0-4) = ? S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-0) = b S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-1) = a S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-2) = c S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-3) = d S("evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e)", 0-4) = e S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-0) = a S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-1) = b S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-2) = c S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-3) = d S("evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e)", 0-4) = e orients the transitions evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ] evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1) weakly and the transition evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ] strictly and produces the following problem: 13: T: (1, 1) evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e) (1, 1) evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e) (3*a + 1, 1) evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ] (9*a*b + 3*b + 12*a + 4, 1) evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ] (3*a + 1, 1) evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ] (2232*a^2*b + 29589*a*b + 1824*a^2 + 648*a^2*b^2 + 432*a*b^2 + 72*b^2 + 38684*a + 9615*b + 12692, 1) evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ] (9*a*b + 3*b + 12*a + 4, 1) evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ] (1122508656*a^3*b + 9524400786*a^2*b + 564480576*a^3 + 735184080*a^3*b^2 + 3874388796*a^2*b^2 + 2342217528*a*b^2 + 6171449432*a^2 + 5985829425*a*b + 29382912*a^4*b^2 + 32569344*a^4*b + 11570688*a^4*b^3 + 161103168*a^3*b^3 + 153389376*a^2*b^3 + 50272704*a*b^3 + 13307904*a^4 + 1679616*a^4*b^4 + 2239488*a^3*b^4 + 1119744*a^2*b^4 + 248832*a*b^4 + 20736*b^4 + 5538240*b^3 + 377117820*b^2 + 3935542124*a + 978182025*b + 646873164, 1) evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ] (2232*a^2*b + 29589*a*b + 1824*a^2 + 648*a^2*b^2 + 432*a*b^2 + 72*b^2 + 38684*a + 9615*b + 12692, 1) evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ] (?, 1) evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1) (4464*a^2*b + 59178*a*b + 3648*a^2 + 1296*a^2*b^2 + 864*a*b^2 + 144*b^2 + 77368*a + 19230*b + 25384, 1) evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e) (18*a*b + 6*b + 24*a + 8, 1) evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e) (6*a + 2, 1) evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e) start location: evalfstart leaf cost: 2 Repeatedly propagating knowledge in problem 13 produces the following problem: 14: T: (1, 1) evalfstart(a, b, c, d, e) -> evalfentryin(a, b, c, d, e) (1, 1) evalfentryin(a, b, c, d, e) -> evalfbb10in(b, a, c, d, e) (3*a + 1, 1) evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= 1 ] (9*a*b + 3*b + 12*a + 4, 1) evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, b, e) [ a >= c ] (3*a + 1, 1) evalfbb8in(a, b, c, d, e) -> evalfbb9in(a, b, c, d, e) [ c >= a + 1 ] (2232*a^2*b + 29589*a*b + 1824*a^2 + 648*a^2*b^2 + 432*a*b^2 + 72*b^2 + 38684*a + 9615*b + 12692, 1) evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b + c >= d ] (9*a*b + 3*b + 12*a + 4, 1) evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + c + 1 ] (1122508656*a^3*b + 9524400786*a^2*b + 564480576*a^3 + 735184080*a^3*b^2 + 3874388796*a^2*b^2 + 2342217528*a*b^2 + 6171449432*a^2 + 5985829425*a*b + 29382912*a^4*b^2 + 32569344*a^4*b + 11570688*a^4*b^3 + 161103168*a^3*b^3 + 153389376*a^2*b^3 + 50272704*a*b^3 + 13307904*a^4 + 1679616*a^4*b^4 + 2239488*a^3*b^4 + 1119744*a^2*b^4 + 248832*a*b^4 + 20736*b^4 + 5538240*b^3 + 377117820*b^2 + 3935542124*a + 978182025*b + 646873164, 1) evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ] (2232*a^2*b + 29589*a*b + 1824*a^2 + 648*a^2*b^2 + 432*a*b^2 + 72*b^2 + 38684*a + 9615*b + 12692, 1) evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ] (1122508656*a^3*b + 9524400786*a^2*b + 564480576*a^3 + 735184080*a^3*b^2 + 3874388796*a^2*b^2 + 2342217528*a*b^2 + 6171449432*a^2 + 5985829425*a*b + 29382912*a^4*b^2 + 32569344*a^4*b + 11570688*a^4*b^3 + 161103168*a^3*b^3 + 153389376*a^2*b^3 + 50272704*a*b^3 + 13307904*a^4 + 1679616*a^4*b^4 + 2239488*a^3*b^4 + 1119744*a^2*b^4 + 248832*a*b^4 + 20736*b^4 + 5538240*b^3 + 377117820*b^2 + 3935542124*a + 978182025*b + 646873164, 1) evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1) (4464*a^2*b + 59178*a*b + 3648*a^2 + 1296*a^2*b^2 + 864*a*b^2 + 144*b^2 + 77368*a + 19230*b + 25384, 1) evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e) (18*a*b + 6*b + 24*a + 8, 1) evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e) (6*a + 2, 1) evalfbb9in(a, b, c, d, e) -> evalfbb10in(a, b - 1, c, d, e) start location: evalfstart leaf cost: 2 Complexity upper bound 7871239044*a + 11971777242*a*b + 1956402522*b + 19048810500*a^2*b + 12342906160*a^2 + 7748780184*a^2*b^2 + 4684436784*a*b^2 + 754235928*b^2 + 2245017312*a^3*b + 1128961152*a^3 + 1470368160*a^3*b^2 + 58765824*a^4*b^2 + 65138688*a^4*b + 23141376*a^4*b^3 + 322206336*a^3*b^3 + 306778752*a^2*b^3 + 100545408*a*b^3 + 26615808*a^4 + 3359232*a^4*b^4 + 4478976*a^3*b^4 + 2239488*a^2*b^4 + 497664*a*b^4 + 41472*b^4 + 11076480*b^3 + 1293797120 Time: 0.501 sec (SMT: 0.446 sec)