YES(?, 159238928*b + 242186848*b^2 + 130745520*b^3 + 32197824*b^4 + 165888*b^6 + 3732480*b^5 + 33517630) 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(1, b, c, d, e) (?, 1) evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ] (?, 1) evalfbb10in(a, b, c, d, e) -> evalfreturnin(a, b, c, d, e) [ a >= b + 1 ] (?, 1) evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ] (?, 1) evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ] (?, 1) evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ] (?, 1) evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 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) 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(1, b, c, d, e) (?, 1) evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ] (?, 1) evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ] (?, 1) evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ] (?, 1) evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ] (?, 1) evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 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) 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(1, b, c, d, e) (?, 1) evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ] (?, 1) evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ] (?, 1) evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ] (?, 1) evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ] (?, 1) evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 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) start location: evalfstart leaf cost: 2 A polynomial rank function with Pol(evalfstart) = 2*V_2 - 1 Pol(evalfentryin) = 2*V_2 - 1 Pol(evalfbb10in) = -2*V_1 + 2*V_2 + 1 Pol(evalfbb8in) = -2*V_1 + 2*V_2 Pol(evalfbb6in) = -2*V_1 + 2*V_2 Pol(evalfbb4in) = -2*V_1 + 2*V_2 Pol(evalfbb7in) = -2*V_1 + 2*V_2 Pol(evalfbb3in) = -2*V_1 + 2*V_2 Pol(evalfbb5in) = -2*V_1 + 2*V_2 orients all transitions weakly and the transition evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ] 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(1, b, c, d, e) (2*b + 1, 1) evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ] (?, 1) evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ] (?, 1) evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ] (?, 1) evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ] (?, 1) evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 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) start location: evalfstart leaf cost: 2 A polynomial rank function with Pol(evalfbb8in) = 1 Pol(evalfbb6in) = 1 Pol(evalfbb10in) = 0 Pol(evalfbb7in) = 1 Pol(evalfbb4in) = 1 Pol(evalfbb5in) = 1 Pol(evalfbb3in) = 1 and size complexities S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-0) = ? S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-1) = b 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) = ? S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-1) = b 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) = ? S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-1) = b 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) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-1) = b 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) = ? S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-1) = b 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 + 1 ]", 0-0) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 1 ]", 0-1) = b S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 1 ]", 0-2) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 1 ]", 0-3) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 1 ]", 0-4) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ]", 0-0) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ]", 0-1) = b S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ]", 0-2) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ]", 0-3) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ]", 0-4) = 1 S("evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ]", 0-0) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ]", 0-1) = b S("evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ]", 0-2) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ]", 0-3) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ]", 0-4) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ]", 0-0) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ]", 0-1) = b S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ]", 0-2) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ]", 0-3) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ]", 0-4) = ? S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ]", 0-0) = ? S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ]", 0-1) = b S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ]", 0-2) = 1 S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ]", 0-3) = ? S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ]", 0-4) = ? S("evalfentryin(a, b, c, d, e) -> evalfbb10in(1, b, c, d, e)", 0-0) = 1 S("evalfentryin(a, b, c, d, e) -> evalfbb10in(1, b, c, d, e)", 0-1) = b S("evalfentryin(a, b, c, d, e) -> evalfbb10in(1, b, c, d, e)", 0-2) = c S("evalfentryin(a, b, c, d, e) -> evalfbb10in(1, b, c, d, e)", 0-3) = d S("evalfentryin(a, b, c, d, e) -> evalfbb10in(1, b, 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, a + 1, e) [ a >= c ] evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ] 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 + 1 ] evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= 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) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ] 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(1, b, c, d, e) (2*b + 1, 1) evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ] (?, 1) evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ] (2*b + 1, 1) evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ] (?, 1) evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ] (?, 1) evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 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) 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("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-0) = 2*b + 8 S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-1) = b 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) = 2*b + 8 S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-1) = b 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) = 2*b + 8 S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-1) = b 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) = 2*b + 8 S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-1) = b 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) = 2*b + 8 S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-1) = b 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 + 1 ]", 0-0) = 2*b + 8 S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 1 ]", 0-1) = b S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 1 ]", 0-2) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 1 ]", 0-3) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 1 ]", 0-4) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ]", 0-0) = 2*b + 8 S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ]", 0-1) = b S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ]", 0-2) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ]", 0-3) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ]", 0-4) = 1 S("evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ]", 0-0) = 2*b + 8 S("evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ]", 0-1) = b S("evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ]", 0-2) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ]", 0-3) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ]", 0-4) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ]", 0-0) = 2*b + 8 S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ]", 0-1) = b S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ]", 0-2) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ]", 0-3) = 2*b + 18 S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ]", 0-4) = ? S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ]", 0-0) = 2*b + 8 S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ]", 0-1) = b S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ]", 0-2) = 1 S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ]", 0-3) = ? S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ]", 0-4) = ? S("evalfentryin(a, b, c, d, e) -> evalfbb10in(1, b, c, d, e)", 0-0) = 1 S("evalfentryin(a, b, c, d, e) -> evalfbb10in(1, b, c, d, e)", 0-1) = b S("evalfentryin(a, b, c, d, e) -> evalfbb10in(1, b, c, d, e)", 0-2) = c S("evalfentryin(a, b, c, d, e) -> evalfbb10in(1, b, c, d, e)", 0-3) = d S("evalfentryin(a, b, c, d, e) -> evalfbb10in(1, b, 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, a + 1, 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 + 1 ] evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= 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, a + 1, e) [ a >= c ] 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(1, b, c, d, e) (2*b + 1, 1) evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ] (12*b^2 + 62*b + 28, 1) evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ] (2*b + 1, 1) evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ] (?, 1) evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ] (?, 1) evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 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) 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("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-0) = 2*b + 8 S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-1) = b 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) = 2*b + 8 S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-1) = b 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) = 2*b + 8 S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-1) = b 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) = 2*b + 8 S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-1) = b 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) = 2*b + 8 S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-1) = b 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 + 1 ]", 0-0) = 2*b + 8 S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 1 ]", 0-1) = b S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 1 ]", 0-2) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 1 ]", 0-3) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 1 ]", 0-4) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ]", 0-0) = 2*b + 8 S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ]", 0-1) = b S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ]", 0-2) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ]", 0-3) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ]", 0-4) = 1 S("evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ]", 0-0) = 2*b + 8 S("evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ]", 0-1) = b S("evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ]", 0-2) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ]", 0-3) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ]", 0-4) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ]", 0-0) = 2*b + 8 S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ]", 0-1) = b S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ]", 0-2) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ]", 0-3) = 2*b + 18 S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ]", 0-4) = ? S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ]", 0-0) = 2*b + 8 S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ]", 0-1) = b S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ]", 0-2) = 1 S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ]", 0-3) = ? S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ]", 0-4) = ? S("evalfentryin(a, b, c, d, e) -> evalfbb10in(1, b, c, d, e)", 0-0) = 1 S("evalfentryin(a, b, c, d, e) -> evalfbb10in(1, b, c, d, e)", 0-1) = b S("evalfentryin(a, b, c, d, e) -> evalfbb10in(1, b, c, d, e)", 0-2) = c S("evalfentryin(a, b, c, d, e) -> evalfbb10in(1, b, c, d, e)", 0-3) = d S("evalfentryin(a, b, c, d, e) -> evalfbb10in(1, b, 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 + 1 ] evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= 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: 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(1, b, c, d, e) (2*b + 1, 1) evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ] (12*b^2 + 62*b + 28, 1) evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ] (2*b + 1, 1) evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ] (?, 1) evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ] (?, 1) evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 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) (24*b^2 + 124*b + 56, 1) evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, 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("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-0) = 2*b + 8 S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-1) = b S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-2) = 24*b^2 + 124*b + 57 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) = 2*b + 8 S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-1) = b S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-2) = 24*b^2 + 124*b + 57 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) = 2*b + 8 S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-1) = b S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-2) = 24*b^2 + 124*b + 57 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) = 2*b + 8 S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-1) = b S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-2) = 24*b^2 + 124*b + 57 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) = 2*b + 8 S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-1) = b S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-2) = 24*b^2 + 124*b + 57 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 + 1 ]", 0-0) = 2*b + 8 S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 1 ]", 0-1) = b S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 1 ]", 0-2) = 24*b^2 + 124*b + 57 S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 1 ]", 0-3) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 1 ]", 0-4) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ]", 0-0) = 2*b + 8 S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ]", 0-1) = b S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ]", 0-2) = 24*b^2 + 124*b + 57 S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ]", 0-3) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ]", 0-4) = 1 S("evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ]", 0-0) = 2*b + 8 S("evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ]", 0-1) = b S("evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ]", 0-2) = 24*b^2 + 124*b + 57 S("evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ]", 0-3) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ]", 0-4) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ]", 0-0) = 2*b + 8 S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ]", 0-1) = b S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ]", 0-2) = 24*b^2 + 124*b + 57 S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ]", 0-3) = 2*b + 18 S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ]", 0-4) = ? S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ]", 0-0) = 2*b + 8 S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ]", 0-1) = b S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ]", 0-2) = 1 S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ]", 0-3) = ? S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ]", 0-4) = ? S("evalfentryin(a, b, c, d, e) -> evalfbb10in(1, b, c, d, e)", 0-0) = 1 S("evalfentryin(a, b, c, d, e) -> evalfbb10in(1, b, c, d, e)", 0-1) = b S("evalfentryin(a, b, c, d, e) -> evalfbb10in(1, b, c, d, e)", 0-2) = c S("evalfentryin(a, b, c, d, e) -> evalfbb10in(1, b, c, d, e)", 0-3) = d S("evalfentryin(a, b, c, d, e) -> evalfbb10in(1, b, 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 + 1 ] evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= 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 + 1 ] 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(1, b, c, d, e) (2*b + 1, 1) evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ] (12*b^2 + 62*b + 28, 1) evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ] (2*b + 1, 1) evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ] (?, 1) evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ] (12*b^2 + 62*b + 28, 1) evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 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) (24*b^2 + 124*b + 56, 1) evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e) start location: evalfstart leaf cost: 2 A polynomial rank function with Pol(evalfbb6in) = 4*V_2 - 4*V_4 + 1 Pol(evalfbb4in) = 4*V_2 - 4*V_4 - 1 Pol(evalfbb5in) = 4*V_2 - 4*V_4 - 2 Pol(evalfbb3in) = 4*V_2 - 4*V_4 - 1 and size complexities S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-0) = 2*b + 8 S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-1) = b S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-2) = 24*b^2 + 124*b + 57 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) = 2*b + 8 S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-1) = b S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-2) = 24*b^2 + 124*b + 57 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) = 2*b + 8 S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-1) = b S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-2) = 24*b^2 + 124*b + 57 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) = 2*b + 8 S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-1) = b S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-2) = 24*b^2 + 124*b + 57 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) = 2*b + 8 S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-1) = b S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-2) = 24*b^2 + 124*b + 57 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 + 1 ]", 0-0) = 2*b + 8 S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 1 ]", 0-1) = b S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 1 ]", 0-2) = 24*b^2 + 124*b + 57 S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 1 ]", 0-3) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 1 ]", 0-4) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ]", 0-0) = 2*b + 8 S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ]", 0-1) = b S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ]", 0-2) = 24*b^2 + 124*b + 57 S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ]", 0-3) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ]", 0-4) = 1 S("evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ]", 0-0) = 2*b + 8 S("evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ]", 0-1) = b S("evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ]", 0-2) = 24*b^2 + 124*b + 57 S("evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ]", 0-3) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ]", 0-4) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ]", 0-0) = 2*b + 8 S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ]", 0-1) = b S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ]", 0-2) = 24*b^2 + 124*b + 57 S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ]", 0-3) = 2*b + 18 S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ]", 0-4) = ? S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ]", 0-0) = 2*b + 8 S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ]", 0-1) = b S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ]", 0-2) = 1 S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ]", 0-3) = ? S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ]", 0-4) = ? S("evalfentryin(a, b, c, d, e) -> evalfbb10in(1, b, c, d, e)", 0-0) = 1 S("evalfentryin(a, b, c, d, e) -> evalfbb10in(1, b, c, d, e)", 0-1) = b S("evalfentryin(a, b, c, d, e) -> evalfbb10in(1, b, c, d, e)", 0-2) = c S("evalfentryin(a, b, c, d, e) -> evalfbb10in(1, b, c, d, e)", 0-3) = d S("evalfentryin(a, b, c, d, e) -> evalfbb10in(1, b, 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 >= 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 >= d ] 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(1, b, c, d, e) (2*b + 1, 1) evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ] (12*b^2 + 62*b + 28, 1) evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ] (2*b + 1, 1) evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ] (144*b^3 + 1620*b^2 + 4862*b + 2044, 1) evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ] (12*b^2 + 62*b + 28, 1) evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 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) (24*b^2 + 124*b + 56, 1) evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, 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("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-0) = 2*b + 8 S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-1) = b S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-2) = 24*b^2 + 124*b + 57 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) = 2*b + 8 S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-1) = b S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-2) = 24*b^2 + 124*b + 57 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) = 2*b + 8 S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-1) = b S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-2) = 24*b^2 + 124*b + 57 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) = 2*b + 8 S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-1) = b S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-2) = 24*b^2 + 124*b + 57 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) = 2*b + 8 S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-1) = b S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-2) = 24*b^2 + 124*b + 57 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 + 1 ]", 0-0) = 2*b + 8 S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 1 ]", 0-1) = b S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 1 ]", 0-2) = 24*b^2 + 124*b + 57 S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 1 ]", 0-3) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 1 ]", 0-4) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ]", 0-0) = 2*b + 8 S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ]", 0-1) = b S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ]", 0-2) = 24*b^2 + 124*b + 57 S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ]", 0-3) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ]", 0-4) = 1 S("evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ]", 0-0) = 2*b + 8 S("evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ]", 0-1) = b S("evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ]", 0-2) = 24*b^2 + 124*b + 57 S("evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ]", 0-3) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ]", 0-4) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ]", 0-0) = 2*b + 8 S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ]", 0-1) = b S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ]", 0-2) = 24*b^2 + 124*b + 57 S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ]", 0-3) = 2*b + 18 S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ]", 0-4) = ? S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ]", 0-0) = 2*b + 8 S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ]", 0-1) = b S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ]", 0-2) = 1 S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ]", 0-3) = ? S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ]", 0-4) = ? S("evalfentryin(a, b, c, d, e) -> evalfbb10in(1, b, c, d, e)", 0-0) = 1 S("evalfentryin(a, b, c, d, e) -> evalfbb10in(1, b, c, d, e)", 0-1) = b S("evalfentryin(a, b, c, d, e) -> evalfbb10in(1, b, c, d, e)", 0-2) = c S("evalfentryin(a, b, c, d, e) -> evalfbb10in(1, b, c, d, e)", 0-3) = d S("evalfentryin(a, b, c, d, e) -> evalfbb10in(1, b, 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: 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(1, b, c, d, e) (2*b + 1, 1) evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ] (12*b^2 + 62*b + 28, 1) evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ] (2*b + 1, 1) evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ] (144*b^3 + 1620*b^2 + 4862*b + 2044, 1) evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ] (12*b^2 + 62*b + 28, 1) evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 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) (288*b^3 + 3240*b^2 + 9724*b + 4088, 1) evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e) (24*b^2 + 124*b + 56, 1) evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, 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("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-0) = 2*b + 8 S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-1) = b S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-2) = 24*b^2 + 124*b + 57 S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-3) = 9725*b + 288*b^3 + 3240*b^2 + 4097 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) = 2*b + 8 S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-1) = b S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-2) = 24*b^2 + 124*b + 57 S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-3) = 9725*b + 288*b^3 + 3240*b^2 + 4097 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) = 2*b + 8 S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-1) = b S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-2) = 24*b^2 + 124*b + 57 S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-3) = 9725*b + 288*b^3 + 3240*b^2 + 4097 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) = 2*b + 8 S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-1) = b S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-2) = 24*b^2 + 124*b + 57 S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-3) = 9725*b + 288*b^3 + 3240*b^2 + 4097 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) = 2*b + 8 S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-1) = b S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-2) = 24*b^2 + 124*b + 57 S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-3) = 9725*b + 288*b^3 + 3240*b^2 + 4097 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 + 1 ]", 0-0) = 2*b + 8 S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 1 ]", 0-1) = b S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 1 ]", 0-2) = 24*b^2 + 124*b + 57 S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 1 ]", 0-3) = 9725*b + 288*b^3 + 3240*b^2 + 4097 S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 1 ]", 0-4) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ]", 0-0) = 2*b + 8 S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ]", 0-1) = b S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ]", 0-2) = 24*b^2 + 124*b + 57 S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ]", 0-3) = 9725*b + 288*b^3 + 3240*b^2 + 4097 S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ]", 0-4) = 1 S("evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ]", 0-0) = 2*b + 8 S("evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ]", 0-1) = b S("evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ]", 0-2) = 24*b^2 + 124*b + 57 S("evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ]", 0-3) = d + 9725*b + 288*b^3 + 3240*b^2 + 4097 S("evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ]", 0-4) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ]", 0-0) = 2*b + 8 S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ]", 0-1) = b S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ]", 0-2) = 24*b^2 + 124*b + 57 S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ]", 0-3) = 2*b + 18 S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ]", 0-4) = ? S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ]", 0-0) = 2*b + 8 S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ]", 0-1) = b S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ]", 0-2) = 1 S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ]", 0-3) = d + 9725*b + 288*b^3 + 3240*b^2 + 4097 S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ]", 0-4) = ? S("evalfentryin(a, b, c, d, e) -> evalfbb10in(1, b, c, d, e)", 0-0) = 1 S("evalfentryin(a, b, c, d, e) -> evalfbb10in(1, b, c, d, e)", 0-1) = b S("evalfentryin(a, b, c, d, e) -> evalfbb10in(1, b, c, d, e)", 0-2) = c S("evalfentryin(a, b, c, d, e) -> evalfbb10in(1, b, c, d, e)", 0-3) = d S("evalfentryin(a, b, c, d, e) -> evalfbb10in(1, b, 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: 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(1, b, c, d, e) (2*b + 1, 1) evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ] (12*b^2 + 62*b + 28, 1) evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ] (2*b + 1, 1) evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ] (144*b^3 + 1620*b^2 + 4862*b + 2044, 1) evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ] (12*b^2 + 62*b + 28, 1) evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 1 ] (?, 1) evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ] (144*b^3 + 1620*b^2 + 4862*b + 2044, 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) (288*b^3 + 3240*b^2 + 9724*b + 4088, 1) evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e) (24*b^2 + 124*b + 56, 1) evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, 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("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-0) = 2*b + 8 S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-1) = b S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-2) = 24*b^2 + 124*b + 57 S("evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e)", 0-3) = 9725*b + 288*b^3 + 3240*b^2 + 4097 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) = 2*b + 8 S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-1) = b S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-2) = 24*b^2 + 124*b + 57 S("evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e)", 0-3) = 9725*b + 288*b^3 + 3240*b^2 + 4097 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) = 2*b + 8 S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-1) = b S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-2) = 24*b^2 + 124*b + 57 S("evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1)", 0-3) = 9725*b + 288*b^3 + 3240*b^2 + 4097 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) = 2*b + 8 S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-1) = b S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-2) = 24*b^2 + 124*b + 57 S("evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ]", 0-3) = 9725*b + 288*b^3 + 3240*b^2 + 4097 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) = 2*b + 8 S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-1) = b S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-2) = 24*b^2 + 124*b + 57 S("evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ]", 0-3) = 9725*b + 288*b^3 + 3240*b^2 + 4097 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 + 1 ]", 0-0) = 2*b + 8 S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 1 ]", 0-1) = b S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 1 ]", 0-2) = 24*b^2 + 124*b + 57 S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 1 ]", 0-3) = 9725*b + 288*b^3 + 3240*b^2 + 4097 S("evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 1 ]", 0-4) = ? S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ]", 0-0) = 2*b + 8 S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ]", 0-1) = b S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ]", 0-2) = 24*b^2 + 124*b + 57 S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ]", 0-3) = 9725*b + 288*b^3 + 3240*b^2 + 4097 S("evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ]", 0-4) = 1 S("evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ]", 0-0) = 2*b + 8 S("evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ]", 0-1) = b S("evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ]", 0-2) = 24*b^2 + 124*b + 57 S("evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ]", 0-3) = d + 9725*b + 288*b^3 + 3240*b^2 + 4097 S("evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ]", 0-4) = ? S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ]", 0-0) = 2*b + 8 S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ]", 0-1) = b S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ]", 0-2) = 24*b^2 + 124*b + 57 S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ]", 0-3) = 2*b + 18 S("evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ]", 0-4) = ? S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ]", 0-0) = 2*b + 8 S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ]", 0-1) = b S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ]", 0-2) = 1 S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ]", 0-3) = d + 9725*b + 288*b^3 + 3240*b^2 + 4097 S("evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ]", 0-4) = ? S("evalfentryin(a, b, c, d, e) -> evalfbb10in(1, b, c, d, e)", 0-0) = 1 S("evalfentryin(a, b, c, d, e) -> evalfbb10in(1, b, c, d, e)", 0-1) = b S("evalfentryin(a, b, c, d, e) -> evalfbb10in(1, b, c, d, e)", 0-2) = c S("evalfentryin(a, b, c, d, e) -> evalfbb10in(1, b, c, d, e)", 0-3) = d S("evalfentryin(a, b, c, d, e) -> evalfbb10in(1, b, 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: 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(1, b, c, d, e) (2*b + 1, 1) evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ] (12*b^2 + 62*b + 28, 1) evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ] (2*b + 1, 1) evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ] (144*b^3 + 1620*b^2 + 4862*b + 2044, 1) evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ] (12*b^2 + 62*b + 28, 1) evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 1 ] (16098912*b^4 + 65372472*b^3 + 121090160*b^2 + 82944*b^6 + 1866240*b^5 + 79609614*b + 16754668, 1) evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ] (144*b^3 + 1620*b^2 + 4862*b + 2044, 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) (288*b^3 + 3240*b^2 + 9724*b + 4088, 1) evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e) (24*b^2 + 124*b + 56, 1) evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e) start location: evalfstart leaf cost: 2 Repeatedly propagating knowledge in problem 12 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(1, b, c, d, e) (2*b + 1, 1) evalfbb10in(a, b, c, d, e) -> evalfbb8in(a, b, 1, d, e) [ b >= a ] (12*b^2 + 62*b + 28, 1) evalfbb8in(a, b, c, d, e) -> evalfbb6in(a, b, c, a + 1, e) [ a >= c ] (2*b + 1, 1) evalfbb8in(a, b, c, d, e) -> evalfbb10in(a + 1, b, c, d, e) [ c >= a + 1 ] (144*b^3 + 1620*b^2 + 4862*b + 2044, 1) evalfbb6in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, 1) [ b >= d ] (12*b^2 + 62*b + 28, 1) evalfbb6in(a, b, c, d, e) -> evalfbb7in(a, b, c, d, e) [ d >= b + 1 ] (16098912*b^4 + 65372472*b^3 + 121090160*b^2 + 82944*b^6 + 1866240*b^5 + 79609614*b + 16754668, 1) evalfbb4in(a, b, c, d, e) -> evalfbb3in(a, b, c, d, e) [ d >= e ] (144*b^3 + 1620*b^2 + 4862*b + 2044, 1) evalfbb4in(a, b, c, d, e) -> evalfbb5in(a, b, c, d, e) [ e >= d + 1 ] (16098912*b^4 + 65372472*b^3 + 121090160*b^2 + 82944*b^6 + 1866240*b^5 + 79609614*b + 16754668, 1) evalfbb3in(a, b, c, d, e) -> evalfbb4in(a, b, c, d, e + 1) (288*b^3 + 3240*b^2 + 9724*b + 4088, 1) evalfbb5in(a, b, c, d, e) -> evalfbb6in(a, b, c, d + 1, e) (24*b^2 + 124*b + 56, 1) evalfbb7in(a, b, c, d, e) -> evalfbb8in(a, b, c + 1, d, e) start location: evalfstart leaf cost: 2 Complexity upper bound 159238928*b + 242186848*b^2 + 130745520*b^3 + 32197824*b^4 + 165888*b^6 + 3732480*b^5 + 33517630 Time: 0.474 sec (SMT: 0.426 sec)